mulcxplem

Step	Hyp	Ref	Expression
1		mulcxp.1	$⊢ φ \to A \in ℂ$
2		mulcxp.2	$⊢ φ \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 (0^{C} = A^{C} 0^{C} \leftrightarrow 1 = A^{0} \cdot 1)$
11		cxpcl	$⊢ (A \in ℂ \land C \in ℂ) \to A^{C} \in ℂ$
12	1 2 11	syl2anc	$⊢ φ \to A^{C} \in ℂ$
13	12	adantr	$⊢ (φ \land C \neq 0) \to A^{C} \in ℂ$
14	13	mul01d	$⊢ (φ \land C \neq 0) \to A^{C} \cdot 0 = 0$
15		0cxp	$⊢ (C \in ℂ \land C \neq 0) \to 0^{C} = 0$
16	2 15	sylan	$⊢ (φ \land C \neq 0) \to 0^{C} = 0$
17	16	oveq2d	$⊢ (φ \land C \neq 0) \to A^{C} 0^{C} = A^{C} \cdot 0$
18	14 17 16	3eqtr4rd	$⊢ (φ \land C \neq 0) \to 0^{C} = A^{C} 0^{C}$
19		cxp0	$⊢ A \in ℂ \to A^{0} = 1$
20	1 19	syl	$⊢ φ \to A^{0} = 1$
21	20	oveq1d	$⊢ φ \to A^{0} \cdot 1 = 1 \cdot 1$
22		1t1e1	$⊢ 1 \cdot 1 = 1$
23	21 22	eqtr2di	$⊢ φ \to 1 = A^{0} \cdot 1$
24	10 18 23	pm2.61ne	$⊢ φ \to 0^{C} = A^{C} 0^{C}$

Metamath Proof Explorer