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 ‘ ( 𝐵 − 𝐴 ) ) )