Theorem nnnn0 12616

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 12612	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3904	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕcn 12338  ℕ₀cn0 12609

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-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-n0 12610

This theorem is used by:  nnnn0i  12617  elnnnn0b  12653  elnnnn0c  12654  elz2  12714  nn0ind-raph  12802  zindd  12803  fzo1fzo0n0  13853  ubmelfzo  13868  elfzom1elp1fzo  13870  fzo0sn0fzo1  13893  quoremnn0ALT  14000  modmulnn  14032  modsumfzodifsn  14090  addmodlteq  14092  expneg  14215  expcllem  14218  expcl2lem  14219  expeq0  14238  mulexpz  14248  expmordi  14313  rpexpmord  14314  expnlbnd  14380  expmulnbnd  14382  digit2  14383  digit1  14384  facmapnn  14432  facdiv  14434  faclbnd  14437  faclbnd3  14439  faclbnd4lem3  14442  faclbnd4lem4  14443  faclbnd5  14445  faclbnd6  14446  bcval5  14465  ishashinf  14611  iswrdi  14665  pfxn0  14840  repswfsts  14936  repswlsw  14937  repswcshw  14967  relexpnnrn  15203  relexpaddg  15211  absexpz  15477  isercoll  15840  summolem3  15885  summolem2a  15886  climcndslem2  16024  climcnds  16025  harmonic  16033  arisum  16034  expcnv  16038  geo2sum  16047  geo2lim  16049  geoisum1  16053  geoisum1c  16054  0.999...  16055  mertenslem2  16059  fallfacfwd  16207  0fallfac  16208  0risefac  16209  ef0lem  16249  ege2le3  16261  efaddlem  16264  efexp  16274  rpnnen2lem2  16388  rpnnen2lem4  16390  ruclem12  16414  dvdsmodexp  16435  dvdsexp2im  16502  nn0enne  16552  nnehalf  16554  nno  16557  nn0o  16558  pwp1fsum  16566  divalg2  16580  ndvdssub  16584  gcdmultiplez  16713  gcddiv  16729  rpmulgcd  16736  rplpwr  16737  nn0expgcd  16743  dvdsexpnn  16745  eucalgf  16763  lcmflefac  16828  1nprm  16859  2mulprm  16873  isprm5  16888  isprm6  16895  prmdvdsexp  16896  phicl2  16950  phibndlem  16952  phiprmpw  16958  crth  16960  eulerthlem2  16964  hashgcdlem  16970  phisum  16973  pythagtriplem10  17003  pythagtriplem6  17004  pythagtriplem7  17005  pythagtriplem12  17009  pythagtriplem14  17011  pclem  17021  pcexp  17042  pcid  17056  pcprod  17078  pcbc  17083  prmpwdvds  17087  infpnlem1  17093  infpnlem2  17094  prmunb  17097  prmreclem6  17104  1arith  17110  vdwapf  17155  0hashbc  17190  ram0  17205  prmdvdsprmo  17225  prmdvdsprmop  17226  prmolefac  17229  prmgaplem1  17232  prmgaplem2  17233  prmgapprmolem  17244  prmgapprmo  17245  cshwrepswhash1  17285  smndex1n0mnd  19116  ghmmulg  19447  odmodnn0  19759  dfod2  19783  submod  19788  prmirredlem  21783  prmirred  21785  znf1o  21862  znhash  21869  znfi  21870  znfld  21871  znidomb  21872  znunithash  21875  znrrg  21876  frobrhm  21886  cply1mul  22619  cply1coe0  22624  cply1coe0bi  22625  ply1fermltlchr  22635  cpmatmcllem  23041  m2cpm  23064  m2cpminvid2lem  23077  fvmptnn04ifa  23173  chfacfisf  23177  chfacfisfcpmat  23178  chfacffsupp  23179  chfacfscmul0  23181  chfacfscmulfsupp  23182  chfacfscmulgsum  23183  chfacfpmmul0  23185  chfacfpmmulfsupp  23186  chfacfpmmulgsum  23187  chfacfpmmulgsum2  23188  cayhamlem1  23189  cpmadugsumlemF  23199  tgpmulg  24417  cmodscexp  25447  cphipval  25569  ovollb2lem  25814  ovoliunlem1  25828  ovoliunlem3  25830  uniioombllem3  25911  uniioombllem4  25912  opnmbllem  25927  mbfi1fseqlem1  26041  mbfi1fseqlem3  26043  mbfi1fseqlem4  26044  mbfi1fseqlem5  26045  mbfi1fseqlem6  26046  dvexp  26278  dvexp3  26303  idomrootle  26496  plyco  26565  dgrcolem1  26597  plydivex  26623  aaliou3lem2  26675  aaliou3lem3  26676  aaliou3lem5  26679  aaliou3lem6  26680  aaliou3lem7  26681  aaliou3lem9  26682  radcnvlem2  26746  dvradcnv  26753  pserdv2  26762  abelthlem6  26768  abelthlem9  26772  logtayllem  26992  logtayl  26993  logtaylsum  26994  logtayl2  26995  cxproot  27023  root1id  27087  logbgcd1irr  27127  atantayl  27270  atantayl2  27271  leibpilem2  27274  leibpi  27275  birthdaylem2  27285  birthdaylem3  27286  dfef2  27303  basellem2  27414  basellem4  27416  basellem5  27417  basellem6  27418  basellem8  27420  isppw2  27447  vmappw  27448  sqf11  27471  vma1  27498  1sgm2ppw  27532  chtublem  27543  fsumvma2  27546  vmasum  27548  dchrelbas4  27575  dchrzrhcl  27577  dchrfi  27587  dchrhash  27603  pcbcctr  27608  bclbnd  27612  bposlem1  27616  lgsval4a  27651  lgsdchrval  27686  lgsdchr  27687  gausslemma2dlem0c  27690  gausslemma2dlem0d  27691  gausslemma2dlem6  27704  2lgslem1a1  27721  2lgslem1c  27725  2lgslem3a1  27732  2lgslem3b1  27733  2lgslem3c1  27734  2lgslem3d1  27735  2sqreunnlem1  27781  2sqreunnltblem  27783  rplogsumlem2  27817  dchrisumlem2  27822  ostth2lem1  27950  ostth2lem3  27967  ostth3  27970  fltoprm  28000  cusgrsize2inds  30039  pthdivtx  30317  cyclnumvtx  30393  crctcshwlkn0lem4  30407  crctcshwlkn0lem5  30408  crctcshwlkn0lem7  30410  0enwwlksnge1  30458  rusgr0edg  30570  clwlkclwwlkf1lem2  30601  clwlkclwwlkf1lem3  30602  clwwisshclwwslem  30610  clwwlkinwwlk  30636  clwwlkel  30642  clwwlkf  30643  clwwlkf1  30645  clwwlknwwlksnb  30651  wwlksubclwwlk  30654  erclwwlknref  30665  clwwlknonwwlknonb  30702  numclwwlkqhash  30981  numclwwlk2lem1  30982  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  ipval2  31314  ipasslem3  31440  ipasslem4  31441  nn0min  33458  znfermltl  33968  ply1fermltl  34164  esumcst  34741  eulerpartlemb  35046  fibp1  35079  ballotlem1  35165  subfacp1lem6  36036  subfaclim  36039  subfacval3  36040  snmlff  36180  bcprod  36595  faclim2  36605  nn0prpwlem  37202  knoppndvlem18  37487  opnmbllem0  38667  nnubfi  38777  nninfnub  38778  geomcau  38786  heiborlem5  38842  heiborlem6  38843  heiborlem7  38844  heiborlem8  38845  bfplem1  38849  lcmineqlem12  43183  aks4d1p1p2  43213  primrootscoprmpow  43242  2ap1caineq  43288  dvdsexpnn0  43479  zaddcomlem  43620  fidomncyc  43692  dffltz  43763  fltnltalem  43766  irrapxlem2  43923  pellexlem1  43929  pellexlem5  43933  pellqrex  43979  monotoddzzfi  44042  jm2.17c  44062  acongeq  44083  jm2.18  44088  jm2.23  44096  jm2.26lem3  44101  jm3.1  44120  expdiophlem1  44121  idomodle  44286  proot1ex  44291  rp-isfinite6  44612  cnvtrclfv  44817  cotrclrcl  44835  inductionexd  45248  binomcxplemnotnn0  45433  nnne1ge2  46400  dvnmptconst  47044  stoweidlem3  47106  stoweidlem7  47110  stoweidlem34  47137  wallispilem4  47171  wallispilem5  47172  wallispi2lem1  47174  wallispi2lem2  47175  stirlinglem2  47178  stirlinglem3  47179  stirlinglem4  47180  stirlinglem5  47181  stirlinglem7  47183  stirlinglem11  47187  stirlinglem14  47190  stirlinglem15  47191  stirlingr  47193  fourierdlem15  47225  fourierdlem21  47231  fourierdlem22  47232  fourierdlem92  47301  fourierdlem112  47321  fouriersw  47334  sge0rpcpnf  47524  sge0ad2en  47534  ovnsubaddlem1  47673  ovnsubaddlem2  47674  ovolval5lem1  47755  ovolval5lem2  47756  ceilhalfelfzo1  48497  modlt0b  48532  muldvdsfacm1  48550  iccpartiltu  48597  iccpartigtl  48598  iccpartlt  48599  iccpartleu  48603  iccpartrn  48605  iccelpart  48608  iccpartiun  48609  iccpartdisj  48612  sqrtpwpw2p  48716  fmtnosqrt  48717  odz2prm2pw  48741  fmtnoprmfac1lem  48742  fmtnoprmfac1  48743  2pwp1prm  48767  lighneallem1  48783  lighneallem2  48784  lighneallem3  48785  lighneallem4a  48786  lighneallem4  48788  nnpw2evenALTV  48893  dfwppr  48929  gpgorder  49250  gpgedgvtx0  49252  gpgedgvtx1  49253  cznabel  49450  cznrng  49451  ztprmneprm  49552  altgsumbc  49557  altgsumbcALT  49558  pw2m1lepw2m1  49725  nneom  49732  logbpw2m1  49772  blennn  49780  blenpw2m1  49784  blengt1fldiv2p1  49798  dignn0ldlem  49807  dignnld  49808  dig2nn1st  49810  dignn0flhalflem1  49820  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  itcovalt2lem2lem1  49878