Theorem nnnn0 9553

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℕcn 9287  ℕ₀cn0 9546

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9547

This theorem is referenced by:  nnnn0i  9554  elnnnn0b  9590  elnnnn0c  9591  elnn0z  9640  elz2  9699  nn0ind-raph  9746  zindd  9747  fzo1fzo0n0  10578  ubmelfzo  10601  elfzom1elp1fzo  10603  fzo0sn0fzo1  10622  modqmulnn  10762  expnegap0  10967  expcllem  10970  expcl2lemap  10971  expap0  10989  expeq0  10990  mulexpzap  10999  expnlbnd  11085  apexp1  11139  facdiv  11159  faclbnd  11162  faclbnd3  11164  faclbnd6  11165  pfxn0  11443  resqrexlemlo  11762  absexpzap  11829  nnf1o  12126  summodclem2a  12131  fsum3  12137  arisum  12248  expcnvap0  12252  expcnv  12254  geo2sum  12264  geo2lim  12266  geoisum1c  12270  0.999...  12271  mertenslem2  12286  fprodseq  12333  fprodfac  12365  ef0lem  12410  ege2le3  12421  efaddlem  12424  efexp  12432  dvdsmodexp  12545  nn0enne  12652  nnehalf  12654  nno  12656  nn0o  12657  divalg2  12676  ndvdssub  12680  gcddiv  12779  gcdmultiple  12780  gcdmultiplez  12781  rpmulgcd  12786  rplpwr  12787  dvdssqlem  12790  eucalgf  12816  1nprm  12875  isprm6  12908  prmdvdsexp  12909  pw2dvds  12927  oddpwdc  12935  phicl2  12975  phibndlem  12977  phiprmpw  12983  crth  12985  hashgcdlem  12999  phisum  13002  pythagtriplem10  13031  pythagtriplem6  13032  pythagtriplem7  13033  pythagtriplem12  13037  pythagtriplem14  13039  pclemub  13049  pcexp  13071  pcid  13086  pcprod  13108  pcbc  13113  prmpwdvds  13117  infpnlem1  13121  infpnlem2  13122  prmunb  13124  1arith  13129  ennnfonelemjn  13276  ghmmulg  14042  znf1o  14969  znfi  14973  znhash  14974  znidom  14975  znidomb  14976  znrrg  14978  dvexp  15795  plycolemc  15842  logbgcd1irr  16052  birthdaylem2  16071  birthdaylem3  16072  pellexlem1  16074  1sgm2ppw  16092  lgsval4a  16124  gausslemma2dlem0c  16153  gausslemma2dlem0d  16154  gausslemma2dlem6  16169  2lgslem1a1  16188  2lgslem1c  16192  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  isclwwlknx  16640