Theorem nnnn0 12560

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-n0 12554

This theorem is referenced by:  nnnn0i  12561  elnnnn0b  12597  elnnnn0c  12598  elz2  12657  nn0ind-raph  12743  zindd  12744  fzo1fzo0n0  13767  ubmelfzo  13781  elfzom1elp1fzo  13783  fzo0sn0fzo1  13805  quoremnn0ALT  13908  modmulnn  13940  modsumfzodifsn  13995  addmodlteq  13997  expneg  14120  expcllem  14123  expcl2lem  14124  expeq0  14143  mulexpz  14153  expmordi  14217  rpexpmord  14218  expnlbnd  14282  expmulnbnd  14284  digit2  14285  digit1  14286  facmapnn  14334  facdiv  14336  faclbnd  14339  faclbnd3  14341  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd5  14347  faclbnd6  14348  bcval5  14367  ishashinf  14512  iswrdi  14566  pfxn0  14734  repswfsts  14829  repswlsw  14830  repswcshw  14860  relexpnnrn  15094  relexpaddg  15102  absexpz  15354  isercoll  15716  summolem3  15762  summolem2a  15763  climcndslem2  15898  climcnds  15899  harmonic  15907  arisum  15908  expcnv  15912  geo2sum  15921  geo2lim  15923  geoisum1  15927  geoisum1c  15928  0.999...  15929  mertenslem2  15933  fallfacfwd  16084  0fallfac  16085  0risefac  16086  ef0lem  16126  ege2le3  16138  efaddlem  16141  efexp  16149  rpnnen2lem2  16263  rpnnen2lem4  16265  ruclem12  16289  dvdsmodexp  16310  dvdsexp2im  16375  nn0enne  16425  nnehalf  16427  nno  16430  nn0o  16431  pwp1fsum  16439  divalg2  16453  ndvdssub  16457  gcdmultiplez  16582  gcddiv  16598  rpmulgcd  16604  rplpwr  16605  nn0expgcd  16611  dvdssqlem  16613  eucalgf  16630  lcmflefac  16695  1nprm  16726  2mulprm  16740  isprm5  16754  isprm6  16761  prmdvdsexp  16762  phicl2  16815  phibndlem  16817  phiprmpw  16823  crth  16825  eulerthlem2  16829  hashgcdlem  16835  phisum  16837  pythagtriplem10  16867  pythagtriplem6  16868  pythagtriplem7  16869  pythagtriplem12  16873  pythagtriplem14  16875  pclem  16885  pcexp  16906  pcid  16920  pcprod  16942  pcbc  16947  prmpwdvds  16951  infpnlem1  16957  infpnlem2  16958  prmunb  16961  prmreclem6  16968  1arith  16974  vdwapf  17019  0hashbc  17054  ram0  17069  prmdvdsprmo  17089  prmdvdsprmop  17090  prmolefac  17093  prmgaplem1  17096  prmgaplem2  17097  prmgapprmolem  17108  prmgapprmo  17109  cshwrepswhash1  17150  smndex1n0mnd  18947  ghmmulg  19268  odmodnn0  19582  dfod2  19606  submod  19611  prmirredlem  21506  prmirred  21508  znf1o  21593  znhash  21600  znfi  21601  znfld  21602  znidomb  21603  znunithash  21606  znrrg  21607  frobrhm  21617  cply1mul  22321  cply1coe0  22326  cply1coe0bi  22327  ply1fermltlchr  22337  cpmatmcllem  22745  m2cpm  22768  m2cpminvid2lem  22781  fvmptnn04ifa  22877  chfacfisf  22881  chfacfisfcpmat  22882  chfacffsupp  22883  chfacfscmul0  22885  chfacfscmulfsupp  22886  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulfsupp  22890  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmadugsumlemF  22903  tgpmulg  24122  cmodscexp  25173  cphipval  25296  ovollb2lem  25542  ovoliunlem1  25556  ovoliunlem3  25558  uniioombllem3  25639  uniioombllem4  25640  opnmbllem  25655  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  dvexp  26011  dvexp3  26036  idomrootle  26232  plyco  26300  dgrcolem1  26333  plydivex  26357  aaliou3lem2  26403  aaliou3lem3  26404  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  aaliou3lem9  26410  radcnvlem2  26475  dvradcnv  26482  pserdv2  26492  abelthlem6  26498  abelthlem9  26502  logtayllem  26719  logtayl  26720  logtaylsum  26721  logtayl2  26722  cxproot  26750  root1id  26815  logbgcd1irr  26855  atantayl  26998  atantayl2  26999  leibpilem2  27002  leibpi  27003  birthdaylem2  27013  birthdaylem3  27014  dfef2  27032  basellem2  27143  basellem4  27145  basellem5  27146  basellem6  27147  basellem8  27149  isppw2  27176  vmappw  27177  sqf11  27200  vma1  27227  1sgm2ppw  27262  chtublem  27273  fsumvma2  27276  vmasum  27278  dchrelbas4  27305  dchrzrhcl  27307  dchrfi  27317  dchrhash  27333  pcbcctr  27338  bclbnd  27342  bposlem1  27346  lgsval4a  27381  lgsdchrval  27416  lgsdchr  27417  gausslemma2dlem0c  27420  gausslemma2dlem0d  27421  gausslemma2dlem6  27434  2lgslem1a1  27451  2lgslem1c  27455  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2sqreunnlem1  27511  2sqreunnltblem  27513  rplogsumlem2  27547  dchrisumlem2  27552  ostth2lem1  27680  ostth2lem3  27697  ostth3  27700  cusgrsize2inds  29489  pthdivtx  29765  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem7  29849  0enwwlksnge1  29897  rusgr0edg  30006  clwlkclwwlkf1lem2  30037  clwlkclwwlkf1lem3  30038  clwwisshclwwslem  30046  clwwlkinwwlk  30072  clwwlkel  30078  clwwlkf  30079  clwwlkf1  30081  clwwlknwwlksnb  30087  wwlksubclwwlk  30090  erclwwlknref  30101  clwwlknonwwlknonb  30138  numclwwlkqhash  30407  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  ipval2  30739  ipasslem3  30865  ipasslem4  30866  nn0min  32824  znfermltl  33359  ply1fermltl  33574  esumcst  34027  eulerpartlemb  34333  fibp1  34366  ballotlem1  34451  subfacp1lem6  35153  subfaclim  35156  subfacval3  35157  snmlff  35297  bcprod  35700  faclim2  35710  nn0prpwlem  36288  knoppndvlem18  36495  opnmbllem0  37616  nnubfi  37710  nninfnub  37711  geomcau  37719  heiborlem5  37775  heiborlem6  37776  heiborlem7  37777  heiborlem8  37778  bfplem1  37782  lcmineqlem12  41997  aks4d1p1p2  42027  primrootscoprmpow  42056  2ap1caineq  42102  dvdsexpnn  42320  dvdsexpnn0  42321  zaddcomlem  42427  fidomncyc  42490  dffltz  42589  fltnltalem  42617  irrapxlem2  42779  pellexlem1  42785  pellexlem5  42789  pellqrex  42835  monotoddzzfi  42899  jm2.17c  42919  acongeq  42940  jm2.18  42945  jm2.23  42953  jm2.26lem3  42958  jm3.1  42977  expdiophlem1  42978  idomodle  43152  proot1ex  43157  rp-isfinite6  43480  cnvtrclfv  43686  cotrclrcl  43704  inductionexd  44117  binomcxplemnotnn0  44325  nnne1ge2  45206  dvnmptconst  45862  stoweidlem3  45924  stoweidlem7  45928  stoweidlem34  45955  wallispilem4  45989  wallispilem5  45990  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem2  45996  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem11  46005  stirlinglem14  46008  stirlinglem15  46009  stirlingr  46011  fourierdlem15  46043  fourierdlem21  46049  fourierdlem22  46050  fourierdlem92  46119  fourierdlem112  46139  fouriersw  46152  sge0rpcpnf  46342  sge0ad2en  46352  ovnsubaddlem1  46491  ovnsubaddlem2  46492  ovolval5lem1  46573  ovolval5lem2  46574  iccpartiltu  47296  iccpartigtl  47297  iccpartlt  47298  iccpartleu  47302  iccpartrn  47304  iccelpart  47307  iccpartiun  47308  iccpartdisj  47311  sqrtpwpw2p  47412  fmtnosqrt  47413  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  2pwp1prm  47463  lighneallem1  47479  lighneallem2  47480  lighneallem3  47481  lighneallem4a  47482  lighneallem4  47484  nnpw2evenALTV  47576  dfwppr  47612  cznabel  47983  cznrng  47984  ztprmneprm  48072  altgsumbc  48077  altgsumbcALT  48078  pw2m1lepw2m1  48249  nneom  48261  logbpw2m1  48301  blennn  48309  blenpw2m1  48313  blengt1fldiv2p1  48327  dignn0ldlem  48336  dignnld  48337  dig2nn1st  48339  dignn0flhalflem1  48349  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  itcovalt2lem2lem1  48407  eenglngeehlnm  48473