Theorem mulcxplem

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

	Ref	Expression
Hypotheses	mulcxp.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	mulcxp.2	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	mulcxplem	⊢ ( 𝜑 → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulcxp.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		mulcxp.2	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3		oveq2	⊢ ( 𝐶 = 0 → ( 0 ↑𝑐 𝐶 ) = ( 0 ↑𝑐 0 ) )
4		0cn	⊢ 0 ∈ ℂ
5		cxp0	⊢ ( 0 ∈ ℂ → ( 0 ↑𝑐 0 ) = 1 )
6	4 5	ax-mp	⊢ ( 0 ↑𝑐 0 ) = 1
7	3 6	eqtrdi	⊢ ( 𝐶 = 0 → ( 0 ↑𝑐 𝐶 ) = 1 )
8		oveq2	⊢ ( 𝐶 = 0 → ( 𝐴 ↑𝑐 𝐶 ) = ( 𝐴 ↑𝑐 0 ) )
9	8 7	oveq12d	⊢ ( 𝐶 = 0 → ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 0 ) · 1 ) )
10	7 9	eqeq12d	⊢ ( 𝐶 = 0 → ( ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) ↔ 1 = ( ( 𝐴 ↑𝑐 0 ) · 1 ) ) )
11		cxpcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
12	1 2 11	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
14	13	mul01d	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 ↑𝑐 𝐶 ) · 0 ) = 0 )
15		0cxp	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 0 ↑𝑐 𝐶 ) = 0 )
16	2 15	sylan	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → ( 0 ↑𝑐 𝐶 ) = 0 )
17	16	oveq2d	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐶 ) · 0 ) )
18	14 17 16	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )
19		cxp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 0 ) = 1 )
20	1 19	syl	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 0 ) = 1 )
21	20	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 0 ) · 1 ) = ( 1 · 1 ) )
22		1t1e1	⊢ ( 1 · 1 ) = 1
23	21 22	eqtr2di	⊢ ( 𝜑 → 1 = ( ( 𝐴 ↑𝑐 0 ) · 1 ) )
24	10 18 23	pm2.61ne	⊢ ( 𝜑 → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )