Description: Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | cxprec | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpcn | |
|
2 | cxpcl | |
|
3 | 1 2 | sylan | |
4 | rpreccl | |
|
5 | 4 | rpcnd | |
6 | cxpcl | |
|
7 | 5 6 | sylan | |
8 | 1 | adantr | |
9 | rpne0 | |
|
10 | 9 | adantr | |
11 | simpr | |
|
12 | cxpne0 | |
|
13 | 8 10 11 12 | syl3anc | |
14 | 8 10 | recidd | |
15 | 14 | oveq1d | |
16 | rprege0 | |
|
17 | 16 | adantr | |
18 | 4 | rprege0d | |
19 | 18 | adantr | |
20 | mulcxp | |
|
21 | 17 19 11 20 | syl3anc | |
22 | 1cxp | |
|
23 | 11 22 | syl | |
24 | 15 21 23 | 3eqtr3d | |
25 | 3 7 13 24 | mvllmuld | |