Metamath Proof Explorer


Theorem divcxp

Description: Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Assertion divcxp A0AB+CABC=ACBC

Proof

Step Hyp Ref Expression
1 simp1l A0AB+CA
2 simp1r A0AB+C0A
3 simp2 A0AB+CB+
4 3 rpreccld A0AB+C1B+
5 4 rpred A0AB+C1B
6 4 rpge0d A0AB+C01B
7 simp3 A0AB+CC
8 mulcxp A0A1B01BCA1BC=AC1BC
9 1 2 5 6 7 8 syl221anc A0AB+CA1BC=AC1BC
10 cxprec B+C1BC=1BC
11 3 7 10 syl2anc A0AB+C1BC=1BC
12 11 oveq2d A0AB+CAC1BC=AC1BC
13 9 12 eqtrd A0AB+CA1BC=AC1BC
14 1 recnd A0AB+CA
15 3 rpcnd A0AB+CB
16 3 rpne0d A0AB+CB0
17 14 15 16 divrecd A0AB+CAB=A1B
18 17 oveq1d A0AB+CABC=A1BC
19 cxpcl ACAC
20 14 7 19 syl2anc A0AB+CAC
21 cxpcl BCBC
22 15 7 21 syl2anc A0AB+CBC
23 cxpne0 BB0CBC0
24 15 16 7 23 syl3anc A0AB+CBC0
25 20 22 24 divrecd A0AB+CACBC=AC1BC
26 13 18 25 3eqtr4d A0AB+CABC=ACBC