# Metamath Proof Explorer

## 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 ↑𝑐 𝐶 ) ) )