Theorem subdid 11674

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	⊢ (𝜑 → 𝐴 ∈ ℂ)
mulnegd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
subdid.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
subdid	⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))

Proof of Theorem subdid

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subdid.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		subdi 11651	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1369	1 ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117   − cmin 11448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450

This theorem is referenced by:  muls1d  11678  addmulsub  11680  recextlem1  11848  cru  12208  cju  12212  zneo  12649  qbtwnre  13182  lincmb01cmp  13476  iccf1o  13477  intfracq  13828  modlt  13849  moddi  13908  modsubdir  13909  subsq  14178  expmulnbnd  14202  crre  15065  remullem  15079  mulcn2  15544  iseraltlem3  15634  fsumparts  15756  geoserg  15816  mertens  15836  bpolydiflem  16002  bpoly4  16007  fsumcube  16008  tanval3  16081  tanadd  16114  eirrlem  16151  bezoutlem3  16487  cncongr1  16608  eulerthlem2  16719  prmdiv  16722  prmdiveq  16723  4sqlem10  16884  mul4sqlem  16890  4sqlem17  16898  blcvx  24534  icopnfhmeo  24688  pcoass  24771  cphipval  24991  pjthlem1  25185  itgmulc2lem2  25582  dvmulbr  25689  dvmulbrOLD  25690  cmvth  25743  dvcvx  25772  dvfsumle  25773  dvfsumabs  25775  dvfsumlem2  25779  aaliou3lem8  26094  abelthlem2  26180  tangtx  26251  tanregt0  26284  efif1olem2  26288  efif1olem4  26290  ang180lem5  26554  isosctrlem2  26560  isosctrlem3  26561  affineequiv  26564  heron  26579  dcubic1  26586  dquart  26594  quartlem1  26598  asinsin  26633  efiatan  26653  atanlogsublem  26656  efiatan2  26658  2efiatan  26659  tanatan  26660  atantayl2  26679  lgamgulmlem2  26770  lgamgulmlem3  26771  ftalem5  26817  basellem3  26823  basellem5  26825  logfaclbnd  26961  lgseisenlem2  27115  lgsquadlem1  27119  2sqlem4  27160  2sqmod  27175  vmadivsum  27221  rplogsumlem1  27223  dchrmusum2  27233  dchrvmasumiflem2  27241  rpvmasum2  27251  dchrisum0lem2a  27256  dchrisum0lem2  27257  rplogsum  27266  mulogsumlem  27270  mulogsum  27271  mulog2sumlem1  27273  mulog2sumlem2  27274  mulog2sumlem3  27275  vmalogdivsum2  27277  vmalogdivsum  27278  2vmadivsumlem  27279  logsqvma  27281  selberglem1  27284  selberglem2  27285  selberg2lem  27289  chpdifbndlem1  27292  selberg3lem1  27296  selberg4lem1  27299  selberg4  27300  pntrsumo1  27304  selbergr  27307  selberg3r  27308  selberg4r  27309  selberg34r  27310  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntlemo  27346  ttgcontlem1  28409  brbtwn2  28430  colinearalglem1  28431  axcontlem8  28496  pjhthlem1  30911  gg-cmvth  35466  gg-dvfsumle  35468  gg-dvfsumlem2  35469  knoppndvlem11  35701  knoppndvlem14  35704  knoppndvlem15  35705  knoppndvlem16  35706  bj-bary1lem  36494  bj-bary1lem1  36495  itgmulc2nclem2  36858  areacirclem1  36879  areacirclem4  36882  areacirc  36884  cntotbnd  36967  nicomachus  41512  irrapxlem2  41863  irrapxlem3  41864  irrapxlem5  41866  pellexlem6  41874  pell1qrgaplem  41913  qirropth  41948  jm2.17a  42001  congmul  42008  jm2.18  42029  areaquad  42267  itgsinexp  44969  stoweidlem26  45040  stirlinglem7  45094  fourierdlem83  45203  etransclem46  45294  smfmullem1  45805  fmtnorec3  46514  fmtnorec4  46515  fppr2odd  46697  itcovalt2lem2lem2  47447  submuladdmuld  47474  affinecomb2  47476  itsclc0yqsollem1  47535  itsclc0yqsol  47537  itscnhlc0xyqsol  47538  itsclc0xyqsolr  47542  2itscplem3  47553  itscnhlinecirc02plem1  47555