MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subdid Unicode version

Theorem subdid 9322
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
StepHypRef 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 9300 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  -  C ) )  =  ( ( A  x.  B )  -  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( A  x.  ( B  -  C )
)  =  ( ( A  x.  B )  -  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710  (class class class)co 5942   CCcc 8822    x. cmul 8829    - cmin 9124
This theorem is referenced by:  recextlem1  9485  cru  9825  cju  9829  zneo  10183  qbtwnre  10615  lincmb01cmp  10866  iccf1o  10867  intfracq  11052  modlt  11070  moddi  11096  modsubdir  11097  subsq  11300  expmulnbnd  11323  crre  11689  remullem  11703  mulcn2  12159  iseraltlem3  12247  fsumparts  12355  geoserg  12415  mertens  12433  tanval3  12505  tanadd  12538  eirrlem  12573  3dvds  12682  bezoutlem3  12810  eulerthlem2  12941  prmdiv  12944  prmdiveq  12945  4sqlem10  13085  mul4sqlem  13091  4sqlem17  13099  blcvx  18400  icopnfhmeo  18539  pcoass  18620  pjthlem1  18899  itgmulc2lem2  19285  dvmulbr  19386  cmvth  19436  dvcvx  19465  dvfsumle  19466  dvfsumabs  19468  dvfsumlem2  19472  aaliou3lem8  19823  abelthlem2  19909  tangtx  19974  tanregt0  20002  efif1olem2  20006  efif1olem4  20008  ang180lem5  20216  isosctrlem2  20224  isosctrlem3  20225  affineequiv  20228  dcubic1  20246  dquart  20254  quartlem1  20258  asinsin  20293  efiatan  20313  atanlogsublem  20316  efiatan2  20318  2efiatan  20319  tanatan  20320  atantayl2  20339  wilthlem2  20413  ftalem5  20420  basellem3  20426  basellem5  20428  logfaclbnd  20567  bposlem1  20629  lgseisenlem2  20695  lgsquadlem1  20699  2sqlem4  20712  vmadivsum  20737  rplogsumlem1  20739  dchrmusum2  20749  dchrvmasumiflem2  20757  rpvmasum2  20767  dchrisum0lem2a  20772  dchrisum0lem2  20773  rplogsum  20782  mulogsumlem  20786  mulogsum  20787  mulog2sumlem1  20789  mulog2sumlem2  20790  mulog2sumlem3  20791  vmalogdivsum2  20793  vmalogdivsum  20794  2vmadivsumlem  20795  logsqvma  20797  selberglem1  20800  selberglem2  20801  selberg2lem  20805  chpdifbndlem1  20808  selberg3lem1  20812  selberg4lem1  20815  selberg4  20816  pntrsumo1  20820  selbergr  20823  selberg3r  20824  selberg4r  20825  selberg34r  20826  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  pntrlog2bndlem6  20838  pntlemo  20862  pjhthlem1  22078  lgamgulmlem2  24063  lgamgulmlem3  24064  muls1d  24514  brbtwn2  25092  colinearalglem1  25093  axcontlem8  25158  bpolydiflem  25348  bpoly4  25353  itgmulc2nclem2  25507  areacirclem2  25517  areacirclem5  25521  areacirc  25523  cntotbnd  25843  irrapxlem2  26231  irrapxlem3  26232  irrapxlem5  26234  pellexlem6  26242  pell1qrgaplem  26281  qirropth  26316  jm2.17a  26370  congmul  26377  jm2.18  26404  itgsinexp  27072  stirlinglem7  27152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-po 4393  df-so 4394  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-riota 6388  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-ltxr 8959  df-sub 9126
  Copyright terms: Public domain W3C validator