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

Theorem 2nn0 11347
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 11223 . 2 2 ∈ ℕ
21nnnn0i 11338 1 2 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  2c2 11108  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-1cn 10032
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059  df-2 11117  df-n0 11331
This theorem is referenced by:  nn0n0n1ge2  11396  7p6e13  11646  8p3e11  11650  8p3e11OLD  11651  8p5e13  11653  9p3e12  11659  9p4e13  11660  4t3e12  11670  4t4e16  11671  5t3e15  11673  5t3e15OLD  11674  5t5e25  11677  5t5e25OLD  11678  6t3e18  11680  6t5e30  11682  6t5e30OLD  11683  7t3e21  11687  7t4e28  11688  7t5e35  11689  7t6e42  11690  7t7e49  11691  8t3e24  11693  8t4e32  11694  8t5e40  11695  8t5e40OLD  11696  9t3e27  11702  9t4e36  11703  9t8e72  11707  9t9e81  11708  decbin3  11722  2eluzge0  11771  xnn0le2is012  12114  fzo0to42pr  12595  nn0sqcl  12927  sqmul  12966  resqcl  12971  zsqcl  12974  cu2  13003  i3  13006  i4  13007  binom3  13025  expmulnbnd  13036  nn0opthlem1  13095  fac3  13107  faclbnd2  13118  faclbnd4lem1  13120  faclbnd4lem3  13122  hash2pr  13289  hashtplei  13304  s4fv2  13688  repsw3  13740  swrd2lsw  13741  2swrd2eqwrdeq  13742  abssq  14090  sqabs  14091  iseraltlem2  14457  iseraltlem3  14458  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  ef4p  14887  efgt1p2  14888  efi4p  14911  ef01bndlem  14958  cos01bnd  14960  oexpneg  15116  oddge22np1  15120  bitsinv2  15212  bitsf1ocnv  15213  sadcaddlem  15226  sadadd2lem  15228  pythagtriplem4  15571  iserodd  15587  oddprmdvds  15654  prmreclem2  15668  prmreclem6  15672  vdwlem7  15738  vdwlem10  15741  vdwlem12  15743  dec2dvds  15814  dec5dvds  15815  decexp2  15826  2exp4  15841  2exp6  15842  2exp8  15843  2exp16  15844  3exp3  15845  2expltfac  15846  5prm  15862  7prm  15864  11prm  15869  13prm  15870  17prm  15871  19prm  15872  23prm  15873  prmlem2  15874  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  ressds  16120  prdsvalstr  16160  pmtrprfval  17953  psgnunilem2  17961  efgredleme  18202  lt6abl  18342  mgpds  18545  srads  19234  cnfldstr  19796  cnfldfun  19806  setsmsds  22328  tmslem  22334  tnglem  22491  tngds  22499  sqcn  22724  dveflem  23787  iaa  24125  tangtx  24302  efif1olem3  24335  efif1olem4  24336  root1id  24540  mcubic  24619  cubic2  24620  cubic  24621  binom4  24622  dquartlem2  24624  dquart  24625  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem2  24630  atandmcj  24681  bndatandm  24701  atansopn  24704  atantayl3  24711  leibpilem2  24713  leibpi  24714  leibpisum  24715  log2cnv  24716  log2tlbnd  24717  log2ublem2  24719  log2ublem3  24720  log2ub  24721  log2le1  24722  birthday  24726  basellem3  24854  basellem4  24855  basellem5  24856  basellem8  24859  issqf  24907  ppi3  24942  ppiublem2  24973  chtublem  24981  mersenne  24997  bcmax  25048  bcp1ctr  25049  bclbnd  25050  bpos1  25053  bposlem6  25059  bposlem8  25061  lgslem1  25067  lgsqrlem2  25117  gausslemma2dlem6  25142  lgseisenlem4  25148  2lgslem1c  25163  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  chebbnd1lem3  25205  rplogsumlem2  25219  dchrisumlem2  25224  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0flb  25244  selberglem2  25280  pntrmax  25298  pntlemo  25341  trkgstr  25388  ttgplusg  25803  ttgds  25806  eengstr  25905  usgrexmplef  26196  upgr2wlk  26620  usgr2pthlem  26715  usgr2pth  26716  wpthswwlks2on  26927  elwspths2spth  26934  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  1kp2ke3k  27433  ex-mod  27436  ex-exp  27437  ex-fac  27438  ipidsq  27693  strlem3a  29239  dpmul4  29750  madjusmdetlem4  30024  zlmds  30136  coinflippv  30673  prodfzo03  30809  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  tgoldbachgnn  30865  tgoldbachgtde  30866  tgoldbachgt  30869  kur14lem8  31321  sinccvglem  31692  dvtan  33590  diophin  37653  irrapxlem5  37707  pellexlem2  37711  pell1qrge1  37751  jm2.22  37879  jm2.20nn  37881  jm2.27c  37891  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  frlmpwfi  37985  isnumbasgrplem3  37992  amgm2d  38818  dvdivbd  40456  itgsinexplem1  40487  itgsinexp  40488  stoweidlem1  40536  wallispilem4  40603  wallispilem5  40604  wallispi2lem2  40607  stirlinglem3  40611  stirlinglem5  40613  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  hoiqssbllem2  41158  pfx2  41737  fmtnoge3  41767  fmtnom1nn  41769  fmtnof1  41772  fmtnorec1  41774  sqrtpwpw2p  41775  fmtnosqrt  41776  fmtnorec2lem  41779  fmtnodvds  41781  fmtnorec3  41785  fmtnorec4  41786  fmtno2  41787  fmtno3  41788  fmtno5lem2  41791  fmtno5lem4  41793  fmtno5  41794  257prm  41798  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnoprmfac2lem1  41803  fmtnofac2lem  41805  fmtnofac2  41806  fmtnofac1  41807  fmtno4prmfac  41809  fmtno4nprmfac193  41811  fmtno4prm  41812  fmtno5faclem1  41816  fmtno5faclem2  41817  fmtno5faclem3  41818  fmtno5fac  41819  2exp5  41832  flsqrt  41833  139prmALT  41836  31prm  41837  m5prm  41838  2exp7  41839  127prm  41840  m7prm  41841  2exp11  41842  m11nprm  41843  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem3  41849  lighneallem4a  41850  proththd  41856  3exp4mod41  41858  41prothprmlem1  41859  oexpnegALTV  41913  evengpoap3  42012  tgblthelfgott  42028  tgoldbachlt  42029  tgoldbach  42030  tgblthelfgottOLD  42034  tgoldbachltOLD  42035  tgoldbachOLD  42037  pgrple2abl  42471  pgrpgt2nabl  42472  ply1mulgsumlem2  42500  logbpw2m1  42686  blenpw2m1  42698  dignn0ehalf  42736  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0mullong  42744  onetansqsecsq  42830  cotsqcscsq  42831
  Copyright terms: Public domain W3C validator