Theorem 2nn0 12155

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

Syntax hints:   ∈ wcel 2112  2c2 11933  ℕ₀cn0 12138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563  ax-1cn 10835

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-nn 11879  df-2 11941  df-n0 12139

This theorem is referenced by:  nn0n0n1ge2  12205  7p6e13  12419  8p3e11  12422  8p5e13  12424  9p3e12  12429  9p4e13  12430  4t3e12  12439  4t4e16  12440  5t3e15  12442  5t5e25  12444  6t3e18  12446  6t5e30  12448  7t3e21  12451  7t4e28  12452  7t5e35  12453  7t6e42  12454  7t7e49  12455  8t3e24  12457  8t4e32  12458  8t5e40  12459  9t3e27  12464  9t4e36  12465  9t8e72  12469  9t9e81  12470  decbin3  12483  2eluzge0  12537  xnn0le2is012  12884  fzo0to42pr  13377  nn0sqcl  13713  sqmul  13742  resqcl  13747  zsqcl  13751  cu2  13820  i3  13823  i4  13824  binom3  13842  expmulnbnd  13853  nn0opthlem1  13885  fac3  13897  faclbnd2  13908  faclbnd4lem1  13910  faclbnd4lem3  13912  hash2pr  14086  hashtplei  14101  s4fv2  14513  pfx2  14563  repsw3  14567  swrd2lsw  14568  2swrd2eqwrdeq  14569  abssq  14921  sqabs  14922  iseraltlem2  15297  iseraltlem3  15298  bpoly2  15670  bpoly3  15671  bpoly4  15672  fsumcube  15673  ef4p  15725  efgt1p2  15726  efi4p  15749  ef01bndlem  15796  cos01bnd  15798  oexpneg  15957  oddge22np1  15961  bitsinv2  16053  bitsf1ocnv  16054  sadcaddlem  16067  sadadd2lem  16069  pythagtriplem4  16423  iserodd  16439  oddprmdvds  16507  prmreclem2  16521  prmreclem6  16525  vdwlem7  16591  vdwlem10  16594  vdwlem12  16596  dec2dvds  16667  dec5dvds  16668  decexp2  16679  2exp4  16689  2exp5  16690  2exp6  16691  2exp7  16692  2exp8  16693  2exp11  16694  2exp16  16695  3exp3  16696  2expltfac  16697  5prm  16713  7prm  16715  11prm  16719  13prm  16720  17prm  16721  19prm  16722  23prm  16723  prmlem2  16724  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  basendxltdsndx  16994  dsndxnplusgndx  16996  dsndxnmulrndx  16997  slotsdnscsi  16998  dsndxntsetndx  16999  prdsvalstr  17055  smndex2dbas  18443  smndex2dlinvh  18446  pmtrprfval  18985  psgnunilem2  18993  efgredleme  19239  lt6abl  19386  mgpdsOLD  19624  sradsOLD  20344  cnfldstr  20487  cnfldfun  20497  setsmsds  23512  tmslemOLD  23519  tnglemOLD  23678  tngdsOLD  23693  sqcn  23918  ehl2eudis  24466  dveflem  25023  iaa  25365  tangtx  25542  efif1olem3  25580  efif1olem4  25581  root1id  25787  2logb9irr  25825  mcubic  25877  cubic2  25878  cubic  25879  binom4  25880  dquartlem2  25882  dquart  25883  quart1cl  25884  quart1lem  25885  quart1  25886  quartlem1  25887  quartlem2  25888  atandmcj  25939  bndatandm  25959  atansopn  25962  atantayl3  25969  leibpilem2  25971  leibpi  25972  leibpisum  25973  log2cnv  25974  log2tlbnd  25975  log2ublem2  25977  log2ublem3  25978  log2ub  25979  log2le1  25980  birthday  25984  basellem3  26112  basellem4  26113  basellem5  26114  basellem8  26117  issqf  26165  ppi3  26200  ppiublem2  26231  chtublem  26239  mersenne  26255  bcmax  26306  bcp1ctr  26307  bclbnd  26308  bpos1  26311  bposlem6  26317  bposlem8  26319  lgslem1  26325  lgsqrlem2  26375  gausslemma2dlem6  26400  lgseisenlem4  26406  2lgslem1c  26421  2lgslem3a  26424  2lgslem3b  26425  2lgslem3c  26426  2lgslem3d  26427  2sq2  26461  2sqreultlem  26475  2sqreunnltlem  26478  chebbnd1lem3  26499  rplogsumlem2  26513  dchrisumlem2  26518  dchrisum0flblem1  26536  dchrisum0flblem2  26537  dchrisum0flb  26538  selberglem2  26574  pntrmax  26592  pntlemo  26635  slotsinbpsd  26682  slotslnbpsd  26683  trkgstr  26684  ttgplusgOLD  27121  ttgdsOLD  27126  eengstr  27226  usgrexmplef  27504  upgr2wlk  27913  usgr2pthlem  28007  usgr2pth  28008  wpthswwlks2on  28202  elwspths2spth  28208  upgr3v3e3cycl  28420  upgr4cycl4dv4e  28425  konigsbergiedgw  28488  konigsberglem1  28492  konigsberglem2  28493  konigsberglem3  28494  clwlknon2num  28608  1kp2ke3k  28686  ex-mod  28689  ex-exp  28690  ex-fac  28691  9p10ne21  28710  ipidsq  28948  strlem3a  30490  xnn01gt  30970  dpmul4  31065  pfxlsw2ccat  31101  wrdt2ind  31102  madjusmdetlem4  31657  zlmds  31789  coinflippv  32325  prodfzo03  32458  hgt750lemd  32503  hgt750lem  32506  hgt750lem2  32507  hgt750leme  32513  tgoldbachgnn  32514  tgoldbachgtde  32515  tgoldbachgt  32518  cusgredgex  32958  kur14lem8  33050  sinccvglem  33505  dvtan  35733  420gcd8e4  39921  12lcm5e60  39923  60lcm7e420  39925  lcmineqlem17  39960  lcmineqlem18  39961  lcmineqlem20  39963  lcmineqlem21  39964  lcmineqlem22  39965  lcmineqlem  39967  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow2ineq1  39973  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  aks4d1p1p2  39984  aks4d1p1p7  39988  aks4d1p1p5  39989  aks4d1p1  39990  2np3bcnp1  40000  2ap1caineq  40001  fac2xp3  40060  sqn5i  40206  235t711  40212  ex-decpmul  40213  dffltz  40359  flt4lem  40370  flt4lem3  40373  flt4lem7  40384  nna4b4nsq  40385  3cubeslem2  40395  3cubeslem3l  40396  3cubeslem3r  40397  diophin  40482  irrapxlem5  40536  pellexlem2  40540  pell1qrge1  40580  jm2.22  40705  jm2.20nn  40707  jm2.27c  40717  rmydioph  40724  rmxdioph  40726  expdiophlem2  40732  frlmpwfi  40811  isnumbasgrplem3  40818  resqrtvalex  41114  imsqrtvalex  41115  amgm2d  41671  dvdivbd  43327  itgsinexplem1  43358  itgsinexp  43359  stoweidlem1  43405  wallispilem4  43472  wallispilem5  43473  wallispi2lem2  43476  stirlinglem3  43480  stirlinglem5  43482  stirlinglem7  43484  stirlinglem8  43485  stirlinglem10  43487  stirlinglem11  43488  hoiqssbllem2  44024  fmtnoge3  44843  fmtnom1nn  44845  fmtnof1  44848  fmtnorec1  44850  sqrtpwpw2p  44851  fmtnosqrt  44852  fmtnorec2lem  44855  fmtnodvds  44857  fmtnorec3  44861  fmtnorec4  44862  fmtno2  44863  fmtno3  44864  fmtno5lem2  44867  fmtno5lem4  44869  fmtno5  44870  257prm  44874  odz2prm2pw  44876  fmtnoprmfac1lem  44877  fmtnoprmfac2lem1  44879  fmtnofac2lem  44881  fmtnofac2  44882  fmtnofac1  44883  fmtno4prmfac  44885  fmtno4nprmfac193  44887  fmtno4prm  44888  fmtno5faclem1  44892  fmtno5faclem2  44893  fmtno5faclem3  44894  fmtno5fac  44895  flsqrt  44906  139prmALT  44909  31prm  44910  m5prm  44911  127prm  44912  m7prm  44913  m11nprm  44914  sfprmdvdsmersenne  44916  lighneallem2  44919  lighneallem3  44920  lighneallem4a  44921  proththd  44927  3exp4mod41  44929  41prothprmlem1  44930  oexpnegALTV  44990  fppr2odd  45044  2exp340mod341  45046  341fppr2  45047  8exp8mod9  45049  nfermltl2rev  45056  evengpoap3  45112  tgblthelfgott  45128  tgoldbachlt  45129  tgoldbach  45130  pgrple2abl  45562  pgrpgt2nabl  45563  ply1mulgsumlem2  45589  logbpw2m1  45774  blenpw2m1  45786  dignn0ehalf  45824  nn0sumshdiglemA  45826  nn0sumshdiglemB  45827  nn0mullong  45832  2aryfvalel  45854  itcoval2  45871  itcoval3  45872  itcovalt2lem2lem2  45881  itcovalt2lem1  45882  ackval2  45889  ackval3  45890  ackval0012  45896  ackval1012  45897  ackval2012  45898  ackval3012  45899  ackval42  45903  2sphere  45956  itscnhlinecirc02plem3  45991  inlinecirc02p  45994  onetansqsecsq  46322  cotsqcscsq  46323