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

Theorem 1nn0 10707
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 10445 . 2  |-  1  e.  NN
21nnnn0i 10699 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   1c1 9395   NN0cn0 10691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-1cn 9452
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-om 6588  df-recs 6943  df-rdg 6977  df-nn 10435  df-n0 10692
This theorem is referenced by:  peano2nn0  10732  numsucc  10893  numadd  10901  numaddc  10902  6p5lem  10916  6p6e12  10918  7p5e12  10920  8p4e12  10924  9p2e11  10929  9p3e12  10930  10p10e20  10937  4t4e16  10940  5t4e20  10942  6t3e18  10945  6t4e24  10946  7t3e21  10950  7t4e28  10951  8t3e24  10956  9t3e27  10963  9t9e81  10969  4fvwrd4  11651  fzo0ss1  11697  fzo0sn0fzo1  11735  injresinjlem  11756  expn1  11993  nn0expcl  11997  sqval  12043  nn0opthlem1  12164  fac2  12175  faclbnd4lem2  12188  bcn1  12207  bcpasc  12215  bccl  12216  hashsng  12254  hashen1  12255  hashrabrsn  12256  hashprlei  12296  hashtplei  12304  swrd0len0  12448  swrdtrcfv  12456  swrdccatwrd  12481  wrdeqs1cat  12488  repsw1  12540  cshw1  12575  s3fv1  12635  repsw2  12669  repsw3  12670  bcxmas  13417  climcndslem2  13432  climcnds  13433  arisum  13441  geoisum1  13458  geoisum1c  13459  mertenslem2  13464  ege2le3  13494  ef4p  13516  efgt1p2  13517  efgt1p  13518  sin01gt0  13593  rpnnen2lem3  13618  dvds1  13700  bitsmod  13751  bitsinv1lem  13756  sadadd2lem  13774  sadadd  13782  sadass  13786  smupp1  13795  smumul  13808  dfphi2  13968  reumodprminv  13991  pcelnn  14055  pockthg  14086  vdwlem12  14172  dec5nprm  14214  dec2nprm  14215  modxp1i  14218  2exp6  14234  2exp8  14235  2exp16  14236  2expltfac  14238  5prm  14255  11prm  14261  13prm  14262  17prm  14263  19prm  14264  23prm  14265  prmlem2  14266  37prm  14267  43prm  14268  83prm  14269  139prm  14270  163prm  14271  317prm  14272  631prm  14273  1259lem1  14274  1259lem2  14275  1259lem3  14276  1259lem4  14277  1259lem5  14278  1259prm  14279  2503lem1  14280  2503lem2  14281  2503lem3  14282  2503prm  14283  4001lem1  14284  4001lem2  14285  4001lem3  14286  4001lem4  14287  4001prm  14288  ocndx  14459  ocid  14460  dsndx  14461  dsid  14462  unifndx  14463  unifid  14464  odrngstr  14465  ressds  14472  homndx  14473  homid  14474  ccondx  14475  ccoid  14476  resshom  14477  ressco  14478  imasvalstr  14510  prdsvalstr  14511  oppchomfval  14773  oppcbas  14777  rescbas  14862  rescco  14865  rescabs  14866  catstr  14987  ipostr  15443  psgnunilem2  16121  odcau  16225  efgsp1  16356  efgsres  16357  efgredlemd  16363  efgredlem  16366  lt6abl  16493  mgpds  16724  srads  17391  mvridlemOLD  17617  mvrid  17621  mvrf1  17623  mplcoe3  17670  mplcoe3OLD  17671  psrbagsn  17702  evlslem1  17726  cnfldstr  17946  nn0srg  18007  thlbas  18247  thlle  18248  ressunif  19970  tuslem  19975  tmslem  20190  dscmet  20298  tnglem  20359  iblcnlem1  21399  dveflem  21585  c1lip2  21604  ply1remlem  21768  fta1glem1  21771  fta1blem  21774  plyid  21811  coeidp  21864  dgrid  21865  dvply1  21884  vieta1lem2  21911  vieta1  21912  aalioulem3  21934  aaliou2b  21941  dvtaylp  21969  taylthlem1  21972  taylthlem2  21973  radcnvlem2  22013  dvradcnv  22020  pserdvlem2  22027  logtayllem  22238  logtayl  22239  cxp1  22250  dcubic1lem  22372  dcubic2  22373  mcubic  22376  quart1cl  22383  quart1lem  22384  quart1  22385  quartlem1  22386  quartlem2  22387  leibpilem2  22470  log2ublem3  22477  log2ub  22478  birthday  22482  basellem5  22556  issqf  22608  ppi2  22642  mumullem2  22652  sqff1o  22654  1sgmprm  22672  ppiublem2  22676  chtublem  22684  logfacbnd3  22696  logexprlim  22698  logfacrlim2  22699  perfectlem1  22702  perfectlem2  22703  bclbnd  22753  bpos1  22756  bposlem6  22762  lgsval  22773  rpvmasumlem  22870  log2sumbnd  22927  itvndx  23034  lngndx  23035  itvid  23036  lngid  23037  trkgstr  23038  ttgval  23274  ttglem  23275  ttgbas  23276  ttgds  23280  eengstr  23379  usgraex1elv  23468  cusgrasizeindb1  23532  redwlklem  23657  redwlk  23658  usgrcyclnl2  23680  3v3e3cycl1  23683  constr3pthlem3  23696  4cycl4v4e  23705  4cycl4dv  23706  konigsberg  23761  1kp2ke3k  23806  omndmul2  26321  nexple  26594  oddpwdc  26882  eulerpartlemd  26894  eulerpartlemgs2  26908  eulerpartlemn  26909  iwrdsplit  26915  fib0  26927  fib1  26928  fibp1  26929  ballotlemfrci  27055  ballotlemfrceq  27056  sgnmulsgn  27077  sgnmulsgp  27078  plymulx0  27093  signstfveq0  27123  signsvvf  27125  signsvfn  27128  signshlen  27136  lgamcvg2  27186  gamp1  27189  subfac1  27211  kur14lem9  27247  relexpsucr  27477  rtrclreclem.subset  27492  fprodnn0cl  27615  nn0risefaccl  27670  bpoly1  28339  bpoly3  28346  bpoly4  28347  fsumcube  28348  nn0prpw  28667  pell1qr1  29361  rmspecfund  29399  jm2.23  29494  jm2.27c  29505  itgpowd  29739  areaquad  29741  wallispilem2  30010  wallispilem5  30013  wallispi2lem2  30016  stirlinglem5  30022  stirlinglem7  30024  stirlinglem10  30027  stirlinglem11  30028  wwlktovf  30400  ccatw2s1p2  30419  usgra2pthlem1  30449  usg2cwwkdifex  30644  rusgranumwlkl1  30708  rusgranumwlkb1  30721  0rngnnzr  30927  pmatcollpw3fi1lem1  31274  chfacfscmulgsum  31347  chfacfpmmulfsupp  31350  chfacfpmmulgsum  31351  chfacfpmmulgsum2  31352  cpmadugsumlemB  31361  cpmadugsumlemF  31363
  Copyright terms: Public domain W3C validator