Theorem nnnn0d 9302

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 9252	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3181	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 8990  ℕ₀cn0 9249

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 9250

This theorem is referenced by:  nn0ge2m1nn0  9310  nnzd  9447  eluzge2nn0  9643  modsumfzodifsn  10488  addmodlteq  10490  expnnval  10634  expgt1  10669  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  expnbnd  10755  facwordi  10832  faclbnd  10833  facavg  10838  bcm1k  10852  bcval5  10855  1elfz0hash  10898  resqrexlemnm  11183  resqrexlemcvg  11184  summodc  11548  zsumdc  11549  bcxmas  11654  geo2sum  11679  geo2lim  11681  geoisum1  11684  geoisum1c  11685  cvgratnnlembern  11688  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  mertenslemi1  11700  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  eftabs  11821  efcllemp  11823  eftlub  11855  eirraplem  11942  dvdsfac  12025  divalglemnqt  12085  divalglemeunn  12086  bitsfzo  12119  gcdval  12126  gcdcl  12133  dvdsgcdidd  12161  mulgcd  12183  rplpwr  12194  rppwr  12195  lcmcl  12240  lcmgcdnn  12250  nprmdvds1  12308  isprm5lem  12309  rpexp  12321  pw2dvdslemn  12333  sqpweven  12343  2sqpwodd  12344  nn0sqrtelqelz  12374  phiprmpw  12390  crth  12392  eulerthlema  12398  eulerthlemth  12400  eulerth  12401  fermltl  12402  odzcllem  12411  odzdvds  12414  odzphi  12415  modprm0  12423  prm23lt5  12432  pythagtriplem6  12439  pythagtriplem7  12440  pcprmpw2  12502  dvdsprmpweqle  12506  pcprod  12515  pcfac  12519  pcbc  12520  expnprm  12522  pockthlem  12525  pockthg  12526  prmunb  12531  mul4sqlem  12562  4sqlem11  12570  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  2expltfac  12608  znf1o  14207  dvply1  15001  logbgcd1irraplemexp  15204  wilthlem1  15216  mpodvdsmulf1o  15226  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgslem1  15241  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsvalmod  15260  lgsmod  15267  lgsdirprm  15275  lgsne0  15279  gausslemma2dlem0b  15291  gausslemma2dlem0c  15292  gausslemma2dlem1  15302  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem2  15319  lgsquadlem3  15320  m1lgs  15326  2lgslem1a  15329  2sqlem3  15358  cvgcmp2nlemabs  15676  trilpolemlt1  15685  redcwlpolemeq1  15698  nconstwlpolem0  15707