Theorem 1nn0 12458

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

Syntax hints:   ∈ wcel 2109  1c1 11069  ℕ₀cn0 12442

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  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 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  peano2nn0  12482  deccl  12664  10nn0  12667  numsucc  12689  numadd  12696  numaddc  12697  11multnc  12717  6p5lem  12719  6p6e12  12723  7p5e12  12726  8p4e12  12731  9p2e11  12736  9p3e12  12737  10p10e20  12744  4t4e16  12748  5t2e10  12749  5t4e20  12751  6t3e18  12754  6t4e24  12755  7t3e21  12759  7t4e28  12760  8t3e24  12765  9t3e27  12772  9t9e81  12778  xnn0n0n1ge2b  13092  fz0to3un2pr  13590  elfzom1elp1fzo  13693  fzo0sn0fzo1  13716  fvf1tp  13751  fldiv4lem1div2  13799  expn1  14036  nn0expcl  14040  sqval  14079  nn0opthlem1  14233  fac2  14244  faclbnd4lem2  14259  bccl  14287  hashsng  14334  hashen1  14335  hashrabrsn  14337  1elfz0hash  14355  hashgt23el  14389  hashprlei  14433  hashtplei  14449  tpf1ofv1  14462  tpfo  14465  wrdred1hash  14526  pfx1  14668  repsw1  14748  cshw1  14787  s3fv1  14858  s4fv1  14862  pfx2  14913  repsw2  14916  repsw3  14917  wwlktovf  14922  relexp1g  14992  relexpaddg  15019  rtrclreclem1  15023  bcxmas  15801  climcndslem2  15816  climcnds  15817  arisum  15826  geoisum1  15845  geoisum1c  15846  mertenslem2  15851  fprodnn0cl  15923  nn0risefaccl  15988  bpoly1  16017  bpoly4  16025  fsumcube  16026  ege2le3  16056  ef4p  16081  efgt1p2  16082  efgt1p  16083  sin01gt0  16158  rpnnen2lem3  16184  dvds1  16289  3dvds2dec  16303  5ndvds6  16384  bitsmod  16406  bitsinv1lem  16411  sadadd2lem  16429  sadadd  16437  sadass  16441  smupp1  16450  smumul  16463  nn0rppwr  16531  prmdvdsbc  16696  pcelnn  16841  pockthg  16877  vdwlem12  16963  prmo1  17008  dec5nprm  17037  dec2nprm  17038  modxp1i  17041  2exp8  17059  2exp11  17060  2exp16  17061  2expltfac  17063  5prm  17079  11prm  17085  13prm  17086  17prm  17087  19prm  17088  23prm  17089  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  ocndx  17344  ocid  17345  basendxnocndx  17346  plendxnocndx  17347  dsndx  17348  dsid  17349  dsndxnn  17350  basendxltdsndx  17351  slotsdifdsndx  17357  unifndx  17358  unifid  17359  unifndxnn  17360  basendxltunifndx  17361  slotsdifunifndx  17364  odrngstr  17366  homndx  17374  homid  17375  ccondx  17376  ccoid  17377  slotsbhcdif  17378  slotsdifplendx2  17379  slotsdifocndx  17380  imasvalstr  17414  prdsvalstr  17415  catstr  17922  ipostr  18488  smndex2dnrinv  18842  cycsubmcl  19133  psgnunilem2  19425  odcau  19534  lt6abl  19825  0ringnnzr  20434  cnfldstr  21266  cnfldstrOLD  21281  nn0srg  21354  freshmansdream  21484  mvrid  21893  mvrf1  21895  mplcoe3  21945  psrbagsn  21970  evlslem1  21989  mhpvarcl  22035  psdcl  22048  psdmul  22053  psdmvr  22056  pmatcollpw3fi1lem1  22673  chfacfscmulgsum  22747  chfacfpmmulfsupp  22750  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cpmadugsumlemB  22761  cpmadugsumlemF  22763  dscmet  24460  ehl1eudis  25320  dveflem  25883  c1lip2  25903  itgpowd  25957  ply1remlem  26070  fta1glem1  26073  fta1blem  26076  plyid  26114  coeidp  26169  dgrid  26170  vieta1lem2  26219  vieta1  26220  aalioulem3  26242  aaliou2b  26249  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  radcnvlem2  26323  dvradcnv  26330  pserdvlem2  26338  logtayllem  26568  logtayl  26569  cxp1  26580  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  leibpilem2  26851  log2ublem3  26858  log2ub  26859  birthday  26864  lgamcvg2  26965  gamp1  26968  issqf  27046  ppi2  27080  mumullem2  27090  sqff1o  27092  1sgmprm  27110  ppiublem2  27114  chtublem  27122  logfacbnd3  27134  logexprlim  27136  logfacrlim2  27137  perfectlem1  27140  perfectlem2  27141  bclbnd  27191  bpos1  27194  bposlem6  27200  lgsval  27212  2lgslem3a  27307  2lgslem3c  27309  rpvmasumlem  27398  log2sumbnd  27455  itvndx  28364  lngndx  28365  itvid  28366  lngid  28367  slotsinbpsd  28368  slotslnbpsd  28369  lngndxnitvndx  28370  trkgstr  28371  eengstr  28907  edgfid  28917  edgfndx  28918  edgfndxnn  28919  basendxltedgfndx  28921  usgrexmplef  29186  cusgrsizeindb1  29378  wlk1ewlk  29568  usgr2pthlem  29693  uspgrn2crct  29738  crctcshwlkn0lem5  29744  rusgrnumwwlkl1  29898  rusgrnumwwlkb1  29902  clwwlkccatlem  29918  clwwlkinwwlk  29969  umgr2cwwkdifex  29994  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem4  30184  1kp2ke3k  30375  ex-exp  30379  ex-fac  30380  9p10ne21  30399  sgnmulsgn  32767  sgnmulsgp  32768  nexple  32769  dpmul4  32834  threehalves  32835  1mhdrd  32836  s2f1  32866  omndmul2  33026  cycpm2tr  33076  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1dg1rt  33548  coe1vr1  33557  deg1vr  33558  drngdimgt0  33614  rtelextdg2lem  33716  fldext2chn  33718  constrdircl  33755  iconstr  33756  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminply  33778  lmat22e12  33809  lmat22e21  33810  lmat22e22  33811  madjusmdetlem4  33820  oddpwdc  34345  eulerpartlemd  34357  eulerpartlemgs2  34371  eulerpartlemn  34372  iwrdsplit  34378  fib0  34390  fib1  34391  fibp1  34392  plymulx0  34538  signstfveq0  34568  signsvvf  34570  signsvfn  34573  signshlen  34581  prodfzo03  34594  reprsuc  34606  breprexplemc  34623  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  usgrgt2cycl  35117  subfac1  35165  kur14lem9  35201  bccolsum  35726  nn0prpw  36311  12gcd5e1  41991  60gcd6e6  41992  60gcd7e1  41993  420gcd8e4  41994  12lcm5e60  41996  lcmineqlem11  42027  lcmineqlem18  42034  lcmineqlem22  42038  lcmineqlem  42040  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq5  42048  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks6d1c1p8  42103  aks6d1c5lem3  42125  2np3bcnp1  42132  2ap1caineq  42133  sticksstones22  42156  aks6d1c6lem1  42158  aks6d1c7lem1  42168  aks6d1c7  42172  235t711  42293  ex-decpmul  42294  fltnltalem  42650  sum9cubes  42660  3cubeslem3l  42674  3cubeslem3r  42675  pell1qr1  42859  rmspecfund  42897  jm2.23  42985  jm2.27c  42996  areaquad  43205  resqrtvalex  43634  imsqrtvalex  43635  brfvidRP  43677  brfvrcld  43680  corclrcl  43696  dftrcl3  43709  dfrtrcl3  43722  fvrtrcllb1d  43726  corcltrcl  43728  cotrclrcl  43731  inductionexd  44144  radcnvrat  44303  binomcxplemnn0  44338  binomcxplemfrat  44340  binomcxplemnotnn0  44345  rexanuz2nf  45488  wallispilem2  46064  wallispilem5  46067  wallispi2lem2  46070  stirlinglem5  46076  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  fourierdlem48  46152  ormkglobd  46873  iccpartigtl  47424  iccpartlt  47425  iccpartgel  47430  fmtnosqrt  47540  fmtno1  47542  fmtno2  47551  fmtno5lem1  47554  fmtno5lem2  47555  fmtno5lem3  47556  fmtno5lem4  47557  fmtno5  47558  257prm  47562  fmtnofac1  47571  fmtno4prmfac  47573  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  fmtno5faclem1  47580  fmtno5faclem2  47581  fmtno5faclem3  47582  fmtno5fac  47583  fmtno5nprm  47584  3ndvds4  47596  139prmALT  47597  31prm  47598  m5prm  47599  127prm  47600  m7prm  47601  m11nprm  47602  lighneallem2  47607  perfectALTVlem1  47722  perfectALTVlem2  47723  11t31e341  47733  2exp340mod341  47734  341fppr2  47735  8exp8mod9  47737  nfermltl8rev  47743  nfermltl2rev  47744  evengpoap3  47800  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  bgoldbachlt  47814  tgblthelfgott  47816  cycl3grtri  47946  stgr1  47960  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgprismgriedgdmss  48043  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem9  48093  gpgprismgr4cycllem10  48094  nnpw2pmod  48572  dig1  48597  dignn0flhalflem2  48605  1aryfvalel  48625  itcoval1  48652  itcoval2  48653  ackval1  48670  ackval2  48671  ackval3  48672  ackendofnn0  48673  ackvalsucsucval  48677  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval41a  48683  ackval42  48685