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)
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)
have q₁ : b - 1 ∣ b ^ p - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p
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)
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)
have q₂ : b + 1 ∣ b ^ p + 1 := by simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
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

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
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)
convert Nat.div_mul_div_comm q₁ q₂ using 2 <;> rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
no goals
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
⊢ b - 1 ∣ b ^ p - 1
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p
no goals
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ b + 1 ∣ b ^ p + 1
simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
no goals
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
ring_nf
no goals
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
simp