Theorem 2nn0 12398

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

Syntax hints:   ∈ wcel 2111  2c2 12180  ℕ₀cn0 12381

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-2 12188  df-n0 12382

This theorem is referenced by:  nn0n0n1ge2  12449  7p6e13  12666  8p3e11  12669  8p5e13  12671  9p3e12  12676  9p4e13  12677  4t3e12  12686  4t4e16  12687  5t3e15  12689  5t5e25  12691  6t3e18  12693  6t5e30  12695  7t3e21  12698  7t4e28  12699  7t5e35  12700  7t6e42  12701  7t7e49  12702  8t3e24  12704  8t4e32  12705  8t5e40  12706  9t3e27  12711  9t4e36  12712  9t8e72  12716  9t9e81  12717  decbin3  12730  2eluzge0  12779  xnn0le2is012  13145  fzo0to42pr  13653  fvf1tp  13693  nn0sqcl  13996  sqmul  14026  resqcl  14031  zsqcl  14036  cu2  14107  i3  14110  i4  14111  binom3  14131  expmulnbnd  14142  nn0opthlem1  14175  fac3  14187  faclbnd2  14198  faclbnd4lem1  14200  faclbnd4lem3  14202  hash2pr  14376  hashtplei  14391  tpf1ofv2  14405  tpfo  14407  s4fv2  14804  pfx2  14854  repsw3  14858  swrd2lsw  14859  2swrd2eqwrdeq  14860  abssq  15213  sqabs  15214  iseraltlem2  15590  iseraltlem3  15591  bpoly2  15964  bpoly3  15965  bpoly4  15966  fsumcube  15967  ef4p  16022  efgt1p2  16023  efi4p  16046  ef01bndlem  16093  cos01bnd  16095  oexpneg  16256  oddge22np1  16260  bitsinv2  16354  bitsf1ocnv  16355  sadcaddlem  16368  sadadd2lem  16370  pythagtriplem4  16731  iserodd  16747  oddprmdvds  16815  prmreclem2  16829  prmreclem6  16833  vdwlem7  16899  vdwlem10  16902  vdwlem12  16904  dec2dvds  16975  dec5dvds  16976  2exp4  16996  2exp5  16997  2exp6  16998  2exp7  16999  2exp8  17000  2exp11  17001  2exp16  17002  3exp3  17003  2expltfac  17004  5prm  17020  7prm  17022  11prm  17026  13prm  17027  17prm  17028  19prm  17029  23prm  17030  prmlem2  17031  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  basendxltdsndx  17292  dsndxnplusgndx  17294  dsndxnmulrndx  17295  slotsdnscsi  17296  dsndxntsetndx  17297  slotsdifdsndx  17298  slotsdifunifndx  17305  prdsvalstr  17356  smndex2dbas  18822  smndex2dlinvh  18825  pmtrprfval  19400  psgnunilem2  19408  efgredleme  19656  lt6abl  19808  cnfldstr  21294  cnfldstrOLD  21309  sqcn  24795  ehl2eudis  25350  dveflem  25911  iaa  26261  tangtx  26442  efif1olem3  26481  efif1olem4  26482  root1id  26692  2logb9irr  26733  mcubic  26785  cubic2  26786  cubic  26787  binom4  26788  dquartlem2  26790  dquart  26791  quart1cl  26792  quart1lem  26793  quart1  26794  quartlem1  26795  quartlem2  26796  atandmcj  26847  bndatandm  26867  atansopn  26870  atantayl3  26877  leibpilem2  26879  leibpi  26880  leibpisum  26881  log2cnv  26882  log2tlbnd  26883  log2ublem2  26885  log2ublem3  26886  log2ub  26887  log2le1  26888  birthday  26892  basellem3  27021  basellem4  27022  basellem5  27023  basellem8  27026  issqf  27074  ppi3  27109  ppiublem2  27142  chtublem  27150  mersenne  27166  bcmax  27217  bcp1ctr  27218  bclbnd  27219  bpos1  27222  bposlem6  27228  bposlem8  27230  lgslem1  27236  lgsqrlem2  27286  gausslemma2dlem6  27311  lgseisenlem4  27317  2lgslem1c  27332  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  2sq2  27372  2sqreultlem  27386  2sqreunnltlem  27389  chebbnd1lem3  27410  rplogsumlem2  27424  dchrisumlem2  27429  dchrisum0flblem1  27447  dchrisum0flblem2  27448  dchrisum0flb  27449  selberglem2  27485  pntrmax  27503  pntlemo  27546  slotsinbpsd  28420  slotslnbpsd  28421  trkgstr  28423  eengstr  28959  usgrexmplef  29238  upgr2wlk  29646  usgr2pthlem  29742  usgr2pth  29743  wpthswwlks2on  29940  elwspths2spth  29946  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  konigsbergiedgw  30226  konigsberglem1  30230  konigsberglem2  30231  konigsberglem3  30232  clwlknon2num  30346  1kp2ke3k  30424  ex-mod  30427  ex-exp  30428  ex-fac  30429  9p10ne21  30448  ipidsq  30688  strlem3a  32230  xnn01gt  32751  expevenpos  32827  dpmul4  32892  pfxlsw2ccat  32929  wrdt2ind  32932  eufndx  33254  eufid  33255  evl1deg2  33538  evl1deg3  33539  fldext2rspun  33693  rtelextdg2lem  33737  rtelextdg2  33738  constrelextdg2  33758  2sqr3minply  33791  cos9thpiminplylem1  33793  cos9thpiminplylem2  33794  cos9thpiminplylem4  33796  cos9thpiminplylem5  33797  cos9thpinconstrlem1  33800  madjusmdetlem4  33841  coinflippv  34495  prodfzo03  34614  hgt750lemd  34659  hgt750lem  34662  hgt750lem2  34663  hgt750leme  34669  tgoldbachgnn  34670  tgoldbachgtde  34671  tgoldbachgt  34674  cusgredgex  35164  kur14lem8  35255  sinccvglem  35714  dvtan  37716  420gcd8e4  42045  12lcm5e60  42047  60lcm7e420  42049  lcmineqlem17  42084  lcmineqlem18  42085  lcmineqlem20  42087  lcmineqlem21  42088  lcmineqlem22  42089  lcmineqlem  42091  3exp7  42092  3lexlogpow5ineq1  42093  3lexlogpow5ineq2  42094  3lexlogpow2ineq1  42097  3lexlogpow2ineq2  42098  3lexlogpow5ineq5  42099  aks4d1p1p2  42109  aks4d1p1p7  42113  aks4d1p1p5  42114  aks4d1p1  42115  2np3bcnp1  42183  2ap1caineq  42184  aks6d1c7lem1  42219  sqn5i  42324  235t711  42344  ex-decpmul  42345  nicomachus  42351  dffltz  42673  flt4lem  42684  flt4lem3  42687  flt4lem7  42698  nna4b4nsq  42699  sum9cubes  42711  3cubeslem2  42724  3cubeslem3l  42725  3cubeslem3r  42726  diophin  42811  irrapxlem5  42865  pellexlem2  42869  pell1qrge1  42909  jm2.22  43034  jm2.20nn  43036  jm2.27c  43046  rmydioph  43053  rmxdioph  43055  expdiophlem2  43061  frlmpwfi  43137  isnumbasgrplem3  43144  resqrtvalex  43684  imsqrtvalex  43685  amgm2d  44237  dvdivbd  45967  itgsinexplem1  45998  itgsinexp  45999  stoweidlem1  46045  wallispilem4  46112  wallispilem5  46113  wallispi2lem2  46116  stirlinglem3  46120  stirlinglem5  46122  stirlinglem7  46124  stirlinglem8  46125  stirlinglem10  46127  stirlinglem11  46128  hoiqssbllem2  46667  fmtnoge3  47567  fmtnom1nn  47569  fmtnof1  47572  fmtnorec1  47574  sqrtpwpw2p  47575  fmtnosqrt  47576  fmtnorec2lem  47579  fmtnodvds  47581  fmtnorec3  47585  fmtnorec4  47586  fmtno2  47587  fmtno3  47588  fmtno5lem2  47591  fmtno5lem4  47593  fmtno5  47594  257prm  47598  odz2prm2pw  47600  fmtnoprmfac1lem  47601  fmtnoprmfac2lem1  47603  fmtnofac2lem  47605  fmtnofac2  47606  fmtnofac1  47607  fmtno4prmfac  47609  fmtno4nprmfac193  47611  fmtno4prm  47612  fmtno5faclem1  47616  fmtno5faclem2  47617  fmtno5faclem3  47618  fmtno5fac  47619  flsqrt  47630  139prmALT  47633  31prm  47634  m5prm  47635  127prm  47636  m7prm  47637  m11nprm  47638  sfprmdvdsmersenne  47640  lighneallem2  47643  lighneallem3  47644  lighneallem4a  47645  proththd  47651  3exp4mod41  47653  41prothprmlem1  47654  oexpnegALTV  47714  fppr2odd  47768  2exp340mod341  47770  341fppr2  47771  8exp8mod9  47773  nfermltl2rev  47780  evengpoap3  47836  tgblthelfgott  47852  tgoldbachlt  47853  tgoldbach  47854  cycl3grtri  47984  usgrexmpl1lem  48058  usgrexmpl2lem  48063  gpg3nbgrvtx0  48113  gpgprismgr4cycllem7  48138  gpgprismgr4cycllem10  48141  gpg5edgnedg  48167  pgrple2abl  48402  pgrpgt2nabl  48403  ply1mulgsumlem2  48425  logbpw2m1  48605  blenpw2m1  48617  dignn0ehalf  48655  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  nn0mullong  48663  2aryfvalel  48685  itcoval2  48702  itcoval3  48703  itcovalt2lem2lem2  48712  itcovalt2lem1  48713  ackval2  48720  ackval3  48721  ackval0012  48727  ackval1012  48728  ackval2012  48729  ackval3012  48730  ackval42  48734  2sphere  48787  itscnhlinecirc02plem3  48822  inlinecirc02p  48825  onetansqsecsq  49799  cotsqcscsq  49800