Theorem nnnn0d 9163

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 9113	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3139	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2136  ℕcn 8853  ℕ₀cn0 9110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-n0 9111

This theorem is referenced by:  nn0ge2m1nn0  9171  nnzd  9308  eluzge2nn0  9503  modsumfzodifsn  10327  addmodlteq  10329  expnnval  10454  expgt1  10489  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  expnbnd  10574  facwordi  10649  faclbnd  10650  facavg  10655  bcm1k  10669  bcval5  10672  1elfz0hash  10715  resqrexlemnm  10956  resqrexlemcvg  10957  summodc  11320  zsumdc  11321  bcxmas  11426  geo2sum  11451  geo2lim  11453  geoisum1  11456  geoisum1c  11457  cvgratnnlembern  11460  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  mertenslemi1  11472  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  eftabs  11593  efcllemp  11595  eftlub  11627  eirraplem  11713  dvdsfac  11794  divalglemnqt  11853  divalglemeunn  11854  gcdval  11888  gcdcl  11895  dvdsgcdidd  11923  mulgcd  11945  rplpwr  11956  rppwr  11957  lcmcl  12000  lcmgcdnn  12010  nprmdvds1  12068  isprm5lem  12069  rpexp  12081  pw2dvdslemn  12093  sqpweven  12103  2sqpwodd  12104  nn0sqrtelqelz  12134  phiprmpw  12150  crth  12152  eulerthlema  12158  eulerthlemth  12160  eulerth  12161  fermltl  12162  odzcllem  12170  odzdvds  12173  odzphi  12174  modprm0  12182  prm23lt5  12191  pythagtriplem6  12198  pythagtriplem7  12199  pcprmpw2  12260  dvdsprmpweqle  12264  pcprod  12272  pcfac  12276  pcbc  12277  expnprm  12279  pockthlem  12282  pockthg  12283  prmunb  12288  mul4sqlem  12319  logbgcd1irraplemexp  13486  lgslem1  13501  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsvalmod  13520  lgsmod  13527  lgsdirprm  13535  lgsne0  13539  2sqlem3  13553  cvgcmp2nlemabs  13871  trilpolemlt1  13880  redcwlpolemeq1  13893  nconstwlpolem0  13901