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 ) )