Theorem nnnn0d 9383

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnnn0d	|- ( ph -> A e. NN0 )

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 9333	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3199	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2178   NNcn 9071   NN0cn0 9330

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-n0 9331

This theorem is referenced by:  nn0ge2m1nn0  9391  nnzd  9529  eluzge2nn0  9725  modsumfzodifsn  10578  addmodlteq  10580  expnnval  10724  expgt1  10759  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  expnbnd  10845  facwordi  10922  faclbnd  10923  facavg  10928  bcm1k  10942  bcval5  10945  1elfz0hash  10988  pfxfvlsw  11186  wrdeqs1cat  11211  resqrexlemnm  11444  resqrexlemcvg  11445  summodc  11809  zsumdc  11810  bcxmas  11915  geo2sum  11940  geo2lim  11942  geoisum1  11945  geoisum1c  11946  cvgratnnlembern  11949  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  mertenslemi1  11961  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  eftabs  12082  efcllemp  12084  eftlub  12116  eirraplem  12203  dvdsfac  12286  divalglemnqt  12346  divalglemeunn  12347  bitsfzo  12381  bitsfi  12383  gcdval  12395  gcdcl  12402  dvdsgcdidd  12430  mulgcd  12452  rplpwr  12463  rppwr  12464  lcmcl  12509  lcmgcdnn  12519  nprmdvds1  12577  isprm5lem  12578  rpexp  12590  pw2dvdslemn  12602  sqpweven  12612  2sqpwodd  12613  nn0sqrtelqelz  12643  phiprmpw  12659  crth  12661  eulerthlema  12667  eulerthlemth  12669  eulerth  12670  fermltl  12671  odzcllem  12680  odzdvds  12683  odzphi  12684  modprm0  12692  prm23lt5  12701  pythagtriplem6  12708  pythagtriplem7  12709  pcprmpw2  12771  dvdsprmpweqle  12775  pcprod  12784  pcfac  12788  pcbc  12789  expnprm  12791  pockthlem  12794  pockthg  12795  prmunb  12800  mul4sqlem  12831  4sqlem11  12839  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  2expltfac  12877  znf1o  14528  dvply1  15352  logbgcd1irraplemexp  15555  wilthlem1  15567  mpodvdsmulf1o  15577  mersenne  15584  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgslem1  15592  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsvalmod  15611  lgsmod  15618  lgsdirprm  15626  lgsne0  15630  gausslemma2dlem0b  15642  gausslemma2dlem0c  15643  gausslemma2dlem1  15653  gausslemma2dlem7  15660  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem2  15670  lgsquadlem3  15671  m1lgs  15677  2lgslem1a  15680  2sqlem3  15709  cvgcmp2nlemabs  16173  trilpolemlt1  16182  redcwlpolemeq1  16195  nconstwlpolem0  16204