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

Theorem 1nn0 10874
Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
1nn0  |-  1  e.  NN0

Proof of Theorem 1nn0
StepHypRef Expression
1 1nn 10609 . 2  |-  1  e.  NN
21nnnn0i 10866 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867   1c1 9529   NN0cn0 10858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-1cn 9586
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-nn 10599  df-n0 10859
This theorem is referenced by:  peano2nn0  10899  numsucc  11066  numadd  11074  numaddc  11075  6p5lem  11089  6p6e12  11091  7p5e12  11093  8p4e12  11097  9p2e11  11102  9p3e12  11103  10p10e20  11110  4t4e16  11113  5t4e20  11115  6t3e18  11118  6t4e24  11119  7t3e21  11123  7t4e28  11124  8t3e24  11129  9t3e27  11136  9t9e81  11142  elfzom1elp1fzo  11967  fzo0sn0fzo1  11987  expn1  12268  nn0expcl  12272  sqval  12320  nn0opthlem1  12440  fac2  12451  faclbnd4lem2  12465  bccl  12493  hashsng  12535  hashen1  12536  hashrabrsn  12537  1elfz0hash  12555  hashprlei  12612  hashtplei  12620  swrd0len0  12766  swrdtrcfv  12771  swrdccatwrd  12798  wrdeqs1cat  12805  repsw1  12860  cshw1  12895  s3fv1  12959  repsw2  12993  repsw3  12994  wwlktovf  12999  relexp1g  13057  relexpaddg  13084  rtrclreclem2  13090  bcxmas  13860  climcndslem2  13875  climcnds  13876  arisum  13885  geoisum1  13902  geoisum1c  13903  mertenslem2  13908  fprodnn0cl  13978  nn0risefaccl  14042  bpoly1  14071  bpoly4  14079  fsumcube  14080  ege2le3  14111  ef4p  14134  efgt1p2  14135  efgt1p  14136  sin01gt0  14211  rpnnen2lem3  14236  dvds1  14320  bitsmod  14373  bitsinv1lem  14378  sadadd2lem  14396  sadadd  14404  sadass  14408  smupp1  14417  smumul  14430  pcelnn  14771  pockthg  14802  vdwlem12  14894  prmo1  14947  dec5nprm  14990  dec2nprm  14991  modxp1i  14994  2exp6OLD  15011  2exp8  15012  2exp16  15013  2expltfac  15015  5prm  15032  11prm  15038  13prm  15039  17prm  15040  19prm  15041  23prm  15042  prmlem2  15043  37prm  15044  43prm  15045  83prm  15046  139prm  15047  163prm  15048  317prm  15049  631prm  15050  1259lem1  15054  1259lem2  15055  1259lem3  15056  1259lem4  15057  1259lem5  15058  1259prm  15059  2503lem1  15060  2503lem2  15061  2503lem3  15062  2503prm  15063  4001lem1  15064  4001lem2  15065  4001lem3  15066  4001lem4  15067  4001prm  15068  ocndx  15250  ocid  15251  dsndx  15252  dsid  15253  unifndx  15254  unifid  15255  odrngstr  15256  ressds  15263  homndx  15264  homid  15265  ccondx  15266  ccoid  15267  resshom  15268  ressco  15269  slotsbhcdif  15270  imasvalstr  15302  prdsvalstr  15303  oppchomfval  15563  oppcbas  15567  rescbas  15678  rescco  15681  rescabs  15682  catstr  15806  ipostr  16343  psgnunilem2  17080  odcau  17184  lt6abl  17457  mgpds  17661  srads  18337  0ringnnzr  18421  mvrid  18575  mvrf1  18577  mplcoe3  18618  psrbagsn  18646  evlslem1  18666  cnfldstr  18900  nn0srg  18964  thlbas  19183  thlle  19184  pmatcollpw3fi1lem1  19734  chfacfscmulgsum  19808  chfacfpmmulfsupp  19811  chfacfpmmulgsum  19812  chfacfpmmulgsum2  19813  cpmadugsumlemB  19822  cpmadugsumlemF  19824  ressunif  21201  tuslem  21206  tmslem  21421  dscmet  21511  tnglem  21572  dveflem  22805  c1lip2  22824  ply1remlem  22985  fta1glem1  22988  fta1blem  22991  plyid  23028  coeidp  23082  dgrid  23083  vieta1lem2  23129  vieta1  23130  aalioulem3  23152  aaliou2b  23159  dvtaylp  23187  taylthlem1  23190  taylthlem2  23191  radcnvlem2  23231  dvradcnv  23238  pserdvlem2  23245  logtayllem  23466  logtayl  23467  cxp1  23478  dcubic1lem  23631  dcubic2  23632  mcubic  23635  quart1cl  23642  quart1lem  23643  quart1  23644  quartlem1  23645  quartlem2  23646  leibpilem2  23729  log2ublem3  23736  log2ub  23737  birthday  23742  lgamcvg2  23842  gamp1  23845  issqf  23923  ppi2  23957  mumullem2  23967  sqff1o  23969  1sgmprm  23987  ppiublem2  23991  chtublem  23999  logfacbnd3  24011  logexprlim  24013  logfacrlim2  24014  perfectlem1  24017  perfectlem2  24018  bclbnd  24068  bpos1  24071  bposlem6  24077  lgsval  24088  rpvmasumlem  24185  log2sumbnd  24242  itvndx  24348  lngndx  24349  itvid  24350  lngid  24351  trkgstr  24352  ttgval  24748  ttglem  24749  ttgbas  24750  ttgds  24754  eengstr  24853  usgraex1elv  24967  cusgrasizeindb1  25041  redwlklem  25177  usgrcyclnl2  25211  3v3e3cycl1  25214  4cycl4v4e  25236  4cycl4dv  25237  usg2cwwkdifex  25391  rusgranumwlkl1  25517  rusgranumwlkb1  25524  konigsberg  25557  1kp2ke3k  25738  omndmul2  28310  lmat22e12  28481  lmat22e21  28482  lmat22e22  28483  madjusmdetlem4  28492  nexple  28667  oddpwdc  29010  eulerpartlemd  29022  eulerpartlemgs2  29036  eulerpartlemn  29037  iwrdsplit  29043  fib0  29055  fib1  29056  fibp1  29057  sgnmulsgn  29205  sgnmulsgp  29206  plymulx0  29221  signstfveq0  29251  signsvvf  29253  signsvfn  29256  signshlen  29264  subfac1  29686  kur14lem9  29722  bccolsum  30159  nn0prpw  30761  pell1qr1  35427  rmspecfund  35467  jm2.23  35561  jm2.27c  35572  itgpowd  35802  areaquad  35804  brfvidRP  35923  brfvrcld  35926  corclrcl  35942  dftrcl3  35955  dfrtrcl3  35968  fvrtrcllb1d  35972  corcltrcl  35974  cotrclrcl  35977  inductionexd  36234  radcnvrat  36304  binomcxplemnn0  36339  binomcxplemfrat  36341  binomcxplemnotnn0  36346  wallispilem2  37501  wallispilem5  37504  wallispi2lem2  37507  stirlinglem5  37513  stirlinglem7  37515  stirlinglem10  37518  stirlinglem11  37519  fourierdlem48  37590  iccpartigtl  38140  iccpartlt  38141  iccpartgel  38146  perfectALTVlem1  38246  perfectALTVlem2  38247  nnsum4primesevenALTV  38299  bgoldbtbndlem1  38303  bgoldbachlt  38309  tgblthelfgott  38311  pfx1  38355  pfx2  38356  usgra2pthlem1  38436  uhgrepe  38461  nnpw2pmod  39168  dig1  39193  dignn0flhalflem2  39201
  Copyright terms: Public domain W3C validator