Theorem nnnn0 9317

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℕcn 9051  ℕ₀cn0 9310

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-n0 9311

This theorem is referenced by:  nnnn0i  9318  elnnnn0b  9354  elnnnn0c  9355  elnn0z  9400  elz2  9459  nn0ind-raph  9505  zindd  9506  fzo1fzo0n0  10324  ubmelfzo  10346  elfzom1elp1fzo  10348  fzo0sn0fzo1  10367  modqmulnn  10504  expnegap0  10709  expcllem  10712  expcl2lemap  10713  expap0  10731  expeq0  10732  mulexpzap  10741  expnlbnd  10826  apexp1  10880  facdiv  10900  faclbnd  10903  faclbnd3  10905  faclbnd6  10906  pfxn0  11159  resqrexlemlo  11394  absexpzap  11461  nnf1o  11757  summodclem2a  11762  fsum3  11768  arisum  11879  expcnvap0  11883  expcnv  11885  geo2sum  11895  geo2lim  11897  geoisum1c  11901  0.999...  11902  mertenslem2  11917  fprodseq  11964  fprodfac  11996  ef0lem  12041  ege2le3  12052  efaddlem  12055  efexp  12063  dvdsmodexp  12176  nn0enne  12283  nnehalf  12285  nno  12287  nn0o  12288  divalg2  12307  ndvdssub  12311  gcddiv  12410  gcdmultiple  12411  gcdmultiplez  12412  rpmulgcd  12417  rplpwr  12418  dvdssqlem  12421  eucalgf  12447  1nprm  12506  isprm6  12539  prmdvdsexp  12540  pw2dvds  12558  oddpwdc  12566  phicl2  12606  phibndlem  12608  phiprmpw  12614  crth  12616  hashgcdlem  12630  phisum  12633  pythagtriplem10  12662  pythagtriplem6  12663  pythagtriplem7  12664  pythagtriplem12  12668  pythagtriplem14  12670  pclemub  12680  pcexp  12702  pcid  12717  pcprod  12739  pcbc  12744  prmpwdvds  12748  infpnlem1  12752  infpnlem2  12753  prmunb  12755  1arith  12760  ennnfonelemjn  12843  ghmmulg  13662  znf1o  14483  znfi  14487  znhash  14488  znidom  14489  znidomb  14490  znrrg  14492  dvexp  15253  plycolemc  15300  logbgcd1irr  15509  1sgm2ppw  15537  lgsval4a  15569  gausslemma2dlem0c  15598  gausslemma2dlem0d  15599  gausslemma2dlem6  15614  2lgslem1a1  15633  2lgslem1c  15637  2lgslem3a1  15644  2lgslem3b1  15645  2lgslem3c1  15646  2lgslem3d1  15647