Theorem nnnn0 12475

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℕcn 12208  ℕ₀cn0 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945  df-in 3947  df-ss 3957  df-n0 12469

This theorem is referenced by:  nnnn0i  12476  elnnnn0b  12512  elnnnn0c  12513  elz2  12572  nn0ind-raph  12658  zindd  12659  fzo1fzo0n0  13679  ubmelfzo  13693  elfzom1elp1fzo  13695  fzo0sn0fzo1  13717  quoremnn0ALT  13818  modmulnn  13850  modsumfzodifsn  13905  addmodlteq  13907  expneg  14031  expcllem  14034  expcl2lem  14035  expeq0  14054  mulexpz  14064  expmordi  14128  rpexpmord  14129  expnlbnd  14192  expmulnbnd  14194  digit2  14195  digit1  14196  facmapnn  14241  facdiv  14243  faclbnd  14246  faclbnd3  14248  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd5  14254  faclbnd6  14255  bcval5  14274  ishashinf  14420  iswrdi  14464  pfxn0  14632  repswfsts  14727  repswlsw  14728  repswcshw  14758  relexpnnrn  14988  relexpaddg  14996  absexpz  15248  isercoll  15610  summolem3  15656  summolem2a  15657  climcndslem2  15792  climcnds  15793  harmonic  15801  arisum  15802  expcnv  15806  geo2sum  15815  geo2lim  15817  geoisum1  15821  geoisum1c  15822  0.999...  15823  mertenslem2  15827  fallfacfwd  15976  0fallfac  15977  0risefac  15978  ef0lem  16018  ege2le3  16029  efaddlem  16032  efexp  16040  rpnnen2lem2  16154  rpnnen2lem4  16156  ruclem12  16180  dvdsmodexp  16201  dvdsexp2im  16266  nn0enne  16316  nnehalf  16318  nno  16321  nn0o  16322  pwp1fsum  16330  divalg2  16344  ndvdssub  16348  gcdmultiplez  16473  gcddiv  16489  rpmulgcd  16494  rplpwr  16495  dvdssqlem  16499  eucalgf  16516  lcmflefac  16581  1nprm  16612  2mulprm  16626  isprm5  16640  isprm6  16647  prmdvdsexp  16648  phicl2  16697  phibndlem  16699  phiprmpw  16705  crth  16707  eulerthlem2  16711  hashgcdlem  16717  phisum  16719  pythagtriplem10  16749  pythagtriplem6  16750  pythagtriplem7  16751  pythagtriplem12  16755  pythagtriplem14  16757  pclem  16767  pcexp  16788  pcid  16802  pcprod  16824  pcbc  16829  prmpwdvds  16833  infpnlem1  16839  infpnlem2  16840  prmunb  16843  prmreclem6  16850  1arith  16856  vdwapf  16901  0hashbc  16936  ram0  16951  prmdvdsprmo  16971  prmdvdsprmop  16972  prmolefac  16975  prmgaplem1  16978  prmgaplem2  16979  prmgapprmolem  16990  prmgapprmo  16991  cshwrepswhash1  17032  smndex1n0mnd  18824  ghmmulg  19138  odmodnn0  19445  dfod2  19469  submod  19474  prmirredlem  21322  prmirred  21324  znf1o  21407  znhash  21414  znfi  21415  znfld  21416  znidomb  21417  znunithash  21420  znrrg  21421  cply1mul  22128  cply1coe0  22133  cply1coe0bi  22134  cpmatmcllem  22530  m2cpm  22553  m2cpminvid2lem  22566  fvmptnn04ifa  22662  chfacfisf  22666  chfacfisfcpmat  22667  chfacffsupp  22668  chfacfscmul0  22670  chfacfscmulfsupp  22671  chfacfscmulgsum  22672  chfacfpmmul0  22674  chfacfpmmulfsupp  22675  chfacfpmmulgsum  22676  chfacfpmmulgsum2  22677  cayhamlem1  22678  cpmadugsumlemF  22688  tgpmulg  23907  cmodscexp  24958  cphipval  25081  ovollb2lem  25327  ovoliunlem1  25341  ovoliunlem3  25343  uniioombllem3  25424  uniioombllem4  25425  opnmbllem  25440  mbfi1fseqlem1  25555  mbfi1fseqlem3  25557  mbfi1fseqlem4  25558  mbfi1fseqlem5  25559  mbfi1fseqlem6  25560  dvexp  25795  dvexp3  25820  plyco  26083  dgrcolem1  26116  plydivex  26139  aaliou3lem2  26185  aaliou3lem3  26186  aaliou3lem5  26189  aaliou3lem6  26190  aaliou3lem7  26191  aaliou3lem9  26192  radcnvlem2  26255  dvradcnv  26262  pserdv2  26272  abelthlem6  26278  abelthlem9  26282  logtayllem  26497  logtayl  26498  logtaylsum  26499  logtayl2  26500  cxproot  26528  root1id  26593  logbgcd1irr  26630  atantayl  26773  atantayl2  26774  leibpilem2  26777  leibpi  26778  birthdaylem2  26788  birthdaylem3  26789  dfef2  26807  basellem2  26918  basellem4  26920  basellem5  26921  basellem6  26922  basellem8  26924  isppw2  26951  vmappw  26952  sqf11  26975  vma1  27002  1sgm2ppw  27037  chtublem  27048  fsumvma2  27051  vmasum  27053  dchrelbas4  27080  dchrzrhcl  27082  dchrfi  27092  dchrhash  27108  pcbcctr  27113  bclbnd  27117  bposlem1  27121  lgsval4a  27156  lgsdchrval  27191  lgsdchr  27192  gausslemma2dlem0c  27195  gausslemma2dlem0d  27196  gausslemma2dlem6  27209  2lgslem1a1  27226  2lgslem1c  27230  2lgslem3a1  27237  2lgslem3b1  27238  2lgslem3c1  27239  2lgslem3d1  27240  2sqreunnlem1  27286  2sqreunnltblem  27288  rplogsumlem2  27322  dchrisumlem2  27327  ostth2lem1  27455  ostth2lem3  27472  ostth3  27475  cusgrsize2inds  29134  pthdivtx  29410  crctcshwlkn0lem4  29491  crctcshwlkn0lem5  29492  crctcshwlkn0lem7  29494  0enwwlksnge1  29542  rusgr0edg  29651  clwlkclwwlkf1lem2  29682  clwlkclwwlkf1lem3  29683  clwwisshclwwslem  29691  clwwlkinwwlk  29717  clwwlkel  29723  clwwlkf  29724  clwwlkf1  29726  clwwlknwwlksnb  29732  wwlksubclwwlk  29735  erclwwlknref  29746  clwwlknonwwlknonb  29783  numclwwlkqhash  30052  numclwwlk2lem1  30053  numclwlk2lem2f  30054  numclwlk2lem2f1o  30056  ipval2  30384  ipasslem3  30510  ipasslem4  30511  nn0min  32450  frobrhm  32809  znfermltl  32910  ply1fermltlchr  33093  ply1fermltl  33094  esumcst  33516  eulerpartlemb  33822  fibp1  33855  ballotlem1  33940  subfacp1lem6  34631  subfaclim  34634  subfacval3  34635  snmlff  34775  bcprod  35169  faclim2  35179  nn0prpwlem  35663  knoppndvlem18  35861  opnmbllem0  36980  nnubfi  37074  nninfnub  37075  geomcau  37083  heiborlem5  37139  heiborlem6  37140  heiborlem7  37141  heiborlem8  37142  bfplem1  37146  lcmineqlem12  41364  aks4d1p1p2  41394  2ap1caineq  41420  nn0expgcd  41681  dvdsexpnn  41686  dvdsexpnn0  41687  zaddcomlem  41779  dffltz  41831  fltnltalem  41859  irrapxlem2  42016  pellexlem1  42022  pellexlem5  42026  pellqrex  42072  monotoddzzfi  42136  jm2.17c  42156  acongeq  42177  jm2.18  42182  jm2.23  42190  jm2.26lem3  42195  jm3.1  42214  expdiophlem1  42215  idomrootle  42392  idomodle  42393  proot1ex  42398  rp-isfinite6  42724  cnvtrclfv  42930  cotrclrcl  42948  inductionexd  43361  binomcxplemnotnn0  43570  nnne1ge2  44452  dvnmptconst  45108  stoweidlem3  45170  stoweidlem7  45174  stoweidlem34  45201  wallispilem4  45235  wallispilem5  45236  wallispi2lem1  45238  wallispi2lem2  45239  stirlinglem2  45242  stirlinglem3  45243  stirlinglem4  45244  stirlinglem5  45245  stirlinglem7  45247  stirlinglem11  45251  stirlinglem14  45254  stirlinglem15  45255  stirlingr  45257  fourierdlem15  45289  fourierdlem21  45295  fourierdlem22  45296  fourierdlem92  45365  fourierdlem112  45385  fouriersw  45398  sge0rpcpnf  45588  sge0ad2en  45598  ovnsubaddlem1  45737  ovnsubaddlem2  45738  ovolval5lem1  45819  ovolval5lem2  45820  iccpartiltu  46541  iccpartigtl  46542  iccpartlt  46543  iccpartleu  46547  iccpartrn  46549  iccelpart  46552  iccpartiun  46553  iccpartdisj  46556  sqrtpwpw2p  46657  fmtnosqrt  46658  odz2prm2pw  46682  fmtnoprmfac1lem  46683  fmtnoprmfac1  46684  2pwp1prm  46708  lighneallem1  46724  lighneallem2  46725  lighneallem3  46726  lighneallem4a  46727  lighneallem4  46729  nnpw2evenALTV  46821  dfwppr  46857  cznabel  47089  cznrng  47090  ztprmneprm  47178  altgsumbc  47183  altgsumbcALT  47184  pw2m1lepw2m1  47355  nneom  47367  logbpw2m1  47407  blennn  47415  blenpw2m1  47419  blengt1fldiv2p1  47433  dignn0ldlem  47442  dignnld  47443  dig2nn1st  47445  dignn0flhalflem1  47455  nn0sumshdiglemA  47459  nn0sumshdiglemB  47460  itcovalt2lem2lem1  47513  eenglngeehlnm  47579