Theorem nnnn0 12408

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-n0 12402

This theorem is referenced by:  nnnn0i  12409  elnnnn0b  12445  elnnnn0c  12446  elz2  12506  nn0ind-raph  12592  zindd  12593  fzo1fzo0n0  13631  ubmelfzo  13646  elfzom1elp1fzo  13648  fzo0sn0fzo1  13671  quoremnn0ALT  13777  modmulnn  13809  modsumfzodifsn  13867  addmodlteq  13869  expneg  13992  expcllem  13995  expcl2lem  13996  expeq0  14015  mulexpz  14025  expmordi  14090  rpexpmord  14091  expnlbnd  14156  expmulnbnd  14158  digit2  14159  digit1  14160  facmapnn  14208  facdiv  14210  faclbnd  14213  faclbnd3  14215  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd5  14221  faclbnd6  14222  bcval5  14241  ishashinf  14386  iswrdi  14440  pfxn0  14610  repswfsts  14704  repswlsw  14705  repswcshw  14735  relexpnnrn  14968  relexpaddg  14976  absexpz  15228  isercoll  15591  summolem3  15637  summolem2a  15638  climcndslem2  15773  climcnds  15774  harmonic  15782  arisum  15783  expcnv  15787  geo2sum  15796  geo2lim  15798  geoisum1  15802  geoisum1c  15803  0.999...  15804  mertenslem2  15808  fallfacfwd  15959  0fallfac  15960  0risefac  15961  ef0lem  16001  ege2le3  16013  efaddlem  16016  efexp  16026  rpnnen2lem2  16140  rpnnen2lem4  16142  ruclem12  16166  dvdsmodexp  16187  dvdsexp2im  16254  nn0enne  16304  nnehalf  16306  nno  16309  nn0o  16310  pwp1fsum  16318  divalg2  16332  ndvdssub  16336  gcdmultiplez  16462  gcddiv  16478  rpmulgcd  16484  rplpwr  16485  nn0expgcd  16491  dvdssqlem  16493  eucalgf  16510  lcmflefac  16575  1nprm  16606  2mulprm  16620  isprm5  16634  isprm6  16641  prmdvdsexp  16642  phicl2  16695  phibndlem  16697  phiprmpw  16703  crth  16705  eulerthlem2  16709  hashgcdlem  16715  phisum  16718  pythagtriplem10  16748  pythagtriplem6  16749  pythagtriplem7  16750  pythagtriplem12  16754  pythagtriplem14  16756  pclem  16766  pcexp  16787  pcid  16801  pcprod  16823  pcbc  16828  prmpwdvds  16832  infpnlem1  16838  infpnlem2  16839  prmunb  16842  prmreclem6  16849  1arith  16855  vdwapf  16900  0hashbc  16935  ram0  16950  prmdvdsprmo  16970  prmdvdsprmop  16971  prmolefac  16974  prmgaplem1  16977  prmgaplem2  16978  prmgapprmolem  16989  prmgapprmo  16990  cshwrepswhash1  17030  smndex1n0mnd  18837  ghmmulg  19157  odmodnn0  19469  dfod2  19493  submod  19498  prmirredlem  21427  prmirred  21429  znf1o  21506  znhash  21513  znfi  21514  znfld  21515  znidomb  21516  znunithash  21519  znrrg  21520  frobrhm  21530  cply1mul  22240  cply1coe0  22245  cply1coe0bi  22246  ply1fermltlchr  22256  cpmatmcllem  22662  m2cpm  22685  m2cpminvid2lem  22698  fvmptnn04ifa  22794  chfacfisf  22798  chfacfisfcpmat  22799  chfacffsupp  22800  chfacfscmul0  22802  chfacfscmulfsupp  22803  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulfsupp  22807  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadugsumlemF  22820  tgpmulg  24037  cmodscexp  25077  cphipval  25199  ovollb2lem  25445  ovoliunlem1  25459  ovoliunlem3  25461  uniioombllem3  25542  uniioombllem4  25543  opnmbllem  25558  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  dvexp  25913  dvexp3  25938  idomrootle  26134  plyco  26202  dgrcolem1  26235  plydivex  26261  aaliou3lem2  26307  aaliou3lem3  26308  aaliou3lem5  26311  aaliou3lem6  26312  aaliou3lem7  26313  aaliou3lem9  26314  radcnvlem2  26379  dvradcnv  26386  pserdv2  26396  abelthlem6  26402  abelthlem9  26406  logtayllem  26624  logtayl  26625  logtaylsum  26626  logtayl2  26627  cxproot  26655  root1id  26720  logbgcd1irr  26760  atantayl  26903  atantayl2  26904  leibpilem2  26907  leibpi  26908  birthdaylem2  26918  birthdaylem3  26919  dfef2  26937  basellem2  27048  basellem4  27050  basellem5  27051  basellem6  27052  basellem8  27054  isppw2  27081  vmappw  27082  sqf11  27105  vma1  27132  1sgm2ppw  27167  chtublem  27178  fsumvma2  27181  vmasum  27183  dchrelbas4  27210  dchrzrhcl  27212  dchrfi  27222  dchrhash  27238  pcbcctr  27243  bclbnd  27247  bposlem1  27251  lgsval4a  27286  lgsdchrval  27321  lgsdchr  27322  gausslemma2dlem0c  27325  gausslemma2dlem0d  27326  gausslemma2dlem6  27339  2lgslem1a1  27356  2lgslem1c  27360  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2sqreunnlem1  27416  2sqreunnltblem  27418  rplogsumlem2  27452  dchrisumlem2  27457  ostth2lem1  27585  ostth2lem3  27602  ostth3  27605  cusgrsize2inds  29527  pthdivtx  29800  cyclnumvtx  29873  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem7  29889  0enwwlksnge1  29937  rusgr0edg  30049  clwlkclwwlkf1lem2  30080  clwlkclwwlkf1lem3  30081  clwwisshclwwslem  30089  clwwlkinwwlk  30115  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  clwwlknwwlksnb  30130  wwlksubclwwlk  30133  erclwwlknref  30144  clwwlknonwwlknonb  30181  numclwwlkqhash  30450  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  ipval2  30782  ipasslem3  30908  ipasslem4  30909  nn0min  32901  znfermltl  33447  ply1fermltl  33667  esumcst  34220  eulerpartlemb  34525  fibp1  34558  ballotlem1  34644  subfacp1lem6  35379  subfaclim  35382  subfacval3  35383  snmlff  35523  bcprod  35932  faclim2  35942  nn0prpwlem  36516  knoppndvlem18  36729  opnmbllem0  37853  nnubfi  37947  nninfnub  37948  geomcau  37956  heiborlem5  38012  heiborlem6  38013  heiborlem7  38014  heiborlem8  38015  bfplem1  38019  lcmineqlem12  42290  aks4d1p1p2  42320  primrootscoprmpow  42349  2ap1caineq  42395  dvdsexpnn  42584  dvdsexpnn0  42585  zaddcomlem  42714  fidomncyc  42786  dffltz  42873  fltnltalem  42901  irrapxlem2  43061  pellexlem1  43067  pellexlem5  43071  pellqrex  43117  monotoddzzfi  43180  jm2.17c  43200  acongeq  43221  jm2.18  43226  jm2.23  43234  jm2.26lem3  43239  jm3.1  43258  expdiophlem1  43259  idomodle  43429  proot1ex  43434  rp-isfinite6  43755  cnvtrclfv  43961  cotrclrcl  43979  inductionexd  44392  binomcxplemnotnn0  44593  nnne1ge2  45535  dvnmptconst  46181  stoweidlem3  46243  stoweidlem7  46247  stoweidlem34  46274  wallispilem4  46308  wallispilem5  46309  wallispi2lem1  46311  wallispi2lem2  46312  stirlinglem2  46315  stirlinglem3  46316  stirlinglem4  46317  stirlinglem5  46318  stirlinglem7  46320  stirlinglem11  46324  stirlinglem14  46327  stirlinglem15  46328  stirlingr  46330  fourierdlem15  46362  fourierdlem21  46368  fourierdlem22  46369  fourierdlem92  46438  fourierdlem112  46458  fouriersw  46471  sge0rpcpnf  46661  sge0ad2en  46671  ovnsubaddlem1  46810  ovnsubaddlem2  46811  ovolval5lem1  46892  ovolval5lem2  46893  nthrucw  47126  ceilhalfelfzo1  47572  modlt0b  47605  iccpartiltu  47664  iccpartigtl  47665  iccpartlt  47666  iccpartleu  47670  iccpartrn  47672  iccelpart  47675  iccpartiun  47676  iccpartdisj  47679  sqrtpwpw2p  47780  fmtnosqrt  47781  odz2prm2pw  47805  fmtnoprmfac1lem  47806  fmtnoprmfac1  47807  2pwp1prm  47831  lighneallem1  47847  lighneallem2  47848  lighneallem3  47849  lighneallem4a  47850  lighneallem4  47852  nnpw2evenALTV  47944  dfwppr  47980  gpgorder  48301  gpgedgvtx0  48303  gpgedgvtx1  48304  cznabel  48502  cznrng  48503  ztprmneprm  48589  altgsumbc  48594  altgsumbcALT  48595  pw2m1lepw2m1  48762  nneom  48769  logbpw2m1  48809  blennn  48817  blenpw2m1  48821  blengt1fldiv2p1  48835  dignn0ldlem  48844  dignnld  48845  dig2nn1st  48847  dignn0flhalflem1  48857  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  itcovalt2lem2lem1  48915  eenglngeehlnm  48981