Metamath Proof Explorer


Theorem mulcxp

Description: Complex exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion mulcxp A0AB0BCABC=ACBC

Proof

Step Hyp Ref Expression
1 simp1l A0AB0BCA
2 1 recnd A0AB0BCA
3 2 mul01d A0AB0BCA0=0
4 3 oveq1d A0AB0BCA0C=0C
5 simp3 A0AB0BCC
6 2 5 mulcxplem A0AB0BC0C=AC0C
7 4 6 eqtrd A0AB0BCA0C=AC0C
8 oveq2 B=0AB=A0
9 8 oveq1d B=0ABC=A0C
10 oveq1 B=0BC=0C
11 10 oveq2d B=0ACBC=AC0C
12 9 11 eqeq12d B=0ABC=ACBCA0C=AC0C
13 7 12 syl5ibrcom A0AB0BCB=0ABC=ACBC
14 simp2l A0AB0BCB
15 14 recnd A0AB0BCB
16 15 mul02d A0AB0BC0B=0
17 16 oveq1d A0AB0BC0BC=0C
18 15 5 mulcxplem A0AB0BC0C=BC0C
19 cxpcl BCBC
20 15 5 19 syl2anc A0AB0BCBC
21 0cn 0
22 cxpcl 0C0C
23 21 5 22 sylancr A0AB0BC0C
24 20 23 mulcomd A0AB0BCBC0C=0CBC
25 18 24 eqtrd A0AB0BC0C=0CBC
26 17 25 eqtrd A0AB0BC0BC=0CBC
27 oveq1 A=0AB=0B
28 27 oveq1d A=0ABC=0BC
29 oveq1 A=0AC=0C
30 29 oveq1d A=0ACBC=0CBC
31 28 30 eqeq12d A=0ABC=ACBC0BC=0CBC
32 26 31 syl5ibrcom A0AB0BCA=0ABC=ACBC
33 32 a1dd A0AB0BCA=0B0ABC=ACBC
34 1 adantr A0AB0BCA0B0A
35 simpl1r A0AB0BCA0B00A
36 simprl A0AB0BCA0B0A0
37 34 35 36 ne0gt0d A0AB0BCA0B00<A
38 34 37 elrpd A0AB0BCA0B0A+
39 14 adantr A0AB0BCA0B0B
40 simpl2r A0AB0BCA0B00B
41 simprr A0AB0BCA0B0B0
42 39 40 41 ne0gt0d A0AB0BCA0B00<B
43 39 42 elrpd A0AB0BCA0B0B+
44 38 43 relogmuld A0AB0BCA0B0logAB=logA+logB
45 44 oveq2d A0AB0BCA0B0ClogAB=ClogA+logB
46 5 adantr A0AB0BCA0B0C
47 2 adantr A0AB0BCA0B0A
48 47 36 logcld A0AB0BCA0B0logA
49 15 adantr A0AB0BCA0B0B
50 49 41 logcld A0AB0BCA0B0logB
51 46 48 50 adddid A0AB0BCA0B0ClogA+logB=ClogA+ClogB
52 45 51 eqtrd A0AB0BCA0B0ClogAB=ClogA+ClogB
53 52 fveq2d A0AB0BCA0B0eClogAB=eClogA+ClogB
54 46 48 mulcld A0AB0BCA0B0ClogA
55 46 50 mulcld A0AB0BCA0B0ClogB
56 efadd ClogAClogBeClogA+ClogB=eClogAeClogB
57 54 55 56 syl2anc A0AB0BCA0B0eClogA+ClogB=eClogAeClogB
58 53 57 eqtrd A0AB0BCA0B0eClogAB=eClogAeClogB
59 47 49 mulcld A0AB0BCA0B0AB
60 47 49 36 41 mulne0d A0AB0BCA0B0AB0
61 cxpef ABAB0CABC=eClogAB
62 59 60 46 61 syl3anc A0AB0BCA0B0ABC=eClogAB
63 cxpef AA0CAC=eClogA
64 47 36 46 63 syl3anc A0AB0BCA0B0AC=eClogA
65 cxpef BB0CBC=eClogB
66 49 41 46 65 syl3anc A0AB0BCA0B0BC=eClogB
67 64 66 oveq12d A0AB0BCA0B0ACBC=eClogAeClogB
68 58 62 67 3eqtr4d A0AB0BCA0B0ABC=ACBC
69 68 exp32 A0AB0BCA0B0ABC=ACBC
70 33 69 pm2.61dne A0AB0BCB0ABC=ACBC
71 13 70 pm2.61dne A0AB0BCABC=ACBC