Theorem sqrt00

Description: A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	sqrt00	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sqrt0	⊢ ( √ ‘ 0 ) = 0
2	1	eqeq2i	⊢ ( ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) ↔ ( √ ‘ 𝐴 ) = 0 )
3		0re	⊢ 0 ∈ ℝ
4		0le0	⊢ 0 ≤ 0
5		sqrt11	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 0 ∈ ℝ ∧ 0 ≤ 0 ) ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) ↔ 𝐴 = 0 ) )
6	3 4 5	mpanr12	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) ↔ 𝐴 = 0 ) )
7	2 6	bitr3id	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )