Source indexedlemma · leanprover/lean4:v4.32.0

Complex.norm_le_abs_im_add_one

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3147 to 3158

Mathematical statement

Exact Lean statement

lemma _root_.Complex.norm_le_abs_im_add_one {z : ℂ} (hz_re : z.re ∈ Set.Icc (-1 : ℝ) 1) :
    ‖z‖ ≤ |z.im| + 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma _root_.Complex.norm_le_abs_im_add_one {z : ℂ} (hz_re : z.re ∈ Set.Icc (-1 : ℝ) 1) :    ‖z‖ ≤ |z.im| + 1 := by  calc ‖z‖    _ = ‖(z.re : ℂ) + (z.im : ℂ) * I‖ := by rw [Complex.re_add_im]    _ ≤ ‖(z.re : ℂ)‖ + ‖(z.im : ℂ) * I‖ := norm_add_le _ _    _ = |z.re| + |z.im| := by        rw [Complex.norm_real, norm_mul, Complex.norm_I, Complex.norm_real]        simp only [norm_eq_abs, mul_one]    _ ≤ 1 + |z.im|     := by        have : |z.re| ≤ 1 := abs_le.mpr hz_re        linarith    _ = |z.im| + 1     := add_comm 1 _