Metamath Proof Explorer

Theorem sqrt0

Description: Square root of 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 sqr0lem 
 |-  ( ( x e. CC /\ ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) <-> x = 0 )
6 5 biimpi 
 |-  ( ( x e. CC /\ ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> x = 0 )
7 6 ex 
 |-  ( x e. CC -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> x = 0 ) )
8 simpr 
 |-  ( ( x e. CC /\ ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
9 5 8 sylbir 
 |-  ( x = 0 -> ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
10 7 9 impbid1 
 |-  ( x e. CC -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> x = 0 ) )
11 10 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> x = 0 ) )
12 4 11 riota5 
 |-  ( 0 e. CC -> ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = 0 )
13 1 12 ax-mp 
 |-  ( iota_ x e. CC ( ( x ^ 2 ) = 0 /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = 0
14 3 13 eqtri 
 |-  ( sqrt ` 0 ) = 0