Theorem nn0le2msqi

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

	Ref	Expression
Hypotheses	nn0le2msqi.1	$$⊢A\in {\mathbb{N}}_0$$
	nn0le2msqi.2	$$⊢B\in {\mathbb{N}}_0$$
Assertion	nn0le2msqi	$$⊢A\le B\leftrightarrow AA\le BB$$

Proof

Step	Hyp	Ref	Expression
1		nn0le2msqi.1	$$⊢A\in {\mathbb{N}}_0$$
2		nn0le2msqi.2	$$⊢B\in {\mathbb{N}}_0$$
3	1	nn0ge0i	$$⊢0\le A$$
4	2	nn0ge0i	$$⊢0\le B$$
5	1	nn0rei	$$⊢A\in ℝ$$
6	2	nn0rei	$$⊢B\in ℝ$$
7	5 6	le2sqi	$$⊢\left(0\le A\wedge 0\le B\right)\to \left(A\le B\leftrightarrow A^2\le B^2\right)$$
8	3 4 7	mp2an	$$⊢A\le B\leftrightarrow A^2\le B^2$$
9	1	nn0cni	$$⊢A\in ℂ$$
10	9	sqvali	$$⊢A^2=AA$$
11	2	nn0cni	$$⊢B\in ℂ$$
12	11	sqvali	$$⊢B^2=BB$$
13	10 12	breq12i	$$⊢A^2\le B^2\leftrightarrow AA\le BB$$
14	8 13	bitri	$$⊢A\le B\leftrightarrow AA\le BB$$