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	|- ( ph -> A e. CC )
	absimlere.2	|- ( ph -> B e. RR )
Assertion	absimlere	|- ( ph -> ( abs ` ( Im ` A ) ) <_ ( abs ` ( B - A ) ) )

Proof

Step	Hyp	Ref	Expression
1		absimlere.1	|- ( ph -> A e. CC )
2		absimlere.2	|- ( ph -> B e. RR )
3	2	recnd	|- ( ph -> B e. CC )
4	1 3	subcld	|- ( ph -> ( A - B ) e. CC )
5		absimle	|- ( ( A - B ) e. CC -> ( abs ` ( Im ` ( A - B ) ) ) <_ ( abs ` ( A - B ) ) )
6	4 5	syl	|- ( ph -> ( abs ` ( Im ` ( A - B ) ) ) <_ ( abs ` ( A - B ) ) )
7	1 3	imsubd	|- ( ph -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
8	2	reim0d	|- ( ph -> ( Im ` B ) = 0 )
9	8	oveq2d	|- ( ph -> ( ( Im ` A ) - ( Im ` B ) ) = ( ( Im ` A ) - 0 ) )
10	1	imcld	|- ( ph -> ( Im ` A ) e. RR )
11	10	recnd	|- ( ph -> ( Im ` A ) e. CC )
12	11	subid1d	|- ( ph -> ( ( Im ` A ) - 0 ) = ( Im ` A ) )
13	7 9 12	3eqtrrd	|- ( ph -> ( Im ` A ) = ( Im ` ( A - B ) ) )
14	13	fveq2d	|- ( ph -> ( abs ` ( Im ` A ) ) = ( abs ` ( Im ` ( A - B ) ) ) )
15	3 1	abssubd	|- ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( A - B ) ) )
16	6 14 15	3brtr4d	|- ( ph -> ( abs ` ( Im ` A ) ) <_ ( abs ` ( B - A ) ) )