Theorem nnnn0 9142

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 8878  ℕ₀cn0 9135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-n0 9136

This theorem is referenced by:  nnnn0i  9143  elnnnn0b  9179  elnnnn0c  9180  elnn0z  9225  elz2  9283  nn0ind-raph  9329  zindd  9330  fzo1fzo0n0  10139  ubmelfzo  10156  elfzom1elp1fzo  10158  fzo0sn0fzo1  10177  modqmulnn  10298  expnegap0  10484  expcllem  10487  expcl2lemap  10488  expap0  10506  expeq0  10507  mulexpzap  10516  expnlbnd  10600  apexp1  10652  facdiv  10672  faclbnd  10675  faclbnd3  10677  faclbnd6  10678  resqrexlemlo  10977  absexpzap  11044  nnf1o  11339  summodclem2a  11344  fsum3  11350  arisum  11461  expcnvap0  11465  expcnv  11467  geo2sum  11477  geo2lim  11479  geoisum1c  11483  0.999...  11484  mertenslem2  11499  fprodseq  11546  fprodfac  11578  ef0lem  11623  ege2le3  11634  efaddlem  11637  efexp  11645  dvdsmodexp  11757  nn0enne  11861  nnehalf  11863  nno  11865  nn0o  11866  divalg2  11885  ndvdssub  11889  gcddiv  11974  gcdmultiple  11975  gcdmultiplez  11976  rpmulgcd  11981  rplpwr  11982  dvdssqlem  11985  eucalgf  12009  1nprm  12068  isprm6  12101  prmdvdsexp  12102  pw2dvds  12120  oddpwdc  12128  phicl2  12168  phibndlem  12170  phiprmpw  12176  crth  12178  hashgcdlem  12192  phisum  12194  pythagtriplem10  12223  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  pclemub  12241  pcexp  12263  pcid  12277  pcprod  12298  pcbc  12303  prmpwdvds  12307  infpnlem1  12311  infpnlem2  12312  prmunb  12314  1arith  12319  ennnfonelemjn  12357  dvexp  13469  logbgcd1irr  13679  lgsval4a  13717