Description: The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resqrcld.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
resqrcld.2 | ⊢ ( 𝜑 → 0 ≤ 𝐴 ) | ||
sqr11d.3 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | ||
sqr11d.4 | ⊢ ( 𝜑 → 0 ≤ 𝐵 ) | ||
sqrt11d.5 | ⊢ ( 𝜑 → ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ) | ||
Assertion | sqr11d | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resqrcld.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
2 | resqrcld.2 | ⊢ ( 𝜑 → 0 ≤ 𝐴 ) | |
3 | sqr11d.3 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | |
4 | sqr11d.4 | ⊢ ( 𝜑 → 0 ≤ 𝐵 ) | |
5 | sqrt11d.5 | ⊢ ( 𝜑 → ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ) | |
6 | sqrt11 | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) ) | |
7 | 1 2 3 4 6 | syl22anc | ⊢ ( 𝜑 → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |
8 | 5 7 | mpbid | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |