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

Theorem 1nn0 11346
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 11069 . 2 1 ∈ ℕ
21nnnn0i 11338 1 1 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  1c1 9975  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-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059  df-n0 11331
This theorem is referenced by:  peano2nn0  11371  deccl  11550  10nn0  11554  numsucc  11587  numadd  11598  numaddc  11599  11multnc  11630  6p5lem  11633  6p6e12  11640  7p5e12  11645  8p4e12  11652  9p2e11  11657  9p2e11OLD  11658  9p3e12  11659  10p10e20  11666  10p10e20OLD  11667  4t4e16  11671  5t2e10  11672  5t4e20  11675  5t4e20OLD  11676  6t3e18  11680  6t4e24  11681  7t3e21  11687  7t4e28  11688  8t3e24  11693  9t3e27  11702  9t9e81  11708  xnn0n0n1ge2b  12003  fz0to3un2pr  12480  elfzom1elp1fzo  12574  fzo0sn0fzo1  12597  fldiv4lem1div2  12678  expn1  12910  nn0expcl  12914  sqval  12962  sq10  13088  nn0opthlem1  13095  fac2  13106  faclbnd4lem2  13121  bccl  13149  hashsng  13197  hashen1  13198  hashrabrsn  13199  1elfz0hash  13217  hashprlei  13288  hashtplei  13304  wrdred1hash  13383  swrd0len0  13482  swrdtrcfv  13487  swrdccatwrd  13514  wrdeqs1cat  13520  repsw1  13576  cshw1  13614  s3fv1  13683  s4fv1  13687  repsw2  13739  repsw3  13740  wwlktovf  13745  relexp1g  13810  relexpaddg  13837  rtrclreclem2  13843  bcxmas  14611  climcndslem2  14626  climcnds  14627  arisum  14636  geoisum1  14654  geoisum1c  14655  mertenslem2  14661  fprodnn0cl  14731  nn0risefaccl  14797  bpoly1  14826  bpoly4  14834  fsumcube  14835  ege2le3  14864  ef4p  14887  efgt1p2  14888  efgt1p  14889  sin01gt0  14964  rpnnen2lem3  14989  dvds1  15088  3dvds2dec  15103  3dvds2decOLD  15104  bitsmod  15205  bitsinv1lem  15210  sadadd2lem  15228  sadadd  15236  sadass  15240  smupp1  15249  smumul  15262  pcelnn  15621  pockthg  15657  vdwlem12  15743  prmo1  15788  dec5nprm  15817  dec2nprm  15818  modxp1i  15821  2exp8  15843  2exp16  15844  2expltfac  15846  5prm  15862  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  ocndx  16107  ocid  16108  dsndx  16109  dsid  16110  unifndx  16111  unifid  16112  odrngstr  16113  ressds  16120  homndx  16121  homid  16122  ccondx  16123  ccoid  16124  resshom  16125  ressco  16126  slotsbhcdif  16127  imasvalstr  16159  prdsvalstr  16160  oppchomfval  16421  oppcbas  16425  rescbas  16536  rescco  16539  rescabs  16540  catstr  16664  ipostr  17200  psgnunilem2  17961  odcau  18065  lt6abl  18342  mgpds  18545  srads  19234  0ringnnzr  19317  mvrid  19471  mvrf1  19473  mplcoe3  19514  psrbagsn  19543  evlslem1  19563  cnfldstr  19796  cnfldfun  19806  nn0srg  19864  thlbas  20088  thlle  20089  pmatcollpw3fi1lem1  20639  chfacfscmulgsum  20713  chfacfpmmulfsupp  20716  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cpmadugsumlemB  20727  cpmadugsumlemF  20729  ressunif  22113  tuslem  22118  tmslem  22334  dscmet  22424  tnglem  22491  dveflem  23787  c1lip2  23806  ply1remlem  23967  fta1glem1  23970  fta1blem  23973  plyid  24010  coeidp  24064  dgrid  24065  vieta1lem2  24111  vieta1  24112  aalioulem3  24134  aaliou2b  24141  dvtaylp  24169  taylthlem1  24172  taylthlem2  24173  radcnvlem2  24213  dvradcnv  24220  pserdvlem2  24227  logtayllem  24450  logtayl  24451  cxp1  24462  dcubic1lem  24615  dcubic2  24616  mcubic  24619  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem2  24630  leibpilem2  24713  log2ublem3  24720  log2ub  24721  birthday  24726  lgamcvg2  24826  gamp1  24829  issqf  24907  ppi2  24941  mumullem2  24951  sqff1o  24953  1sgmprm  24969  ppiublem2  24973  chtublem  24981  logfacbnd3  24993  logexprlim  24995  logfacrlim2  24996  perfectlem1  24999  perfectlem2  25000  bclbnd  25050  bpos1  25053  bposlem6  25059  lgsval  25071  2lgslem3a  25166  2lgslem3c  25168  rpvmasumlem  25221  log2sumbnd  25278  itvndx  25384  lngndx  25385  itvid  25386  lngid  25387  trkgstr  25388  ttgval  25800  ttglem  25801  ttgbas  25802  ttgds  25806  eengstr  25905  edgfid  25914  edgfndxnn  25915  edgfndxid  25916  baseltedgf  25917  usgrexmplef  26196  cusgrsizeindb1  26402  wlk1ewlk  26592  usgr2pthlem  26715  uspgrn2crct  26756  crctcshwlkn0lem5  26762  rusgrnumwwlkl1  26935  rusgrnumwwlkb1  26939  clwwlkinwwlk  27003  umgr2cwwkdifex  27029  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem4  27233  extwwlkfablem  27326  2clwwlk2clwwlklem2lem1  27328  clwwlkccatlem  27331  1kp2ke3k  27433  ex-exp  27437  ex-fac  27438  dpmul4  29750  threehalves  29751  1mhdrd  29752  omndmul2  29840  lmat22e12  30013  lmat22e21  30014  lmat22e22  30015  madjusmdetlem4  30024  nexple  30199  oddpwdc  30544  eulerpartlemd  30556  eulerpartlemgs2  30570  eulerpartlemn  30571  iwrdsplit  30577  fib0  30589  fib1  30590  fibp1  30591  sgnmulsgn  30739  sgnmulsgp  30740  plymulx0  30752  signstfveq0  30782  signsvvf  30784  signsvfn  30787  signshlen  30795  prodfzo03  30809  reprsuc  30821  breprexplemc  30838  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  subfac1  31286  kur14lem9  31322  bccolsum  31751  nn0prpw  32443  pell1qr1  37752  rmspecfund  37791  jm2.23  37880  jm2.27c  37891  itgpowd  38117  areaquad  38119  brfvidRP  38297  brfvrcld  38300  corclrcl  38316  dftrcl3  38329  dfrtrcl3  38342  fvrtrcllb1d  38346  corcltrcl  38348  cotrclrcl  38351  inductionexd  38770  radcnvrat  38830  binomcxplemnn0  38865  binomcxplemfrat  38867  binomcxplemnotnn0  38872  wallispilem2  40601  wallispilem5  40604  wallispi2lem2  40607  stirlinglem5  40613  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  fourierdlem48  40689  iccpartigtl  41684  iccpartlt  41685  iccpartgel  41690  pfx1  41736  pfx2  41737  fmtnosqrt  41776  fmtno1  41778  fmtno2  41787  fmtno5lem1  41790  fmtno5lem2  41791  fmtno5lem3  41792  fmtno5lem4  41793  fmtno5  41794  257prm  41798  fmtnofac1  41807  fmtno4prmfac  41809  fmtno4prmfac193  41810  fmtno4nprmfac193  41811  fmtno5faclem1  41816  fmtno5faclem2  41817  fmtno5faclem3  41818  fmtno5fac  41819  fmtno5nprm  41820  3ndvds4  41835  139prmALT  41836  31prm  41837  m5prm  41838  127prm  41840  m7prm  41841  2exp11  41842  m11nprm  41843  lighneallem2  41848  perfectALTVlem1  41955  perfectALTVlem2  41956  evengpoap3  42012  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  bgoldbachlt  42026  tgblthelfgott  42028  bgoldbachltOLD  42032  tgblthelfgottOLD  42034  nnpw2pmod  42702  dig1  42727  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator