Theorem nnnn0d 9445

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9133  ℕ₀cn0 9392

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-n0 9393

This theorem is referenced by:  nn0ge2m1nn0  9453  nnzd  9591  eluzge2nn0  9794  modsumfzodifsn  10648  addmodlteq  10650  expnnval  10794  expgt1  10829  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  expnbnd  10915  facwordi  10992  faclbnd  10993  facavg  10998  bcm1k  11012  bcval5  11015  1elfz0hash  11060  pfxfvlsw  11266  wrdeqs1cat  11291  resqrexlemnm  11569  resqrexlemcvg  11570  summodc  11934  zsumdc  11935  bcxmas  12040  geo2sum  12065  geo2lim  12067  geoisum1  12070  geoisum1c  12071  cvgratnnlembern  12074  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  mertenslemi1  12086  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  eftabs  12207  efcllemp  12209  eftlub  12241  eirraplem  12328  dvdsfac  12411  divalglemnqt  12471  divalglemeunn  12472  bitsfzo  12506  bitsfi  12508  gcdval  12520  gcdcl  12527  dvdsgcdidd  12555  mulgcd  12577  rplpwr  12588  rppwr  12589  lcmcl  12634  lcmgcdnn  12644  nprmdvds1  12702  isprm5lem  12703  rpexp  12715  pw2dvdslemn  12727  sqpweven  12737  2sqpwodd  12738  nn0sqrtelqelz  12768  phiprmpw  12784  crth  12786  eulerthlema  12792  eulerthlemth  12794  eulerth  12795  fermltl  12796  odzcllem  12805  odzdvds  12808  odzphi  12809  modprm0  12817  prm23lt5  12826  pythagtriplem6  12833  pythagtriplem7  12834  pcprmpw2  12896  dvdsprmpweqle  12900  pcprod  12909  pcfac  12913  pcbc  12914  expnprm  12916  pockthlem  12919  pockthg  12920  prmunb  12925  mul4sqlem  12956  4sqlem11  12964  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  2expltfac  13002  znf1o  14655  dvply1  15479  logbgcd1irraplemexp  15682  wilthlem1  15694  mpodvdsmulf1o  15704  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsvalmod  15738  lgsmod  15745  lgsdirprm  15753  lgsne0  15757  gausslemma2dlem0b  15769  gausslemma2dlem0c  15770  gausslemma2dlem1  15780  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem2  15797  lgsquadlem3  15798  m1lgs  15804  2lgslem1a  15807  2sqlem3  15836  isclwwlkn  16208  clwwlknccat  16218  clwwlknon  16224  cvgcmp2nlemabs  16572  trilpolemlt1  16581  redcwlpolemeq1  16594  nconstwlpolem0  16603