Theorem 2nn0 12489

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

Syntax hints:   ∈ wcel 2107  2c2 12267  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213  df-2 12275  df-n0 12473

This theorem is referenced by:  nn0n0n1ge2  12539  7p6e13  12755  8p3e11  12758  8p5e13  12760  9p3e12  12765  9p4e13  12766  4t3e12  12775  4t4e16  12776  5t3e15  12778  5t5e25  12780  6t3e18  12782  6t5e30  12784  7t3e21  12787  7t4e28  12788  7t5e35  12789  7t6e42  12790  7t7e49  12791  8t3e24  12793  8t4e32  12794  8t5e40  12795  9t3e27  12800  9t4e36  12801  9t8e72  12805  9t9e81  12806  decbin3  12819  2eluzge0  12877  xnn0le2is012  13225  fzo0to42pr  13719  nn0sqcl  14055  sqmul  14084  resqcl  14089  zsqcl  14094  cu2  14164  i3  14167  i4  14168  binom3  14187  expmulnbnd  14198  nn0opthlem1  14228  fac3  14240  faclbnd2  14251  faclbnd4lem1  14253  faclbnd4lem3  14255  hash2pr  14430  hashtplei  14445  s4fv2  14848  pfx2  14898  repsw3  14902  swrd2lsw  14903  2swrd2eqwrdeq  14904  abssq  15253  sqabs  15254  iseraltlem2  15629  iseraltlem3  15630  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  ef4p  16056  efgt1p2  16057  efi4p  16080  ef01bndlem  16127  cos01bnd  16129  oexpneg  16288  oddge22np1  16292  bitsinv2  16384  bitsf1ocnv  16385  sadcaddlem  16398  sadadd2lem  16400  pythagtriplem4  16752  iserodd  16768  oddprmdvds  16836  prmreclem2  16850  prmreclem6  16854  vdwlem7  16920  vdwlem10  16923  vdwlem12  16925  dec2dvds  16996  dec5dvds  16997  decexp2  17008  2exp4  17018  2exp5  17019  2exp6  17020  2exp7  17021  2exp8  17022  2exp11  17023  2exp16  17024  3exp3  17025  2expltfac  17026  5prm  17042  7prm  17044  11prm  17048  13prm  17049  17prm  17050  19prm  17051  23prm  17052  prmlem2  17053  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  basendxltdsndx  17333  dsndxnplusgndx  17335  dsndxnmulrndx  17336  slotsdnscsi  17337  dsndxntsetndx  17338  slotsdifdsndx  17339  slotsdifunifndx  17346  prdsvalstr  17398  smndex2dbas  18795  smndex2dlinvh  18798  pmtrprfval  19355  psgnunilem2  19363  efgredleme  19611  lt6abl  19763  mgpdsOLD  20001  sradsOLD  20807  cnfldstr  20946  cnfldfunALTOLD  20958  setsmsdsOLD  23984  tmslemOLD  23991  tnglemOLD  24150  tngdsOLD  24165  sqcn  24390  ehl2eudis  24939  dveflem  25496  iaa  25838  tangtx  26015  efif1olem3  26053  efif1olem4  26054  root1id  26262  2logb9irr  26300  mcubic  26352  cubic2  26353  cubic  26354  binom4  26355  dquartlem2  26357  dquart  26358  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem2  26363  atandmcj  26414  bndatandm  26434  atansopn  26437  atantayl3  26444  leibpilem2  26446  leibpi  26447  leibpisum  26448  log2cnv  26449  log2tlbnd  26450  log2ublem2  26452  log2ublem3  26453  log2ub  26454  log2le1  26455  birthday  26459  basellem3  26587  basellem4  26588  basellem5  26589  basellem8  26592  issqf  26640  ppi3  26675  ppiublem2  26706  chtublem  26714  mersenne  26730  bcmax  26781  bcp1ctr  26782  bclbnd  26783  bpos1  26786  bposlem6  26792  bposlem8  26794  lgslem1  26800  lgsqrlem2  26850  gausslemma2dlem6  26875  lgseisenlem4  26881  2lgslem1c  26896  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2sq2  26936  2sqreultlem  26950  2sqreunnltlem  26953  chebbnd1lem3  26974  rplogsumlem2  26988  dchrisumlem2  26993  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0flb  27013  selberglem2  27049  pntrmax  27067  pntlemo  27110  slotsinbpsd  27692  slotslnbpsd  27693  trkgstr  27695  ttgplusgOLD  28133  ttgdsOLD  28138  eengstr  28238  usgrexmplef  28516  upgr2wlk  28925  usgr2pthlem  29020  usgr2pth  29021  wpthswwlks2on  29215  elwspths2spth  29221  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  konigsbergiedgw  29501  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  clwlknon2num  29621  1kp2ke3k  29699  ex-mod  29702  ex-exp  29703  ex-fac  29704  9p10ne21  29723  ipidsq  29963  strlem3a  31505  xnn01gt  31983  dpmul4  32080  pfxlsw2ccat  32116  wrdt2ind  32117  eufndx  32390  eufid  32391  madjusmdetlem4  32810  zlmdsOLD  32943  coinflippv  33482  prodfzo03  33615  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  tgoldbachgnn  33671  tgoldbachgtde  33672  tgoldbachgt  33675  cusgredgex  34112  kur14lem8  34204  sinccvglem  34657  dvtan  36538  420gcd8e4  40871  12lcm5e60  40873  60lcm7e420  40875  lcmineqlem17  40910  lcmineqlem18  40911  lcmineqlem20  40913  lcmineqlem21  40914  lcmineqlem22  40915  lcmineqlem  40917  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow5ineq2  40920  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1p2  40935  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  2np3bcnp1  40960  2ap1caineq  40961  fac2xp3  41020  sqn5i  41197  235t711  41205  ex-decpmul  41206  nicomachus  41210  dffltz  41376  flt4lem  41387  flt4lem3  41390  flt4lem7  41401  nna4b4nsq  41402  sum9cubes  41414  3cubeslem2  41423  3cubeslem3l  41424  3cubeslem3r  41425  diophin  41510  irrapxlem5  41564  pellexlem2  41568  pell1qrge1  41608  jm2.22  41734  jm2.20nn  41736  jm2.27c  41746  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  frlmpwfi  41840  isnumbasgrplem3  41847  resqrtvalex  42396  imsqrtvalex  42397  amgm2d  42950  dvdivbd  44639  itgsinexplem1  44670  itgsinexp  44671  stoweidlem1  44717  wallispilem4  44784  wallispilem5  44785  wallispi2lem2  44788  stirlinglem3  44792  stirlinglem5  44794  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  hoiqssbllem2  45339  fmtnoge3  46198  fmtnom1nn  46200  fmtnof1  46203  fmtnorec1  46205  sqrtpwpw2p  46206  fmtnosqrt  46207  fmtnorec2lem  46210  fmtnodvds  46212  fmtnorec3  46216  fmtnorec4  46217  fmtno2  46218  fmtno3  46219  fmtno5lem2  46222  fmtno5lem4  46224  fmtno5  46225  257prm  46229  odz2prm2pw  46231  fmtnoprmfac1lem  46232  fmtnoprmfac2lem1  46234  fmtnofac2lem  46236  fmtnofac2  46237  fmtnofac1  46238  fmtno4prmfac  46240  fmtno4nprmfac193  46242  fmtno4prm  46243  fmtno5faclem1  46247  fmtno5faclem2  46248  fmtno5faclem3  46249  fmtno5fac  46250  flsqrt  46261  139prmALT  46264  31prm  46265  m5prm  46266  127prm  46267  m7prm  46268  m11nprm  46269  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem3  46275  lighneallem4a  46276  proththd  46282  3exp4mod41  46284  41prothprmlem1  46285  oexpnegALTV  46345  fppr2odd  46399  2exp340mod341  46401  341fppr2  46402  8exp8mod9  46404  nfermltl2rev  46411  evengpoap3  46467  tgblthelfgott  46483  tgoldbachlt  46484  tgoldbach  46485  pgrple2abl  47041  pgrpgt2nabl  47042  ply1mulgsumlem2  47068  logbpw2m1  47253  blenpw2m1  47265  dignn0ehalf  47303  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0mullong  47311  2aryfvalel  47333  itcoval2  47350  itcoval3  47351  itcovalt2lem2lem2  47360  itcovalt2lem1  47361  ackval2  47368  ackval3  47369  ackval0012  47375  ackval1012  47376  ackval2012  47377  ackval3012  47378  ackval42  47382  2sphere  47435  itscnhlinecirc02plem3  47470  inlinecirc02p  47473  onetansqsecsq  47806  cotsqcscsq  47807