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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
absimlere.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion absimlere ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )

Proof

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