Theorem nnnn0 9273

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 9007  ℕ₀cn0 9266

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-n0 9267

This theorem is referenced by:  nnnn0i  9274  elnnnn0b  9310  elnnnn0c  9311  elnn0z  9356  elz2  9414  nn0ind-raph  9460  zindd  9461  fzo1fzo0n0  10276  ubmelfzo  10293  elfzom1elp1fzo  10295  fzo0sn0fzo1  10314  modqmulnn  10451  expnegap0  10656  expcllem  10659  expcl2lemap  10660  expap0  10678  expeq0  10679  mulexpzap  10688  expnlbnd  10773  apexp1  10827  facdiv  10847  faclbnd  10850  faclbnd3  10852  faclbnd6  10853  resqrexlemlo  11195  absexpzap  11262  nnf1o  11558  summodclem2a  11563  fsum3  11569  arisum  11680  expcnvap0  11684  expcnv  11686  geo2sum  11696  geo2lim  11698  geoisum1c  11702  0.999...  11703  mertenslem2  11718  fprodseq  11765  fprodfac  11797  ef0lem  11842  ege2le3  11853  efaddlem  11856  efexp  11864  dvdsmodexp  11977  nn0enne  12084  nnehalf  12086  nno  12088  nn0o  12089  divalg2  12108  ndvdssub  12112  gcddiv  12211  gcdmultiple  12212  gcdmultiplez  12213  rpmulgcd  12218  rplpwr  12219  dvdssqlem  12222  eucalgf  12248  1nprm  12307  isprm6  12340  prmdvdsexp  12341  pw2dvds  12359  oddpwdc  12367  phicl2  12407  phibndlem  12409  phiprmpw  12415  crth  12417  hashgcdlem  12431  phisum  12434  pythagtriplem10  12463  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  pclemub  12481  pcexp  12503  pcid  12518  pcprod  12540  pcbc  12545  prmpwdvds  12549  infpnlem1  12553  infpnlem2  12554  prmunb  12556  1arith  12561  ennnfonelemjn  12644  ghmmulg  13462  znf1o  14283  znfi  14287  znhash  14288  znidom  14289  znidomb  14290  znrrg  14292  dvexp  15031  plycolemc  15078  logbgcd1irr  15287  1sgm2ppw  15315  lgsval4a  15347  gausslemma2dlem0c  15376  gausslemma2dlem0d  15377  gausslemma2dlem6  15392  2lgslem1a1  15411  2lgslem1c  15415  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425