Theorem nnnn0 11892

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 11625  ℕ₀cn0 11885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-n0 11886

This theorem is referenced by:  nnnn0i  11893  elnnnn0b  11929  elnnnn0c  11930  elz2  11987  nn0ind-raph  12070  zindd  12071  fzo1fzo0n0  13083  ubmelfzo  13097  elfzom1elp1fzo  13099  fzo0sn0fzo1  13121  quoremnn0ALT  13220  modmulnn  13252  modsumfzodifsn  13307  addmodlteq  13309  expneg  13433  expcllem  13436  expcl2lem  13437  expeq0  13455  mulexpz  13465  expmordi  13527  rpexpmord  13528  expnlbnd  13590  expmulnbnd  13592  digit2  13593  digit1  13594  facmapnn  13641  facdiv  13643  faclbnd  13646  faclbnd3  13648  faclbnd4lem3  13651  faclbnd4lem4  13652  faclbnd5  13654  faclbnd6  13655  bcval5  13674  ishashinf  13817  iswrdi  13861  pfxn0  14039  repswfsts  14134  repswlsw  14135  repswcshw  14165  relexpnnrn  14396  relexpaddg  14404  absexpz  14657  isercoll  15016  summolem3  15063  summolem2a  15064  climcndslem2  15197  climcnds  15198  harmonic  15206  arisum  15207  expcnv  15211  geo2sum  15221  geo2lim  15223  geoisum1  15227  geoisum1c  15228  0.999...  15229  mertenslem2  15233  fallfacfwd  15382  0fallfac  15383  0risefac  15384  ef0lem  15424  ege2le3  15435  efaddlem  15438  efexp  15446  rpnnen2lem2  15560  rpnnen2lem4  15562  ruclem12  15586  dvdsmodexp  15607  nn0enne  15718  nnehalf  15720  nno  15723  nn0o  15724  pwp1fsum  15732  divalg2  15746  ndvdssub  15750  gcdmultiplez  15873  gcddiv  15889  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  rpmulgcd  15896  rplpwr  15897  dvdssqlem  15900  eucalgf  15917  lcmflefac  15982  1nprm  16013  2mulprm  16027  isprm5  16041  isprm6  16048  prmdvdsexp  16049  phicl2  16095  phibndlem  16097  phiprmpw  16103  crth  16105  eulerthlem2  16109  hashgcdlem  16115  phisum  16117  pythagtriplem10  16147  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem12  16153  pythagtriplem14  16155  pclem  16165  pcexp  16186  pcid  16199  pcprod  16221  pcbc  16226  prmpwdvds  16230  infpnlem1  16236  infpnlem2  16237  prmunb  16240  prmreclem6  16247  1arith  16253  vdwapf  16298  0hashbc  16333  ram0  16348  prmdvdsprmo  16368  prmdvdsprmop  16369  prmolefac  16372  prmgaplem1  16375  prmgaplem2  16376  prmgapprmolem  16387  prmgapprmo  16388  cshwrepswhash1  16428  smndex1n0mnd  18069  ghmmulg  18362  odmodnn0  18660  dfod2  18683  submod  18686  prmirredlem  20186  prmirred  20188  znf1o  20243  znhash  20250  znfi  20251  znfld  20252  znidomb  20253  znunithash  20256  znrrg  20257  cply1mul  20923  cply1coe0  20928  cply1coe0bi  20929  cpmatmcllem  21323  m2cpm  21346  m2cpminvid2lem  21359  fvmptnn04ifa  21455  chfacfisf  21459  chfacfisfcpmat  21460  chfacffsupp  21461  chfacfscmul0  21463  chfacfscmulfsupp  21464  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulfsupp  21468  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmadugsumlemF  21481  tgpmulg  22698  cmodscexp  23726  cphipval  23847  ovollb2lem  24092  ovoliunlem1  24106  ovoliunlem3  24108  uniioombllem3  24189  uniioombllem4  24190  opnmbllem  24205  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  dvexp  24556  dvexp3  24581  plyco  24838  dgrcolem1  24870  plydivex  24893  aaliou3lem2  24939  aaliou3lem3  24940  aaliou3lem5  24943  aaliou3lem6  24944  aaliou3lem7  24945  aaliou3lem9  24946  radcnvlem2  25009  dvradcnv  25016  pserdv2  25025  abelthlem6  25031  abelthlem9  25035  logtayllem  25250  logtayl  25251  logtaylsum  25252  logtayl2  25253  cxproot  25281  root1id  25343  logbgcd1irr  25380  atantayl  25523  atantayl2  25524  leibpilem2  25527  leibpi  25528  birthdaylem2  25538  birthdaylem3  25539  dfef2  25556  basellem2  25667  basellem4  25669  basellem5  25670  basellem6  25671  basellem8  25673  isppw2  25700  vmappw  25701  sqf11  25724  vma1  25751  1sgm2ppw  25784  chtublem  25795  fsumvma2  25798  vmasum  25800  dchrelbas4  25827  dchrzrhcl  25829  dchrfi  25839  dchrhash  25855  pcbcctr  25860  bclbnd  25864  bposlem1  25868  lgsval4a  25903  lgsdchrval  25938  lgsdchr  25939  gausslemma2dlem0c  25942  gausslemma2dlem0d  25943  gausslemma2dlem6  25956  2lgslem1a1  25973  2lgslem1c  25977  2lgslem3a1  25984  2lgslem3b1  25985  2lgslem3c1  25986  2lgslem3d1  25987  2sqreunnlem1  26033  2sqreunnltblem  26035  rplogsumlem2  26069  dchrisumlem2  26074  ostth2lem1  26202  ostth2lem3  26219  ostth3  26222  cusgrsize2inds  27243  pthdivtx  27518  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem7  27602  0enwwlksnge1  27650  rusgr0edg  27759  clwlkclwwlkf1lem2  27790  clwlkclwwlkf1lem3  27791  clwwisshclwwslem  27799  clwwlkinwwlk  27825  clwwlkel  27831  clwwlkf  27832  clwwlkf1  27834  clwwlknwwlksnb  27840  wwlksubclwwlk  27843  erclwwlknref  27854  clwwlknonwwlknonb  27891  numclwwlkqhash  28160  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  ipval2  28490  ipasslem3  28616  ipasslem4  28617  nn0min  30562  frobrhm  30910  esumcst  31432  eulerpartlemb  31736  fibp1  31769  ballotlem1  31854  subfacp1lem6  32545  subfaclim  32548  subfacval3  32549  snmlff  32689  bcprod  33083  faclim2  33093  dvdspw  33095  nn0prpwlem  33783  knoppndvlem18  33981  opnmbllem0  35093  nnubfi  35188  nninfnub  35189  geomcau  35197  heiborlem5  35253  heiborlem6  35254  heiborlem7  35255  heiborlem8  35256  bfplem1  35260  lcmineqlem12  39328  2ap1caineq  39349  nn0expgcd  39492  dffltz  39615  fltnltalem  39618  irrapxlem2  39764  pellexlem1  39770  pellexlem5  39774  pellqrex  39820  monotoddzzfi  39883  jm2.17c  39903  acongeq  39924  jm2.18  39929  jm2.23  39937  jm2.26lem3  39942  jm3.1  39961  expdiophlem1  39962  idomrootle  40139  idomodle  40140  proot1ex  40145  rp-isfinite6  40226  cnvtrclfv  40425  cotrclrcl  40443  inductionexd  40858  binomcxplemnotnn0  41060  nnne1ge2  41923  dvnmptconst  42583  stoweidlem3  42645  stoweidlem7  42649  stoweidlem34  42676  wallispilem4  42710  wallispilem5  42711  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem2  42717  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem7  42722  stirlinglem11  42726  stirlinglem14  42729  stirlinglem15  42730  stirlingr  42732  fourierdlem15  42764  fourierdlem21  42770  fourierdlem22  42771  fourierdlem92  42840  fourierdlem112  42860  fouriersw  42873  sge0rpcpnf  43060  sge0ad2en  43070  ovnsubaddlem1  43209  ovnsubaddlem2  43210  ovolval5lem1  43291  ovolval5lem2  43292  iccpartiltu  43939  iccpartigtl  43940  iccpartlt  43941  iccpartleu  43945  iccpartrn  43947  iccelpart  43950  iccpartiun  43951  iccpartdisj  43954  sqrtpwpw2p  44055  fmtnosqrt  44056  odz2prm2pw  44080  fmtnoprmfac1lem  44081  fmtnoprmfac1  44082  2pwp1prm  44106  lighneallem1  44123  lighneallem2  44124  lighneallem3  44125  lighneallem4a  44126  lighneallem4  44128  nnpw2evenALTV  44220  dfwppr  44256  cznabel  44578  cznrng  44579  ztprmneprm  44749  altgsumbc  44754  altgsumbcALT  44755  pw2m1lepw2m1  44929  nneom  44941  logbpw2m1  44981  blennn  44989  blenpw2m1  44993  blengt1fldiv2p1  45007  dignn0ldlem  45016  dignnld  45017  dig2nn1st  45019  dignn0flhalflem1  45029  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  itcovalt2lem2lem1  45087  eenglngeehlnm  45153