b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
⊢ p < (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
⊢ p < FermatPsp.psp_from_prime b p
unfold psp_from_prime
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
⊢ p < A * ((b ^ p + 1) / (b + 1))
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
⊢ p < (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))
set A := (b ^ p - 1) / (b - 1)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A * B
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
⊢ p < A * ((b ^ p + 1) / (b + 1))
set B := (b ^ p + 1) / (b + 1)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A * B
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)]
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
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
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)

case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
suffices h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
rw [Nat.mul_sub_left_distrib, mul_one, pow_mul]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
conv_rhs => rw [← Nat.sub_add_cancel (show 1 ≤ p by linarith)]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1) - 1
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
rw [pow_succ (b ^ 2)]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ p * b ^ 2 - p < b ^ 2 * (b ^ 2) ^ (p - 1) - 1

case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1) - 1
suffices h : p * b ^ 2 < b ^ 2 * (b ^ 2) ^ (p - 1)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)

case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
suffices h : p < (b ^ 2) ^ (p - 1)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
rw [← pow_mul, Nat.mul_sub_left_distrib, mul_one]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
have : 2 ≤ 2 * p - 2 := le_tsub_of_add_le_left (show 4 ≤ 2 * p by linarith)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
have : 2 + p ≤ 2 * p := by linarith
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
have : p ≤ 2 * p - 2 := le_tsub_of_add_le_left this
no goals
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
exact Nat.lt_of_le_of_lt this (pow_gt_exponent _ b_ge_two)
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
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
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
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)]
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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)
rwa [Nat.mul_div_cancel _ h₂] at h₁
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
linarith [show 3 ≤ b ^ 2 - 1 from le_tsub_of_add_le_left (show 4 ≤ b ^ 2 by nlinarith)]
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
nlinarith
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
linarith
case h.h₁
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ b ^ 2 * (b ^ 2) ^ (p - 1) - 1 ≥ ?h.b

case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ ?h.b > p * b ^ 2 - p

case h.b
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ ℕ
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ p * b ^ 2 - p < b ^ 2 * (b ^ 2) ^ (p - 1) - 1
apply gt_of_ge_of_gt
no goals
case h.h₁
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ b ^ 2 * (b ^ 2) ^ (p - 1) - 1 ≥ ?h.b
exact tsub_le_tsub_left (show 1 ≤ p by linarith) (b ^ 2 * (b ^ 2) ^ (p - 1))
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ 1 ≤ p
linarith
case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
this : p ≤ p * b ^ 2
⊢ b ^ 2 * (b ^ 2) ^ (p - 1) - p > p * b ^ 2 - p
case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ b ^ 2 * (b ^ 2) ^ (p - 1) - p > p * b ^ 2 - p
have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right (show 0 < b ^ 2 by nlinarith)
no goals
case h.h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
this : p ≤ p * b ^ 2
⊢ b ^ 2 * (b ^ 2) ^ (p - 1) - p > p * b ^ 2 - p
exact tsub_lt_tsub_right_of_le this h
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
⊢ 0 < b ^ 2
nlinarith
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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 * (b ^ 2) ^ (p - 1)
rw [mul_comm (b ^ 2)]
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
have : 4 ≤ b ^ 2 := by nlinarith
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
have : 0 < b ^ 2 := by linarith
no goals
case h
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
exact mul_lt_mul_of_pos_right h this
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
nlinarith
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
linarith
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
linarith
no goals
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Nat.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
linarith