Theorem subdid 11593

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 11570	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031   − cmin 11364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366

This theorem is referenced by:  muls1d  11597  addmulsub  11599  recextlem1  11767  cru  12137  cju  12141  zneo  12575  qbtwnre  13114  lincmb01cmp  13411  iccf1o  13412  intfracq  13779  modlt  13800  moddi  13862  modsubdir  13863  subsq  14133  expmulnbnd  14158  crre  15037  remullem  15051  mulcn2  15519  iseraltlem3  15607  fsumparts  15729  geoserg  15789  mertens  15809  bpolydiflem  15977  bpoly4  15982  fsumcube  15983  tanval3  16059  tanadd  16092  eirrlem  16129  bezoutlem3  16468  cncongr1  16594  eulerthlem2  16709  prmdiv  16712  prmdiveq  16713  4sqlem10  16875  mul4sqlem  16881  4sqlem17  16889  blcvx  24742  icopnfhmeo  24897  pcoass  24980  cphipval  25199  pjthlem1  25393  itgmulc2lem2  25790  dvmulbr  25897  dvmulbrOLD  25898  cmvth  25951  cmvthOLD  25952  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  aaliou3lem8  26309  abelthlem2  26398  tangtx  26470  tanregt0  26504  efif1olem2  26508  efif1olem4  26510  ang180lem5  26779  isosctrlem2  26785  isosctrlem3  26786  affineequiv  26789  heron  26804  dcubic1  26811  dquart  26819  quartlem1  26823  asinsin  26858  efiatan  26878  atanlogsublem  26881  efiatan2  26883  2efiatan  26884  tanatan  26885  atantayl2  26904  lgamgulmlem2  26996  lgamgulmlem3  26997  ftalem5  27043  basellem3  27049  basellem5  27051  logfaclbnd  27189  lgseisenlem2  27343  lgsquadlem1  27347  2sqlem4  27388  2sqmod  27403  vmadivsum  27449  rplogsumlem1  27451  dchrmusum2  27461  dchrvmasumiflem2  27469  rpvmasum2  27479  dchrisum0lem2a  27484  dchrisum0lem2  27485  rplogsum  27494  mulogsumlem  27498  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  logsqvma  27509  selberglem1  27512  selberglem2  27513  selberg2lem  27517  chpdifbndlem1  27520  selberg3lem1  27524  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  selbergr  27535  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntlemo  27574  ttgcontlem1  28957  brbtwn2  28978  colinearalglem1  28979  axcontlem8  29044  pjhthlem1  31466  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrremulcl  33924  constrrecl  33926  constrreinvcl  33929  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem16  36727  bj-bary1lem  37511  bj-bary1lem1  37512  itgmulc2nclem2  37884  areacirclem1  37905  areacirclem4  37908  areacirc  37910  cntotbnd  37993  posbezout  42350  hashscontpow1  42371  nicomachus  42563  irrapxlem2  43061  irrapxlem3  43062  irrapxlem5  43064  pellexlem6  43072  pell1qrgaplem  43111  qirropth  43146  jm2.17a  43198  congmul  43205  jm2.18  43226  areaquad  43454  itgsinexp  46195  stoweidlem26  46266  stirlinglem7  46320  fourierdlem83  46429  etransclem46  46520  smfmullem1  47031  fmtnorec3  47790  fmtnorec4  47791  fppr2odd  47973  itcovalt2lem2lem2  48916  submuladdmuld  48943  affinecomb2  48945  itsclc0yqsollem1  49004  itsclc0yqsol  49006  itscnhlc0xyqsol  49007  itsclc0xyqsolr  49011  2itscplem3  49022  itscnhlinecirc02plem1  49024