sqrt11

Description: The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013)

		Ref	Expression
	Assertion	sqrt11	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (\sqrt{A} = \sqrt{B} \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
2		sqrtge0	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$
3	1 2	jca	$⊢ (A \in ℝ \land 0 \leq A) \to (\sqrt{A} \in ℝ \land 0 \leq \sqrt{A})$
4		resqrtcl	$⊢ (B \in ℝ \land 0 \leq B) \to \sqrt{B} \in ℝ$
5		sqrtge0	$⊢ (B \in ℝ \land 0 \leq B) \to 0 \leq \sqrt{B}$
6	4 5	jca	$⊢ (B \in ℝ \land 0 \leq B) \to (\sqrt{B} \in ℝ \land 0 \leq \sqrt{B})$
7		sq11	$⊢ ((\sqrt{A} \in ℝ \land 0 \leq \sqrt{A}) \land (\sqrt{B} \in ℝ \land 0 \leq \sqrt{B})) \to ({\sqrt{A}}^{2} = {\sqrt{B}}^{2} \leftrightarrow \sqrt{A} = \sqrt{B})$
8	3 6 7	syl2an	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to ({\sqrt{A}}^{2} = {\sqrt{B}}^{2} \leftrightarrow \sqrt{A} = \sqrt{B})$
9		resqrtth	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$
10		resqrtth	$⊢ (B \in ℝ \land 0 \leq B) \to {\sqrt{B}}^{2} = B$
11	9 10	eqeqan12d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to ({\sqrt{A}}^{2} = {\sqrt{B}}^{2} \leftrightarrow A = B)$
12	8 11	bitr3d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (\sqrt{A} = \sqrt{B} \leftrightarrow A = B)$

Metamath Proof Explorer