English
Let q be a positive rational. Then the numerator of fract(q⁻¹) is less than q.num; i.e. (fract q⁻¹).num < q.num.
Русский
Пусть q — положительный рационал. Тогда числитель fract(q⁻¹) меньше q.num.
LaTeX
$$$$ (\\operatorname{fract}(q^{-1})).num < q.num, \\quad q > 0, \\ q \\in \\mathbb{Q}. $$$$
Lean4
theorem fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).num < q.num := by
-- we know that the numerator must be positive
have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos
have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
set q_inv : ℚ := q.den / q.num with q_inv_def
have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num
by
simp only [gt_iff_lt, q_inv]
field_simp
simp [q_inv, this]
suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
-- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ :=
by
suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
mod_cast Rat.num_div_eq_of_coprime q_num_pos this
have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
rwa [this]
-- to show the claim, start with the following inequality
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den :=
by
have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
rwa [← sub_lt_iff_lt_add'] at this
have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs :=
by
have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
have : Int.natAbs q.den = q.den := by simp
rw [← this] at coprime_q_denom_q_num
rw [q_inv_def]
constructor
· exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
· suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
rw [q_num_abs_eq_q_num]
exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
