Theorem nnnn0 9402

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9136  ℕ₀cn0 9395

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-n0 9396

This theorem is referenced by:  nnnn0i  9403  elnnnn0b  9439  elnnnn0c  9440  elnn0z  9485  elz2  9544  nn0ind-raph  9590  zindd  9591  fzo1fzo0n0  10415  ubmelfzo  10438  elfzom1elp1fzo  10440  fzo0sn0fzo1  10459  modqmulnn  10597  expnegap0  10802  expcllem  10805  expcl2lemap  10806  expap0  10824  expeq0  10825  mulexpzap  10834  expnlbnd  10919  apexp1  10973  facdiv  10993  faclbnd  10996  faclbnd3  10998  faclbnd6  10999  pfxn0  11262  resqrexlemlo  11567  absexpzap  11634  nnf1o  11930  summodclem2a  11935  fsum3  11941  arisum  12052  expcnvap0  12056  expcnv  12058  geo2sum  12068  geo2lim  12070  geoisum1c  12074  0.999...  12075  mertenslem2  12090  fprodseq  12137  fprodfac  12169  ef0lem  12214  ege2le3  12225  efaddlem  12228  efexp  12236  dvdsmodexp  12349  nn0enne  12456  nnehalf  12458  nno  12460  nn0o  12461  divalg2  12480  ndvdssub  12484  gcddiv  12583  gcdmultiple  12584  gcdmultiplez  12585  rpmulgcd  12590  rplpwr  12591  dvdssqlem  12594  eucalgf  12620  1nprm  12679  isprm6  12712  prmdvdsexp  12713  pw2dvds  12731  oddpwdc  12739  phicl2  12779  phibndlem  12781  phiprmpw  12787  crth  12789  hashgcdlem  12803  phisum  12806  pythagtriplem10  12835  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem12  12841  pythagtriplem14  12843  pclemub  12853  pcexp  12875  pcid  12890  pcprod  12912  pcbc  12917  prmpwdvds  12921  infpnlem1  12925  infpnlem2  12926  prmunb  12928  1arith  12933  ennnfonelemjn  13016  ghmmulg  13836  znf1o  14658  znfi  14662  znhash  14663  znidom  14664  znidomb  14665  znrrg  14667  dvexp  15428  plycolemc  15475  logbgcd1irr  15684  1sgm2ppw  15712  lgsval4a  15744  gausslemma2dlem0c  15773  gausslemma2dlem0d  15774  gausslemma2dlem6  15789  2lgslem1a1  15808  2lgslem1c  15812  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  isclwwlknx  16225