Theorem nnnn0 11905

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 11638  ℕ₀cn0 11898

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-n0 11899

This theorem is referenced by:  nnnn0i  11906  elnnnn0b  11942  elnnnn0c  11943  elz2  12000  nn0ind-raph  12083  zindd  12084  fzo1fzo0n0  13089  ubmelfzo  13103  elfzom1elp1fzo  13105  fzo0sn0fzo1  13127  quoremnn0ALT  13226  modmulnn  13258  modsumfzodifsn  13313  addmodlteq  13315  expneg  13438  expcllem  13441  expcl2lem  13442  expeq0  13460  mulexpz  13470  expmordi  13532  rpexpmord  13533  expnlbnd  13595  expmulnbnd  13597  digit2  13598  digit1  13599  facmapnn  13646  facdiv  13648  faclbnd  13651  faclbnd3  13653  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd5  13659  faclbnd6  13660  bcval5  13679  ishashinf  13822  iswrdi  13866  pfxn0  14048  repswfsts  14143  repswlsw  14144  repswcshw  14174  relexpnnrn  14404  relexpaddg  14412  absexpz  14665  isercoll  15024  summolem3  15071  summolem2a  15072  climcndslem2  15205  climcnds  15206  harmonic  15214  arisum  15215  expcnv  15219  geo2sum  15229  geo2lim  15231  geoisum1  15235  geoisum1c  15236  0.999...  15237  mertenslem2  15241  fallfacfwd  15390  0fallfac  15391  0risefac  15392  ef0lem  15432  ege2le3  15443  efaddlem  15446  efexp  15454  rpnnen2lem2  15568  rpnnen2lem4  15570  ruclem12  15594  dvdsmodexp  15615  nn0enne  15728  nnehalf  15730  nno  15733  nn0o  15734  pwp1fsum  15742  divalg2  15756  ndvdssub  15760  gcdmultiplez  15883  gcddiv  15899  gcdmultipleOLD  15900  gcdmultiplezOLD  15901  rpmulgcd  15906  rplpwr  15907  dvdssqlem  15910  eucalgf  15927  lcmflefac  15992  1nprm  16023  2mulprm  16037  isprm5  16051  isprm6  16058  prmdvdsexp  16059  phicl2  16105  phibndlem  16107  phiprmpw  16113  crth  16115  eulerthlem2  16119  hashgcdlem  16125  phisum  16127  pythagtriplem10  16157  pythagtriplem6  16158  pythagtriplem7  16159  pythagtriplem12  16163  pythagtriplem14  16165  pclem  16175  pcexp  16196  pcid  16209  pcprod  16231  pcbc  16236  prmpwdvds  16240  infpnlem1  16246  infpnlem2  16247  prmunb  16250  prmreclem6  16257  1arith  16263  vdwapf  16308  0hashbc  16343  ram0  16358  prmdvdsprmo  16378  prmdvdsprmop  16379  prmolefac  16382  prmgaplem1  16385  prmgaplem2  16386  prmgapprmolem  16397  prmgapprmo  16398  cshwrepswhash1  16436  smndex1n0mnd  18077  ghmmulg  18370  odmodnn0  18668  dfod2  18691  submod  18694  cply1mul  20462  cply1coe0  20467  cply1coe0bi  20468  prmirredlem  20640  prmirred  20642  znf1o  20698  znhash  20705  znfi  20706  znfld  20707  znidomb  20708  znunithash  20711  znrrg  20712  cpmatmcllem  21326  m2cpm  21349  m2cpminvid2lem  21362  fvmptnn04ifa  21458  chfacfisf  21462  chfacfisfcpmat  21463  chfacffsupp  21464  chfacfscmul0  21466  chfacfscmulfsupp  21467  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulfsupp  21471  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadugsumlemF  21484  tgpmulg  22701  cmodscexp  23725  cphipval  23846  ovollb2lem  24089  ovoliunlem1  24103  ovoliunlem3  24105  uniioombllem3  24186  uniioombllem4  24187  opnmbllem  24202  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  dvexp  24550  dvexp3  24575  plyco  24831  dgrcolem1  24863  plydivex  24886  aaliou3lem2  24932  aaliou3lem3  24933  aaliou3lem5  24936  aaliou3lem6  24937  aaliou3lem7  24938  aaliou3lem9  24939  radcnvlem2  25002  dvradcnv  25009  pserdv2  25018  abelthlem6  25024  abelthlem9  25028  logtayllem  25242  logtayl  25243  logtaylsum  25244  logtayl2  25245  cxproot  25273  root1id  25335  logbgcd1irr  25372  atantayl  25515  atantayl2  25516  leibpilem2  25519  leibpi  25520  birthdaylem2  25530  birthdaylem3  25531  dfef2  25548  basellem2  25659  basellem4  25661  basellem5  25662  basellem6  25663  basellem8  25665  isppw2  25692  vmappw  25693  sqf11  25716  vma1  25743  1sgm2ppw  25776  chtublem  25787  fsumvma2  25790  vmasum  25792  dchrelbas4  25819  dchrzrhcl  25821  dchrfi  25831  dchrhash  25847  pcbcctr  25852  bclbnd  25856  bposlem1  25860  lgsval4a  25895  lgsdchrval  25930  lgsdchr  25931  gausslemma2dlem0c  25934  gausslemma2dlem0d  25935  gausslemma2dlem6  25948  2lgslem1a1  25965  2lgslem1c  25969  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2sqreunnlem1  26025  2sqreunnltblem  26027  rplogsumlem2  26061  dchrisumlem2  26066  ostth2lem1  26194  ostth2lem3  26211  ostth3  26214  cusgrsize2inds  27235  pthdivtx  27510  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem7  27594  0enwwlksnge1  27642  rusgr0edg  27752  clwlkclwwlkf1lem2  27783  clwlkclwwlkf1lem3  27784  clwwisshclwwslem  27792  clwwlkinwwlk  27818  clwwlknfiOLD  27824  clwwlkel  27825  clwwlkf  27826  clwwlkf1  27828  clwwlknwwlksnb  27834  wwlksubclwwlk  27837  erclwwlknref  27848  clwwlknonwwlknonb  27885  numclwwlkqhash  28154  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  ipval2  28484  ipasslem3  28610  ipasslem4  28611  nn0min  30536  esumcst  31322  eulerpartlemb  31626  fibp1  31659  ballotlem1  31744  subfacp1lem6  32432  subfaclim  32435  subfacval3  32436  snmlff  32576  bcprod  32970  faclim2  32980  dvdspw  32982  nn0prpwlem  33670  knoppndvlem18  33868  opnmbllem0  34943  nnubfi  35040  nninfnub  35041  geomcau  35049  heiborlem5  35108  heiborlem6  35109  heiborlem7  35110  heiborlem8  35111  bfplem1  35115  nn0expgcd  39233  dffltz  39320  fltnltalem  39323  irrapxlem2  39469  pellexlem1  39475  pellexlem5  39479  pellqrex  39525  monotoddzzfi  39588  jm2.17c  39608  acongeq  39629  jm2.18  39634  jm2.23  39642  jm2.26lem3  39647  jm3.1  39666  expdiophlem1  39667  idomrootle  39844  idomodle  39845  proot1ex  39850  rp-isfinite6  39933  cnvtrclfv  40118  cotrclrcl  40136  inductionexd  40554  binomcxplemnotnn0  40737  nnne1ge2  41607  dvnmptconst  42275  stoweidlem3  42337  stoweidlem7  42341  stoweidlem34  42368  wallispilem4  42402  wallispilem5  42403  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem2  42409  stirlinglem3  42410  stirlinglem4  42411  stirlinglem5  42412  stirlinglem7  42414  stirlinglem11  42418  stirlinglem14  42421  stirlinglem15  42422  stirlingr  42424  fourierdlem15  42456  fourierdlem21  42462  fourierdlem22  42463  fourierdlem92  42532  fourierdlem112  42552  fouriersw  42565  sge0rpcpnf  42752  sge0ad2en  42762  ovnsubaddlem1  42901  ovnsubaddlem2  42902  ovolval5lem1  42983  ovolval5lem2  42984  iccpartiltu  43631  iccpartigtl  43632  iccpartlt  43633  iccpartleu  43637  iccpartrn  43639  iccelpart  43642  iccpartiun  43643  iccpartdisj  43646  sqrtpwpw2p  43749  fmtnosqrt  43750  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  2pwp1prm  43800  lighneallem1  43819  lighneallem2  43820  lighneallem3  43821  lighneallem4a  43822  lighneallem4  43824  nnpw2evenALTV  43916  dfwppr  43952  cznabel  44274  cznrng  44275  ztprmneprm  44444  altgsumbc  44449  altgsumbcALT  44450  pw2m1lepw2m1  44624  nneom  44636  logbpw2m1  44676  blennn  44684  blenpw2m1  44688  blengt1fldiv2p1  44702  dignn0ldlem  44711  dignnld  44712  dig2nn1st  44714  dignn0flhalflem1  44724  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  eenglngeehlnm  44775