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

Theorem 2nn0 11909
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 11705 . 2 2 ∈ ℕ
21nnnn0i 11900 1 2 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  2c2 11687  0cn0 11892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-1cn 10589
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-ov 7149  df-om 7572  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-nn 11633  df-2 11695  df-n0 11893
This theorem is referenced by:  nn0n0n1ge2  11957  7p6e13  12171  8p3e11  12174  8p5e13  12176  9p3e12  12181  9p4e13  12182  4t3e12  12191  4t4e16  12192  5t3e15  12194  5t5e25  12196  6t3e18  12198  6t5e30  12200  7t3e21  12203  7t4e28  12204  7t5e35  12205  7t6e42  12206  7t7e49  12207  8t3e24  12209  8t4e32  12210  8t5e40  12211  9t3e27  12216  9t4e36  12217  9t8e72  12221  9t9e81  12222  decbin3  12235  2eluzge0  12288  xnn0le2is012  12634  fzo0to42pr  13126  nn0sqcl  13459  sqmul  13488  resqcl  13493  zsqcl  13497  cu2  13566  i3  13569  i4  13570  binom3  13588  expmulnbnd  13599  nn0opthlem1  13631  fac3  13643  faclbnd2  13654  faclbnd4lem1  13656  faclbnd4lem3  13658  hash2pr  13830  hashtplei  13845  s4fv2  14257  pfx2  14307  repsw3  14311  swrd2lsw  14312  2swrd2eqwrdeq  14313  abssq  14664  sqabs  14665  iseraltlem2  15037  iseraltlem3  15038  bpoly2  15409  bpoly3  15410  bpoly4  15411  fsumcube  15412  ef4p  15464  efgt1p2  15465  efi4p  15488  ef01bndlem  15535  cos01bnd  15537  oexpneg  15692  oddge22np1  15696  bitsinv2  15788  bitsf1ocnv  15789  sadcaddlem  15802  sadadd2lem  15804  pythagtriplem4  16152  iserodd  16168  oddprmdvds  16235  prmreclem2  16249  prmreclem6  16253  vdwlem7  16319  vdwlem10  16322  vdwlem12  16324  dec2dvds  16395  dec5dvds  16396  decexp2  16407  2exp4  16417  2exp5  16418  2exp6  16419  2exp7  16420  2exp8  16421  2exp16  16422  3exp3  16423  2expltfac  16424  5prm  16440  7prm  16442  11prm  16446  13prm  16447  17prm  16448  19prm  16449  23prm  16450  prmlem2  16451  37prm  16452  43prm  16453  83prm  16454  139prm  16455  163prm  16456  317prm  16457  631prm  16458  1259lem1  16462  1259lem2  16463  1259lem3  16464  1259lem4  16465  1259lem5  16466  1259prm  16467  2503lem1  16468  2503lem2  16469  2503lem3  16470  2503prm  16471  4001lem1  16472  4001lem2  16473  4001lem3  16474  4001lem4  16475  4001prm  16476  ressds  16684  prdsvalstr  16724  smndex2dbas  18077  smndex2dlinvh  18080  pmtrprfval  18613  psgnunilem2  18621  efgredleme  18867  lt6abl  19013  mgpds  19247  srads  19953  cnfldstr  20542  cnfldfun  20552  setsmsds  23081  tmslem  23087  tnglem  23244  tngds  23252  sqcn  23477  ehl2eudis  24024  dveflem  24580  iaa  24919  tangtx  25096  efif1olem3  25134  efif1olem4  25135  root1id  25341  2logb9irr  25379  mcubic  25431  cubic2  25432  cubic  25433  binom4  25434  dquartlem2  25436  dquart  25437  quart1cl  25438  quart1lem  25439  quart1  25440  quartlem1  25441  quartlem2  25442  atandmcj  25493  bndatandm  25513  atansopn  25516  atantayl3  25523  leibpilem2  25525  leibpi  25526  leibpisum  25527  log2cnv  25528  log2tlbnd  25529  log2ublem2  25531  log2ublem3  25532  log2ub  25533  log2le1  25534  birthday  25538  basellem3  25666  basellem4  25667  basellem5  25668  basellem8  25671  issqf  25719  ppi3  25754  ppiublem2  25785  chtublem  25793  mersenne  25809  bcmax  25860  bcp1ctr  25861  bclbnd  25862  bpos1  25865  bposlem6  25871  bposlem8  25873  lgslem1  25879  lgsqrlem2  25929  gausslemma2dlem6  25954  lgseisenlem4  25960  2lgslem1c  25975  2lgslem3a  25978  2lgslem3b  25979  2lgslem3c  25980  2lgslem3d  25981  2sq2  26015  2sqreultlem  26029  2sqreunnltlem  26032  chebbnd1lem3  26053  rplogsumlem2  26067  dchrisumlem2  26072  dchrisum0flblem1  26090  dchrisum0flblem2  26091  dchrisum0flb  26092  selberglem2  26128  pntrmax  26146  pntlemo  26189  trkgstr  26236  ttgplusg  26670  ttgds  26673  eengstr  26772  usgrexmplef  27047  upgr2wlk  27456  usgr2pthlem  27550  usgr2pth  27551  wpthswwlks2on  27745  elwspths2spth  27751  upgr3v3e3cycl  27963  upgr4cycl4dv4e  27968  konigsbergiedgw  28031  konigsberglem1  28035  konigsberglem2  28036  konigsberglem3  28037  clwlknon2num  28151  1kp2ke3k  28229  ex-mod  28232  ex-exp  28233  ex-fac  28234  9p10ne21  28253  ipidsq  28491  strlem3a  30033  xnn01gt  30501  dpmul4  30596  pfxlsw2ccat  30632  wrdt2ind  30633  madjusmdetlem4  31125  zlmds  31232  coinflippv  31768  prodfzo03  31901  hgt750lemd  31946  hgt750lem  31949  hgt750lem2  31950  hgt750leme  31956  tgoldbachgnn  31957  tgoldbachgtde  31958  tgoldbachgt  31961  cusgredgex  32395  kur14lem8  32487  sinccvglem  32942  dvtan  35019  420gcd8e4  39202  12lcm5e60  39204  60lcm7e420  39206  lcmineqlem17  39241  lcmineqlem18  39242  lcmineqlem20  39244  lcmineqlem21  39245  lcmineqlem22  39246  lcmineqlem  39248  3lexlogpow5ineq1  39249  fac2xp3  39267  sqn5i  39353  235t711  39359  ex-decpmul  39360  dffltz  39471  3cubeslem2  39482  3cubeslem3l  39483  3cubeslem3r  39484  diophin  39569  irrapxlem5  39623  pellexlem2  39627  pell1qrge1  39667  jm2.22  39792  jm2.20nn  39794  jm2.27c  39804  rmydioph  39811  rmxdioph  39813  expdiophlem2  39819  frlmpwfi  39898  isnumbasgrplem3  39905  resqrtvalex  40201  imsqrtvalex  40202  amgm2d  40763  dvdivbd  42431  itgsinexplem1  42462  itgsinexp  42463  stoweidlem1  42509  wallispilem4  42576  wallispilem5  42577  wallispi2lem2  42580  stirlinglem3  42584  stirlinglem5  42586  stirlinglem7  42588  stirlinglem8  42589  stirlinglem10  42591  stirlinglem11  42592  hoiqssbllem2  43128  fmtnoge3  43913  fmtnom1nn  43915  fmtnof1  43918  fmtnorec1  43920  sqrtpwpw2p  43921  fmtnosqrt  43922  fmtnorec2lem  43925  fmtnodvds  43927  fmtnorec3  43931  fmtnorec4  43932  fmtno2  43933  fmtno3  43934  fmtno5lem2  43937  fmtno5lem4  43939  fmtno5  43940  257prm  43944  odz2prm2pw  43946  fmtnoprmfac1lem  43947  fmtnoprmfac2lem1  43949  fmtnofac2lem  43951  fmtnofac2  43952  fmtnofac1  43953  fmtno4prmfac  43955  fmtno4nprmfac193  43957  fmtno4prm  43958  fmtno5faclem1  43962  fmtno5faclem2  43963  fmtno5faclem3  43964  fmtno5fac  43965  flsqrt  43976  139prmALT  43979  31prm  43980  m5prm  43981  127prm  43982  m7prm  43983  2exp11  43984  m11nprm  43985  sfprmdvdsmersenne  43987  lighneallem2  43990  lighneallem3  43991  lighneallem4a  43992  proththd  43998  3exp4mod41  44000  41prothprmlem1  44001  oexpnegALTV  44061  fppr2odd  44115  2exp340mod341  44117  341fppr2  44118  8exp8mod9  44120  nfermltl2rev  44127  evengpoap3  44183  tgblthelfgott  44199  tgoldbachlt  44200  tgoldbach  44201  pgrple2abl  44632  pgrpgt2nabl  44633  ply1mulgsumlem2  44660  logbpw2m1  44846  blenpw2m1  44858  dignn0ehalf  44896  nn0sumshdiglemA  44898  nn0sumshdiglemB  44899  nn0mullong  44904  itcoval2  44932  itcoval3  44933  itcovalt2lem2lem2  44942  itcovalt2lem1  44943  ackval2  44950  ackval3  44951  ackval0012  44957  ackval1012  44958  ackval2012  44959  ackval3012  44960  ackval42  44964  2sphere  45017  itscnhlinecirc02plem3  45052  inlinecirc02p  45055  onetansqsecsq  45141  cotsqcscsq  45142
  Copyright terms: Public domain W3C validator