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 φA0
cxpefd.3 φB
cxpmul2zd.4 φC
Assertion cxpmul2zd φABC=ABC

Proof

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