Theorem nnnn0 9409

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9143  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-n0 9403

This theorem is referenced by:  nnnn0i  9410  elnnnn0b  9446  elnnnn0c  9447  elnn0z  9492  elz2  9551  nn0ind-raph  9597  zindd  9598  fzo1fzo0n0  10423  ubmelfzo  10446  elfzom1elp1fzo  10448  fzo0sn0fzo1  10467  modqmulnn  10605  expnegap0  10810  expcllem  10813  expcl2lemap  10814  expap0  10832  expeq0  10833  mulexpzap  10842  expnlbnd  10927  apexp1  10981  facdiv  11001  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  pfxn0  11273  resqrexlemlo  11578  absexpzap  11645  nnf1o  11942  summodclem2a  11947  fsum3  11953  arisum  12064  expcnvap0  12068  expcnv  12070  geo2sum  12080  geo2lim  12082  geoisum1c  12086  0.999...  12087  mertenslem2  12102  fprodseq  12149  fprodfac  12181  ef0lem  12226  ege2le3  12237  efaddlem  12240  efexp  12248  dvdsmodexp  12361  nn0enne  12468  nnehalf  12470  nno  12472  nn0o  12473  divalg2  12492  ndvdssub  12496  gcddiv  12595  gcdmultiple  12596  gcdmultiplez  12597  rpmulgcd  12602  rplpwr  12603  dvdssqlem  12606  eucalgf  12632  1nprm  12691  isprm6  12724  prmdvdsexp  12725  pw2dvds  12743  oddpwdc  12751  phicl2  12791  phibndlem  12793  phiprmpw  12799  crth  12801  hashgcdlem  12815  phisum  12818  pythagtriplem10  12847  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem12  12853  pythagtriplem14  12855  pclemub  12865  pcexp  12887  pcid  12902  pcprod  12924  pcbc  12929  prmpwdvds  12933  infpnlem1  12937  infpnlem2  12938  prmunb  12940  1arith  12945  ennnfonelemjn  13028  ghmmulg  13848  znf1o  14671  znfi  14675  znhash  14676  znidom  14677  znidomb  14678  znrrg  14680  dvexp  15441  plycolemc  15488  logbgcd1irr  15697  1sgm2ppw  15725  lgsval4a  15757  gausslemma2dlem0c  15786  gausslemma2dlem0d  15787  gausslemma2dlem6  15802  2lgslem1a1  15821  2lgslem1c  15825  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  isclwwlknx  16273