Theorem abslt2sqd

Description: Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	abslt2sqd.a	|- ( ph -> A e. RR )
	abslt2sqd.b	|- ( ph -> B e. RR )
	abslt2sqd.l	|- ( ph -> ( abs ` A ) < ( abs ` B ) )
Assertion	abslt2sqd	|- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		abslt2sqd.a	|- ( ph -> A e. RR )
2		abslt2sqd.b	|- ( ph -> B e. RR )
3		abslt2sqd.l	|- ( ph -> ( abs ` A ) < ( abs ` B ) )
4	1	recnd	|- ( ph -> A e. CC )
5	4	abscld	|- ( ph -> ( abs ` A ) e. RR )
6	4	absge0d	|- ( ph -> 0 <_ ( abs ` A ) )
7	2	recnd	|- ( ph -> B e. CC )
8	7	abscld	|- ( ph -> ( abs ` B ) e. RR )
9	7	absge0d	|- ( ph -> 0 <_ ( abs ` B ) )
10		lt2sq	|- ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
11	5 6 8 9 10	syl22anc	|- ( ph -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
12	3 11	mpbid	|- ( ph -> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) )
13		absresq	|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
14	1 13	syl	|- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
15		absresq	|- ( B e. RR -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
16	2 15	syl	|- ( ph -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
17	14 16	breq12d	|- ( ph -> ( ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( A ^ 2 ) < ( B ^ 2 ) ) )
18	12 17	mpbid	|- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )