n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]
n b : ℕ
h : 1 ≤ b
⊢ ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]
have : 1 ≤ b ^ (n - 1) := one_le_pow_of_one_le h (n - 1)
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ 1 ≡ b ^ (n - 1) [MOD n]
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]
rw [Nat.ModEq.comm]
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b → 1 ≡ b ^ (n - 1) [MOD n]

case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → ProbablePrime n b
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ 1 ≡ b ^ (n - 1) [MOD n]
constructor
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ 1 ≡ b ^ (n - 1) [MOD n]
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b → 1 ≡ b ^ (n - 1) [MOD n]
intro h₁
case mp.a
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ ↑n ∣ ↑(b ^ (n - 1)) - ↑1
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ 1 ≡ b ^ (n - 1) [MOD n]
apply Nat.modEq_of_dvd
no goals
case mp.a
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ ↑n ∣ ↑(b ^ (n - 1)) - ↑1
exact_mod_cast h₁
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ ProbablePrime n b
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → ProbablePrime n b
intro h₁
no goals
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ ProbablePrime n b
exact_mod_cast Nat.ModEq.dvd h₁