Theorem expcld 14053

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 13986	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  ℕ₀cn0 12384  ↑cexp 13968

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472  df-uz 12736  df-seq 13909  df-exp 13969

This theorem is referenced by:  absexpz  15212  binomlem  15736  incexclem  15743  incexc  15744  incexc2  15745  geoserg  15773  pwdif  15775  pwm1geoser  15776  geolim  15777  geolim2  15778  geo2sum2  15781  geomulcvg  15783  bpolycl  15959  bpolydiflem  15961  efaddlem  16000  oexpneg  16256  pwp1fsum  16302  oddpwp1fsum  16303  cphipval  25141  dvexp3  25880  itgpowd  25955  ply1termlem  26106  dgrcolem2  26178  dvply1  26189  aareccl  26232  aalioulem1  26238  taylfvallem1  26262  tayl0  26267  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  radcnvlem1  26320  pserulm  26329  logtayl  26567  cxpeq  26665  atantayl2  26846  atantayl3  26847  dfef2  26879  ftalem1  26981  ftalem2  26982  ftalem5  26985  basellem4  26992  logexprlim  27134  nrt2irr  30417  psgnfzto1st  33047  fldext2rspun  33649  fldext2chn  33695  2sqr3minply  33747  cos9thpiminplylem2  33750  madjusmdetlem4  33797  oddpwdc  34322  eulerpartlemgs2  34348  signsplypnf  34518  signsply0  34519  breprexplemc  34600  breprexpnat  34602  bcprod  35715  knoppcnlem4  36474  knoppcnlem10  36480  knoppndvlem2  36491  knoppndvlem6  36495  knoppndvlem7  36496  knoppndvlem8  36497  knoppndvlem9  36498  knoppndvlem10  36499  knoppndvlem14  36503  knoppndvlem17  36506  lcmineqlem8  42013  lcmineqlem10  42015  lcmineqlem12  42017  dvrelogpow2b  42045  aks4d1p1p6  42050  aks4d1p1p7  42051  aks4d1p1  42053  2ap1caineq  42122  nicomachus  42289  exp11d  42303  dffltz  42611  fltmul  42612  fltdiv  42613  fltaccoprm  42617  flt4lem6  42635  fltltc  42638  fltnltalem  42639  3cubeslem3l  42663  3cubeslem3r  42664  3cubeslem4  42666  jm2.18  42965  jm2.22  42972  jm2.23  42973  radcnvrat  44291  binomcxplemnn0  44326  binomcxplemnotnn0  44333  expcnfg  45576  fprodexp  45579  climexp  45590  dvsinexp  45896  dvxpaek  45925  dvnxpaek  45927  ibliccsinexp  45936  iblioosinexp  45938  itgsinexplem1  45939  itgsinexp  45940  iblsplit  45951  stoweidlem1  45986  stoweidlem7  45992  wallispi2lem2  46057  wallispi2  46058  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  stirlinglem13  46071  stirlinglem14  46072  stirlinglem15  46073  elaa2lem  46218  etransclem1  46220  etransclem4  46223  etransclem8  46227  etransclem18  46237  etransclem20  46239  etransclem21  46240  etransclem23  46242  etransclem35  46254  etransclem41  46260  etransclem46  46265  etransclem48  46267  2pwp1prm  47577  lighneallem4  47598  oexpnegALTV  47665  fppr2odd  47719  altgsumbcALT  48341  dignn0flhalflem1  48604  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609