# Metamath Proof Explorer

## Theorem cxpcl

Description: Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {{A}}^{{B}}\in ℂ$

### Proof

Step Hyp Ref Expression
1 cxpval ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {{A}}^{{B}}=if\left({A}=0,if\left({B}=0,1,0\right),{\mathrm{e}}^{{B}\mathrm{log}{A}}\right)$
2 ax-1cn ${⊢}1\in ℂ$
3 0cn ${⊢}0\in ℂ$
4 2 3 ifcli ${⊢}if\left({B}=0,1,0\right)\in ℂ$
5 4 a1i ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {A}=0\right)\to if\left({B}=0,1,0\right)\in ℂ$
6 df-ne ${⊢}{A}\ne 0↔¬{A}=0$
7 id ${⊢}{B}\in ℂ\to {B}\in ℂ$
8 logcl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \mathrm{log}{A}\in ℂ$
9 mulcl ${⊢}\left({B}\in ℂ\wedge \mathrm{log}{A}\in ℂ\right)\to {B}\mathrm{log}{A}\in ℂ$
10 7 8 9 syl2anr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {B}\in ℂ\right)\to {B}\mathrm{log}{A}\in ℂ$
11 10 an32s ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {A}\ne 0\right)\to {B}\mathrm{log}{A}\in ℂ$
12 efcl ${⊢}{B}\mathrm{log}{A}\in ℂ\to {\mathrm{e}}^{{B}\mathrm{log}{A}}\in ℂ$
13 11 12 syl ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {A}\ne 0\right)\to {\mathrm{e}}^{{B}\mathrm{log}{A}}\in ℂ$
14 6 13 sylan2br ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge ¬{A}=0\right)\to {\mathrm{e}}^{{B}\mathrm{log}{A}}\in ℂ$
15 5 14 ifclda ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to if\left({A}=0,if\left({B}=0,1,0\right),{\mathrm{e}}^{{B}\mathrm{log}{A}}\right)\in ℂ$
16 1 15 eqeltrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {{A}}^{{B}}\in ℂ$