Theorem expcld 14296

Description: Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
expcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
expcld.2	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
expcld	⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)

Proof of Theorem expcld

Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		expcld.2	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
3		expcl 14229	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7424  ℂcc 11205  ℕ₀cn0 12613  ↑cexp 14211

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-n0 12614  df-z 12701  df-uz 12973  df-seq 14152  df-exp 14212

This theorem is used by:  absexpz  15481  binomlem  16007  incexclem  16014  incexc  16015  incexc2  16016  geoserg  16044  pwdif  16046  pwm1geoser  16047  geolim  16048  geolim2  16049  geo2sum2  16052  geomulcvg  16054  bpolycl  16227  bpolydiflem  16229  efaddlem  16268  oexpneg  16524  pwp1fsum  16570  oddpwp1fsum  16571  cphipval  25573  dvexp3  26307  itgpowd  26379  ply1termlem  26530  dgrcolem2  26602  dvply1  26614  aareccl  26662  aalioulem1  26668  taylfvallem1  26693  tayl0  26698  dvtaylp  26706  taylthlem2  26710  radcnvlem1  26749  pserulm  26758  logtayl  26997  cxpeq  27094  atantayl2  27275  atantayl3  27276  dfef2  27307  ftalem1  27409  ftalem2  27410  ftalem5  27413  basellem4  27420  logexprlim  27561  fltdiv  27977  fltaccoprm  27981  flt4lem6  27997  nrt2irr  31083  psgnfzto1st  33716  fldext2rspun  34364  fldext2chn  34410  2sqr3minply  34462  cos9thpiminplylem2  34465  madjusmdetlem4  34512  oddpwdc  35036  eulerpartlemgs2  35062  signsplypnf  35229  signsply0  35230  breprexplemc  35311  breprexpnat  35313  bcprod  36627  knoppcnlem4  37486  knoppcnlem10  37492  knoppndvlem2  37503  knoppndvlem6  37507  knoppndvlem7  37508  knoppndvlem8  37509  knoppndvlem9  37510  knoppndvlem10  37511  knoppndvlem14  37515  knoppndvlem17  37518  lcmineqlem8  43223  lcmineqlem10  43225  lcmineqlem12  43227  dvrelogpow2b  43255  aks4d1p1p6  43260  aks4d1p1p7  43261  aks4d1p1  43263  2ap1caineq  43332  nicomachus  43506  exp11d  43520  dffltz  43807  fltmul  43808  fltltc  43809  fltnltalem  43810  3cubeslem3l  43833  3cubeslem3r  43834  3cubeslem4  43836  jm2.18  44132  jm2.22  44139  jm2.23  44140  radcnvrat  45435  binomcxplemnn0  45470  binomcxplemnotnn0  45477  expcnfg  46739  fprodexp  46742  climexp  46753  dvsinexp  47057  dvxpaek  47086  dvnxpaek  47088  ibliccsinexp  47097  iblioosinexp  47099  itgsinexplem1  47100  itgsinexp  47101  iblsplit  47112  stoweidlem1  47147  stoweidlem7  47153  wallispi2lem2  47218  wallispi2  47219  stirlinglem3  47222  stirlinglem4  47223  stirlinglem5  47224  stirlinglem7  47226  stirlinglem8  47227  stirlinglem10  47229  stirlinglem11  47230  stirlinglem13  47232  stirlinglem14  47233  stirlinglem15  47234  elaa2lem  47379  etransclem1  47381  etransclem4  47384  etransclem8  47388  etransclem18  47398  etransclem20  47400  etransclem21  47401  etransclem23  47403  etransclem35  47415  etransclem41  47421  etransclem46  47426  etransclem48  47428  sin3t  48053  cos3t  48054  sin5tlem1  48055  sin5tlem2  48056  sin5tlem3  48057  sin5tlem4  48058  sin5tlem5  48059  2pwp1prm  48810  lighneallem4  48831  oexpnegALTV  48911  fppr2odd  48965  altgsumbcALT  49601  dignn0flhalflem1  49863  nn0sumshdiglemA  49867  nn0sumshdiglemB  49868