Theorem nnnn0d 9553

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℕcn 9237  ℕ₀cn0 9496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-n0 9497

This theorem is referenced by:  nn0ge2m1nn0  9561  nnzd  9699  eluzge2nn0  9902  modsumfzodifsn  10758  addmodlteq  10760  expnnval  10904  expgt1  10939  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  expnbnd  11025  facwordi  11102  faclbnd  11103  facavg  11108  bcm1k  11122  bcval5  11125  bcm1n  11131  1elfz0hash  11171  pfxfvlsw  11387  wrdeqs1cat  11412  resqrexlemnm  11703  resqrexlemcvg  11704  summodc  12069  zsumdc  12070  bcxmas  12175  geo2sum  12200  geo2lim  12202  geoisum1  12205  geoisum1c  12206  cvgratnnlembern  12209  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  mertenslemi1  12221  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  eftabs  12342  efcllemp  12344  eftlub  12376  eirraplem  12463  dvdsfac  12546  divalglemnqt  12606  divalglemeunn  12607  bitsfzo  12641  bitsfi  12643  gcdval  12655  gcdcl  12662  dvdsgcdidd  12690  mulgcd  12712  rplpwr  12723  rppwr  12724  lcmcl  12769  lcmgcdnn  12779  nprmdvds1  12837  isprm5lem  12838  rpexp  12850  pw2dvdslemn  12862  sqpweven  12872  2sqpwodd  12873  nn0sqrtelqelz  12903  phiprmpw  12919  crth  12921  eulerthlema  12927  eulerthlemth  12929  eulerth  12930  fermltl  12931  odzcllem  12940  odzdvds  12943  odzphi  12944  modprm0  12952  prm23lt5  12961  pythagtriplem6  12968  pythagtriplem7  12969  pcprmpw2  13031  dvdsprmpweqle  13035  pcprod  13044  pcfac  13048  pcbc  13049  expnprm  13051  pockthlem  13054  pockthg  13055  prmunb  13060  mul4sqlem  13091  4sqlem11  13099  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  2expltfac  13137  znf1o  14799  dvply1  15630  logbgcd1irraplemexp  15833  pellexlem2  15846  wilthlem1  15848  mpodvdsmulf1o  15858  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsvalmod  15892  lgsmod  15899  lgsdirprm  15907  lgsne0  15911  gausslemma2dlem0b  15923  gausslemma2dlem0c  15924  gausslemma2dlem1  15934  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem2  15951  lgsquadlem3  15952  m1lgs  15958  2lgslem1a  15961  2sqlem3  15990  isclwwlkn  16408  clwwlknccat  16418  clwwlknon  16424  depindlem1  16501  cvgcmp2nlemabs  16816  trilpolemlt1  16825  redcwlpolemeq1  16839  nconstwlpolem0  16849