English
For a > 1 and m, n ∈ ℕ, yn(a,m) ∣ yn(a,n) iff m ∣ n.
Русский
Для a > 1 и натуральных m, n выполняется yn(a,m) ∣ yn(a,n) тогда и только тогда, когда m ∣ n.
LaTeX
$$$y^{(a)}_{m} \\mid y^{(a)}_{n} \\;\\Leftrightarrow\\; m \\mid n$.$$
Lean4
theorem y_dvd_iff (m n) : yn a1 m ∣ yn a1 n ↔ m ∣ n :=
⟨fun h =>
Nat.dvd_of_mod_eq_zero <|
(Nat.eq_zero_or_pos _).resolve_right fun hp =>
by
have co : Nat.Coprime (yn a1 m) (xn a1 (m * (n / m))) :=
Nat.Coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))
have m0 : 0 < m :=
m.eq_zero_or_pos.resolve_left fun e => by
rw [e, Nat.mod_zero] at hp; rw [e] at h
exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm
rw [← Nat.mod_add_div n m, yn_add] at h
exact
not_le_of_gt (strictMono_y _ <| Nat.mod_lt n m0)
(Nat.le_of_dvd (strictMono_y _ hp) <|
co.dvd_of_dvd_mul_right <| (Nat.dvd_add_iff_right <| (y_mul_dvd _ _ _).mul_left _).2 h),
fun ⟨k, e⟩ => by rw [e]; apply y_mul_dvd⟩
