Step |
Hyp |
Ref |
Expression |
1 |
|
cjcl |
|- ( A e. CC -> ( * ` A ) e. CC ) |
2 |
1
|
adantr |
|- ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) e. CC ) |
3 |
|
simpl |
|- ( ( A e. CC /\ A =/= 0 ) -> A e. CC ) |
4 |
2 3
|
mulcomd |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` A ) x. A ) = ( A x. ( * ` A ) ) ) |
5 |
|
absvalsq |
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) ) |
6 |
5
|
adantr |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) ) |
7 |
4 6
|
eqtr4d |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` A ) x. A ) = ( ( abs ` A ) ^ 2 ) ) |
8 |
|
abscl |
|- ( A e. CC -> ( abs ` A ) e. RR ) |
9 |
8
|
adantr |
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR ) |
10 |
9
|
recnd |
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC ) |
11 |
10
|
sqcld |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) e. CC ) |
12 |
|
cjne0 |
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) ) |
13 |
12
|
biimpa |
|- ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) =/= 0 ) |
14 |
11 2 3 13
|
divmuld |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) = A <-> ( ( * ` A ) x. A ) = ( ( abs ` A ) ^ 2 ) ) ) |
15 |
7 14
|
mpbird |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) = A ) |
16 |
15
|
oveq2d |
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) ) = ( 1 / A ) ) |
17 |
|
abs00 |
|- ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) ) |
18 |
17
|
necon3bid |
|- ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) ) |
19 |
18
|
biimpar |
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 ) |
20 |
|
sqne0 |
|- ( ( abs ` A ) e. CC -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) ) |
21 |
10 20
|
syl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) ) |
22 |
19 21
|
mpbird |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) =/= 0 ) |
23 |
11 2 22 13
|
recdivd |
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) ) |
24 |
16 23
|
eqtr3d |
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) ) |