Metamath Proof Explorer

Theorem lt2msq

Description: Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lt2msq 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )

Proof

Step Hyp Ref Expression
1 lt2msq1 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )
2 1 3expia 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) -> ( A < B -> ( A x. A ) < ( B x. B ) ) )
3 2 adantrr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B -> ( A x. A ) < ( B x. B ) ) )
4 id 
 |-  ( A = B -> A = B )
5 4 4 oveq12d 
 |-  ( A = B -> ( A x. A ) = ( B x. B ) )
6 5 a1i 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A = B -> ( A x. A ) = ( B x. B ) ) )
7 lt2msq1 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ A e. RR /\ B < A ) -> ( B x. B ) < ( A x. A ) )
8 7 3expia 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ A e. RR ) -> ( B < A -> ( B x. B ) < ( A x. A ) ) )
9 8 adantrr 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ ( A e. RR /\ 0 <_ A ) ) -> ( B < A -> ( B x. B ) < ( A x. A ) ) )
10 9 ancoms 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B < A -> ( B x. B ) < ( A x. A ) ) )
11 6 10 orim12d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A = B \/ B < A ) -> ( ( A x. A ) = ( B x. B ) \/ ( B x. B ) < ( A x. A ) ) ) )
12 11 con3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( -. ( ( A x. A ) = ( B x. B ) \/ ( B x. B ) < ( A x. A ) ) -> -. ( A = B \/ B < A ) ) )
13 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
14 13 13 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A x. A ) e. RR )
15 simprl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
16 15 15 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B x. B ) e. RR )
17 14 16 lttrid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) < ( B x. B ) <-> -. ( ( A x. A ) = ( B x. B ) \/ ( B x. B ) < ( A x. A ) ) ) )
18 13 15 lttrid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
19 12 17 18 3imtr4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) < ( B x. B ) -> A < B ) )
20 3 19 impbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )