Theorem 1nn0 12408

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

Syntax hints:   ∈ wcel 2113  1c1 11018  ℕ₀cn0 12392

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11075

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-nn 12137  df-n0 12393

This theorem is referenced by:  peano2nn0  12432  deccl  12613  10nn0  12616  numsucc  12638  numadd  12645  numaddc  12646  11multnc  12666  6p5lem  12668  6p6e12  12672  7p5e12  12675  8p4e12  12680  9p2e11  12685  9p3e12  12686  10p10e20  12693  4t4e16  12697  5t2e10  12698  5t4e20  12700  6t3e18  12703  6t4e24  12704  7t3e21  12708  7t4e28  12709  8t3e24  12714  9t3e27  12721  9t9e81  12727  xnn0n0n1ge2b  13037  fz0to3un2pr  13536  elfzom1elp1fzo  13639  fzo0sn0fzo1  13662  fvf1tp  13700  fldiv4lem1div2  13748  expn1  13985  nn0expcl  13989  sqval  14028  nn0opthlem1  14182  fac2  14193  faclbnd4lem2  14208  bccl  14236  hashsng  14283  hashen1  14284  hashrabrsn  14286  1elfz0hash  14304  hashgt23el  14338  hashprlei  14382  hashtplei  14398  tpf1ofv1  14411  tpfo  14414  wrdred1hash  14475  pfx1  14617  repsw1  14697  cshw1  14736  s3fv1  14806  s4fv1  14810  pfx2  14861  repsw2  14864  repsw3  14865  wwlktovf  14870  relexp1g  14940  relexpaddg  14967  rtrclreclem1  14971  bcxmas  15749  climcndslem2  15764  climcnds  15765  arisum  15774  geoisum1  15793  geoisum1c  15794  mertenslem2  15799  fprodnn0cl  15871  nn0risefaccl  15936  bpoly1  15965  bpoly4  15973  fsumcube  15974  ege2le3  16004  ef4p  16029  efgt1p2  16030  efgt1p  16031  sin01gt0  16106  rpnnen2lem3  16132  dvds1  16237  3dvds2dec  16251  5ndvds6  16332  bitsmod  16354  bitsinv1lem  16359  sadadd2lem  16377  sadadd  16385  sadass  16389  smupp1  16398  smumul  16411  nn0rppwr  16479  prmdvdsbc  16644  pcelnn  16789  pockthg  16825  vdwlem12  16911  prmo1  16956  dec5nprm  16985  dec2nprm  16986  modxp1i  16989  2exp8  17007  2exp11  17008  2exp16  17009  2expltfac  17011  5prm  17027  11prm  17033  13prm  17034  17prm  17035  19prm  17036  23prm  17037  prmlem2  17038  37prm  17039  43prm  17040  83prm  17041  139prm  17042  163prm  17043  317prm  17044  631prm  17045  1259lem1  17049  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  1259prm  17054  2503lem1  17055  2503lem2  17056  2503lem3  17057  2503prm  17058  4001lem1  17059  4001lem2  17060  4001lem3  17061  4001lem4  17062  4001prm  17063  ocndx  17292  ocid  17293  basendxnocndx  17294  plendxnocndx  17295  dsndx  17296  dsid  17297  dsndxnn  17298  basendxltdsndx  17299  slotsdifdsndx  17305  unifndx  17306  unifid  17307  unifndxnn  17308  basendxltunifndx  17309  slotsdifunifndx  17312  odrngstr  17314  homndx  17322  homid  17323  ccondx  17324  ccoid  17325  slotsbhcdif  17326  slotsdifplendx2  17327  slotsdifocndx  17328  imasvalstr  17362  prdsvalstr  17363  catstr  17875  ipostr  18443  smndex2dnrinv  18831  cycsubmcl  19121  psgnunilem2  19415  odcau  19524  lt6abl  19815  omndmul2  20053  0ringnnzr  20449  cnfldstr  21302  cnfldstrOLD  21317  nn0srg  21383  freshmansdream  21520  mvrid  21930  mvrf1  21932  mplcoe3  21984  psrbagsn  22009  evlslem1  22028  mhpvarcl  22082  psdcl  22095  psdmul  22100  psdmvr  22103  pmatcollpw3fi1lem1  22721  chfacfscmulgsum  22795  chfacfpmmulfsupp  22798  chfacfpmmulgsum  22799  chfacfpmmulgsum2  22800  cpmadugsumlemB  22809  cpmadugsumlemF  22811  dscmet  24507  ehl1eudis  25367  dveflem  25930  c1lip2  25950  itgpowd  26004  ply1remlem  26117  fta1glem1  26120  fta1blem  26123  plyid  26161  coeidp  26216  dgrid  26217  vieta1lem2  26266  vieta1  26267  aalioulem3  26289  aaliou2b  26296  dvtaylp  26325  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  radcnvlem2  26370  dvradcnv  26377  pserdvlem2  26385  logtayllem  26615  logtayl  26616  cxp1  26627  quart1cl  26811  quart1lem  26812  quart1  26813  quartlem1  26814  quartlem2  26815  leibpilem2  26898  log2ublem3  26905  log2ub  26906  birthday  26911  lgamcvg2  27012  gamp1  27015  issqf  27093  ppi2  27127  mumullem2  27137  sqff1o  27139  1sgmprm  27157  ppiublem2  27161  chtublem  27169  logfacbnd3  27181  logexprlim  27183  logfacrlim2  27184  perfectlem1  27187  perfectlem2  27188  bclbnd  27238  bpos1  27241  bposlem6  27247  lgsval  27259  2lgslem3a  27354  2lgslem3c  27356  rpvmasumlem  27445  log2sumbnd  27502  itvndx  28435  lngndx  28436  itvid  28437  lngid  28438  slotsinbpsd  28439  slotslnbpsd  28440  lngndxnitvndx  28441  trkgstr  28442  eengstr  28979  edgfid  28989  edgfndx  28990  edgfndxnn  28991  basendxltedgfndx  28993  usgrexmplef  29258  cusgrsizeindb1  29450  wlk1ewlk  29639  usgr2pthlem  29762  uspgrn2crct  29807  crctcshwlkn0lem5  29813  rusgrnumwwlkl1  29970  rusgrnumwwlkb1  29974  clwwlkccatlem  29990  clwwlkinwwlk  30041  umgr2cwwkdifex  30066  upgr3v3e3cycl  30181  upgr4cycl4dv4e  30186  konigsbergiedgw  30249  konigsberglem1  30253  konigsberglem2  30254  konigsberglem3  30255  konigsberglem4  30256  1kp2ke3k  30447  ex-exp  30451  ex-fac  30452  9p10ne21  30471  sgnmulsgn  32851  sgnmulsgp  32852  nexple  32853  dpmul4  32923  threehalves  32924  1mhdrd  32925  s2f1  32955  cycpm2tr  33129  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  ply1dg1rt  33589  coe1vr1  33600  deg1vr  33601  mplmulmvr  33632  esplylem  33652  esplyfv1  33655  esplyind  33659  drngdimgt0  33703  rtelextdg2lem  33811  fldext2chn  33813  constrdircl  33850  iconstr  33851  2sqr3minply  33865  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminply  33873  lmat22e12  33904  lmat22e21  33905  lmat22e22  33906  madjusmdetlem4  33915  oddpwdc  34439  eulerpartlemd  34451  eulerpartlemgs2  34465  eulerpartlemn  34466  iwrdsplit  34472  fib0  34484  fib1  34485  fibp1  34486  plymulx0  34632  signstfveq0  34662  signsvvf  34664  signsvfn  34667  signshlen  34675  prodfzo03  34688  reprsuc  34700  breprexplemc  34717  hgt750lemd  34733  hgt750lem  34736  hgt750lem2  34737  hgt750leme  34743  usgrgt2cycl  35246  subfac1  35294  kur14lem9  35330  bccolsum  35855  nn0prpw  36439  12gcd5e1  42169  60gcd6e6  42170  60gcd7e1  42171  420gcd8e4  42172  12lcm5e60  42174  lcmineqlem11  42205  lcmineqlem18  42212  lcmineqlem22  42216  lcmineqlem  42218  3exp7  42219  3lexlogpow5ineq1  42220  3lexlogpow5ineq2  42221  3lexlogpow5ineq4  42222  3lexlogpow5ineq5  42226  dvrelogpow2b  42234  aks4d1p1p2  42236  aks4d1p1p4  42237  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  aks4d1p3  42244  aks6d1c1p8  42281  aks6d1c5lem3  42303  2np3bcnp1  42310  2ap1caineq  42311  sticksstones22  42334  aks6d1c6lem1  42336  aks6d1c7lem1  42346  aks6d1c7  42350  235t711  42475  ex-decpmul  42476  fltnltalem  42820  sum9cubes  42830  3cubeslem3l  42843  3cubeslem3r  42844  pell1qr1  43028  rmspecfund  43066  jm2.23  43153  jm2.27c  43164  areaquad  43373  resqrtvalex  43802  imsqrtvalex  43803  brfvidRP  43845  brfvrcld  43848  corclrcl  43864  dftrcl3  43877  dfrtrcl3  43890  fvrtrcllb1d  43894  corcltrcl  43896  cotrclrcl  43899  inductionexd  44312  radcnvrat  44471  binomcxplemnn0  44506  binomcxplemfrat  44508  binomcxplemnotnn0  44513  rexanuz2nf  45652  wallispilem2  46226  wallispilem5  46229  wallispi2lem2  46232  stirlinglem5  46238  stirlinglem7  46240  stirlinglem10  46243  stirlinglem11  46244  fourierdlem48  46314  ormkglobd  47035  iccpartigtl  47585  iccpartlt  47586  iccpartgel  47591  fmtnosqrt  47701  fmtno1  47703  fmtno2  47712  fmtno5lem1  47715  fmtno5lem2  47716  fmtno5lem3  47717  fmtno5lem4  47718  fmtno5  47719  257prm  47723  fmtnofac1  47732  fmtno4prmfac  47734  fmtno4prmfac193  47735  fmtno4nprmfac193  47736  fmtno5faclem1  47741  fmtno5faclem2  47742  fmtno5faclem3  47743  fmtno5fac  47744  fmtno5nprm  47745  3ndvds4  47757  139prmALT  47758  31prm  47759  m5prm  47760  127prm  47761  m7prm  47762  m11nprm  47763  lighneallem2  47768  perfectALTVlem1  47883  perfectALTVlem2  47884  11t31e341  47894  2exp340mod341  47895  341fppr2  47896  8exp8mod9  47898  nfermltl8rev  47904  nfermltl2rev  47905  evengpoap3  47961  nnsum4primesevenALTV  47963  bgoldbtbndlem1  47967  bgoldbachlt  47975  tgblthelfgott  47977  cycl3grtri  48109  stgr1  48123  usgrexmpl1lem  48183  usgrexmpl2lem  48188  gpgprismgriedgdmss  48214  gpgprismgr4cycllem3  48259  gpgprismgr4cycllem7  48263  gpgprismgr4cycllem9  48265  gpgprismgr4cycllem10  48266  grlimedgnedg  48293  nnpw2pmod  48745  dig1  48770  dignn0flhalflem2  48778  1aryfvalel  48798  itcoval1  48825  itcoval2  48826  ackval1  48843  ackval2  48844  ackval3  48845  ackendofnn0  48846  ackvalsucsucval  48850  ackval0012  48851  ackval1012  48852  ackval2012  48853  ackval3012  48854  ackval41a  48856  ackval42  48858