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

Metamath Proof Explorer

Theorem sq11i

Description: The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999)

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

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