Theorem nnnn0 9214

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℕcn 8950  ℕ₀cn0 9207

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-n0 9208

This theorem is referenced by:  nnnn0i  9215  elnnnn0b  9251  elnnnn0c  9252  elnn0z  9297  elz2  9355  nn0ind-raph  9401  zindd  9402  fzo1fzo0n0  10215  ubmelfzo  10232  elfzom1elp1fzo  10234  fzo0sn0fzo1  10253  modqmulnn  10375  expnegap0  10562  expcllem  10565  expcl2lemap  10566  expap0  10584  expeq0  10585  mulexpzap  10594  expnlbnd  10679  apexp1  10733  facdiv  10753  faclbnd  10756  faclbnd3  10758  faclbnd6  10759  resqrexlemlo  11057  absexpzap  11124  nnf1o  11419  summodclem2a  11424  fsum3  11430  arisum  11541  expcnvap0  11545  expcnv  11547  geo2sum  11557  geo2lim  11559  geoisum1c  11563  0.999...  11564  mertenslem2  11579  fprodseq  11626  fprodfac  11658  ef0lem  11703  ege2le3  11714  efaddlem  11717  efexp  11725  dvdsmodexp  11837  nn0enne  11942  nnehalf  11944  nno  11946  nn0o  11947  divalg2  11966  ndvdssub  11970  gcddiv  12055  gcdmultiple  12056  gcdmultiplez  12057  rpmulgcd  12062  rplpwr  12063  dvdssqlem  12066  eucalgf  12090  1nprm  12149  isprm6  12182  prmdvdsexp  12183  pw2dvds  12201  oddpwdc  12209  phicl2  12249  phibndlem  12251  phiprmpw  12257  crth  12259  hashgcdlem  12273  phisum  12275  pythagtriplem10  12304  pythagtriplem6  12305  pythagtriplem7  12306  pythagtriplem12  12310  pythagtriplem14  12312  pclemub  12322  pcexp  12344  pcid  12359  pcprod  12381  pcbc  12386  prmpwdvds  12390  infpnlem1  12394  infpnlem2  12395  prmunb  12397  1arith  12402  ennnfonelemjn  12456  ghmmulg  13212  dvexp  14652  logbgcd1irr  14862  lgsval4a  14901