Theorem nnnn0 12643

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℕcn 12365  ℕ₀cn0 12636

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-n0 12637

This theorem is used by:  nnnn0i  12644  elnnnn0b  12680  elnnnn0c  12681  elz2  12741  nn0ind-raph  12829  zindd  12830  fzo1fzo0n0  13880  ubmelfzo  13895  elfzom1elp1fzo  13897  fzo0sn0fzo1  13920  quoremnn0ALT  14027  modmulnn  14059  modsumfzodifsn  14117  addmodlteq  14119  expneg  14242  expcllem  14245  expcl2lem  14246  expeq0  14265  mulexpz  14275  expmordi  14340  rpexpmord  14341  expnlbnd  14407  expmulnbnd  14409  digit2  14410  digit1  14411  facmapnn  14459  facdiv  14461  faclbnd  14464  faclbnd3  14466  faclbnd4lem3  14469  faclbnd4lem4  14470  faclbnd5  14472  faclbnd6  14473  bcval5  14492  ishashinf  14638  iswrdi  14692  pfxn0  14867  repswfsts  14963  repswlsw  14964  repswcshw  14994  relexpnnrn  15230  relexpaddg  15238  absexpz  15504  isercoll  15867  summolem3  15912  summolem2a  15913  climcndslem2  16051  climcnds  16052  harmonic  16060  arisum  16061  expcnv  16065  geo2sum  16074  geo2lim  16076  geoisum1  16080  geoisum1c  16081  0.999...  16082  mertenslem2  16086  fallfacfwd  16234  0fallfac  16235  0risefac  16236  ef0lem  16276  ege2le3  16288  efaddlem  16291  efexp  16301  rpnnen2lem2  16415  rpnnen2lem4  16417  ruclem12  16441  dvdsmodexp  16462  dvdsexp2im  16529  nn0enne  16579  nnehalf  16581  nno  16584  nn0o  16585  pwp1fsum  16593  divalg2  16607  ndvdssub  16611  gcdmultiplez  16740  gcddiv  16756  rpmulgcd  16763  rplpwr  16764  nn0expgcd  16770  dvdsexpnn  16772  eucalgf  16790  lcmflefac  16855  1nprm  16886  2mulprm  16900  isprm5  16915  isprm6  16922  prmdvdsexp  16923  phicl2  16977  phibndlem  16979  phiprmpw  16985  crth  16987  eulerthlem2  16991  hashgcdlem  16997  phisum  17000  pythagtriplem10  17030  pythagtriplem6  17031  pythagtriplem7  17032  pythagtriplem12  17036  pythagtriplem14  17038  pclem  17048  pcexp  17069  pcid  17083  pcprod  17105  pcbc  17110  prmpwdvds  17114  infpnlem1  17120  infpnlem2  17121  prmunb  17124  prmreclem6  17131  1arith  17137  vdwapf  17182  0hashbc  17217  ram0  17232  prmdvdsprmo  17252  prmdvdsprmop  17253  prmolefac  17256  prmgaplem1  17259  prmgaplem2  17260  prmgapprmolem  17271  prmgapprmo  17272  cshwrepswhash1  17312  smndex1n0mnd  19143  ghmmulg  19474  odmodnn0  19787  dfod2  19811  submod  19816  prmirredlem  21811  prmirred  21813  znf1o  21890  znhash  21897  znfi  21898  znfld  21899  znidomb  21900  znunithash  21903  znrrg  21904  frobrhm  21914  cply1mul  22647  cply1coe0  22652  cply1coe0bi  22653  ply1fermltlchr  22663  cpmatmcllem  23069  m2cpm  23092  m2cpminvid2lem  23105  fvmptnn04ifa  23201  chfacfisf  23205  chfacfisfcpmat  23206  chfacffsupp  23207  chfacfscmul0  23209  chfacfscmulfsupp  23210  chfacfscmulgsum  23211  chfacfpmmul0  23213  chfacfpmmulfsupp  23214  chfacfpmmulgsum  23215  chfacfpmmulgsum2  23216  cayhamlem1  23217  cpmadugsumlemF  23227  tgpmulg  24445  cmodscexp  25475  cphipval  25597  ovollb2lem  25842  ovoliunlem1  25856  ovoliunlem3  25858  uniioombllem3  25939  uniioombllem4  25940  opnmbllem  25955  mbfi1fseqlem1  26069  mbfi1fseqlem3  26071  mbfi1fseqlem4  26072  mbfi1fseqlem5  26073  mbfi1fseqlem6  26074  dvexp  26306  dvexp3  26331  idomrootle  26524  plyco  26593  dgrcolem1  26625  plydivex  26651  aaliou3lem2  26703  aaliou3lem3  26704  aaliou3lem5  26707  aaliou3lem6  26708  aaliou3lem7  26709  aaliou3lem9  26710  radcnvlem2  26774  dvradcnv  26781  pserdv2  26790  abelthlem6  26796  abelthlem9  26800  logtayllem  27020  logtayl  27021  logtaylsum  27022  logtayl2  27023  cxproot  27051  root1id  27115  logbgcd1irr  27155  atantayl  27298  atantayl2  27299  leibpilem2  27302  leibpi  27303  birthdaylem2  27313  birthdaylem3  27314  dfef2  27331  basellem2  27442  basellem4  27444  basellem5  27445  basellem6  27446  basellem8  27448  isppw2  27475  vmappw  27476  sqf11  27499  vma1  27526  1sgm2ppw  27560  chtublem  27571  fsumvma2  27574  vmasum  27576  dchrelbas4  27603  dchrzrhcl  27605  dchrfi  27615  dchrhash  27631  pcbcctr  27636  bclbnd  27640  bposlem1  27644  lgsval4a  27679  lgsdchrval  27714  lgsdchr  27715  gausslemma2dlem0c  27718  gausslemma2dlem0d  27719  gausslemma2dlem6  27732  2lgslem1a1  27749  2lgslem1c  27753  2lgslem3a1  27760  2lgslem3b1  27761  2lgslem3c1  27762  2lgslem3d1  27763  2sqreunnlem1  27809  2sqreunnltblem  27811  rplogsumlem2  27845  dchrisumlem2  27850  ostth2lem1  27978  ostth2lem3  27995  ostth3  27998  fltoprm  28028  cusgrsize2inds  30067  pthdivtx  30345  cyclnumvtx  30421  crctcshwlkn0lem4  30435  crctcshwlkn0lem5  30436  crctcshwlkn0lem7  30438  0enwwlksnge1  30486  rusgr0edg  30598  clwlkclwwlkf1lem2  30629  clwlkclwwlkf1lem3  30630  clwwisshclwwslem  30638  clwwlkinwwlk  30664  clwwlkel  30670  clwwlkf  30671  clwwlkf1  30673  clwwlknwwlksnb  30679  wwlksubclwwlk  30682  erclwwlknref  30693  clwwlknonwwlknonb  30730  numclwwlkqhash  31009  numclwwlk2lem1  31010  numclwlk2lem2f  31011  numclwlk2lem2f1o  31013  ipval2  31342  ipasslem3  31468  ipasslem4  31469  nn0min  33485  znfermltl  34006  ply1fermltl  34201  esumcst  34778  eulerpartlemb  35083  fibp1  35116  ballotlem1  35202  subfacp1lem6  36130  subfaclim  36133  subfacval3  36134  snmlff  36274  bcprod  36694  faclim2  36704  nn0prpwlem  37301  knoppndvlem18  37586  opnmbllem0  38779  nnubfi  38887  nninfnub  38888  geomcau  38896  heiborlem5  38952  heiborlem6  38953  heiborlem7  38954  heiborlem8  38955  bfplem1  38959  lcmineqlem12  43293  aks4d1p1p2  43323  primrootscoprmpow  43352  2ap1caineq  43398  dvdsexpnn0  43590  zaddcomlem  43731  fidomncyc  43803  dffltz  43874  fltnltalem  43877  irrapxlem2  44034  pellexlem1  44040  pellexlem5  44044  pellqrex  44090  monotoddzzfi  44153  jm2.17c  44173  acongeq  44194  jm2.18  44199  jm2.23  44207  jm2.26lem3  44212  jm3.1  44231  expdiophlem1  44232  idomodle  44396  proot1ex  44401  rp-isfinite6  44722  cnvtrclfv  44927  cotrclrcl  44945  inductionexd  45358  binomcxplemnotnn0  45543  nnne1ge2  46522  dvnmptconst  47166  stoweidlem3  47228  stoweidlem7  47232  stoweidlem34  47259  wallispilem4  47293  wallispilem5  47294  wallispi2lem1  47296  wallispi2lem2  47297  stirlinglem2  47300  stirlinglem3  47301  stirlinglem4  47302  stirlinglem5  47303  stirlinglem7  47305  stirlinglem11  47309  stirlinglem14  47312  stirlinglem15  47313  stirlingr  47315  fourierdlem15  47347  fourierdlem21  47353  fourierdlem22  47354  fourierdlem92  47423  fourierdlem112  47443  fouriersw  47456  sge0rpcpnf  47646  sge0ad2en  47656  ovnsubaddlem1  47795  ovnsubaddlem2  47796  ovolval5lem1  47877  ovolval5lem2  47878  ceilhalfelfzo1  48619  modlt0b  48654  muldvdsfacm1  48672  iccpartiltu  48719  iccpartigtl  48720  iccpartlt  48721  iccpartleu  48725  iccpartrn  48727  iccelpart  48730  iccpartiun  48731  iccpartdisj  48734  sqrtpwpw2p  48838  fmtnosqrt  48839  odz2prm2pw  48863  fmtnoprmfac1lem  48864  fmtnoprmfac1  48865  2pwp1prm  48889  lighneallem1  48905  lighneallem2  48906  lighneallem3  48907  lighneallem4a  48908  lighneallem4  48910  nnpw2evenALTV  49015  dfwppr  49051  gpgorder  49372  gpgedgvtx0  49374  gpgedgvtx1  49375  cznabel  49572  cznrng  49573  ztprmneprm  49674  altgsumbc  49679  altgsumbcALT  49680  pw2m1lepw2m1  49847  nneom  49854  logbpw2m1  49894  blennn  49902  blenpw2m1  49906  blengt1fldiv2p1  49920  dignn0ldlem  49929  dignnld  49930  dig2nn1st  49932  dignn0flhalflem1  49942  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947  itcovalt2lem2lem1  50000