Theorem 1nn0 12512

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

Syntax hints:   ∈ wcel 2099  1c1 11133  ℕ₀cn0 12496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-1cn 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12237  df-n0 12497

This theorem is referenced by:  peano2nn0  12536  deccl  12716  10nn0  12719  numsucc  12741  numadd  12748  numaddc  12749  11multnc  12769  6p5lem  12771  6p6e12  12775  7p5e12  12778  8p4e12  12783  9p2e11  12788  9p3e12  12789  10p10e20  12796  4t4e16  12800  5t2e10  12801  5t4e20  12803  6t3e18  12806  6t4e24  12807  7t3e21  12811  7t4e28  12812  8t3e24  12817  9t3e27  12824  9t9e81  12830  xnn0n0n1ge2b  13137  fz0to3un2pr  13629  elfzom1elp1fzo  13725  fzo0sn0fzo1  13747  fldiv4lem1div2  13828  expn1  14062  nn0expcl  14066  sqval  14105  nn0opthlem1  14253  fac2  14264  faclbnd4lem2  14279  bccl  14307  hashsng  14354  hashen1  14355  hashrabrsn  14357  1elfz0hash  14375  hashgt23el  14409  hashprlei  14455  hashtplei  14471  wrdred1hash  14537  pfx1  14679  repsw1  14759  cshw1  14798  s3fv1  14869  s4fv1  14873  pfx2  14924  repsw2  14927  repsw3  14928  wwlktovf  14933  relexp1g  14999  relexpaddg  15026  rtrclreclem1  15030  bcxmas  15807  climcndslem2  15822  climcnds  15823  arisum  15832  geoisum1  15851  geoisum1c  15852  mertenslem2  15857  fprodnn0cl  15927  nn0risefaccl  15992  bpoly1  16021  bpoly4  16029  fsumcube  16030  ege2le3  16060  ef4p  16083  efgt1p2  16084  efgt1p  16085  sin01gt0  16160  rpnnen2lem3  16186  dvds1  16289  3dvds2dec  16303  bitsmod  16404  bitsinv1lem  16409  sadadd2lem  16427  sadadd  16435  sadass  16439  smupp1  16448  smumul  16461  prmdvdsbc  16691  pcelnn  16832  pockthg  16868  vdwlem12  16954  prmo1  16999  dec5nprm  17028  dec2nprm  17029  modxp1i  17032  2exp8  17051  2exp11  17052  2exp16  17053  2expltfac  17055  5prm  17071  11prm  17077  13prm  17078  17prm  17079  19prm  17080  23prm  17081  prmlem2  17082  37prm  17083  43prm  17084  83prm  17085  139prm  17086  163prm  17087  317prm  17088  631prm  17089  1259lem1  17093  1259lem2  17094  1259lem3  17095  1259lem4  17096  1259lem5  17097  1259prm  17098  2503lem1  17099  2503lem2  17100  2503lem3  17101  2503prm  17102  4001lem1  17103  4001lem2  17104  4001lem3  17105  4001lem4  17106  4001prm  17107  ocndx  17355  ocid  17356  basendxnocndx  17357  plendxnocndx  17358  dsndx  17359  dsid  17360  dsndxnn  17361  basendxltdsndx  17362  slotsdifdsndx  17368  unifndx  17369  unifid  17370  unifndxnn  17371  basendxltunifndx  17372  slotsdifunifndx  17375  odrngstr  17377  homndx  17385  homid  17386  ccondx  17387  ccoid  17388  slotsbhcdif  17389  slotsbhcdifOLD  17390  slotsdifplendx2  17391  slotsdifocndx  17392  imasvalstr  17426  prdsvalstr  17427  oppchomfvalOLD  17688  oppcbasOLD  17693  rescbasOLD  17806  resccoOLD  17810  rescabsOLD  17812  catstr  17941  ipostr  18514  smndex2dnrinv  18860  cycsubmcl  19149  psgnunilem2  19443  odcau  19552  lt6abl  19843  mgpdsOLD  20081  0ringnnzr  20455  sradsOLD  21071  cnfldstr  21274  cnfldstrOLD  21289  cnfldfunALTOLDOLD  21301  nn0srg  21363  freshmansdream  21501  thlbasOLD  21622  thlleOLD  21624  mvrid  21919  mvrf1  21921  mplcoe3  21969  psrbagsn  22000  evlslem1  22021  mhpvarcl  22065  psdcl  22078  psdmul  22083  pmatcollpw3fi1lem1  22681  chfacfscmulgsum  22755  chfacfpmmulfsupp  22758  chfacfpmmulgsum  22759  chfacfpmmulgsum2  22760  cpmadugsumlemB  22769  cpmadugsumlemF  22771  tuslemOLD  24165  tmslemOLD  24384  dscmet  24474  tnglemOLD  24543  ehl1eudis  25341  dveflem  25904  c1lip2  25924  itgpowd  25978  ply1remlem  26092  fta1glem1  26095  fta1blem  26098  plyid  26136  coeidp  26191  dgrid  26192  vieta1lem2  26239  vieta1  26240  aalioulem3  26262  aaliou2b  26269  dvtaylp  26298  taylthlem1  26301  taylthlem2  26302  taylthlem2OLD  26303  radcnvlem2  26343  dvradcnv  26350  pserdvlem2  26358  logtayllem  26586  logtayl  26587  cxp1  26598  quart1cl  26779  quart1lem  26780  quart1  26781  quartlem1  26782  quartlem2  26783  leibpilem2  26866  log2ublem3  26873  log2ub  26874  birthday  26879  lgamcvg2  26980  gamp1  26983  issqf  27061  ppi2  27095  mumullem2  27105  sqff1o  27107  1sgmprm  27125  ppiublem2  27129  chtublem  27137  logfacbnd3  27149  logexprlim  27151  logfacrlim2  27152  perfectlem1  27155  perfectlem2  27156  bclbnd  27206  bpos1  27209  bposlem6  27215  lgsval  27227  2lgslem3a  27322  2lgslem3c  27324  rpvmasumlem  27413  log2sumbnd  27470  itvndx  28234  lngndx  28235  itvid  28236  lngid  28237  slotsinbpsd  28238  slotslnbpsd  28239  lngndxnitvndx  28240  trkgstr  28241  ttgvalOLD  28673  ttglemOLD  28675  ttgbasOLD  28677  ttgdsOLD  28684  eengstr  28784  edgfid  28794  edgfndx  28795  edgfndxnn  28796  edgfndxidOLD  28798  basendxltedgfndx  28799  baseltedgfOLD  28800  usgrexmplef  29065  cusgrsizeindb1  29257  wlk1ewlk  29447  usgr2pthlem  29570  uspgrn2crct  29612  crctcshwlkn0lem5  29618  rusgrnumwwlkl1  29772  rusgrnumwwlkb1  29776  clwwlkccatlem  29792  clwwlkinwwlk  29843  umgr2cwwkdifex  29868  upgr3v3e3cycl  29983  upgr4cycl4dv4e  29988  konigsbergiedgw  30051  konigsberglem1  30055  konigsberglem2  30056  konigsberglem3  30057  konigsberglem4  30058  1kp2ke3k  30249  ex-exp  30253  ex-fac  30254  9p10ne21  30273  dpmul4  32631  threehalves  32632  1mhdrd  32633  s2f1  32662  omndmul2  32786  cycpm2tr  32834  drngdimgt0  33306  lmat22e12  33414  lmat22e21  33415  lmat22e22  33416  madjusmdetlem4  33425  nexple  33622  oddpwdc  33968  eulerpartlemd  33980  eulerpartlemgs2  33994  eulerpartlemn  33995  iwrdsplit  34001  fib0  34013  fib1  34014  fibp1  34015  sgnmulsgn  34163  sgnmulsgp  34164  plymulx0  34173  signstfveq0  34203  signsvvf  34205  signsvfn  34208  signshlen  34216  prodfzo03  34229  reprsuc  34241  breprexplemc  34258  hgt750lemd  34274  hgt750lem  34277  hgt750lem2  34278  hgt750leme  34284  usgrgt2cycl  34734  subfac1  34782  kur14lem9  34818  bccolsum  35327  nn0prpw  35801  12gcd5e1  41468  60gcd6e6  41469  60gcd7e1  41470  420gcd8e4  41471  12lcm5e60  41473  lcmineqlem11  41504  lcmineqlem18  41511  lcmineqlem22  41515  lcmineqlem  41517  3exp7  41518  3lexlogpow5ineq1  41519  3lexlogpow5ineq2  41520  3lexlogpow5ineq4  41521  3lexlogpow5ineq5  41525  dvrelogpow2b  41533  aks4d1p1p2  41535  aks4d1p1p4  41536  aks4d1p1p6  41538  aks4d1p1p7  41539  aks4d1p1p5  41540  aks4d1p1  41541  aks4d1p3  41543  aks6d1c1p8  41580  aks6d1c5lem3  41602  2np3bcnp1  41610  2ap1caineq  41611  sticksstones22  41634  aks6d1c6lem1  41636  aks6d1c7lem1  41646  aks6d1c7  41650  factwoffsmonot  41688  235t711  41861  ex-decpmul  41862  nn0rppwr  41887  fltnltalem  42080  sum9cubes  42090  3cubeslem3l  42100  3cubeslem3r  42101  pell1qr1  42285  rmspecfund  42323  jm2.23  42411  jm2.27c  42422  areaquad  42638  resqrtvalex  43069  imsqrtvalex  43070  brfvidRP  43112  brfvrcld  43115  corclrcl  43131  dftrcl3  43144  dfrtrcl3  43157  fvrtrcllb1d  43161  corcltrcl  43163  cotrclrcl  43166  inductionexd  43579  radcnvrat  43745  binomcxplemnn0  43780  binomcxplemfrat  43782  binomcxplemnotnn0  43787  rexanuz2nf  44869  wallispilem2  45448  wallispilem5  45451  wallispi2lem2  45454  stirlinglem5  45460  stirlinglem7  45462  stirlinglem10  45465  stirlinglem11  45466  fourierdlem48  45536  iccpartigtl  46757  iccpartlt  46758  iccpartgel  46763  fmtnosqrt  46873  fmtno1  46875  fmtno2  46884  fmtno5lem1  46887  fmtno5lem2  46888  fmtno5lem3  46889  fmtno5lem4  46890  fmtno5  46891  257prm  46895  fmtnofac1  46904  fmtno4prmfac  46906  fmtno4prmfac193  46907  fmtno4nprmfac193  46908  fmtno5faclem1  46913  fmtno5faclem2  46914  fmtno5faclem3  46915  fmtno5fac  46916  fmtno5nprm  46917  3ndvds4  46929  139prmALT  46930  31prm  46931  m5prm  46932  127prm  46933  m7prm  46934  m11nprm  46935  lighneallem2  46940  perfectALTVlem1  47055  perfectALTVlem2  47056  11t31e341  47066  2exp340mod341  47067  341fppr2  47068  8exp8mod9  47070  nfermltl8rev  47076  nfermltl2rev  47077  evengpoap3  47133  nnsum4primesevenALTV  47135  bgoldbtbndlem1  47139  bgoldbachlt  47147  tgblthelfgott  47149  nnpw2pmod  47650  dig1  47675  dignn0flhalflem2  47683  1aryfvalel  47703  itcoval1  47730  itcoval2  47731  ackval1  47748  ackval2  47749  ackval3  47750  ackendofnn0  47751  ackvalsucsucval  47755  ackval0012  47756  ackval1012  47757  ackval2012  47758  ackval3012  47759  ackval41a  47761  ackval42  47763  prstclevalOLD  48069  prstcocvalOLD  48072