Metamath Proof Explorer

Theorem msq11i

Description: The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999)

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

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