This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0le2msqi

Description: The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Hypotheses nn0le2msqi.1 
|- A e. NN0
nn0le2msqi.2 
|- B e. NN0
Assertion nn0le2msqi 
|- ( A <_ B <-> ( A x. A ) <_ ( B x. B ) )

Proof

Step Hyp Ref Expression
1 nn0le2msqi.1 
 |-  A e. NN0
2 nn0le2msqi.2 
 |-  B e. NN0
3 1 nn0ge0i 
 |-  0 <_ A
4 2 nn0ge0i 
 |-  0 <_ B
5 1 nn0rei 
 |-  A e. RR
6 2 nn0rei 
 |-  B e. RR
7 5 6 le2sqi 
 |-  ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
8 3 4 7 mp2an 
 |-  ( A <_ B <-> ( A ^ 2 ) <_ ( B ^ 2 ) )
9 1 nn0cni 
 |-  A e. CC
10 9 sqvali 
 |-  ( A ^ 2 ) = ( A x. A )
11 2 nn0cni 
 |-  B e. CC
12 11 sqvali 
 |-  ( B ^ 2 ) = ( B x. B )
13 10 12 breq12i 
 |-  ( ( A ^ 2 ) <_ ( B ^ 2 ) <-> ( A x. A ) <_ ( B x. B ) )
14 8 13 bitri 
 |-  ( A <_ B <-> ( A x. A ) <_ ( B x. B ) )