Theorem subdid 11576

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   · cmul 11014   − cmin 11347

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349

This theorem is referenced by:  muls1d  11580  addmulsub  11582  recextlem1  11750  cru  12120  cju  12124  zneo  12559  qbtwnre  13101  lincmb01cmp  13398  iccf1o  13399  intfracq  13763  modlt  13784  moddi  13846  modsubdir  13847  subsq  14117  expmulnbnd  14142  crre  15021  remullem  15035  mulcn2  15503  iseraltlem3  15591  fsumparts  15713  geoserg  15773  mertens  15793  bpolydiflem  15961  bpoly4  15966  fsumcube  15967  tanval3  16043  tanadd  16076  eirrlem  16113  bezoutlem3  16452  cncongr1  16578  eulerthlem2  16693  prmdiv  16696  prmdiveq  16697  4sqlem10  16859  mul4sqlem  16865  4sqlem17  16873  blcvx  24684  icopnfhmeo  24839  pcoass  24922  cphipval  25141  pjthlem1  25335  itgmulc2lem2  25732  dvmulbr  25839  dvmulbrOLD  25840  cmvth  25893  cmvthOLD  25894  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  aaliou3lem8  26251  abelthlem2  26340  tangtx  26412  tanregt0  26446  efif1olem2  26450  efif1olem4  26452  ang180lem5  26721  isosctrlem2  26727  isosctrlem3  26728  affineequiv  26731  heron  26746  dcubic1  26753  dquart  26761  quartlem1  26765  asinsin  26800  efiatan  26820  atanlogsublem  26823  efiatan2  26825  2efiatan  26826  tanatan  26827  atantayl2  26846  lgamgulmlem2  26938  lgamgulmlem3  26939  ftalem5  26985  basellem3  26991  basellem5  26993  logfaclbnd  27131  lgseisenlem2  27285  lgsquadlem1  27289  2sqlem4  27330  2sqmod  27345  vmadivsum  27391  rplogsumlem1  27393  dchrmusum2  27403  dchrvmasumiflem2  27411  rpvmasum2  27421  dchrisum0lem2a  27426  dchrisum0lem2  27427  rplogsum  27436  mulogsumlem  27440  mulogsum  27441  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  logsqvma  27451  selberglem1  27454  selberglem2  27455  selberg2lem  27459  chpdifbndlem1  27462  selberg3lem1  27466  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  selbergr  27477  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntlemo  27516  ttgcontlem1  28830  brbtwn2  28850  colinearalglem1  28851  axcontlem8  28916  pjhthlem1  31335  constrrtll  33698  constrrtlc1  33699  constrrtcclem  33701  constrremulcl  33734  constrrecl  33736  constrreinvcl  33739  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  knoppndvlem11  36500  knoppndvlem14  36503  knoppndvlem15  36504  knoppndvlem16  36505  bj-bary1lem  37288  bj-bary1lem1  37289  itgmulc2nclem2  37671  areacirclem1  37692  areacirclem4  37695  areacirc  37697  cntotbnd  37780  posbezout  42077  hashscontpow1  42098  nicomachus  42289  irrapxlem2  42800  irrapxlem3  42801  irrapxlem5  42803  pellexlem6  42811  pell1qrgaplem  42850  qirropth  42885  jm2.17a  42937  congmul  42944  jm2.18  42965  areaquad  43193  itgsinexp  45940  stoweidlem26  46011  stirlinglem7  46065  fourierdlem83  46174  etransclem46  46265  smfmullem1  46776  fmtnorec3  47536  fmtnorec4  47537  fppr2odd  47719  itcovalt2lem2lem2  48663  submuladdmuld  48690  affinecomb2  48692  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  2itscplem3  48769  itscnhlinecirc02plem1  48771