Theorem expcld 14168

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135  ℕ₀cn0 12509  ↑cexp 14084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-n0 12510  df-z 12597  df-uz 12861  df-seq 14025  df-exp 14085

This theorem is referenced by:  absexpz  15326  binomlem  15847  incexclem  15854  incexc  15855  incexc2  15856  geoserg  15884  pwdif  15886  pwm1geoser  15887  geolim  15888  geolim2  15889  geo2sum2  15892  geomulcvg  15894  bpolycl  16070  bpolydiflem  16072  efaddlem  16111  oexpneg  16364  pwp1fsum  16410  oddpwp1fsum  16411  cphipval  25213  dvexp3  25952  itgpowd  26027  ply1termlem  26178  dgrcolem2  26250  dvply1  26261  aareccl  26304  aalioulem1  26310  taylfvallem1  26334  tayl0  26339  dvtaylp  26348  taylthlem2  26352  taylthlem2OLD  26353  radcnvlem1  26392  pserulm  26401  logtayl  26638  cxpeq  26736  atantayl2  26917  atantayl3  26918  dfef2  26950  ftalem1  27052  ftalem2  27053  ftalem5  27056  basellem4  27063  logexprlim  27205  nrt2irr  30420  psgnfzto1st  33064  fldext2rspun  33669  fldext2chn  33708  2sqr3minply  33749  madjusmdetlem4  33788  oddpwdc  34315  eulerpartlemgs2  34341  signsplypnf  34524  signsply0  34525  breprexplemc  34606  breprexpnat  34608  bcprod  35697  knoppcnlem4  36456  knoppcnlem10  36462  knoppndvlem2  36473  knoppndvlem6  36477  knoppndvlem7  36478  knoppndvlem8  36479  knoppndvlem9  36480  knoppndvlem10  36481  knoppndvlem14  36485  knoppndvlem17  36488  lcmineqlem8  41996  lcmineqlem10  41998  lcmineqlem12  42000  dvrelogpow2b  42028  aks4d1p1p6  42033  aks4d1p1p7  42034  aks4d1p1  42036  2ap1caineq  42105  nicomachus  42309  exp11d  42324  dffltz  42607  fltmul  42608  fltdiv  42609  fltaccoprm  42613  flt4lem6  42631  fltltc  42634  fltnltalem  42635  3cubeslem3l  42660  3cubeslem3r  42661  3cubeslem4  42663  jm2.18  42963  jm2.22  42970  jm2.23  42971  radcnvrat  44290  binomcxplemnn0  44325  binomcxplemnotnn0  44332  expcnfg  45563  fprodexp  45566  climexp  45577  dvsinexp  45883  dvxpaek  45912  dvnxpaek  45914  ibliccsinexp  45923  iblioosinexp  45925  itgsinexplem1  45926  itgsinexp  45927  iblsplit  45938  stoweidlem1  45973  stoweidlem7  45979  wallispi2lem2  46044  wallispi2  46045  stirlinglem3  46048  stirlinglem4  46049  stirlinglem5  46050  stirlinglem7  46052  stirlinglem8  46053  stirlinglem10  46055  stirlinglem11  46056  stirlinglem13  46058  stirlinglem14  46059  stirlinglem15  46060  elaa2lem  46205  etransclem1  46207  etransclem4  46210  etransclem8  46214  etransclem18  46224  etransclem20  46226  etransclem21  46227  etransclem23  46229  etransclem35  46241  etransclem41  46247  etransclem46  46252  etransclem48  46254  2pwp1prm  47534  lighneallem4  47555  oexpnegALTV  47622  fppr2odd  47676  altgsumbcALT  48227  dignn0flhalflem1  48494  nn0sumshdiglemA  48498  nn0sumshdiglemB  48499