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

Theorem 1nn0 11901
Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
1nn0 1 ∈ ℕ0

Proof of Theorem 1nn0
StepHypRef Expression
1 1nn 11637 . 2 1 ∈ ℕ
21nnnn0i 11893 1 1 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10526  0cn0 11885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-1cn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-nn 11627  df-n0 11886
This theorem is referenced by:  peano2nn0  11925  deccl  12101  10nn0  12104  numsucc  12126  numadd  12133  numaddc  12134  11multnc  12154  6p5lem  12156  6p6e12  12160  7p5e12  12163  8p4e12  12168  9p2e11  12173  9p3e12  12174  10p10e20  12181  4t4e16  12185  5t2e10  12186  5t4e20  12188  6t3e18  12191  6t4e24  12192  7t3e21  12196  7t4e28  12197  8t3e24  12202  9t3e27  12209  9t9e81  12215  xnn0n0n1ge2b  12514  fz0to3un2pr  12997  elfzom1elp1fzo  13092  fzo0sn0fzo1  13114  fldiv4lem1div2  13195  expn1  13427  nn0expcl  13431  sqval  13469  nn0opthlem1  13616  fac2  13627  faclbnd4lem2  13642  bccl  13670  hashsng  13718  hashen1  13719  hashrabrsn  13721  1elfz0hash  13739  hashgt23el  13773  hashprlei  13814  hashtplei  13830  wrdred1hash  13901  pfx1  14053  repsw1  14133  cshw1  14172  s3fv1  14242  s4fv1  14246  pfx2  14297  repsw2  14300  repsw3  14301  wwlktovf  14308  relexp1g  14373  relexpaddg  14400  rtrclreclem2  14406  bcxmas  15178  climcndslem2  15193  climcnds  15194  arisum  15203  geoisum1  15223  geoisum1c  15224  mertenslem2  15229  fprodnn0cl  15299  nn0risefaccl  15364  bpoly1  15393  bpoly4  15401  fsumcube  15402  ege2le3  15431  ef4p  15454  efgt1p2  15455  efgt1p  15456  sin01gt0  15531  rpnnen2lem3  15557  dvds1  15657  3dvds2dec  15670  bitsmod  15773  bitsinv1lem  15778  sadadd2lem  15796  sadadd  15804  sadass  15808  smupp1  15817  smumul  15830  pcelnn  16194  pockthg  16230  vdwlem12  16316  prmo1  16361  dec5nprm  16390  dec2nprm  16391  modxp1i  16394  2exp8  16411  2exp16  16412  2expltfac  16414  5prm  16430  11prm  16436  13prm  16437  17prm  16438  19prm  16439  23prm  16440  prmlem2  16441  37prm  16442  43prm  16443  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  1259prm  16457  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  ocndx  16661  ocid  16662  dsndx  16663  dsid  16664  unifndx  16665  unifid  16666  odrngstr  16667  ressds  16674  homndx  16675  homid  16676  ccondx  16677  ccoid  16678  resshom  16679  ressco  16680  slotsbhcdif  16681  imasvalstr  16713  prdsvalstr  16714  oppchomfval  16972  oppcbas  16976  rescbas  17087  rescco  17090  rescabs  17091  catstr  17215  ipostr  17751  cycsubmcl  18282  psgnunilem2  18552  odcau  18658  lt6abl  18944  mgpds  19178  srads  19887  0ringnnzr  19970  mvrid  20131  mvrf1  20133  mplcoe3  20175  psrbagsn  20203  evlslem1  20223  cnfldstr  20475  cnfldfun  20485  nn0srg  20543  thlbas  20768  thlle  20769  pmatcollpw3fi1lem1  21322  chfacfscmulgsum  21396  chfacfpmmulfsupp  21399  chfacfpmmulgsum  21400  chfacfpmmulgsum2  21401  cpmadugsumlemB  21410  cpmadugsumlemF  21412  ressunif  22798  tuslem  22803  tmslem  23019  dscmet  23109  tnglem  23176  ehl1eudis  23950  dveflem  24503  c1lip2  24522  ply1remlem  24683  fta1glem1  24686  fta1blem  24689  plyid  24726  coeidp  24780  dgrid  24781  vieta1lem2  24827  vieta1  24828  aalioulem3  24850  aaliou2b  24857  dvtaylp  24885  taylthlem1  24888  taylthlem2  24889  radcnvlem2  24929  dvradcnv  24936  pserdvlem2  24943  logtayllem  25169  logtayl  25170  cxp1  25181  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  quartlem2  25363  leibpilem2  25446  log2ublem3  25453  log2ub  25454  birthday  25459  lgamcvg2  25559  gamp1  25562  issqf  25640  ppi2  25674  mumullem2  25684  sqff1o  25686  1sgmprm  25702  ppiublem2  25706  chtublem  25714  logfacbnd3  25726  logexprlim  25728  logfacrlim2  25729  perfectlem1  25732  perfectlem2  25733  bclbnd  25783  bpos1  25786  bposlem6  25792  lgsval  25804  2lgslem3a  25899  2lgslem3c  25901  rpvmasumlem  25990  log2sumbnd  26047  itvndx  26153  lngndx  26154  itvid  26155  lngid  26156  trkgstr  26157  ttgval  26588  ttglem  26589  ttgbas  26590  ttgds  26594  eengstr  26693  edgfid  26703  edgfndxnn  26704  edgfndxid  26705  baseltedgf  26706  usgrexmplef  26968  cusgrsizeindb1  27159  wlk1ewlk  27348  usgr2pthlem  27471  uspgrn2crct  27513  crctcshwlkn0lem5  27519  rusgrnumwwlkl1  27674  rusgrnumwwlkb1  27678  clwwlkccatlem  27694  clwwlkinwwlk  27745  umgr2cwwkdifex  27771  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  konigsbergiedgw  27954  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960  konigsberglem4  27961  1kp2ke3k  28152  ex-exp  28156  ex-fac  28157  9p10ne21  28176  prmdvdsbc  30458  dpmul4  30517  threehalves  30518  1mhdrd  30519  s2f1  30548  omndmul2  30640  cycpm2tr  30688  freshmansdream  30786  drngdimgt0  30915  lmat22e12  30983  lmat22e21  30984  lmat22e22  30985  madjusmdetlem4  30994  nexple  31167  oddpwdc  31511  eulerpartlemd  31523  eulerpartlemgs2  31537  eulerpartlemn  31538  iwrdsplit  31544  fib0  31556  fib1  31557  fibp1  31558  sgnmulsgn  31706  sgnmulsgp  31707  plymulx0  31716  signstfveq0  31746  signsvvf  31748  signsvfn  31751  signshlen  31759  prodfzo03  31773  reprsuc  31785  breprexplemc  31802  hgt750lemd  31818  hgt750lem  31821  hgt750lem2  31822  hgt750leme  31828  usgrgt2cycl  32274  subfac1  32322  kur14lem9  32358  bccolsum  32868  nn0prpw  33568  235t711  39055  ex-decpmul  39056  nn0rppwr  39060  fltnltalem  39152  3cubeslem3l  39161  3cubeslem3r  39162  pell1qr1  39346  rmspecfund  39384  jm2.23  39471  jm2.27c  39482  itgpowd  39699  areaquad  39701  brfvidRP  39911  brfvrcld  39914  corclrcl  39930  dftrcl3  39943  dfrtrcl3  39956  fvrtrcllb1d  39960  corcltrcl  39962  cotrclrcl  39965  inductionexd  40383  radcnvrat  40523  binomcxplemnn0  40558  binomcxplemfrat  40560  binomcxplemnotnn0  40565  wallispilem2  42228  wallispilem5  42231  wallispi2lem2  42234  stirlinglem5  42240  stirlinglem7  42242  stirlinglem10  42245  stirlinglem11  42246  fourierdlem48  42316  iccpartigtl  43460  iccpartlt  43461  iccpartgel  43466  fmtnosqrt  43578  fmtno1  43580  fmtno2  43589  fmtno5lem1  43592  fmtno5lem2  43593  fmtno5lem3  43594  fmtno5lem4  43595  fmtno5  43596  257prm  43600  fmtnofac1  43609  fmtno4prmfac  43611  fmtno4prmfac193  43612  fmtno4nprmfac193  43613  fmtno5faclem1  43618  fmtno5faclem2  43619  fmtno5faclem3  43620  fmtno5fac  43621  fmtno5nprm  43622  3ndvds4  43635  139prmALT  43636  31prm  43637  m5prm  43638  127prm  43640  m7prm  43641  2exp11  43642  m11nprm  43643  lighneallem2  43648  perfectALTVlem1  43763  perfectALTVlem2  43764  11t31e341  43774  2exp340mod341  43775  341fppr2  43776  8exp8mod9  43778  nfermltl8rev  43784  nfermltl2rev  43785  evengpoap3  43841  nnsum4primesevenALTV  43843  bgoldbtbndlem1  43847  bgoldbachlt  43855  tgblthelfgott  43857  smndex2dnrinv  44015  nnpw2pmod  44571  dig1  44596  dignn0flhalflem2  44604
  Copyright terms: Public domain W3C validator