MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2nn0 Structured version   Visualization version   GIF version

Theorem 2nn0 11574
Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
2nn0 2 ∈ ℕ0

Proof of Theorem 2nn0
StepHypRef Expression
1 2nn 11460 . 2 2 ∈ ℕ
21nnnn0i 11565 1 2 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  2c2 11354  0cn0 11557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-1cn 10277
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-ov 6875  df-om 7294  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-nn 11304  df-2 11362  df-n0 11558
This theorem is referenced by:  nn0n0n1ge2  11622  7p6e13  11835  8p3e11  11838  8p5e13  11840  9p3e12  11845  9p4e13  11846  4t3e12  11855  4t4e16  11856  5t3e15  11858  5t5e25  11860  6t3e18  11862  6t5e30  11864  7t3e21  11867  7t4e28  11868  7t5e35  11869  7t6e42  11870  7t7e49  11871  8t3e24  11873  8t4e32  11874  8t5e40  11875  9t3e27  11880  9t4e36  11881  9t8e72  11885  9t9e81  11886  decbin3  11899  2eluzge0  11949  xnn0le2is012  12292  fzo0to42pr  12777  nn0sqcl  13108  sqmul  13147  resqcl  13152  zsqcl  13155  cu2  13184  i3  13187  i4  13188  binom3  13206  expmulnbnd  13217  nn0opthlem1  13273  fac3  13285  faclbnd2  13296  faclbnd4lem1  13298  faclbnd4lem3  13300  hash2pr  13466  hashtplei  13481  s4fv2  13864  repsw3  13917  swrd2lsw  13918  2swrd2eqwrdeq  13919  abssq  14267  sqabs  14268  iseraltlem2  14634  iseraltlem3  14635  bpoly2  15006  bpoly3  15007  bpoly4  15008  fsumcube  15009  ef4p  15061  efgt1p2  15062  efi4p  15085  ef01bndlem  15132  cos01bnd  15134  oexpneg  15287  oddge22np1  15291  bitsinv2  15382  bitsf1ocnv  15383  sadcaddlem  15396  sadadd2lem  15398  pythagtriplem4  15739  iserodd  15755  oddprmdvds  15822  prmreclem2  15836  prmreclem6  15840  vdwlem7  15906  vdwlem10  15909  vdwlem12  15911  dec2dvds  15982  dec5dvds  15983  decexp2  15994  2exp4  16004  2exp6  16005  2exp8  16006  2exp16  16007  3exp3  16008  2expltfac  16009  5prm  16025  7prm  16027  11prm  16031  13prm  16032  17prm  16033  19prm  16034  23prm  16035  prmlem2  16036  37prm  16037  43prm  16038  83prm  16039  139prm  16040  163prm  16041  317prm  16042  631prm  16043  1259lem1  16047  1259lem2  16048  1259lem3  16049  1259lem4  16050  1259lem5  16051  1259prm  16052  2503lem1  16053  2503lem2  16054  2503lem3  16055  2503prm  16056  4001lem1  16057  4001lem2  16058  4001lem3  16059  4001lem4  16060  4001prm  16061  ressds  16276  prdsvalstr  16316  pmtrprfval  18106  psgnunilem2  18114  efgredleme  18355  lt6abl  18495  mgpds  18699  srads  19393  cnfldstr  19954  cnfldfun  19964  setsmsds  22492  tmslem  22498  tnglem  22655  tngds  22663  sqcn  22888  dveflem  23954  iaa  24292  tangtx  24470  efif1olem3  24503  efif1olem4  24504  root1id  24707  mcubic  24786  cubic2  24787  cubic  24788  binom4  24789  dquartlem2  24791  dquart  24792  quart1cl  24793  quart1lem  24794  quart1  24795  quartlem1  24796  quartlem2  24797  atandmcj  24848  bndatandm  24868  atansopn  24871  atantayl3  24878  leibpilem2  24880  leibpi  24881  leibpisum  24882  log2cnv  24883  log2tlbnd  24884  log2ublem2  24886  log2ublem3  24887  log2ub  24888  log2le1  24889  birthday  24893  basellem3  25021  basellem4  25022  basellem5  25023  basellem8  25026  issqf  25074  ppi3  25109  ppiublem2  25140  chtublem  25148  mersenne  25164  bcmax  25215  bcp1ctr  25216  bclbnd  25217  bpos1  25220  bposlem6  25226  bposlem8  25228  lgslem1  25234  lgsqrlem2  25284  gausslemma2dlem6  25309  lgseisenlem4  25315  2lgslem1c  25330  2lgslem3a  25333  2lgslem3b  25334  2lgslem3c  25335  2lgslem3d  25336  chebbnd1lem3  25372  rplogsumlem2  25386  dchrisumlem2  25391  dchrisum0flblem1  25409  dchrisum0flblem2  25410  dchrisum0flb  25411  selberglem2  25447  pntrmax  25465  pntlemo  25508  trkgstr  25555  ttgplusg  25970  ttgds  25973  eengstr  26072  usgrexmplef  26365  upgr2wlk  26790  usgr2pthlem  26885  usgr2pth  26886  wpthswwlks2on  27100  elwspths2spth  27107  upgr3v3e3cycl  27351  upgr4cycl4dv4e  27356  konigsbergiedgw  27419  konigsberglem1  27423  konigsberglem2  27424  konigsberglem3  27425  clwlknon2num  27546  1kp2ke3k  27632  ex-mod  27635  ex-exp  27636  ex-fac  27637  ipidsq  27891  strlem3a  29437  dpmul4  29945  madjusmdetlem4  30219  zlmds  30331  coinflippv  30868  prodfzo03  31004  hgt750lemd  31049  hgt750lem  31052  hgt750lem2  31053  hgt750leme  31059  tgoldbachgnn  31060  tgoldbachgtde  31061  tgoldbachgt  31064  kur14lem8  31516  sinccvglem  31886  dvtan  33770  sqn5i  37744  diophin  37836  irrapxlem5  37890  pellexlem2  37894  pell1qrge1  37934  jm2.22  38061  jm2.20nn  38063  jm2.27c  38073  rmydioph  38080  rmxdioph  38082  expdiophlem2  38088  frlmpwfi  38167  isnumbasgrplem3  38174  amgm2d  38999  dvdivbd  40616  itgsinexplem1  40647  itgsinexp  40648  stoweidlem1  40695  wallispilem4  40762  wallispilem5  40763  wallispi2lem2  40766  stirlinglem3  40770  stirlinglem5  40772  stirlinglem7  40774  stirlinglem8  40775  stirlinglem10  40777  stirlinglem11  40778  hoiqssbllem2  41317  pfx2  41985  fmtnoge3  42015  fmtnom1nn  42017  fmtnof1  42020  fmtnorec1  42022  sqrtpwpw2p  42023  fmtnosqrt  42024  fmtnorec2lem  42027  fmtnodvds  42029  fmtnorec3  42033  fmtnorec4  42034  fmtno2  42035  fmtno3  42036  fmtno5lem2  42039  fmtno5lem4  42041  fmtno5  42042  257prm  42046  odz2prm2pw  42048  fmtnoprmfac1lem  42049  fmtnoprmfac2lem1  42051  fmtnofac2lem  42053  fmtnofac2  42054  fmtnofac1  42055  fmtno4prmfac  42057  fmtno4nprmfac193  42059  fmtno4prm  42060  fmtno5faclem1  42064  fmtno5faclem2  42065  fmtno5faclem3  42066  fmtno5fac  42067  2exp5  42080  flsqrt  42081  139prmALT  42084  31prm  42085  m5prm  42086  2exp7  42087  127prm  42088  m7prm  42089  2exp11  42090  m11nprm  42091  sfprmdvdsmersenne  42093  lighneallem2  42096  lighneallem3  42097  lighneallem4a  42098  proththd  42104  3exp4mod41  42106  41prothprmlem1  42107  oexpnegALTV  42161  evengpoap3  42260  tgblthelfgott  42276  tgoldbachlt  42277  tgoldbach  42278  pgrple2abl  42712  pgrpgt2nabl  42713  ply1mulgsumlem2  42741  logbpw2m1  42927  blenpw2m1  42939  dignn0ehalf  42977  nn0sumshdiglemA  42979  nn0sumshdiglemB  42980  nn0mullong  42985  onetansqsecsq  43071  cotsqcscsq  43072
  Copyright terms: Public domain W3C validator