Theorem expcl 14249

Description: Closure law for nonnegative integer exponentiation. For integer exponents, see expclz 14254. (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 3935	. 2 ⊢ ℂ ⊆ ℂ
2		mulcl 11311	. 2 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
3		ax-1cn 11285	. 2 ⊢ 1 ∈ ℂ
4	1, 2, 3	expcllem 14242	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  ℕ₀cn0 12633  ↑cexp 14231

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-nn 12363  df-n0 12634  df-z 12721  df-uz 12993  df-seq 14172  df-exp 14232

This theorem is used by:  expeq0  14262  expnegz  14266  mulexp  14271  mulexpz  14272  expadd  14274  expaddzlem  14275  expaddz  14276  expmul  14277  expmulz  14278  expdiv  14283  expcld  14316  binom3  14395  digit2  14407  digit1  14408  faclbnd2  14462  faclbnd4lem4  14467  faclbnd6  14470  cjexp  15346  absexp  15500  ackbijnn  16026  binomlem  16027  binom1p  16029  binom1dif  16031  expcnv  16062  geolim  16068  geolim2  16069  geo2sum  16071  geomulcvg  16074  geoisum  16075  geoisumr  16076  geoisum1  16077  geoisum1c  16078  0.999...  16079  fallrisefac  16221  0risefac  16233  binomrisefac  16237  bpolysum  16248  bpolydiflem  16249  fsumkthpow  16251  bpoly3  16253  bpoly4  16254  fsumcube  16255  eftcl  16268  eftabs  16270  efcllem  16272  efcj  16287  efaddlem  16288  eflegeo  16318  efi4p  16334  prmreclem6  17128  karatsuba  17290  expmhm  21772  expcn  25223  mbfi1fseqlem6  26071  itg0  26130  itgz  26131  itgcl  26134  itgcnlem  26140  itgsplit  26186  dvexp  26303  dvexp3  26328  plyf  26546  ply1termlem  26551  plypow  26553  plyeq0lem  26559  plypf1  26561  plyaddlem1  26562  plymullem1  26563  coeeulem  26573  coeidlem  26586  coeid3  26589  plyco  26590  dgrcolem2  26623  plycjlem  26625  plyrecj  26628  vieta1  26665  elqaalem3  26674  aareccl  26683  aalioulem1  26689  geolim3  26696  psergf  26769  dvradcnv  26778  psercn2  26780  pserdvlem2  26785  pserdv2  26787  abelthlem4  26791  abelthlem5  26792  abelthlem6  26793  abelthlem7  26795  abelthlem9  26797  advlogexp  27013  logtayllem  27017  logtayl  27018  logtaylsum  27019  logtayl2  27020  cxpeq  27115  dcubic1lem  27201  dcubic2  27202  dcubic1  27203  dcubic  27204  mcubic  27205  cubic2  27206  cubic  27207  binom4  27208  dquartlem2  27210  dquart  27211  quart1cl  27212  quart1lem  27213  quart1  27214  quartlem1  27215  quartlem2  27216  quart  27219  atantayl  27295  atantayl2  27296  atantayl3  27297  leibpi  27300  log2cnv  27302  log2tlbnd  27303  log2ublem3  27306  ftalem1  27430  ftalem4  27433  ftalem5  27434  basellem3  27440  musum  27548  1sgmprm  27556  perfect  27588  lgsquadlem1  27737  rplogsumlem2  27842  ostth2lem2  27991  numclwwlk3lem1  31013  ipval2  31339  dipcl  31344  dipcn  31352  cos9thpiminplylem5  34488  subfacval2  36119  lcmineqlem1  43271  lcmineqlem2  43272  lcmineqlem8  43278  lcmineqlem10  43280  jm2.23  44196  lhe4.4ex1a  45505  goldpolyfactor  48132  goldratmolem2  48138  goldratmolem3  48139  perfectALTV  49026  altgsumbc  49669  altgsumbcALT  49670  nn0digval  49917  ackval42  50013