Theorem nnnn0 9156

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

Syntax hints:   → wi 4   ∈ wcel 2146  ℕcn 8892  ℕ₀cn0 9149

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-n0 9150

This theorem is referenced by:  nnnn0i  9157  elnnnn0b  9193  elnnnn0c  9194  elnn0z  9239  elz2  9297  nn0ind-raph  9343  zindd  9344  fzo1fzo0n0  10153  ubmelfzo  10170  elfzom1elp1fzo  10172  fzo0sn0fzo1  10191  modqmulnn  10312  expnegap0  10498  expcllem  10501  expcl2lemap  10502  expap0  10520  expeq0  10521  mulexpzap  10530  expnlbnd  10614  apexp1  10666  facdiv  10686  faclbnd  10689  faclbnd3  10691  faclbnd6  10692  resqrexlemlo  10990  absexpzap  11057  nnf1o  11352  summodclem2a  11357  fsum3  11363  arisum  11474  expcnvap0  11478  expcnv  11480  geo2sum  11490  geo2lim  11492  geoisum1c  11496  0.999...  11497  mertenslem2  11512  fprodseq  11559  fprodfac  11591  ef0lem  11636  ege2le3  11647  efaddlem  11650  efexp  11658  dvdsmodexp  11770  nn0enne  11874  nnehalf  11876  nno  11878  nn0o  11879  divalg2  11898  ndvdssub  11902  gcddiv  11987  gcdmultiple  11988  gcdmultiplez  11989  rpmulgcd  11994  rplpwr  11995  dvdssqlem  11998  eucalgf  12022  1nprm  12081  isprm6  12114  prmdvdsexp  12115  pw2dvds  12133  oddpwdc  12141  phicl2  12181  phibndlem  12183  phiprmpw  12189  crth  12191  hashgcdlem  12205  phisum  12207  pythagtriplem10  12236  pythagtriplem6  12237  pythagtriplem7  12238  pythagtriplem12  12242  pythagtriplem14  12244  pclemub  12254  pcexp  12276  pcid  12290  pcprod  12311  pcbc  12316  prmpwdvds  12320  infpnlem1  12324  infpnlem2  12325  prmunb  12327  1arith  12332  ennnfonelemjn  12370  dvexp  13755  logbgcd1irr  13965  lgsval4a  14003