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

Theorem 1nn0 11575
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 11316 . 2 1 ∈ ℕ
21nnnn0i 11567 1 1 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  1c1 10222  0cn0 11559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-1cn 10279
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-nn 11306  df-n0 11560
This theorem is referenced by:  peano2nn0  11599  deccl  11774  10nn0  11777  numsucc  11799  numadd  11806  numaddc  11807  11multnc  11827  6p5lem  11829  6p6e12  11833  7p5e12  11836  8p4e12  11841  9p2e11  11846  9p3e12  11847  10p10e20  11854  4t4e16  11858  5t2e10  11859  5t4e20  11861  6t3e18  11864  6t4e24  11865  7t3e21  11869  7t4e28  11870  8t3e24  11875  9t3e27  11882  9t9e81  11888  xnn0n0n1ge2b  12181  fz0to3un2pr  12665  elfzom1elp1fzo  12759  fzo0sn0fzo1  12781  fldiv4lem1div2  12862  expn1  13093  nn0expcl  13097  sqval  13145  sq10  13271  nn0opthlem1  13275  fac2  13286  faclbnd4lem2  13301  bccl  13329  hashsng  13377  hashen1  13378  hashrabrsn  13379  1elfz0hash  13397  hashprlei  13467  hashtplei  13483  wrdred1hash  13562  swrd0len0  13660  swrdtrcfv  13665  swrdccatwrd  13692  wrdeqs1cat  13698  repsw1  13754  cshw1  13792  s3fv1  13861  s4fv1  13865  repsw2  13918  repsw3  13919  wwlktovf  13924  relexp1g  13989  relexpaddg  14016  rtrclreclem2  14022  bcxmas  14789  climcndslem2  14804  climcnds  14805  arisum  14814  geoisum1  14832  geoisum1c  14833  mertenslem2  14838  fprodnn0cl  14908  nn0risefaccl  14973  bpoly1  15002  bpoly4  15010  fsumcube  15011  ege2le3  15040  ef4p  15063  efgt1p2  15064  efgt1p  15065  sin01gt0  15140  rpnnen2lem3  15165  dvds1  15264  3dvds2dec  15277  bitsmod  15377  bitsinv1lem  15382  sadadd2lem  15400  sadadd  15408  sadass  15412  smupp1  15421  smumul  15434  pcelnn  15791  pockthg  15827  vdwlem12  15913  prmo1  15958  dec5nprm  15987  dec2nprm  15988  modxp1i  15991  2exp8  16008  2exp16  16009  2expltfac  16011  5prm  16027  11prm  16033  13prm  16034  17prm  16035  19prm  16036  23prm  16037  prmlem2  16038  37prm  16039  43prm  16040  83prm  16041  139prm  16042  163prm  16043  317prm  16044  631prm  16045  1259lem1  16049  1259lem2  16050  1259lem3  16051  1259lem4  16052  1259lem5  16053  1259prm  16054  2503lem1  16055  2503lem2  16056  2503lem3  16057  2503prm  16058  4001lem1  16059  4001lem2  16060  4001lem3  16061  4001lem4  16062  4001prm  16063  ocndx  16265  ocid  16266  dsndx  16267  dsid  16268  unifndx  16269  unifid  16270  odrngstr  16271  ressds  16278  homndx  16279  homid  16280  ccondx  16281  ccoid  16282  resshom  16283  ressco  16284  slotsbhcdif  16285  imasvalstr  16317  prdsvalstr  16318  oppchomfval  16578  oppcbas  16582  rescbas  16693  rescco  16696  rescabs  16697  catstr  16821  ipostr  17358  psgnunilem2  18116  odcau  18220  lt6abl  18497  mgpds  18701  srads  19395  0ringnnzr  19478  mvrid  19632  mvrf1  19634  mplcoe3  19675  psrbagsn  19703  evlslem1  19723  cnfldstr  19956  cnfldfun  19966  nn0srg  20024  thlbas  20250  thlle  20251  pmatcollpw3fi1lem1  20804  chfacfscmulgsum  20878  chfacfpmmulfsupp  20881  chfacfpmmulgsum  20882  chfacfpmmulgsum2  20883  cpmadugsumlemB  20892  cpmadugsumlemF  20894  ressunif  22279  tuslem  22284  tmslem  22500  dscmet  22590  tnglem  22657  dveflem  23956  c1lip2  23975  ply1remlem  24136  fta1glem1  24139  fta1blem  24142  plyid  24179  coeidp  24233  dgrid  24234  vieta1lem2  24280  vieta1  24281  aalioulem3  24303  aaliou2b  24310  dvtaylp  24338  taylthlem1  24341  taylthlem2  24342  radcnvlem2  24382  dvradcnv  24389  pserdvlem2  24396  logtayllem  24619  logtayl  24620  cxp1  24631  dcubic1lem  24784  dcubic2  24785  mcubic  24788  quart1cl  24795  quart1lem  24796  quart1  24797  quartlem1  24798  quartlem2  24799  leibpilem2  24882  log2ublem3  24889  log2ub  24890  birthday  24895  lgamcvg2  24995  gamp1  24998  issqf  25076  ppi2  25110  mumullem2  25120  sqff1o  25122  1sgmprm  25138  ppiublem2  25142  chtublem  25150  logfacbnd3  25162  logexprlim  25164  logfacrlim2  25165  perfectlem1  25168  perfectlem2  25169  bclbnd  25219  bpos1  25222  bposlem6  25228  lgsval  25240  2lgslem3a  25335  2lgslem3c  25337  rpvmasumlem  25390  log2sumbnd  25447  itvndx  25553  lngndx  25554  itvid  25555  lngid  25556  trkgstr  25557  ttgval  25969  ttglem  25970  ttgbas  25971  ttgds  25975  eengstr  26074  edgfid  26083  edgfndxnn  26084  edgfndxid  26085  baseltedgf  26086  usgrexmplef  26367  cusgrsizeindb1  26574  wlk1ewlk  26764  usgr2pthlem  26887  uspgrn2crct  26929  crctcshwlkn0lem5  26935  rusgrnumwwlkl1  27110  rusgrnumwwlkb1  27114  clwwlkccatlem  27132  clwwlkinwwlk  27189  umgr2cwwkdifex  27216  upgr3v3e3cycl  27353  upgr4cycl4dv4e  27358  konigsbergiedgw  27421  konigsberglem1  27425  konigsberglem2  27426  konigsberglem3  27427  konigsberglem4  27428  1kp2ke3k  27634  ex-exp  27638  ex-fac  27639  dpmul4  29947  threehalves  29948  1mhdrd  29949  omndmul2  30037  lmat22e12  30210  lmat22e21  30211  lmat22e22  30212  madjusmdetlem4  30221  nexple  30396  oddpwdc  30741  eulerpartlemd  30753  eulerpartlemgs2  30767  eulerpartlemn  30768  iwrdsplit  30774  fib0  30786  fib1  30787  fibp1  30788  sgnmulsgn  30936  sgnmulsgp  30937  plymulx0  30949  signstfveq0  30979  signsvvf  30981  signsvfn  30984  signshlen  30992  prodfzo03  31006  reprsuc  31018  breprexplemc  31035  hgt750lemd  31051  hgt750lem  31054  hgt750lem2  31055  hgt750leme  31061  subfac1  31483  kur14lem9  31519  bccolsum  31947  nn0prpw  32639  pell1qr1  37937  rmspecfund  37975  jm2.23  38064  jm2.27c  38075  itgpowd  38300  areaquad  38302  brfvidRP  38480  brfvrcld  38483  corclrcl  38499  dftrcl3  38512  dfrtrcl3  38525  fvrtrcllb1d  38529  corcltrcl  38531  cotrclrcl  38534  inductionexd  38953  radcnvrat  39013  binomcxplemnn0  39048  binomcxplemfrat  39050  binomcxplemnotnn0  39055  wallispilem2  40762  wallispilem5  40765  wallispi2lem2  40768  stirlinglem5  40774  stirlinglem7  40776  stirlinglem10  40779  stirlinglem11  40780  fourierdlem48  40850  iccpartigtl  41934  iccpartlt  41935  iccpartgel  41940  pfx1  41986  pfx2  41987  fmtnosqrt  42026  fmtno1  42028  fmtno2  42037  fmtno5lem1  42040  fmtno5lem2  42041  fmtno5lem3  42042  fmtno5lem4  42043  fmtno5  42044  257prm  42048  fmtnofac1  42057  fmtno4prmfac  42059  fmtno4prmfac193  42060  fmtno4nprmfac193  42061  fmtno5faclem1  42066  fmtno5faclem2  42067  fmtno5faclem3  42068  fmtno5fac  42069  fmtno5nprm  42070  3ndvds4  42085  139prmALT  42086  31prm  42087  m5prm  42088  127prm  42090  m7prm  42091  2exp11  42092  m11nprm  42093  lighneallem2  42098  perfectALTVlem1  42205  perfectALTVlem2  42206  evengpoap3  42262  nnsum4primesevenALTV  42264  bgoldbtbndlem1  42268  bgoldbachlt  42276  tgblthelfgott  42278  nnpw2pmod  42945  dig1  42970  dignn0flhalflem2  42978
  Copyright terms: Public domain W3C validator