Theorem nnnn0 9523

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℕcn 9257  ℕ₀cn0 9516

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-n0 9517

This theorem is referenced by:  nnnn0i  9524  elnnnn0b  9560  elnnnn0c  9561  elnn0z  9610  elz2  9669  nn0ind-raph  9716  zindd  9717  fzo1fzo0n0  10547  ubmelfzo  10570  elfzom1elp1fzo  10572  fzo0sn0fzo1  10591  modqmulnn  10731  expnegap0  10936  expcllem  10939  expcl2lemap  10940  expap0  10958  expeq0  10959  mulexpzap  10968  expnlbnd  11054  apexp1  11108  facdiv  11128  faclbnd  11131  faclbnd3  11133  faclbnd6  11134  pfxn0  11408  resqrexlemlo  11727  absexpzap  11794  nnf1o  12091  summodclem2a  12096  fsum3  12102  arisum  12213  expcnvap0  12217  expcnv  12219  geo2sum  12229  geo2lim  12231  geoisum1c  12235  0.999...  12236  mertenslem2  12251  fprodseq  12298  fprodfac  12330  ef0lem  12375  ege2le3  12386  efaddlem  12389  efexp  12397  dvdsmodexp  12510  nn0enne  12617  nnehalf  12619  nno  12621  nn0o  12622  divalg2  12641  ndvdssub  12645  gcddiv  12744  gcdmultiple  12745  gcdmultiplez  12746  rpmulgcd  12751  rplpwr  12752  dvdssqlem  12755  eucalgf  12781  1nprm  12840  isprm6  12873  prmdvdsexp  12874  pw2dvds  12892  oddpwdc  12900  phicl2  12940  phibndlem  12942  phiprmpw  12948  crth  12950  hashgcdlem  12964  phisum  12967  pythagtriplem10  12996  pythagtriplem6  12997  pythagtriplem7  12998  pythagtriplem12  13002  pythagtriplem14  13004  pclemub  13014  pcexp  13036  pcid  13051  pcprod  13073  pcbc  13078  prmpwdvds  13082  infpnlem1  13086  infpnlem2  13087  prmunb  13089  1arith  13094  ennnfonelemjn  13241  ghmmulg  14013  znf1o  14929  znfi  14933  znhash  14934  znidom  14935  znidomb  14936  znrrg  14938  dvexp  15706  plycolemc  15753  logbgcd1irr  15962  pellexlem1  15975  1sgm2ppw  15993  lgsval4a  16025  gausslemma2dlem0c  16054  gausslemma2dlem0d  16055  gausslemma2dlem6  16070  2lgslem1a1  16089  2lgslem1c  16093  2lgslem3a1  16100  2lgslem3b1  16101  2lgslem3c1  16102  2lgslem3d1  16103  isclwwlknx  16541