Theorem 2nn0 12459

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

Syntax hints:   ∈ wcel 2109  2c2 12241  ℕ₀cn0 12442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-2 12249  df-n0 12443

This theorem is referenced by:  nn0n0n1ge2  12510  7p6e13  12727  8p3e11  12730  8p5e13  12732  9p3e12  12737  9p4e13  12738  4t3e12  12747  4t4e16  12748  5t3e15  12750  5t5e25  12752  6t3e18  12754  6t5e30  12756  7t3e21  12759  7t4e28  12760  7t5e35  12761  7t6e42  12762  7t7e49  12763  8t3e24  12765  8t4e32  12766  8t5e40  12767  9t3e27  12772  9t4e36  12773  9t8e72  12777  9t9e81  12778  decbin3  12791  2eluzge0  12840  xnn0le2is012  13206  fzo0to42pr  13714  fvf1tp  13751  nn0sqcl  14054  sqmul  14084  resqcl  14089  zsqcl  14094  cu2  14165  i3  14168  i4  14169  binom3  14189  expmulnbnd  14200  nn0opthlem1  14233  fac3  14245  faclbnd2  14256  faclbnd4lem1  14258  faclbnd4lem3  14260  hash2pr  14434  hashtplei  14449  tpf1ofv2  14463  tpfo  14465  s4fv2  14863  pfx2  14913  repsw3  14917  swrd2lsw  14918  2swrd2eqwrdeq  14919  abssq  15272  sqabs  15273  iseraltlem2  15649  iseraltlem3  15650  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  ef4p  16081  efgt1p2  16082  efi4p  16105  ef01bndlem  16152  cos01bnd  16154  oexpneg  16315  oddge22np1  16319  bitsinv2  16413  bitsf1ocnv  16414  sadcaddlem  16427  sadadd2lem  16429  pythagtriplem4  16790  iserodd  16806  oddprmdvds  16874  prmreclem2  16888  prmreclem6  16892  vdwlem7  16958  vdwlem10  16961  vdwlem12  16963  dec2dvds  17034  dec5dvds  17035  2exp4  17055  2exp5  17056  2exp6  17057  2exp7  17058  2exp8  17059  2exp11  17060  2exp16  17061  3exp3  17062  2expltfac  17063  5prm  17079  7prm  17081  11prm  17085  13prm  17086  17prm  17087  19prm  17088  23prm  17089  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  basendxltdsndx  17351  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  slotsdifunifndx  17364  prdsvalstr  17415  smndex2dbas  18841  smndex2dlinvh  18844  pmtrprfval  19417  psgnunilem2  19425  efgredleme  19673  lt6abl  19825  cnfldstr  21266  cnfldstrOLD  21281  sqcn  24767  ehl2eudis  25322  dveflem  25883  iaa  26233  tangtx  26414  efif1olem3  26453  efif1olem4  26454  root1id  26664  2logb9irr  26705  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  atandmcj  26819  bndatandm  26839  atansopn  26842  atantayl3  26849  leibpilem2  26851  leibpi  26852  leibpisum  26853  log2cnv  26854  log2tlbnd  26855  log2ublem2  26857  log2ublem3  26858  log2ub  26859  log2le1  26860  birthday  26864  basellem3  26993  basellem4  26994  basellem5  26995  basellem8  26998  issqf  27046  ppi3  27081  ppiublem2  27114  chtublem  27122  mersenne  27138  bcmax  27189  bcp1ctr  27190  bclbnd  27191  bpos1  27194  bposlem6  27200  bposlem8  27202  lgslem1  27208  lgsqrlem2  27258  gausslemma2dlem6  27283  lgseisenlem4  27289  2lgslem1c  27304  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2sq2  27344  2sqreultlem  27358  2sqreunnltlem  27361  chebbnd1lem3  27382  rplogsumlem2  27396  dchrisumlem2  27401  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0flb  27421  selberglem2  27457  pntrmax  27475  pntlemo  27518  slotsinbpsd  28368  slotslnbpsd  28369  trkgstr  28371  eengstr  28907  usgrexmplef  29186  upgr2wlk  29596  usgr2pthlem  29693  usgr2pth  29694  wpthswwlks2on  29891  elwspths2spth  29897  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  clwlknon2num  30297  1kp2ke3k  30375  ex-mod  30378  ex-exp  30379  ex-fac  30380  9p10ne21  30399  ipidsq  30639  strlem3a  32181  xnn01gt  32693  expevenpos  32771  dpmul4  32834  pfxlsw2ccat  32872  wrdt2ind  32875  eufndx  33240  eufid  33241  evl1deg2  33546  evl1deg3  33547  fldext2rspun  33677  rtelextdg2lem  33716  rtelextdg2  33717  constrelextdg2  33737  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpinconstrlem1  33779  madjusmdetlem4  33820  coinflippv  34475  prodfzo03  34594  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  tgoldbachgnn  34650  tgoldbachgtde  34651  tgoldbachgt  34654  cusgredgex  35109  kur14lem8  35200  sinccvglem  35659  dvtan  37664  420gcd8e4  41994  12lcm5e60  41996  60lcm7e420  41998  lcmineqlem17  42033  lcmineqlem18  42034  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  lcmineqlem  42040  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p2  42058  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c7lem1  42168  sqn5i  42273  235t711  42293  ex-decpmul  42294  nicomachus  42300  dffltz  42622  flt4lem  42633  flt4lem3  42636  flt4lem7  42647  nna4b4nsq  42648  sum9cubes  42660  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  diophin  42760  irrapxlem5  42814  pellexlem2  42818  pell1qrge1  42858  jm2.22  42984  jm2.20nn  42986  jm2.27c  42996  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  frlmpwfi  43087  isnumbasgrplem3  43094  resqrtvalex  43634  imsqrtvalex  43635  amgm2d  44187  dvdivbd  45921  itgsinexplem1  45952  itgsinexp  45953  stoweidlem1  45999  wallispilem4  46066  wallispilem5  46067  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem5  46076  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  hoiqssbllem2  46621  fmtnoge3  47531  fmtnom1nn  47533  fmtnof1  47536  fmtnorec1  47538  sqrtpwpw2p  47539  fmtnosqrt  47540  fmtnorec2lem  47543  fmtnodvds  47545  fmtnorec3  47549  fmtnorec4  47550  fmtno2  47551  fmtno3  47552  fmtno5lem2  47555  fmtno5lem4  47557  fmtno5  47558  257prm  47562  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac2lem1  47567  fmtnofac2lem  47569  fmtnofac2  47570  fmtnofac1  47571  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno4prm  47576  fmtno5faclem1  47580  fmtno5faclem2  47581  fmtno5faclem3  47582  fmtno5fac  47583  flsqrt  47594  139prmALT  47597  31prm  47598  m5prm  47599  127prm  47600  m7prm  47601  m11nprm  47602  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem3  47608  lighneallem4a  47609  proththd  47615  3exp4mod41  47617  41prothprmlem1  47618  oexpnegALTV  47678  fppr2odd  47732  2exp340mod341  47734  341fppr2  47735  8exp8mod9  47737  nfermltl2rev  47744  evengpoap3  47800  tgblthelfgott  47816  tgoldbachlt  47817  tgoldbach  47818  cycl3grtri  47946  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpg3nbgrvtx0  48067  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  pgrple2abl  48353  pgrpgt2nabl  48354  ply1mulgsumlem2  48376  logbpw2m1  48556  blenpw2m1  48568  dignn0ehalf  48606  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0mullong  48614  2aryfvalel  48636  itcoval2  48653  itcoval3  48654  itcovalt2lem2lem2  48663  itcovalt2lem1  48664  ackval2  48671  ackval3  48672  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval42  48685  2sphere  48738  itscnhlinecirc02plem3  48773  inlinecirc02p  48776  onetansqsecsq  49750  cotsqcscsq  49751