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

Theorem 1nn0 10885
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 10620 . 2  |-  1  e.  NN
21nnnn0i 10877 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1887   1c1 9540   NN0cn0 10869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-1cn 9597
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-nn 10610  df-n0 10870
This theorem is referenced by:  peano2nn0  10910  numsucc  11077  numadd  11085  numaddc  11086  6p5lem  11100  6p6e12  11102  7p5e12  11104  8p4e12  11108  9p2e11  11113  9p3e12  11114  10p10e20  11121  4t4e16  11124  5t4e20  11126  6t3e18  11129  6t4e24  11130  7t3e21  11134  7t4e28  11135  8t3e24  11140  9t3e27  11147  9t9e81  11153  elfzom1elp1fzo  11981  fzo0sn0fzo1  12001  expn1  12282  nn0expcl  12286  sqval  12334  nn0opthlem1  12454  fac2  12465  faclbnd4lem2  12479  bccl  12507  hashsng  12549  hashen1  12550  hashrabrsn  12551  1elfz0hash  12569  hashprlei  12629  hashtplei  12640  swrd0len0  12792  swrdtrcfv  12797  swrdccatwrd  12824  wrdeqs1cat  12831  repsw1  12886  cshw1  12921  s3fv1  12986  s4fv1  12990  repsw2  13025  repsw3  13026  wwlktovf  13031  relexp1g  13089  relexpaddg  13116  rtrclreclem2  13122  bcxmas  13893  climcndslem2  13908  climcnds  13909  arisum  13918  geoisum1  13935  geoisum1c  13936  mertenslem2  13941  fprodnn0cl  14011  nn0risefaccl  14075  bpoly1  14104  bpoly4  14112  fsumcube  14113  ege2le3  14144  ef4p  14167  efgt1p2  14168  efgt1p  14169  sin01gt0  14244  rpnnen2lem3  14269  dvds1  14353  bitsmod  14410  bitsinv1lem  14415  sadadd2lem  14433  sadadd  14441  sadass  14445  smupp1  14454  smumul  14467  pcelnn  14819  pockthg  14850  vdwlem12  14942  prmo1  14995  dec5nprm  15038  dec2nprm  15039  modxp1i  15042  2exp6OLD  15059  2exp8  15060  2exp16  15061  2expltfac  15063  5prm  15080  11prm  15086  13prm  15087  17prm  15088  19prm  15089  23prm  15090  prmlem2  15091  37prm  15092  43prm  15093  83prm  15094  139prm  15095  163prm  15096  317prm  15097  631prm  15098  1259lem1  15102  1259lem2  15103  1259lem3  15104  1259lem4  15105  1259lem5  15106  1259prm  15107  2503lem1  15108  2503lem2  15109  2503lem3  15110  2503prm  15111  4001lem1  15112  4001lem2  15113  4001lem3  15114  4001lem4  15115  4001prm  15116  ocndx  15298  ocid  15299  dsndx  15300  dsid  15301  unifndx  15302  unifid  15303  odrngstr  15304  ressds  15311  homndx  15312  homid  15313  ccondx  15314  ccoid  15315  resshom  15316  ressco  15317  slotsbhcdif  15318  imasvalstr  15350  prdsvalstr  15351  oppchomfval  15619  oppcbas  15623  rescbas  15734  rescco  15737  rescabs  15738  catstr  15862  ipostr  16399  psgnunilem2  17136  odcau  17256  lt6abl  17529  mgpds  17733  srads  18409  0ringnnzr  18493  mvrid  18647  mvrf1  18649  mplcoe3  18690  psrbagsn  18718  evlslem1  18738  cnfldstr  18972  nn0srg  19037  thlbas  19259  thlle  19260  pmatcollpw3fi1lem1  19810  chfacfscmulgsum  19884  chfacfpmmulfsupp  19887  chfacfpmmulgsum  19888  chfacfpmmulgsum2  19889  cpmadugsumlemB  19898  cpmadugsumlemF  19900  ressunif  21277  tuslem  21282  tmslem  21497  dscmet  21587  tnglem  21648  dveflem  22931  c1lip2  22950  ply1remlem  23113  fta1glem1  23116  fta1blem  23119  plyid  23163  coeidp  23217  dgrid  23218  vieta1lem2  23264  vieta1  23265  aalioulem3  23290  aaliou2b  23297  dvtaylp  23325  taylthlem1  23328  taylthlem2  23329  radcnvlem2  23369  dvradcnv  23376  pserdvlem2  23383  logtayllem  23604  logtayl  23605  cxp1  23616  dcubic1lem  23769  dcubic2  23770  mcubic  23773  quart1cl  23780  quart1lem  23781  quart1  23782  quartlem1  23783  quartlem2  23784  leibpilem2  23867  log2ublem3  23874  log2ub  23875  birthday  23880  lgamcvg2  23980  gamp1  23983  issqf  24063  ppi2  24097  mumullem2  24107  sqff1o  24109  1sgmprm  24127  ppiublem2  24131  chtublem  24139  logfacbnd3  24151  logexprlim  24153  logfacrlim2  24154  perfectlem1  24157  perfectlem2  24158  bclbnd  24208  bpos1  24211  bposlem6  24217  lgsval  24228  rpvmasumlem  24325  log2sumbnd  24382  itvndx  24488  lngndx  24489  itvid  24490  lngid  24491  trkgstr  24492  ttgval  24905  ttglem  24906  ttgbas  24907  ttgds  24911  eengstr  25010  usgraex1elv  25124  cusgrasizeindb1  25199  redwlklem  25335  usgrcyclnl2  25369  3v3e3cycl1  25372  4cycl4v4e  25394  4cycl4dv  25395  usg2cwwkdifex  25549  rusgranumwlkl1  25675  rusgranumwlkb1  25682  konigsberg  25715  1kp2ke3k  25896  omndmul2  28475  lmat22e12  28645  lmat22e21  28646  lmat22e22  28647  madjusmdetlem4  28656  nexple  28831  oddpwdc  29187  eulerpartlemd  29199  eulerpartlemgs2  29213  eulerpartlemn  29214  iwrdsplit  29220  fib0  29232  fib1  29233  fibp1  29234  sgnmulsgn  29420  sgnmulsgp  29421  plymulx0  29436  signstfveq0  29466  signsvvf  29468  signsvfn  29471  signshlen  29479  subfac1  29901  kur14lem9  29937  bccolsum  30375  nn0prpw  30979  pell1qr1  35717  rmspecfund  35757  jm2.23  35851  jm2.27c  35862  itgpowd  36099  areaquad  36101  brfvidRP  36280  brfvrcld  36283  corclrcl  36299  dftrcl3  36312  dfrtrcl3  36325  fvrtrcllb1d  36329  corcltrcl  36331  cotrclrcl  36334  inductionexd  36593  radcnvrat  36663  binomcxplemnn0  36698  binomcxplemfrat  36700  binomcxplemnotnn0  36705  wallispilem2  37928  wallispilem5  37931  wallispi2lem2  37934  stirlinglem5  37940  stirlinglem7  37942  stirlinglem10  37945  stirlinglem11  37946  fourierdlem48  38018  iccpartigtl  38737  iccpartlt  38738  iccpartgel  38743  perfectALTVlem1  38843  perfectALTVlem2  38844  nnsum4primesevenALTV  38896  bgoldbtbndlem1  38900  bgoldbachlt  38906  tgblthelfgott  38908  pfx1  38952  pfx2  38953  edgfndxnn  39097  edgfndxid  39098  baseltedgf  39099  struct2griedg  39130  cusgrsizeindb1  39511  1wlk1ewlk  39649  usgra2pthlem1  39720  uhgrepe  39743  nnpw2pmod  40447  dig1  40472  dignn0flhalflem2  40480
  Copyright terms: Public domain W3C validator