Theorem 2nn0 12511

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

Syntax hints:   ∈ wcel 2099  2c2 12289  ℕ₀cn0 12494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-1cn 11188

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12235  df-2 12297  df-n0 12495

This theorem is referenced by:  nn0n0n1ge2  12561  7p6e13  12777  8p3e11  12780  8p5e13  12782  9p3e12  12787  9p4e13  12788  4t3e12  12797  4t4e16  12798  5t3e15  12800  5t5e25  12802  6t3e18  12804  6t5e30  12806  7t3e21  12809  7t4e28  12810  7t5e35  12811  7t6e42  12812  7t7e49  12813  8t3e24  12815  8t4e32  12816  8t5e40  12817  9t3e27  12822  9t4e36  12823  9t8e72  12827  9t9e81  12828  decbin3  12841  2eluzge0  12899  xnn0le2is012  13249  fzo0to42pr  13743  nn0sqcl  14078  sqmul  14107  resqcl  14112  zsqcl  14117  cu2  14187  i3  14190  i4  14191  binom3  14210  expmulnbnd  14221  nn0opthlem1  14251  fac3  14263  faclbnd2  14274  faclbnd4lem1  14276  faclbnd4lem3  14278  hash2pr  14454  hashtplei  14469  s4fv2  14872  pfx2  14922  repsw3  14926  swrd2lsw  14927  2swrd2eqwrdeq  14928  abssq  15277  sqabs  15278  iseraltlem2  15653  iseraltlem3  15654  bpoly2  16025  bpoly3  16026  bpoly4  16027  fsumcube  16028  ef4p  16081  efgt1p2  16082  efi4p  16105  ef01bndlem  16152  cos01bnd  16154  oexpneg  16313  oddge22np1  16317  bitsinv2  16409  bitsf1ocnv  16410  sadcaddlem  16423  sadadd2lem  16425  pythagtriplem4  16779  iserodd  16795  oddprmdvds  16863  prmreclem2  16877  prmreclem6  16881  vdwlem7  16947  vdwlem10  16950  vdwlem12  16952  dec2dvds  17023  dec5dvds  17024  decexp2  17035  2exp4  17045  2exp5  17046  2exp6  17047  2exp7  17048  2exp8  17049  2exp11  17050  2exp16  17051  3exp3  17052  2expltfac  17053  5prm  17069  7prm  17071  11prm  17075  13prm  17076  17prm  17077  19prm  17078  23prm  17079  prmlem2  17080  37prm  17081  43prm  17082  83prm  17083  139prm  17084  163prm  17085  317prm  17086  631prm  17087  1259lem1  17091  1259lem2  17092  1259lem3  17093  1259lem4  17094  1259lem5  17095  1259prm  17096  2503lem1  17097  2503lem2  17098  2503lem3  17099  2503prm  17100  4001lem1  17101  4001lem2  17102  4001lem3  17103  4001lem4  17104  4001prm  17105  basendxltdsndx  17360  dsndxnplusgndx  17362  dsndxnmulrndx  17363  slotsdnscsi  17364  dsndxntsetndx  17365  slotsdifdsndx  17366  slotsdifunifndx  17373  prdsvalstr  17425  smndex2dbas  18857  smndex2dlinvh  18860  pmtrprfval  19433  psgnunilem2  19441  efgredleme  19689  lt6abl  19841  mgpdsOLD  20079  sradsOLD  21067  cnfldstr  21268  cnfldstrOLD  21283  cnfldfunALTOLDOLD  21295  setsmsdsOLD  24371  tmslemOLD  24378  tnglemOLD  24537  tngdsOLD  24552  sqcn  24781  ehl2eudis  25337  dveflem  25898  iaa  26247  tangtx  26427  efif1olem3  26465  efif1olem4  26466  root1id  26676  2logb9irr  26714  mcubic  26766  cubic2  26767  cubic  26768  binom4  26769  dquartlem2  26771  dquart  26772  quart1cl  26773  quart1lem  26774  quart1  26775  quartlem1  26776  quartlem2  26777  atandmcj  26828  bndatandm  26848  atansopn  26851  atantayl3  26858  leibpilem2  26860  leibpi  26861  leibpisum  26862  log2cnv  26863  log2tlbnd  26864  log2ublem2  26866  log2ublem3  26867  log2ub  26868  log2le1  26869  birthday  26873  basellem3  27002  basellem4  27003  basellem5  27004  basellem8  27007  issqf  27055  ppi3  27090  ppiublem2  27123  chtublem  27131  mersenne  27147  bcmax  27198  bcp1ctr  27199  bclbnd  27200  bpos1  27203  bposlem6  27209  bposlem8  27211  lgslem1  27217  lgsqrlem2  27267  gausslemma2dlem6  27292  lgseisenlem4  27298  2lgslem1c  27313  2lgslem3a  27316  2lgslem3b  27317  2lgslem3c  27318  2lgslem3d  27319  2sq2  27353  2sqreultlem  27367  2sqreunnltlem  27370  chebbnd1lem3  27391  rplogsumlem2  27405  dchrisumlem2  27410  dchrisum0flblem1  27428  dchrisum0flblem2  27429  dchrisum0flb  27430  selberglem2  27466  pntrmax  27484  pntlemo  27527  slotsinbpsd  28232  slotslnbpsd  28233  trkgstr  28235  ttgplusgOLD  28673  ttgdsOLD  28678  eengstr  28778  usgrexmplef  29059  upgr2wlk  29469  usgr2pthlem  29564  usgr2pth  29565  wpthswwlks2on  29759  elwspths2spth  29765  upgr3v3e3cycl  29977  upgr4cycl4dv4e  29982  konigsbergiedgw  30045  konigsberglem1  30049  konigsberglem2  30050  konigsberglem3  30051  clwlknon2num  30165  1kp2ke3k  30243  ex-mod  30246  ex-exp  30247  ex-fac  30248  9p10ne21  30267  ipidsq  30507  strlem3a  32049  xnn01gt  32524  dpmul4  32619  pfxlsw2ccat  32655  wrdt2ind  32656  eufndx  32927  eufid  32928  madjusmdetlem4  33367  zlmdsOLD  33500  coinflippv  34039  prodfzo03  34171  hgt750lemd  34216  hgt750lem  34219  hgt750lem2  34220  hgt750leme  34226  tgoldbachgnn  34227  tgoldbachgtde  34228  tgoldbachgt  34231  cusgredgex  34667  kur14lem8  34759  sinccvglem  35212  dvtan  37078  420gcd8e4  41414  12lcm5e60  41416  60lcm7e420  41418  lcmineqlem17  41453  lcmineqlem18  41454  lcmineqlem20  41456  lcmineqlem21  41457  lcmineqlem22  41458  lcmineqlem  41460  3exp7  41461  3lexlogpow5ineq1  41462  3lexlogpow5ineq2  41463  3lexlogpow2ineq1  41466  3lexlogpow2ineq2  41467  3lexlogpow5ineq5  41468  aks4d1p1p2  41478  aks4d1p1p7  41482  aks4d1p1p5  41483  aks4d1p1  41484  2np3bcnp1  41548  2ap1caineq  41549  fac2xp3  41611  sqn5i  41781  235t711  41789  ex-decpmul  41790  nicomachus  41794  dffltz  41980  flt4lem  41991  flt4lem3  41994  flt4lem7  42005  nna4b4nsq  42006  sum9cubes  42018  3cubeslem2  42027  3cubeslem3l  42028  3cubeslem3r  42029  diophin  42114  irrapxlem5  42168  pellexlem2  42172  pell1qrge1  42212  jm2.22  42338  jm2.20nn  42340  jm2.27c  42350  rmydioph  42357  rmxdioph  42359  expdiophlem2  42365  frlmpwfi  42444  isnumbasgrplem3  42451  resqrtvalex  42998  imsqrtvalex  42999  amgm2d  43551  dvdivbd  45234  itgsinexplem1  45265  itgsinexp  45266  stoweidlem1  45312  wallispilem4  45379  wallispilem5  45380  wallispi2lem2  45383  stirlinglem3  45387  stirlinglem5  45389  stirlinglem7  45391  stirlinglem8  45392  stirlinglem10  45394  stirlinglem11  45395  hoiqssbllem2  45934  fmtnoge3  46793  fmtnom1nn  46795  fmtnof1  46798  fmtnorec1  46800  sqrtpwpw2p  46801  fmtnosqrt  46802  fmtnorec2lem  46805  fmtnodvds  46807  fmtnorec3  46811  fmtnorec4  46812  fmtno2  46813  fmtno3  46814  fmtno5lem2  46817  fmtno5lem4  46819  fmtno5  46820  257prm  46824  odz2prm2pw  46826  fmtnoprmfac1lem  46827  fmtnoprmfac2lem1  46829  fmtnofac2lem  46831  fmtnofac2  46832  fmtnofac1  46833  fmtno4prmfac  46835  fmtno4nprmfac193  46837  fmtno4prm  46838  fmtno5faclem1  46842  fmtno5faclem2  46843  fmtno5faclem3  46844  fmtno5fac  46845  flsqrt  46856  139prmALT  46859  31prm  46860  m5prm  46861  127prm  46862  m7prm  46863  m11nprm  46864  sfprmdvdsmersenne  46866  lighneallem2  46869  lighneallem3  46870  lighneallem4a  46871  proththd  46877  3exp4mod41  46879  41prothprmlem1  46880  oexpnegALTV  46940  fppr2odd  46994  2exp340mod341  46996  341fppr2  46997  8exp8mod9  46999  nfermltl2rev  47006  evengpoap3  47062  tgblthelfgott  47078  tgoldbachlt  47079  tgoldbach  47080  pgrple2abl  47352  pgrpgt2nabl  47353  ply1mulgsumlem2  47378  logbpw2m1  47563  blenpw2m1  47575  dignn0ehalf  47613  nn0sumshdiglemA  47615  nn0sumshdiglemB  47616  nn0mullong  47621  2aryfvalel  47643  itcoval2  47660  itcoval3  47661  itcovalt2lem2lem2  47670  itcovalt2lem1  47671  ackval2  47678  ackval3  47679  ackval0012  47685  ackval1012  47686  ackval2012  47687  ackval3012  47688  ackval42  47692  2sphere  47745  itscnhlinecirc02plem3  47780  inlinecirc02p  47783  onetansqsecsq  48115  cotsqcscsq  48116