Theorem expcl 14095

Description: Closure law for nonnegative integer exponentiation. For integer exponents, see expclz 14100. (Contributed by NM, 26-May-2005.)

Assertion

Ref	Expression
expcl	⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)

Proof of Theorem expcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3981	. 2 ⊢ ℂ ⊆ ℂ
2		mulcl 11211	. 2 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
3		ax-1cn 11185	. 2 ⊢ 1 ∈ ℂ
4	1, 2, 3	expcllem 14088	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  ℕ₀cn0 12499  ↑cexp 14077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587  df-uz 12851  df-seq 14018  df-exp 14078

This theorem is referenced by:  expeq0  14108  expnegz  14112  mulexp  14117  mulexpz  14118  expadd  14120  expaddzlem  14121  expaddz  14122  expmul  14123  expmulz  14124  expdiv  14129  expcld  14162  binom3  14240  digit2  14252  digit1  14253  faclbnd2  14307  faclbnd4lem4  14312  faclbnd6  14315  cjexp  15167  absexp  15321  ackbijnn  15842  binomlem  15843  binom1p  15845  binom1dif  15847  expcnv  15878  geolim  15884  geolim2  15885  geo2sum  15887  geomulcvg  15890  geoisum  15891  geoisumr  15892  geoisum1  15893  geoisum1c  15894  0.999...  15895  fallrisefac  16039  0risefac  16052  binomrisefac  16056  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  bpoly3  16072  bpoly4  16073  fsumcube  16074  eftcl  16087  eftabs  16089  efcllem  16091  efcj  16106  efaddlem  16107  eflegeo  16137  efi4p  16153  prmreclem6  16939  karatsuba  17101  expmhm  21402  expcn  24812  mbfi1fseqlem6  25671  itg0  25731  itgz  25732  itgcl  25735  itgcnlem  25741  itgsplit  25787  dvexp  25907  dvexp3  25932  plyf  26153  ply1termlem  26158  plypow  26160  plyeq0lem  26165  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  coeid3  26195  plyco  26196  dgrcolem2  26230  plycjlem  26232  plyrecj  26237  vieta1  26270  elqaalem3  26279  aareccl  26284  aalioulem1  26290  geolim3  26297  psergf  26371  dvradcnv  26380  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv2  26390  abelthlem4  26394  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem9  26400  advlogexp  26614  logtayllem  26618  logtayl  26619  logtaylsum  26620  logtayl2  26621  cxpeq  26717  dcubic1lem  26803  dcubic2  26804  dcubic1  26805  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  binom4  26810  dquartlem2  26812  dquart  26813  quart1cl  26814  quart1lem  26815  quart1  26816  quartlem1  26817  quartlem2  26818  quart  26821  atantayl  26897  atantayl2  26898  atantayl3  26899  leibpi  26902  log2cnv  26904  log2tlbnd  26905  log2ublem3  26908  ftalem1  27033  ftalem4  27036  ftalem5  27037  basellem3  27043  musum  27151  1sgmprm  27160  perfect  27192  lgsquadlem1  27341  rplogsumlem2  27446  ostth2lem2  27595  numclwwlk3lem1  30309  ipval2  30634  dipcl  30639  dipcn  30647  cos9thpiminplylem5  33766  subfacval2  35155  lcmineqlem1  41988  lcmineqlem2  41989  lcmineqlem8  41995  lcmineqlem10  41997  jm2.23  42967  lhe4.4ex1a  44301  perfectALTV  47685  altgsumbc  48275  altgsumbcALT  48276  nn0digval  48528  ackval42  48624