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

Metamath Proof Explorer

Theorem le2msqi

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

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
Assertion	le2msqi	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A A \leq B B)$

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		le2msq	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow A A \leq B B)$
4	2 3	mpanr1	$⊢ ((A \in ℝ \land 0 \leq A) \land 0 \leq B) \to (A \leq B \leftrightarrow A A \leq B B)$
5	1 4	mpanl1	$⊢ (0 \leq A \land 0 \leq B) \to (A \leq B \leftrightarrow A A \leq B B)$