Theorem nnnn0d 9433

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9121  ℕ₀cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9381

This theorem is referenced by:  nn0ge2m1nn0  9441  nnzd  9579  eluzge2nn0  9776  modsumfzodifsn  10630  addmodlteq  10632  expnnval  10776  expgt1  10811  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  expnbnd  10897  facwordi  10974  faclbnd  10975  facavg  10980  bcm1k  10994  bcval5  10997  1elfz0hash  11041  pfxfvlsw  11242  wrdeqs1cat  11267  resqrexlemnm  11544  resqrexlemcvg  11545  summodc  11909  zsumdc  11910  bcxmas  12015  geo2sum  12040  geo2lim  12042  geoisum1  12045  geoisum1c  12046  cvgratnnlembern  12049  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  mertenslemi1  12061  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  eftabs  12182  efcllemp  12184  eftlub  12216  eirraplem  12303  dvdsfac  12386  divalglemnqt  12446  divalglemeunn  12447  bitsfzo  12481  bitsfi  12483  gcdval  12495  gcdcl  12502  dvdsgcdidd  12530  mulgcd  12552  rplpwr  12563  rppwr  12564  lcmcl  12609  lcmgcdnn  12619  nprmdvds1  12677  isprm5lem  12678  rpexp  12690  pw2dvdslemn  12702  sqpweven  12712  2sqpwodd  12713  nn0sqrtelqelz  12743  phiprmpw  12759  crth  12761  eulerthlema  12767  eulerthlemth  12769  eulerth  12770  fermltl  12771  odzcllem  12780  odzdvds  12783  odzphi  12784  modprm0  12792  prm23lt5  12801  pythagtriplem6  12808  pythagtriplem7  12809  pcprmpw2  12871  dvdsprmpweqle  12875  pcprod  12884  pcfac  12888  pcbc  12889  expnprm  12891  pockthlem  12894  pockthg  12895  prmunb  12900  mul4sqlem  12931  4sqlem11  12939  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  4sqlem18  12946  2expltfac  12977  znf1o  14630  dvply1  15454  logbgcd1irraplemexp  15657  wilthlem1  15669  mpodvdsmulf1o  15679  mersenne  15686  perfect1  15687  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgslem1  15694  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsvalmod  15713  lgsmod  15720  lgsdirprm  15728  lgsne0  15732  gausslemma2dlem0b  15744  gausslemma2dlem0c  15745  gausslemma2dlem1  15755  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem2  15772  lgsquadlem3  15773  m1lgs  15779  2lgslem1a  15782  2sqlem3  15811  cvgcmp2nlemabs  16460  trilpolemlt1  16469  redcwlpolemeq1  16482  nconstwlpolem0  16491