[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ Nat.Prime p
[PROOFSTEP]
have h0 : p ≠ 0 := by
  rintro ⟨⟩
  exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
a : ZMod 0
ha : a ^ (0 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 0 - 1 → a ^ ((0 - 1) / q) ≠ 1
⊢ False
[PROOFSTEP]
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
⊢ Nat.Prime p
[PROOFSTEP]
have h1 : p ≠ 1 := by
  rintro ⟨⟩
  exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
⊢ p ≠ 1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
a : ZMod 1
ha : a ^ (1 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 1 - 1 → a ^ ((1 - 1) / q) ≠ 1
h0 : 1 ≠ 0
⊢ False
[PROOFSTEP]
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
⊢ Nat.Prime p
[PROOFSTEP]
have hp1 : 1 < p := lt_of_le_of_ne h0.bot_lt h1.symm
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ Nat.Prime p
[PROOFSTEP]
have order_of_a : orderOf a = p - 1 :=
  by
  apply orderOf_eq_of_pow_and_pow_div_prime _ ha hd
  exact tsub_pos_of_lt hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ orderOf a = p - 1
[PROOFSTEP]
apply orderOf_eq_of_pow_and_pow_div_prime _ ha hd
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ 0 < p - 1
[PROOFSTEP]
exact tsub_pos_of_lt hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
⊢ Nat.Prime p
[PROOFSTEP]
haveI : NeZero p := ⟨h0⟩
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ Nat.Prime p
[PROOFSTEP]
rw [Nat.prime_iff_card_units]
  -- Prove cardinality of `Units` of `ZMod p` is both `≤ p-1` and `≥ p-1`
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
refine' le_antisymm (Nat.card_units_zmod_lt_sub_one hp1) _
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
have hp' : p - 2 + 1 = p - 1 := tsub_add_eq_add_tsub hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - 2)) (by rw [← pow_succ, hp', ha])
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
⊢ a * a ^ (p - 2) = 1
[PROOFSTEP]
rw [← pow_succ, hp', ha]
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
a' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - 2)) (_ : a * a ^ (p - 2) = 1)
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
calc
  p - 1 = orderOf a := order_of_a.symm
  _ = orderOf a' := (orderOf_injective (Units.coeHom (ZMod p)) Units.ext a')
  _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ
