Theorem expcld 14211

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℂcc 11123  ℕ₀cn0 12529  ↑cexp 14126

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

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 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 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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-n0 12530  df-z 12617  df-uz 12889  df-seq 14067  df-exp 14127

This theorem is used by:  absexpz  15393  binomlem  15919  incexclem  15926  incexc  15927  incexc2  15928  geoserg  15956  pwdif  15958  pwm1geoser  15959  geolim  15960  geolim2  15961  geo2sum2  15964  geomulcvg  15966  bpolycl  16139  bpolydiflem  16141  efaddlem  16180  oexpneg  16436  pwp1fsum  16482  oddpwp1fsum  16483  cphipval  25472  dvexp3  26206  itgpowd  26278  ply1termlem  26429  dgrcolem2  26501  dvply1  26515  aareccl  26563  aalioulem1  26569  taylfvallem1  26594  tayl0  26599  dvtaylp  26607  taylthlem2  26611  radcnvlem1  26650  pserulm  26659  logtayl  26898  cxpeq  26995  atantayl2  27176  atantayl3  27177  dfef2  27208  ftalem1  27310  ftalem2  27311  ftalem5  27314  basellem4  27321  logexprlim  27462  nrt2irr  30954  psgnfzto1st  33546  fldext2rspun  34193  fldext2chn  34239  2sqr3minply  34291  cos9thpiminplylem2  34294  madjusmdetlem4  34341  oddpwdc  34866  eulerpartlemgs2  34892  signsplypnf  35059  signsply0  35060  breprexplemc  35141  breprexpnat  35143  bcprod  36318  knoppcnlem4  37194  knoppcnlem10  37200  knoppndvlem2  37211  knoppndvlem6  37215  knoppndvlem7  37216  knoppndvlem8  37217  knoppndvlem9  37218  knoppndvlem10  37219  knoppndvlem14  37223  knoppndvlem17  37226  lcmineqlem8  42903  lcmineqlem10  42905  lcmineqlem12  42907  dvrelogpow2b  42935  aks4d1p1p6  42940  aks4d1p1p7  42941  aks4d1p1  42943  2ap1caineq  43012  nicomachus  43188  exp11d  43202  dffltz  43481  fltmul  43482  fltdiv  43483  fltaccoprm  43487  flt4lem6  43505  fltltc  43508  fltnltalem  43509  3cubeslem3l  43532  3cubeslem3r  43533  3cubeslem4  43535  jm2.18  43830  jm2.22  43837  jm2.23  43838  radcnvrat  45139  binomcxplemnn0  45174  binomcxplemnotnn0  45181  expcnfg  46422  fprodexp  46425  climexp  46436  dvsinexp  46740  dvxpaek  46769  dvnxpaek  46771  ibliccsinexp  46780  iblioosinexp  46782  itgsinexplem1  46783  itgsinexp  46784  iblsplit  46795  stoweidlem1  46830  stoweidlem7  46836  wallispi2lem2  46901  wallispi2  46902  stirlinglem3  46905  stirlinglem4  46906  stirlinglem5  46907  stirlinglem7  46909  stirlinglem8  46910  stirlinglem10  46912  stirlinglem11  46913  stirlinglem13  46915  stirlinglem14  46916  stirlinglem15  46917  elaa2lem  47062  etransclem1  47064  etransclem4  47067  etransclem8  47071  etransclem18  47081  etransclem20  47083  etransclem21  47084  etransclem23  47086  etransclem35  47098  etransclem41  47104  etransclem46  47109  etransclem48  47111  sin3t  47736  cos3t  47737  sin5tlem1  47738  sin5tlem2  47739  sin5tlem3  47740  sin5tlem4  47741  sin5tlem5  47742  2pwp1prm  48493  lighneallem4  48514  oexpnegALTV  48594  fppr2odd  48648  altgsumbcALT  49284  dignn0flhalflem1  49546  nn0sumshdiglemA  49550  nn0sumshdiglemB  49551