nn0le2msqi

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

	Ref	Expression
Hypotheses	nn0le2msqi.1	$⊢ A \in ℕ_{0}$
	nn0le2msqi.2	$⊢ B \in ℕ_{0}$
Assertion	nn0le2msqi	$⊢ A \leq B \leftrightarrow A A \leq B B$

Step	Hyp	Ref	Expression
1		nn0le2msqi.1	$⊢ A \in ℕ_{0}$
2		nn0le2msqi.2	$⊢ B \in ℕ_{0}$
3	1	nn0ge0i	$⊢ 0 \leq A$
4	2	nn0ge0i	$⊢ 0 \leq B$
5	1	nn0rei	$⊢ A \in ℝ$
6	2	nn0rei	$⊢ B \in ℝ$
7	5 6	le2sqi	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$
8	3 4 7	mp2an	$⊢ A \leq B \leftrightarrow A^{2} \leq B^{2}$
9	1	nn0cni	$⊢ A \in ℂ$
10	9	sqvali	$⊢ A^{2} = A A$
11	2	nn0cni	$⊢ B \in ℂ$
12	11	sqvali	$⊢ B^{2} = B B$
13	10 12	breq12i	$⊢ A^{2} \leq B^{2} \leftrightarrow A A \leq B B$
14	8 13	bitri	$⊢ A \leq B \leftrightarrow A A \leq B B$

Metamath Proof Explorer