Metamath Proof Explorer

Theorem cxpmul2d

Description: Product of exponents law for complex exponentiation. Variation on cxpmul with more general conditions on A and B when C is an integer. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses cxp0d.1 φ A
cxpcld.2 φ B
cxpmul2d.4 φ C 0
Assertion cxpmul2d φ A B C = A B C


Step Hyp Ref Expression
1 cxp0d.1 φ A
2 cxpcld.2 φ B
3 cxpmul2d.4 φ C 0
4 cxpmul2 A B C 0 A B C = A B C
5 1 2 3 4 syl3anc φ A B C = A B C