Theorem 1nn0 12490

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

Syntax hints:   ∈ wcel 2106  1c1 11113  ℕ₀cn0 12474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12215  df-n0 12475

This theorem is referenced by:  peano2nn0  12514  deccl  12694  10nn0  12697  numsucc  12719  numadd  12726  numaddc  12727  11multnc  12747  6p5lem  12749  6p6e12  12753  7p5e12  12756  8p4e12  12761  9p2e11  12766  9p3e12  12767  10p10e20  12774  4t4e16  12778  5t2e10  12779  5t4e20  12781  6t3e18  12784  6t4e24  12785  7t3e21  12789  7t4e28  12790  8t3e24  12795  9t3e27  12802  9t9e81  12808  xnn0n0n1ge2b  13113  fz0to3un2pr  13605  elfzom1elp1fzo  13701  fzo0sn0fzo1  13723  fldiv4lem1div2  13804  expn1  14039  nn0expcl  14043  sqval  14082  nn0opthlem1  14230  fac2  14241  faclbnd4lem2  14256  bccl  14284  hashsng  14331  hashen1  14332  hashrabrsn  14334  1elfz0hash  14352  hashgt23el  14386  hashprlei  14431  hashtplei  14447  wrdred1hash  14513  pfx1  14655  repsw1  14735  cshw1  14774  s3fv1  14845  s4fv1  14849  pfx2  14900  repsw2  14903  repsw3  14904  wwlktovf  14909  relexp1g  14975  relexpaddg  15002  rtrclreclem1  15006  bcxmas  15783  climcndslem2  15798  climcnds  15799  arisum  15808  geoisum1  15827  geoisum1c  15828  mertenslem2  15833  fprodnn0cl  15903  nn0risefaccl  15968  bpoly1  15997  bpoly4  16005  fsumcube  16006  ege2le3  16035  ef4p  16058  efgt1p2  16059  efgt1p  16060  sin01gt0  16135  rpnnen2lem3  16161  dvds1  16264  3dvds2dec  16278  bitsmod  16379  bitsinv1lem  16384  sadadd2lem  16402  sadadd  16410  sadass  16414  smupp1  16423  smumul  16436  pcelnn  16805  pockthg  16841  vdwlem12  16927  prmo1  16972  dec5nprm  17001  dec2nprm  17002  modxp1i  17005  2exp8  17024  2exp11  17025  2exp16  17026  2expltfac  17028  5prm  17044  11prm  17050  13prm  17051  17prm  17052  19prm  17053  23prm  17054  prmlem2  17055  37prm  17056  43prm  17057  83prm  17058  139prm  17059  163prm  17060  317prm  17061  631prm  17062  1259lem1  17066  1259lem2  17067  1259lem3  17068  1259lem4  17069  1259lem5  17070  1259prm  17071  2503lem1  17072  2503lem2  17073  2503lem3  17074  2503prm  17075  4001lem1  17076  4001lem2  17077  4001lem3  17078  4001lem4  17079  4001prm  17080  ocndx  17328  ocid  17329  basendxnocndx  17330  plendxnocndx  17331  dsndx  17332  dsid  17333  dsndxnn  17334  basendxltdsndx  17335  slotsdifdsndx  17341  unifndx  17342  unifid  17343  unifndxnn  17344  basendxltunifndx  17345  slotsdifunifndx  17348  odrngstr  17350  homndx  17358  homid  17359  ccondx  17360  ccoid  17361  slotsbhcdif  17362  slotsbhcdifOLD  17363  slotsdifplendx2  17364  slotsdifocndx  17365  imasvalstr  17399  prdsvalstr  17400  oppchomfvalOLD  17661  oppcbasOLD  17666  rescbasOLD  17779  resccoOLD  17783  rescabsOLD  17785  catstr  17911  ipostr  18484  smndex2dnrinv  18798  cycsubmcl  19080  psgnunilem2  19365  odcau  19474  lt6abl  19765  mgpdsOLD  20003  0ringnnzr  20306  sradsOLD  20813  cnfldstr  20952  cnfldfunALTOLD  20964  nn0srg  21021  thlbasOLD  21256  thlleOLD  21258  mvrid  21549  mvrf1  21551  mplcoe3  21599  psrbagsn  21630  evlslem1  21651  mhpvarcl  21697  pmatcollpw3fi1lem1  22295  chfacfscmulgsum  22369  chfacfpmmulfsupp  22372  chfacfpmmulgsum  22373  chfacfpmmulgsum2  22374  cpmadugsumlemB  22383  cpmadugsumlemF  22385  tuslemOLD  23779  tmslemOLD  23998  dscmet  24088  tnglemOLD  24157  ehl1eudis  24944  dveflem  25503  c1lip2  25522  itgpowd  25574  ply1remlem  25687  fta1glem1  25690  fta1blem  25693  plyid  25730  coeidp  25784  dgrid  25785  vieta1lem2  25831  vieta1  25832  aalioulem3  25854  aaliou2b  25861  dvtaylp  25889  taylthlem1  25892  taylthlem2  25893  radcnvlem2  25933  dvradcnv  25940  pserdvlem2  25947  logtayllem  26174  logtayl  26175  cxp1  26186  quart1cl  26366  quart1lem  26367  quart1  26368  quartlem1  26369  quartlem2  26370  leibpilem2  26453  log2ublem3  26460  log2ub  26461  birthday  26466  lgamcvg2  26566  gamp1  26569  issqf  26647  ppi2  26681  mumullem2  26691  sqff1o  26693  1sgmprm  26709  ppiublem2  26713  chtublem  26721  logfacbnd3  26733  logexprlim  26735  logfacrlim2  26736  perfectlem1  26739  perfectlem2  26740  bclbnd  26790  bpos1  26793  bposlem6  26799  lgsval  26811  2lgslem3a  26906  2lgslem3c  26908  rpvmasumlem  26997  log2sumbnd  27054  itvndx  27726  lngndx  27727  itvid  27728  lngid  27729  slotsinbpsd  27730  slotslnbpsd  27731  lngndxnitvndx  27732  trkgstr  27733  ttgvalOLD  28165  ttglemOLD  28167  ttgbasOLD  28169  ttgdsOLD  28176  eengstr  28276  edgfid  28286  edgfndx  28287  edgfndxnn  28288  edgfndxidOLD  28290  basendxltedgfndx  28291  baseltedgfOLD  28292  usgrexmplef  28554  cusgrsizeindb1  28745  wlk1ewlk  28935  usgr2pthlem  29058  uspgrn2crct  29100  crctcshwlkn0lem5  29106  rusgrnumwwlkl1  29260  rusgrnumwwlkb1  29264  clwwlkccatlem  29280  clwwlkinwwlk  29331  umgr2cwwkdifex  29356  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  konigsbergiedgw  29539  konigsberglem1  29543  konigsberglem2  29544  konigsberglem3  29545  konigsberglem4  29546  1kp2ke3k  29737  ex-exp  29741  ex-fac  29742  9p10ne21  29761  prmdvdsbc  32060  dpmul4  32118  threehalves  32119  1mhdrd  32120  s2f1  32149  omndmul2  32271  cycpm2tr  32319  freshmansdream  32422  drngdimgt0  32762  lmat22e12  32868  lmat22e21  32869  lmat22e22  32870  madjusmdetlem4  32879  nexple  33076  oddpwdc  33422  eulerpartlemd  33434  eulerpartlemgs2  33448  eulerpartlemn  33449  iwrdsplit  33455  fib0  33467  fib1  33468  fibp1  33469  sgnmulsgn  33617  sgnmulsgp  33618  plymulx0  33627  signstfveq0  33657  signsvvf  33659  signsvfn  33662  signshlen  33670  prodfzo03  33684  reprsuc  33696  breprexplemc  33713  hgt750lemd  33729  hgt750lem  33732  hgt750lem2  33733  hgt750leme  33739  usgrgt2cycl  34190  subfac1  34238  kur14lem9  34274  bccolsum  34784  gg-cnfldstr  35263  nn0prpw  35300  12gcd5e1  40960  60gcd6e6  40961  60gcd7e1  40962  420gcd8e4  40963  12lcm5e60  40965  lcmineqlem11  40996  lcmineqlem18  41003  lcmineqlem22  41007  lcmineqlem  41009  3exp7  41010  3lexlogpow5ineq1  41011  3lexlogpow5ineq2  41012  3lexlogpow5ineq4  41013  3lexlogpow5ineq5  41017  dvrelogpow2b  41025  aks4d1p1p2  41027  aks4d1p1p4  41028  aks4d1p1p6  41030  aks4d1p1p7  41031  aks4d1p1p5  41032  aks4d1p1  41033  aks4d1p3  41035  2np3bcnp1  41052  2ap1caineq  41053  sticksstones22  41076  factwoffsmonot  41115  235t711  41293  ex-decpmul  41294  nn0rppwr  41312  fltnltalem  41492  sum9cubes  41502  3cubeslem3l  41512  3cubeslem3r  41513  pell1qr1  41697  rmspecfund  41735  jm2.23  41823  jm2.27c  41834  areaquad  42053  resqrtvalex  42484  imsqrtvalex  42485  brfvidRP  42527  brfvrcld  42530  corclrcl  42546  dftrcl3  42559  dfrtrcl3  42572  fvrtrcllb1d  42576  corcltrcl  42578  cotrclrcl  42581  inductionexd  42994  radcnvrat  43161  binomcxplemnn0  43196  binomcxplemfrat  43198  binomcxplemnotnn0  43203  rexanuz2nf  44288  wallispilem2  44867  wallispilem5  44870  wallispi2lem2  44873  stirlinglem5  44879  stirlinglem7  44881  stirlinglem10  44884  stirlinglem11  44885  fourierdlem48  44955  iccpartigtl  46176  iccpartlt  46177  iccpartgel  46182  fmtnosqrt  46292  fmtno1  46294  fmtno2  46303  fmtno5lem1  46306  fmtno5lem2  46307  fmtno5lem3  46308  fmtno5lem4  46309  fmtno5  46310  257prm  46314  fmtnofac1  46323  fmtno4prmfac  46325  fmtno4prmfac193  46326  fmtno4nprmfac193  46327  fmtno5faclem1  46332  fmtno5faclem2  46333  fmtno5faclem3  46334  fmtno5fac  46335  fmtno5nprm  46336  3ndvds4  46348  139prmALT  46349  31prm  46350  m5prm  46351  127prm  46352  m7prm  46353  m11nprm  46354  lighneallem2  46359  perfectALTVlem1  46474  perfectALTVlem2  46475  11t31e341  46485  2exp340mod341  46486  341fppr2  46487  8exp8mod9  46489  nfermltl8rev  46495  nfermltl2rev  46496  evengpoap3  46552  nnsum4primesevenALTV  46554  bgoldbtbndlem1  46558  bgoldbachlt  46566  tgblthelfgott  46568  nnpw2pmod  47353  dig1  47378  dignn0flhalflem2  47386  1aryfvalel  47406  itcoval1  47433  itcoval2  47434  ackval1  47451  ackval2  47452  ackval3  47453  ackendofnn0  47454  ackvalsucsucval  47458  ackval0012  47459  ackval1012  47460  ackval2012  47461  ackval3012  47462  ackval41a  47464  ackval42  47466  prstclevalOLD  47773  prstcocvalOLD  47776