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  9669  elz2  9728  nn0ind-raph  9775  zindd  9776  fzo1fzo0n0  10613  ubmelfzo  10636  elfzom1elp1fzo  10638  fzo0sn0fzo1  10657  modqmulnn  10801  expnegap0  11006  expcllem  11009  expcl2lemap  11010  expap0  11028  expeq0  11029  mulexpzap  11038  expnlbnd  11124  apexp1  11179  facdiv  11199  faclbnd  11202  faclbnd3  11204  faclbnd6  11205  pfxn0  11483  resqrexlemlo  11802  absexpzap  11870  nnf1o  12169  summodclem2a  12174  fsum3  12180  arisum  12291  expcnvap0  12295  expcnv  12297  geo2sum  12307  geo2lim  12309  geoisum1c  12313  0.999...  12314  mertenslem2  12329  fprodseq  12376  fprodfac  12408  ef0lem  12453  ege2le3  12464  efaddlem  12467  efexp  12475  dvdsmodexp  12588  nn0enne  12695  nnehalf  12697  nno  12699  nn0o  12700  divalg2  12719  ndvdssub  12723  gcddiv  12822  gcdmultiple  12823  gcdmultiplez  12824  rpmulgcd  12829  rplpwr  12830  dvdssqlem  12833  eucalgf  12859  1nprm  12918  isprm6  12952  prmdvdsexp  12953  pwbdvdslemn  12970  phicl2  13022  phibndlem  13024  phiprmpw  13030  crth  13032  hashgcdlem  13046  phisum  13049  pythagtriplem10  13078  pythagtriplem6  13079  pythagtriplem7  13080  pythagtriplem12  13084  pythagtriplem14  13086  pclemub  13096  pcexp  13118  pcid  13133  pcprod  13155  pcbc  13160  prmpwdvds  13164  infpnlem1  13168  infpnlem2  13169  prmunb  13171  1arith  13176  ennnfonelemjn  13352  ghmmulg  14119  znf1o  15096  znfi  15100  znhash  15101  znidom  15102  znidomb  15103  znrrg  15105  dvexp  15949  plycolemc  15996  logbgcd1irr  16215  birthdaylem2  16238  birthdaylem3  16239  pellexlem1  16241  1sgm2ppw  16301  chtublem  16307  pcbcctr  16315  bclbnd  16319  bposlem1  16323  lgsval4a  16358  gausslemma2dlem0c  16387  gausslemma2dlem0d  16388  gausslemma2dlem6  16403  2lgslem1a1  16422  2lgslem1c  16426  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  isclwwlknx  16874