Theorem 2nn0 12570

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 12366	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 12561	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 2108  2c2 12348  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-2 12356  df-n0 12554

This theorem is referenced by:  nn0n0n1ge2  12620  7p6e13  12836  8p3e11  12839  8p5e13  12841  9p3e12  12846  9p4e13  12847  4t3e12  12856  4t4e16  12857  5t3e15  12859  5t5e25  12861  6t3e18  12863  6t5e30  12865  7t3e21  12868  7t4e28  12869  7t5e35  12870  7t6e42  12871  7t7e49  12872  8t3e24  12874  8t4e32  12875  8t5e40  12876  9t3e27  12881  9t4e36  12882  9t8e72  12886  9t9e81  12887  decbin3  12900  2eluzge0  12958  xnn0le2is012  13308  fzo0to42pr  13803  fvf1tp  13840  nn0sqcl  14140  sqmul  14169  resqcl  14174  zsqcl  14179  cu2  14249  i3  14252  i4  14253  binom3  14273  expmulnbnd  14284  nn0opthlem1  14317  fac3  14329  faclbnd2  14340  faclbnd4lem1  14342  faclbnd4lem3  14344  hash2pr  14518  hashtplei  14533  tpf1ofv2  14547  tpfo  14549  s4fv2  14946  pfx2  14996  repsw3  15000  swrd2lsw  15001  2swrd2eqwrdeq  15002  abssq  15355  sqabs  15356  iseraltlem2  15731  iseraltlem3  15732  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  ef4p  16161  efgt1p2  16162  efi4p  16185  ef01bndlem  16232  cos01bnd  16234  oexpneg  16393  oddge22np1  16397  bitsinv2  16489  bitsf1ocnv  16490  sadcaddlem  16503  sadadd2lem  16505  pythagtriplem4  16866  iserodd  16882  oddprmdvds  16950  prmreclem2  16964  prmreclem6  16968  vdwlem7  17034  vdwlem10  17037  vdwlem12  17039  dec2dvds  17110  dec5dvds  17111  decexp2  17122  2exp4  17132  2exp5  17133  2exp6  17134  2exp7  17135  2exp8  17136  2exp11  17137  2exp16  17138  3exp3  17139  2expltfac  17140  5prm  17156  7prm  17158  11prm  17162  13prm  17163  17prm  17164  19prm  17165  23prm  17166  prmlem2  17167  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  basendxltdsndx  17447  dsndxnplusgndx  17449  dsndxnmulrndx  17450  slotsdnscsi  17451  dsndxntsetndx  17452  slotsdifdsndx  17453  slotsdifunifndx  17460  prdsvalstr  17512  smndex2dbas  18949  smndex2dlinvh  18952  pmtrprfval  19529  psgnunilem2  19537  efgredleme  19785  lt6abl  19937  mgpdsOLD  20175  sradsOLD  21215  cnfldstr  21389  cnfldstrOLD  21404  cnfldfunALTOLDOLD  21416  setsmsdsOLD  24509  tmslemOLD  24516  tnglemOLD  24675  tngdsOLD  24690  sqcn  24919  ehl2eudis  25475  dveflem  26037  iaa  26385  tangtx  26565  efif1olem3  26604  efif1olem4  26605  root1id  26815  2logb9irr  26856  mcubic  26908  cubic2  26909  cubic  26910  binom4  26911  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  atandmcj  26970  bndatandm  26990  atansopn  26993  atantayl3  27000  leibpilem2  27002  leibpi  27003  leibpisum  27004  log2cnv  27005  log2tlbnd  27006  log2ublem2  27008  log2ublem3  27009  log2ub  27010  log2le1  27011  birthday  27015  basellem3  27144  basellem4  27145  basellem5  27146  basellem8  27149  issqf  27197  ppi3  27232  ppiublem2  27265  chtublem  27273  mersenne  27289  bcmax  27340  bcp1ctr  27341  bclbnd  27342  bpos1  27345  bposlem6  27351  bposlem8  27353  lgslem1  27359  lgsqrlem2  27409  gausslemma2dlem6  27434  lgseisenlem4  27440  2lgslem1c  27455  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2sq2  27495  2sqreultlem  27509  2sqreunnltlem  27512  chebbnd1lem3  27533  rplogsumlem2  27547  dchrisumlem2  27552  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0flb  27572  selberglem2  27608  pntrmax  27626  pntlemo  27669  slotsinbpsd  28467  slotslnbpsd  28468  trkgstr  28470  ttgplusgOLD  28908  ttgdsOLD  28913  eengstr  29013  usgrexmplef  29294  upgr2wlk  29704  usgr2pthlem  29799  usgr2pth  29800  wpthswwlks2on  29994  elwspths2spth  30000  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsbergiedgw  30280  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  clwlknon2num  30400  1kp2ke3k  30478  ex-mod  30481  ex-exp  30482  ex-fac  30483  9p10ne21  30502  ipidsq  30742  strlem3a  32284  xnn01gt  32777  dpmul4  32878  pfxlsw2ccat  32917  wrdt2ind  32920  eufndx  33259  eufid  33260  evl1deg2  33567  evl1deg3  33568  rtelextdg2lem  33717  rtelextdg2  33718  constrelextdg2  33737  2sqr3minply  33738  madjusmdetlem4  33776  zlmdsOLD  33909  coinflippv  34448  prodfzo03  34580  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  tgoldbachgnn  34636  tgoldbachgtde  34637  tgoldbachgt  34640  cusgredgex  35089  kur14lem8  35181  sinccvglem  35640  dvtan  37630  420gcd8e4  41963  12lcm5e60  41965  60lcm7e420  41967  lcmineqlem17  42002  lcmineqlem18  42003  lcmineqlem20  42005  lcmineqlem21  42006  lcmineqlem22  42007  lcmineqlem  42009  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1p1p2  42027  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  2np3bcnp1  42101  2ap1caineq  42102  aks6d1c7lem1  42137  fac2xp3  42196  sqn5i  42274  235t711  42293  ex-decpmul  42294  nicomachus  42300  dffltz  42589  flt4lem  42600  flt4lem3  42603  flt4lem7  42614  nna4b4nsq  42615  sum9cubes  42627  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  diophin  42728  irrapxlem5  42782  pellexlem2  42786  pell1qrge1  42826  jm2.22  42952  jm2.20nn  42954  jm2.27c  42964  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  frlmpwfi  43055  isnumbasgrplem3  43062  resqrtvalex  43607  imsqrtvalex  43608  amgm2d  44160  dvdivbd  45844  itgsinexplem1  45875  itgsinexp  45876  stoweidlem1  45922  wallispilem4  45989  wallispilem5  45990  wallispi2lem2  45993  stirlinglem3  45997  stirlinglem5  45999  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  hoiqssbllem2  46544  fmtnoge3  47404  fmtnom1nn  47406  fmtnof1  47409  fmtnorec1  47411  sqrtpwpw2p  47412  fmtnosqrt  47413  fmtnorec2lem  47416  fmtnodvds  47418  fmtnorec3  47422  fmtnorec4  47423  fmtno2  47424  fmtno3  47425  fmtno5lem2  47428  fmtno5lem4  47430  fmtno5  47431  257prm  47435  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac2lem1  47440  fmtnofac2lem  47442  fmtnofac2  47443  fmtnofac1  47444  fmtno4prmfac  47446  fmtno4nprmfac193  47448  fmtno4prm  47449  fmtno5faclem1  47453  fmtno5faclem2  47454  fmtno5faclem3  47455  fmtno5fac  47456  flsqrt  47467  139prmALT  47470  31prm  47471  m5prm  47472  127prm  47473  m7prm  47474  m11nprm  47475  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem3  47481  lighneallem4a  47482  proththd  47488  3exp4mod41  47490  41prothprmlem1  47491  oexpnegALTV  47551  fppr2odd  47605  2exp340mod341  47607  341fppr2  47608  8exp8mod9  47610  nfermltl2rev  47617  evengpoap3  47673  tgblthelfgott  47689  tgoldbachlt  47690  tgoldbach  47691  usgrexmpl1lem  47836  usgrexmpl2lem  47841  pgrple2abl  48090  pgrpgt2nabl  48091  ply1mulgsumlem2  48116  logbpw2m1  48301  blenpw2m1  48313  dignn0ehalf  48351  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0mullong  48359  2aryfvalel  48381  itcoval2  48398  itcoval3  48399  itcovalt2lem2lem2  48408  itcovalt2lem1  48409  ackval2  48416  ackval3  48417  ackval0012  48423  ackval1012  48424  ackval2012  48425  ackval3012  48426  ackval42  48430  2sphere  48483  itscnhlinecirc02plem3  48518  inlinecirc02p  48521  onetansqsecsq  48853  cotsqcscsq  48854