Theorem 2nn0 12445

Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
2nn0	⊢ 2 ∈ ℕ0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 12245	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 12436	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 2119  2c2 12227  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-2 12235  df-n0 12429

This theorem is referenced by:  nn0n0n1ge2  12496  7p6e13  12713  8p3e11  12716  8p5e13  12718  9p3e12  12723  9p4e13  12724  4t3e12  12733  4t4e16  12734  5t3e15  12736  5t5e25  12738  6t3e18  12740  6t5e30  12742  7t3e21  12745  7t4e28  12746  7t5e35  12747  7t6e42  12748  7t7e49  12749  8t3e24  12751  8t4e32  12752  8t5e40  12753  9t3e27  12758  9t4e36  12759  9t8e72  12763  9t9e81  12764  decbin3  12777  2eluzge0  12822  xnn0le2is012  13189  fzo0to42pr  13699  fvf1tp  13739  nn0sqcl  14042  sqmul  14072  resqcl  14077  zsqcl  14082  cu2  14153  i3  14156  i4  14157  binom3  14177  expmulnbnd  14188  nn0opthlem1  14221  fac3  14233  faclbnd2  14244  faclbnd4lem1  14246  faclbnd4lem3  14248  hash2pr  14422  hashtplei  14437  tpf1ofv2  14451  tpfo  14453  s4fv2  14850  pfx2  14900  repsw3  14904  swrd2lsw  14905  2swrd2eqwrdeq  14906  abssq  15259  sqabs  15260  iseraltlem2  15636  iseraltlem3  15637  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  ef4p  16071  efgt1p2  16072  efi4p  16095  ef01bndlem  16142  cos01bnd  16144  oexpneg  16305  oddge22np1  16309  bitsinv2  16403  bitsf1ocnv  16404  sadcaddlem  16417  sadadd2lem  16419  pythagtriplem4  16781  iserodd  16797  oddprmdvds  16865  prmreclem2  16879  prmreclem6  16883  vdwlem7  16949  vdwlem10  16952  vdwlem12  16954  dec2dvds  17025  dec5dvds  17026  2exp4  17046  2exp5  17047  2exp6  17048  2exp7  17049  2exp8  17050  2exp11  17051  2exp16  17052  3exp3  17053  2expltfac  17054  5prm  17070  7prm  17072  11prm  17076  13prm  17077  17prm  17078  19prm  17079  23prm  17080  prmlem2  17081  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  basendxltdsndx  17342  dsndxnplusgndx  17344  dsndxnmulrndx  17345  slotsdnscsi  17346  dsndxntsetndx  17347  slotsdifdsndx  17348  slotsdifunifndx  17355  prdsvalstr  17406  smndex2dbas  18876  smndex2dlinvh  18879  pmtrprfval  19453  psgnunilem2  19461  efgredleme  19709  lt6abl  19861  cnfldstr  21349  sqcn  24859  ehl2eudis  25407  dveflem  25964  iaa  26309  tangtx  26487  efif1olem3  26526  efif1olem4  26527  root1id  26736  2logb9irr  26777  mcubic  26829  cubic2  26830  cubic  26831  binom4  26832  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem2  26840  atandmcj  26891  bndatandm  26911  atansopn  26914  atantayl3  26921  leibpilem2  26923  leibpi  26924  leibpisum  26925  log2cnv  26926  log2tlbnd  26927  log2ublem2  26929  log2ublem3  26930  log2ub  26931  log2le1  26932  birthday  26936  basellem3  27064  basellem4  27065  basellem5  27066  basellem8  27069  issqf  27117  ppi3  27152  ppiublem2  27184  chtublem  27192  mersenne  27208  bcmax  27259  bcp1ctr  27260  bclbnd  27261  bpos1  27264  bposlem6  27270  bposlem8  27272  lgslem1  27278  lgsqrlem2  27328  gausslemma2dlem6  27353  lgseisenlem4  27359  2lgslem1c  27374  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2sq2  27414  2sqreultlem  27428  2sqreunnltlem  27431  chebbnd1lem3  27452  rplogsumlem2  27466  dchrisumlem2  27471  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0flb  27491  selberglem2  27527  pntrmax  27545  pntlemo  27588  slotsinbpsd  28527  slotslnbpsd  28528  trkgstr  28530  eengstr  29067  usgrexmplef  29346  upgr2wlk  29753  usgr2pthlem  29849  usgr2pth  29850  wpthswwlks2on  30050  elwspths2spth  30056  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  konigsbergiedgw  30336  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  clwlknon2num  30456  1kp2ke3k  30534  ex-mod  30537  ex-exp  30538  ex-fac  30539  9p10ne21  30558  ipidsq  30799  strlem3a  32341  xnn01gt  32862  expevenpos  32938  dpmul4  32992  pfxlsw2ccat  33029  wrdt2ind  33032  eufndx  33374  eufid  33375  evl1deg2  33660  evl1deg3  33661  fldext2rspun  33866  rtelextdg2lem  33910  rtelextdg2  33911  constrelextdg2  33931  2sqr3minply  33964  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  cos9thpinconstrlem1  33973  madjusmdetlem4  34014  coinflippv  34668  prodfzo03  34787  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  tgoldbachgnn  34843  tgoldbachgtde  34844  tgoldbachgt  34847  cusgredgex  35350  kur14lem8  35441  sinccvglem  35900  dvtan  38037  420gcd8e4  42491  12lcm5e60  42493  60lcm7e420  42495  lcmineqlem17  42530  lcmineqlem18  42531  lcmineqlem20  42533  lcmineqlem21  42534  lcmineqlem22  42535  lcmineqlem  42537  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow5ineq2  42540  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p2  42555  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  2np3bcnp1  42629  2ap1caineq  42630  aks6d1c7lem1  42665  sqn5i  42762  235t711  42782  ex-decpmul  42783  nicomachus  42789  dffltz  43084  flt4lem  43095  flt4lem3  43098  flt4lem7  43109  nna4b4nsq  43110  sum9cubes  43122  3cubeslem2  43134  3cubeslem3l  43135  3cubeslem3r  43136  diophin  43221  irrapxlem5  43271  pellexlem2  43275  pell1qrge1  43315  jm2.22  43440  jm2.20nn  43442  jm2.27c  43452  rmydioph  43459  rmxdioph  43461  expdiophlem2  43467  frlmpwfi  43543  isnumbasgrplem3  43550  resqrtvalex  44089  imsqrtvalex  44090  amgm2d  44642  dvdivbd  46366  itgsinexplem1  46397  itgsinexp  46398  stoweidlem1  46444  wallispilem4  46511  wallispilem5  46512  wallispi2lem2  46515  stirlinglem3  46519  stirlinglem5  46521  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  hoiqssbllem2  47066  nthrucw  47331  sin3t  47334  cos3t  47335  sin5tlem1  47336  sin5tlem2  47337  sin5tlem4  47339  fmtnoge3  48008  fmtnom1nn  48010  fmtnof1  48013  fmtnorec1  48015  sqrtpwpw2p  48016  fmtnosqrt  48017  fmtnorec2lem  48020  fmtnodvds  48022  fmtnorec3  48026  fmtnorec4  48027  fmtno2  48028  fmtno3  48029  fmtno5lem2  48032  fmtno5lem4  48034  fmtno5  48035  257prm  48039  odz2prm2pw  48041  fmtnoprmfac1lem  48042  fmtnoprmfac2lem1  48044  fmtnofac2lem  48046  fmtnofac2  48047  fmtnofac1  48048  fmtno4prmfac  48050  fmtno4nprmfac193  48052  fmtno4prm  48053  fmtno5faclem1  48057  fmtno5faclem2  48058  fmtno5faclem3  48059  fmtno5fac  48060  flsqrt  48071  139prmALT  48074  31prm  48075  m5prm  48076  127prm  48077  m7prm  48078  m11nprm  48079  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem3  48085  lighneallem4a  48086  proththd  48092  3exp4mod41  48094  41prothprmlem1  48095  oexpnegALTV  48168  fppr2odd  48222  2exp340mod341  48224  341fppr2  48225  8exp8mod9  48227  nfermltl2rev  48234  evengpoap3  48290  tgblthelfgott  48306  tgoldbachlt  48307  tgoldbach  48308  cycl3grtri  48438  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpg3nbgrvtx0  48567  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem10  48595  gpg5edgnedg  48621  pgrple2abl  48856  pgrpgt2nabl  48857  ply1mulgsumlem2  48878  logbpw2m1  49058  blenpw2m1  49070  dignn0ehalf  49108  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0mullong  49116  2aryfvalel  49138  itcoval2  49155  itcoval3  49156  itcovalt2lem2lem2  49165  itcovalt2lem1  49166  ackval2  49173  ackval3  49174  ackval0012  49180  ackval1012  49181  ackval2012  49182  ackval3012  49183  ackval42  49187  2sphere  49240  itscnhlinecirc02plem3  49275  inlinecirc02p  49278  onetansqsecsq  50251  cotsqcscsq  50252