Theorem nnnn0 9315

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℕcn 9049  ℕ₀cn0 9308

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 3172  df-in 3174  df-ss 3181  df-n0 9309

This theorem is referenced by:  nnnn0i  9316  elnnnn0b  9352  elnnnn0c  9353  elnn0z  9398  elz2  9457  nn0ind-raph  9503  zindd  9504  fzo1fzo0n0  10320  ubmelfzo  10342  elfzom1elp1fzo  10344  fzo0sn0fzo1  10363  modqmulnn  10500  expnegap0  10705  expcllem  10708  expcl2lemap  10709  expap0  10727  expeq0  10728  mulexpzap  10737  expnlbnd  10822  apexp1  10876  facdiv  10896  faclbnd  10899  faclbnd3  10901  faclbnd6  10902  pfxn0  11153  resqrexlemlo  11374  absexpzap  11441  nnf1o  11737  summodclem2a  11742  fsum3  11748  arisum  11859  expcnvap0  11863  expcnv  11865  geo2sum  11875  geo2lim  11877  geoisum1c  11881  0.999...  11882  mertenslem2  11897  fprodseq  11944  fprodfac  11976  ef0lem  12021  ege2le3  12032  efaddlem  12035  efexp  12043  dvdsmodexp  12156  nn0enne  12263  nnehalf  12265  nno  12267  nn0o  12268  divalg2  12287  ndvdssub  12291  gcddiv  12390  gcdmultiple  12391  gcdmultiplez  12392  rpmulgcd  12397  rplpwr  12398  dvdssqlem  12401  eucalgf  12427  1nprm  12486  isprm6  12519  prmdvdsexp  12520  pw2dvds  12538  oddpwdc  12546  phicl2  12586  phibndlem  12588  phiprmpw  12594  crth  12596  hashgcdlem  12610  phisum  12613  pythagtriplem10  12642  pythagtriplem6  12643  pythagtriplem7  12644  pythagtriplem12  12648  pythagtriplem14  12650  pclemub  12660  pcexp  12682  pcid  12697  pcprod  12719  pcbc  12724  prmpwdvds  12728  infpnlem1  12732  infpnlem2  12733  prmunb  12735  1arith  12740  ennnfonelemjn  12823  ghmmulg  13642  znf1o  14463  znfi  14467  znhash  14468  znidom  14469  znidomb  14470  znrrg  14472  dvexp  15233  plycolemc  15280  logbgcd1irr  15489  1sgm2ppw  15517  lgsval4a  15549  gausslemma2dlem0c  15578  gausslemma2dlem0d  15579  gausslemma2dlem6  15594  2lgslem1a1  15613  2lgslem1c  15617  2lgslem3a1  15624  2lgslem3b1  15625  2lgslem3c1  15626  2lgslem3d1  15627