Theorem nnnn0 9256

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 8990  ℕ₀cn0 9249

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-n0 9250

This theorem is referenced by:  nnnn0i  9257  elnnnn0b  9293  elnnnn0c  9294  elnn0z  9339  elz2  9397  nn0ind-raph  9443  zindd  9444  fzo1fzo0n0  10259  ubmelfzo  10276  elfzom1elp1fzo  10278  fzo0sn0fzo1  10297  modqmulnn  10434  expnegap0  10639  expcllem  10642  expcl2lemap  10643  expap0  10661  expeq0  10662  mulexpzap  10671  expnlbnd  10756  apexp1  10810  facdiv  10830  faclbnd  10833  faclbnd3  10835  faclbnd6  10836  resqrexlemlo  11178  absexpzap  11245  nnf1o  11541  summodclem2a  11546  fsum3  11552  arisum  11663  expcnvap0  11667  expcnv  11669  geo2sum  11679  geo2lim  11681  geoisum1c  11685  0.999...  11686  mertenslem2  11701  fprodseq  11748  fprodfac  11780  ef0lem  11825  ege2le3  11836  efaddlem  11839  efexp  11847  dvdsmodexp  11960  nn0enne  12067  nnehalf  12069  nno  12071  nn0o  12072  divalg2  12091  ndvdssub  12095  gcddiv  12186  gcdmultiple  12187  gcdmultiplez  12188  rpmulgcd  12193  rplpwr  12194  dvdssqlem  12197  eucalgf  12223  1nprm  12282  isprm6  12315  prmdvdsexp  12316  pw2dvds  12334  oddpwdc  12342  phicl2  12382  phibndlem  12384  phiprmpw  12390  crth  12392  hashgcdlem  12406  phisum  12409  pythagtriplem10  12438  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem14  12446  pclemub  12456  pcexp  12478  pcid  12493  pcprod  12515  pcbc  12520  prmpwdvds  12524  infpnlem1  12528  infpnlem2  12529  prmunb  12531  1arith  12536  ennnfonelemjn  12619  ghmmulg  13386  znf1o  14207  znfi  14211  znhash  14212  znidom  14213  znidomb  14214  znrrg  14216  dvexp  14947  plycolemc  14994  logbgcd1irr  15203  1sgm2ppw  15231  lgsval4a  15263  gausslemma2dlem0c  15292  gausslemma2dlem0d  15293  gausslemma2dlem6  15308  2lgslem1a1  15327  2lgslem1c  15331  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341