Theorem 1nn0 12444

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

Syntax hints:   ∈ wcel 2114  1c1 11030  ℕ₀cn0 12428

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-n0 12429

This theorem is referenced by:  peano2nn0  12468  deccl  12650  10nn0  12653  numsucc  12675  numadd  12682  numaddc  12683  11multnc  12703  6p5lem  12705  6p6e12  12709  7p5e12  12712  8p4e12  12717  9p2e11  12722  9p3e12  12723  10p10e20  12730  4t4e16  12734  5t2e10  12735  5t4e20  12737  6t3e18  12740  6t4e24  12741  7t3e21  12745  7t4e28  12746  8t3e24  12751  9t3e27  12758  9t9e81  12764  xnn0n0n1ge2b  13074  fz0to3un2pr  13574  elfzom1elp1fzo  13678  fzo0sn0fzo1  13701  fvf1tp  13739  fldiv4lem1div2  13787  expn1  14024  nn0expcl  14028  sqval  14067  nn0opthlem1  14221  fac2  14232  faclbnd4lem2  14247  bccl  14275  hashsng  14322  hashen1  14323  hashrabrsn  14325  1elfz0hash  14343  hashgt23el  14377  hashprlei  14421  hashtplei  14437  tpf1ofv1  14450  tpfo  14453  wrdred1hash  14514  pfx1  14656  repsw1  14736  cshw1  14775  s3fv1  14845  s4fv1  14849  pfx2  14900  repsw2  14903  repsw3  14904  wwlktovf  14909  relexp1g  14979  relexpaddg  15006  rtrclreclem1  15010  bcxmas  15791  climcndslem2  15806  climcnds  15807  arisum  15816  geoisum1  15835  geoisum1c  15836  mertenslem2  15841  fprodnn0cl  15913  nn0risefaccl  15978  bpoly1  16007  bpoly4  16015  fsumcube  16016  ege2le3  16046  ef4p  16071  efgt1p2  16072  efgt1p  16073  sin01gt0  16148  rpnnen2lem3  16174  dvds1  16279  3dvds2dec  16293  5ndvds6  16374  bitsmod  16396  bitsinv1lem  16401  sadadd2lem  16419  sadadd  16427  sadass  16431  smupp1  16440  smumul  16453  nn0rppwr  16521  prmdvdsbc  16687  pcelnn  16832  pockthg  16868  vdwlem12  16954  prmo1  16999  dec5nprm  17028  dec2nprm  17029  modxp1i  17032  2exp8  17050  2exp11  17051  2exp16  17052  2expltfac  17054  5prm  17070  11prm  17076  13prm  17077  17prm  17078  19prm  17079  23prm  17080  prmlem2  17081  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  ocndx  17335  ocid  17336  basendxnocndx  17337  plendxnocndx  17338  dsndx  17339  dsid  17340  dsndxnn  17341  basendxltdsndx  17342  slotsdifdsndx  17348  unifndx  17349  unifid  17350  unifndxnn  17351  basendxltunifndx  17352  slotsdifunifndx  17355  odrngstr  17357  homndx  17365  homid  17366  ccondx  17367  ccoid  17368  slotsbhcdif  17369  slotsdifplendx2  17370  slotsdifocndx  17371  imasvalstr  17405  prdsvalstr  17406  catstr  17918  ipostr  18486  smndex2dnrinv  18877  cycsubmcl  19167  psgnunilem2  19461  odcau  19570  lt6abl  19861  omndmul2  20099  0ringnnzr  20493  cnfldstr  21346  cnfldstrOLD  21361  nn0srg  21427  freshmansdream  21564  mvrid  21972  mvrf1  21974  mplcoe3  22026  psrbagsn  22051  evlslem1  22070  mhpvarcl  22124  psdcl  22137  psdmul  22142  psdmvr  22145  pmatcollpw3fi1lem1  22761  chfacfscmulgsum  22835  chfacfpmmulfsupp  22838  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cpmadugsumlemB  22849  cpmadugsumlemF  22851  dscmet  24547  ehl1eudis  25397  dveflem  25956  c1lip2  25975  itgpowd  26027  ply1remlem  26140  fta1glem1  26143  fta1blem  26146  plyid  26184  coeidp  26238  dgrid  26239  vieta1lem2  26288  vieta1  26289  aalioulem3  26311  aaliou2b  26318  dvtaylp  26347  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  radcnvlem2  26392  dvradcnv  26399  pserdvlem2  26406  logtayllem  26636  logtayl  26637  cxp1  26648  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  leibpilem2  26918  log2ublem3  26925  log2ub  26926  birthday  26931  lgamcvg2  27032  gamp1  27035  issqf  27113  ppi2  27147  mumullem2  27157  sqff1o  27159  1sgmprm  27176  ppiublem2  27180  chtublem  27188  logfacbnd3  27200  logexprlim  27202  logfacrlim2  27203  perfectlem1  27206  perfectlem2  27207  bclbnd  27257  bpos1  27260  bposlem6  27266  lgsval  27278  2lgslem3a  27373  2lgslem3c  27375  rpvmasumlem  27464  log2sumbnd  27521  itvndx  28519  lngndx  28520  itvid  28521  lngid  28522  slotsinbpsd  28523  slotslnbpsd  28524  lngndxnitvndx  28525  trkgstr  28526  eengstr  29063  edgfid  29073  edgfndx  29074  edgfndxnn  29075  basendxltedgfndx  29077  usgrexmplef  29342  cusgrsizeindb1  29534  wlk1ewlk  29723  usgr2pthlem  29846  uspgrn2crct  29891  crctcshwlkn0lem5  29897  rusgrnumwwlkl1  30054  rusgrnumwwlkb1  30058  clwwlkccatlem  30074  clwwlkinwwlk  30125  umgr2cwwkdifex  30150  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  konigsbergiedgw  30333  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  konigsberglem4  30340  1kp2ke3k  30531  ex-exp  30535  ex-fac  30536  9p10ne21  30555  sgnmulsgn  32930  sgnmulsgp  32931  nexple  32932  dpmul4  32988  threehalves  32989  1mhdrd  32990  s2f1  33020  cycpm2tr  33195  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  ply1dg1rt  33655  coe1vr1  33666  deg1vr  33667  mplmulmvr  33698  esplylem  33725  esplyfv1  33728  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  drngdimgt0  33778  rtelextdg2lem  33886  fldext2chn  33888  constrdircl  33925  iconstr  33926  2sqr3minply  33940  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminply  33948  lmat22e12  33979  lmat22e21  33980  lmat22e22  33981  madjusmdetlem4  33990  oddpwdc  34514  eulerpartlemd  34526  eulerpartlemgs2  34540  eulerpartlemn  34541  iwrdsplit  34547  fib0  34559  fib1  34560  fibp1  34561  plymulx0  34707  signstfveq0  34737  signsvvf  34739  signsvfn  34742  signshlen  34750  prodfzo03  34763  reprsuc  34775  breprexplemc  34792  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  hgt750leme  34818  usgrgt2cycl  35328  subfac1  35376  kur14lem9  35412  bccolsum  35937  nn0prpw  36521  12gcd5e1  42456  60gcd6e6  42457  60gcd7e1  42458  420gcd8e4  42459  12lcm5e60  42461  lcmineqlem11  42492  lcmineqlem18  42499  lcmineqlem22  42503  lcmineqlem  42505  3exp7  42506  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq5  42513  dvrelogpow2b  42521  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p3  42531  aks6d1c1p8  42568  aks6d1c5lem3  42590  2np3bcnp1  42597  2ap1caineq  42598  sticksstones22  42621  aks6d1c6lem1  42623  aks6d1c7lem1  42633  aks6d1c7  42637  235t711  42751  ex-decpmul  42752  fltnltalem  43109  sum9cubes  43119  3cubeslem3l  43132  3cubeslem3r  43133  pell1qr1  43317  rmspecfund  43355  jm2.23  43442  jm2.27c  43453  areaquad  43662  resqrtvalex  44090  imsqrtvalex  44091  brfvidRP  44133  brfvrcld  44136  corclrcl  44152  dftrcl3  44165  dfrtrcl3  44178  fvrtrcllb1d  44182  corcltrcl  44184  cotrclrcl  44187  inductionexd  44600  radcnvrat  44759  binomcxplemnn0  44794  binomcxplemfrat  44796  binomcxplemnotnn0  44801  rexanuz2nf  45938  wallispilem2  46512  wallispilem5  46515  wallispi2lem2  46518  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  fourierdlem48  46600  ormkglobd  47321  sin5tlem4  47340  sin5tlem5  47341  iccpartigtl  47895  iccpartlt  47896  iccpartgel  47901  fmtnosqrt  48014  fmtno1  48016  fmtno2  48025  fmtno5lem1  48028  fmtno5lem2  48029  fmtno5lem3  48030  fmtno5lem4  48031  fmtno5  48032  257prm  48036  fmtnofac1  48045  fmtno4prmfac  48047  fmtno4prmfac193  48048  fmtno4nprmfac193  48049  fmtno5faclem1  48054  fmtno5faclem2  48055  fmtno5faclem3  48056  fmtno5fac  48057  fmtno5nprm  48058  3ndvds4  48070  139prmALT  48071  31prm  48072  m5prm  48073  127prm  48074  m7prm  48075  m11nprm  48076  lighneallem2  48081  perfectALTVlem1  48209  perfectALTVlem2  48210  11t31e341  48220  2exp340mod341  48221  341fppr2  48222  8exp8mod9  48224  nfermltl8rev  48230  nfermltl2rev  48231  evengpoap3  48287  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  bgoldbachlt  48301  tgblthelfgott  48303  cycl3grtri  48435  stgr1  48449  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpgprismgriedgdmss  48540  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem9  48591  gpgprismgr4cycllem10  48592  grlimedgnedg  48619  nnpw2pmod  49071  dig1  49096  dignn0flhalflem2  49104  1aryfvalel  49124  itcoval1  49151  itcoval2  49152  ackval1  49169  ackval2  49170  ackval3  49171  ackendofnn0  49172  ackvalsucsucval  49176  ackval0012  49177  ackval1012  49178  ackval2012  49179  ackval3012  49180  ackval41a  49182  ackval42  49184