Theorem nnexpcld 14277

Description: Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
nnexpcld.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
nnexpcld.2	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
nnexpcld	⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ)

Proof of Theorem nnexpcld

Step	Hyp	Ref	Expression
1		nnexpcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnexpcld.2	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
3		nnexpcl 14106	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℕcn 12228  ℕ₀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:  bitsp1  16484  bitsfzolem  16487  bitsfzo  16488  bitsmod  16489  bitsfi  16490  bitscmp  16491  bitsinv1lem  16494  bitsinv1  16495  2ebits  16500  bitsinvp1  16502  sadcaddlem  16510  sadadd3  16514  sadaddlem  16519  sadasslem  16523  bitsres  16526  bitsuz  16527  bitsshft  16528  smumullem  16545  smumul  16546  rplpwr  16611  rprpwr  16612  rppwr  16613  expgcd  16616  nn0expgcd  16617  numdenexp  16814  pclem  16893  pcprendvds2  16896  pcpre1  16897  pcpremul  16898  pcdvdsb  16924  pcidlem  16927  pcid  16928  pcdvdstr  16931  pcgcd1  16932  pcprmpw2  16937  pcaddlem  16943  pcadd  16944  pcfaclem  16953  pcfac  16954  pcbc  16955  oddprmdvds  16958  prmpwdvds  16959  pockthlem  16960  2expltfac  17147  pgpfi1  19660  sylow1lem1  19663  sylow1lem3  19665  sylow1lem4  19666  sylow1lem5  19667  pgpfi  19670  gexexlem  19917  ablfac1lem  20135  ablfac1b  20137  ablfac1eu  20140  aalioulem2  26496  aalioulem5  26499  aaliou3lem9  26513  isppw2  27279  sgmppw  27361  fsumvma2  27378  pclogsum  27379  chpchtsum  27383  logfacubnd  27385  bposlem1  27448  bposlem5  27452  gausslemma2d  27538  lgseisen  27543  chebbnd1lem1  27633  rpvmasumlem  27651  dchrisum0flblem1  27672  dchrisum0flblem2  27673  ostth2lem2  27798  ostth2lem3  27799  2exple2exp  33178  fldext2rspun  34072  oddpwdc  34744  eulerpartlemgh  34768  aks4d1p3  42845  aks4d1p7d1  42849  aks4d1p8d2  42852  aks6d1c1  42883  aks6d1c2p1  42885  aks6d1c2p2  42886  aks6d1c7  42951  aks5  42971  dvdsexpnn  43094  fltdvdsabdvdsc  43370  fltaccoprm  43372  fltbccoprm  43373  fltne  43376  flt4lem6  43390  flt4lem7  43391  nna4b4nsq  43392  3cubeslem3r  43418  3cubes  43421  jm3.1lem3  43746  inductionexd  44881  stoweidlem25  46739  stoweidlem45  46759  wallispi2lem1  46785  ovnsubaddlem1  47284  ovolval5lem2  47367  fmtnoodd  48285  fmtnof1  48287  fmtnosqrt  48291  fmtnorec4  48301  odz2prm2pw  48315  fmtnoprmfac1lem  48316  fmtnoprmfac1  48317  fmtnoprmfac2lem1  48318  fmtnoprmfac2  48319  2pwp1prm  48341  lighneallem1  48357  proththdlem  48365  proththd  48366  pw2m1lepw2m1  49300  nnpw2even  49309  logbpw2m1  49347  nnpw2pmod  49363  nnpw2p  49366  nnolog2flm1  49370  dignn0flhalflem1  49395  itcovalt2lem2  49456