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

Theorem 2nn0 11153
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 11029 . 2 2 ∈ ℕ
21nnnn0i 11144 1 2 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  2c2 10914  0cn0 11136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-1cn 9847
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-om 6932  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-nn 10865  df-2 10923  df-n0 11137
This theorem is referenced by:  nn0n0n1ge2  11202  7p6e13  11437  8p3e11  11441  8p3e11OLD  11442  8p5e13  11444  9p3e12  11450  9p4e13  11451  4t3e12  11461  4t4e16  11462  5t3e15  11464  5t3e15OLD  11465  5t5e25  11468  5t5e25OLD  11469  6t3e18  11471  6t5e30  11473  6t5e30OLD  11474  7t3e21  11478  7t4e28  11479  7t5e35  11480  7t6e42  11481  7t7e49  11482  8t3e24  11484  8t4e32  11485  8t5e40  11486  8t5e40OLD  11487  9t3e27  11493  9t4e36  11494  9t8e72  11498  9t9e81  11499  decbin3  11513  2eluzge0  11562  fzo0to42pr  12374  nn0sqcl  12701  sqmul  12740  resqcl  12745  zsqcl  12748  cu2  12777  i3  12780  i4  12781  binom3  12799  expmulnbnd  12810  nn0opthlem1  12869  fac3  12881  faclbnd2  12892  faclbnd4lem1  12894  faclbnd4lem3  12896  hash2pr  13057  hashtplei  13067  s4fv2  13435  repsw3  13485  swrd2lsw  13486  2swrd2eqwrdeq  13487  abssq  13837  sqabs  13838  iseraltlem2  14204  iseraltlem3  14205  bpoly2  14570  bpoly3  14571  bpoly4  14572  fsumcube  14573  ef4p  14625  efgt1p2  14626  efi4p  14649  ef01bndlem  14696  cos01bnd  14698  oexpneg  14850  oddge22np1  14854  bitsinv2  14946  bitsf1ocnv  14947  sadcaddlem  14960  sadadd2lem  14962  pythagtriplem4  15305  iserodd  15321  oddprmdvds  15388  prmreclem2  15402  prmreclem6  15406  vdwlem7  15472  vdwlem10  15475  vdwlem12  15477  dec2dvds  15548  dec5dvds  15549  decexp2  15560  2exp4  15575  2exp6  15576  2exp8  15577  2exp16  15578  3exp3  15579  2expltfac  15580  5prm  15596  7prm  15598  11prm  15603  13prm  15604  17prm  15605  19prm  15606  23prm  15607  prmlem2  15608  37prm  15609  43prm  15610  83prm  15611  139prm  15612  163prm  15613  317prm  15614  631prm  15615  1259lem1  15619  1259lem2  15620  1259lem3  15621  1259lem4  15622  1259lem5  15623  1259prm  15624  2503lem1  15625  2503lem2  15626  2503lem3  15627  2503prm  15628  4001lem1  15629  4001lem2  15630  4001lem3  15631  4001lem4  15632  4001prm  15633  ressds  15839  prdsvalstr  15879  pmtrprfval  17673  psgnunilem2  17681  efgredleme  17922  lt6abl  18062  mgpds  18265  srads  18950  cnfldstr  19512  setsmsds  22029  tmslem  22035  tnglem  22189  tngds  22197  sqcn  22413  dveflem  23460  iaa  23798  tangtx  23975  efif1olem3  24008  efif1olem4  24009  root1id  24209  mcubic  24288  cubic2  24289  cubic  24290  binom4  24291  dquartlem2  24293  dquart  24294  quart1cl  24295  quart1lem  24296  quart1  24297  quartlem1  24298  quartlem2  24299  atandmcj  24350  bndatandm  24370  atansopn  24373  atantayl3  24380  leibpilem2  24382  leibpi  24383  leibpisum  24384  log2cnv  24385  log2tlbnd  24386  log2ublem2  24388  log2ublem3  24389  log2ub  24390  log2le1  24391  birthday  24395  basellem3  24523  basellem4  24524  basellem5  24525  basellem8  24528  issqf  24576  ppi3  24611  ppiublem2  24642  chtublem  24650  mersenne  24666  bcmax  24717  bcp1ctr  24718  bclbnd  24719  bpos1  24722  bposlem6  24728  bposlem8  24730  lgslem1  24736  lgsqrlem2  24786  gausslemma2dlem6  24811  lgseisenlem4  24817  2lgslem1c  24832  2lgslem3a  24835  2lgslem3b  24836  2lgslem3c  24837  2lgslem3d  24838  chebbnd1lem3  24874  rplogsumlem2  24888  dchrisumlem2  24893  dchrisum0flblem1  24911  dchrisum0flblem2  24912  dchrisum0flb  24913  selberglem2  24949  pntrmax  24967  pntlemo  25010  trkgstr  25057  ttgplusg  25473  ttgds  25476  eengstr  25575  usgraex2elv  25689  is2wlk  25858  3v3e3cycl1  25935  constr3trllem3  25943  4cycl4v4e  25957  4cycl4dv  25958  clwwlkn2  26066  wwlkext2clwwlk  26094  extwwlkfablem2lem  26365  numclwwlkovf2  26374  numclwwlk2lem1  26392  numclwlk2lem2f  26393  numclwlk2lem2f1o  26395  1kp2ke3k  26458  ex-mod  26461  ex-exp  26462  ex-fac  26463  ipidsq  26750  strlem3a  28298  madjusmdetlem4  29027  zlmds  29139  coinflippv  29675  kur14lem8  30252  sinccvglem  30623  dvtan  32430  diophin  36154  irrapxlem5  36208  pellexlem2  36212  pell1qrge1  36252  jm2.22  36380  jm2.20nn  36382  jm2.27c  36392  rmydioph  36399  rmxdioph  36401  expdiophlem2  36407  frlmpwfi  36486  isnumbasgrplem3  36494  amgm2d  37323  dvdivbd  38614  itgsinexplem1  38646  itgsinexp  38647  stoweidlem1  38695  wallispilem4  38762  wallispilem5  38763  wallispi2lem2  38766  stirlinglem3  38770  stirlinglem5  38772  stirlinglem7  38774  stirlinglem8  38775  stirlinglem10  38777  stirlinglem11  38778  hoiqssbllem2  39314  fmtnoge3  39782  fmtnom1nn  39784  fmtnof1  39787  fmtnorec1  39789  sqrtpwpw2p  39790  fmtnosqrt  39791  fmtnorec2lem  39794  fmtnodvds  39796  fmtnorec3  39800  fmtnorec4  39801  fmtno2  39802  fmtno3  39803  fmtno5lem2  39806  fmtno5lem4  39808  fmtno5  39809  257prm  39813  odz2prm2pw  39815  fmtnoprmfac1lem  39816  fmtnoprmfac2lem1  39818  fmtnofac2lem  39820  fmtnofac2  39821  fmtnofac1  39822  fmtno4prmfac  39824  fmtno4nprmfac193  39826  fmtno4prm  39827  fmtno5faclem1  39831  fmtno5faclem2  39832  fmtno5faclem3  39833  fmtno5fac  39834  2exp5  39847  flsqrt  39848  139prmALT  39851  31prm  39852  m5prm  39853  2exp7  39854  127prm  39855  m7prm  39856  2exp11  39857  m11nprm  39858  sfprmdvdsmersenne  39860  lighneallem2  39863  lighneallem3  39864  lighneallem4a  39865  proththd  39871  3exp4mod41  39873  41prothprmlem1  39874  oexpnegALTV  39928  evengpoap3  40017  tgblthelfgott  40031  tgoldbachlt  40032  tgoldbach  40034  tgblthelfgottOLD  40038  tgoldbachltOLD  40039  tgoldbachOLD  40041  pfx2  40077  upgredg  40369  upgr2wlk  40875  usgr2pthlem  40968  usgr2pth  40969  wwlks2onv  41157  elwwlks2  41169  elwspths2spth  41170  upgr3v3e3cycl  41346  upgr4cycl4dv4e  41351  konigsbergiedgw  41415  konigsbergiedgwOLD  41416  konigsberglem1  41421  konigsberglem2  41422  konigsberglem3  41423  fusgr2wsp2nb  41497  av-extwwlkfablem2lem  41506  pgrple2abl  41939  pgrpgt2nabl  41940  ply1mulgsumlem2  41968  logbpw2m1  42158  blenpw2m1  42170  dignn0ehalf  42208  nn0sumshdiglemA  42210  nn0sumshdiglemB  42211  nn0mullong  42216  onetansqsecsq  42261  cotsqcscsq  42262
  Copyright terms: Public domain W3C validator