Theorem nnnn0 12479

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 12475	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3979	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 12212  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-n0 12473

This theorem is referenced by:  nnnn0i  12480  elnnnn0b  12516  elnnnn0c  12517  elz2  12576  nn0ind-raph  12662  zindd  12663  fzo1fzo0n0  13683  ubmelfzo  13697  elfzom1elp1fzo  13699  fzo0sn0fzo1  13721  quoremnn0ALT  13822  modmulnn  13854  modsumfzodifsn  13909  addmodlteq  13911  expneg  14035  expcllem  14038  expcl2lem  14039  expeq0  14058  mulexpz  14068  expmordi  14132  rpexpmord  14133  expnlbnd  14196  expmulnbnd  14198  digit2  14199  digit1  14200  facmapnn  14245  facdiv  14247  faclbnd  14250  faclbnd3  14252  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd5  14258  faclbnd6  14259  bcval5  14278  ishashinf  14424  iswrdi  14468  pfxn0  14636  repswfsts  14731  repswlsw  14732  repswcshw  14762  relexpnnrn  14992  relexpaddg  15000  absexpz  15252  isercoll  15614  summolem3  15660  summolem2a  15661  climcndslem2  15796  climcnds  15797  harmonic  15805  arisum  15806  expcnv  15810  geo2sum  15819  geo2lim  15821  geoisum1  15825  geoisum1c  15826  0.999...  15827  mertenslem2  15831  fallfacfwd  15980  0fallfac  15981  0risefac  15982  ef0lem  16022  ege2le3  16033  efaddlem  16036  efexp  16044  rpnnen2lem2  16158  rpnnen2lem4  16160  ruclem12  16184  dvdsmodexp  16205  dvdsexp2im  16270  nn0enne  16320  nnehalf  16322  nno  16325  nn0o  16326  pwp1fsum  16334  divalg2  16348  ndvdssub  16352  gcdmultiplez  16477  gcddiv  16493  rpmulgcd  16498  rplpwr  16499  dvdssqlem  16503  eucalgf  16520  lcmflefac  16585  1nprm  16616  2mulprm  16630  isprm5  16644  isprm6  16651  prmdvdsexp  16652  phicl2  16701  phibndlem  16703  phiprmpw  16709  crth  16711  eulerthlem2  16715  hashgcdlem  16721  phisum  16723  pythagtriplem10  16753  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem12  16759  pythagtriplem14  16761  pclem  16771  pcexp  16792  pcid  16806  pcprod  16828  pcbc  16833  prmpwdvds  16837  infpnlem1  16843  infpnlem2  16844  prmunb  16847  prmreclem6  16854  1arith  16860  vdwapf  16905  0hashbc  16940  ram0  16955  prmdvdsprmo  16975  prmdvdsprmop  16976  prmolefac  16979  prmgaplem1  16982  prmgaplem2  16983  prmgapprmolem  16994  prmgapprmo  16995  cshwrepswhash1  17036  smndex1n0mnd  18793  ghmmulg  19104  odmodnn0  19408  dfod2  19432  submod  19437  prmirredlem  21042  prmirred  21044  znf1o  21107  znhash  21114  znfi  21115  znfld  21116  znidomb  21117  znunithash  21120  znrrg  21121  cply1mul  21818  cply1coe0  21823  cply1coe0bi  21824  cpmatmcllem  22220  m2cpm  22243  m2cpminvid2lem  22256  fvmptnn04ifa  22352  chfacfisf  22356  chfacfisfcpmat  22357  chfacffsupp  22358  chfacfscmul0  22360  chfacfscmulfsupp  22361  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulfsupp  22365  chfacfpmmulgsum  22366  chfacfpmmulgsum2  22367  cayhamlem1  22368  cpmadugsumlemF  22378  tgpmulg  23597  cmodscexp  24637  cphipval  24760  ovollb2lem  25005  ovoliunlem1  25019  ovoliunlem3  25021  uniioombllem3  25102  uniioombllem4  25103  opnmbllem  25118  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  dvexp  25470  dvexp3  25495  plyco  25755  dgrcolem1  25787  plydivex  25810  aaliou3lem2  25856  aaliou3lem3  25857  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  aaliou3lem9  25863  radcnvlem2  25926  dvradcnv  25933  pserdv2  25942  abelthlem6  25948  abelthlem9  25952  logtayllem  26167  logtayl  26168  logtaylsum  26169  logtayl2  26170  cxproot  26198  root1id  26262  logbgcd1irr  26299  atantayl  26442  atantayl2  26443  leibpilem2  26446  leibpi  26447  birthdaylem2  26457  birthdaylem3  26458  dfef2  26475  basellem2  26586  basellem4  26588  basellem5  26589  basellem6  26590  basellem8  26592  isppw2  26619  vmappw  26620  sqf11  26643  vma1  26670  1sgm2ppw  26703  chtublem  26714  fsumvma2  26717  vmasum  26719  dchrelbas4  26746  dchrzrhcl  26748  dchrfi  26758  dchrhash  26774  pcbcctr  26779  bclbnd  26783  bposlem1  26787  lgsval4a  26822  lgsdchrval  26857  lgsdchr  26858  gausslemma2dlem0c  26861  gausslemma2dlem0d  26862  gausslemma2dlem6  26875  2lgslem1a1  26892  2lgslem1c  26896  2lgslem3a1  26903  2lgslem3b1  26904  2lgslem3c1  26905  2lgslem3d1  26906  2sqreunnlem1  26952  2sqreunnltblem  26954  rplogsumlem2  26988  dchrisumlem2  26993  ostth2lem1  27121  ostth2lem3  27138  ostth3  27141  cusgrsize2inds  28741  pthdivtx  29017  crctcshwlkn0lem4  29098  crctcshwlkn0lem5  29099  crctcshwlkn0lem7  29101  0enwwlksnge1  29149  rusgr0edg  29258  clwlkclwwlkf1lem2  29289  clwlkclwwlkf1lem3  29290  clwwisshclwwslem  29298  clwwlkinwwlk  29324  clwwlkel  29330  clwwlkf  29331  clwwlkf1  29333  clwwlknwwlksnb  29339  wwlksubclwwlk  29342  erclwwlknref  29353  clwwlknonwwlknonb  29390  numclwwlkqhash  29659  numclwwlk2lem1  29660  numclwlk2lem2f  29661  numclwlk2lem2f1o  29663  ipval2  29991  ipasslem3  30117  ipasslem4  30118  nn0min  32057  frobrhm  32413  znfermltl  32510  ply1fermltlchr  32693  ply1fermltl  32694  esumcst  33092  eulerpartlemb  33398  fibp1  33431  ballotlem1  33516  subfacp1lem6  34207  subfaclim  34210  subfacval3  34211  snmlff  34351  bcprod  34739  faclim2  34749  nn0prpwlem  35255  knoppndvlem18  35453  opnmbllem0  36572  nnubfi  36666  nninfnub  36667  geomcau  36675  heiborlem5  36731  heiborlem6  36732  heiborlem7  36733  heiborlem8  36734  bfplem1  36738  lcmineqlem12  40953  aks4d1p1p2  40983  2ap1caineq  41009  nn0expgcd  41274  dvdsexpnn  41279  dvdsexpnn0  41280  zaddcomlem  41372  dffltz  41424  fltnltalem  41452  irrapxlem2  41609  pellexlem1  41615  pellexlem5  41619  pellqrex  41665  monotoddzzfi  41729  jm2.17c  41749  acongeq  41770  jm2.18  41775  jm2.23  41783  jm2.26lem3  41788  jm3.1  41807  expdiophlem1  41808  idomrootle  41985  idomodle  41986  proot1ex  41991  rp-isfinite6  42317  cnvtrclfv  42523  cotrclrcl  42541  inductionexd  42954  binomcxplemnotnn0  43163  nnne1ge2  44049  dvnmptconst  44705  stoweidlem3  44767  stoweidlem7  44771  stoweidlem34  44798  wallispilem4  44832  wallispilem5  44833  wallispi2lem1  44835  wallispi2lem2  44836  stirlinglem2  44839  stirlinglem3  44840  stirlinglem4  44841  stirlinglem5  44842  stirlinglem7  44844  stirlinglem11  44848  stirlinglem14  44851  stirlinglem15  44852  stirlingr  44854  fourierdlem15  44886  fourierdlem21  44892  fourierdlem22  44893  fourierdlem92  44962  fourierdlem112  44982  fouriersw  44995  sge0rpcpnf  45185  sge0ad2en  45195  ovnsubaddlem1  45334  ovnsubaddlem2  45335  ovolval5lem1  45416  ovolval5lem2  45417  iccpartiltu  46138  iccpartigtl  46139  iccpartlt  46140  iccpartleu  46144  iccpartrn  46146  iccelpart  46149  iccpartiun  46150  iccpartdisj  46153  sqrtpwpw2p  46254  fmtnosqrt  46255  odz2prm2pw  46279  fmtnoprmfac1lem  46280  fmtnoprmfac1  46281  2pwp1prm  46305  lighneallem1  46321  lighneallem2  46322  lighneallem3  46323  lighneallem4a  46324  lighneallem4  46326  nnpw2evenALTV  46418  dfwppr  46454  cznabel  46900  cznrng  46901  ztprmneprm  47071  altgsumbc  47076  altgsumbcALT  47077  pw2m1lepw2m1  47249  nneom  47261  logbpw2m1  47301  blennn  47309  blenpw2m1  47313  blengt1fldiv2p1  47327  dignn0ldlem  47336  dignnld  47337  dig2nn1st  47339  dignn0flhalflem1  47349  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  itcovalt2lem2lem1  47407  eenglngeehlnm  47473