Theorem nnexpcl 14109

Description: Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)

Assertion

Ref	Expression
nnexpcl	⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)

Proof of Theorem nnexpcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnsscn 12237	. 2 ⊢ ℕ ⊆ ℂ
2		nnmulcl 12256	. 2 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℕ)
3		1nn 12243	. 2 ⊢ 1 ∈ ℕ
4	1, 2, 3	expcllem 14107	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  (class class class)co 7411  ℕcn 12232  ℕ₀cn0 12503  ↑cexp 14096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-n0 12504  df-z 12591  df-uz 12862  df-seq 14037  df-exp 14097

This theorem is referenced by:  digit1  14272  nnexpcld  14280  faclbnd4lem3  14330  faclbnd5  14333  climcndslem1  15902  climcndslem2  15903  climcnds  15904  harmonic  15912  geo2sum  15926  geo2lim  15928  ege2le3  16143  eftlub  16164  ef01bndlem  16239  expgcd  16620  phiprmpw  16834  pcdvdsb  16928  pcmptcl  16950  pcfac  16958  pockthi  16966  prmreclem3  16977  prmreclem5  16979  prmreclem6  16980  modxai  17127  1259lem5  17194  2503lem3  17198  4001lem4  17203  ovollb2lem  25615  ovoliunlem1  25629  ovoliunlem3  25631  dyadf  25718  dyadovol  25720  dyadss  25721  dyaddisjlem  25722  dyadmaxlem  25724  opnmbllem  25728  mbfi1fseqlem1  25842  mbfi1fseqlem3  25844  mbfi1fseqlem4  25845  mbfi1fseqlem5  25846  mbfi1fseqlem6  25847  aalioulem1  26461  aaliou2b  26470  aaliou3lem9  26479  log2cnv  27074  log2tlbnd  27075  log2ublem1  27076  log2ublem2  27077  log2ub  27079  zetacvg  27144  vmappw  27245  sgmnncl  27276  dvdsppwf1o  27315  0sgmppw  27327  1sgm2ppw  27329  vmasum  27345  mersenne  27356  perfect1  27357  perfectlem1  27358  perfectlem2  27359  perfect  27360  pcbcctr  27405  bclbnd  27409  bposlem2  27414  bposlem6  27418  bposlem8  27420  chebbnd1lem1  27598  rplogsumlem2  27614  ostth2lem3  27764  ostth3  27767  oddpwdc  34688  tgoldbachgt  34994  faclim2  36138  opnmbllem0  38194  heiborlem3  38351  heiborlem5  38353  heiborlem6  38354  heiborlem7  38355  heiborlem8  38356  heibor  38359  dvdsexpnn0  42984  hoicvrrex  47161  ovnsubaddlem2  47176  ovolval5lem1  47257  fmtnoprmfac2lem1  48206  fmtno4prm  48215  perfectALTVlem1  48374  perfectALTVlem2  48375  perfectALTV  48376  bgoldbachlt  48466  tgblthelfgott  48468  tgoldbachlt  48469  blenpw2  49242  nnpw2pb  49251  nnolog2flm1  49254