Theorem nnnn0d 9422

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 9372	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3222	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9110   NN0cn0 9369

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 9370

This theorem is referenced by:  nn0ge2m1nn0  9430  nnzd  9568  eluzge2nn0  9764  modsumfzodifsn  10618  addmodlteq  10620  expnnval  10764  expgt1  10799  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  expnbnd  10885  facwordi  10962  faclbnd  10963  facavg  10968  bcm1k  10982  bcval5  10985  1elfz0hash  11028  pfxfvlsw  11227  wrdeqs1cat  11252  resqrexlemnm  11529  resqrexlemcvg  11530  summodc  11894  zsumdc  11895  bcxmas  12000  geo2sum  12025  geo2lim  12027  geoisum1  12030  geoisum1c  12031  cvgratnnlembern  12034  cvgratnnlemsumlt  12039  cvgratnnlemfm  12040  mertenslemi1  12046  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  eftabs  12167  efcllemp  12169  eftlub  12201  eirraplem  12288  dvdsfac  12371  divalglemnqt  12431  divalglemeunn  12432  bitsfzo  12466  bitsfi  12468  gcdval  12480  gcdcl  12487  dvdsgcdidd  12515  mulgcd  12537  rplpwr  12548  rppwr  12549  lcmcl  12594  lcmgcdnn  12604  nprmdvds1  12662  isprm5lem  12663  rpexp  12675  pw2dvdslemn  12687  sqpweven  12697  2sqpwodd  12698  nn0sqrtelqelz  12728  phiprmpw  12744  crth  12746  eulerthlema  12752  eulerthlemth  12754  eulerth  12755  fermltl  12756  odzcllem  12765  odzdvds  12768  odzphi  12769  modprm0  12777  prm23lt5  12786  pythagtriplem6  12793  pythagtriplem7  12794  pcprmpw2  12856  dvdsprmpweqle  12860  pcprod  12869  pcfac  12873  pcbc  12874  expnprm  12876  pockthlem  12879  pockthg  12880  prmunb  12885  mul4sqlem  12916  4sqlem11  12924  4sqlem13m  12926  4sqlem14  12927  4sqlem17  12930  4sqlem18  12931  2expltfac  12962  znf1o  14615  dvply1  15439  logbgcd1irraplemexp  15642  wilthlem1  15654  mpodvdsmulf1o  15664  mersenne  15671  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgslem1  15679  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsvalmod  15698  lgsmod  15705  lgsdirprm  15713  lgsne0  15717  gausslemma2dlem0b  15729  gausslemma2dlem0c  15730  gausslemma2dlem1  15740  gausslemma2dlem7  15747  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem2  15757  lgsquadlem3  15758  m1lgs  15764  2lgslem1a  15767  2sqlem3  15796  cvgcmp2nlemabs  16400  trilpolemlt1  16409  redcwlpolemeq1  16422  nconstwlpolem0  16431