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

Metamath Proof Explorer

Theorem sqrtsq2

Description: Relationship between square root and squares. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 29-May-2016)

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

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 sq11 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
5 3 4 sylan ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
6 resqrtth ⊢ A ∈ ℝ ∧ 0 ≤ A → A 2 = A
7 6 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = A
8 7 eqeq1d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B 2
9 5 8 bitr3d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A = B ↔ A = B 2