Theorem nnnn0 9575

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9307  ℕ₀cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9569

This theorem is used by:  nnnn0i  9576  elnnnn0b  9612  elnnnn0c  9613  elnn0z  9662  elz2  9721  nn0ind-raph  9768  zindd  9769  fzo1fzo0n0  10606  ubmelfzo  10629  elfzom1elp1fzo  10631  fzo0sn0fzo1  10650  modqmulnn  10793  expnegap0  10998  expcllem  11001  expcl2lemap  11002  expap0  11020  expeq0  11021  mulexpzap  11030  expnlbnd  11116  apexp1  11171  facdiv  11191  faclbnd  11194  faclbnd3  11196  faclbnd6  11197  pfxn0  11475  resqrexlemlo  11794  absexpzap  11862  nnf1o  12161  summodclem2a  12166  fsum3  12172  arisum  12283  expcnvap0  12287  expcnv  12289  geo2sum  12299  geo2lim  12301  geoisum1c  12305  0.999...  12306  mertenslem2  12321  fprodseq  12368  fprodfac  12400  ef0lem  12445  ege2le3  12456  efaddlem  12459  efexp  12467  dvdsmodexp  12580  nn0enne  12687  nnehalf  12689  nno  12691  nn0o  12692  divalg2  12711  ndvdssub  12715  gcddiv  12814  gcdmultiple  12815  gcdmultiplez  12816  rpmulgcd  12821  rplpwr  12822  dvdssqlem  12825  eucalgf  12851  1nprm  12910  isprm6  12944  prmdvdsexp  12945  pwbdvdslemn  12962  phicl2  13014  phibndlem  13016  phiprmpw  13022  crth  13024  hashgcdlem  13038  phisum  13041  pythagtriplem10  13070  pythagtriplem6  13071  pythagtriplem7  13072  pythagtriplem12  13076  pythagtriplem14  13078  pclemub  13088  pcexp  13110  pcid  13125  pcprod  13147  pcbc  13152  prmpwdvds  13156  infpnlem1  13160  infpnlem2  13161  prmunb  13163  1arith  13168  ennnfonelemjn  13344  ghmmulg  14110  znf1o  15037  znfi  15041  znhash  15042  znidom  15043  znidomb  15044  znrrg  15046  dvexp  15864  plycolemc  15911  logbgcd1irr  16125  birthdaylem2  16148  birthdaylem3  16149  pellexlem1  16151  1sgm2ppw  16211  chtublem  16217  pcbcctr  16225  bclbnd  16229  bposlem1  16233  lgsval4a  16263  gausslemma2dlem0c  16292  gausslemma2dlem0d  16293  gausslemma2dlem6  16308  2lgslem1a1  16327  2lgslem1c  16331  2lgslem3a1  16338  2lgslem3b1  16339  2lgslem3c1  16340  2lgslem3d1  16341  isclwwlknx  16779