Metamath Proof Explorer


Theorem cxprec

Description: Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxprec A+B1AB=1AB

Proof

Step Hyp Ref Expression
1 rpcn A+A
2 cxpcl ABAB
3 1 2 sylan A+BAB
4 rpreccl A+1A+
5 4 rpcnd A+1A
6 cxpcl 1AB1AB
7 5 6 sylan A+B1AB
8 1 adantr A+BA
9 rpne0 A+A0
10 9 adantr A+BA0
11 simpr A+BB
12 cxpne0 AA0BAB0
13 8 10 11 12 syl3anc A+BAB0
14 8 10 recidd A+BA1A=1
15 14 oveq1d A+BA1AB=1B
16 rprege0 A+A0A
17 16 adantr A+BA0A
18 4 rprege0d A+1A01A
19 18 adantr A+B1A01A
20 mulcxp A0A1A01ABA1AB=AB1AB
21 17 19 11 20 syl3anc A+BA1AB=AB1AB
22 1cxp B1B=1
23 11 22 syl A+B1B=1
24 15 21 23 3eqtr3d A+BAB1AB=1
25 3 7 13 24 mvllmuld A+B1AB=1AB