Theorem nnnn0 9364

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9098  ℕ₀cn0 9357

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 9358

This theorem is referenced by:  nnnn0i  9365  elnnnn0b  9401  elnnnn0c  9402  elnn0z  9447  elz2  9506  nn0ind-raph  9552  zindd  9553  fzo1fzo0n0  10371  ubmelfzo  10393  elfzom1elp1fzo  10395  fzo0sn0fzo1  10414  modqmulnn  10551  expnegap0  10756  expcllem  10759  expcl2lemap  10760  expap0  10778  expeq0  10779  mulexpzap  10788  expnlbnd  10873  apexp1  10927  facdiv  10947  faclbnd  10950  faclbnd3  10952  faclbnd6  10953  pfxn0  11206  resqrexlemlo  11510  absexpzap  11577  nnf1o  11873  summodclem2a  11878  fsum3  11884  arisum  11995  expcnvap0  11999  expcnv  12001  geo2sum  12011  geo2lim  12013  geoisum1c  12017  0.999...  12018  mertenslem2  12033  fprodseq  12080  fprodfac  12112  ef0lem  12157  ege2le3  12168  efaddlem  12171  efexp  12179  dvdsmodexp  12292  nn0enne  12399  nnehalf  12401  nno  12403  nn0o  12404  divalg2  12423  ndvdssub  12427  gcddiv  12526  gcdmultiple  12527  gcdmultiplez  12528  rpmulgcd  12533  rplpwr  12534  dvdssqlem  12537  eucalgf  12563  1nprm  12622  isprm6  12655  prmdvdsexp  12656  pw2dvds  12674  oddpwdc  12682  phicl2  12722  phibndlem  12724  phiprmpw  12730  crth  12732  hashgcdlem  12746  phisum  12749  pythagtriplem10  12778  pythagtriplem6  12779  pythagtriplem7  12780  pythagtriplem12  12784  pythagtriplem14  12786  pclemub  12796  pcexp  12818  pcid  12833  pcprod  12855  pcbc  12860  prmpwdvds  12864  infpnlem1  12868  infpnlem2  12869  prmunb  12871  1arith  12876  ennnfonelemjn  12959  ghmmulg  13779  znf1o  14600  znfi  14604  znhash  14605  znidom  14606  znidomb  14607  znrrg  14609  dvexp  15370  plycolemc  15417  logbgcd1irr  15626  1sgm2ppw  15654  lgsval4a  15686  gausslemma2dlem0c  15715  gausslemma2dlem0d  15716  gausslemma2dlem6  15731  2lgslem1a1  15750  2lgslem1c  15754  2lgslem3a1  15761  2lgslem3b1  15762  2lgslem3c1  15763  2lgslem3d1  15764