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

Theorem 1nn0 10807
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 10542 . 2  |-  1  e.  NN
21nnnn0i 10799 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   1c1 9482   NN0cn0 10791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-1cn 9539
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532  df-n0 10792
This theorem is referenced by:  peano2nn0  10832  numsucc  11002  numadd  11010  numaddc  11011  6p5lem  11025  6p6e12  11027  7p5e12  11029  8p4e12  11033  9p2e11  11038  9p3e12  11039  10p10e20  11046  4t4e16  11049  5t4e20  11051  6t3e18  11054  6t4e24  11055  7t3e21  11059  7t4e28  11060  8t3e24  11065  9t3e27  11072  9t9e81  11078  elfzom1elp1fzo  11864  fzo0sn0fzo1  11883  expn1  12158  nn0expcl  12162  sqval  12209  nn0opthlem1  12330  fac2  12341  faclbnd4lem2  12354  bccl  12382  hashsng  12421  hashen1  12422  hashrabrsn  12423  1elfz0hash  12441  hashprlei  12498  hashtplei  12506  swrd0len0  12652  swrdtrcfv  12657  swrdccatwrd  12684  wrdeqs1cat  12691  repsw1  12746  cshw1  12781  s3fv1  12845  repsw2  12879  repsw3  12880  wwlktovf  12885  relexp1g  12943  relexpaddg  12968  rtrclreclem2  12974  bcxmas  13729  climcndslem2  13744  climcnds  13745  arisum  13753  geoisum1  13770  geoisum1c  13771  mertenslem2  13776  fprodnn0cl  13846  ege2le3  13907  ef4p  13930  efgt1p2  13931  efgt1p  13932  sin01gt0  14007  rpnnen2lem3  14034  dvds1  14118  bitsmod  14170  bitsinv1lem  14175  sadadd2lem  14193  sadadd  14201  sadass  14205  smupp1  14214  smumul  14227  pcelnn  14477  pockthg  14508  vdwlem12  14594  dec5nprm  14636  dec2nprm  14637  modxp1i  14640  2exp6OLD  14657  2exp8  14658  2exp16  14659  2expltfac  14661  5prm  14678  11prm  14684  13prm  14685  17prm  14686  19prm  14687  23prm  14688  prmlem2  14689  37prm  14690  43prm  14691  83prm  14692  139prm  14693  163prm  14694  317prm  14695  631prm  14696  1259lem1  14697  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  1259prm  14702  2503lem1  14703  2503lem2  14704  2503lem3  14705  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  4001prm  14711  ocndx  14889  ocid  14890  dsndx  14891  dsid  14892  unifndx  14893  unifid  14894  odrngstr  14895  ressds  14902  homndx  14903  homid  14904  ccondx  14905  ccoid  14906  resshom  14907  ressco  14908  slotsbhcdif  14909  imasvalstr  14941  prdsvalstr  14942  oppchomfval  15202  oppcbas  15206  rescbas  15317  rescco  15320  rescabs  15321  catstr  15445  ipostr  15982  psgnunilem2  16719  odcau  16823  lt6abl  17096  mgpds  17346  srads  18027  0ringnnzr  18112  mvridlemOLD  18270  mvrid  18274  mvrf1  18276  mplcoe3  18323  mplcoe3OLD  18324  psrbagsn  18355  evlslem1  18379  cnfldstr  18617  nn0srg  18681  thlbas  18900  thlle  18901  pmatcollpw3fi1lem1  19454  chfacfscmulgsum  19528  chfacfpmmulfsupp  19531  chfacfpmmulgsum  19532  chfacfpmmulgsum2  19533  cpmadugsumlemB  19542  cpmadugsumlemF  19544  ressunif  20931  tuslem  20936  tmslem  21151  dscmet  21259  tnglem  21320  dveflem  22546  c1lip2  22565  ply1remlem  22729  fta1glem1  22732  fta1blem  22735  plyid  22772  coeidp  22826  dgrid  22827  vieta1lem2  22873  vieta1  22874  aalioulem3  22896  aaliou2b  22903  dvtaylp  22931  taylthlem1  22934  taylthlem2  22935  radcnvlem2  22975  dvradcnv  22982  pserdvlem2  22989  logtayllem  23208  logtayl  23209  cxp1  23220  dcubic1lem  23371  dcubic2  23372  mcubic  23375  quart1cl  23382  quart1lem  23383  quart1  23384  quartlem1  23385  quartlem2  23386  leibpilem2  23469  log2ublem3  23476  log2ub  23477  birthday  23482  issqf  23608  ppi2  23642  mumullem2  23652  sqff1o  23654  1sgmprm  23672  ppiublem2  23676  chtublem  23684  logfacbnd3  23696  logexprlim  23698  logfacrlim2  23699  perfectlem1  23702  perfectlem2  23703  bclbnd  23753  bpos1  23756  bposlem6  23762  lgsval  23773  rpvmasumlem  23870  log2sumbnd  23927  itvndx  24034  lngndx  24035  itvid  24036  lngid  24037  trkgstr  24038  ttgval  24380  ttglem  24381  ttgbas  24382  ttgds  24386  eengstr  24485  usgraex1elv  24599  cusgrasizeindb1  24673  redwlklem  24809  usgrcyclnl2  24843  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv  24869  usg2cwwkdifex  25023  rusgranumwlkl1  25149  rusgranumwlkb1  25156  konigsberg  25189  1kp2ke3k  25369  omndmul2  27936  nexple  28239  oddpwdc  28557  eulerpartlemd  28569  eulerpartlemgs2  28583  eulerpartlemn  28584  iwrdsplit  28590  fib0  28602  fib1  28603  fibp1  28604  sgnmulsgn  28752  sgnmulsgp  28753  plymulx0  28768  signstfveq0  28798  signsvvf  28800  signsvfn  28803  signshlen  28811  lgamcvg2  28861  gamp1  28864  subfac1  28886  kur14lem9  28922  nn0risefaccl  29385  bpoly1  30041  bpoly4  30049  fsumcube  30050  nn0prpw  30381  pell1qr1  31046  rmspecfund  31084  jm2.23  31177  jm2.27c  31188  itgpowd  31423  areaquad  31425  radcnvrat  31436  binomcxplemnn0  31495  binomcxplemfrat  31497  binomcxplemnotnn0  31502  wallispilem2  32087  wallispilem5  32090  wallispi2lem2  32093  stirlinglem5  32099  stirlinglem7  32101  stirlinglem10  32104  stirlinglem11  32105  fourierdlem48  32176  pfx1  32639  pfx2  32640  usgra2pthlem1  32725  uhgrepe  32750  nnpw2pmod  33458  dig1  33483  dignn0flhalflem2  33491  dftrcl3  38213  dfrtrcl3  38214  corclrcl  38230  corcltrcl  38231  cotrclrcl  38232  inductionexd  38419
  Copyright terms: Public domain W3C validator