n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
n : ℕ
hn : 2 < n
⊢ Even (φ n)
haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
haveI : NeZero n := NeZero.of_gt hn
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
suffices 2 = orderOf (-1 : (ZMod n)ˣ) by
  rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
  exact orderOf_dvd_card_univ
no goals
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)
rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
no goals
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ
exact orderOf_dvd_card_univ