Theorem expcld 14178

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  ℕ₀cn0 12499  ↑cexp 14093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-seq 14034  df-exp 14094

This theorem is referenced by:  absexpz  15352  binomlem  15879  incexclem  15886  incexc  15887  incexc2  15888  geoserg  15916  pwdif  15918  pwm1geoser  15919  geolim  15920  geolim2  15921  geo2sum2  15924  geomulcvg  15926  bpolycl  16101  bpolydiflem  16103  efaddlem  16142  oexpneg  16398  pwp1fsum  16444  oddpwp1fsum  16445  cphipval  25402  dvexp3  26137  itgpowd  26209  ply1termlem  26360  dgrcolem2  26431  dvply1  26445  aareccl  26489  aalioulem1  26495  taylfvallem1  26520  tayl0  26525  dvtaylp  26533  taylthlem2  26537  radcnvlem1  26576  pserulm  26585  logtayl  26825  cxpeq  26922  atantayl2  27103  atantayl3  27104  dfef2  27135  ftalem1  27237  ftalem2  27238  ftalem5  27241  basellem4  27248  logexprlim  27389  nrt2irr  30824  psgnfzto1st  33425  fldext2rspun  34072  fldext2chn  34118  2sqr3minply  34170  cos9thpiminplylem2  34173  madjusmdetlem4  34220  oddpwdc  34744  eulerpartlemgs2  34770  signsplypnf  34937  signsply0  34938  breprexplemc  35019  breprexpnat  35021  bcprod  36230  knoppcnlem4  37085  knoppcnlem10  37091  knoppndvlem2  37102  knoppndvlem6  37106  knoppndvlem7  37107  knoppndvlem8  37108  knoppndvlem9  37109  knoppndvlem10  37110  knoppndvlem14  37114  knoppndvlem17  37117  lcmineqlem8  42803  lcmineqlem10  42805  lcmineqlem12  42807  dvrelogpow2b  42835  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1  42843  2ap1caineq  42912  nicomachus  43073  exp11d  43087  dffltz  43366  fltmul  43367  fltdiv  43368  fltaccoprm  43372  flt4lem6  43390  fltltc  43393  fltnltalem  43394  3cubeslem3l  43417  3cubeslem3r  43418  3cubeslem4  43420  jm2.18  43715  jm2.22  43722  jm2.23  43723  radcnvrat  45024  binomcxplemnn0  45059  binomcxplemnotnn0  45066  expcnfg  46307  fprodexp  46310  climexp  46321  dvsinexp  46625  dvxpaek  46654  dvnxpaek  46656  ibliccsinexp  46665  iblioosinexp  46667  itgsinexplem1  46668  itgsinexp  46669  iblsplit  46680  stoweidlem1  46715  stoweidlem7  46721  wallispi2lem2  46786  wallispi2  46787  stirlinglem3  46790  stirlinglem4  46791  stirlinglem5  46792  stirlinglem7  46794  stirlinglem8  46795  stirlinglem10  46797  stirlinglem11  46798  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  elaa2lem  46947  etransclem1  46949  etransclem4  46952  etransclem8  46956  etransclem18  46966  etransclem20  46968  etransclem21  46969  etransclem23  46971  etransclem35  46983  etransclem41  46989  etransclem46  46994  etransclem48  46996  sin3t  47608  cos3t  47609  sin5tlem1  47610  sin5tlem2  47611  sin5tlem3  47612  sin5tlem4  47613  sin5tlem5  47614  2pwp1prm  48341  lighneallem4  48362  oexpnegALTV  48442  fppr2odd  48496  altgsumbcALT  49133  dignn0flhalflem1  49395  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400