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