Theorem nnnn0 9582

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

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

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 9576

This theorem is used by:  nnnn0i  9583  elnnnn0b  9619  elnnnn0c  9620  elnn0z  9667  elz2  9726  nn0ind-raph  9774  zindd  9775  fzo1fzo0n0  10612  ubmelfzo  10635  elfzom1elp1fzo  10637  fzo0sn0fzo1  10656  modqmulnn  10800  expnegap0  11005  expcllem  11008  expcl2lemap  11009  expap0  11027  expeq0  11028  mulexpzap  11037  expnlbnd  11123  apexp1  11178  facdiv  11198  faclbnd  11201  faclbnd3  11203  faclbnd6  11204  pfxn0  11482  resqrexlemlo  11801  absexpzap  11869  nnf1o  12168  summodclem2a  12173  fsum3  12179  arisum  12290  expcnvap0  12294  expcnv  12296  geo2sum  12306  geo2lim  12308  geoisum1c  12312  0.999...  12313  mertenslem2  12328  fprodseq  12375  fprodfac  12407  ef0lem  12452  ege2le3  12463  efaddlem  12466  efexp  12474  dvdsmodexp  12587  nn0enne  12694  nnehalf  12696  nno  12698  nn0o  12699  divalg2  12718  ndvdssub  12722  gcddiv  12821  gcdmultiple  12822  gcdmultiplez  12823  rpmulgcd  12828  rplpwr  12829  dvdssqlem  12832  eucalgf  12858  1nprm  12917  isprm6  12951  prmdvdsexp  12952  pwbdvdslemn  12969  phicl2  13021  phibndlem  13023  phiprmpw  13029  crth  13031  hashgcdlem  13045  phisum  13048  pythagtriplem10  13077  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pclemub  13095  pcexp  13117  pcid  13132  pcprod  13154  pcbc  13159  prmpwdvds  13163  infpnlem1  13167  infpnlem2  13168  prmunb  13170  1arith  13175  ennnfonelemjn  13351  ghmmulg  14118  znf1o  15095  znfi  15099  znhash  15100  znidom  15101  znidomb  15102  znrrg  15104  dvexp  15970  plycolemc  16017  logbgcd1irr  16236  birthdaylem2  16259  birthdaylem3  16260  pellexlem1  16262  1sgm2ppw  16322  chtublem  16328  pcbcctr  16336  bclbnd  16340  bposlem1  16344  lgsval4a  16379  gausslemma2dlem0c  16408  gausslemma2dlem0d  16409  gausslemma2dlem6  16424  2lgslem1a1  16443  2lgslem1c  16447  2lgslem3a1  16454  2lgslem3b1  16455  2lgslem3c1  16456  2lgslem3d1  16457  isclwwlknx  16895