[GOAL]
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
⊢ coprime n b
[PROOFSTEP]
by_cases h₃ : 2 ≤ n
[GOAL]
case pos
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ coprime n b
[PROOFSTEP]
apply Nat.coprime_of_dvd
[GOAL]
case pos.H
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b
[PROOFSTEP]
rintro k hk ⟨m, rfl⟩
  ⟨j, rfl⟩
      -- Because prime numbers do not divide 1, it suffices to show that `k ∣ 1` to prove a
          -- contradiction
[GOAL]
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ False
[PROOFSTEP]
apply Nat.Prime.not_dvd_one hk
[GOAL]
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ k ∣ 1
[PROOFSTEP]
replace h := dvd_of_mul_right_dvd h
[GOAL]
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1
[PROOFSTEP]
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
  -- Since `k` divides `b`, `k` also divides any power of `b` except `b ^ 0`. Therefore, it
      -- suffices to show that `n - 1` isn't zero. However, we know that `n - 1` isn't zero because we
      -- assumed `2 ≤ n` when doing `by_cases`.
[GOAL]
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
[PROOFSTEP]
refine' dvd_of_mul_right_dvd (dvd_pow_self (k * j) _)
[GOAL]
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0
[PROOFSTEP]
linarith [tsub_pos_of_lt (one_lt_two.trans_le h₃)]
  -- If `n = 1`, then it follows trivially that `n` is coprime with `b`.
[GOAL]
case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ coprime n b
[PROOFSTEP]
rw [show n = 1 by linarith]
[GOAL]
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n = 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ coprime 1 b
[PROOFSTEP]
norm_num
[GOAL]
n b : ℕ
h : 1 ≤ b
⊢ ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]
[PROOFSTEP]
have : 1 ≤ b ^ (n - 1) :=
  one_le_pow_of_one_le h
    (n - 1)
      -- For exact_mod_cast
