Theorem 2nn0 12430

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

Syntax hints:   ∈ wcel 2114  2c2 12212  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-2 12220  df-n0 12414

This theorem is referenced by:  nn0n0n1ge2  12481  7p6e13  12697  8p3e11  12700  8p5e13  12702  9p3e12  12707  9p4e13  12708  4t3e12  12717  4t4e16  12718  5t3e15  12720  5t5e25  12722  6t3e18  12724  6t5e30  12726  7t3e21  12729  7t4e28  12730  7t5e35  12731  7t6e42  12732  7t7e49  12733  8t3e24  12735  8t4e32  12736  8t5e40  12737  9t3e27  12742  9t4e36  12743  9t8e72  12747  9t9e81  12748  decbin3  12761  2eluzge0  12806  xnn0le2is012  13173  fzo0to42pr  13681  fvf1tp  13721  nn0sqcl  14024  sqmul  14054  resqcl  14059  zsqcl  14064  cu2  14135  i3  14138  i4  14139  binom3  14159  expmulnbnd  14170  nn0opthlem1  14203  fac3  14215  faclbnd2  14226  faclbnd4lem1  14228  faclbnd4lem3  14230  hash2pr  14404  hashtplei  14419  tpf1ofv2  14433  tpfo  14435  s4fv2  14832  pfx2  14882  repsw3  14886  swrd2lsw  14887  2swrd2eqwrdeq  14888  abssq  15241  sqabs  15242  iseraltlem2  15618  iseraltlem3  15619  bpoly2  15992  bpoly3  15993  bpoly4  15994  fsumcube  15995  ef4p  16050  efgt1p2  16051  efi4p  16074  ef01bndlem  16121  cos01bnd  16123  oexpneg  16284  oddge22np1  16288  bitsinv2  16382  bitsf1ocnv  16383  sadcaddlem  16396  sadadd2lem  16398  pythagtriplem4  16759  iserodd  16775  oddprmdvds  16843  prmreclem2  16857  prmreclem6  16861  vdwlem7  16927  vdwlem10  16930  vdwlem12  16932  dec2dvds  17003  dec5dvds  17004  2exp4  17024  2exp5  17025  2exp6  17026  2exp7  17027  2exp8  17028  2exp11  17029  2exp16  17030  3exp3  17031  2expltfac  17032  5prm  17048  7prm  17050  11prm  17054  13prm  17055  17prm  17056  19prm  17057  23prm  17058  prmlem2  17059  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  basendxltdsndx  17320  dsndxnplusgndx  17322  dsndxnmulrndx  17323  slotsdnscsi  17324  dsndxntsetndx  17325  slotsdifdsndx  17326  slotsdifunifndx  17333  prdsvalstr  17384  smndex2dbas  18851  smndex2dlinvh  18854  pmtrprfval  19428  psgnunilem2  19436  efgredleme  19684  lt6abl  19836  cnfldstr  21323  cnfldstrOLD  21338  sqcn  24835  ehl2eudis  25390  dveflem  25951  iaa  26301  tangtx  26482  efif1olem3  26521  efif1olem4  26522  root1id  26732  2logb9irr  26773  mcubic  26825  cubic2  26826  cubic  26827  binom4  26828  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  atandmcj  26887  bndatandm  26907  atansopn  26910  atantayl3  26917  leibpilem2  26919  leibpi  26920  leibpisum  26921  log2cnv  26922  log2tlbnd  26923  log2ublem2  26925  log2ublem3  26926  log2ub  26927  log2le1  26928  birthday  26932  basellem3  27061  basellem4  27062  basellem5  27063  basellem8  27066  issqf  27114  ppi3  27149  ppiublem2  27182  chtublem  27190  mersenne  27206  bcmax  27257  bcp1ctr  27258  bclbnd  27259  bpos1  27262  bposlem6  27268  bposlem8  27270  lgslem1  27276  lgsqrlem2  27326  gausslemma2dlem6  27351  lgseisenlem4  27357  2lgslem1c  27372  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2sq2  27412  2sqreultlem  27426  2sqreunnltlem  27429  chebbnd1lem3  27450  rplogsumlem2  27464  dchrisumlem2  27469  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0flb  27489  selberglem2  27525  pntrmax  27543  pntlemo  27586  slotsinbpsd  28525  slotslnbpsd  28526  trkgstr  28528  eengstr  29065  usgrexmplef  29344  upgr2wlk  29752  usgr2pthlem  29848  usgr2pth  29849  wpthswwlks2on  30049  elwspths2spth  30055  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  konigsbergiedgw  30335  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  clwlknon2num  30455  1kp2ke3k  30533  ex-mod  30536  ex-exp  30537  ex-fac  30538  9p10ne21  30557  ipidsq  30797  strlem3a  32339  xnn01gt  32860  expevenpos  32937  dpmul4  33005  pfxlsw2ccat  33042  wrdt2ind  33045  eufndx  33383  eufid  33384  evl1deg2  33669  evl1deg3  33670  fldext2rspun  33859  rtelextdg2lem  33903  rtelextdg2  33904  constrelextdg2  33924  2sqr3minply  33957  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  cos9thpiminplylem4  33962  cos9thpiminplylem5  33963  cos9thpinconstrlem1  33966  madjusmdetlem4  34007  coinflippv  34661  prodfzo03  34780  hgt750lemd  34825  hgt750lem  34828  hgt750lem2  34829  hgt750leme  34835  tgoldbachgnn  34836  tgoldbachgtde  34837  tgoldbachgt  34840  cusgredgex  35335  kur14lem8  35426  sinccvglem  35885  dvtan  37918  420gcd8e4  42373  12lcm5e60  42375  60lcm7e420  42377  lcmineqlem17  42412  lcmineqlem18  42413  lcmineqlem20  42415  lcmineqlem21  42416  lcmineqlem22  42417  lcmineqlem  42419  3exp7  42420  3lexlogpow5ineq1  42421  3lexlogpow5ineq2  42422  3lexlogpow2ineq1  42425  3lexlogpow2ineq2  42426  3lexlogpow5ineq5  42427  aks4d1p1p2  42437  aks4d1p1p7  42441  aks4d1p1p5  42442  aks4d1p1  42443  2np3bcnp1  42511  2ap1caineq  42512  aks6d1c7lem1  42547  sqn5i  42652  235t711  42672  ex-decpmul  42673  nicomachus  42679  dffltz  42989  flt4lem  43000  flt4lem3  43003  flt4lem7  43014  nna4b4nsq  43015  sum9cubes  43027  3cubeslem2  43039  3cubeslem3l  43040  3cubeslem3r  43041  diophin  43126  irrapxlem5  43180  pellexlem2  43184  pell1qrge1  43224  jm2.22  43349  jm2.20nn  43351  jm2.27c  43361  rmydioph  43368  rmxdioph  43370  expdiophlem2  43376  frlmpwfi  43452  isnumbasgrplem3  43459  resqrtvalex  43998  imsqrtvalex  43999  amgm2d  44551  dvdivbd  46278  itgsinexplem1  46309  itgsinexp  46310  stoweidlem1  46356  wallispilem4  46423  wallispilem5  46424  wallispi2lem2  46427  stirlinglem3  46431  stirlinglem5  46433  stirlinglem7  46435  stirlinglem8  46436  stirlinglem10  46438  stirlinglem11  46439  hoiqssbllem2  46978  nthrucw  47241  fmtnoge3  47887  fmtnom1nn  47889  fmtnof1  47892  fmtnorec1  47894  sqrtpwpw2p  47895  fmtnosqrt  47896  fmtnorec2lem  47899  fmtnodvds  47901  fmtnorec3  47905  fmtnorec4  47906  fmtno2  47907  fmtno3  47908  fmtno5lem2  47911  fmtno5lem4  47913  fmtno5  47914  257prm  47918  odz2prm2pw  47920  fmtnoprmfac1lem  47921  fmtnoprmfac2lem1  47923  fmtnofac2lem  47925  fmtnofac2  47926  fmtnofac1  47927  fmtno4prmfac  47929  fmtno4nprmfac193  47931  fmtno4prm  47932  fmtno5faclem1  47936  fmtno5faclem2  47937  fmtno5faclem3  47938  fmtno5fac  47939  flsqrt  47950  139prmALT  47953  31prm  47954  m5prm  47955  127prm  47956  m7prm  47957  m11nprm  47958  sfprmdvdsmersenne  47960  lighneallem2  47963  lighneallem3  47964  lighneallem4a  47965  proththd  47971  3exp4mod41  47973  41prothprmlem1  47974  oexpnegALTV  48034  fppr2odd  48088  2exp340mod341  48090  341fppr2  48091  8exp8mod9  48093  nfermltl2rev  48100  evengpoap3  48156  tgblthelfgott  48172  tgoldbachlt  48173  tgoldbach  48174  cycl3grtri  48304  usgrexmpl1lem  48378  usgrexmpl2lem  48383  gpg3nbgrvtx0  48433  gpgprismgr4cycllem7  48458  gpgprismgr4cycllem10  48461  gpg5edgnedg  48487  pgrple2abl  48722  pgrpgt2nabl  48723  ply1mulgsumlem2  48744  logbpw2m1  48924  blenpw2m1  48936  dignn0ehalf  48974  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977  nn0mullong  48982  2aryfvalel  49004  itcoval2  49021  itcoval3  49022  itcovalt2lem2lem2  49031  itcovalt2lem1  49032  ackval2  49039  ackval3  49040  ackval0012  49046  ackval1012  49047  ackval2012  49048  ackval3012  49049  ackval42  49053  2sphere  49106  itscnhlinecirc02plem3  49141  inlinecirc02p  49144  onetansqsecsq  50117  cotsqcscsq  50118