Metamath Proof Explorer

Theorem sq11

Description: The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001) (Proof shortened by Mario Carneiro, 28-May-2016)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ
2 1 recnd ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℂ
3 sqval ⊢ A ∈ ℂ → A 2 = A ⁢ A
4 2 3 syl ⊢ A ∈ ℝ ∧ 0 ≤ A → A 2 = A ⁢ A
5 simpl ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
6 5 recnd ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℂ
7 sqval ⊢ B ∈ ℂ → B 2 = B ⁢ B
8 6 7 syl ⊢ B ∈ ℝ ∧ 0 ≤ B → B 2 = B ⁢ B
9 4 8 eqeqan12d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A ⁢ A = B ⁢ B
10 msq11 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A = B ⁢ B ↔ A = B
11 9 10 bitrd ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B