This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem le2sqi

Description: The square function on nonnegative reals is nondecreasing. (Contributed by NM, 12-Sep-1999)

	Ref	Expression
Hypotheses	resqcl.1	$⊢ A \in ℝ$
	lt2sq.2	$⊢ B \in ℝ$
Assertion	le2sqi	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$

Step	Hyp	Ref	Expression
1		resqcl.1	$⊢ A \in ℝ$
2		lt2sq.2	$⊢ B \in ℝ$
3	1 2	le2msqi	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A A \leq B B)$
4	1	recni	$⊢ A \in ℂ$
5	4	sqvali	$⊢ A^{2} = A A$
6	2	recni	$⊢ B \in ℂ$
7	6	sqvali	$⊢ B^{2} = B B$
8	5 7	breq12i	$⊢ A^{2} \leq B^{2} \leftrightarrow A A \leq B B$
9	3 8	bitr4di	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A^{2} \leq B^{2})$