Theorem 1nn0 12232

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

Syntax hints:   ∈ wcel 2109  1c1 10856  ℕ₀cn0 12216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-nn 11957  df-n0 12217

This theorem is referenced by:  peano2nn0  12256  deccl  12434  10nn0  12437  numsucc  12459  numadd  12466  numaddc  12467  11multnc  12487  6p5lem  12489  6p6e12  12493  7p5e12  12496  8p4e12  12501  9p2e11  12506  9p3e12  12507  10p10e20  12514  4t4e16  12518  5t2e10  12519  5t4e20  12521  6t3e18  12524  6t4e24  12525  7t3e21  12529  7t4e28  12530  8t3e24  12535  9t3e27  12542  9t9e81  12548  xnn0n0n1ge2b  12849  fz0to3un2pr  13340  elfzom1elp1fzo  13435  fzo0sn0fzo1  13457  fldiv4lem1div2  13538  expn1  13773  nn0expcl  13777  sqval  13816  nn0opthlem1  13963  fac2  13974  faclbnd4lem2  13989  bccl  14017  hashsng  14065  hashen1  14066  hashrabrsn  14068  1elfz0hash  14086  hashgt23el  14120  hashprlei  14163  hashtplei  14179  wrdred1hash  14245  pfx1  14397  repsw1  14477  cshw1  14516  s3fv1  14586  s4fv1  14590  pfx2  14641  repsw2  14644  repsw3  14645  wwlktovf  14652  relexp1g  14718  relexpaddg  14745  rtrclreclem1  14749  bcxmas  15528  climcndslem2  15543  climcnds  15544  arisum  15553  geoisum1  15572  geoisum1c  15573  mertenslem2  15578  fprodnn0cl  15648  nn0risefaccl  15713  bpoly1  15742  bpoly4  15750  fsumcube  15751  ege2le3  15780  ef4p  15803  efgt1p2  15804  efgt1p  15805  sin01gt0  15880  rpnnen2lem3  15906  dvds1  16009  3dvds2dec  16023  bitsmod  16124  bitsinv1lem  16129  sadadd2lem  16147  sadadd  16155  sadass  16159  smupp1  16168  smumul  16181  pcelnn  16552  pockthg  16588  vdwlem12  16674  prmo1  16719  dec5nprm  16748  dec2nprm  16749  modxp1i  16752  2exp8  16771  2exp11  16772  2exp16  16773  2expltfac  16775  5prm  16791  11prm  16797  13prm  16798  17prm  16799  19prm  16800  23prm  16801  prmlem2  16802  37prm  16803  43prm  16804  83prm  16805  139prm  16806  163prm  16807  317prm  16808  631prm  16809  1259lem1  16813  1259lem2  16814  1259lem3  16815  1259lem4  16816  1259lem5  16817  1259prm  16818  2503lem1  16819  2503lem2  16820  2503lem3  16821  2503prm  16822  4001lem1  16823  4001lem2  16824  4001lem3  16825  4001lem4  16826  4001prm  16827  ocndx  17072  ocid  17073  basendxnocndx  17074  plendxnocndx  17075  dsndx  17076  dsid  17077  dsndxnn  17078  basendxltdsndx  17079  slotsdifdsndx  17085  unifndx  17086  unifid  17087  unifndxnn  17088  basendxltunifndx  17089  slotsdifunifndx  17092  odrngstr  17094  homndx  17102  homid  17103  ccondx  17104  ccoid  17105  slotsbhcdif  17106  slotsbhcdifOLD  17107  slotsdifplendx2  17108  slotsdifocndx  17109  imasvalstr  17143  prdsvalstr  17144  oppchomfvalOLD  17405  oppcbasOLD  17410  rescbasOLD  17523  resccoOLD  17527  rescabsOLD  17529  catstr  17655  ipostr  18228  smndex2dnrinv  18535  cycsubmcl  18801  psgnunilem2  19084  odcau  19190  lt6abl  19477  mgpdsOLD  19715  sradsOLD  20437  0ringnnzr  20521  cnfldstr  20580  cnfldfunOLD  20591  nn0srg  20649  thlbasOLD  20883  thlleOLD  20885  mvrid  21173  mvrf1  21175  mplcoe3  21220  psrbagsn  21252  evlslem1  21273  mhpvarcl  21319  pmatcollpw3fi1lem1  21916  chfacfscmulgsum  21990  chfacfpmmulfsupp  21993  chfacfpmmulgsum  21994  chfacfpmmulgsum2  21995  cpmadugsumlemB  22004  cpmadugsumlemF  22006  tuslemOLD  23400  tmslemOLD  23619  dscmet  23709  tnglemOLD  23778  ehl1eudis  24565  dveflem  25124  c1lip2  25143  itgpowd  25195  ply1remlem  25308  fta1glem1  25311  fta1blem  25314  plyid  25351  coeidp  25405  dgrid  25406  vieta1lem2  25452  vieta1  25453  aalioulem3  25475  aaliou2b  25482  dvtaylp  25510  taylthlem1  25513  taylthlem2  25514  radcnvlem2  25554  dvradcnv  25561  pserdvlem2  25568  logtayllem  25795  logtayl  25796  cxp1  25807  quart1cl  25985  quart1lem  25986  quart1  25987  quartlem1  25988  quartlem2  25989  leibpilem2  26072  log2ublem3  26079  log2ub  26080  birthday  26085  lgamcvg2  26185  gamp1  26188  issqf  26266  ppi2  26300  mumullem2  26310  sqff1o  26312  1sgmprm  26328  ppiublem2  26332  chtublem  26340  logfacbnd3  26352  logexprlim  26354  logfacrlim2  26355  perfectlem1  26358  perfectlem2  26359  bclbnd  26409  bpos1  26412  bposlem6  26418  lgsval  26430  2lgslem3a  26525  2lgslem3c  26527  rpvmasumlem  26616  log2sumbnd  26673  itvndx  26779  lngndx  26780  itvid  26781  lngid  26782  slotsinbpsd  26783  slotslnbpsd  26784  lngndxnitvndx  26785  trkgstr  26786  ttgvalOLD  27218  ttglemOLD  27220  ttgbasOLD  27222  ttgdsOLD  27229  eengstr  27329  edgfid  27339  edgfndx  27340  edgfndxnn  27341  edgfndxidOLD  27343  basendxltedgfndx  27344  baseltedgfOLD  27345  usgrexmplef  27607  cusgrsizeindb1  27798  wlk1ewlk  27987  usgr2pthlem  28110  uspgrn2crct  28152  crctcshwlkn0lem5  28158  rusgrnumwwlkl1  28312  rusgrnumwwlkb1  28316  clwwlkccatlem  28332  clwwlkinwwlk  28383  umgr2cwwkdifex  28408  upgr3v3e3cycl  28523  upgr4cycl4dv4e  28528  konigsbergiedgw  28591  konigsberglem1  28595  konigsberglem2  28596  konigsberglem3  28597  konigsberglem4  28598  1kp2ke3k  28789  ex-exp  28793  ex-fac  28794  9p10ne21  28813  prmdvdsbc  31109  dpmul4  31167  threehalves  31168  1mhdrd  31169  s2f1  31198  omndmul2  31317  cycpm2tr  31365  freshmansdream  31463  drngdimgt0  31680  lmat22e12  31748  lmat22e21  31749  lmat22e22  31750  madjusmdetlem4  31759  nexple  31956  oddpwdc  32300  eulerpartlemd  32312  eulerpartlemgs2  32326  eulerpartlemn  32327  iwrdsplit  32333  fib0  32345  fib1  32346  fibp1  32347  sgnmulsgn  32495  sgnmulsgp  32496  plymulx0  32505  signstfveq0  32535  signsvvf  32537  signsvfn  32540  signshlen  32548  prodfzo03  32562  reprsuc  32574  breprexplemc  32591  hgt750lemd  32607  hgt750lem  32610  hgt750lem2  32611  hgt750leme  32617  usgrgt2cycl  33071  subfac1  33119  kur14lem9  33155  bccolsum  33684  nn0prpw  34491  12gcd5e1  39991  60gcd6e6  39992  60gcd7e1  39993  420gcd8e4  39994  12lcm5e60  39996  lcmineqlem11  40027  lcmineqlem18  40034  lcmineqlem22  40038  lcmineqlem  40040  3exp7  40041  3lexlogpow5ineq1  40042  3lexlogpow5ineq2  40043  3lexlogpow5ineq4  40044  3lexlogpow5ineq5  40048  dvrelogpow2b  40056  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p3  40066  2np3bcnp1  40080  2ap1caineq  40081  sticksstones22  40104  factwoffsmonot  40143  235t711  40299  ex-decpmul  40300  nn0rppwr  40313  fltnltalem  40479  3cubeslem3l  40488  3cubeslem3r  40489  pell1qr1  40673  rmspecfund  40711  jm2.23  40798  jm2.27c  40809  areaquad  41027  resqrtvalex  41206  imsqrtvalex  41207  brfvidRP  41249  brfvrcld  41252  corclrcl  41268  dftrcl3  41281  dfrtrcl3  41294  fvrtrcllb1d  41298  corcltrcl  41300  cotrclrcl  41303  inductionexd  41718  radcnvrat  41885  binomcxplemnn0  41920  binomcxplemfrat  41922  binomcxplemnotnn0  41927  wallispilem2  43561  wallispilem5  43564  wallispi2lem2  43567  stirlinglem5  43573  stirlinglem7  43575  stirlinglem10  43578  stirlinglem11  43579  fourierdlem48  43649  iccpartigtl  44827  iccpartlt  44828  iccpartgel  44833  fmtnosqrt  44943  fmtno1  44945  fmtno2  44954  fmtno5lem1  44957  fmtno5lem2  44958  fmtno5lem3  44959  fmtno5lem4  44960  fmtno5  44961  257prm  44965  fmtnofac1  44974  fmtno4prmfac  44976  fmtno4prmfac193  44977  fmtno4nprmfac193  44978  fmtno5faclem1  44983  fmtno5faclem2  44984  fmtno5faclem3  44985  fmtno5fac  44986  fmtno5nprm  44987  3ndvds4  44999  139prmALT  45000  31prm  45001  m5prm  45002  127prm  45003  m7prm  45004  m11nprm  45005  lighneallem2  45010  perfectALTVlem1  45125  perfectALTVlem2  45126  11t31e341  45136  2exp340mod341  45137  341fppr2  45138  8exp8mod9  45140  nfermltl8rev  45146  nfermltl2rev  45147  evengpoap3  45203  nnsum4primesevenALTV  45205  bgoldbtbndlem1  45209  bgoldbachlt  45217  tgblthelfgott  45219  nnpw2pmod  45881  dig1  45906  dignn0flhalflem2  45914  1aryfvalel  45934  itcoval1  45961  itcoval2  45962  ackval1  45979  ackval2  45980  ackval3  45981  ackendofnn0  45982  ackvalsucsucval  45986  ackval0012  45987  ackval1012  45988  ackval2012  45989  ackval3012  45990  ackval41a  45992  ackval42  45994  prstclevalOLD  46302  prstcocvalOLD  46305