Theorem 1nn0 12397

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

Syntax hints:   ∈ wcel 2111  1c1 11007  ℕ₀cn0 12381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-n0 12382

This theorem is referenced by:  peano2nn0  12421  deccl  12603  10nn0  12606  numsucc  12628  numadd  12635  numaddc  12636  11multnc  12656  6p5lem  12658  6p6e12  12662  7p5e12  12665  8p4e12  12670  9p2e11  12675  9p3e12  12676  10p10e20  12683  4t4e16  12687  5t2e10  12688  5t4e20  12690  6t3e18  12693  6t4e24  12694  7t3e21  12698  7t4e28  12699  8t3e24  12704  9t3e27  12711  9t9e81  12717  xnn0n0n1ge2b  13031  fz0to3un2pr  13529  elfzom1elp1fzo  13632  fzo0sn0fzo1  13655  fvf1tp  13693  fldiv4lem1div2  13741  expn1  13978  nn0expcl  13982  sqval  14021  nn0opthlem1  14175  fac2  14186  faclbnd4lem2  14201  bccl  14229  hashsng  14276  hashen1  14277  hashrabrsn  14279  1elfz0hash  14297  hashgt23el  14331  hashprlei  14375  hashtplei  14391  tpf1ofv1  14404  tpfo  14407  wrdred1hash  14468  pfx1  14610  repsw1  14690  cshw1  14729  s3fv1  14799  s4fv1  14803  pfx2  14854  repsw2  14857  repsw3  14858  wwlktovf  14863  relexp1g  14933  relexpaddg  14960  rtrclreclem1  14964  bcxmas  15742  climcndslem2  15757  climcnds  15758  arisum  15767  geoisum1  15786  geoisum1c  15787  mertenslem2  15792  fprodnn0cl  15864  nn0risefaccl  15929  bpoly1  15958  bpoly4  15966  fsumcube  15967  ege2le3  15997  ef4p  16022  efgt1p2  16023  efgt1p  16024  sin01gt0  16099  rpnnen2lem3  16125  dvds1  16230  3dvds2dec  16244  5ndvds6  16325  bitsmod  16347  bitsinv1lem  16352  sadadd2lem  16370  sadadd  16378  sadass  16382  smupp1  16391  smumul  16404  nn0rppwr  16472  prmdvdsbc  16637  pcelnn  16782  pockthg  16818  vdwlem12  16904  prmo1  16949  dec5nprm  16978  dec2nprm  16979  modxp1i  16982  2exp8  17000  2exp11  17001  2exp16  17002  2expltfac  17004  5prm  17020  11prm  17026  13prm  17027  17prm  17028  19prm  17029  23prm  17030  prmlem2  17031  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  ocndx  17285  ocid  17286  basendxnocndx  17287  plendxnocndx  17288  dsndx  17289  dsid  17290  dsndxnn  17291  basendxltdsndx  17292  slotsdifdsndx  17298  unifndx  17299  unifid  17300  unifndxnn  17301  basendxltunifndx  17302  slotsdifunifndx  17305  odrngstr  17307  homndx  17315  homid  17316  ccondx  17317  ccoid  17318  slotsbhcdif  17319  slotsdifplendx2  17320  slotsdifocndx  17321  imasvalstr  17355  prdsvalstr  17356  catstr  17867  ipostr  18435  smndex2dnrinv  18823  cycsubmcl  19114  psgnunilem2  19408  odcau  19517  lt6abl  19808  omndmul2  20046  0ringnnzr  20441  cnfldstr  21294  cnfldstrOLD  21309  nn0srg  21375  freshmansdream  21512  mvrid  21922  mvrf1  21924  mplcoe3  21974  psrbagsn  21999  evlslem1  22018  mhpvarcl  22064  psdcl  22077  psdmul  22082  psdmvr  22085  pmatcollpw3fi1lem1  22702  chfacfscmulgsum  22776  chfacfpmmulfsupp  22779  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cpmadugsumlemB  22790  cpmadugsumlemF  22792  dscmet  24488  ehl1eudis  25348  dveflem  25911  c1lip2  25931  itgpowd  25985  ply1remlem  26098  fta1glem1  26101  fta1blem  26104  plyid  26142  coeidp  26197  dgrid  26198  vieta1lem2  26247  vieta1  26248  aalioulem3  26270  aaliou2b  26277  dvtaylp  26306  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  radcnvlem2  26351  dvradcnv  26358  pserdvlem2  26366  logtayllem  26596  logtayl  26597  cxp1  26608  quart1cl  26792  quart1lem  26793  quart1  26794  quartlem1  26795  quartlem2  26796  leibpilem2  26879  log2ublem3  26886  log2ub  26887  birthday  26892  lgamcvg2  26993  gamp1  26996  issqf  27074  ppi2  27108  mumullem2  27118  sqff1o  27120  1sgmprm  27138  ppiublem2  27142  chtublem  27150  logfacbnd3  27162  logexprlim  27164  logfacrlim2  27165  perfectlem1  27168  perfectlem2  27169  bclbnd  27219  bpos1  27222  bposlem6  27228  lgsval  27240  2lgslem3a  27335  2lgslem3c  27337  rpvmasumlem  27426  log2sumbnd  27483  itvndx  28416  lngndx  28417  itvid  28418  lngid  28419  slotsinbpsd  28420  slotslnbpsd  28421  lngndxnitvndx  28422  trkgstr  28423  eengstr  28959  edgfid  28969  edgfndx  28970  edgfndxnn  28971  basendxltedgfndx  28973  usgrexmplef  29238  cusgrsizeindb1  29430  wlk1ewlk  29619  usgr2pthlem  29742  uspgrn2crct  29787  crctcshwlkn0lem5  29793  rusgrnumwwlkl1  29947  rusgrnumwwlkb1  29951  clwwlkccatlem  29967  clwwlkinwwlk  30018  umgr2cwwkdifex  30043  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  konigsbergiedgw  30226  konigsberglem1  30230  konigsberglem2  30231  konigsberglem3  30232  konigsberglem4  30233  1kp2ke3k  30424  ex-exp  30428  ex-fac  30429  9p10ne21  30448  sgnmulsgn  32823  sgnmulsgp  32824  nexple  32825  dpmul4  32892  threehalves  32893  1mhdrd  32894  s2f1  32924  cycpm2tr  33086  evl1deg1  33537  evl1deg2  33538  evl1deg3  33539  ply1dg1rt  33541  coe1vr1  33550  deg1vr  33551  esplylem  33585  esplyfv1  33588  drngdimgt0  33629  rtelextdg2lem  33737  fldext2chn  33739  constrdircl  33776  iconstr  33777  2sqr3minply  33791  cos9thpiminplylem1  33793  cos9thpiminplylem2  33794  cos9thpiminply  33799  lmat22e12  33830  lmat22e21  33831  lmat22e22  33832  madjusmdetlem4  33841  oddpwdc  34365  eulerpartlemd  34377  eulerpartlemgs2  34391  eulerpartlemn  34392  iwrdsplit  34398  fib0  34410  fib1  34411  fibp1  34412  plymulx0  34558  signstfveq0  34588  signsvvf  34590  signsvfn  34593  signshlen  34601  prodfzo03  34614  reprsuc  34626  breprexplemc  34643  hgt750lemd  34659  hgt750lem  34662  hgt750lem2  34663  hgt750leme  34669  usgrgt2cycl  35172  subfac1  35220  kur14lem9  35256  bccolsum  35781  nn0prpw  36363  12gcd5e1  42042  60gcd6e6  42043  60gcd7e1  42044  420gcd8e4  42045  12lcm5e60  42047  lcmineqlem11  42078  lcmineqlem18  42085  lcmineqlem22  42089  lcmineqlem  42091  3exp7  42092  3lexlogpow5ineq1  42093  3lexlogpow5ineq2  42094  3lexlogpow5ineq4  42095  3lexlogpow5ineq5  42099  dvrelogpow2b  42107  aks4d1p1p2  42109  aks4d1p1p4  42110  aks4d1p1p6  42112  aks4d1p1p7  42113  aks4d1p1p5  42114  aks4d1p1  42115  aks4d1p3  42117  aks6d1c1p8  42154  aks6d1c5lem3  42176  2np3bcnp1  42183  2ap1caineq  42184  sticksstones22  42207  aks6d1c6lem1  42209  aks6d1c7lem1  42219  aks6d1c7  42223  235t711  42344  ex-decpmul  42345  fltnltalem  42701  sum9cubes  42711  3cubeslem3l  42725  3cubeslem3r  42726  pell1qr1  42910  rmspecfund  42948  jm2.23  43035  jm2.27c  43046  areaquad  43255  resqrtvalex  43684  imsqrtvalex  43685  brfvidRP  43727  brfvrcld  43730  corclrcl  43746  dftrcl3  43759  dfrtrcl3  43772  fvrtrcllb1d  43776  corcltrcl  43778  cotrclrcl  43781  inductionexd  44194  radcnvrat  44353  binomcxplemnn0  44388  binomcxplemfrat  44390  binomcxplemnotnn0  44395  rexanuz2nf  45536  wallispilem2  46110  wallispilem5  46113  wallispi2lem2  46116  stirlinglem5  46122  stirlinglem7  46124  stirlinglem10  46127  stirlinglem11  46128  fourierdlem48  46198  ormkglobd  46919  iccpartigtl  47460  iccpartlt  47461  iccpartgel  47466  fmtnosqrt  47576  fmtno1  47578  fmtno2  47587  fmtno5lem1  47590  fmtno5lem2  47591  fmtno5lem3  47592  fmtno5lem4  47593  fmtno5  47594  257prm  47598  fmtnofac1  47607  fmtno4prmfac  47609  fmtno4prmfac193  47610  fmtno4nprmfac193  47611  fmtno5faclem1  47616  fmtno5faclem2  47617  fmtno5faclem3  47618  fmtno5fac  47619  fmtno5nprm  47620  3ndvds4  47632  139prmALT  47633  31prm  47634  m5prm  47635  127prm  47636  m7prm  47637  m11nprm  47638  lighneallem2  47643  perfectALTVlem1  47758  perfectALTVlem2  47759  11t31e341  47769  2exp340mod341  47770  341fppr2  47771  8exp8mod9  47773  nfermltl8rev  47779  nfermltl2rev  47780  evengpoap3  47836  nnsum4primesevenALTV  47838  bgoldbtbndlem1  47842  bgoldbachlt  47850  tgblthelfgott  47852  cycl3grtri  47984  stgr1  47998  usgrexmpl1lem  48058  usgrexmpl2lem  48063  gpgprismgriedgdmss  48089  gpgprismgr4cycllem3  48134  gpgprismgr4cycllem7  48138  gpgprismgr4cycllem9  48140  gpgprismgr4cycllem10  48141  grlimedgnedg  48168  nnpw2pmod  48621  dig1  48646  dignn0flhalflem2  48654  1aryfvalel  48674  itcoval1  48701  itcoval2  48702  ackval1  48719  ackval2  48720  ackval3  48721  ackendofnn0  48722  ackvalsucsucval  48726  ackval0012  48727  ackval1012  48728  ackval2012  48729  ackval3012  48730  ackval41a  48732  ackval42  48734