Theorem nnnn0 9452

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9186  ℕ₀cn0 9445

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-n0 9446

This theorem is referenced by:  nnnn0i  9453  elnnnn0b  9489  elnnnn0c  9490  elnn0z  9535  elz2  9594  nn0ind-raph  9640  zindd  9641  fzo1fzo0n0  10466  ubmelfzo  10489  elfzom1elp1fzo  10491  fzo0sn0fzo1  10510  modqmulnn  10648  expnegap0  10853  expcllem  10856  expcl2lemap  10857  expap0  10875  expeq0  10876  mulexpzap  10885  expnlbnd  10970  apexp1  11024  facdiv  11044  faclbnd  11047  faclbnd3  11049  faclbnd6  11050  pfxn0  11316  resqrexlemlo  11634  absexpzap  11701  nnf1o  11998  summodclem2a  12003  fsum3  12009  arisum  12120  expcnvap0  12124  expcnv  12126  geo2sum  12136  geo2lim  12138  geoisum1c  12142  0.999...  12143  mertenslem2  12158  fprodseq  12205  fprodfac  12237  ef0lem  12282  ege2le3  12293  efaddlem  12296  efexp  12304  dvdsmodexp  12417  nn0enne  12524  nnehalf  12526  nno  12528  nn0o  12529  divalg2  12548  ndvdssub  12552  gcddiv  12651  gcdmultiple  12652  gcdmultiplez  12653  rpmulgcd  12658  rplpwr  12659  dvdssqlem  12662  eucalgf  12688  1nprm  12747  isprm6  12780  prmdvdsexp  12781  pw2dvds  12799  oddpwdc  12807  phicl2  12847  phibndlem  12849  phiprmpw  12855  crth  12857  hashgcdlem  12871  phisum  12874  pythagtriplem10  12903  pythagtriplem6  12904  pythagtriplem7  12905  pythagtriplem12  12909  pythagtriplem14  12911  pclemub  12921  pcexp  12943  pcid  12958  pcprod  12980  pcbc  12985  prmpwdvds  12989  infpnlem1  12993  infpnlem2  12994  prmunb  12996  1arith  13001  ennnfonelemjn  13084  ghmmulg  13904  znf1o  14727  znfi  14731  znhash  14732  znidom  14733  znidomb  14734  znrrg  14736  dvexp  15502  plycolemc  15549  logbgcd1irr  15758  pellexlem1  15771  1sgm2ppw  15789  lgsval4a  15821  gausslemma2dlem0c  15850  gausslemma2dlem0d  15851  gausslemma2dlem6  15866  2lgslem1a1  15885  2lgslem1c  15889  2lgslem3a1  15896  2lgslem3b1  15897  2lgslem3c1  15898  2lgslem3d1  15899  isclwwlknx  16337