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

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

Proof of Theorem 1nn0
StepHypRef Expression
1 1nn 11638 . 2 1 ∈ ℕ
21nnnn0i 11894 1 1 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10527  0cn0 11886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628  df-n0 11887
This theorem is referenced by:  peano2nn0  11926  deccl  12102  10nn0  12105  numsucc  12127  numadd  12134  numaddc  12135  11multnc  12155  6p5lem  12157  6p6e12  12161  7p5e12  12164  8p4e12  12169  9p2e11  12174  9p3e12  12175  10p10e20  12182  4t4e16  12186  5t2e10  12187  5t4e20  12189  6t3e18  12192  6t4e24  12193  7t3e21  12197  7t4e28  12198  8t3e24  12203  9t3e27  12210  9t9e81  12216  xnn0n0n1ge2b  12516  fz0to3un2pr  12999  elfzom1elp1fzo  13094  fzo0sn0fzo1  13116  fldiv4lem1div2  13197  expn1  13429  nn0expcl  13433  sqval  13471  nn0opthlem1  13618  fac2  13629  faclbnd4lem2  13644  bccl  13672  hashsng  13720  hashen1  13721  hashrabrsn  13723  1elfz0hash  13741  hashgt23el  13775  hashprlei  13816  hashtplei  13832  wrdred1hash  13903  pfx1  14055  repsw1  14135  cshw1  14174  s3fv1  14244  s4fv1  14248  pfx2  14299  repsw2  14302  repsw3  14303  wwlktovf  14310  relexp1g  14375  relexpaddg  14402  rtrclreclem2  14408  bcxmas  15180  climcndslem2  15195  climcnds  15196  arisum  15205  geoisum1  15225  geoisum1c  15226  mertenslem2  15231  fprodnn0cl  15301  nn0risefaccl  15366  bpoly1  15395  bpoly4  15403  fsumcube  15404  ege2le3  15433  ef4p  15456  efgt1p2  15457  efgt1p  15458  sin01gt0  15533  rpnnen2lem3  15559  dvds1  15659  3dvds2dec  15672  bitsmod  15775  bitsinv1lem  15780  sadadd2lem  15798  sadadd  15806  sadass  15810  smupp1  15819  smumul  15832  pcelnn  16196  pockthg  16232  vdwlem12  16318  prmo1  16363  dec5nprm  16392  dec2nprm  16393  modxp1i  16396  2exp8  16413  2exp16  16414  2expltfac  16416  5prm  16432  11prm  16438  13prm  16439  17prm  16440  19prm  16441  23prm  16442  prmlem2  16443  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  ocndx  16663  ocid  16664  dsndx  16665  dsid  16666  unifndx  16667  unifid  16668  odrngstr  16669  ressds  16676  homndx  16677  homid  16678  ccondx  16679  ccoid  16680  resshom  16681  ressco  16682  slotsbhcdif  16683  imasvalstr  16715  prdsvalstr  16716  oppchomfval  16974  oppcbas  16978  rescbas  17089  rescco  17092  rescabs  17093  catstr  17217  ipostr  17753  cycsubmcl  18284  psgnunilem2  18554  odcau  18660  lt6abl  18946  mgpds  19180  srads  19889  0ringnnzr  19972  mvrid  20133  mvrf1  20135  mplcoe3  20177  psrbagsn  20205  evlslem1  20225  cnfldstr  20477  cnfldfun  20487  nn0srg  20545  thlbas  20770  thlle  20771  pmatcollpw3fi1lem1  21324  chfacfscmulgsum  21398  chfacfpmmulfsupp  21401  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cpmadugsumlemB  21412  cpmadugsumlemF  21414  ressunif  22800  tuslem  22805  tmslem  23021  dscmet  23111  tnglem  23178  ehl1eudis  23952  dveflem  24505  c1lip2  24524  ply1remlem  24685  fta1glem1  24688  fta1blem  24691  plyid  24728  coeidp  24782  dgrid  24783  vieta1lem2  24829  vieta1  24830  aalioulem3  24852  aaliou2b  24859  dvtaylp  24887  taylthlem1  24890  taylthlem2  24891  radcnvlem2  24931  dvradcnv  24938  pserdvlem2  24945  logtayllem  25169  logtayl  25170  cxp1  25181  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  quartlem2  25363  leibpilem2  25447  log2ublem3  25454  log2ub  25455  birthday  25460  lgamcvg2  25560  gamp1  25563  issqf  25641  ppi2  25675  mumullem2  25685  sqff1o  25687  1sgmprm  25703  ppiublem2  25707  chtublem  25715  logfacbnd3  25727  logexprlim  25729  logfacrlim2  25730  perfectlem1  25733  perfectlem2  25734  bclbnd  25784  bpos1  25787  bposlem6  25793  lgsval  25805  2lgslem3a  25900  2lgslem3c  25902  rpvmasumlem  25991  log2sumbnd  26048  itvndx  26154  lngndx  26155  itvid  26156  lngid  26157  trkgstr  26158  ttgval  26589  ttglem  26590  ttgbas  26591  ttgds  26595  eengstr  26694  edgfid  26704  edgfndxnn  26705  edgfndxid  26706  baseltedgf  26707  usgrexmplef  26969  cusgrsizeindb1  27160  wlk1ewlk  27349  usgr2pthlem  27472  uspgrn2crct  27514  crctcshwlkn0lem5  27520  rusgrnumwwlkl1  27675  rusgrnumwwlkb1  27679  clwwlkccatlem  27695  clwwlkinwwlk  27746  umgr2cwwkdifex  27772  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  konigsbergiedgw  27955  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  konigsberglem4  27962  1kp2ke3k  28153  ex-exp  28157  ex-fac  28158  9p10ne21  28177  prmdvdsbc  30459  dpmul4  30518  threehalves  30519  1mhdrd  30520  s2f1  30549  omndmul2  30641  cycpm2tr  30689  freshmansdream  30787  drngdimgt0  30916  lmat22e12  30984  lmat22e21  30985  lmat22e22  30986  madjusmdetlem4  30995  nexple  31168  oddpwdc  31512  eulerpartlemd  31524  eulerpartlemgs2  31538  eulerpartlemn  31539  iwrdsplit  31545  fib0  31557  fib1  31558  fibp1  31559  sgnmulsgn  31707  sgnmulsgp  31708  plymulx0  31717  signstfveq0  31747  signsvvf  31749  signsvfn  31752  signshlen  31760  prodfzo03  31774  reprsuc  31786  breprexplemc  31803  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  hgt750leme  31829  usgrgt2cycl  32275  subfac1  32323  kur14lem9  32359  bccolsum  32869  nn0prpw  33569  235t711  39057  ex-decpmul  39058  nn0rppwr  39062  fltnltalem  39154  3cubeslem3l  39163  3cubeslem3r  39164  pell1qr1  39348  rmspecfund  39386  jm2.23  39473  jm2.27c  39484  itgpowd  39701  areaquad  39703  brfvidRP  39913  brfvrcld  39916  corclrcl  39932  dftrcl3  39945  dfrtrcl3  39958  fvrtrcllb1d  39962  corcltrcl  39964  cotrclrcl  39967  inductionexd  40385  radcnvrat  40526  binomcxplemnn0  40561  binomcxplemfrat  40563  binomcxplemnotnn0  40568  wallispilem2  42232  wallispilem5  42235  wallispi2lem2  42238  stirlinglem5  42244  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  fourierdlem48  42320  iccpartigtl  43430  iccpartlt  43431  iccpartgel  43436  fmtnosqrt  43548  fmtno1  43550  fmtno2  43559  fmtno5lem1  43562  fmtno5lem2  43563  fmtno5lem3  43564  fmtno5lem4  43565  fmtno5  43566  257prm  43570  fmtnofac1  43579  fmtno4prmfac  43581  fmtno4prmfac193  43582  fmtno4nprmfac193  43583  fmtno5faclem1  43588  fmtno5faclem2  43589  fmtno5faclem3  43590  fmtno5fac  43591  fmtno5nprm  43592  3ndvds4  43605  139prmALT  43606  31prm  43607  m5prm  43608  127prm  43610  m7prm  43611  2exp11  43612  m11nprm  43613  lighneallem2  43618  perfectALTVlem1  43733  perfectALTVlem2  43734  11t31e341  43744  2exp340mod341  43745  341fppr2  43746  8exp8mod9  43748  nfermltl8rev  43754  nfermltl2rev  43755  evengpoap3  43811  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  bgoldbachlt  43825  tgblthelfgott  43827  smndex2dnrinv  43985  nnpw2pmod  44541  dig1  44566  dignn0flhalflem2  44574
  Copyright terms: Public domain W3C validator