MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnexpcld Structured version   Visualization version   GIF version

Theorem nnexpcld 14100
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
StepHypRef Expression
1 nnexpcld.1 . 2 (𝜑𝐴 ∈ ℕ)
2 nnexpcld.2 . 2 (𝜑𝑁 ∈ ℕ0)
3 nnexpcl 13935 . 2 ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴𝑁) ∈ ℕ)
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴𝑁) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7352  cn 12112  0cn0 12372  cexp 13922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7665  ax-cnex 11066  ax-resscn 11067  ax-1cn 11068  ax-icn 11069  ax-addcl 11070  ax-addrcl 11071  ax-mulcl 11072  ax-mulrcl 11073  ax-mulcom 11074  ax-addass 11075  ax-mulass 11076  ax-distr 11077  ax-i2m1 11078  ax-1ne0 11079  ax-1rid 11080  ax-rnegex 11081  ax-rrecex 11082  ax-cnre 11083  ax-pre-lttri 11084  ax-pre-lttrn 11085  ax-pre-ltadd 11086  ax-pre-mulgt0 11087
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7308  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7796  df-2nd 7915  df-frecs 8205  df-wrecs 8236  df-recs 8310  df-rdg 8349  df-er 8607  df-en 8843  df-dom 8844  df-sdom 8845  df-pnf 11150  df-mnf 11151  df-xr 11152  df-ltxr 11153  df-le 11154  df-sub 11346  df-neg 11347  df-nn 12113  df-n0 12373  df-z 12459  df-uz 12723  df-seq 13862  df-exp 13923
This theorem is referenced by:  bitsp1  16271  bitsfzolem  16274  bitsfzo  16275  bitsmod  16276  bitsfi  16277  bitscmp  16278  bitsinv1lem  16281  bitsinv1  16282  2ebits  16287  bitsinvp1  16289  sadcaddlem  16297  sadadd3  16301  sadaddlem  16306  sadasslem  16310  bitsres  16313  bitsuz  16314  bitsshft  16315  smumullem  16332  smumul  16333  rplpwr  16398  rprpwr  16399  rppwr  16400  pclem  16670  pcprendvds2  16673  pcpre1  16674  pcpremul  16675  pcdvdsb  16701  pcidlem  16704  pcid  16705  pcdvdstr  16708  pcgcd1  16709  pcprmpw2  16714  pcaddlem  16720  pcadd  16721  pcfaclem  16730  pcfac  16731  pcbc  16732  oddprmdvds  16735  prmpwdvds  16736  pockthlem  16737  2expltfac  16925  pgpfi1  19336  sylow1lem1  19339  sylow1lem3  19341  sylow1lem4  19342  sylow1lem5  19343  pgpfi  19346  gexexlem  19589  ablfac1lem  19806  ablfac1b  19808  ablfac1eu  19811  aalioulem2  25645  aalioulem5  25648  aaliou3lem9  25662  isppw2  26416  sgmppw  26497  fsumvma2  26514  pclogsum  26515  chpchtsum  26519  logfacubnd  26521  bposlem1  26584  bposlem5  26588  gausslemma2d  26674  lgseisen  26679  chebbnd1lem1  26769  rpvmasumlem  26787  dchrisum0flblem1  26808  dchrisum0flblem2  26809  ostth2lem2  26934  ostth2lem3  26935  oddpwdc  32758  eulerpartlemgh  32782  aks4d1p3  40467  aks4d1p7d1  40471  aks4d1p8d2  40474  aks6d1c2p1  40480  aks6d1c2p2  40481  expgcd  40723  nn0expgcd  40724  numdenexp  40726  dvdsexpnn  40729  fltdvdsabdvdsc  40879  fltaccoprm  40881  fltbccoprm  40882  fltne  40885  flt4lem6  40899  flt4lem7  40900  nna4b4nsq  40901  3cubeslem3r  40913  3cubes  40916  jm3.1lem3  41246  inductionexd  42332  stoweidlem25  44161  stoweidlem45  44181  wallispi2lem1  44207  ovnsubaddlem1  44706  ovolval5lem2  44789  fmtnoodd  45620  fmtnof1  45622  fmtnosqrt  45626  fmtnorec4  45636  odz2prm2pw  45650  fmtnoprmfac1lem  45651  fmtnoprmfac1  45652  fmtnoprmfac2lem1  45653  fmtnoprmfac2  45654  2pwp1prm  45676  lighneallem1  45692  proththdlem  45700  proththd  45701  pw2m1lepw2m1  46496  nnpw2even  46510  logbpw2m1  46548  nnpw2pmod  46564  nnpw2p  46567  nnolog2flm1  46571  dignn0flhalflem1  46596  itcovalt2lem2  46657
  Copyright terms: Public domain W3C validator