Metamath Proof Explorer

Theorem sqrt11

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

Ref Expression
Assertion sqrt11 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A = B ↔ A = B

Proof

Step Hyp Ref Expression
1 resqrtcl ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ
2 sqrtge0 ⊢ A ∈ ℝ ∧ 0 ≤ A → 0 ≤ A
3 1 2 jca ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ ∧ 0 ≤ A
4 resqrtcl ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
5 sqrtge0 ⊢ B ∈ ℝ ∧ 0 ≤ B → 0 ≤ B
6 4 5 jca ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ ∧ 0 ≤ B
7 sq11 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
8 3 6 7 syl2an ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
9 resqrtth ⊢ A ∈ ℝ ∧ 0 ≤ A → A 2 = A
10 resqrtth ⊢ B ∈ ℝ ∧ 0 ≤ B → B 2 = B
11 9 10 eqeqan12d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
12 8 11 bitr3d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A = B ↔ A = B