English
If m,n are coprime and a,b ≠ 0, then a m + b n ≠ m n.
Русский
Пусть m,n взаимно просты и a,b ≠ 0. Тогда a m + b n ≠ m n.
LaTeX
$$$\forall m,n,a,b \in \mathbb{N}, (\gcd(m,n)=1) \land a \neq 0 \land b \neq 0 \Rightarrow a m + b n \neq m n$$$
Lean4
theorem mul_add_mul_ne_mul {m n a b : ℕ} (cop : Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) : a * m + b * n ≠ m * n :=
by
intro h
obtain ⟨x, rfl⟩ : n ∣ a :=
cop.symm.dvd_of_dvd_mul_right
((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
obtain ⟨y, rfl⟩ : m ∣ b :=
cop.dvd_of_dvd_mul_right
((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)
rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
