Theorem subdid 11148

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  (class class class)co 7157  ℂcc 10587   · cmul 10594   − cmin 10922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-ltxr 10732  df-sub 10924

This theorem is referenced by:  muls1d  11152  addmulsub  11154  recextlem1  11322  cru  11680  cju  11684  zneo  12118  qbtwnre  12647  lincmb01cmp  12941  iccf1o  12942  intfracq  13290  modlt  13311  moddi  13370  modsubdir  13371  subsq  13636  expmulnbnd  13660  crre  14535  remullem  14549  mulcn2  15014  iseraltlem3  15102  fsumparts  15223  geoserg  15283  mertens  15304  bpolydiflem  15470  bpoly4  15475  fsumcube  15476  tanval3  15549  tanadd  15582  eirrlem  15619  bezoutlem3  15955  cncongr1  16078  eulerthlem2  16189  prmdiv  16192  prmdiveq  16193  4sqlem10  16353  mul4sqlem  16359  4sqlem17  16367  blcvx  23514  icopnfhmeo  23659  pcoass  23740  cphipval  23958  pjthlem1  24152  itgmulc2lem2  24547  dvmulbr  24653  cmvth  24705  dvcvx  24734  dvfsumle  24735  dvfsumabs  24737  dvfsumlem2  24741  aaliou3lem8  25055  abelthlem2  25141  tangtx  25212  tanregt0  25245  efif1olem2  25249  efif1olem4  25251  ang180lem5  25513  isosctrlem2  25519  isosctrlem3  25520  affineequiv  25523  heron  25538  dcubic1  25545  dquart  25553  quartlem1  25557  asinsin  25592  efiatan  25612  atanlogsublem  25615  efiatan2  25617  2efiatan  25618  tanatan  25619  atantayl2  25638  lgamgulmlem2  25729  lgamgulmlem3  25730  ftalem5  25776  basellem3  25782  basellem5  25784  logfaclbnd  25920  lgseisenlem2  26074  lgsquadlem1  26078  2sqlem4  26119  2sqmod  26134  vmadivsum  26180  rplogsumlem1  26182  dchrmusum2  26192  dchrvmasumiflem2  26200  rpvmasum2  26210  dchrisum0lem2a  26215  dchrisum0lem2  26216  rplogsum  26225  mulogsumlem  26229  mulogsum  26230  mulog2sumlem1  26232  mulog2sumlem2  26233  mulog2sumlem3  26234  vmalogdivsum2  26236  vmalogdivsum  26237  2vmadivsumlem  26238  logsqvma  26240  selberglem1  26243  selberglem2  26244  selberg2lem  26248  chpdifbndlem1  26251  selberg3lem1  26255  selberg4lem1  26258  selberg4  26259  pntrsumo1  26263  selbergr  26266  selberg3r  26267  selberg4r  26268  selberg34r  26269  pntrlog2bndlem4  26278  pntrlog2bndlem5  26279  pntrlog2bndlem6  26281  pntlemo  26305  ttgcontlem1  26793  brbtwn2  26813  colinearalglem1  26814  axcontlem8  26879  pjhthlem1  29288  knoppndvlem11  34287  knoppndvlem14  34290  knoppndvlem15  34291  knoppndvlem16  34292  bj-bary1lem  35040  bj-bary1lem1  35041  itgmulc2nclem2  35440  areacirclem1  35461  areacirclem4  35464  areacirc  35466  cntotbnd  35550  irrapxlem2  40183  irrapxlem3  40184  irrapxlem5  40186  pellexlem6  40194  pell1qrgaplem  40233  qirropth  40268  jm2.17a  40320  congmul  40327  jm2.18  40348  areaquad  40585  itgsinexp  43009  stoweidlem26  43080  stirlinglem7  43134  fourierdlem83  43243  etransclem46  43334  smfmullem1  43835  fmtnorec3  44493  fmtnorec4  44494  fppr2odd  44676  itcovalt2lem2lem2  45513  submuladdmuld  45540  affinecomb2  45542  itsclc0yqsollem1  45601  itsclc0yqsol  45603  itscnhlc0xyqsol  45604  itsclc0xyqsolr  45608  2itscplem3  45619  itscnhlinecirc02plem1  45621