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	$$⊢\phi \to A\in ℂ$$
	absimlere.2	$$⊢\phi \to B\in ℝ$$
Assertion	absimlere	$$⊢\phi \to \left|\Im \left(A\right)\right|\le \left|B-A\right|$$

Proof

Step	Hyp	Ref	Expression
1		absimlere.1	$$⊢\phi \to A\in ℂ$$
2		absimlere.2	$$⊢\phi \to B\in ℝ$$
3	2	recnd	$$⊢\phi \to B\in ℂ$$
4	1 3	subcld	$$⊢\phi \to A-B\in ℂ$$
5		absimle	$$⊢A-B\in ℂ\to \left|\Im \left(A-B\right)\right|\le \left|A-B\right|$$
6	4 5	syl	$$⊢\phi \to \left|\Im \left(A-B\right)\right|\le \left|A-B\right|$$
7	1 3	imsubd	$$⊢\phi \to \Im \left(A-B\right)=\Im \left(A\right)-\Im \left(B\right)$$
8	2	reim0d	$$⊢\phi \to \Im \left(B\right)=0$$
9	8	oveq2d	$$⊢\phi \to \Im \left(A\right)-\Im \left(B\right)=\Im \left(A\right)-0$$
10	1	imcld	$$⊢\phi \to \Im \left(A\right)\in ℝ$$
11	10	recnd	$$⊢\phi \to \Im \left(A\right)\in ℂ$$
12	11	subid1d	$$⊢\phi \to \Im \left(A\right)-0=\Im \left(A\right)$$
13	7 9 12	3eqtrrd	$$⊢\phi \to \Im \left(A\right)=\Im \left(A-B\right)$$
14	13	fveq2d	$$⊢\phi \to \left|\Im \left(A\right)\right|=\left|\Im \left(A-B\right)\right|$$
15	3 1	abssubd	$$⊢\phi \to \left|B-A\right|=\left|A-B\right|$$
16	6 14 15	3brtr4d	$$⊢\phi \to \left|\Im \left(A\right)\right|\le \left|B-A\right|$$