Theorem subdid 10944

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  (class class class)co 7016  ℂcc 10381   · cmul 10388   − cmin 10717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-po 5362  df-so 5363  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-ltxr 10526  df-sub 10719

This theorem is referenced by:  muls1d  10948  addmulsub  10950  recextlem1  11118  cru  11478  cju  11482  zneo  11914  qbtwnre  12442  lincmb01cmp  12731  iccf1o  12732  intfracq  13077  modlt  13098  moddi  13157  modsubdir  13158  subsq  13422  expmulnbnd  13446  crre  14307  remullem  14321  mulcn2  14786  iseraltlem3  14874  fsumparts  14994  geoserg  15054  mertens  15075  bpolydiflem  15241  bpoly4  15246  fsumcube  15247  tanval3  15320  tanadd  15353  eirrlem  15390  bezoutlem3  15718  cncongr1  15840  eulerthlem2  15948  prmdiv  15951  prmdiveq  15952  4sqlem10  16112  mul4sqlem  16118  4sqlem17  16126  blcvx  23089  icopnfhmeo  23230  pcoass  23311  cphipval  23529  pjthlem1  23723  itgmulc2lem2  24116  dvmulbr  24219  cmvth  24271  dvcvx  24300  dvfsumle  24301  dvfsumabs  24303  dvfsumlem2  24307  aaliou3lem8  24617  abelthlem2  24703  tangtx  24774  tanregt0  24804  efif1olem2  24808  efif1olem4  24810  ang180lem5  25072  isosctrlem2  25078  isosctrlem3  25079  affineequiv  25082  heron  25097  dcubic1  25104  dquart  25112  quartlem1  25116  asinsin  25151  efiatan  25171  atanlogsublem  25174  efiatan2  25176  2efiatan  25177  tanatan  25178  atantayl2  25197  lgamgulmlem2  25289  lgamgulmlem3  25290  ftalem5  25336  basellem3  25342  basellem5  25344  logfaclbnd  25480  lgseisenlem2  25634  lgsquadlem1  25638  2sqlem4  25679  2sqmod  25694  vmadivsum  25740  rplogsumlem1  25742  dchrmusum2  25752  dchrvmasumiflem2  25760  rpvmasum2  25770  dchrisum0lem2a  25775  dchrisum0lem2  25776  rplogsum  25785  mulogsumlem  25789  mulogsum  25790  mulog2sumlem1  25792  mulog2sumlem2  25793  mulog2sumlem3  25794  vmalogdivsum2  25796  vmalogdivsum  25797  2vmadivsumlem  25798  logsqvma  25800  selberglem1  25803  selberglem2  25804  selberg2lem  25808  chpdifbndlem1  25811  selberg3lem1  25815  selberg4lem1  25818  selberg4  25819  pntrsumo1  25823  selbergr  25826  selberg3r  25827  selberg4r  25828  selberg34r  25829  pntrlog2bndlem4  25838  pntrlog2bndlem5  25839  pntrlog2bndlem6  25841  pntlemo  25865  ttgcontlem1  26354  brbtwn2  26374  colinearalglem1  26375  axcontlem8  26440  pjhthlem1  28859  knoppndvlem11  33471  knoppndvlem14  33474  knoppndvlem15  33475  knoppndvlem16  33476  bj-bary1lem  34147  bj-bary1lem1  34148  itgmulc2nclem2  34509  areacirclem1  34532  areacirclem4  34535  areacirc  34537  cntotbnd  34625  irrapxlem2  38924  irrapxlem3  38925  irrapxlem5  38927  pellexlem6  38935  pell1qrgaplem  38974  qirropth  39009  jm2.17a  39061  congmul  39068  jm2.18  39089  areaquad  39327  itgsinexp  41801  stoweidlem26  41873  stirlinglem7  41927  fourierdlem83  42036  etransclem46  42127  smfmullem1  42628  fmtnorec3  43212  fmtnorec4  43213  fppr2odd  43398  submuladdmuld  44189  affinecomb2  44191  itsclc0yqsollem1  44250  itsclc0yqsol  44252  itscnhlc0xyqsol  44253  itsclc0xyqsolr  44257  2itscplem3  44268  itscnhlinecirc02plem1  44270