Theorem 1nn0 12438

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

Syntax hints:   ∈ wcel 2106  1c1 11061  ℕ₀cn0 12422

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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11118

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-nn 12163  df-n0 12423

This theorem is referenced by:  peano2nn0  12462  deccl  12642  10nn0  12645  numsucc  12667  numadd  12674  numaddc  12675  11multnc  12695  6p5lem  12697  6p6e12  12701  7p5e12  12704  8p4e12  12709  9p2e11  12714  9p3e12  12715  10p10e20  12722  4t4e16  12726  5t2e10  12727  5t4e20  12729  6t3e18  12732  6t4e24  12733  7t3e21  12737  7t4e28  12738  8t3e24  12743  9t3e27  12750  9t9e81  12756  xnn0n0n1ge2b  13061  fz0to3un2pr  13553  elfzom1elp1fzo  13649  fzo0sn0fzo1  13671  fldiv4lem1div2  13752  expn1  13987  nn0expcl  13991  sqval  14030  nn0opthlem1  14178  fac2  14189  faclbnd4lem2  14204  bccl  14232  hashsng  14279  hashen1  14280  hashrabrsn  14282  1elfz0hash  14300  hashgt23el  14334  hashprlei  14379  hashtplei  14395  wrdred1hash  14461  pfx1  14603  repsw1  14683  cshw1  14722  s3fv1  14793  s4fv1  14797  pfx2  14848  repsw2  14851  repsw3  14852  wwlktovf  14857  relexp1g  14923  relexpaddg  14950  rtrclreclem1  14954  bcxmas  15731  climcndslem2  15746  climcnds  15747  arisum  15756  geoisum1  15775  geoisum1c  15776  mertenslem2  15781  fprodnn0cl  15851  nn0risefaccl  15916  bpoly1  15945  bpoly4  15953  fsumcube  15954  ege2le3  15983  ef4p  16006  efgt1p2  16007  efgt1p  16008  sin01gt0  16083  rpnnen2lem3  16109  dvds1  16212  3dvds2dec  16226  bitsmod  16327  bitsinv1lem  16332  sadadd2lem  16350  sadadd  16358  sadass  16362  smupp1  16371  smumul  16384  pcelnn  16753  pockthg  16789  vdwlem12  16875  prmo1  16920  dec5nprm  16949  dec2nprm  16950  modxp1i  16953  2exp8  16972  2exp11  16973  2exp16  16974  2expltfac  16976  5prm  16992  11prm  16998  13prm  16999  17prm  17000  19prm  17001  23prm  17002  prmlem2  17003  37prm  17004  43prm  17005  83prm  17006  139prm  17007  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  1259lem5  17018  1259prm  17019  2503lem1  17020  2503lem2  17021  2503lem3  17022  2503prm  17023  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  4001prm  17028  ocndx  17276  ocid  17277  basendxnocndx  17278  plendxnocndx  17279  dsndx  17280  dsid  17281  dsndxnn  17282  basendxltdsndx  17283  slotsdifdsndx  17289  unifndx  17290  unifid  17291  unifndxnn  17292  basendxltunifndx  17293  slotsdifunifndx  17296  odrngstr  17298  homndx  17306  homid  17307  ccondx  17308  ccoid  17309  slotsbhcdif  17310  slotsbhcdifOLD  17311  slotsdifplendx2  17312  slotsdifocndx  17313  imasvalstr  17347  prdsvalstr  17348  oppchomfvalOLD  17609  oppcbasOLD  17614  rescbasOLD  17727  resccoOLD  17731  rescabsOLD  17733  catstr  17859  ipostr  18432  smndex2dnrinv  18739  cycsubmcl  19008  psgnunilem2  19291  odcau  19400  lt6abl  19686  mgpdsOLD  19924  0ringnnzr  20212  sradsOLD  20714  cnfldstr  20835  cnfldfunALTOLD  20847  nn0srg  20904  thlbasOLD  21138  thlleOLD  21140  mvrid  21429  mvrf1  21431  mplcoe3  21476  psrbagsn  21508  evlslem1  21529  mhpvarcl  21575  pmatcollpw3fi1lem1  22172  chfacfscmulgsum  22246  chfacfpmmulfsupp  22249  chfacfpmmulgsum  22250  chfacfpmmulgsum2  22251  cpmadugsumlemB  22260  cpmadugsumlemF  22262  tuslemOLD  23656  tmslemOLD  23875  dscmet  23965  tnglemOLD  24034  ehl1eudis  24821  dveflem  25380  c1lip2  25399  itgpowd  25451  ply1remlem  25564  fta1glem1  25567  fta1blem  25570  plyid  25607  coeidp  25661  dgrid  25662  vieta1lem2  25708  vieta1  25709  aalioulem3  25731  aaliou2b  25738  dvtaylp  25766  taylthlem1  25769  taylthlem2  25770  radcnvlem2  25810  dvradcnv  25817  pserdvlem2  25824  logtayllem  26051  logtayl  26052  cxp1  26063  quart1cl  26241  quart1lem  26242  quart1  26243  quartlem1  26244  quartlem2  26245  leibpilem2  26328  log2ublem3  26335  log2ub  26336  birthday  26341  lgamcvg2  26441  gamp1  26444  issqf  26522  ppi2  26556  mumullem2  26566  sqff1o  26568  1sgmprm  26584  ppiublem2  26588  chtublem  26596  logfacbnd3  26608  logexprlim  26610  logfacrlim2  26611  perfectlem1  26614  perfectlem2  26615  bclbnd  26665  bpos1  26668  bposlem6  26674  lgsval  26686  2lgslem3a  26781  2lgslem3c  26783  rpvmasumlem  26872  log2sumbnd  26929  itvndx  27442  lngndx  27443  itvid  27444  lngid  27445  slotsinbpsd  27446  slotslnbpsd  27447  lngndxnitvndx  27448  trkgstr  27449  ttgvalOLD  27881  ttglemOLD  27883  ttgbasOLD  27885  ttgdsOLD  27892  eengstr  27992  edgfid  28002  edgfndx  28003  edgfndxnn  28004  edgfndxidOLD  28006  basendxltedgfndx  28007  baseltedgfOLD  28008  usgrexmplef  28270  cusgrsizeindb1  28461  wlk1ewlk  28651  usgr2pthlem  28774  uspgrn2crct  28816  crctcshwlkn0lem5  28822  rusgrnumwwlkl1  28976  rusgrnumwwlkb1  28980  clwwlkccatlem  28996  clwwlkinwwlk  29047  umgr2cwwkdifex  29072  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  konigsbergiedgw  29255  konigsberglem1  29259  konigsberglem2  29260  konigsberglem3  29261  konigsberglem4  29262  1kp2ke3k  29453  ex-exp  29457  ex-fac  29458  9p10ne21  29477  prmdvdsbc  31782  dpmul4  31840  threehalves  31841  1mhdrd  31842  s2f1  31871  omndmul2  31990  cycpm2tr  32038  freshmansdream  32137  drngdimgt0  32400  lmat22e12  32489  lmat22e21  32490  lmat22e22  32491  madjusmdetlem4  32500  nexple  32697  oddpwdc  33043  eulerpartlemd  33055  eulerpartlemgs2  33069  eulerpartlemn  33070  iwrdsplit  33076  fib0  33088  fib1  33089  fibp1  33090  sgnmulsgn  33238  sgnmulsgp  33239  plymulx0  33248  signstfveq0  33278  signsvvf  33280  signsvfn  33283  signshlen  33291  prodfzo03  33305  reprsuc  33317  breprexplemc  33334  hgt750lemd  33350  hgt750lem  33353  hgt750lem2  33354  hgt750leme  33360  usgrgt2cycl  33811  subfac1  33859  kur14lem9  33895  bccolsum  34398  nn0prpw  34871  12gcd5e1  40533  60gcd6e6  40534  60gcd7e1  40535  420gcd8e4  40536  12lcm5e60  40538  lcmineqlem11  40569  lcmineqlem18  40576  lcmineqlem22  40580  lcmineqlem  40582  3exp7  40583  3lexlogpow5ineq1  40584  3lexlogpow5ineq2  40585  3lexlogpow5ineq4  40586  3lexlogpow5ineq5  40590  dvrelogpow2b  40598  aks4d1p1p2  40600  aks4d1p1p4  40601  aks4d1p1p6  40603  aks4d1p1p7  40604  aks4d1p1p5  40605  aks4d1p1  40606  aks4d1p3  40608  2np3bcnp1  40625  2ap1caineq  40626  sticksstones22  40649  factwoffsmonot  40688  235t711  40863  ex-decpmul  40864  nn0rppwr  40877  fltnltalem  41058  3cubeslem3l  41067  3cubeslem3r  41068  pell1qr1  41252  rmspecfund  41290  jm2.23  41378  jm2.27c  41389  areaquad  41608  resqrtvalex  42039  imsqrtvalex  42040  brfvidRP  42082  brfvrcld  42085  corclrcl  42101  dftrcl3  42114  dfrtrcl3  42127  fvrtrcllb1d  42131  corcltrcl  42133  cotrclrcl  42136  inductionexd  42549  radcnvrat  42716  binomcxplemnn0  42751  binomcxplemfrat  42753  binomcxplemnotnn0  42758  rexanuz2nf  43848  wallispilem2  44427  wallispilem5  44430  wallispi2lem2  44433  stirlinglem5  44439  stirlinglem7  44441  stirlinglem10  44444  stirlinglem11  44445  fourierdlem48  44515  iccpartigtl  45735  iccpartlt  45736  iccpartgel  45741  fmtnosqrt  45851  fmtno1  45853  fmtno2  45862  fmtno5lem1  45865  fmtno5lem2  45866  fmtno5lem3  45867  fmtno5lem4  45868  fmtno5  45869  257prm  45873  fmtnofac1  45882  fmtno4prmfac  45884  fmtno4prmfac193  45885  fmtno4nprmfac193  45886  fmtno5faclem1  45891  fmtno5faclem2  45892  fmtno5faclem3  45893  fmtno5fac  45894  fmtno5nprm  45895  3ndvds4  45907  139prmALT  45908  31prm  45909  m5prm  45910  127prm  45911  m7prm  45912  m11nprm  45913  lighneallem2  45918  perfectALTVlem1  46033  perfectALTVlem2  46034  11t31e341  46044  2exp340mod341  46045  341fppr2  46046  8exp8mod9  46048  nfermltl8rev  46054  nfermltl2rev  46055  evengpoap3  46111  nnsum4primesevenALTV  46113  bgoldbtbndlem1  46117  bgoldbachlt  46125  tgblthelfgott  46127  nnpw2pmod  46789  dig1  46814  dignn0flhalflem2  46822  1aryfvalel  46842  itcoval1  46869  itcoval2  46870  ackval1  46887  ackval2  46888  ackval3  46889  ackendofnn0  46890  ackvalsucsucval  46894  ackval0012  46895  ackval1012  46896  ackval2012  46897  ackval3012  46898  ackval41a  46900  ackval42  46902  prstclevalOLD  47209  prstcocvalOLD  47212