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

Theorem 1nn0 11155
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 10878 . 2 1 ∈ ℕ
21nnnn0i 11147 1 1 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  1c1 9793  0cn0 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-1cn 9850
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10868  df-n0 11140
This theorem is referenced by:  peano2nn0  11180  deccl  11344  10nn0  11348  numsucc  11381  numadd  11392  numaddc  11393  11multnc  11424  6p5lem  11427  6p6e12  11434  7p5e12  11439  8p4e12  11446  9p2e11  11451  9p2e11OLD  11452  9p3e12  11453  10p10e20  11460  10p10e20OLD  11461  4t4e16  11465  5t2e10  11466  5t4e20  11469  5t4e20OLD  11470  6t3e18  11474  6t4e24  11475  7t3e21  11481  7t4e28  11482  8t3e24  11487  9t3e27  11496  9t9e81  11502  fz0to3un2pr  12265  elfzom1elp1fzo  12357  fzo0sn0fzo1  12379  fldiv4lem1div2  12455  expn1  12687  nn0expcl  12691  sqval  12739  sq10  12865  nn0opthlem1  12872  fac2  12883  faclbnd4lem2  12898  bccl  12926  hashsng  12972  hashen1  12973  hashrabrsn  12974  1elfz0hash  12992  hashprlei  13059  hashtplei  13070  swrd0len0  13234  swrdtrcfv  13239  swrdccatwrd  13266  wrdeqs1cat  13272  repsw1  13327  cshw1  13365  s3fv1  13433  s4fv1  13437  repsw2  13487  repsw3  13488  wwlktovf  13493  relexp1g  13560  relexpaddg  13587  rtrclreclem2  13593  bcxmas  14352  climcndslem2  14367  climcnds  14368  arisum  14377  geoisum1  14395  geoisum1c  14396  mertenslem2  14402  fprodnn0cl  14472  nn0risefaccl  14538  bpoly1  14567  bpoly4  14575  fsumcube  14576  ege2le3  14605  ef4p  14628  efgt1p2  14629  efgt1p  14630  sin01gt0  14705  rpnnen2lem3  14730  dvds1  14825  3dvds2dec  14840  3dvds2decOLD  14841  bitsmod  14942  bitsinv1lem  14947  sadadd2lem  14965  sadadd  14973  sadass  14977  smupp1  14986  smumul  14999  pcelnn  15358  pockthg  15394  vdwlem12  15480  prmo1  15525  dec5nprm  15554  dec2nprm  15555  modxp1i  15558  2exp8  15580  2exp16  15581  2expltfac  15583  5prm  15599  11prm  15606  13prm  15607  17prm  15608  19prm  15609  23prm  15610  prmlem2  15611  37prm  15612  43prm  15613  83prm  15614  139prm  15615  163prm  15616  317prm  15617  631prm  15618  1259lem1  15622  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  2503prm  15631  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  4001prm  15636  ocndx  15829  ocid  15830  dsndx  15831  dsid  15832  unifndx  15833  unifid  15834  odrngstr  15835  ressds  15842  homndx  15843  homid  15844  ccondx  15845  ccoid  15846  resshom  15847  ressco  15848  slotsbhcdif  15849  imasvalstr  15881  prdsvalstr  15882  oppchomfval  16143  oppcbas  16147  rescbas  16258  rescco  16261  rescabs  16262  catstr  16386  ipostr  16922  psgnunilem2  17684  odcau  17788  lt6abl  18065  mgpds  18268  srads  18953  0ringnnzr  19036  mvrid  19190  mvrf1  19192  mplcoe3  19233  psrbagsn  19262  evlslem1  19282  cnfldstr  19515  nn0srg  19581  thlbas  19801  thlle  19802  pmatcollpw3fi1lem1  20352  chfacfscmulgsum  20426  chfacfpmmulfsupp  20429  chfacfpmmulgsum  20430  chfacfpmmulgsum2  20431  cpmadugsumlemB  20440  cpmadugsumlemF  20442  ressunif  21818  tuslem  21823  tmslem  22038  dscmet  22128  tnglem  22192  dveflem  23463  c1lip2  23482  ply1remlem  23643  fta1glem1  23646  fta1blem  23649  plyid  23686  coeidp  23740  dgrid  23741  vieta1lem2  23787  vieta1  23788  aalioulem3  23810  aaliou2b  23817  dvtaylp  23845  taylthlem1  23848  taylthlem2  23849  radcnvlem2  23889  dvradcnv  23896  pserdvlem2  23903  logtayllem  24122  logtayl  24123  cxp1  24134  dcubic1lem  24287  dcubic2  24288  mcubic  24291  quart1cl  24298  quart1lem  24299  quart1  24300  quartlem1  24301  quartlem2  24302  leibpilem2  24385  log2ublem3  24392  log2ub  24393  birthday  24398  lgamcvg2  24498  gamp1  24501  issqf  24579  ppi2  24613  mumullem2  24623  sqff1o  24625  1sgmprm  24641  ppiublem2  24645  chtublem  24653  logfacbnd3  24665  logexprlim  24667  logfacrlim2  24668  perfectlem1  24671  perfectlem2  24672  bclbnd  24722  bpos1  24725  bposlem6  24731  lgsval  24743  2lgslem3a  24838  2lgslem3c  24840  rpvmasumlem  24893  log2sumbnd  24950  itvndx  25056  lngndx  25057  itvid  25058  lngid  25059  trkgstr  25060  ttgval  25473  ttglem  25474  ttgbas  25475  ttgds  25479  eengstr  25578  usgraex1elv  25691  cusgrasizeindb1  25766  redwlklem  25901  usgrcyclnl2  25935  3v3e3cycl1  25938  4cycl4v4e  25960  4cycl4dv  25961  usg2cwwkdifex  26115  rusgranumwlkl1  26240  rusgranumwlkb1  26247  1kp2ke3k  26461  ex-exp  26465  ex-fac  26466  omndmul2  28849  lmat22e12  29019  lmat22e21  29020  lmat22e22  29021  madjusmdetlem4  29030  nexple  29205  oddpwdc  29549  eulerpartlemd  29561  eulerpartlemgs2  29575  eulerpartlemn  29576  iwrdsplit  29582  fib0  29594  fib1  29595  fibp1  29596  sgnmulsgn  29744  sgnmulsgp  29745  plymulx0  29756  signstfveq0  29786  signsvvf  29788  signsvfn  29791  signshlen  29799  subfac1  30220  kur14lem9  30256  bccolsum  30684  nn0prpw  31294  pell1qr1  36249  rmspecfund  36288  jm2.23  36377  jm2.27c  36388  itgpowd  36615  areaquad  36617  brfvidRP  36795  brfvrcld  36798  corclrcl  36814  dftrcl3  36827  dfrtrcl3  36840  fvrtrcllb1d  36844  corcltrcl  36846  cotrclrcl  36849  inductionexd  37269  radcnvrat  37331  binomcxplemnn0  37366  binomcxplemfrat  37368  binomcxplemnotnn0  37373  wallispilem2  38756  wallispilem5  38759  wallispi2lem2  38762  stirlinglem5  38768  stirlinglem7  38770  stirlinglem10  38773  stirlinglem11  38774  fourierdlem48  38844  iccpartigtl  39759  iccpartlt  39760  iccpartgel  39765  fmtnosqrt  39787  fmtno1  39789  fmtno2  39798  fmtno5lem1  39801  fmtno5lem2  39802  fmtno5lem3  39803  fmtno5lem4  39804  fmtno5  39805  257prm  39809  fmtnofac1  39818  fmtno4prmfac  39820  fmtno4prmfac193  39821  fmtno4nprmfac193  39822  fmtno5faclem1  39827  fmtno5faclem2  39828  fmtno5faclem3  39829  fmtno5fac  39830  fmtno5nprm  39831  3ndvds4  39846  139prmALT  39847  31prm  39848  m5prm  39849  127prm  39851  m7prm  39852  2exp11  39853  m11nprm  39854  lighneallem2  39859  perfectALTVlem1  39962  perfectALTVlem2  39963  evengpoap3  40013  nnsum4primesevenALTV  40015  bgoldbtbndlem1  40019  bgoldbachlt  40025  tgblthelfgott  40027  bgoldbachltOLD  40032  tgblthelfgottOLD  40034  wrdred1hash  40039  pfx1  40072  pfx2  40073  xnn0n0n1ge2b  40211  edgfndxnn  40220  edgfndxid  40221  baseltedgf  40222  struct2griedg  40256  uhgrstrrepe  40299  cusgrsizeindb1  40661  1wlk1ewlk  40839  usgr2pthlem  40964  uspgrn2crct  41006  crctcsh1wlkn0lem5  41012  rusgrnumwwlkl1  41167  rusgrnumwwlkb1  41170  umgr2cwwkdifex  41244  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  konigsbergiedgw  41411  konigsbergiedgwOLD  41412  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419  konigsberglem4  41420  nnpw2pmod  42170  dig1  42195  dignn0flhalflem2  42203
  Copyright terms: Public domain W3C validator