Theorem nnnn0 9247

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℕcn 8982  ℕ₀cn0 9240

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-n0 9241

This theorem is referenced by:  nnnn0i  9248  elnnnn0b  9284  elnnnn0c  9285  elnn0z  9330  elz2  9388  nn0ind-raph  9434  zindd  9435  fzo1fzo0n0  10250  ubmelfzo  10267  elfzom1elp1fzo  10269  fzo0sn0fzo1  10288  modqmulnn  10413  expnegap0  10618  expcllem  10621  expcl2lemap  10622  expap0  10640  expeq0  10641  mulexpzap  10650  expnlbnd  10735  apexp1  10789  facdiv  10809  faclbnd  10812  faclbnd3  10814  faclbnd6  10815  resqrexlemlo  11157  absexpzap  11224  nnf1o  11519  summodclem2a  11524  fsum3  11530  arisum  11641  expcnvap0  11645  expcnv  11647  geo2sum  11657  geo2lim  11659  geoisum1c  11663  0.999...  11664  mertenslem2  11679  fprodseq  11726  fprodfac  11758  ef0lem  11803  ege2le3  11814  efaddlem  11817  efexp  11825  dvdsmodexp  11938  nn0enne  12043  nnehalf  12045  nno  12047  nn0o  12048  divalg2  12067  ndvdssub  12071  gcddiv  12156  gcdmultiple  12157  gcdmultiplez  12158  rpmulgcd  12163  rplpwr  12164  dvdssqlem  12167  eucalgf  12193  1nprm  12252  isprm6  12285  prmdvdsexp  12286  pw2dvds  12304  oddpwdc  12312  phicl2  12352  phibndlem  12354  phiprmpw  12360  crth  12362  hashgcdlem  12376  phisum  12378  pythagtriplem10  12407  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  pclemub  12425  pcexp  12447  pcid  12462  pcprod  12484  pcbc  12489  prmpwdvds  12493  infpnlem1  12497  infpnlem2  12498  prmunb  12500  1arith  12505  ennnfonelemjn  12559  ghmmulg  13326  znf1o  14139  znfi  14143  znhash  14144  znidom  14145  znidomb  14146  znrrg  14148  dvexp  14860  logbgcd1irr  15099  lgsval4a  15138  gausslemma2dlem0c  15167  gausslemma2dlem0d  15168  gausslemma2dlem6  15183