Theorem nnexpcl 13254

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 11440	. 2 ⊢ ℕ ⊆ ℂ
2		nnmulcl 11460	. 2 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℕ)
3		1nn 11448	. 2 ⊢ 1 ∈ ℕ
4	1, 2, 3	expcllem 13252	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  (class class class)co 6974  ℕcn 11435  ℕ₀cn0 11704  ↑cexp 13241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-2nd 7499  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-er 8085  df-en 8303  df-dom 8304  df-sdom 8305  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-nn 11436  df-n0 11705  df-z 11791  df-uz 12056  df-seq 13182  df-exp 13242

This theorem is referenced by:  digit1  13410  nnexpcld  13418  faclbnd4lem3  13467  faclbnd5  13470  climcndslem1  15058  climcndslem2  15059  climcnds  15060  harmonic  15068  geo2sum  15083  geo2lim  15085  ege2le3  15297  eftlub  15316  ef01bndlem  15391  phiprmpw  15963  pcdvdsb  16055  pcmptcl  16077  pcfac  16085  pockthi  16093  prmreclem3  16104  prmreclem5  16106  prmreclem6  16107  modxai  16254  1259lem5  16318  2503lem3  16322  4001lem4  16327  ovollb2lem  23786  ovoliunlem1  23800  ovoliunlem3  23802  dyadf  23889  dyadovol  23891  dyadss  23892  dyaddisjlem  23893  dyadmaxlem  23895  opnmbllem  23899  mbfi1fseqlem1  24013  mbfi1fseqlem3  24015  mbfi1fseqlem4  24016  mbfi1fseqlem5  24017  mbfi1fseqlem6  24018  aalioulem1  24618  aaliou2b  24627  aaliou3lem9  24636  log2cnv  25218  log2tlbnd  25219  log2ublem1  25220  log2ublem2  25221  log2ub  25223  zetacvg  25288  vmappw  25389  sgmnncl  25420  dvdsppwf1o  25459  0sgmppw  25470  1sgm2ppw  25472  vmasum  25488  mersenne  25499  perfect1  25500  perfectlem1  25501  perfectlem2  25502  perfect  25503  pcbcctr  25548  bclbnd  25552  bposlem2  25557  bposlem6  25561  bposlem8  25563  chebbnd1lem1  25741  rplogsumlem2  25757  ostth2lem3  25907  ostth3  25910  oddpwdc  31248  tgoldbachgt  31573  faclim2  32470  opnmbllem0  34347  heiborlem3  34511  heiborlem5  34513  heiborlem6  34514  heiborlem7  34515  heiborlem8  34516  heibor  34519  expgcd  38593  hoicvrrex  42248  ovnsubaddlem2  42263  ovolval5lem1  42344  fmtnoprmfac2lem1  43070  fmtno4prm  43079  perfectALTVlem1  43228  perfectALTVlem2  43229  perfectALTV  43230  bgoldbachlt  43320  tgblthelfgott  43322  tgoldbachlt  43323  blenpw2  43980  nnpw2pb  43989  nnolog2flm1  43992