Metamath Proof Explorer


Theorem cxpmul2zd

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

Ref Expression
Hypotheses cxp0d.1 ( 𝜑𝐴 ∈ ℂ )
cxpefd.2 ( 𝜑𝐴 ≠ 0 )
cxpefd.3 ( 𝜑𝐵 ∈ ℂ )
cxpmul2zd.4 ( 𝜑𝐶 ∈ ℤ )
Assertion cxpmul2zd ( 𝜑 → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cxp0d.1 ( 𝜑𝐴 ∈ ℂ )
2 cxpefd.2 ( 𝜑𝐴 ≠ 0 )
3 cxpefd.3 ( 𝜑𝐵 ∈ ℂ )
4 cxpmul2zd.4 ( 𝜑𝐶 ∈ ℤ )
5 cxpmul2z ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑ 𝐶 ) )
6 1 2 3 4 5 syl22anc ( 𝜑 → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑ 𝐶 ) )