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 ) |