Theorem nnnn0 9384

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9118  ℕ₀cn0 9377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9378

This theorem is referenced by:  nnnn0i  9385  elnnnn0b  9421  elnnnn0c  9422  elnn0z  9467  elz2  9526  nn0ind-raph  9572  zindd  9573  fzo1fzo0n0  10391  ubmelfzo  10414  elfzom1elp1fzo  10416  fzo0sn0fzo1  10435  modqmulnn  10572  expnegap0  10777  expcllem  10780  expcl2lemap  10781  expap0  10799  expeq0  10800  mulexpzap  10809  expnlbnd  10894  apexp1  10948  facdiv  10968  faclbnd  10971  faclbnd3  10973  faclbnd6  10974  pfxn0  11228  resqrexlemlo  11532  absexpzap  11599  nnf1o  11895  summodclem2a  11900  fsum3  11906  arisum  12017  expcnvap0  12021  expcnv  12023  geo2sum  12033  geo2lim  12035  geoisum1c  12039  0.999...  12040  mertenslem2  12055  fprodseq  12102  fprodfac  12134  ef0lem  12179  ege2le3  12190  efaddlem  12193  efexp  12201  dvdsmodexp  12314  nn0enne  12421  nnehalf  12423  nno  12425  nn0o  12426  divalg2  12445  ndvdssub  12449  gcddiv  12548  gcdmultiple  12549  gcdmultiplez  12550  rpmulgcd  12555  rplpwr  12556  dvdssqlem  12559  eucalgf  12585  1nprm  12644  isprm6  12677  prmdvdsexp  12678  pw2dvds  12696  oddpwdc  12704  phicl2  12744  phibndlem  12746  phiprmpw  12752  crth  12754  hashgcdlem  12768  phisum  12771  pythagtriplem10  12800  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem12  12806  pythagtriplem14  12808  pclemub  12818  pcexp  12840  pcid  12855  pcprod  12877  pcbc  12882  prmpwdvds  12886  infpnlem1  12890  infpnlem2  12891  prmunb  12893  1arith  12898  ennnfonelemjn  12981  ghmmulg  13801  znf1o  14623  znfi  14627  znhash  14628  znidom  14629  znidomb  14630  znrrg  14632  dvexp  15393  plycolemc  15440  logbgcd1irr  15649  1sgm2ppw  15677  lgsval4a  15709  gausslemma2dlem0c  15738  gausslemma2dlem0d  15739  gausslemma2dlem6  15754  2lgslem1a1  15773  2lgslem1c  15777  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787