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 )