[GOAL]
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]
[PROOFSTEP]
rw [Nat.ModEq.comm]
[GOAL]
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b ↔ 1 ≡ b ^ (n - 1) [MOD n]
[PROOFSTEP]
constructor
[GOAL]
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ ProbablePrime n b → 1 ≡ b ^ (n - 1) [MOD n]
[PROOFSTEP]
intro h₁
[GOAL]
case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ 1 ≡ b ^ (n - 1) [MOD n]
[PROOFSTEP]
apply Nat.modEq_of_dvd
[GOAL]
case mp.a
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : ProbablePrime n b
⊢ ↑n ∣ ↑(b ^ (n - 1)) - ↑1
[PROOFSTEP]
exact_mod_cast h₁
[GOAL]
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → ProbablePrime n b
[PROOFSTEP]
intro h₁
[GOAL]
case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ ProbablePrime n b
[PROOFSTEP]
exact_mod_cast Nat.ModEq.dvd h₁
[GOAL]
n b : ℕ
h : FermatPsp n b
h₁ : 1 ≤ b
⊢ coprime n b
[PROOFSTEP]
rcases h with ⟨hp, _, hn₂⟩
[GOAL]
case intro.intro
n b : ℕ
h₁ : 1 ≤ b
hp : ProbablePrime n b
left✝ : ¬Prime n
hn₂ : 1 < n
⊢ coprime n b
[PROOFSTEP]
exact coprime_of_probablePrime hp (by linarith) h₁
[GOAL]
n b : ℕ
h₁ : 1 ≤ b
hp : ProbablePrime n b
left✝ : ¬Prime n
hn₂ : 1 < n
⊢ 1 ≤ n
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ FermatPsp n 1
[PROOFSTEP]
refine' ⟨show n ∣ 1 ^ (n - 1) - 1 from _, h₂, h₁⟩
[GOAL]
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n ∣ 1 ^ (n - 1) - 1
[PROOFSTEP]
exact show 0 = 1 ^ (n - 1) - 1 by norm_num ▸ dvd_zero n
[GOAL]
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ 0 = 1 ^ (n - 1) - 1
[PROOFSTEP]
norm_num
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ 2 ≤ (a ^ b - 1) / (a - 1)
[PROOFSTEP]
change 1 < _
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ 1 < (a ^ b - 1) / (a - 1)
[PROOFSTEP]
have h₁ : a - 1 ∣ a ^ b - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow a 1 b
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ a - 1 ∣ a ^ b - 1
[PROOFSTEP]
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow a 1 b
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ 1 < (a ^ b - 1) / (a - 1)
[PROOFSTEP]
rw [Nat.lt_div_iff_mul_lt h₁, mul_one, tsub_lt_tsub_iff_right (Nat.le_of_succ_le ha)]
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ a < a ^ b
[PROOFSTEP]
convert pow_lt_pow (Nat.lt_of_succ_le ha) hb
[GOAL]
case h.e'_3
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ a = a ^ 1
[PROOFSTEP]
rw [pow_one]
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 ≤ (a ^ b + 1) / (a + 1)
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le (Nat.zero_lt_succ _)]
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * succ a ≤ a ^ b + 1
[PROOFSTEP]
apply Nat.succ_le_succ
[GOAL]
case a
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ Nat.mul 2 a + 1 ≤ a ^ b
[PROOFSTEP]
calc
  2 * a + 1 ≤ a ^ 2 * a := by nlinarith
  _ = a ^ 3 := by rw [pow_succ a 2]
  _ ≤ a ^ b := pow_le_pow (Nat.le_of_succ_le ha) hb
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a + 1 ≤ a ^ 2 * a
[PROOFSTEP]
nlinarith
[GOAL]
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ a ^ 2 * a = a ^ 3
[PROOFSTEP]
rw [pow_succ a 2]
[GOAL]
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
have q₁ : b - 1 ∣ b ^ p - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p
[GOAL]
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
⊢ b - 1 ∣ b ^ p - 1
[PROOFSTEP]
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p
[GOAL]
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
have q₂ : b + 1 ∣ b ^ p + 1 := by simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
[GOAL]
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ b + 1 ∣ b ^ p + 1
[PROOFSTEP]
simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
[GOAL]
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
convert Nat.div_mul_div_comm q₁ q₂ using 2
[GOAL]
case h.e'_3.h.e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p - 1) * (b ^ p + 1)
[PROOFSTEP]
rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
[GOAL]
case h.e'_3.h.e'_6
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ 2 - 1 = (b - 1) * (b + 1)
[PROOFSTEP]
rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
[GOAL]
case h.e'_3.h.e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 1 ^ 2
[PROOFSTEP]
ring_nf
[GOAL]
case h.e'_3.h.e'_6
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ 2 - 1 = b ^ 2 - 1 ^ 2
[PROOFSTEP]
simp
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - 1 - (b ^ 2 - 1) = b ^ (2 * p) - (1 + (b ^ 2 - 1))
[PROOFSTEP]
rw [Nat.sub_sub]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + b ^ 2 - 1)
[PROOFSTEP]
rw [Nat.add_sub_assoc hi_bsquared]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + b ^ 2 - 1) = b ^ (2 * p) - b ^ 2
[PROOFSTEP]
rw [Nat.add_sub_cancel_left]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - b ^ 2 = b ^ (p * 2) - b ^ 2
[PROOFSTEP]
rw [mul_comm]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (p * 2) - b ^ 2 = (b ^ p) ^ 2 - b ^ 2
[PROOFSTEP]
rw [pow_mul]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p) ^ 2 - b ^ 2 = (b ^ p + b) * (b ^ p - b)
[PROOFSTEP]
rw [Nat.sq_sub_sq]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)
[PROOFSTEP]
rw [Nat.sub_add_cancel hp]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
[PROOFSTEP]
rw [pow_succ']
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)
[PROOFSTEP]
rw [mul_one]
[GOAL]
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
rw [Nat.mul_sub_left_distrib]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
⊢ FermatPsp (Nat.psp_from_prime b p) b
[PROOFSTEP]
unfold psp_from_prime
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
⊢ FermatPsp ((b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))) b
[PROOFSTEP]
set A := (b ^ p - 1) / (b - 1)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
⊢ FermatPsp (A * ((b ^ p + 1) / (b + 1))) b
[PROOFSTEP]
set B :=
  (b ^ p + 1) /
    (b + 1)
      -- Inequalities
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_A : 1 < A := a_id_helper (Nat.succ_le_iff.mp b_ge_two) (Nat.Prime.one_lt p_prime)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_B : 1 < B := b_id_helper (Nat.succ_le_iff.mp b_ge_two) p_gt_two
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_AB : 1 < A * B := one_lt_mul'' hi_A hi_B
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_b : 0 < b := by linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
⊢ 0 < b
[PROOFSTEP]
linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_p : 1 ≤ p := Nat.one_le_of_lt p_gt_two
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_bsquared : 0 < b ^ 2 - 1 := by
  -- Porting note: was `by nlinarith [Nat.one_le_pow 2 b hi_b]`
  have h0 := mul_le_mul b_ge_two b_ge_two zero_le_two hi_b.le
  have h1 : 1 < 2 * 2 := by linarith
  have := tsub_pos_of_lt (h1.trans_le h0)
  rwa [pow_two]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
