Theorem 1nn0 12295

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

Syntax hints:   ∈ wcel 2104  1c1 10918  ℕ₀cn0 12279

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-n0 12280

This theorem is referenced by:  peano2nn0  12319  deccl  12498  10nn0  12501  numsucc  12523  numadd  12530  numaddc  12531  11multnc  12551  6p5lem  12553  6p6e12  12557  7p5e12  12560  8p4e12  12565  9p2e11  12570  9p3e12  12571  10p10e20  12578  4t4e16  12582  5t2e10  12583  5t4e20  12585  6t3e18  12588  6t4e24  12589  7t3e21  12593  7t4e28  12594  8t3e24  12599  9t3e27  12606  9t9e81  12612  xnn0n0n1ge2b  12913  fz0to3un2pr  13404  elfzom1elp1fzo  13500  fzo0sn0fzo1  13522  fldiv4lem1div2  13603  expn1  13838  nn0expcl  13842  sqval  13881  nn0opthlem1  14028  fac2  14039  faclbnd4lem2  14054  bccl  14082  hashsng  14129  hashen1  14130  hashrabrsn  14132  1elfz0hash  14150  hashgt23el  14184  hashprlei  14227  hashtplei  14243  wrdred1hash  14309  pfx1  14461  repsw1  14541  cshw1  14580  s3fv1  14650  s4fv1  14654  pfx2  14705  repsw2  14708  repsw3  14709  wwlktovf  14716  relexp1g  14782  relexpaddg  14809  rtrclreclem1  14813  bcxmas  15592  climcndslem2  15607  climcnds  15608  arisum  15617  geoisum1  15636  geoisum1c  15637  mertenslem2  15642  fprodnn0cl  15712  nn0risefaccl  15777  bpoly1  15806  bpoly4  15814  fsumcube  15815  ege2le3  15844  ef4p  15867  efgt1p2  15868  efgt1p  15869  sin01gt0  15944  rpnnen2lem3  15970  dvds1  16073  3dvds2dec  16087  bitsmod  16188  bitsinv1lem  16193  sadadd2lem  16211  sadadd  16219  sadass  16223  smupp1  16232  smumul  16245  pcelnn  16616  pockthg  16652  vdwlem12  16738  prmo1  16783  dec5nprm  16812  dec2nprm  16813  modxp1i  16816  2exp8  16835  2exp11  16836  2exp16  16837  2expltfac  16839  5prm  16855  11prm  16861  13prm  16862  17prm  16863  19prm  16864  23prm  16865  prmlem2  16866  37prm  16867  43prm  16868  83prm  16869  139prm  16870  163prm  16871  317prm  16872  631prm  16873  1259lem1  16877  1259lem2  16878  1259lem3  16879  1259lem4  16880  1259lem5  16881  1259prm  16882  2503lem1  16883  2503lem2  16884  2503lem3  16885  2503prm  16886  4001lem1  16887  4001lem2  16888  4001lem3  16889  4001lem4  16890  4001prm  16891  ocndx  17136  ocid  17137  basendxnocndx  17138  plendxnocndx  17139  dsndx  17140  dsid  17141  dsndxnn  17142  basendxltdsndx  17143  slotsdifdsndx  17149  unifndx  17150  unifid  17151  unifndxnn  17152  basendxltunifndx  17153  slotsdifunifndx  17156  odrngstr  17158  homndx  17166  homid  17167  ccondx  17168  ccoid  17169  slotsbhcdif  17170  slotsbhcdifOLD  17171  slotsdifplendx2  17172  slotsdifocndx  17173  imasvalstr  17207  prdsvalstr  17208  oppchomfvalOLD  17469  oppcbasOLD  17474  rescbasOLD  17587  resccoOLD  17591  rescabsOLD  17593  catstr  17719  ipostr  18292  smndex2dnrinv  18599  cycsubmcl  18865  psgnunilem2  19148  odcau  19254  lt6abl  19541  mgpdsOLD  19779  sradsOLD  20501  0ringnnzr  20585  cnfldstr  20644  cnfldfunALTOLD  20656  nn0srg  20713  thlbasOLD  20947  thlleOLD  20949  mvrid  21237  mvrf1  21239  mplcoe3  21284  psrbagsn  21316  evlslem1  21337  mhpvarcl  21383  pmatcollpw3fi1lem1  21980  chfacfscmulgsum  22054  chfacfpmmulfsupp  22057  chfacfpmmulgsum  22058  chfacfpmmulgsum2  22059  cpmadugsumlemB  22068  cpmadugsumlemF  22070  tuslemOLD  23464  tmslemOLD  23683  dscmet  23773  tnglemOLD  23842  ehl1eudis  24629  dveflem  25188  c1lip2  25207  itgpowd  25259  ply1remlem  25372  fta1glem1  25375  fta1blem  25378  plyid  25415  coeidp  25469  dgrid  25470  vieta1lem2  25516  vieta1  25517  aalioulem3  25539  aaliou2b  25546  dvtaylp  25574  taylthlem1  25577  taylthlem2  25578  radcnvlem2  25618  dvradcnv  25625  pserdvlem2  25632  logtayllem  25859  logtayl  25860  cxp1  25871  quart1cl  26049  quart1lem  26050  quart1  26051  quartlem1  26052  quartlem2  26053  leibpilem2  26136  log2ublem3  26143  log2ub  26144  birthday  26149  lgamcvg2  26249  gamp1  26252  issqf  26330  ppi2  26364  mumullem2  26374  sqff1o  26376  1sgmprm  26392  ppiublem2  26396  chtublem  26404  logfacbnd3  26416  logexprlim  26418  logfacrlim2  26419  perfectlem1  26422  perfectlem2  26423  bclbnd  26473  bpos1  26476  bposlem6  26482  lgsval  26494  2lgslem3a  26589  2lgslem3c  26591  rpvmasumlem  26680  log2sumbnd  26737  itvndx  26843  lngndx  26844  itvid  26845  lngid  26846  slotsinbpsd  26847  slotslnbpsd  26848  lngndxnitvndx  26849  trkgstr  26850  ttgvalOLD  27282  ttglemOLD  27284  ttgbasOLD  27286  ttgdsOLD  27293  eengstr  27393  edgfid  27403  edgfndx  27404  edgfndxnn  27405  edgfndxidOLD  27407  basendxltedgfndx  27408  baseltedgfOLD  27409  usgrexmplef  27671  cusgrsizeindb1  27862  wlk1ewlk  28052  usgr2pthlem  28176  uspgrn2crct  28218  crctcshwlkn0lem5  28224  rusgrnumwwlkl1  28378  rusgrnumwwlkb1  28382  clwwlkccatlem  28398  clwwlkinwwlk  28449  umgr2cwwkdifex  28474  upgr3v3e3cycl  28589  upgr4cycl4dv4e  28594  konigsbergiedgw  28657  konigsberglem1  28661  konigsberglem2  28662  konigsberglem3  28663  konigsberglem4  28664  1kp2ke3k  28855  ex-exp  28859  ex-fac  28860  9p10ne21  28879  prmdvdsbc  31175  dpmul4  31233  threehalves  31234  1mhdrd  31235  s2f1  31264  omndmul2  31383  cycpm2tr  31431  freshmansdream  31529  drngdimgt0  31746  lmat22e12  31814  lmat22e21  31815  lmat22e22  31816  madjusmdetlem4  31825  nexple  32022  oddpwdc  32366  eulerpartlemd  32378  eulerpartlemgs2  32392  eulerpartlemn  32393  iwrdsplit  32399  fib0  32411  fib1  32412  fibp1  32413  sgnmulsgn  32561  sgnmulsgp  32562  plymulx0  32571  signstfveq0  32601  signsvvf  32603  signsvfn  32606  signshlen  32614  prodfzo03  32628  reprsuc  32640  breprexplemc  32657  hgt750lemd  32673  hgt750lem  32676  hgt750lem2  32677  hgt750leme  32683  usgrgt2cycl  33137  subfac1  33185  kur14lem9  33221  bccolsum  33750  nn0prpw  34557  12gcd5e1  40053  60gcd6e6  40054  60gcd7e1  40055  420gcd8e4  40056  12lcm5e60  40058  lcmineqlem11  40089  lcmineqlem18  40096  lcmineqlem22  40100  lcmineqlem  40102  3exp7  40103  3lexlogpow5ineq1  40104  3lexlogpow5ineq2  40105  3lexlogpow5ineq4  40106  3lexlogpow5ineq5  40110  dvrelogpow2b  40118  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p3  40128  2np3bcnp1  40142  2ap1caineq  40143  sticksstones22  40166  factwoffsmonot  40205  235t711  40356  ex-decpmul  40357  nn0rppwr  40370  fltnltalem  40536  3cubeslem3l  40545  3cubeslem3r  40546  pell1qr1  40730  rmspecfund  40768  jm2.23  40856  jm2.27c  40867  areaquad  41085  resqrtvalex  41291  imsqrtvalex  41292  brfvidRP  41334  brfvrcld  41337  corclrcl  41353  dftrcl3  41366  dfrtrcl3  41379  fvrtrcllb1d  41383  corcltrcl  41385  cotrclrcl  41388  inductionexd  41803  radcnvrat  41970  binomcxplemnn0  42005  binomcxplemfrat  42007  binomcxplemnotnn0  42012  wallispilem2  43656  wallispilem5  43659  wallispi2lem2  43662  stirlinglem5  43668  stirlinglem7  43670  stirlinglem10  43673  stirlinglem11  43674  fourierdlem48  43744  iccpartigtl  44933  iccpartlt  44934  iccpartgel  44939  fmtnosqrt  45049  fmtno1  45051  fmtno2  45060  fmtno5lem1  45063  fmtno5lem2  45064  fmtno5lem3  45065  fmtno5lem4  45066  fmtno5  45067  257prm  45071  fmtnofac1  45080  fmtno4prmfac  45082  fmtno4prmfac193  45083  fmtno4nprmfac193  45084  fmtno5faclem1  45089  fmtno5faclem2  45090  fmtno5faclem3  45091  fmtno5fac  45092  fmtno5nprm  45093  3ndvds4  45105  139prmALT  45106  31prm  45107  m5prm  45108  127prm  45109  m7prm  45110  m11nprm  45111  lighneallem2  45116  perfectALTVlem1  45231  perfectALTVlem2  45232  11t31e341  45242  2exp340mod341  45243  341fppr2  45244  8exp8mod9  45246  nfermltl8rev  45252  nfermltl2rev  45253  evengpoap3  45309  nnsum4primesevenALTV  45311  bgoldbtbndlem1  45315  bgoldbachlt  45323  tgblthelfgott  45325  nnpw2pmod  45987  dig1  46012  dignn0flhalflem2  46020  1aryfvalel  46040  itcoval1  46067  itcoval2  46068  ackval1  46085  ackval2  46086  ackval3  46087  ackendofnn0  46088  ackvalsucsucval  46092  ackval0012  46093  ackval1012  46094  ackval2012  46095  ackval3012  46096  ackval41a  46098  ackval42  46100  prstclevalOLD  46408  prstcocvalOLD  46411