English
In the three-gen setting, for every S' the square of λ divides at least one of the sums S'.a + S'.b, S'.a + η S'.b, or S'.a + η^2 S'.b.
Русский
В трехгенном случае квадраты лямбда делят по крайней мере одно из чисел S'.a + S'.b, S'.a + η S'.b, S'.a + η^2 S'.b.
LaTeX
$$$\lambda^2 \mid S'.a + S'.b \;\lor\; \lambda^2 \mid S'.a + \eta S'.b \;\lor\; \lambda^2 \mid S'.a + \eta^2 S'.b$$$
Lean4
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides one amongst `S'.a + S'.b`,
`S'.a + η * S'.b` and `S'.a + η ^ 2 * S'.b`. -/
theorem lambda_sq_dvd_or_dvd_or_dvd : λ ^ 2 ∣ S'.a + S'.b ∨ λ ^ 2 ∣ S'.a + η * S'.b ∨ λ ^ 2 ∣ S'.a + η ^ 2 * S'.b :=
by
by_contra! h
rcases h with ⟨h1, h2, h3⟩
rw [← emultiplicity_lt_iff_not_dvd] at h1 h2 h3
have h1' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + S'.b) :=
finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ by simp [ht] at h1)
have h2' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η * S'.b) :=
by
refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
rw [coe_eta] at ht
simp [ht] at h2
have h3' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η ^ 2 * S'.b) :=
by
refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
rw [coe_eta] at ht
simp [ht] at h3
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3
have := (pow_dvd_pow_of_dvd (lambda_sq_dvd_c S') 3).mul_left S'.u
rw [← pow_mul, ← S'.H, a_cube_add_b_cube_eq_mul, pow_dvd_iff_le_emultiplicity,
emultiplicity_mul hζ.zeta_sub_one_prime', emultiplicity_mul hζ.zeta_sub_one_prime',
h1'.emultiplicity_eq_multiplicity, h2'.emultiplicity_eq_multiplicity, h3'.emultiplicity_eq_multiplicity, ←
Nat.cast_add, ← Nat.cast_add, Nat.cast_le] at this
cutsat
