Metamath Proof Explorer

Theorem sqrt0

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

Ref Expression
Assertion sqrt0 
|- ( sqrt ` 0 ) = 0

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 sqrtval 
 |-  ( 0 e. CC -> ( sqrt ` 0 ) = ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
3 1 2 ax-mp 
 |-  ( sqrt ` 0 ) = ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
4 id 
 |-  ( 0 e. CC -> 0 e. CC )
5 sqeq0 
 |-  ( x e. CC -> ( ( x ^ 2 ) = 0 <-> x = 0 ) )
6 5 biimpa 
 |-  ( ( x e. CC /\ ( x ^ 2 ) = 0 ) -> x = 0 )
7 6 3ad2antr1 
 |-  ( ( x e. CC /\ ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> x = 0 )
8 7 ex 
 |-  ( x e. CC -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> x = 0 ) )
9 sq0i 
 |-  ( x = 0 -> ( x ^ 2 ) = 0 )
10 0le0 
 |-  0 <_ 0
11 fveq2 
 |-  ( x = 0 -> ( Re ` x ) = ( Re ` 0 ) )
12 re0 
 |-  ( Re ` 0 ) = 0
13 11 12 eqtrdi 
 |-  ( x = 0 -> ( Re ` x ) = 0 )
14 10 13 breqtrrid 
 |-  ( x = 0 -> 0 <_ ( Re ` x ) )
15 0re 
 |-  0 e. RR
16 eleq1 
 |-  ( x = 0 -> ( x e. RR <-> 0 e. RR ) )
17 15 16 mpbiri 
 |-  ( x = 0 -> x e. RR )
18 rennim 
 |-  ( x e. RR -> ( _i x. x ) e/ RR+ )
19 17 18 syl 
 |-  ( x = 0 -> ( _i x. x ) e/ RR+ )
20 9 14 19 3jca 
 |-  ( x = 0 -> ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
21 8 20 impbid1 
 |-  ( x e. CC -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> x = 0 ) )
22 21 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> x = 0 ) )
23 4 22 riota5 
 |-  ( 0 e. CC -> ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = 0 )
24 1 23 ax-mp 
 |-  ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = 0
25 3 24 eqtri 
 |-  ( sqrt ` 0 ) = 0