Theorem nnnn0d 9454

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9142  ℕ₀cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-n0 9402

This theorem is referenced by:  nn0ge2m1nn0  9462  nnzd  9600  eluzge2nn0  9803  modsumfzodifsn  10657  addmodlteq  10659  expnnval  10803  expgt1  10838  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  expnbnd  10924  facwordi  11001  faclbnd  11002  facavg  11007  bcm1k  11021  bcval5  11024  1elfz0hash  11069  pfxfvlsw  11275  wrdeqs1cat  11300  resqrexlemnm  11578  resqrexlemcvg  11579  summodc  11943  zsumdc  11944  bcxmas  12049  geo2sum  12074  geo2lim  12076  geoisum1  12079  geoisum1c  12080  cvgratnnlembern  12083  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  mertenslemi1  12095  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  eftabs  12216  efcllemp  12218  eftlub  12250  eirraplem  12337  dvdsfac  12420  divalglemnqt  12480  divalglemeunn  12481  bitsfzo  12515  bitsfi  12517  gcdval  12529  gcdcl  12536  dvdsgcdidd  12564  mulgcd  12586  rplpwr  12597  rppwr  12598  lcmcl  12643  lcmgcdnn  12653  nprmdvds1  12711  isprm5lem  12712  rpexp  12724  pw2dvdslemn  12736  sqpweven  12746  2sqpwodd  12747  nn0sqrtelqelz  12777  phiprmpw  12793  crth  12795  eulerthlema  12801  eulerthlemth  12803  eulerth  12804  fermltl  12805  odzcllem  12814  odzdvds  12817  odzphi  12818  modprm0  12826  prm23lt5  12835  pythagtriplem6  12842  pythagtriplem7  12843  pcprmpw2  12905  dvdsprmpweqle  12909  pcprod  12918  pcfac  12922  pcbc  12923  expnprm  12925  pockthlem  12928  pockthg  12929  prmunb  12934  mul4sqlem  12965  4sqlem11  12973  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  2expltfac  13011  znf1o  14664  dvply1  15488  logbgcd1irraplemexp  15691  wilthlem1  15703  mpodvdsmulf1o  15713  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgslem1  15728  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsvalmod  15747  lgsmod  15754  lgsdirprm  15762  lgsne0  15766  gausslemma2dlem0b  15778  gausslemma2dlem0c  15779  gausslemma2dlem1  15789  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem2  15806  lgsquadlem3  15807  m1lgs  15813  2lgslem1a  15816  2sqlem3  15845  isclwwlkn  16263  clwwlknccat  16273  clwwlknon  16279  cvgcmp2nlemabs  16636  trilpolemlt1  16645  redcwlpolemeq1  16658  nconstwlpolem0  16667