English
If h is a LiouvilleWith-predicated function at x, then subtracting any rational r keeps the LiouvilleWith-predicate, i.e., LiouvilleWith p (x − r).
Русский
Если функция является предикатом LiouvilleWith в точке x, то вычитание любого рационального числа r сохраняет это свойство: LiouvilleWith p (x − r).
LaTeX
$$$\\forall x:\\ LiouvilleWith\\ p\\ x\\to\\forall r:\\mathbb Q,\\ LiouvilleWith\\ p\\ (x-r)$$$
Lean4
protected theorem irrational {x : ℝ} (h : Liouville x) : Irrational x := by
-- By contradiction, `x = a / b`, with `a ∈ ℤ`, `0 < b ∈ ℕ` is a Liouville number,
rintro
⟨⟨a, b, bN0, cop⟩, rfl⟩
-- clear up the mess of constructions of rationals
rw [Rat.cast_mk'] at h
rcases h (b + 1) with
⟨p, q, q1, a0, a1⟩
-- A few useful inequalities
have qR0 : (0 : ℝ) < q := Int.cast_pos.mpr (zero_lt_one.trans q1)
have b0 : (b : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr bN0
have bq0 : (0 : ℝ) < b * q := mul_pos (Nat.cast_pos.mpr bN0.bot_lt) qR0
replace a1 : |a * q - b * p| * q ^ (b + 1) < b * q :=
by
rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _), abs_of_pos bq0,
one_mul] at a1
exact mod_cast a1
replace a0 : a * q - ↑b * p ≠ 0 :=
by
rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0
exact mod_cast a0
lift q to ℕ using (zero_lt_one.trans q1).le
have ap : 0 < |a * ↑q - ↑b * p| := abs_pos.mpr a0
lift |a * ↑q - ↑b * p| to ℕ using abs_nonneg (a * ↑q - ↑b * p) with e he
norm_cast at a1 ap q1
exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ ap q1).le
