Theorem subdid 10102

Description: Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
mulm1d.1	|- ( ph -> A e. CC )
mulnegd.2	|- ( ph -> B e. CC )
subdid.3	|- ( ph -> C e. CC )

Assertion

Ref	Expression
subdid	|- ( ph -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )

Proof of Theorem subdid

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 |- ( ph -> A e. CC )
2		mulnegd.2	. 2 |- ( ph -> B e. CC )
3		subdid.3	. 2 |- ( ph -> C e. CC )
4		subdi 10080	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
5	1, 2, 3, 4	syl3anc 1276	1 |- ( ph -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898  (class class class)co 6315   CCcc 9563   x. cmul 9570   - cmin 9886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706  df-sub 9888

This theorem is referenced by:  recextlem1  10270  cru  10629  cju  10633  zneo  11047  qbtwnre  11521  lincmb01cmp  11804  iccf1o  11805  intfracq  12118  modlt  12139  moddi  12189  modsubdir  12190  subsq  12414  expmulnbnd  12436  crre  13226  remullem  13240  mulcn2  13708  iseraltlem3  13799  fsumparts  13915  geoserg  13973  mertens  13991  bpolydiflem  14156  bpoly4  14161  fsumcube  14162  tanval3  14237  tanadd  14270  eirrlem  14305  3dvds  14418  bezoutlem3OLD  14554  bezoutlem3  14557  eulerthlem2  14779  prmdiv  14782  prmdiveq  14783  4sqlem10  14940  mul4sqlem  14946  4sqlem17OLD  14954  4sqlem17  14960  blcvx  21865  icopnfhmeo  22020  pcoass  22104  pjthlem1  22440  itgmulc2lem2  22839  dvmulbr  22942  cmvth  22992  dvcvx  23021  dvfsumle  23022  dvfsumabs  23024  dvfsumlem2  23028  aaliou3lem8  23350  abelthlem2  23436  tangtx  23509  tanregt0  23537  efif1olem2  23541  efif1olem4  23543  ang180lem5  23791  isosctrlem2  23797  isosctrlem3  23798  affineequiv  23801  heron  23813  dcubic1  23820  dquart  23828  quartlem1  23832  asinsin  23867  efiatan  23887  atanlogsublem  23890  efiatan2  23892  2efiatan  23893  tanatan  23894  atantayl2  23913  lgamgulmlem2  24004  lgamgulmlem3  24005  wilthlem2  24043  ftalem5  24050  ftalem5OLD  24052  basellem3  24058  basellem5  24060  logfaclbnd  24199  bposlem1  24261  lgseisenlem2  24327  lgsquadlem1  24331  2sqlem4  24344  vmadivsum  24369  rplogsumlem1  24371  dchrmusum2  24381  dchrvmasumiflem2  24389  rpvmasum2  24399  dchrisum0lem2a  24404  dchrisum0lem2  24405  rplogsum  24414  mulogsumlem  24418  mulogsum  24419  mulog2sumlem1  24421  mulog2sumlem2  24422  mulog2sumlem3  24423  vmalogdivsum2  24425  vmalogdivsum  24426  2vmadivsumlem  24427  logsqvma  24429  selberglem1  24432  selberglem2  24433  selberg2lem  24437  chpdifbndlem1  24440  selberg3lem1  24444  selberg4lem1  24447  selberg4  24448  pntrsumo1  24452  selbergr  24455  selberg3r  24456  selberg4r  24457  selberg34r  24458  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntrlog2bndlem6  24470  pntlemo  24494  ttgcontlem1  24964  brbtwn2  24984  colinearalglem1  24985  axcontlem8  25050  pjhthlem1  27093  2sqmod  28458  muls1d  30417  bj-bary1lem  31760  bj-bary1lem1  31761  itgmulc2nclem2  32054  areacirclem1  32077  areacirclem4  32080  areacirc  32082  cntotbnd  32173  irrapxlem2  35712  irrapxlem3  35713  irrapxlem5  35715  pellexlem6  35723  pell1qrgaplem  35764  qirropth  35801  jm2.17a  35855  congmul  35862  jm2.18  35888  areaquad  36146  itgsinexp  37869  stoweidlem26  37924  stirlinglem7  37980  fourierdlem83  38091  etransclem46  38183