Theorem nnnn0 9392

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9126  ℕ₀cn0 9385

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9386

This theorem is referenced by:  nnnn0i  9393  elnnnn0b  9429  elnnnn0c  9430  elnn0z  9475  elz2  9534  nn0ind-raph  9580  zindd  9581  fzo1fzo0n0  10400  ubmelfzo  10423  elfzom1elp1fzo  10425  fzo0sn0fzo1  10444  modqmulnn  10581  expnegap0  10786  expcllem  10789  expcl2lemap  10790  expap0  10808  expeq0  10809  mulexpzap  10818  expnlbnd  10903  apexp1  10957  facdiv  10977  faclbnd  10980  faclbnd3  10982  faclbnd6  10983  pfxn0  11241  resqrexlemlo  11545  absexpzap  11612  nnf1o  11908  summodclem2a  11913  fsum3  11919  arisum  12030  expcnvap0  12034  expcnv  12036  geo2sum  12046  geo2lim  12048  geoisum1c  12052  0.999...  12053  mertenslem2  12068  fprodseq  12115  fprodfac  12147  ef0lem  12192  ege2le3  12203  efaddlem  12206  efexp  12214  dvdsmodexp  12327  nn0enne  12434  nnehalf  12436  nno  12438  nn0o  12439  divalg2  12458  ndvdssub  12462  gcddiv  12561  gcdmultiple  12562  gcdmultiplez  12563  rpmulgcd  12568  rplpwr  12569  dvdssqlem  12572  eucalgf  12598  1nprm  12657  isprm6  12690  prmdvdsexp  12691  pw2dvds  12709  oddpwdc  12717  phicl2  12757  phibndlem  12759  phiprmpw  12765  crth  12767  hashgcdlem  12781  phisum  12784  pythagtriplem10  12813  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem12  12819  pythagtriplem14  12821  pclemub  12831  pcexp  12853  pcid  12868  pcprod  12890  pcbc  12895  prmpwdvds  12899  infpnlem1  12903  infpnlem2  12904  prmunb  12906  1arith  12911  ennnfonelemjn  12994  ghmmulg  13814  znf1o  14636  znfi  14640  znhash  14641  znidom  14642  znidomb  14643  znrrg  14645  dvexp  15406  plycolemc  15453  logbgcd1irr  15662  1sgm2ppw  15690  lgsval4a  15722  gausslemma2dlem0c  15751  gausslemma2dlem0d  15752  gausslemma2dlem6  15767  2lgslem1a1  15786  2lgslem1c  15790  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  isclwwlknx  16184