lemma
proved
tactic proof
neg_one_zpow_sq
show as:
view Lean formalization →
formal statement (Lean)
127private lemma neg_one_zpow_sq (n : ℤ) : ((-1 : ℝ) ^ n) ^ 2 = 1 := by
proof body
Tactic-mode proof.
128 have h : (-1 : ℝ) * (-1 : ℝ) = 1 := by norm_num
129 calc ((-1 : ℝ) ^ n) ^ 2 = ((-1 : ℝ) ^ n * (-1 : ℝ) ^ n) := sq _
130 _ = ((-1 : ℝ) * (-1 : ℝ)) ^ n := (mul_zpow (-1) (-1) n).symm
131 _ = 1 ^ n := by rw [h]
132 _ = 1 := one_zpow n
133
134/-- cos(nπ)² = 1 for any integer n. -/