Theorem nnnn0d 9347

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℕcn 9035  ℕ₀cn0 9294

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-n0 9295

This theorem is referenced by:  nn0ge2m1nn0  9355  nnzd  9493  eluzge2nn0  9689  modsumfzodifsn  10539  addmodlteq  10541  expnnval  10685  expgt1  10720  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  expnbnd  10806  facwordi  10883  faclbnd  10884  facavg  10889  bcm1k  10903  bcval5  10906  1elfz0hash  10949  resqrexlemnm  11271  resqrexlemcvg  11272  summodc  11636  zsumdc  11637  bcxmas  11742  geo2sum  11767  geo2lim  11769  geoisum1  11772  geoisum1c  11773  cvgratnnlembern  11776  cvgratnnlemsumlt  11781  cvgratnnlemfm  11782  mertenslemi1  11788  prodmodclem3  11828  prodmodclem2a  11829  zproddc  11832  fprodseq  11836  eftabs  11909  efcllemp  11911  eftlub  11943  eirraplem  12030  dvdsfac  12113  divalglemnqt  12173  divalglemeunn  12174  bitsfzo  12208  bitsfi  12210  gcdval  12222  gcdcl  12229  dvdsgcdidd  12257  mulgcd  12279  rplpwr  12290  rppwr  12291  lcmcl  12336  lcmgcdnn  12346  nprmdvds1  12404  isprm5lem  12405  rpexp  12417  pw2dvdslemn  12429  sqpweven  12439  2sqpwodd  12440  nn0sqrtelqelz  12470  phiprmpw  12486  crth  12488  eulerthlema  12494  eulerthlemth  12496  eulerth  12497  fermltl  12498  odzcllem  12507  odzdvds  12510  odzphi  12511  modprm0  12519  prm23lt5  12528  pythagtriplem6  12535  pythagtriplem7  12536  pcprmpw2  12598  dvdsprmpweqle  12602  pcprod  12611  pcfac  12615  pcbc  12616  expnprm  12618  pockthlem  12621  pockthg  12622  prmunb  12627  mul4sqlem  12658  4sqlem11  12666  4sqlem13m  12668  4sqlem14  12669  4sqlem17  12672  4sqlem18  12673  2expltfac  12704  znf1o  14355  dvply1  15179  logbgcd1irraplemexp  15382  wilthlem1  15394  mpodvdsmulf1o  15404  mersenne  15411  perfect1  15412  perfectlem1  15413  perfectlem2  15414  perfect  15415  lgslem1  15419  lgsval  15423  lgsfvalg  15424  lgsval2lem  15429  lgsvalmod  15438  lgsmod  15445  lgsdirprm  15453  lgsne0  15457  gausslemma2dlem0b  15469  gausslemma2dlem0c  15470  gausslemma2dlem1  15480  gausslemma2dlem7  15487  gausslemma2d  15488  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisenlem4  15492  lgseisen  15493  lgsquadlem2  15497  lgsquadlem3  15498  m1lgs  15504  2lgslem1a  15507  2sqlem3  15536  cvgcmp2nlemabs  15904  trilpolemlt1  15913  redcwlpolemeq1  15926  nconstwlpolem0  15935