Theorem nnnn0 9520

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℕcn 9254  ℕ₀cn0 9513

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-n0 9514

This theorem is referenced by:  nnnn0i  9521  elnnnn0b  9557  elnnnn0c  9558  elnn0z  9607  elz2  9666  nn0ind-raph  9713  zindd  9714  fzo1fzo0n0  10544  ubmelfzo  10567  elfzom1elp1fzo  10569  fzo0sn0fzo1  10588  modqmulnn  10728  expnegap0  10933  expcllem  10936  expcl2lemap  10937  expap0  10955  expeq0  10956  mulexpzap  10965  expnlbnd  11051  apexp1  11105  facdiv  11125  faclbnd  11128  faclbnd3  11130  faclbnd6  11131  pfxn0  11405  resqrexlemlo  11723  absexpzap  11790  nnf1o  12087  summodclem2a  12092  fsum3  12098  arisum  12209  expcnvap0  12213  expcnv  12215  geo2sum  12225  geo2lim  12227  geoisum1c  12231  0.999...  12232  mertenslem2  12247  fprodseq  12294  fprodfac  12326  ef0lem  12371  ege2le3  12382  efaddlem  12385  efexp  12393  dvdsmodexp  12506  nn0enne  12613  nnehalf  12615  nno  12617  nn0o  12618  divalg2  12637  ndvdssub  12641  gcddiv  12740  gcdmultiple  12741  gcdmultiplez  12742  rpmulgcd  12747  rplpwr  12748  dvdssqlem  12751  eucalgf  12777  1nprm  12836  isprm6  12869  prmdvdsexp  12870  pw2dvds  12888  oddpwdc  12896  phicl2  12936  phibndlem  12938  phiprmpw  12944  crth  12946  hashgcdlem  12960  phisum  12963  pythagtriplem10  12992  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  pclemub  13010  pcexp  13032  pcid  13047  pcprod  13069  pcbc  13074  prmpwdvds  13078  infpnlem1  13082  infpnlem2  13083  prmunb  13085  1arith  13090  ennnfonelemjn  13237  ghmmulg  14057  znf1o  14911  znfi  14915  znhash  14916  znidom  14917  znidomb  14918  znrrg  14920  dvexp  15688  plycolemc  15735  logbgcd1irr  15944  pellexlem1  15957  1sgm2ppw  15975  lgsval4a  16007  gausslemma2dlem0c  16036  gausslemma2dlem0d  16037  gausslemma2dlem6  16052  2lgslem1a1  16071  2lgslem1c  16075  2lgslem3a1  16082  2lgslem3b1  16083  2lgslem3c1  16084  2lgslem3d1  16085  isclwwlknx  16523