Theorem nnnn0 9183

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8919  ℕ₀cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-n0 9177

This theorem is referenced by:  nnnn0i  9184  elnnnn0b  9220  elnnnn0c  9221  elnn0z  9266  elz2  9324  nn0ind-raph  9370  zindd  9371  fzo1fzo0n0  10183  ubmelfzo  10200  elfzom1elp1fzo  10202  fzo0sn0fzo1  10221  modqmulnn  10342  expnegap0  10528  expcllem  10531  expcl2lemap  10532  expap0  10550  expeq0  10551  mulexpzap  10560  expnlbnd  10645  apexp1  10698  facdiv  10718  faclbnd  10721  faclbnd3  10723  faclbnd6  10724  resqrexlemlo  11022  absexpzap  11089  nnf1o  11384  summodclem2a  11389  fsum3  11395  arisum  11506  expcnvap0  11510  expcnv  11512  geo2sum  11522  geo2lim  11524  geoisum1c  11528  0.999...  11529  mertenslem2  11544  fprodseq  11591  fprodfac  11623  ef0lem  11668  ege2le3  11679  efaddlem  11682  efexp  11690  dvdsmodexp  11802  nn0enne  11907  nnehalf  11909  nno  11911  nn0o  11912  divalg2  11931  ndvdssub  11935  gcddiv  12020  gcdmultiple  12021  gcdmultiplez  12022  rpmulgcd  12027  rplpwr  12028  dvdssqlem  12031  eucalgf  12055  1nprm  12114  isprm6  12147  prmdvdsexp  12148  pw2dvds  12166  oddpwdc  12174  phicl2  12214  phibndlem  12216  phiprmpw  12222  crth  12224  hashgcdlem  12238  phisum  12240  pythagtriplem10  12269  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  pclemub  12287  pcexp  12309  pcid  12323  pcprod  12344  pcbc  12349  prmpwdvds  12353  infpnlem1  12357  infpnlem2  12358  prmunb  12360  1arith  12365  ennnfonelemjn  12403  dvexp  14178  logbgcd1irr  14388  lgsval4a  14426