le2sq

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999)

		Ref	Expression
	Assertion	le2sq	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$

Step	Hyp	Ref	Expression
1		le2msq	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow A A \leq B B)$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4		sqval	$⊢ A \in ℂ \to A^{2} = A A$
5		sqval	$⊢ B \in ℂ \to B^{2} = B B$
6	4 5	breqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} \leq B^{2} \leftrightarrow A A \leq B B)$
7	2 3 6	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (A^{2} \leq B^{2} \leftrightarrow A A \leq B B)$
8	7	ad2ant2r	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A^{2} \leq B^{2} \leftrightarrow A A \leq B B)$
9	1 8	bitr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$

Metamath Proof Explorer