Theorem nnnn0 12485

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 12207  ℕ₀cn0 12478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-n0 12479

This theorem is referenced by:  nnnn0i  12486  elnnnn0b  12522  elnnnn0c  12523  elz2  12583  nn0ind-raph  12670  zindd  12671  fzo1fzo0n0  13718  ubmelfzo  13733  elfzom1elp1fzo  13735  fzo0sn0fzo1  13758  quoremnn0ALT  13864  modmulnn  13896  modsumfzodifsn  13954  addmodlteq  13956  expneg  14079  expcllem  14082  expcl2lem  14083  expeq0  14102  mulexpz  14112  expmordi  14177  rpexpmord  14178  expnlbnd  14243  expmulnbnd  14245  digit2  14246  digit1  14247  facmapnn  14295  facdiv  14297  faclbnd  14300  faclbnd3  14302  faclbnd4lem3  14305  faclbnd4lem4  14306  faclbnd5  14308  faclbnd6  14309  bcval5  14328  ishashinf  14473  iswrdi  14527  pfxn0  14697  repswfsts  14791  repswlsw  14792  repswcshw  14822  relexpnnrn  15055  relexpaddg  15063  absexpz  15315  isercoll  15678  summolem3  15724  summolem2a  15725  climcndslem2  15863  climcnds  15864  harmonic  15872  arisum  15873  expcnv  15877  geo2sum  15886  geo2lim  15888  geoisum1  15892  geoisum1c  15893  0.999...  15894  mertenslem2  15898  fallfacfwd  16049  0fallfac  16050  0risefac  16051  ef0lem  16091  ege2le3  16103  efaddlem  16106  efexp  16116  rpnnen2lem2  16230  rpnnen2lem4  16232  ruclem12  16256  dvdsmodexp  16277  dvdsexp2im  16344  nn0enne  16394  nnehalf  16396  nno  16399  nn0o  16400  pwp1fsum  16408  divalg2  16422  ndvdssub  16426  gcdmultiplez  16552  gcddiv  16568  rpmulgcd  16574  rplpwr  16575  nn0expgcd  16581  dvdssqlem  16583  eucalgf  16600  lcmflefac  16665  1nprm  16696  2mulprm  16710  isprm5  16725  isprm6  16732  prmdvdsexp  16733  phicl2  16786  phibndlem  16788  phiprmpw  16794  crth  16796  eulerthlem2  16800  hashgcdlem  16806  phisum  16809  pythagtriplem10  16839  pythagtriplem6  16840  pythagtriplem7  16841  pythagtriplem12  16845  pythagtriplem14  16847  pclem  16857  pcexp  16878  pcid  16892  pcprod  16914  pcbc  16919  prmpwdvds  16923  infpnlem1  16929  infpnlem2  16930  prmunb  16933  prmreclem6  16940  1arith  16946  vdwapf  16991  0hashbc  17026  ram0  17041  prmdvdsprmo  17061  prmdvdsprmop  17062  prmolefac  17065  prmgaplem1  17068  prmgaplem2  17069  prmgapprmolem  17080  prmgapprmo  17081  cshwrepswhash1  17121  smndex1n0mnd  18932  ghmmulg  19251  odmodnn0  19563  dfod2  19587  submod  19592  prmirredlem  21504  prmirred  21506  znf1o  21583  znhash  21590  znfi  21591  znfld  21592  znidomb  21593  znunithash  21596  znrrg  21597  frobrhm  21607  cply1mul  22339  cply1coe0  22344  cply1coe0bi  22345  ply1fermltlchr  22355  cpmatmcllem  22758  m2cpm  22781  m2cpminvid2lem  22794  fvmptnn04ifa  22890  chfacfisf  22894  chfacfisfcpmat  22895  chfacffsupp  22896  chfacfscmul0  22898  chfacfscmulfsupp  22899  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulfsupp  22903  chfacfpmmulgsum  22904  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmadugsumlemF  22916  tgpmulg  24133  cmodscexp  25163  cphipval  25285  ovollb2lem  25530  ovoliunlem1  25544  ovoliunlem3  25546  uniioombllem3  25627  uniioombllem4  25628  opnmbllem  25643  mbfi1fseqlem1  25757  mbfi1fseqlem3  25759  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mbfi1fseqlem6  25762  dvexp  25995  dvexp3  26020  idomrootle  26213  plyco  26281  dgrcolem1  26313  plydivex  26338  aaliou3lem2  26384  aaliou3lem3  26385  aaliou3lem5  26388  aaliou3lem6  26389  aaliou3lem7  26390  aaliou3lem9  26391  radcnvlem2  26454  dvradcnv  26461  pserdv2  26470  abelthlem6  26476  abelthlem9  26480  logtayllem  26701  logtayl  26702  logtaylsum  26703  logtayl2  26704  cxproot  26732  root1id  26796  logbgcd1irr  26836  atantayl  26979  atantayl2  26980  leibpilem2  26983  leibpi  26984  birthdaylem2  26994  birthdaylem3  26995  dfef2  27012  basellem2  27123  basellem4  27125  basellem5  27126  basellem6  27127  basellem8  27129  isppw2  27156  vmappw  27157  sqf11  27180  vma1  27207  1sgm2ppw  27241  chtublem  27252  fsumvma2  27255  vmasum  27257  dchrelbas4  27284  dchrzrhcl  27286  dchrfi  27296  dchrhash  27312  pcbcctr  27317  bclbnd  27321  bposlem1  27325  lgsval4a  27360  lgsdchrval  27395  lgsdchr  27396  gausslemma2dlem0c  27399  gausslemma2dlem0d  27400  gausslemma2dlem6  27413  2lgslem1a1  27430  2lgslem1c  27434  2lgslem3a1  27441  2lgslem3b1  27442  2lgslem3c1  27443  2lgslem3d1  27444  2sqreunnlem1  27490  2sqreunnltblem  27492  rplogsumlem2  27526  dchrisumlem2  27531  ostth2lem1  27659  ostth2lem3  27676  ostth3  27679  cusgrsize2inds  29600  pthdivtx  29873  cyclnumvtx  29946  crctcshwlkn0lem4  29959  crctcshwlkn0lem5  29960  crctcshwlkn0lem7  29962  0enwwlksnge1  30010  rusgr0edg  30122  clwlkclwwlkf1lem2  30153  clwlkclwwlkf1lem3  30154  clwwisshclwwslem  30162  clwwlkinwwlk  30188  clwwlkel  30194  clwwlkf  30195  clwwlkf1  30197  clwwlknwwlksnb  30203  wwlksubclwwlk  30206  erclwwlknref  30217  clwwlknonwwlknonb  30254  numclwwlkqhash  30523  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  ipval2  30856  ipasslem3  30982  ipasslem4  30983  nn0min  32973  znfermltl  33513  ply1fermltl  33743  esumcst  34321  eulerpartlemb  34626  fibp1  34659  ballotlem1  34745  subfacp1lem6  35499  subfaclim  35502  subfacval3  35503  snmlff  35643  bcprod  36052  faclim2  36062  nn0prpwlem  36646  knoppndvlem18  36931  opnmbllem0  38119  nnubfi  38213  nninfnub  38214  geomcau  38222  heiborlem5  38278  heiborlem6  38279  heiborlem7  38280  heiborlem8  38281  bfplem1  38285  lcmineqlem12  42621  aks4d1p1p2  42651  primrootscoprmpow  42680  2ap1caineq  42726  dvdsexpnn  42906  dvdsexpnn0  42907  zaddcomlem  43049  fidomncyc  43117  dffltz  43180  fltnltalem  43208  irrapxlem2  43364  pellexlem1  43370  pellexlem5  43374  pellqrex  43420  monotoddzzfi  43483  jm2.17c  43503  acongeq  43524  jm2.18  43529  jm2.23  43537  jm2.26lem3  43542  jm3.1  43561  expdiophlem1  43562  idomodle  43732  proot1ex  43737  rp-isfinite6  44058  cnvtrclfv  44264  cotrclrcl  44282  inductionexd  44695  binomcxplemnotnn0  44896  nnne1ge2  45834  dvnmptconst  46479  stoweidlem3  46541  stoweidlem7  46545  stoweidlem34  46572  wallispilem4  46606  wallispilem5  46607  wallispi2lem1  46609  wallispi2lem2  46610  stirlinglem2  46613  stirlinglem3  46614  stirlinglem4  46615  stirlinglem5  46616  stirlinglem7  46618  stirlinglem11  46622  stirlinglem14  46625  stirlinglem15  46626  stirlingr  46628  fourierdlem15  46660  fourierdlem21  46666  fourierdlem22  46667  fourierdlem92  46736  fourierdlem112  46756  fouriersw  46769  sge0rpcpnf  46959  sge0ad2en  46969  ovnsubaddlem1  47108  ovnsubaddlem2  47109  ovolval5lem1  47190  ovolval5lem2  47191  nthrucw  47426  ceilhalfelfzo1  47892  modlt0b  47927  muldvdsfacm1  47945  iccpartiltu  47992  iccpartigtl  47993  iccpartlt  47994  iccpartleu  47998  iccpartrn  48000  iccelpart  48003  iccpartiun  48004  iccpartdisj  48007  sqrtpwpw2p  48111  fmtnosqrt  48112  odz2prm2pw  48136  fmtnoprmfac1lem  48137  fmtnoprmfac1  48138  2pwp1prm  48162  lighneallem1  48178  lighneallem2  48179  lighneallem3  48180  lighneallem4a  48181  lighneallem4  48183  nnpw2evenALTV  48288  dfwppr  48324  gpgorder  48645  gpgedgvtx0  48647  gpgedgvtx1  48648  cznabel  48846  cznrng  48847  ztprmneprm  48933  altgsumbc  48938  altgsumbcALT  48939  pw2m1lepw2m1  49106  nneom  49113  logbpw2m1  49153  blennn  49161  blenpw2m1  49165  blengt1fldiv2p1  49179  dignn0ldlem  49188  dignnld  49189  dig2nn1st  49191  dignn0flhalflem1  49201  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  itcovalt2lem2lem1  49259  eenglngeehlnm  49325