Theorem 2nn0 12409

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

Syntax hints:   ∈ wcel 2113  2c2 12191  ℕ₀cn0 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11075

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-nn 12137  df-2 12199  df-n0 12393

This theorem is referenced by:  nn0n0n1ge2  12460  7p6e13  12676  8p3e11  12679  8p5e13  12681  9p3e12  12686  9p4e13  12687  4t3e12  12696  4t4e16  12697  5t3e15  12699  5t5e25  12701  6t3e18  12703  6t5e30  12705  7t3e21  12708  7t4e28  12709  7t5e35  12710  7t6e42  12711  7t7e49  12712  8t3e24  12714  8t4e32  12715  8t5e40  12716  9t3e27  12721  9t4e36  12722  9t8e72  12726  9t9e81  12727  decbin3  12740  2eluzge0  12785  xnn0le2is012  13152  fzo0to42pr  13660  fvf1tp  13700  nn0sqcl  14003  sqmul  14033  resqcl  14038  zsqcl  14043  cu2  14114  i3  14117  i4  14118  binom3  14138  expmulnbnd  14149  nn0opthlem1  14182  fac3  14194  faclbnd2  14205  faclbnd4lem1  14207  faclbnd4lem3  14209  hash2pr  14383  hashtplei  14398  tpf1ofv2  14412  tpfo  14414  s4fv2  14811  pfx2  14861  repsw3  14865  swrd2lsw  14866  2swrd2eqwrdeq  14867  abssq  15220  sqabs  15221  iseraltlem2  15597  iseraltlem3  15598  bpoly2  15971  bpoly3  15972  bpoly4  15973  fsumcube  15974  ef4p  16029  efgt1p2  16030  efi4p  16053  ef01bndlem  16100  cos01bnd  16102  oexpneg  16263  oddge22np1  16267  bitsinv2  16361  bitsf1ocnv  16362  sadcaddlem  16375  sadadd2lem  16377  pythagtriplem4  16738  iserodd  16754  oddprmdvds  16822  prmreclem2  16836  prmreclem6  16840  vdwlem7  16906  vdwlem10  16909  vdwlem12  16911  dec2dvds  16982  dec5dvds  16983  2exp4  17003  2exp5  17004  2exp6  17005  2exp7  17006  2exp8  17007  2exp11  17008  2exp16  17009  3exp3  17010  2expltfac  17011  5prm  17027  7prm  17029  11prm  17033  13prm  17034  17prm  17035  19prm  17036  23prm  17037  prmlem2  17038  37prm  17039  43prm  17040  83prm  17041  139prm  17042  163prm  17043  317prm  17044  631prm  17045  1259lem1  17049  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  1259prm  17054  2503lem1  17055  2503lem2  17056  2503lem3  17057  2503prm  17058  4001lem1  17059  4001lem2  17060  4001lem3  17061  4001lem4  17062  4001prm  17063  basendxltdsndx  17299  dsndxnplusgndx  17301  dsndxnmulrndx  17302  slotsdnscsi  17303  dsndxntsetndx  17304  slotsdifdsndx  17305  slotsdifunifndx  17312  prdsvalstr  17363  smndex2dbas  18830  smndex2dlinvh  18833  pmtrprfval  19407  psgnunilem2  19415  efgredleme  19663  lt6abl  19815  cnfldstr  21302  cnfldstrOLD  21317  sqcn  24814  ehl2eudis  25369  dveflem  25930  iaa  26280  tangtx  26461  efif1olem3  26500  efif1olem4  26501  root1id  26711  2logb9irr  26752  mcubic  26804  cubic2  26805  cubic  26806  binom4  26807  dquartlem2  26809  dquart  26810  quart1cl  26811  quart1lem  26812  quart1  26813  quartlem1  26814  quartlem2  26815  atandmcj  26866  bndatandm  26886  atansopn  26889  atantayl3  26896  leibpilem2  26898  leibpi  26899  leibpisum  26900  log2cnv  26901  log2tlbnd  26902  log2ublem2  26904  log2ublem3  26905  log2ub  26906  log2le1  26907  birthday  26911  basellem3  27040  basellem4  27041  basellem5  27042  basellem8  27045  issqf  27093  ppi3  27128  ppiublem2  27161  chtublem  27169  mersenne  27185  bcmax  27236  bcp1ctr  27237  bclbnd  27238  bpos1  27241  bposlem6  27247  bposlem8  27249  lgslem1  27255  lgsqrlem2  27305  gausslemma2dlem6  27330  lgseisenlem4  27336  2lgslem1c  27351  2lgslem3a  27354  2lgslem3b  27355  2lgslem3c  27356  2lgslem3d  27357  2sq2  27391  2sqreultlem  27405  2sqreunnltlem  27408  chebbnd1lem3  27429  rplogsumlem2  27443  dchrisumlem2  27448  dchrisum0flblem1  27466  dchrisum0flblem2  27467  dchrisum0flb  27468  selberglem2  27504  pntrmax  27522  pntlemo  27565  slotsinbpsd  28439  slotslnbpsd  28440  trkgstr  28442  eengstr  28979  usgrexmplef  29258  upgr2wlk  29666  usgr2pthlem  29762  usgr2pth  29763  wpthswwlks2on  29963  elwspths2spth  29969  upgr3v3e3cycl  30181  upgr4cycl4dv4e  30186  konigsbergiedgw  30249  konigsberglem1  30253  konigsberglem2  30254  konigsberglem3  30255  clwlknon2num  30369  1kp2ke3k  30447  ex-mod  30450  ex-exp  30451  ex-fac  30452  9p10ne21  30471  ipidsq  30711  strlem3a  32253  xnn01gt  32778  expevenpos  32855  dpmul4  32923  pfxlsw2ccat  32960  wrdt2ind  32963  eufndx  33300  eufid  33301  evl1deg2  33586  evl1deg3  33587  fldext2rspun  33767  rtelextdg2lem  33811  rtelextdg2  33812  constrelextdg2  33832  2sqr3minply  33865  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminplylem4  33870  cos9thpiminplylem5  33871  cos9thpinconstrlem1  33874  madjusmdetlem4  33915  coinflippv  34569  prodfzo03  34688  hgt750lemd  34733  hgt750lem  34736  hgt750lem2  34737  hgt750leme  34743  tgoldbachgnn  34744  tgoldbachgtde  34745  tgoldbachgt  34748  cusgredgex  35238  kur14lem8  35329  sinccvglem  35788  dvtan  37783  420gcd8e4  42172  12lcm5e60  42174  60lcm7e420  42176  lcmineqlem17  42211  lcmineqlem18  42212  lcmineqlem20  42214  lcmineqlem21  42215  lcmineqlem22  42216  lcmineqlem  42218  3exp7  42219  3lexlogpow5ineq1  42220  3lexlogpow5ineq2  42221  3lexlogpow2ineq1  42224  3lexlogpow2ineq2  42225  3lexlogpow5ineq5  42226  aks4d1p1p2  42236  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  2np3bcnp1  42310  2ap1caineq  42311  aks6d1c7lem1  42346  sqn5i  42455  235t711  42475  ex-decpmul  42476  nicomachus  42482  dffltz  42792  flt4lem  42803  flt4lem3  42806  flt4lem7  42817  nna4b4nsq  42818  sum9cubes  42830  3cubeslem2  42842  3cubeslem3l  42843  3cubeslem3r  42844  diophin  42929  irrapxlem5  42983  pellexlem2  42987  pell1qrge1  43027  jm2.22  43152  jm2.20nn  43154  jm2.27c  43164  rmydioph  43171  rmxdioph  43173  expdiophlem2  43179  frlmpwfi  43255  isnumbasgrplem3  43262  resqrtvalex  43802  imsqrtvalex  43803  amgm2d  44355  dvdivbd  46083  itgsinexplem1  46114  itgsinexp  46115  stoweidlem1  46161  wallispilem4  46228  wallispilem5  46229  wallispi2lem2  46232  stirlinglem3  46236  stirlinglem5  46238  stirlinglem7  46240  stirlinglem8  46241  stirlinglem10  46243  stirlinglem11  46244  hoiqssbllem2  46783  nthrucw  47046  fmtnoge3  47692  fmtnom1nn  47694  fmtnof1  47697  fmtnorec1  47699  sqrtpwpw2p  47700  fmtnosqrt  47701  fmtnorec2lem  47704  fmtnodvds  47706  fmtnorec3  47710  fmtnorec4  47711  fmtno2  47712  fmtno3  47713  fmtno5lem2  47716  fmtno5lem4  47718  fmtno5  47719  257prm  47723  odz2prm2pw  47725  fmtnoprmfac1lem  47726  fmtnoprmfac2lem1  47728  fmtnofac2lem  47730  fmtnofac2  47731  fmtnofac1  47732  fmtno4prmfac  47734  fmtno4nprmfac193  47736  fmtno4prm  47737  fmtno5faclem1  47741  fmtno5faclem2  47742  fmtno5faclem3  47743  fmtno5fac  47744  flsqrt  47755  139prmALT  47758  31prm  47759  m5prm  47760  127prm  47761  m7prm  47762  m11nprm  47763  sfprmdvdsmersenne  47765  lighneallem2  47768  lighneallem3  47769  lighneallem4a  47770  proththd  47776  3exp4mod41  47778  41prothprmlem1  47779  oexpnegALTV  47839  fppr2odd  47893  2exp340mod341  47895  341fppr2  47896  8exp8mod9  47898  nfermltl2rev  47905  evengpoap3  47961  tgblthelfgott  47977  tgoldbachlt  47978  tgoldbach  47979  cycl3grtri  48109  usgrexmpl1lem  48183  usgrexmpl2lem  48188  gpg3nbgrvtx0  48238  gpgprismgr4cycllem7  48263  gpgprismgr4cycllem10  48266  gpg5edgnedg  48292  pgrple2abl  48527  pgrpgt2nabl  48528  ply1mulgsumlem2  48549  logbpw2m1  48729  blenpw2m1  48741  dignn0ehalf  48779  nn0sumshdiglemA  48781  nn0sumshdiglemB  48782  nn0mullong  48787  2aryfvalel  48809  itcoval2  48826  itcoval3  48827  itcovalt2lem2lem2  48836  itcovalt2lem1  48837  ackval2  48844  ackval3  48845  ackval0012  48851  ackval1012  48852  ackval2012  48853  ackval3012  48854  ackval42  48858  2sphere  48911  itscnhlinecirc02plem3  48946  inlinecirc02p  48949  onetansqsecsq  49922  cotsqcscsq  49923