Metamath Proof Explorer


Theorem lt2sqi

Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999)

Ref Expression
Hypotheses resqcl.1
|- A e. RR
lt2sq.2
|- B e. RR
Assertion lt2sqi
|- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A ^ 2 ) < ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 resqcl.1
 |-  A e. RR
2 lt2sq.2
 |-  B e. RR
3 1 2 lt2msqi
 |-  ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
4 1 recni
 |-  A e. CC
5 4 sqvali
 |-  ( A ^ 2 ) = ( A x. A )
6 2 recni
 |-  B e. CC
7 6 sqvali
 |-  ( B ^ 2 ) = ( B x. B )
8 5 7 breq12i
 |-  ( ( A ^ 2 ) < ( B ^ 2 ) <-> ( A x. A ) < ( B x. B ) )
9 3 8 bitr4di
 |-  ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A ^ 2 ) < ( B ^ 2 ) ) )