Metamath Proof Explorer


Theorem sqrt0

Description: The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrt0 0 = 0

Proof

Step Hyp Ref Expression
1 0cn 0
2 sqrtval 0 0 = ι x | x 2 = 0 0 x i x +
3 1 2 ax-mp 0 = ι x | x 2 = 0 0 x i x +
4 id 0 0
5 sqeq0 x x 2 = 0 x = 0
6 5 biimpa x x 2 = 0 x = 0
7 6 3ad2antr1 x x 2 = 0 0 x i x + x = 0
8 7 ex x x 2 = 0 0 x i x + x = 0
9 sq0i x = 0 x 2 = 0
10 0le0 0 0
11 fveq2 x = 0 x = 0
12 re0 0 = 0
13 11 12 eqtrdi x = 0 x = 0
14 10 13 breqtrrid x = 0 0 x
15 0re 0
16 eleq1 x = 0 x 0
17 15 16 mpbiri x = 0 x
18 rennim x i x +
19 17 18 syl x = 0 i x +
20 9 14 19 3jca x = 0 x 2 = 0 0 x i x +
21 8 20 impbid1 x x 2 = 0 0 x i x + x = 0
22 21 adantl 0 x x 2 = 0 0 x i x + x = 0
23 4 22 riota5 0 ι x | x 2 = 0 0 x i x + = 0
24 1 23 ax-mp ι x | x 2 = 0 0 x i x + = 0
25 3 24 eqtri 0 = 0