Theorem subdid 11671

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11444

This theorem is referenced by:  muls1d  11675  addmulsub  11677  recextlem1  11845  cru  12211  cju  12215  zneo  12680  qbtwnre  13226  lincmb01cmp  13523  iccf1o  13524  intfracq  13894  modlt  13915  moddi  13977  modsubdir  13978  subsq  14248  expmulnbnd  14273  crre  15167  remullem  15181  mulcn2  15649  iseraltlem3  15737  fsumparts  15860  geoserg  15922  mertens  15942  bpolydiflem  16109  bpoly4  16114  fsumcube  16115  tanval3  16191  tanadd  16224  eirrlem  16261  bezoutlem3  16600  cncongr1  16726  eulerthlem2  16842  prmdiv  16845  prmdiveq  16846  4sqlem10  17008  mul4sqlem  17014  4sqlem17  17022  blcvx  24936  icopnfhmeo  25083  pcoass  25164  cphipval  25383  pjthlem1  25577  itgmulc2lem2  25973  dvmulbr  26079  cmvth  26131  dvcvx  26160  dvfsumle  26161  dvfsumabs  26163  dvfsumlem2  26167  aaliou3lem8  26487  abelthlem2  26573  tangtx  26648  tanregt0  26682  efif1olem2  26686  efif1olem4  26688  ang180lem5  26956  isosctrlem2  26962  isosctrlem3  26963  affineequiv  26966  heron  26981  dcubic1  26988  dquart  26996  quartlem1  27000  asinsin  27035  efiatan  27055  atanlogsublem  27058  efiatan2  27060  2efiatan  27061  tanatan  27062  atantayl2  27081  lgamgulmlem2  27172  lgamgulmlem3  27173  ftalem5  27219  basellem3  27225  basellem5  27227  logfaclbnd  27364  lgseisenlem2  27518  lgsquadlem1  27522  2sqlem4  27563  2sqmod  27578  vmadivsum  27624  rplogsumlem1  27626  dchrmusum2  27636  dchrvmasumiflem2  27644  rpvmasum2  27654  dchrisum0lem2a  27659  dchrisum0lem2  27660  rplogsum  27669  mulogsumlem  27673  mulogsum  27674  mulog2sumlem1  27676  mulog2sumlem2  27677  mulog2sumlem3  27678  vmalogdivsum2  27680  vmalogdivsum  27681  2vmadivsumlem  27682  logsqvma  27684  selberglem1  27687  selberglem2  27688  selberg2lem  27692  chpdifbndlem1  27695  selberg3lem1  27699  selberg4lem1  27702  selberg4  27703  pntrsumo1  27707  selbergr  27710  selberg3r  27711  selberg4r  27712  selberg34r  27713  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntrlog2bndlem6  27725  pntlemo  27749  ttgcontlem1  29212  brbtwn2  29233  colinearalglem1  29234  axcontlem8  29299  pjhthlem1  31721  constrrtll  34099  constrrtlc1  34100  constrrtcclem  34102  constrremulcl  34135  constrrecl  34137  constrreinvcl  34140  cos9thpiminplylem1  34150  cos9thpiminplylem2  34151  knoppndvlem11  37089  knoppndvlem14  37092  knoppndvlem15  37093  knoppndvlem16  37094  bj-bary1lem  37932  bj-bary1lem1  37933  qdiff  37949  itgmulc2nclem2  38316  areacirclem1  38337  areacirclem4  38340  areacirc  38342  cntotbnd  38425  posbezout  42845  hashscontpow1  42866  nicomachus  43051  irrapxlem2  43530  irrapxlem3  43531  irrapxlem5  43533  pellexlem6  43541  pell1qrgaplem  43580  qirropth  43615  jm2.17a  43667  congmul  43674  jm2.18  43695  areaquad  43923  itgsinexp  46649  stoweidlem26  46720  stirlinglem7  46774  fourierdlem83  46883  etransclem46  46974  smfmullem1  47485  sin3t  47585  cos3t  47586  sin5tlem4  47590  cos5t  47593  fmtnorec3  48277  fmtnorec4  48278  fppr2odd  48473  itcovalt2lem2lem2  49431  submuladdmuld  49458  affinecomb2  49460  itsclc0yqsollem1  49519  itsclc0yqsol  49521  itscnhlc0xyqsol  49522  itsclc0xyqsolr  49526  2itscplem3  49537  itscnhlinecirc02plem1  49539