⊢ 0 < b ^ 2 - 1
[PROOFSTEP]
have h0 := mul_le_mul b_ge_two b_ge_two zero_le_two hi_b.le
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
h0 : 2 * 2 ≤ b * b
⊢ 0 < b ^ 2 - 1
[PROOFSTEP]
have h1 : 1 < 2 * 2 := by linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
h0 : 2 * 2 ≤ b * b
⊢ 1 < 2 * 2
[PROOFSTEP]
linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
h0 : 2 * 2 ≤ b * b
h1 : 1 < 2 * 2
⊢ 0 < b ^ 2 - 1
[PROOFSTEP]
have := tsub_pos_of_lt (h1.trans_le h0)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
h0 : 2 * 2 ≤ b * b
h1 : 1 < 2 * 2
this : 0 < b * b - 1
⊢ 0 < b ^ 2 - 1
[PROOFSTEP]
rwa [pow_two]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_bpowtwop : 1 ≤ b ^ (2 * p) := Nat.one_le_pow (2 * p) b hi_b
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_b
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have p_odd : Odd p := p_prime.odd_of_ne_two p_gt_two.ne.symm
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have AB_not_prime : ¬Nat.Prime (A * B) := Nat.not_prime_mul hi_A hi_B
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1) := AB_id_helper _ _ b_ge_two p_odd
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ FermatPsp (A * B) b
[PROOFSTEP]
have hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1 := by simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ b ^ 2 - 1 ∣ b ^ (2 * p) - 1
[PROOFSTEP]
simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ FermatPsp (A * B) b
[PROOFSTEP]
refine'
  ⟨_, AB_not_prime, hi_AB⟩
    -- Used to prove that `2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)`.
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b) :=
  by
  apply_fun fun x => x * (b ^ 2 - 1) at AB_id
  rw [Nat.div_mul_cancel hd] at AB_id
  apply_fun fun x => x - (b ^ 2 - 1) at AB_id
  nth_rw 2 [← one_mul (b ^ 2 - 1)] at AB_id
  rw [← Nat.mul_sub_right_distrib, mul_comm] at AB_id
  rw [AB_id]
  exact bp_helper hi_b hi_p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
