standard way to show real.cos(π / 7) + 1 ≠ 0

Stream: new members

[wendy shang]

Hi everyone, I have a noob question. What would be considered the standard way to solve real.cos(π / 7) + 1 ≠ 0?

some half-baked steps that I wrote down:

lemma pi_seven_not_neg_1: real.cos(π / 7) + 1 ≠ 0 :=
begin
  have p: -real.cos(π / 7) ≠ 1, {
  rw <-real.cos_add_pi,
  have pp: π / 7 +  π = 8 * π / 7 := by linarith,
  rw pp,
  have ppp: 8 * π / 7 = 4 / 7 * (2 *  π ) := by linarith,
  --likely I need to use real.cos_eq_one_iff somehow...
  }
end

Thank you very much!

[Eric Wieser]

Can you edit your message to use #backticks?

[Patrick Johnson]

import analysis.special_functions.trigonometric.basic
open_locale real

example : real.cos (π / 7) + 1 ≠ 0 :=
by linarith [real.cos_pi, @real.cos_lt_cos_of_nonneg_of_le_pi
  (π / 7) π (by linarith [le_of_lt real.pi_pos])
  (by refl) (by linarith [real.pi_pos])]