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

Theorem 1nn0 10812
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 10548 . 2  |-  1  e.  NN
21nnnn0i 10804 1  |-  1  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802   1c1 9491   NN0cn0 10796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-1cn 9548
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-om 6682  df-recs 7040  df-rdg 7074  df-nn 10538  df-n0 10797
This theorem is referenced by:  peano2nn0  10837  numsucc  11005  numadd  11013  numaddc  11014  6p5lem  11028  6p6e12  11030  7p5e12  11032  8p4e12  11036  9p2e11  11041  9p3e12  11042  10p10e20  11049  4t4e16  11052  5t4e20  11054  6t3e18  11057  6t4e24  11058  7t3e21  11062  7t4e28  11063  8t3e24  11068  9t3e27  11075  9t9e81  11081  elfzom1elp1fzo  11857  fzo0sn0fzo1  11876  expn1  12150  nn0expcl  12154  sqval  12201  nn0opthlem1  12322  fac2  12333  faclbnd4lem2  12346  bccl  12374  hashsng  12412  hashen1  12413  hashrabrsn  12414  hashprlei  12488  hashtplei  12496  ccatw2s1p2  12615  swrd0len0  12634  swrdtrcfv  12642  swrdccatwrd  12667  wrdeqs1cat  12674  repsw1  12729  cshw1  12764  s3fv1  12828  repsw2  12862  repsw3  12863  wwlktovf  12868  bcxmas  13621  climcndslem2  13636  climcnds  13637  arisum  13645  geoisum1  13662  geoisum1c  13663  mertenslem2  13668  ege2le3  13698  ef4p  13720  efgt1p2  13721  efgt1p  13722  sin01gt0  13797  rpnnen2lem3  13822  dvds1  13906  bitsmod  13958  bitsinv1lem  13963  sadadd2lem  13981  sadadd  13989  sadass  13993  smupp1  14002  smumul  14015  pcelnn  14265  pockthg  14296  vdwlem12  14382  dec5nprm  14424  dec2nprm  14425  modxp1i  14428  2exp6OLD  14444  2exp8  14446  2exp16  14447  2expltfac  14449  5prm  14466  11prm  14472  13prm  14473  17prm  14474  19prm  14475  23prm  14476  prmlem2  14477  37prm  14478  43prm  14479  83prm  14480  139prm  14481  163prm  14482  317prm  14483  631prm  14484  1259lem1  14485  1259lem2  14486  1259lem3  14487  1259lem4  14488  1259lem5  14489  1259prm  14490  2503lem1  14491  2503lem2  14492  2503lem3  14493  2503prm  14494  4001lem1  14495  4001lem2  14496  4001lem3  14497  4001lem4  14498  4001prm  14499  ocndx  14670  ocid  14671  dsndx  14672  dsid  14673  unifndx  14674  unifid  14675  odrngstr  14676  ressds  14683  homndx  14684  homid  14685  ccondx  14686  ccoid  14687  resshom  14688  ressco  14689  imasvalstr  14721  prdsvalstr  14722  oppchomfval  14981  oppcbas  14985  rescbas  15070  rescco  15073  rescabs  15074  catstr  15195  ipostr  15652  psgnunilem2  16389  odcau  16493  lt6abl  16766  mgpds  17019  srads  17700  0ringnnzr  17785  mvridlemOLD  17943  mvrid  17947  mvrf1  17949  mplcoe3  17996  mplcoe3OLD  17997  psrbagsn  18028  evlslem1  18052  cnfldstr  18290  nn0srg  18354  thlbas  18594  thlle  18595  pmatcollpw3fi1lem1  19154  chfacfscmulgsum  19228  chfacfpmmulfsupp  19231  chfacfpmmulgsum  19232  chfacfpmmulgsum2  19233  cpmadugsumlemB  19242  cpmadugsumlemF  19244  ressunif  20631  tuslem  20636  tmslem  20851  dscmet  20959  tnglem  21020  dveflem  22246  c1lip2  22265  ply1remlem  22429  fta1glem1  22432  fta1blem  22435  plyid  22472  coeidp  22525  dgrid  22526  vieta1lem2  22572  vieta1  22573  aalioulem3  22595  aaliou2b  22602  dvtaylp  22630  taylthlem1  22633  taylthlem2  22634  radcnvlem2  22674  dvradcnv  22681  pserdvlem2  22688  logtayllem  22905  logtayl  22906  cxp1  22917  dcubic1lem  23039  dcubic2  23040  mcubic  23043  quart1cl  23050  quart1lem  23051  quart1  23052  quartlem1  23053  quartlem2  23054  leibpilem2  23137  log2ublem3  23144  log2ub  23145  birthday  23149  issqf  23275  ppi2  23309  mumullem2  23319  sqff1o  23321  1sgmprm  23339  ppiublem2  23343  chtublem  23351  logfacbnd3  23363  logexprlim  23365  logfacrlim2  23366  perfectlem1  23369  perfectlem2  23370  bclbnd  23420  bpos1  23423  bposlem6  23429  lgsval  23440  rpvmasumlem  23537  log2sumbnd  23594  itvndx  23701  lngndx  23702  itvid  23703  lngid  23704  trkgstr  23705  ttgval  24043  ttglem  24044  ttgbas  24045  ttgds  24049  eengstr  24148  usgraex1elv  24262  cusgrasizeindb1  24336  redwlklem  24472  usgrcyclnl2  24506  3v3e3cycl1  24509  4cycl4v4e  24531  4cycl4dv  24532  usg2cwwkdifex  24686  rusgranumwlkl1  24812  rusgranumwlkb1  24819  konigsberg  24852  1kp2ke3k  25032  omndmul2  27568  nexple  27871  oddpwdc  28159  eulerpartlemd  28171  eulerpartlemgs2  28185  eulerpartlemn  28186  iwrdsplit  28192  fib0  28204  fib1  28205  fibp1  28206  sgnmulsgn  28354  sgnmulsgp  28355  plymulx0  28370  signstfveq0  28400  signsvvf  28402  signsvfn  28405  signshlen  28413  lgamcvg2  28463  gamp1  28466  subfac1  28488  kur14lem9  28524  relexpsucr  28919  rtrclreclem.subset  28934  fprodnn0cl  29057  nn0risefaccl  29112  bpoly1  29781  bpoly4  29789  fsumcube  29790  nn0prpw  30109  pell1qr1  30775  rmspecfund  30813  jm2.23  30906  jm2.27c  30917  itgpowd  31151  areaquad  31153  radcnvrat  31164  wallispilem2  31733  wallispilem5  31736  wallispi2lem2  31739  stirlinglem5  31745  stirlinglem7  31747  stirlinglem10  31750  stirlinglem11  31751  fourierdlem48  31822  usgra2pthlem1  32187  uhgrepe  32212  slotsbhcdif  32390  inductionexd  37573
  Copyright terms: Public domain W3C validator