apply_fun fun x => x * (b ^ 2 - 1) at AB_id
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
rw [Nat.div_mul_cancel hd] at AB_id
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) = b ^ (2 * p) - 1
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
apply_fun fun x => x - (b ^ 2 - 1) at AB_id
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
nth_rw 2 [← one_mul (b ^ 2 - 1)] at AB_id
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - 1 * (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
rw [← Nat.mul_sub_right_distrib, mul_comm] at AB_id
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (b ^ 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
rw [AB_id]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (b ^ 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ b ^ (2 * p) - 1 - (b ^ 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
exact bp_helper hi_b hi_p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₂ : 2 ∣ b ^ p + b := by
  -- Porting note: golfedrw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]
    -- Since `b` isn't divisible by `p`, `b` is coprime with `p`. we can use Fermat's Little Theorem
      -- to prove this.
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 ∣ b ^ p + b
[PROOFSTEP]
rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]
  -- Since `b` isn't divisible by `p`, `b` is coprime with `p`. we can use Fermat's Little Theorem
    -- to prove this.
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₃ : p ∣ b ^ (p - 1) - 1 :=
  by
  have : ¬p ∣ b := mt (fun h : p ∣ b => dvd_mul_of_dvd_left h _) not_dvd
  have : p.coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
  have : IsCoprime (b : ℤ) ↑p := this.symm.isCoprime
  have : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p] := Int.ModEq.pow_card_sub_one_eq_one p_prime this
  have : ↑p ∣ ↑b ^ (p - 1) - ↑1 := by exact_mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
  exact_mod_cast this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : ¬p ∣ b := mt (fun h : p ∣ b => dvd_mul_of_dvd_left h _) not_dvd
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this : ¬p ∣ b
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : p.coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝ : ¬p ∣ b
this : coprime p b
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : IsCoprime (b : ℤ) ↑p := this.symm.isCoprime
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝¹ : ¬p ∣ b
this✝ : coprime p b
this : IsCoprime ↑b ↑p
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p] := Int.ModEq.pow_card_sub_one_eq_one p_prime this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝² : ¬p ∣ b
this✝¹ : coprime p b
this✝ : IsCoprime ↑b ↑p
this : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p]
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : ↑p ∣ ↑b ^ (p - 1) - ↑1 := by exact_mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝² : ¬p ∣ b
this✝¹ : coprime p b
this✝ : IsCoprime ↑b ↑p
this : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p]
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
exact_mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝³ : ¬p ∣ b
this✝² : coprime p b
this✝¹ : IsCoprime ↑b ↑p
this✝ : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p]
this : p ∣ b ^ (p - 1) - 1
⊢ p ∣ b ^ (p - 1) - 1
[PROOFSTEP]
exact_mod_cast this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1 := by
  cases' p_odd with k hk
  have : 2 ∣ p - 1 := ⟨k, by simp [hk]⟩
  cases' this with c hc
  have : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow _ 1 c
  have : b ^ 2 - 1 ∣ b ^ (2 * c) - 1 := by rwa [← pow_mul] at this
  rwa [← hc] at this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
cases' p_odd with k hk
[GOAL]
case intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : 2 ∣ p - 1 := ⟨k, by simp [hk]⟩
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
⊢ p - 1 = 2 * k
[PROOFSTEP]
simp [hk]
[GOAL]
case intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
this : 2 ∣ p - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
cases' this with c hc
[GOAL]
case intro.intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow _ 1 c
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
⊢ b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
[PROOFSTEP]
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow _ 1 c
[GOAL]
case intro.intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
have : b ^ 2 - 1 ∣ b ^ (2 * c) - 1 := by rwa [← pow_mul] at this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
⊢ b ^ 2 - 1 ∣ b ^ (2 * c) - 1
[PROOFSTEP]
rwa [← pow_mul] at this
[GOAL]
case intro.intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this✝ : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
this : b ^ 2 - 1 ∣ b ^ (2 * c) - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
[PROOFSTEP]
rwa [← hc] at this
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1) :=
  by
  suffices q : 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
  ·
    rwa [ha₁]
      -- We already proved that `b ^ 2 - 1 ∣ b ^ (p - 1) - 1`.
          -- Since `2 ∣ b ^ p + b` and `p ∣ b ^ p + b`, if we show that 2 and p are coprime, then we
          -- know that `2 * p ∣ b ^ p + b`
  have q₁ : Nat.coprime p (b ^ 2 - 1) :=
    haveI q₂ : ¬p ∣ b ^ 2 - 1 := by
      rw [mul_comm] at not_dvd
      exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd
    (Nat.Prime.coprime_iff_not_dvd p_prime).mpr q₂
  have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄
  have q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b) := mul_dvd_mul q₂ ha₂
  have q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b)) := dvd_mul_of_dvd_right q₃ _
  rwa [mul_assoc, mul_comm, mul_assoc b]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
