Theorem 1nn0 12465

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

Syntax hints:   ∈ wcel 2109  1c1 11076  ℕ₀cn0 12449

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  peano2nn0  12489  deccl  12671  10nn0  12674  numsucc  12696  numadd  12703  numaddc  12704  11multnc  12724  6p5lem  12726  6p6e12  12730  7p5e12  12733  8p4e12  12738  9p2e11  12743  9p3e12  12744  10p10e20  12751  4t4e16  12755  5t2e10  12756  5t4e20  12758  6t3e18  12761  6t4e24  12762  7t3e21  12766  7t4e28  12767  8t3e24  12772  9t3e27  12779  9t9e81  12785  xnn0n0n1ge2b  13099  fz0to3un2pr  13597  elfzom1elp1fzo  13700  fzo0sn0fzo1  13723  fvf1tp  13758  fldiv4lem1div2  13806  expn1  14043  nn0expcl  14047  sqval  14086  nn0opthlem1  14240  fac2  14251  faclbnd4lem2  14266  bccl  14294  hashsng  14341  hashen1  14342  hashrabrsn  14344  1elfz0hash  14362  hashgt23el  14396  hashprlei  14440  hashtplei  14456  tpf1ofv1  14469  tpfo  14472  wrdred1hash  14533  pfx1  14675  repsw1  14755  cshw1  14794  s3fv1  14865  s4fv1  14869  pfx2  14920  repsw2  14923  repsw3  14924  wwlktovf  14929  relexp1g  14999  relexpaddg  15026  rtrclreclem1  15030  bcxmas  15808  climcndslem2  15823  climcnds  15824  arisum  15833  geoisum1  15852  geoisum1c  15853  mertenslem2  15858  fprodnn0cl  15930  nn0risefaccl  15995  bpoly1  16024  bpoly4  16032  fsumcube  16033  ege2le3  16063  ef4p  16088  efgt1p2  16089  efgt1p  16090  sin01gt0  16165  rpnnen2lem3  16191  dvds1  16296  3dvds2dec  16310  5ndvds6  16391  bitsmod  16413  bitsinv1lem  16418  sadadd2lem  16436  sadadd  16444  sadass  16448  smupp1  16457  smumul  16470  nn0rppwr  16538  prmdvdsbc  16703  pcelnn  16848  pockthg  16884  vdwlem12  16970  prmo1  17015  dec5nprm  17044  dec2nprm  17045  modxp1i  17048  2exp8  17066  2exp11  17067  2exp16  17068  2expltfac  17070  5prm  17086  11prm  17092  13prm  17093  17prm  17094  19prm  17095  23prm  17096  prmlem2  17097  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  ocndx  17351  ocid  17352  basendxnocndx  17353  plendxnocndx  17354  dsndx  17355  dsid  17356  dsndxnn  17357  basendxltdsndx  17358  slotsdifdsndx  17364  unifndx  17365  unifid  17366  unifndxnn  17367  basendxltunifndx  17368  slotsdifunifndx  17371  odrngstr  17373  homndx  17381  homid  17382  ccondx  17383  ccoid  17384  slotsbhcdif  17385  slotsdifplendx2  17386  slotsdifocndx  17387  imasvalstr  17421  prdsvalstr  17422  catstr  17929  ipostr  18495  smndex2dnrinv  18849  cycsubmcl  19140  psgnunilem2  19432  odcau  19541  lt6abl  19832  0ringnnzr  20441  cnfldstr  21273  cnfldstrOLD  21288  nn0srg  21361  freshmansdream  21491  mvrid  21900  mvrf1  21902  mplcoe3  21952  psrbagsn  21977  evlslem1  21996  mhpvarcl  22042  psdcl  22055  psdmul  22060  psdmvr  22063  pmatcollpw3fi1lem1  22680  chfacfscmulgsum  22754  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cpmadugsumlemB  22768  cpmadugsumlemF  22770  dscmet  24467  ehl1eudis  25327  dveflem  25890  c1lip2  25910  itgpowd  25964  ply1remlem  26077  fta1glem1  26080  fta1blem  26083  plyid  26121  coeidp  26176  dgrid  26177  vieta1lem2  26226  vieta1  26227  aalioulem3  26249  aaliou2b  26256  dvtaylp  26285  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  radcnvlem2  26330  dvradcnv  26337  pserdvlem2  26345  logtayllem  26575  logtayl  26576  cxp1  26587  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  leibpilem2  26858  log2ublem3  26865  log2ub  26866  birthday  26871  lgamcvg2  26972  gamp1  26975  issqf  27053  ppi2  27087  mumullem2  27097  sqff1o  27099  1sgmprm  27117  ppiublem2  27121  chtublem  27129  logfacbnd3  27141  logexprlim  27143  logfacrlim2  27144  perfectlem1  27147  perfectlem2  27148  bclbnd  27198  bpos1  27201  bposlem6  27207  lgsval  27219  2lgslem3a  27314  2lgslem3c  27316  rpvmasumlem  27405  log2sumbnd  27462  itvndx  28371  lngndx  28372  itvid  28373  lngid  28374  slotsinbpsd  28375  slotslnbpsd  28376  lngndxnitvndx  28377  trkgstr  28378  eengstr  28914  edgfid  28924  edgfndx  28925  edgfndxnn  28926  basendxltedgfndx  28928  usgrexmplef  29193  cusgrsizeindb1  29385  wlk1ewlk  29575  usgr2pthlem  29700  uspgrn2crct  29745  crctcshwlkn0lem5  29751  rusgrnumwwlkl1  29905  rusgrnumwwlkb1  29909  clwwlkccatlem  29925  clwwlkinwwlk  29976  umgr2cwwkdifex  30001  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberglem4  30191  1kp2ke3k  30382  ex-exp  30386  ex-fac  30387  9p10ne21  30406  sgnmulsgn  32774  sgnmulsgp  32775  nexple  32776  dpmul4  32841  threehalves  32842  1mhdrd  32843  s2f1  32873  omndmul2  33033  cycpm2tr  33083  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1dg1rt  33555  coe1vr1  33564  deg1vr  33565  drngdimgt0  33621  rtelextdg2lem  33723  fldext2chn  33725  constrdircl  33762  iconstr  33763  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminply  33785  lmat22e12  33816  lmat22e21  33817  lmat22e22  33818  madjusmdetlem4  33827  oddpwdc  34352  eulerpartlemd  34364  eulerpartlemgs2  34378  eulerpartlemn  34379  iwrdsplit  34385  fib0  34397  fib1  34398  fibp1  34399  plymulx0  34545  signstfveq0  34575  signsvvf  34577  signsvfn  34580  signshlen  34588  prodfzo03  34601  reprsuc  34613  breprexplemc  34630  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  usgrgt2cycl  35124  subfac1  35172  kur14lem9  35208  bccolsum  35733  nn0prpw  36318  12gcd5e1  41998  60gcd6e6  41999  60gcd7e1  42000  420gcd8e4  42001  12lcm5e60  42003  lcmineqlem11  42034  lcmineqlem18  42041  lcmineqlem22  42045  lcmineqlem  42047  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq5  42055  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks6d1c1p8  42110  aks6d1c5lem3  42132  2np3bcnp1  42139  2ap1caineq  42140  sticksstones22  42163  aks6d1c6lem1  42165  aks6d1c7lem1  42175  aks6d1c7  42179  235t711  42300  ex-decpmul  42301  fltnltalem  42657  sum9cubes  42667  3cubeslem3l  42681  3cubeslem3r  42682  pell1qr1  42866  rmspecfund  42904  jm2.23  42992  jm2.27c  43003  areaquad  43212  resqrtvalex  43641  imsqrtvalex  43642  brfvidRP  43684  brfvrcld  43687  corclrcl  43703  dftrcl3  43716  dfrtrcl3  43729  fvrtrcllb1d  43733  corcltrcl  43735  cotrclrcl  43738  inductionexd  44151  radcnvrat  44310  binomcxplemnn0  44345  binomcxplemfrat  44347  binomcxplemnotnn0  44352  rexanuz2nf  45495  wallispilem2  46071  wallispilem5  46074  wallispi2lem2  46077  stirlinglem5  46083  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  fourierdlem48  46159  ormkglobd  46880  iccpartigtl  47428  iccpartlt  47429  iccpartgel  47434  fmtnosqrt  47544  fmtno1  47546  fmtno2  47555  fmtno5lem1  47558  fmtno5lem2  47559  fmtno5lem3  47560  fmtno5lem4  47561  fmtno5  47562  257prm  47566  fmtnofac1  47575  fmtno4prmfac  47577  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  fmtno5faclem1  47584  fmtno5faclem2  47585  fmtno5faclem3  47586  fmtno5fac  47587  fmtno5nprm  47588  3ndvds4  47600  139prmALT  47601  31prm  47602  m5prm  47603  127prm  47604  m7prm  47605  m11nprm  47606  lighneallem2  47611  perfectALTVlem1  47726  perfectALTVlem2  47727  11t31e341  47737  2exp340mod341  47738  341fppr2  47739  8exp8mod9  47741  nfermltl8rev  47747  nfermltl2rev  47748  evengpoap3  47804  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  bgoldbachlt  47818  tgblthelfgott  47820  cycl3grtri  47950  stgr1  47964  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgprismgriedgdmss  48047  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem9  48097  gpgprismgr4cycllem10  48098  nnpw2pmod  48576  dig1  48601  dignn0flhalflem2  48609  1aryfvalel  48629  itcoval1  48656  itcoval2  48657  ackval1  48674  ackval2  48675  ackval3  48676  ackendofnn0  48677  ackvalsucsucval  48681  ackval0012  48682  ackval1012  48683  ackval2012  48684  ackval3012  48685  ackval41a  48687  ackval42  48689