Metamath Proof Explorer


Theorem cxpmul2zd

Description: Generalize cxpmul2 to negative integers. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses cxp0d.1 φ A
cxpefd.2 φ A 0
cxpefd.3 φ B
cxpmul2zd.4 φ C
Assertion cxpmul2zd φ A B C = A B C

Proof

Step Hyp Ref Expression
1 cxp0d.1 φ A
2 cxpefd.2 φ A 0
3 cxpefd.3 φ B
4 cxpmul2zd.4 φ C
5 cxpmul2z A A 0 B C A B C = A B C
6 1 2 3 4 5 syl22anc φ A B C = A B C