Theorem expcld 14289

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  ℕ₀cn0 12606  ↑cexp 14204

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  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 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-uz 12966  df-seq 14145  df-exp 14205

This theorem is used by:  absexpz  15472  binomlem  15998  incexclem  16005  incexc  16006  incexc2  16007  geoserg  16035  pwdif  16037  pwm1geoser  16038  geolim  16039  geolim2  16040  geo2sum2  16043  geomulcvg  16045  bpolycl  16218  bpolydiflem  16220  efaddlem  16259  oexpneg  16515  pwp1fsum  16561  oddpwp1fsum  16562  cphipval  25564  dvexp3  26298  itgpowd  26370  ply1termlem  26521  dgrcolem2  26593  dvply1  26605  aareccl  26653  aalioulem1  26659  taylfvallem1  26684  tayl0  26689  dvtaylp  26697  taylthlem2  26701  radcnvlem1  26740  pserulm  26749  logtayl  26988  cxpeq  27085  atantayl2  27266  atantayl3  27267  dfef2  27298  ftalem1  27400  ftalem2  27401  ftalem5  27404  basellem4  27411  logexprlim  27552  fltdiv  27968  fltaccoprm  27972  flt4lem6  27988  nrt2irr  31074  psgnfzto1st  33666  fldext2rspun  34314  fldext2chn  34360  2sqr3minply  34412  cos9thpiminplylem2  34415  madjusmdetlem4  34462  oddpwdc  34986  eulerpartlemgs2  35012  signsplypnf  35179  signsply0  35180  breprexplemc  35261  breprexpnat  35263  bcprod  36503  knoppcnlem4  37362  knoppcnlem10  37368  knoppndvlem2  37379  knoppndvlem6  37383  knoppndvlem7  37384  knoppndvlem8  37385  knoppndvlem9  37386  knoppndvlem10  37387  knoppndvlem14  37391  knoppndvlem17  37394  lcmineqlem8  43086  lcmineqlem10  43088  lcmineqlem12  43090  dvrelogpow2b  43118  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1  43126  2ap1caineq  43195  nicomachus  43369  exp11d  43383  dffltz  43670  fltmul  43671  fltltc  43672  fltnltalem  43673  3cubeslem3l  43696  3cubeslem3r  43697  3cubeslem4  43699  jm2.18  43994  jm2.22  44001  jm2.23  44002  radcnvrat  45297  binomcxplemnn0  45332  binomcxplemnotnn0  45339  expcnfg  46602  fprodexp  46605  climexp  46616  dvsinexp  46920  dvxpaek  46949  dvnxpaek  46951  ibliccsinexp  46960  iblioosinexp  46962  itgsinexplem1  46963  itgsinexp  46964  iblsplit  46975  stoweidlem1  47010  stoweidlem7  47016  wallispi2lem2  47081  wallispi2  47082  stirlinglem3  47085  stirlinglem4  47086  stirlinglem5  47087  stirlinglem7  47089  stirlinglem8  47090  stirlinglem10  47092  stirlinglem11  47093  stirlinglem13  47095  stirlinglem14  47096  stirlinglem15  47097  elaa2lem  47242  etransclem1  47244  etransclem4  47247  etransclem8  47251  etransclem18  47261  etransclem20  47263  etransclem21  47264  etransclem23  47266  etransclem35  47278  etransclem41  47284  etransclem46  47289  etransclem48  47291  sin3t  47916  cos3t  47917  sin5tlem1  47918  sin5tlem2  47919  sin5tlem3  47920  sin5tlem4  47921  sin5tlem5  47922  2pwp1prm  48673  lighneallem4  48694  oexpnegALTV  48774  fppr2odd  48828  altgsumbcALT  49464  dignn0flhalflem1  49726  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731