Metamath Proof Explorer

Theorem le2msq

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 lt2msq 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ ( A e. RR /\ 0 <_ A ) ) -> ( B < A <-> ( B x. B ) < ( A x. A ) ) )
2 1 ancoms 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B < A <-> ( B x. B ) < ( A x. A ) ) )
3 2 notbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( -. B < A <-> -. ( B x. B ) < ( A x. A ) ) )
4 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
5 simprl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
6 4 5 lenltd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> -. B < A ) )
7 4 4 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A x. A ) e. RR )
8 5 5 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B x. B ) e. RR )
9 7 8 lenltd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) <_ ( B x. B ) <-> -. ( B x. B ) < ( A x. A ) ) )
10 3 6 9 3bitr4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )