This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absimlere

Description: The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses absimlere.1 ⊢ φ → A ∈ ℂ
absimlere.2 ⊢ φ → B ∈ ℝ
Assertion absimlere ⊢ φ → ℑ ⁡ A ≤ B − A

Proof

Step Hyp Ref Expression
1 absimlere.1 ⊢ φ → A ∈ ℂ
2 absimlere.2 ⊢ φ → B ∈ ℝ
3 2 recnd ⊢ φ → B ∈ ℂ
4 1 3 subcld ⊢ φ → A − B ∈ ℂ
5 absimle ⊢ A − B ∈ ℂ → ℑ ⁡ A − B ≤ A − B
6 4 5 syl ⊢ φ → ℑ ⁡ A − B ≤ A − B
7 1 3 imsubd ⊢ φ → ℑ ⁡ A − B = ℑ ⁡ A − ℑ ⁡ B
8 2 reim0d ⊢ φ → ℑ ⁡ B = 0
9 8 oveq2d ⊢ φ → ℑ ⁡ A − ℑ ⁡ B = ℑ ⁡ A − 0
10 1 imcld ⊢ φ → ℑ ⁡ A ∈ ℝ
11 10 recnd ⊢ φ → ℑ ⁡ A ∈ ℂ
12 11 subid1d ⊢ φ → ℑ ⁡ A − 0 = ℑ ⁡ A
13 7 9 12 3eqtrrd ⊢ φ → ℑ ⁡ A = ℑ ⁡ A − B
14 13 fveq2d ⊢ φ → ℑ ⁡ A = ℑ ⁡ A − B
15 3 1 abssubd ⊢ φ → B − A = A − B
16 6 14 15 3brtr4d ⊢ φ → ℑ ⁡ A ≤ B − A