Theorem nnexpcld 14267

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7414  ℕcn 12249  ℕ₀cn0 12510  ↑cexp 14085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-pss 3953  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-iun 4975  df-br 5126  df-opab 5188  df-mpt 5208  df-tr 5242  df-id 5560  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6303  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7871  df-2nd 7998  df-frecs 8289  df-wrecs 8320  df-recs 8394  df-rdg 8433  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11477  df-neg 11478  df-nn 12250  df-n0 12511  df-z 12598  df-uz 12862  df-seq 14026  df-exp 14086

This theorem is referenced by:  bitsp1  16451  bitsfzolem  16454  bitsfzo  16455  bitsmod  16456  bitsfi  16457  bitscmp  16458  bitsinv1lem  16461  bitsinv1  16462  2ebits  16467  bitsinvp1  16469  sadcaddlem  16477  sadadd3  16481  sadaddlem  16486  sadasslem  16490  bitsres  16493  bitsuz  16494  bitsshft  16495  smumullem  16512  smumul  16513  rplpwr  16578  rprpwr  16579  rppwr  16580  expgcd  16583  nn0expgcd  16584  numdenexp  16780  pclem  16859  pcprendvds2  16862  pcpre1  16863  pcpremul  16864  pcdvdsb  16890  pcidlem  16893  pcid  16894  pcdvdstr  16897  pcgcd1  16898  pcprmpw2  16903  pcaddlem  16909  pcadd  16910  pcfaclem  16919  pcfac  16920  pcbc  16921  oddprmdvds  16924  prmpwdvds  16925  pockthlem  16926  2expltfac  17113  pgpfi1  19586  sylow1lem1  19589  sylow1lem3  19591  sylow1lem4  19592  sylow1lem5  19593  pgpfi  19596  gexexlem  19843  ablfac1lem  20061  ablfac1b  20063  ablfac1eu  20066  aalioulem2  26330  aalioulem5  26333  aaliou3lem9  26347  isppw2  27113  sgmppw  27196  fsumvma2  27213  pclogsum  27214  chpchtsum  27218  logfacubnd  27220  bposlem1  27283  bposlem5  27287  gausslemma2d  27373  lgseisen  27378  chebbnd1lem1  27468  rpvmasumlem  27486  dchrisum0flblem1  27507  dchrisum0flblem2  27508  ostth2lem2  27633  ostth2lem3  27634  2exple2exp  32781  fldext2rspun  33673  oddpwdc  34297  eulerpartlemgh  34321  aks4d1p3  42020  aks4d1p7d1  42024  aks4d1p8d2  42027  aks6d1c1  42058  aks6d1c2p1  42060  aks6d1c2p2  42061  aks6d1c7  42126  aks5  42146  dvdsexpnn  42313  fltdvdsabdvdsc  42593  fltaccoprm  42595  fltbccoprm  42596  fltne  42599  flt4lem6  42613  flt4lem7  42614  nna4b4nsq  42615  3cubeslem3r  42643  3cubes  42646  jm3.1lem3  42976  inductionexd  44113  stoweidlem25  45985  stoweidlem45  46005  wallispi2lem1  46031  ovnsubaddlem1  46530  ovolval5lem2  46613  fmtnoodd  47466  fmtnof1  47468  fmtnosqrt  47472  fmtnorec4  47482  odz2prm2pw  47496  fmtnoprmfac1lem  47497  fmtnoprmfac1  47498  fmtnoprmfac2lem1  47499  fmtnoprmfac2  47500  2pwp1prm  47522  lighneallem1  47538  proththdlem  47546  proththd  47547  pw2m1lepw2m1  48383  nnpw2even  48396  logbpw2m1  48434  nnpw2pmod  48450  nnpw2p  48453  nnolog2flm1  48457  dignn0flhalflem1  48482  itcovalt2lem2  48543