le2sq2

Description: The square function is nondecreasing on the nonnegative reals. (Contributed by NM, 21-Mar-2008)

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

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to A \leq B$
2		simprl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to B \in ℝ$
3		0re	$⊢ 0 \in ℝ$
4		letr	$⊢ (0 \in ℝ \land A \in ℝ \land B \in ℝ) \to ((0 \leq A \land A \leq B) \to 0 \leq B)$
5	3 4	mp3an1	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 \leq A \land A \leq B) \to 0 \leq B)$
6	5	exp4b	$⊢ A \in ℝ \to (B \in ℝ \to (0 \leq A \to (A \leq B \to 0 \leq B)))$
7	6	com23	$⊢ A \in ℝ \to (0 \leq A \to (B \in ℝ \to (A \leq B \to 0 \leq B)))$
8	7	imp43	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to 0 \leq B$
9	2 8	jca	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to (B \in ℝ \land 0 \leq B)$
10		le2sq	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$
11	9 10	syldan	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$
12	1 11	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land A \leq B)) \to A^{2} \leq B^{2}$

Metamath Proof Explorer