Theorem 1nn0 12531

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

This proof depends on syntax axioms:   ∈ wcel 2146  1c1 11112  ℕ₀cn0 12515

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12245  df-n0 12516

This theorem is used by:  peano2nn0  12555  deccl  12738  11nn0  12739  12nn0  12740  16nn0  12741  10nn0  12745  11nn  12748  numsucc  12768  numadd  12775  numaddc  12776  11multnc  12796  6p5lem  12798  6p6e12  12802  7p5e12  12805  8p4e12  12810  9p2e11  12815  9p3e12  12816  10p10e20  12823  4t4e16  12827  5t2e10  12828  5t4e20  12830  6t3e18  12833  6t4e24  12834  7t3e21  12838  7t4e28  12839  8t3e24  12844  9t3e27  12851  9t9e81  12857  1lt10  12868  xnn0n0n1ge2b  13169  fz0to3un2pr  13670  elfzom1elp1fzo  13774  fzo0sn0fzo1  13797  fvf1tp  13836  fldiv4lem1div2  13884  expn1  14121  nn0expcl  14125  sqval  14164  nn0opthlem1  14318  fac2  14329  faclbnd4lem2  14344  bccl  14372  hashsng  14419  hashen1  14420  hashrabrsn  14422  1elfz0hash  14440  hashgt23el  14475  hashprlei  14519  hashtplei  14535  tpf1ofv1  14548  tpfo  14551  wrdred1hash  14612  pfx1  14758  repsw1  14840  cshw1  14879  s3fv1  14949  s4fv1  14953  pfx2  15004  repsw2  15007  repsw3  15008  wwlktovf  15013  relexp1g  15083  relexpaddg  15110  rtrclreclem1  15114  sgnmulsgn  15166  bcxmas  15908  climcndslem2  15923  climcnds  15924  arisum  15933  geoisum1  15952  geoisum1c  15953  mertenslem2  15958  fprodnn0cl  16030  nn0risefaccl  16095  bpoly1  16123  bpoly4  16131  fsumcube  16132  ege2le3  16162  ef4p  16187  efgt1p2  16188  efgt1p  16189  sin01gt0  16264  rpnnen2lem3  16290  dvds1  16395  3dvds2dec  16409  5ndvds6  16490  bitsmod  16512  bitsinv1lem  16517  sadadd2lem  16535  sadadd  16543  sadass  16547  smupp1  16556  smumul  16569  nn0rppwr  16637  prmdvdsbc  16803  pcelnn  16948  pockthg  16984  vdwlem12  17070  prmo1  17115  dec5nprm  17144  dec2nprm  17145  modxp1i  17148  2exp8  17166  2exp11  17167  2exp16  17168  2expltfac  17170  5prm  17186  11prm  17193  13prm  17194  17prm  17195  19prm  17196  23prm  17197  prmlem2  17198  37prm  17199  43prm  17200  83prm  17201  139prm  17202  163prm  17203  317prm  17204  631prm  17205  1259lem1  17209  1259lem2  17210  1259lem3  17211  1259lem4  17212  1259lem5  17213  1259prm  17214  2503lem1  17215  2503lem2  17216  2503lem3  17217  2503prm  17218  4001lem1  17219  4001lem2  17220  4001lem3  17221  4001lem4  17222  4001prm  17223  ocndx  17452  ocid  17453  basendxnocndx  17454  plendxnocndx  17455  dsndx  17456  dsid  17457  dsndxnn  17458  basendxltdsndx  17459  slotsdifdsndx  17465  unifndx  17466  unifid  17467  unifndxnn  17468  basendxltunifndx  17469  slotsdifunifndx  17472  odrngstr  17474  homndx  17482  homid  17483  ccondx  17484  ccoid  17485  slotsbhcdif  17486  slotsdifplendx2  17487  slotsdifocndx  17488  imasvalstr  17522  prdsvalstr  17523  catstr  18035  ipostr  18603  smndex2dnrinv  19001  cycsubmcl  19296  psgnunilem2  19589  odcau  19698  lt6abl  19989  omndmul2  20227  0ringnnzr  20653  cnfldstr  21554  nn0srg  21617  freshmansdream  21754  mvrid  22163  mvrf1  22165  mplcoe3  22219  psrbagsn  22244  evlslem1  22263  mhpvarcl  22341  psdcl  22354  psdmul  22359  psdmvr  22362  pmatcollpw3fi1lem1  22973  chfacfscmulgsum  23047  chfacfpmmulfsupp  23050  chfacfpmmulgsum  23051  chfacfpmmulgsum2  23052  cpmadugsumlemB  23061  cpmadugsumlemF  23063  dscmet  24760  ehl1eudis  25610  dveflem  26169  c1lip2  26188  itgpowd  26240  ply1remlem  26353  fta1glem1  26356  fta1blem  26359  plyid  26397  coeidp  26451  dgrid  26452  plyn0mulidp  26473  vieta1lem2  26503  vieta1  26504  aalioulem3  26528  aaliou2b  26535  dvtaylp  26564  taylthlem1  26567  taylthlem2  26568  radcnvlem2  26608  dvradcnv  26615  pserdvlem2  26622  logtayllem  26855  logtayl  26856  cxp1  26867  quart1cl  27050  quart1lem  27051  quart1  27052  quartlem1  27053  quartlem2  27054  leibpilem2  27137  log2ublem3  27144  log2ub  27145  birthday  27150  lgamcvg2  27250  gamp1  27253  issqf  27331  ppi2  27365  mumullem2  27375  sqff1o  27377  1sgmprm  27394  ppiublem2  27398  chtublem  27406  logfacbnd3  27418  logexprlim  27420  logfacrlim2  27421  perfectlem1  27424  perfectlem2  27425  bclbnd  27475  bpos1  27478  bposlem6  27484  lgsval  27496  2lgslem3a  27591  2lgslem3c  27593  rpvmasumlem  27682  log2sumbnd  27739  itvndx  28737  lngndx  28738  itvid  28739  lngid  28740  slotsinbpsd  28741  slotslnbpsd  28742  lngndxnitvndx  28743  trkgstr  28744  eengstr  29361  edgfid  29371  edgfndx  29372  edgfndxnn  29373  basendxltedgfndx  29375  usgrexmplef  29643  cusgrsizeindb1  29834  wlk1ewlk  30023  usgr2pthlem  30152  uspgrn2crct  30200  crctcshwlkn0lem5  30206  rusgrnumwwlkl1  30363  rusgrnumwwlkb1  30367  clwwlkccatlem  30383  clwwlkinwwlk  30434  umgr2cwwkdifex  30459  upgr3v3e3cycl  30578  upgr4cycl4dv4e  30583  konigsbergiedgw  30646  konigsberglem1  30650  konigsberglem2  30651  konigsberglem3  30652  konigsberglem4  30653  1kp2ke3k  30844  ex-exp  30848  ex-fac  30849  9p10ne21  30868  sgnmulsgp  33222  nexple  33223  dpmul4  33279  threehalves  33280  1mhdrd  33281  s2f1  33309  cycpm2tr  33479  evl1deg1  33906  evl1deg2  33907  evl1deg3  33908  ply1dg1rt  33910  coe1vr1  33921  deg1vr  33922  mplmulmvr  33969  esplylem  33996  esplyfv1  33999  esplyfval1  34003  esplyfvaln  34004  esplyind  34005  drngdimgt0  34048  rtelextdg2lem  34156  fldext2chn  34158  constrdircl  34195  iconstr  34196  2sqr3minply  34210  cos9thpiminplylem1  34212  cos9thpiminplylem2  34213  cos9thpiminply  34218  lmat22e12  34249  lmat22e21  34250  lmat22e22  34251  madjusmdetlem4  34260  oddpwdc  34785  eulerpartlemd  34797  eulerpartlemgs2  34811  eulerpartlemn  34812  iwrdsplit  34818  fib0  34830  fib1  34831  fibp1  34832  signstfveq0  35005  signsvvf  35007  signsvfn  35010  signshlen  35018  prodfzo03  35031  reprsuc  35043  breprexplemc  35060  hgt750lemd  35076  hgt750lem  35079  hgt750lem2  35080  hgt750leme  35086  usgrgt2cycl  35643  subfac1  35683  kur14lem9  35719  bccolsum  36244  nn0prpw  36867  12gcd5e1  42803  60gcd6e6  42804  60gcd7e1  42805  420gcd8e4  42806  12lcm5e60  42808  lcmineqlem11  42839  lcmineqlem18  42846  lcmineqlem22  42850  lcmineqlem  42852  3exp7  42853  3lexlogpow5ineq1  42854  3lexlogpow5ineq2  42855  3lexlogpow5ineq5  42860  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1p4  42871  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p3  42878  aks6d1c1p8  42915  aks6d1c5lem3  42937  2np3bcnp1  42944  2ap1caineq  42945  sticksstones22  42968  aks6d1c6lem1  42970  aks6d1c7lem1  42980  aks6d1c7  42984  25or6to4  43006  235t711  43099  ex-decpmul  43100  fltnltalem  43427  sum9cubes  43437  3cubeslem3l  43450  3cubeslem3r  43451  pell1qr1  43631  rmspecfund  43669  jm2.23  43756  jm2.27c  43767  areaquad  43976  resqrtvalex  44404  imsqrtvalex  44405  brfvidRP  44447  brfvrcld  44450  corclrcl  44466  dftrcl3  44479  dfrtrcl3  44492  fvrtrcllb1d  44496  corcltrcl  44498  cotrclrcl  44501  inductionexd  44914  radcnvrat  45057  binomcxplemnn0  45092  binomcxplemfrat  45094  binomcxplemnotnn0  45099  rexanuz2nf  46239  wallispilem2  46813  wallispilem5  46816  wallispi2lem2  46819  stirlinglem5  46825  stirlinglem7  46827  stirlinglem10  46830  stirlinglem11  46831  fourierdlem48  46901  ormkglobd  47624  sin5tlem4  47646  goldratmolem2  47656  iccpartigtl  48205  iccpartlt  48206  iccpartgel  48211  fmtnosqrt  48324  fmtno1  48326  fmtno2  48335  fmtno5lem1  48338  fmtno5lem2  48339  fmtno5lem3  48340  fmtno5lem4  48341  fmtno5  48342  257prm  48346  fmtnofac1  48355  fmtno4prmfac  48357  fmtno4prmfac193  48358  fmtno4nprmfac193  48359  fmtno5faclem1  48364  fmtno5faclem2  48365  fmtno5faclem3  48366  fmtno5fac  48367  fmtno5nprm  48368  3ndvds4  48380  139prmALT  48381  31prm  48382  m5prm  48383  127prm  48384  m7prm  48385  m11nprm  48386  lighneallem2  48391  perfectALTVlem1  48519  perfectALTVlem2  48520  11t31e341  48530  2exp340mod341  48531  341fppr2  48532  8exp8mod9  48534  nfermltl8rev  48540  nfermltl2rev  48541  evengpoap3  48597  nnsum4primesevenALTV  48599  bgoldbtbndlem1  48603  bgoldbachlt  48611  tgblthelfgott  48613  cycl3grtri  48745  stgr1  48759  usgrexmpl1lem  48819  usgrexmpl2lem  48824  gpgprismgriedgdmss  48850  gpgprismgr4cycllem3  48895  gpgprismgr4cycllem7  48899  gpgprismgr4cycllem9  48901  gpgprismgr4cycllem10  48902  grlimedgnedg  48929  nnpw2pmod  49396  dig1  49421  dignn0flhalflem2  49429  1aryfvalel  49449  itcoval1  49476  itcoval2  49477  ackval1  49494  ackval2  49495  ackval3  49496  ackendofnn0  49497  ackvalsucsucval  49501  ackval0012  49502  ackval1012  49503  ackval2012  49504  ackval3012  49505  ackval41a  49507  ackval42  49509