Theorem lenegsq

Description: Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	lenegsq	|- ( ( A e. RR /\ B e. RR /\ 0 <_ B ) -> ( ( A <_ B /\ -u A <_ B ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2		abscl	|- ( A e. CC -> ( abs ` A ) e. RR )
3		absge0	|- ( A e. CC -> 0 <_ ( abs ` A ) )
4	2 3	jca	|- ( A e. CC -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
5	1 4	syl	|- ( A e. RR -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
6		le2sq	|- ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( abs ` A ) <_ B <-> ( ( abs ` A ) ^ 2 ) <_ ( B ^ 2 ) ) )
7	5 6	sylan	|- ( ( A e. RR /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( abs ` A ) <_ B <-> ( ( abs ` A ) ^ 2 ) <_ ( B ^ 2 ) ) )
8		absle	|- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
9		lenegcon1	|- ( ( A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ A ) )
10	9	anbi1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( -u A <_ B /\ A <_ B ) <-> ( -u B <_ A /\ A <_ B ) ) )
11		ancom	|- ( ( -u A <_ B /\ A <_ B ) <-> ( A <_ B /\ -u A <_ B ) )
12	10 11	bitr3di	|- ( ( A e. RR /\ B e. RR ) -> ( ( -u B <_ A /\ A <_ B ) <-> ( A <_ B /\ -u A <_ B ) ) )
13	8 12	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) <_ B <-> ( A <_ B /\ -u A <_ B ) ) )
14	13	adantrr	|- ( ( A e. RR /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( abs ` A ) <_ B <-> ( A <_ B /\ -u A <_ B ) ) )
15		absresq	|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
16	15	breq1d	|- ( A e. RR -> ( ( ( abs ` A ) ^ 2 ) <_ ( B ^ 2 ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
17	16	adantr	|- ( ( A e. RR /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( abs ` A ) ^ 2 ) <_ ( B ^ 2 ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
18	7 14 17	3bitr3d	|- ( ( A e. RR /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A <_ B /\ -u A <_ B ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
19	18	3impb	|- ( ( A e. RR /\ B e. RR /\ 0 <_ B ) -> ( ( A <_ B /\ -u A <_ B ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )