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

Theorem 1nn0 10242
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 10016 . 2  |-  1  e.  NN
21nnnn0i 10234 1  |-  1  e.  NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   1c1 8996   NN0cn0 10226
This theorem is referenced by:  peano2nn0  10265  numsucc  10413  numadd  10421  numaddc  10422  6p5lem  10436  6p6e12  10438  7p5e12  10440  8p4e12  10444  9p2e11  10449  9p3e12  10450  10p10e20  10457  4t4e16  10460  5t4e20  10462  6t3e18  10465  6t4e24  10466  7t3e21  10470  7t4e28  10471  8t3e24  10476  9t3e27  10483  9t9e81  10489  4fvwrd4  11126  injresinjlem  11204  expn1  11396  nn0expcl  11400  sqval  11446  nn0opthlem1  11566  fac2  11577  faclbnd4lem2  11590  bcn1  11609  bcpasc  11617  bccl  11618  hashsng  11652  hashrabrsn  11653  hashprlei  11691  hashtplei  11695  wrdeqs1cat  11794  s3fv1  11858  bcxmas  12620  climcndslem2  12635  climcnds  12636  arisum  12644  geoisum1  12661  geoisum1c  12662  mertenslem2  12667  ege2le3  12697  ef4p  12719  efgt1p2  12720  efgt1p  12721  sin01gt0  12796  rpnnen2lem3  12821  dvds1  12903  bitsfzo  12952  bitsmod  12953  bitsinv1lem  12958  sadadd2lem  12976  sadadd  12984  sadass  12988  smupp1  12997  smumul  13010  dfphi2  13168  pythagtriplem4  13198  pcelnn  13248  pockthg  13279  vdwlem12  13365  dec5nprm  13407  dec2nprm  13408  modxp1i  13411  2exp6  13427  2exp8  13428  2exp16  13429  2expltfac  13431  5prm  13436  11prm  13442  13prm  13443  17prm  13444  19prm  13445  23prm  13446  prmlem2  13447  37prm  13448  43prm  13449  83prm  13450  139prm  13451  163prm  13452  317prm  13453  631prm  13454  1259lem1  13455  1259lem2  13456  1259lem3  13457  1259lem4  13458  1259lem5  13459  1259prm  13460  2503lem1  13461  2503lem2  13462  2503lem3  13463  2503prm  13464  4001lem1  13465  4001lem2  13466  4001lem3  13467  4001lem4  13468  4001prm  13469  ocndx  13633  ocid  13634  dsndx  13635  dsid  13636  unifndx  13637  unifid  13638  odrngstr  13639  ressds  13646  homndx  13647  homid  13648  ccondx  13649  ccoid  13650  resshom  13651  ressco  13652  imasvalstr  13680  prdsvalstr  13681  oppchomfval  13945  oppcbas  13949  rescbas  14034  rescco  14037  rescabs  14038  catstr  14159  ipostr  14584  odcau  15243  efgsp1  15374  efgsres  15375  efgredlemd  15381  efgredlem  15384  lt6abl  15509  mgpds  15663  srads  16262  mvridlem  16488  mvrf1  16494  mplcoe3  16534  psrbagsn  16560  cnfldstr  16710  thlbas  16928  thlle  16929  ressunif  18297  tuslem  18302  tmslem  18517  dscmet  18625  tnglem  18686  iblcnlem1  19682  dveflem  19868  c1lip2  19887  evlslem1  19941  ply1remlem  20090  fta1glem1  20093  fta1blem  20096  plyid  20133  coeidp  20186  dgrid  20187  dvply1  20206  vieta1lem2  20233  vieta1  20234  aalioulem3  20256  aaliou2b  20263  aaliou3lem2  20265  dvtaylp  20291  taylthlem1  20294  taylthlem2  20295  radcnvlem2  20335  dvradcnv  20342  pserdvlem2  20349  logtayllem  20555  logtayl  20556  cxp1  20567  dcubic1lem  20688  dcubic2  20689  mcubic  20692  quart1cl  20699  quart1lem  20700  quart1  20701  quartlem1  20702  quartlem2  20703  leibpilem2  20786  log2ublem3  20793  log2ub  20794  birthday  20798  basellem5  20872  issqf  20924  ppi2  20958  mumullem2  20968  sqff1o  20970  1sgmprm  20988  ppiublem2  20992  chtublem  21000  logfacbnd3  21012  logexprlim  21014  logfacrlim2  21015  perfectlem1  21018  perfectlem2  21019  bclbnd  21069  bpos1  21072  bposlem6  21078  lgsval  21089  rpvmasumlem  21186  log2sumbnd  21243  usgraex1elv  21421  cusgrasizeindb1  21485  redwlklem  21610  redwlk  21611  usgrcyclnl2  21633  3v3e3cycl1  21636  constr3pthlem3  21649  4cycl4v4e  21658  4cycl4dv  21659  konigsberg  21714  1kp2ke3k  21759  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemfrci  24790  ballotlemfrceq  24791  lgamcvg2  24844  gamp1  24847  subfac1  24869  kur14lem9  24905  relexpsucr  25135  rtrclreclem.subset  25150  fprodnn0cl  25288  nn0risefaccl  25343  bpoly1  26102  bpoly3  26109  bpoly4  26110  fsumcube  26111  nn0prpw  26339  mzpsubmpt  26813  pell1qr1  26947  rmspecfund  26985  rmxm1  27010  rmym1  27011  jm2.23  27080  jm2.27c  27091  psgnunilem2  27408  wallispilem2  27804  wallispilem5  27807  wallispi2lem2  27810  stirlinglem5  27816  stirlinglem7  27818  stirlinglem10  27821  stirlinglem11  27822  fzo0ss1  28145  fzo0sn0fzo1  28147  swrd0fv0  28226  swrdtrcfv  28227  reumodprminv  28260  swrd0fvls  28297  cshw1  28308  usgra2pthlem1  28347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-1cn 9053
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-recs 6636  df-rdg 6671  df-nn 10006  df-n0 10227
  Copyright terms: Public domain W3C validator