Theorem nnnn0 9182

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8918  ℕ₀cn0 9175

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-n0 9176

This theorem is referenced by:  nnnn0i  9183  elnnnn0b  9219  elnnnn0c  9220  elnn0z  9265  elz2  9323  nn0ind-raph  9369  zindd  9370  fzo1fzo0n0  10182  ubmelfzo  10199  elfzom1elp1fzo  10201  fzo0sn0fzo1  10220  modqmulnn  10341  expnegap0  10527  expcllem  10530  expcl2lemap  10531  expap0  10549  expeq0  10550  mulexpzap  10559  expnlbnd  10644  apexp1  10697  facdiv  10717  faclbnd  10720  faclbnd3  10722  faclbnd6  10723  resqrexlemlo  11021  absexpzap  11088  nnf1o  11383  summodclem2a  11388  fsum3  11394  arisum  11505  expcnvap0  11509  expcnv  11511  geo2sum  11521  geo2lim  11523  geoisum1c  11527  0.999...  11528  mertenslem2  11543  fprodseq  11590  fprodfac  11622  ef0lem  11667  ege2le3  11678  efaddlem  11681  efexp  11689  dvdsmodexp  11801  nn0enne  11906  nnehalf  11908  nno  11910  nn0o  11911  divalg2  11930  ndvdssub  11934  gcddiv  12019  gcdmultiple  12020  gcdmultiplez  12021  rpmulgcd  12026  rplpwr  12027  dvdssqlem  12030  eucalgf  12054  1nprm  12113  isprm6  12146  prmdvdsexp  12147  pw2dvds  12165  oddpwdc  12173  phicl2  12213  phibndlem  12215  phiprmpw  12221  crth  12223  hashgcdlem  12237  phisum  12239  pythagtriplem10  12268  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem14  12276  pclemub  12286  pcexp  12308  pcid  12322  pcprod  12343  pcbc  12348  prmpwdvds  12352  infpnlem1  12356  infpnlem2  12357  prmunb  12359  1arith  12364  ennnfonelemjn  12402  dvexp  14145  logbgcd1irr  14355  lgsval4a  14393