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

Theorem 1nn0 10583
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 10321 . 2  |-  1  e.  NN
21nnnn0i 10575 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   1c1 9271   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-1cn 9328
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10311  df-n0 10568
This theorem is referenced by:  peano2nn0  10608  numsucc  10769  numadd  10777  numaddc  10778  6p5lem  10792  6p6e12  10794  7p5e12  10796  8p4e12  10800  9p2e11  10805  9p3e12  10806  10p10e20  10813  4t4e16  10816  5t4e20  10818  6t3e18  10821  6t4e24  10822  7t3e21  10826  7t4e28  10827  8t3e24  10832  9t3e27  10839  9t9e81  10845  4fvwrd4  11517  fzo0ss1  11563  fzo0sn0fzo1  11601  injresinjlem  11622  expn1  11859  nn0expcl  11863  sqval  11909  nn0opthlem1  12030  fac2  12041  faclbnd4lem2  12054  bcn1  12073  bcpasc  12081  bccl  12082  hashsng  12120  hashrabrsn  12121  hashprlei  12161  hashtplei  12169  swrd0len0  12313  swrdtrcfv  12321  swrdccatwrd  12346  wrdeqs1cat  12353  repsw1  12405  cshw1  12440  s3fv1  12500  repsw2  12534  repsw3  12535  bcxmas  13281  climcndslem2  13296  climcnds  13297  arisum  13305  geoisum1  13322  geoisum1c  13323  mertenslem2  13328  ege2le3  13358  ef4p  13380  efgt1p2  13381  efgt1p  13382  sin01gt0  13457  rpnnen2lem3  13482  dvds1  13564  bitsmod  13615  bitsinv1lem  13620  sadadd2lem  13638  sadadd  13646  sadass  13650  smupp1  13659  smumul  13672  dfphi2  13832  reumodprminv  13855  pcelnn  13919  pockthg  13950  vdwlem12  14036  dec5nprm  14078  dec2nprm  14079  modxp1i  14082  2exp6  14098  2exp8  14099  2exp16  14100  2expltfac  14102  5prm  14119  11prm  14125  13prm  14126  17prm  14127  19prm  14128  23prm  14129  prmlem2  14130  37prm  14131  43prm  14132  83prm  14133  139prm  14134  163prm  14135  317prm  14136  631prm  14137  1259lem1  14138  1259lem2  14139  1259lem3  14140  1259lem4  14141  1259lem5  14142  1259prm  14143  2503lem1  14144  2503lem2  14145  2503lem3  14146  2503prm  14147  4001lem1  14148  4001lem2  14149  4001lem3  14150  4001lem4  14151  4001prm  14152  ocndx  14322  ocid  14323  dsndx  14324  dsid  14325  unifndx  14326  unifid  14327  odrngstr  14328  ressds  14335  homndx  14336  homid  14337  ccondx  14338  ccoid  14339  resshom  14340  ressco  14341  imasvalstr  14373  prdsvalstr  14374  oppchomfval  14636  oppcbas  14640  rescbas  14725  rescco  14728  rescabs  14729  catstr  14850  ipostr  15306  psgnunilem2  15981  odcau  16083  efgsp1  16214  efgsres  16215  efgredlemd  16221  efgredlem  16224  lt6abl  16351  mgpds  16575  srads  17189  mvridlemOLD  17426  mvrid  17430  mvrf1  17432  mplcoe3  17479  mplcoe3OLD  17480  psrbagsn  17509  cnfldstr  17664  thlbas  17963  thlle  17964  ressunif  19679  tuslem  19684  tmslem  19899  dscmet  20007  tnglem  20068  iblcnlem1  21107  dveflem  21293  c1lip2  21312  evlslem1  21367  ply1remlem  21519  fta1glem1  21522  fta1blem  21525  plyid  21562  coeidp  21615  dgrid  21616  dvply1  21635  vieta1lem2  21662  vieta1  21663  aalioulem3  21685  aaliou2b  21692  dvtaylp  21720  taylthlem1  21723  taylthlem2  21724  radcnvlem2  21764  dvradcnv  21771  pserdvlem2  21778  logtayllem  21989  logtayl  21990  cxp1  22001  dcubic1lem  22123  dcubic2  22124  mcubic  22127  quart1cl  22134  quart1lem  22135  quart1  22136  quartlem1  22137  quartlem2  22138  leibpilem2  22221  log2ublem3  22228  log2ub  22229  birthday  22233  basellem5  22307  issqf  22359  ppi2  22393  mumullem2  22403  sqff1o  22405  1sgmprm  22423  ppiublem2  22427  chtublem  22435  logfacbnd3  22447  logexprlim  22449  logfacrlim2  22450  perfectlem1  22453  perfectlem2  22454  bclbnd  22504  bpos1  22507  bposlem6  22513  lgsval  22524  rpvmasumlem  22621  log2sumbnd  22678  itvndx  22786  lngndx  22787  itvid  22788  lngid  22789  trkgstr  22790  ttgval  22944  ttglem  22945  ttgbas  22946  ttgds  22950  eengstr  23049  usgraex1elv  23138  cusgrasizeindb1  23202  redwlklem  23327  redwlk  23328  usgrcyclnl2  23350  3v3e3cycl1  23353  constr3pthlem3  23366  4cycl4v4e  23375  4cycl4dv  23376  konigsberg  23431  1kp2ke3k  23476  omndmul2  25999  nn0srg  26063  nexple  26302  oddpwdc  26585  eulerpartlemd  26597  eulerpartlemgs2  26611  eulerpartlemn  26612  iwrdsplit  26618  fib0  26630  fib1  26631  fibp1  26632  ballotlemfrci  26758  ballotlemfrceq  26759  sgnmulsgn  26780  sgnmulsgp  26781  plymulx0  26796  signstfveq0  26826  signsvvf  26828  signsvfn  26831  signshlen  26839  lgamcvg2  26889  gamp1  26892  subfac1  26914  kur14lem9  26950  relexpsucr  27179  rtrclreclem.subset  27194  fprodnn0cl  27317  nn0risefaccl  27372  bpoly1  28041  bpoly3  28048  bpoly4  28049  fsumcube  28050  nn0prpw  28362  pell1qr1  29057  rmspecfund  29095  jm2.23  29190  jm2.27c  29201  itgpowd  29435  areaquad  29437  wallispilem2  29707  wallispilem5  29710  wallispi2lem2  29713  stirlinglem5  29719  stirlinglem7  29721  stirlinglem10  29724  stirlinglem11  29725  wwlktovf  30097  ccatw2s1p2  30116  usgra2pthlem1  30146  usg2cwwkdifex  30341  rusgranumwlkl1  30405  rusgranumwlkb1  30418  hashen1  30581  0rngnnzr  30609
  Copyright terms: Public domain W3C validator