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	eqtrdi	$$⊢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\leftrightarrow 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	eqtr2di	$$⊢\phi \to 1=A^0\cdot 1$$
24	10 18 23	pm2.61ne	$$⊢\phi \to 0^C=A^C{0}^C$$