Theorem 1nn0 12418

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	⊢ 1 ∈ ℕ0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 12157	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 12410	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2109  1c1 11029  ℕ₀cn0 12402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147  df-n0 12403

This theorem is referenced by:  peano2nn0  12442  deccl  12624  10nn0  12627  numsucc  12649  numadd  12656  numaddc  12657  11multnc  12677  6p5lem  12679  6p6e12  12683  7p5e12  12686  8p4e12  12691  9p2e11  12696  9p3e12  12697  10p10e20  12704  4t4e16  12708  5t2e10  12709  5t4e20  12711  6t3e18  12714  6t4e24  12715  7t3e21  12719  7t4e28  12720  8t3e24  12725  9t3e27  12732  9t9e81  12738  xnn0n0n1ge2b  13052  fz0to3un2pr  13550  elfzom1elp1fzo  13653  fzo0sn0fzo1  13676  fvf1tp  13711  fldiv4lem1div2  13759  expn1  13996  nn0expcl  14000  sqval  14039  nn0opthlem1  14193  fac2  14204  faclbnd4lem2  14219  bccl  14247  hashsng  14294  hashen1  14295  hashrabrsn  14297  1elfz0hash  14315  hashgt23el  14349  hashprlei  14393  hashtplei  14409  tpf1ofv1  14422  tpfo  14425  wrdred1hash  14486  pfx1  14627  repsw1  14707  cshw1  14746  s3fv1  14817  s4fv1  14821  pfx2  14872  repsw2  14875  repsw3  14876  wwlktovf  14881  relexp1g  14951  relexpaddg  14978  rtrclreclem1  14982  bcxmas  15760  climcndslem2  15775  climcnds  15776  arisum  15785  geoisum1  15804  geoisum1c  15805  mertenslem2  15810  fprodnn0cl  15882  nn0risefaccl  15947  bpoly1  15976  bpoly4  15984  fsumcube  15985  ege2le3  16015  ef4p  16040  efgt1p2  16041  efgt1p  16042  sin01gt0  16117  rpnnen2lem3  16143  dvds1  16248  3dvds2dec  16262  5ndvds6  16343  bitsmod  16365  bitsinv1lem  16370  sadadd2lem  16388  sadadd  16396  sadass  16400  smupp1  16409  smumul  16422  nn0rppwr  16490  prmdvdsbc  16655  pcelnn  16800  pockthg  16836  vdwlem12  16922  prmo1  16967  dec5nprm  16996  dec2nprm  16997  modxp1i  17000  2exp8  17018  2exp11  17019  2exp16  17020  2expltfac  17022  5prm  17038  11prm  17044  13prm  17045  17prm  17046  19prm  17047  23prm  17048  prmlem2  17049  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  ocndx  17303  ocid  17304  basendxnocndx  17305  plendxnocndx  17306  dsndx  17307  dsid  17308  dsndxnn  17309  basendxltdsndx  17310  slotsdifdsndx  17316  unifndx  17317  unifid  17318  unifndxnn  17319  basendxltunifndx  17320  slotsdifunifndx  17323  odrngstr  17325  homndx  17333  homid  17334  ccondx  17335  ccoid  17336  slotsbhcdif  17337  slotsdifplendx2  17338  slotsdifocndx  17339  imasvalstr  17373  prdsvalstr  17374  catstr  17885  ipostr  18453  smndex2dnrinv  18807  cycsubmcl  19098  psgnunilem2  19392  odcau  19501  lt6abl  19792  omndmul2  20030  0ringnnzr  20428  cnfldstr  21281  cnfldstrOLD  21296  nn0srg  21362  freshmansdream  21499  mvrid  21909  mvrf1  21911  mplcoe3  21961  psrbagsn  21986  evlslem1  22005  mhpvarcl  22051  psdcl  22064  psdmul  22069  psdmvr  22072  pmatcollpw3fi1lem1  22689  chfacfscmulgsum  22763  chfacfpmmulfsupp  22766  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cpmadugsumlemB  22777  cpmadugsumlemF  22779  dscmet  24476  ehl1eudis  25336  dveflem  25899  c1lip2  25919  itgpowd  25973  ply1remlem  26086  fta1glem1  26089  fta1blem  26092  plyid  26130  coeidp  26185  dgrid  26186  vieta1lem2  26235  vieta1  26236  aalioulem3  26258  aaliou2b  26265  dvtaylp  26294  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  radcnvlem2  26339  dvradcnv  26346  pserdvlem2  26354  logtayllem  26584  logtayl  26585  cxp1  26596  quart1cl  26780  quart1lem  26781  quart1  26782  quartlem1  26783  quartlem2  26784  leibpilem2  26867  log2ublem3  26874  log2ub  26875  birthday  26880  lgamcvg2  26981  gamp1  26984  issqf  27062  ppi2  27096  mumullem2  27106  sqff1o  27108  1sgmprm  27126  ppiublem2  27130  chtublem  27138  logfacbnd3  27150  logexprlim  27152  logfacrlim2  27153  perfectlem1  27156  perfectlem2  27157  bclbnd  27207  bpos1  27210  bposlem6  27216  lgsval  27228  2lgslem3a  27323  2lgslem3c  27325  rpvmasumlem  27414  log2sumbnd  27471  itvndx  28400  lngndx  28401  itvid  28402  lngid  28403  slotsinbpsd  28404  slotslnbpsd  28405  lngndxnitvndx  28406  trkgstr  28407  eengstr  28943  edgfid  28953  edgfndx  28954  edgfndxnn  28955  basendxltedgfndx  28957  usgrexmplef  29222  cusgrsizeindb1  29414  wlk1ewlk  29603  usgr2pthlem  29726  uspgrn2crct  29771  crctcshwlkn0lem5  29777  rusgrnumwwlkl1  29931  rusgrnumwwlkb1  29935  clwwlkccatlem  29951  clwwlkinwwlk  30002  umgr2cwwkdifex  30027  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  konigsbergiedgw  30210  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  konigsberglem4  30217  1kp2ke3k  30408  ex-exp  30412  ex-fac  30413  9p10ne21  30432  sgnmulsgn  32800  sgnmulsgp  32801  nexple  32802  dpmul4  32867  threehalves  32868  1mhdrd  32869  s2f1  32899  cycpm2tr  33074  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  ply1dg1rt  33527  coe1vr1  33536  deg1vr  33537  drngdimgt0  33593  rtelextdg2lem  33695  fldext2chn  33697  constrdircl  33734  iconstr  33735  2sqr3minply  33749  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  cos9thpiminply  33757  lmat22e12  33788  lmat22e21  33789  lmat22e22  33790  madjusmdetlem4  33799  oddpwdc  34324  eulerpartlemd  34336  eulerpartlemgs2  34350  eulerpartlemn  34351  iwrdsplit  34357  fib0  34369  fib1  34370  fibp1  34371  plymulx0  34517  signstfveq0  34547  signsvvf  34549  signsvfn  34552  signshlen  34560  prodfzo03  34573  reprsuc  34585  breprexplemc  34602  hgt750lemd  34618  hgt750lem  34621  hgt750lem2  34622  hgt750leme  34628  usgrgt2cycl  35105  subfac1  35153  kur14lem9  35189  bccolsum  35714  nn0prpw  36299  12gcd5e1  41979  60gcd6e6  41980  60gcd7e1  41981  420gcd8e4  41982  12lcm5e60  41984  lcmineqlem11  42015  lcmineqlem18  42022  lcmineqlem22  42026  lcmineqlem  42028  3exp7  42029  3lexlogpow5ineq1  42030  3lexlogpow5ineq2  42031  3lexlogpow5ineq4  42032  3lexlogpow5ineq5  42036  dvrelogpow2b  42044  aks4d1p1p2  42046  aks4d1p1p4  42047  aks4d1p1p6  42049  aks4d1p1p7  42050  aks4d1p1p5  42051  aks4d1p1  42052  aks4d1p3  42054  aks6d1c1p8  42091  aks6d1c5lem3  42113  2np3bcnp1  42120  2ap1caineq  42121  sticksstones22  42144  aks6d1c6lem1  42146  aks6d1c7lem1  42156  aks6d1c7  42160  235t711  42281  ex-decpmul  42282  fltnltalem  42638  sum9cubes  42648  3cubeslem3l  42662  3cubeslem3r  42663  pell1qr1  42847  rmspecfund  42885  jm2.23  42972  jm2.27c  42983  areaquad  43192  resqrtvalex  43621  imsqrtvalex  43622  brfvidRP  43664  brfvrcld  43667  corclrcl  43683  dftrcl3  43696  dfrtrcl3  43709  fvrtrcllb1d  43713  corcltrcl  43715  cotrclrcl  43718  inductionexd  44131  radcnvrat  44290  binomcxplemnn0  44325  binomcxplemfrat  44327  binomcxplemnotnn0  44332  rexanuz2nf  45475  wallispilem2  46051  wallispilem5  46054  wallispi2lem2  46057  stirlinglem5  46063  stirlinglem7  46065  stirlinglem10  46068  stirlinglem11  46069  fourierdlem48  46139  ormkglobd  46860  iccpartigtl  47411  iccpartlt  47412  iccpartgel  47417  fmtnosqrt  47527  fmtno1  47529  fmtno2  47538  fmtno5lem1  47541  fmtno5lem2  47542  fmtno5lem3  47543  fmtno5lem4  47544  fmtno5  47545  257prm  47549  fmtnofac1  47558  fmtno4prmfac  47560  fmtno4prmfac193  47561  fmtno4nprmfac193  47562  fmtno5faclem1  47567  fmtno5faclem2  47568  fmtno5faclem3  47569  fmtno5fac  47570  fmtno5nprm  47571  3ndvds4  47583  139prmALT  47584  31prm  47585  m5prm  47586  127prm  47587  m7prm  47588  m11nprm  47589  lighneallem2  47594  perfectALTVlem1  47709  perfectALTVlem2  47710  11t31e341  47720  2exp340mod341  47721  341fppr2  47722  8exp8mod9  47724  nfermltl8rev  47730  nfermltl2rev  47731  evengpoap3  47787  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  bgoldbachlt  47801  tgblthelfgott  47803  cycl3grtri  47935  stgr1  47949  usgrexmpl1lem  48009  usgrexmpl2lem  48014  gpgprismgriedgdmss  48040  gpgprismgr4cycllem3  48085  gpgprismgr4cycllem7  48089  gpgprismgr4cycllem9  48091  gpgprismgr4cycllem10  48092  grlimedgnedg  48119  nnpw2pmod  48572  dig1  48597  dignn0flhalflem2  48605  1aryfvalel  48625  itcoval1  48652  itcoval2  48653  ackval1  48670  ackval2  48671  ackval3  48672  ackendofnn0  48673  ackvalsucsucval  48677  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval41a  48683  ackval42  48685