Theorem nnnn0 12449

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12186  ℕ₀cn0 12442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-n0 12443

This theorem is referenced by:  nnnn0i  12450  elnnnn0b  12486  elnnnn0c  12487  elz2  12547  nn0ind-raph  12634  zindd  12635  fzo1fzo0n0  13676  ubmelfzo  13691  elfzom1elp1fzo  13693  fzo0sn0fzo1  13716  quoremnn0ALT  13819  modmulnn  13851  modsumfzodifsn  13909  addmodlteq  13911  expneg  14034  expcllem  14037  expcl2lem  14038  expeq0  14057  mulexpz  14067  expmordi  14132  rpexpmord  14133  expnlbnd  14198  expmulnbnd  14200  digit2  14201  digit1  14202  facmapnn  14250  facdiv  14252  faclbnd  14255  faclbnd3  14257  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd5  14263  faclbnd6  14264  bcval5  14283  ishashinf  14428  iswrdi  14482  pfxn0  14651  repswfsts  14746  repswlsw  14747  repswcshw  14777  relexpnnrn  15011  relexpaddg  15019  absexpz  15271  isercoll  15634  summolem3  15680  summolem2a  15681  climcndslem2  15816  climcnds  15817  harmonic  15825  arisum  15826  expcnv  15830  geo2sum  15839  geo2lim  15841  geoisum1  15845  geoisum1c  15846  0.999...  15847  mertenslem2  15851  fallfacfwd  16002  0fallfac  16003  0risefac  16004  ef0lem  16044  ege2le3  16056  efaddlem  16059  efexp  16069  rpnnen2lem2  16183  rpnnen2lem4  16185  ruclem12  16209  dvdsmodexp  16230  dvdsexp2im  16297  nn0enne  16347  nnehalf  16349  nno  16352  nn0o  16353  pwp1fsum  16361  divalg2  16375  ndvdssub  16379  gcdmultiplez  16505  gcddiv  16521  rpmulgcd  16527  rplpwr  16528  nn0expgcd  16534  dvdssqlem  16536  eucalgf  16553  lcmflefac  16618  1nprm  16649  2mulprm  16663  isprm5  16677  isprm6  16684  prmdvdsexp  16685  phicl2  16738  phibndlem  16740  phiprmpw  16746  crth  16748  eulerthlem2  16752  hashgcdlem  16758  phisum  16761  pythagtriplem10  16791  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem12  16797  pythagtriplem14  16799  pclem  16809  pcexp  16830  pcid  16844  pcprod  16866  pcbc  16871  prmpwdvds  16875  infpnlem1  16881  infpnlem2  16882  prmunb  16885  prmreclem6  16892  1arith  16898  vdwapf  16943  0hashbc  16978  ram0  16993  prmdvdsprmo  17013  prmdvdsprmop  17014  prmolefac  17017  prmgaplem1  17020  prmgaplem2  17021  prmgapprmolem  17032  prmgapprmo  17033  cshwrepswhash1  17073  smndex1n0mnd  18839  ghmmulg  19160  odmodnn0  19470  dfod2  19494  submod  19499  prmirredlem  21382  prmirred  21384  znf1o  21461  znhash  21468  znfi  21469  znfld  21470  znidomb  21471  znunithash  21474  znrrg  21475  frobrhm  21485  cply1mul  22183  cply1coe0  22188  cply1coe0bi  22189  ply1fermltlchr  22199  cpmatmcllem  22605  m2cpm  22628  m2cpminvid2lem  22641  fvmptnn04ifa  22737  chfacfisf  22741  chfacfisfcpmat  22742  chfacffsupp  22743  chfacfscmul0  22745  chfacfscmulfsupp  22746  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulfsupp  22750  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemF  22763  tgpmulg  23980  cmodscexp  25021  cphipval  25143  ovollb2lem  25389  ovoliunlem1  25403  ovoliunlem3  25405  uniioombllem3  25486  uniioombllem4  25487  opnmbllem  25502  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  dvexp  25857  dvexp3  25882  idomrootle  26078  plyco  26146  dgrcolem1  26179  plydivex  26205  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  aaliou3lem9  26258  radcnvlem2  26323  dvradcnv  26330  pserdv2  26340  abelthlem6  26346  abelthlem9  26350  logtayllem  26568  logtayl  26569  logtaylsum  26570  logtayl2  26571  cxproot  26599  root1id  26664  logbgcd1irr  26704  atantayl  26847  atantayl2  26848  leibpilem2  26851  leibpi  26852  birthdaylem2  26862  birthdaylem3  26863  dfef2  26881  basellem2  26992  basellem4  26994  basellem5  26995  basellem6  26996  basellem8  26998  isppw2  27025  vmappw  27026  sqf11  27049  vma1  27076  1sgm2ppw  27111  chtublem  27122  fsumvma2  27125  vmasum  27127  dchrelbas4  27154  dchrzrhcl  27156  dchrfi  27166  dchrhash  27182  pcbcctr  27187  bclbnd  27191  bposlem1  27195  lgsval4a  27230  lgsdchrval  27265  lgsdchr  27266  gausslemma2dlem0c  27269  gausslemma2dlem0d  27270  gausslemma2dlem6  27283  2lgslem1a1  27300  2lgslem1c  27304  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2sqreunnlem1  27360  2sqreunnltblem  27362  rplogsumlem2  27396  dchrisumlem2  27401  ostth2lem1  27529  ostth2lem3  27546  ostth3  27549  cusgrsize2inds  29381  pthdivtx  29657  cyclnumvtx  29730  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem7  29746  0enwwlksnge1  29794  rusgr0edg  29903  clwlkclwwlkf1lem2  29934  clwlkclwwlkf1lem3  29935  clwwisshclwwslem  29943  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  clwwlknwwlksnb  29984  wwlksubclwwlk  29987  erclwwlknref  29998  clwwlknonwwlknonb  30035  numclwwlkqhash  30304  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  ipval2  30636  ipasslem3  30762  ipasslem4  30763  nn0min  32745  znfermltl  33337  ply1fermltl  33553  esumcst  34053  eulerpartlemb  34359  fibp1  34392  ballotlem1  34478  subfacp1lem6  35172  subfaclim  35175  subfacval3  35176  snmlff  35316  bcprod  35725  faclim2  35735  nn0prpwlem  36310  knoppndvlem18  36517  opnmbllem0  37650  nnubfi  37744  nninfnub  37745  geomcau  37753  heiborlem5  37809  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  bfplem1  37816  lcmineqlem12  42028  aks4d1p1p2  42058  primrootscoprmpow  42087  2ap1caineq  42133  dvdsexpnn  42321  dvdsexpnn0  42322  zaddcomlem  42451  fidomncyc  42523  dffltz  42622  fltnltalem  42650  irrapxlem2  42811  pellexlem1  42817  pellexlem5  42821  pellqrex  42867  monotoddzzfi  42931  jm2.17c  42951  acongeq  42972  jm2.18  42977  jm2.23  42985  jm2.26lem3  42990  jm3.1  43009  expdiophlem1  43010  idomodle  43180  proot1ex  43185  rp-isfinite6  43507  cnvtrclfv  43713  cotrclrcl  43731  inductionexd  44144  binomcxplemnotnn0  44345  nnne1ge2  45289  dvnmptconst  45939  stoweidlem3  46001  stoweidlem7  46005  stoweidlem34  46032  wallispilem4  46066  wallispilem5  46067  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem2  46073  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem7  46078  stirlinglem11  46082  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  fourierdlem15  46120  fourierdlem21  46126  fourierdlem22  46127  fourierdlem92  46196  fourierdlem112  46216  fouriersw  46229  sge0rpcpnf  46419  sge0ad2en  46429  ovnsubaddlem1  46568  ovnsubaddlem2  46569  ovolval5lem1  46650  ovolval5lem2  46651  ceilhalfelfzo1  47331  modlt0b  47364  iccpartiltu  47423  iccpartigtl  47424  iccpartlt  47425  iccpartleu  47429  iccpartrn  47431  iccelpart  47434  iccpartiun  47435  iccpartdisj  47438  sqrtpwpw2p  47539  fmtnosqrt  47540  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  2pwp1prm  47590  lighneallem1  47606  lighneallem2  47607  lighneallem3  47608  lighneallem4a  47609  lighneallem4  47611  nnpw2evenALTV  47703  dfwppr  47739  gpgorder  48050  gpgedgvtx0  48052  gpgedgvtx1  48053  cznabel  48248  cznrng  48249  ztprmneprm  48335  altgsumbc  48340  altgsumbcALT  48341  pw2m1lepw2m1  48509  nneom  48516  logbpw2m1  48556  blennn  48564  blenpw2m1  48568  blengt1fldiv2p1  48582  dignn0ldlem  48591  dignnld  48592  dig2nn1st  48594  dignn0flhalflem1  48604  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itcovalt2lem2lem1  48662  eenglngeehlnm  48728