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  28710  pthdivtx  28986  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem7  29070  0enwwlksnge1  29118  rusgr0edg  29227  clwlkclwwlkf1lem2  29258  clwlkclwwlkf1lem3  29259  clwwisshclwwslem  29267  clwwlkinwwlk  29293  clwwlkel  29299  clwwlkf  29300  clwwlkf1  29302  clwwlknwwlksnb  29308  wwlksubclwwlk  29311  erclwwlknref  29322  clwwlknonwwlknonb  29359  numclwwlkqhash  29628  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  ipval2  29960  ipasslem3  30086  ipasslem4  30087  nn0min  32026  frobrhm  32382  znfermltl  32479  ply1fermltlchr  32662  ply1fermltl  32663  esumcst  33061  eulerpartlemb  33367  fibp1  33400  ballotlem1  33485  subfacp1lem6  34176  subfaclim  34179  subfacval3  34180  snmlff  34320  bcprod  34708  faclim2  34718  nn0prpwlem  35207  knoppndvlem18  35405  opnmbllem0  36524  nnubfi  36618  nninfnub  36619  geomcau  36627  heiborlem5  36683  heiborlem6  36684  heiborlem7  36685  heiborlem8  36686  bfplem1  36690  lcmineqlem12  40905  aks4d1p1p2  40935  2ap1caineq  40961  nn0expgcd  41226  dvdsexpnn  41231  dvdsexpnn0  41232  zaddcomlem  41324  dffltz  41376  fltnltalem  41404  irrapxlem2  41561  pellexlem1  41567  pellexlem5  41571  pellqrex  41617  monotoddzzfi  41681  jm2.17c  41701  acongeq  41722  jm2.18  41727  jm2.23  41735  jm2.26lem3  41740  jm3.1  41759  expdiophlem1  41760  idomrootle  41937  idomodle  41938  proot1ex  41943  rp-isfinite6  42269  cnvtrclfv  42475  cotrclrcl  42493  inductionexd  42906  binomcxplemnotnn0  43115  nnne1ge2  44001  dvnmptconst  44657  stoweidlem3  44719  stoweidlem7  44723  stoweidlem34  44750  wallispilem4  44784  wallispilem5  44785  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem2  44791  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem7  44796  stirlinglem11  44800  stirlinglem14  44803  stirlinglem15  44804  stirlingr  44806  fourierdlem15  44838  fourierdlem21  44844  fourierdlem22  44845  fourierdlem92  44914  fourierdlem112  44934  fouriersw  44947  sge0rpcpnf  45137  sge0ad2en  45147  ovnsubaddlem1  45286  ovnsubaddlem2  45287  ovolval5lem1  45368  ovolval5lem2  45369  iccpartiltu  46090  iccpartigtl  46091  iccpartlt  46092  iccpartleu  46096  iccpartrn  46098  iccelpart  46101  iccpartiun  46102  iccpartdisj  46105  sqrtpwpw2p  46206  fmtnosqrt  46207  odz2prm2pw  46231  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  2pwp1prm  46257  lighneallem1  46273  lighneallem2  46274  lighneallem3  46275  lighneallem4a  46276  lighneallem4  46278  nnpw2evenALTV  46370  dfwppr  46406  cznabel  46852  cznrng  46853  ztprmneprm  47023  altgsumbc  47028  altgsumbcALT  47029  pw2m1lepw2m1  47201  nneom  47213  logbpw2m1  47253  blennn  47261  blenpw2m1  47265  blengt1fldiv2p1  47279  dignn0ldlem  47288  dignnld  47289  dig2nn1st  47291  dignn0flhalflem1  47301  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  itcovalt2lem2lem1  47359  eenglngeehlnm  47425