Metamath Proof Explorer

Theorem sqr0lem

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

Ref Expression
Assertion sqr0lem 
|- ( ( A e. CC /\ ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) <-> A = 0 )

Proof

Step Hyp Ref Expression
1 sqeq0 
 |-  ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
2 1 biimpa 
 |-  ( ( A e. CC /\ ( A ^ 2 ) = 0 ) -> A = 0 )
3 2 3ad2antr1 
 |-  ( ( A e. CC /\ ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) -> A = 0 )
4 0re 
 |-  0 e. RR
5 eleq1 
 |-  ( A = 0 -> ( A e. RR <-> 0 e. RR ) )
6 4 5 mpbiri 
 |-  ( A = 0 -> A e. RR )
7 6 recnd 
 |-  ( A = 0 -> A e. CC )
8 sq0i 
 |-  ( A = 0 -> ( A ^ 2 ) = 0 )
9 0le0 
 |-  0 <_ 0
10 fveq2 
 |-  ( A = 0 -> ( Re ` A ) = ( Re ` 0 ) )
11 re0 
 |-  ( Re ` 0 ) = 0
12 10 11 eqtrdi 
 |-  ( A = 0 -> ( Re ` A ) = 0 )
13 9 12 breqtrrid 
 |-  ( A = 0 -> 0 <_ ( Re ` A ) )
14 rennim 
 |-  ( A e. RR -> ( _i x. A ) e/ RR+ )
15 6 14 syl 
 |-  ( A = 0 -> ( _i x. A ) e/ RR+ )
16 8 13 15 3jca 
 |-  ( A = 0 -> ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) )
17 7 16 jca 
 |-  ( A = 0 -> ( A e. CC /\ ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) )
18 3 17 impbii 
 |-  ( ( A e. CC /\ ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) <-> A = 0 )