Theorem 1nn0 12429

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 12168	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 12421	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2114  1c1 11039  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-n0 12414

This theorem is referenced by:  peano2nn0  12453  deccl  12634  10nn0  12637  numsucc  12659  numadd  12666  numaddc  12667  11multnc  12687  6p5lem  12689  6p6e12  12693  7p5e12  12696  8p4e12  12701  9p2e11  12706  9p3e12  12707  10p10e20  12714  4t4e16  12718  5t2e10  12719  5t4e20  12721  6t3e18  12724  6t4e24  12725  7t3e21  12729  7t4e28  12730  8t3e24  12735  9t3e27  12742  9t9e81  12748  xnn0n0n1ge2b  13058  fz0to3un2pr  13557  elfzom1elp1fzo  13660  fzo0sn0fzo1  13683  fvf1tp  13721  fldiv4lem1div2  13769  expn1  14006  nn0expcl  14010  sqval  14049  nn0opthlem1  14203  fac2  14214  faclbnd4lem2  14229  bccl  14257  hashsng  14304  hashen1  14305  hashrabrsn  14307  1elfz0hash  14325  hashgt23el  14359  hashprlei  14403  hashtplei  14419  tpf1ofv1  14432  tpfo  14435  wrdred1hash  14496  pfx1  14638  repsw1  14718  cshw1  14757  s3fv1  14827  s4fv1  14831  pfx2  14882  repsw2  14885  repsw3  14886  wwlktovf  14891  relexp1g  14961  relexpaddg  14988  rtrclreclem1  14992  bcxmas  15770  climcndslem2  15785  climcnds  15786  arisum  15795  geoisum1  15814  geoisum1c  15815  mertenslem2  15820  fprodnn0cl  15892  nn0risefaccl  15957  bpoly1  15986  bpoly4  15994  fsumcube  15995  ege2le3  16025  ef4p  16050  efgt1p2  16051  efgt1p  16052  sin01gt0  16127  rpnnen2lem3  16153  dvds1  16258  3dvds2dec  16272  5ndvds6  16353  bitsmod  16375  bitsinv1lem  16380  sadadd2lem  16398  sadadd  16406  sadass  16410  smupp1  16419  smumul  16432  nn0rppwr  16500  prmdvdsbc  16665  pcelnn  16810  pockthg  16846  vdwlem12  16932  prmo1  16977  dec5nprm  17006  dec2nprm  17007  modxp1i  17010  2exp8  17028  2exp11  17029  2exp16  17030  2expltfac  17032  5prm  17048  11prm  17054  13prm  17055  17prm  17056  19prm  17057  23prm  17058  prmlem2  17059  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  ocndx  17313  ocid  17314  basendxnocndx  17315  plendxnocndx  17316  dsndx  17317  dsid  17318  dsndxnn  17319  basendxltdsndx  17320  slotsdifdsndx  17326  unifndx  17327  unifid  17328  unifndxnn  17329  basendxltunifndx  17330  slotsdifunifndx  17333  odrngstr  17335  homndx  17343  homid  17344  ccondx  17345  ccoid  17346  slotsbhcdif  17347  slotsdifplendx2  17348  slotsdifocndx  17349  imasvalstr  17383  prdsvalstr  17384  catstr  17896  ipostr  18464  smndex2dnrinv  18852  cycsubmcl  19142  psgnunilem2  19436  odcau  19545  lt6abl  19836  omndmul2  20074  0ringnnzr  20470  cnfldstr  21323  cnfldstrOLD  21338  nn0srg  21404  freshmansdream  21541  mvrid  21951  mvrf1  21953  mplcoe3  22005  psrbagsn  22030  evlslem1  22049  mhpvarcl  22103  psdcl  22116  psdmul  22121  psdmvr  22124  pmatcollpw3fi1lem1  22742  chfacfscmulgsum  22816  chfacfpmmulfsupp  22819  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cpmadugsumlemB  22830  cpmadugsumlemF  22832  dscmet  24528  ehl1eudis  25388  dveflem  25951  c1lip2  25971  itgpowd  26025  ply1remlem  26138  fta1glem1  26141  fta1blem  26144  plyid  26182  coeidp  26237  dgrid  26238  vieta1lem2  26287  vieta1  26288  aalioulem3  26310  aaliou2b  26317  dvtaylp  26346  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  radcnvlem2  26391  dvradcnv  26398  pserdvlem2  26406  logtayllem  26636  logtayl  26637  cxp1  26648  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  leibpilem2  26919  log2ublem3  26926  log2ub  26927  birthday  26932  lgamcvg2  27033  gamp1  27036  issqf  27114  ppi2  27148  mumullem2  27158  sqff1o  27160  1sgmprm  27178  ppiublem2  27182  chtublem  27190  logfacbnd3  27202  logexprlim  27204  logfacrlim2  27205  perfectlem1  27208  perfectlem2  27209  bclbnd  27259  bpos1  27262  bposlem6  27268  lgsval  27280  2lgslem3a  27375  2lgslem3c  27377  rpvmasumlem  27466  log2sumbnd  27523  itvndx  28521  lngndx  28522  itvid  28523  lngid  28524  slotsinbpsd  28525  slotslnbpsd  28526  lngndxnitvndx  28527  trkgstr  28528  eengstr  29065  edgfid  29075  edgfndx  29076  edgfndxnn  29077  basendxltedgfndx  29079  usgrexmplef  29344  cusgrsizeindb1  29536  wlk1ewlk  29725  usgr2pthlem  29848  uspgrn2crct  29893  crctcshwlkn0lem5  29899  rusgrnumwwlkl1  30056  rusgrnumwwlkb1  30060  clwwlkccatlem  30076  clwwlkinwwlk  30127  umgr2cwwkdifex  30152  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  konigsbergiedgw  30335  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  konigsberglem4  30342  1kp2ke3k  30533  ex-exp  30537  ex-fac  30538  9p10ne21  30557  sgnmulsgn  32934  sgnmulsgp  32935  nexple  32936  dpmul4  33006  threehalves  33007  1mhdrd  33008  s2f1  33038  cycpm2tr  33213  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  ply1dg1rt  33673  coe1vr1  33684  deg1vr  33685  mplmulmvr  33716  esplylem  33743  esplyfv1  33746  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  drngdimgt0  33796  rtelextdg2lem  33904  fldext2chn  33906  constrdircl  33943  iconstr  33944  2sqr3minply  33958  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminply  33966  lmat22e12  33997  lmat22e21  33998  lmat22e22  33999  madjusmdetlem4  34008  oddpwdc  34532  eulerpartlemd  34544  eulerpartlemgs2  34558  eulerpartlemn  34559  iwrdsplit  34565  fib0  34577  fib1  34578  fibp1  34579  plymulx0  34725  signstfveq0  34755  signsvvf  34757  signsvfn  34760  signshlen  34768  prodfzo03  34781  reprsuc  34793  breprexplemc  34810  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  usgrgt2cycl  35346  subfac1  35394  kur14lem9  35430  bccolsum  35955  nn0prpw  36539  12gcd5e1  42373  60gcd6e6  42374  60gcd7e1  42375  420gcd8e4  42376  12lcm5e60  42378  lcmineqlem11  42409  lcmineqlem18  42416  lcmineqlem22  42420  lcmineqlem  42422  3exp7  42423  3lexlogpow5ineq1  42424  3lexlogpow5ineq2  42425  3lexlogpow5ineq4  42426  3lexlogpow5ineq5  42430  dvrelogpow2b  42438  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p3  42448  aks6d1c1p8  42485  aks6d1c5lem3  42507  2np3bcnp1  42514  2ap1caineq  42515  sticksstones22  42538  aks6d1c6lem1  42540  aks6d1c7lem1  42550  aks6d1c7  42554  235t711  42675  ex-decpmul  42676  fltnltalem  43020  sum9cubes  43030  3cubeslem3l  43043  3cubeslem3r  43044  pell1qr1  43228  rmspecfund  43266  jm2.23  43353  jm2.27c  43364  areaquad  43573  resqrtvalex  44001  imsqrtvalex  44002  brfvidRP  44044  brfvrcld  44047  corclrcl  44063  dftrcl3  44076  dfrtrcl3  44089  fvrtrcllb1d  44093  corcltrcl  44095  cotrclrcl  44098  inductionexd  44511  radcnvrat  44670  binomcxplemnn0  44705  binomcxplemfrat  44707  binomcxplemnotnn0  44712  rexanuz2nf  45850  wallispilem2  46424  wallispilem5  46427  wallispi2lem2  46430  stirlinglem5  46436  stirlinglem7  46438  stirlinglem10  46441  stirlinglem11  46442  fourierdlem48  46512  ormkglobd  47233  iccpartigtl  47783  iccpartlt  47784  iccpartgel  47789  fmtnosqrt  47899  fmtno1  47901  fmtno2  47910  fmtno5lem1  47913  fmtno5lem2  47914  fmtno5lem3  47915  fmtno5lem4  47916  fmtno5  47917  257prm  47921  fmtnofac1  47930  fmtno4prmfac  47932  fmtno4prmfac193  47933  fmtno4nprmfac193  47934  fmtno5faclem1  47939  fmtno5faclem2  47940  fmtno5faclem3  47941  fmtno5fac  47942  fmtno5nprm  47943  3ndvds4  47955  139prmALT  47956  31prm  47957  m5prm  47958  127prm  47959  m7prm  47960  m11nprm  47961  lighneallem2  47966  perfectALTVlem1  48081  perfectALTVlem2  48082  11t31e341  48092  2exp340mod341  48093  341fppr2  48094  8exp8mod9  48096  nfermltl8rev  48102  nfermltl2rev  48103  evengpoap3  48159  nnsum4primesevenALTV  48161  bgoldbtbndlem1  48165  bgoldbachlt  48173  tgblthelfgott  48175  cycl3grtri  48307  stgr1  48321  usgrexmpl1lem  48381  usgrexmpl2lem  48386  gpgprismgriedgdmss  48412  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem9  48463  gpgprismgr4cycllem10  48464  grlimedgnedg  48491  nnpw2pmod  48943  dig1  48968  dignn0flhalflem2  48976  1aryfvalel  48996  itcoval1  49023  itcoval2  49024  ackval1  49041  ackval2  49042  ackval3  49043  ackendofnn0  49044  ackvalsucsucval  49048  ackval0012  49049  ackval1012  49050  ackval2012  49051  ackval3012  49052  ackval41a  49054  ackval42  49056