English
As in item 153793, the squared norm difference between x/y in ℂ and x/y in ℤ[i] is bounded by 1.
Русский
Как в пункте 153793, квадрат нормы разности x/y в ℂ и x/y в ℤ[i] ограничен сверху единицей.
LaTeX
$$$ \operatorname{normSq}\Bigl((x / y : \mathbb{C}) - ((x / y : \mathbb{Z}[i]) : \mathbb{C})\Bigr) < 1 $$$
Lean4
theorem norm_mod_lt (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (x % y).norm < y.norm :=
have : (y : ℂ) ≠ 0 := by rwa [Ne, ← toComplex_zero, toComplex_inj]
(@Int.cast_lt ℝ _ _ _ _).1 <|
calc
↑(Zsqrtd.norm (x % y)) = Complex.normSq (x - y * (x / y : ℤ[i]) : ℂ) := by simp [mod_def]
_ = Complex.normSq (y : ℂ) * Complex.normSq (x / y - (x / y : ℤ[i]) : ℂ) := by
rw [← normSq_mul, mul_sub, mul_div_cancel₀ _ this]
_ < Complex.normSq (y : ℂ) * 1 := (mul_lt_mul_of_pos_left (normSq_div_sub_div_lt_one _ _) (normSq_pos.2 this))
_ = Zsqrtd.norm y := by simp
