# Metamath Proof Explorer

## Theorem mulcxplem

Description: Lemma for mulcxp . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Hypotheses mulcxp.1 ${⊢}{\phi }\to {A}\in ℂ$
mulcxp.2 ${⊢}{\phi }\to {C}\in ℂ$
Assertion mulcxplem ${⊢}{\phi }\to {0}^{{C}}={{A}}^{{C}}{0}^{{C}}$

### Proof

Step Hyp Ref Expression
1 mulcxp.1 ${⊢}{\phi }\to {A}\in ℂ$
2 mulcxp.2 ${⊢}{\phi }\to {C}\in ℂ$
3 oveq2 ${⊢}{C}=0\to {0}^{{C}}={0}^{0}$
4 0cn ${⊢}0\in ℂ$
5 cxp0 ${⊢}0\in ℂ\to {0}^{0}=1$
6 4 5 ax-mp ${⊢}{0}^{0}=1$
7 3 6 syl6eq ${⊢}{C}=0\to {0}^{{C}}=1$
8 oveq2 ${⊢}{C}=0\to {{A}}^{{C}}={{A}}^{0}$
9 8 7 oveq12d ${⊢}{C}=0\to {{A}}^{{C}}{0}^{{C}}={{A}}^{0}\cdot 1$
10 7 9 eqeq12d ${⊢}{C}=0\to \left({0}^{{C}}={{A}}^{{C}}{0}^{{C}}↔1={{A}}^{0}\cdot 1\right)$
11 cxpcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {{A}}^{{C}}\in ℂ$
12 1 2 11 syl2anc ${⊢}{\phi }\to {{A}}^{{C}}\in ℂ$
13 12 adantr ${⊢}\left({\phi }\wedge {C}\ne 0\right)\to {{A}}^{{C}}\in ℂ$
14 13 mul01d ${⊢}\left({\phi }\wedge {C}\ne 0\right)\to {{A}}^{{C}}\cdot 0=0$
15 0cxp ${⊢}\left({C}\in ℂ\wedge {C}\ne 0\right)\to {0}^{{C}}=0$
16 2 15 sylan ${⊢}\left({\phi }\wedge {C}\ne 0\right)\to {0}^{{C}}=0$
17 16 oveq2d ${⊢}\left({\phi }\wedge {C}\ne 0\right)\to {{A}}^{{C}}{0}^{{C}}={{A}}^{{C}}\cdot 0$
18 14 17 16 3eqtr4rd ${⊢}\left({\phi }\wedge {C}\ne 0\right)\to {0}^{{C}}={{A}}^{{C}}{0}^{{C}}$
19 cxp0 ${⊢}{A}\in ℂ\to {{A}}^{0}=1$
20 1 19 syl ${⊢}{\phi }\to {{A}}^{0}=1$
21 20 oveq1d ${⊢}{\phi }\to {{A}}^{0}\cdot 1=1\cdot 1$
22 1t1e1 ${⊢}1\cdot 1=1$
23 21 22 syl6req ${⊢}{\phi }\to 1={{A}}^{0}\cdot 1$
24 10 18 23 pm2.61ne ${⊢}{\phi }\to {0}^{{C}}={{A}}^{{C}}{0}^{{C}}$