Theorem nnnn0 9502

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℕcn 9236  ℕ₀cn0 9495

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-n0 9496

This theorem is referenced by:  nnnn0i  9503  elnnnn0b  9539  elnnnn0c  9540  elnn0z  9589  elz2  9648  nn0ind-raph  9694  zindd  9695  fzo1fzo0n0  10521  ubmelfzo  10544  elfzom1elp1fzo  10546  fzo0sn0fzo1  10565  modqmulnn  10703  expnegap0  10908  expcllem  10911  expcl2lemap  10912  expap0  10930  expeq0  10931  mulexpzap  10940  expnlbnd  11025  apexp1  11079  facdiv  11099  faclbnd  11102  faclbnd3  11104  faclbnd6  11105  pfxn0  11376  resqrexlemlo  11694  absexpzap  11761  nnf1o  12058  summodclem2a  12063  fsum3  12069  arisum  12180  expcnvap0  12184  expcnv  12186  geo2sum  12196  geo2lim  12198  geoisum1c  12202  0.999...  12203  mertenslem2  12218  fprodseq  12265  fprodfac  12297  ef0lem  12342  ege2le3  12353  efaddlem  12356  efexp  12364  dvdsmodexp  12477  nn0enne  12584  nnehalf  12586  nno  12588  nn0o  12589  divalg2  12608  ndvdssub  12612  gcddiv  12711  gcdmultiple  12712  gcdmultiplez  12713  rpmulgcd  12718  rplpwr  12719  dvdssqlem  12722  eucalgf  12748  1nprm  12807  isprm6  12840  prmdvdsexp  12841  pw2dvds  12859  oddpwdc  12867  phicl2  12907  phibndlem  12909  phiprmpw  12915  crth  12917  hashgcdlem  12931  phisum  12934  pythagtriplem10  12963  pythagtriplem6  12964  pythagtriplem7  12965  pythagtriplem12  12969  pythagtriplem14  12971  pclemub  12981  pcexp  13003  pcid  13018  pcprod  13040  pcbc  13045  prmpwdvds  13049  infpnlem1  13053  infpnlem2  13054  prmunb  13056  1arith  13061  ennnfonelemjn  13145  ghmmulg  13965  znf1o  14791  znfi  14795  znhash  14796  znidom  14797  znidomb  14798  znrrg  14800  dvexp  15568  plycolemc  15615  logbgcd1irr  15824  pellexlem1  15837  1sgm2ppw  15855  lgsval4a  15887  gausslemma2dlem0c  15916  gausslemma2dlem0d  15917  gausslemma2dlem6  15932  2lgslem1a1  15951  2lgslem1c  15955  2lgslem3a1  15962  2lgslem3b1  15963  2lgslem3c1  15964  2lgslem3d1  15965  isclwwlknx  16403