[PROOFSTEP]
suffices q : 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q : 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
[PROOFSTEP]
rwa [ha₁]
  -- We already proved that `b ^ 2 - 1 ∣ b ^ (p - 1) - 1`.
      -- Since `2 ∣ b ^ p + b` and `p ∣ b ^ p + b`, if we show that 2 and p are coprime, then we
      -- know that `2 * p ∣ b ^ p + b`
[GOAL]
case q
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
have q₁ : Nat.coprime p (b ^ 2 - 1) :=
  haveI q₂ : ¬p ∣ b ^ 2 - 1 := by
    rw [mul_comm] at not_dvd
    exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd
  (Nat.Prime.coprime_iff_not_dvd p_prime).mpr q₂
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1
[PROOFSTEP]
rw [mul_comm] at not_dvd
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ (b ^ 2 - 1) * b
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1
[PROOFSTEP]
exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd
[GOAL]
case q
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : coprime p (b ^ 2 - 1)
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄
[GOAL]
case q
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : coprime p (b ^ 2 - 1)
q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
have q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b) := mul_dvd_mul q₂ ha₂
[GOAL]
case q
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : coprime p (b ^ 2 - 1)
q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1
q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
have q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b)) := dvd_mul_of_dvd_right q₃ _
[GOAL]
case q
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : coprime p (b ^ 2 - 1)
q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1
q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b)
q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b))
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
[PROOFSTEP]
rwa [mul_assoc, mul_comm, mul_assoc b]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₆ : 2 * p ∣ A * B - 1 := by
  rw [mul_comm] at ha₅
  exact Nat.dvd_of_mul_dvd_mul_left hi_bsquared ha₅
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1
[PROOFSTEP]
rw [mul_comm] at ha₅
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : (b ^ 2 - 1) * (2 * p) ∣ (b ^ 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1
[PROOFSTEP]
exact Nat.dvd_of_mul_dvd_mul_left hi_bsquared ha₅
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₇ : A * B ∣ b ^ (2 * p) - 1 := by
  use b ^ 2 - 1
  have : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1) :=
    congr_arg (fun x : ℕ => x * (b ^ 2 - 1)) AB_id
  simpa only [add_comm, Nat.div_mul_cancel hd, Nat.sub_add_cancel hi_bpowtwop] using this.symm
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
⊢ A * B ∣ b ^ (2 * p) - 1
[PROOFSTEP]
use b ^ 2 - 1
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
⊢ b ^ (2 * p) - 1 = A * B * (b ^ 2 - 1)
[PROOFSTEP]
have : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1) :=
  congr_arg (fun x : ℕ => x * (b ^ 2 - 1)) AB_id
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
this : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1)
⊢ b ^ (2 * p) - 1 = A * B * (b ^ 2 - 1)
[PROOFSTEP]
simpa only [add_comm, Nat.div_mul_cancel hd, Nat.sub_add_cancel hi_bpowtwop] using this.symm
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
ha₇ : A * B ∣ b ^ (2 * p) - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
cases' ha₆ with q hq
[GOAL]
case intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
have ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1 := by
  simpa only [one_pow, pow_mul, hq] using nat_sub_dvd_pow_sub_pow _ 1 q
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1
[PROOFSTEP]
simpa only [one_pow, pow_mul, hq] using nat_sub_dvd_pow_sub_pow _ 1 q
[GOAL]
case intro
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hi_A : 1 < A
hi_B : 1 < B
hi_AB : 1 < A * B
hi_b : 0 < b
hi_p : 1 ≤ p
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1
⊢ ProbablePrime (A * B) b
[PROOFSTEP]
exact dvd_trans ha₇ ha₈
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
⊢ p < Nat.psp_from_prime b p
[PROOFSTEP]
unfold psp_from_prime
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
⊢ p < (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))
[PROOFSTEP]
set A := (b ^ p - 1) / (b - 1)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
⊢ p < A * ((b ^ p + 1) / (b + 1))
[PROOFSTEP]
set B := (b ^ p + 1) / (b + 1)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A * B
[PROOFSTEP]
rw [show A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1) from
    AB_id_helper _ _ b_ge_two (p_prime.odd_of_ne_two p_gt_two.ne.symm)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
have AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1 := by simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ b ^ 2 - 1 ∣ b ^ (2 * p) - 1
[PROOFSTEP]
simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
suffices h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
have h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1) := Nat.div_lt_div_of_lt_of_dvd AB_dvd h
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
have h₂ : 0 < b ^ 2 - 1 := by linarith [show 3 ≤ b ^ 2 - 1 from le_tsub_of_add_le_left (show 4 ≤ b ^ 2 by nlinarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ 0 < b ^ 2 - 1
[PROOFSTEP]
linarith [show 3 ≤ b ^ 2 - 1 from le_tsub_of_add_le_left (show 4 ≤ b ^ 2 by nlinarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ 4 ≤ b ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
h₂ : 0 < b ^ 2 - 1
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
[PROOFSTEP]
rwa [Nat.mul_div_cancel _ h₂] at h₁
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * (b ^ 2 - 1) < b ^ (2 * p) - 1
[PROOFSTEP]
rw [Nat.mul_sub_left_distrib, mul_one, pow_mul]
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ p - 1
[PROOFSTEP]
conv_rhs => rw [← Nat.sub_add_cancel (show 1 ≤ p by linarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
| (b ^ 2) ^ p - 1
[PROOFSTEP]
rw [← Nat.sub_add_cancel (show 1 ≤ p by linarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
| (b ^ 2) ^ p - 1
[PROOFSTEP]
rw [← Nat.sub_add_cancel (show 1 ≤ p by linarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
| (b ^ 2) ^ p - 1
[PROOFSTEP]
rw [← Nat.sub_add_cancel (show 1 ≤ p by linarith)]
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ 1 ≤ p
[PROOFSTEP]
linarith
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ (p - 1 + 1) - 1
[PROOFSTEP]
rw [pow_succ (b ^ 2)]
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ (p - 1) * b ^ 2 - 1
[PROOFSTEP]
suffices h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
⊢ p * b ^ 2 - p < (b ^ 2) ^ (p - 1) * b ^ 2 - 1
[PROOFSTEP]
apply gt_of_ge_of_gt
[GOAL]
case h.h₁
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
⊢ (b ^ 2) ^ (p - 1) * b ^ 2 - 1 ≥ ?h.b
[PROOFSTEP]
exact tsub_le_tsub_left (one_le_of_lt p_gt_two) ((b ^ 2) ^ (p - 1) * b ^ 2)
[GOAL]
case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
⊢ (b ^ 2) ^ (p - 1) * b ^ 2 - p > p * b ^ 2 - p
[PROOFSTEP]
have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right (show 0 < b ^ 2 by nlinarith)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
⊢ 0 < b ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
this : p ≤ p * b ^ 2
⊢ (b ^ 2) ^ (p - 1) * b ^ 2 - p > p * b ^ 2 - p
[PROOFSTEP]
exact tsub_lt_tsub_right_of_le this h
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
[PROOFSTEP]
suffices h : p < (b ^ 2) ^ (p - 1)
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p < (b ^ 2) ^ (p - 1)
⊢ p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
[PROOFSTEP]
have : 4 ≤ b ^ 2 := by nlinarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p < (b ^ 2) ^ (p - 1)
⊢ 4 ≤ b ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p < (b ^ 2) ^ (p - 1)
this : 4 ≤ b ^ 2
⊢ p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
[PROOFSTEP]
have : 0 < b ^ 2 := by linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p < (b ^ 2) ^ (p - 1)
this : 4 ≤ b ^ 2
⊢ 0 < b ^ 2
[PROOFSTEP]
linarith
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p < (b ^ 2) ^ (p - 1)
this✝ : 4 ≤ b ^ 2
this : 0 < b ^ 2
⊢ p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
[PROOFSTEP]
exact mul_lt_mul_of_pos_right h this
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p < (b ^ 2) ^ (p - 1)
[PROOFSTEP]
rw [← pow_mul, Nat.mul_sub_left_distrib, mul_one]
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p < b ^ (2 * p - 2)
[PROOFSTEP]
have : 2 ≤ 2 * p - 2 := le_tsub_of_add_le_left (show 4 ≤ 2 * p by linarith)
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ 4 ≤ 2 * p
[PROOFSTEP]
linarith
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this : 2 ≤ 2 * p - 2
⊢ p < b ^ (2 * p - 2)
[PROOFSTEP]
have : 2 + p ≤ 2 * p := by linarith
[GOAL]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this : 2 ≤ 2 * p - 2
⊢ 2 + p ≤ 2 * p
[PROOFSTEP]
linarith
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this✝ : 2 ≤ 2 * p - 2
this : 2 + p ≤ 2 * p
⊢ p < b ^ (2 * p - 2)
[PROOFSTEP]
have : p ≤ 2 * p - 2 := le_tsub_of_add_le_left this
[GOAL]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this✝¹ : 2 ≤ 2 * p - 2
this✝ : 2 + p ≤ 2 * p
this : p ≤ 2 * p - 2
⊢ p < b ^ (2 * p - 2)
[PROOFSTEP]
exact Nat.lt_of_le_of_lt this (pow_gt_exponent _ b_ge_two)
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
by_cases b_ge_two : 2 ≤ b
[GOAL]
case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)
[GOAL]
case pos
b : ℕ
h✝ : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ p, b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
cases' h with p hp
[GOAL]
case pos.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp : b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
cases' hp with hp₁ hp₂
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₂ : 4 ≤ b ^ 2 := pow_le_pow_of_le_left' b_ge_two 2
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (gt_of_ge_of_gt h₂ (by norm_num))
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ 4 > 1
[PROOFSTEP]
norm_num
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₅ : b * (b ^ 2 - 1) < p := by linarith
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
⊢ b * (b ^ 2 - 1) < p
[PROOFSTEP]
linarith
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right h₃
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₉ : 2 < p := gt_of_gt_of_ge h₅ h₈
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₁₀ := psp_from_prime_gt_p b_ge_two hp₂ h₉
[GOAL]
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
use psp_from_prime b p
[GOAL]
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ FermatPsp (Nat.psp_from_prime b p) b ∧ m ≤ Nat.psp_from_prime b p
[PROOFSTEP]
constructor
[GOAL]
case h.left
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ FermatPsp (Nat.psp_from_prime b p) b
[PROOFSTEP]
exact psp_from_prime_psp b_ge_two hp₂ h₉ h₆
[GOAL]
case h.right
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ m ≤ Nat.psp_from_prime b p
[PROOFSTEP]
exact
  le_trans (show m ≤ p by linarith)
    (le_of_lt h₁₀)
      -- If `¬2 ≤ b`, then `b = 1`. Since all composite numbers are pseudoprimes to base 1, we can pick
        -- any composite number greater than m. We choose `2 * (m + 2)` because it is greater than `m` and
        -- is composite for all natural numbers `m`.
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ m ≤ p
[PROOFSTEP]
linarith
[GOAL]
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
have h₁ : b = 1 := by linarith
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ b = 1
[PROOFSTEP]
linarith
[GOAL]
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ n, FermatPsp n b ∧ m ≤ n
[PROOFSTEP]
rw [h₁]
[GOAL]
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ n, FermatPsp n 1 ∧ m ≤ n
[PROOFSTEP]
use 2 * (m + 2)
[GOAL]
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ FermatPsp (2 * (m + 2)) 1 ∧ m ≤ 2 * (m + 2)
[PROOFSTEP]
have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by norm_num) (by norm_num)
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ 1 < m + 2
[PROOFSTEP]
norm_num
[GOAL]
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ FermatPsp (2 * (m + 2)) 1 ∧ m ≤ 2 * (m + 2)
[PROOFSTEP]
exact ⟨fermatPsp_base_one (by linarith) this, by linarith⟩
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ 1 < 2 * (m + 2)
[PROOFSTEP]
linarith
[GOAL]
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ m ≤ 2 * (m + 2)
[PROOFSTEP]
linarith
[GOAL]
b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, FermatPsp n b
[PROOFSTEP]
refine' Filter.frequently_atTop.2 fun n => _
[GOAL]
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
[PROOFSTEP]
obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n
[GOAL]
case intro
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : FermatPsp p b ∧ n ≤ p
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
[PROOFSTEP]
exact ⟨p, hp.2, hp.1⟩