Theorem 1nn0 12626

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

This proof depends on syntax axioms:   ∈ wcel 2144  1c1 11205  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-nn 12340  df-n0 12611

This theorem is used by:  peano2nn0  12650  deccl  12833  11nn0  12834  12nn0  12835  16nn0  12836  10nn0  12840  11nn  12843  numsucc  12863  numadd  12870  numaddc  12871  11multnc  12891  6p5lem  12893  6p6e12  12897  7p5e12  12900  8p4e12  12905  9p2e11  12910  9p3e12  12911  10p10e20  12918  4t4e16  12922  5t2e10  12923  5t4e20  12925  6t3e18  12928  6t4e24  12929  7t3e21  12933  7t4e28  12934  8t3e24  12939  9t3e27  12946  9t9e81  12952  1lt10  12963  xnn0n0n1ge2b  13265  fz0to3un2pr  13767  elfzom1elp1fzo  13871  fzo0sn0fzo1  13894  fvf1tp  13933  fldiv4lem1div2  13981  expn1  14218  nn0expcl  14222  sqval  14261  nn0opthlem1  14416  fac2  14427  faclbnd4lem2  14442  bccl  14470  hashsng  14517  hashen1  14518  hashrabrsn  14520  1elfz0hash  14538  hashgt23el  14573  hashprlei  14617  hashtplei  14633  tpf1ofv1  14646  tpfo  14649  wrdred1hash  14710  pfx1  14857  repsw1  14939  cshw1  14978  s3fv1  15049  s4fv1  15053  pfx2  15104  repsw2  15109  repsw3  15110  wwlktovf  15115  relexp1g  15185  relexpaddg  15212  rtrclreclem1  15216  sgnmulsgn  15268  bcxmas  16010  climcndslem2  16025  climcnds  16026  arisum  16035  geoisum1  16054  geoisum1c  16055  mertenslem2  16060  fprodnn0cl  16130  nn0risefaccl  16195  bpoly1  16223  bpoly4  16231  fsumcube  16232  ege2le3  16262  ef4p  16287  efgt1p2  16288  efgt1p  16289  sin01gt0  16364  rpnnen2lem3  16390  dvds1  16495  3dvds2dec  16509  5ndvds6  16590  bitsmod  16612  bitsinv1lem  16617  sadadd2lem  16635  sadadd  16643  sadass  16647  smupp1  16656  smumul  16669  nn0rppwr  16741  prmdvdsbc  16908  pcelnn  17054  pockthg  17090  vdwlem12  17176  prmo1  17221  dec5nprm  17250  dec2nprm  17251  modxp1i  17254  2exp8  17272  2exp11  17273  2exp16  17274  2expltfac  17276  5prm  17292  11prm  17299  13prm  17300  17prm  17301  19prm  17302  23prm  17303  prmlem2  17304  37prm  17305  43prm  17306  83prm  17307  139prm  17308  163prm  17309  317prm  17310  631prm  17311  1259lem1  17315  1259lem2  17316  1259lem3  17317  1259lem4  17318  1259lem5  17319  1259prm  17320  2503lem1  17321  2503lem2  17322  2503lem3  17323  2503prm  17324  4001lem1  17325  4001lem2  17326  4001lem3  17327  4001lem4  17328  4001prm  17329  ocndx  17558  ocid  17559  basendxnocndx  17560  plendxnocndx  17561  dsndx  17562  dsid  17563  dsndxnn  17564  basendxltdsndx  17565  slotsdifdsndx  17571  unifndx  17572  unifid  17573  unifndxnn  17574  basendxltunifndx  17575  slotsdifunifndx  17578  odrngstr  17580  homndx  17588  homid  17589  ccondx  17590  ccoid  17591  slotsbhcdif  17592  slotsdifplendx2  17593  slotsdifocndx  17594  imasvalstr  17628  prdsvalstr  17629  catstr  18141  ipostr  18709  smndex2dnrinv  19120  cycsubmcl  19422  psgnunilem2  19715  odcau  19824  lt6abl  20115  omndmul2  20353  0ringnnzr  20782  cnfldstr  21686  nn0srg  21749  freshmansdream  21886  mvrid  22297  mvrf1  22299  mplcoe3  22353  psrbagsn  22378  evlslem1  22397  mhpvarcl  22475  psdcl  22488  psdmul  22493  psdmvr  22496  pmatcollpw3fi1lem1  23110  chfacfscmulgsum  23184  chfacfpmmulfsupp  23187  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cpmadugsumlemB  23198  cpmadugsumlemF  23200  dscmet  24897  ehl1eudis  25747  dveflem  26305  c1lip2  26324  itgpowd  26376  ply1remlem  26489  fta1glem1  26492  fta1blem  26495  plyid  26533  coeidp  26588  dgrid  26589  plyn0mulidp  26608  vieta1lem2  26640  vieta1  26641  aalioulem3  26667  aaliou2b  26674  dvtaylp  26703  taylthlem1  26706  taylthlem2  26707  radcnvlem2  26747  dvradcnv  26754  pserdvlem2  26761  logtayllem  26993  logtayl  26994  cxp1  27005  quart1cl  27188  quart1lem  27189  quart1  27190  quartlem1  27191  quartlem2  27192  leibpilem2  27275  log2ublem3  27282  log2ub  27283  birthday  27288  lgamcvg2  27388  gamp1  27391  issqf  27469  ppi2  27503  mumullem2  27513  sqff1o  27515  1sgmprm  27532  ppiublem2  27536  chtublem  27544  logfacbnd3  27556  logexprlim  27558  logfacrlim2  27559  perfectlem1  27562  perfectlem2  27563  bclbnd  27613  bpos1  27616  bposlem6  27622  lgsval  27634  2lgslem3a  27729  2lgslem3c  27731  rpvmasumlem  27820  log2sumbnd  27877  itvndx  28905  lngndx  28906  itvid  28907  lngid  28908  slotsinbpsd  28909  slotslnbpsd  28910  lngndxnitvndx  28911  trkgstr  28912  eengstr  29564  edgfid  29574  edgfndx  29575  edgfndxnn  29576  basendxltedgfndx  29578  usgrexmplef  29846  cusgrsizeindb1  30037  wlk1ewlk  30226  usgr2pthlem  30355  uspgrn2crct  30403  crctcshwlkn0lem5  30409  rusgrnumwwlkl1  30566  rusgrnumwwlkb1  30570  clwwlkccatlem  30586  clwwlkinwwlk  30637  umgr2cwwkdifex  30662  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  konigsbergiedgw  30855  konigsberglem1  30859  konigsberglem2  30860  konigsberglem3  30861  konigsberglem4  30862  1kp2ke3k  31053  ex-exp  31057  ex-fac  31058  9p10ne21  31077  sgnmulsgp  33470  nexple  33471  dpmul4  33527  threehalves  33528  1mhdrd  33529  s2f1  33557  cycpm2tr  33727  evl1deg1  34155  evl1deg2  34156  evl1deg3  34157  ply1dg1rt  34159  coe1vr1  34170  deg1vr  34171  mplmulmvr  34218  esplylem  34245  esplyfv1  34248  esplyfval1  34252  esplyfvaln  34253  esplyind  34254  drngdimgt0  34297  rtelextdg2lem  34405  fldext2chn  34407  constrdircl  34444  iconstr  34445  2sqr3minply  34459  cos9thpiminplylem1  34461  cos9thpiminplylem2  34462  cos9thpiminply  34467  lmat22e12  34498  lmat22e21  34499  lmat22e22  34500  madjusmdetlem4  34509  oddpwdc  35033  eulerpartlemd  35045  eulerpartlemgs2  35059  eulerpartlemn  35060  iwrdsplit  35066  fib0  35078  fib1  35079  fibp1  35080  signstfveq0  35253  signsvvf  35255  signsvfn  35258  signshlen  35266  prodfzo03  35279  reprsuc  35291  breprexplemc  35308  hgt750lemd  35324  hgt750lem  35327  hgt750lem2  35328  hgt750leme  35334  usgrgt2cycl  35986  subfac1  36030  kur14lem9  36066  bccolsum  36597  nn0prpw  37204  12gcd5e1  43147  60gcd6e6  43148  60gcd7e1  43149  420gcd8e4  43150  12lcm5e60  43152  lcmineqlem11  43183  lcmineqlem18  43190  lcmineqlem22  43194  lcmineqlem  43196  3exp7  43197  3lexlogpow5ineq1  43198  3lexlogpow5ineq2  43199  3lexlogpow5ineq5  43204  dvrelogpow2b  43212  aks4d1p1p2  43214  aks4d1p1p4  43215  aks4d1p1p6  43217  aks4d1p1p7  43218  aks4d1p1p5  43219  aks4d1p1  43220  aks4d1p3  43222  aks6d1c1p8  43259  aks6d1c5lem3  43281  2np3bcnp1  43288  2ap1caineq  43289  sticksstones22  43312  aks6d1c6lem1  43314  aks6d1c7lem1  43324  aks6d1c7  43328  25or6to4  43350  235t711  43456  ex-decpmul  43457  fltnltalem  43767  sum9cubes  43777  3cubeslem3l  43790  3cubeslem3r  43791  pell1qr1  43972  rmspecfund  44010  jm2.23  44097  jm2.27c  44108  areaquad  44312  resqrtvalex  44739  imsqrtvalex  44740  brfvidRP  44782  brfvrcld  44785  corclrcl  44801  dftrcl3  44814  dfrtrcl3  44827  fvrtrcllb1d  44831  corcltrcl  44833  cotrclrcl  44836  inductionexd  45249  radcnvrat  45392  binomcxplemnn0  45427  binomcxplemfrat  45429  binomcxplemnotnn0  45434  rexanuz2nf  46596  wallispilem2  47170  wallispilem5  47173  wallispi2lem2  47176  stirlinglem5  47182  stirlinglem7  47184  stirlinglem10  47187  stirlinglem11  47188  fourierdlem48  47258  ormkglobd  47981  goldratmolem2  48027  iccpartigtl  48599  iccpartlt  48600  iccpartgel  48605  fmtnosqrt  48718  fmtno1  48720  fmtno2  48729  fmtno5lem1  48732  fmtno5lem2  48733  fmtno5lem3  48734  fmtno5lem4  48735  fmtno5  48736  257prm  48740  fmtnofac1  48749  fmtno4prmfac  48751  fmtno4prmfac193  48752  fmtno4nprmfac193  48753  fmtno5faclem1  48758  fmtno5faclem2  48759  fmtno5faclem3  48760  fmtno5fac  48761  fmtno5nprm  48762  3ndvds4  48774  139prmALT  48775  31prm  48776  m5prm  48777  127prm  48778  m7prm  48779  m11nprm  48780  lighneallem2  48785  perfectALTVlem1  48913  perfectALTVlem2  48914  11t31e341  48924  2exp340mod341  48925  341fppr2  48926  8exp8mod9  48928  nfermltl8rev  48934  nfermltl2rev  48935  evengpoap3  48991  nnsum4primesevenALTV  48993  bgoldbtbndlem1  48997  bgoldbachlt  49005  tgblthelfgott  49007  cycl3grtri  49139  stgr1  49153  usgrexmpl1lem  49213  usgrexmpl2lem  49218  gpgprismgriedgdmss  49244  gpgprismgr4cycllem3  49289  gpgprismgr4cycllem7  49293  gpgprismgr4cycllem9  49295  gpgprismgr4cycllem10  49296  grlimedgnedg  49323  nnpw2pmod  49789  dig1  49814  dignn0flhalflem2  49822  1aryfvalel  49842  itcoval1  49869  itcoval2  49870  ackval1  49887  ackval2  49888  ackval3  49889  ackendofnn0  49890  ackvalsucsucval  49894  ackval0012  49895  ackval1012  49896  ackval2012  49897  ackval3012  49898  ackval41a  49900  ackval42  49902