Theorem subdid 11431

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   · cmul 10876   − cmin 11205

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-ltxr 11014  df-sub 11207

This theorem is referenced by:  muls1d  11435  addmulsub  11437  recextlem1  11605  cru  11965  cju  11969  zneo  12403  qbtwnre  12933  lincmb01cmp  13227  iccf1o  13228  intfracq  13579  modlt  13600  moddi  13659  modsubdir  13660  subsq  13926  expmulnbnd  13950  crre  14825  remullem  14839  mulcn2  15305  iseraltlem3  15395  fsumparts  15518  geoserg  15578  mertens  15598  bpolydiflem  15764  bpoly4  15769  fsumcube  15770  tanval3  15843  tanadd  15876  eirrlem  15913  bezoutlem3  16249  cncongr1  16372  eulerthlem2  16483  prmdiv  16486  prmdiveq  16487  4sqlem10  16648  mul4sqlem  16654  4sqlem17  16662  blcvx  23961  icopnfhmeo  24106  pcoass  24187  cphipval  24407  pjthlem1  24601  itgmulc2lem2  24997  dvmulbr  25103  cmvth  25155  dvcvx  25184  dvfsumle  25185  dvfsumabs  25187  dvfsumlem2  25191  aaliou3lem8  25505  abelthlem2  25591  tangtx  25662  tanregt0  25695  efif1olem2  25699  efif1olem4  25701  ang180lem5  25963  isosctrlem2  25969  isosctrlem3  25970  affineequiv  25973  heron  25988  dcubic1  25995  dquart  26003  quartlem1  26007  asinsin  26042  efiatan  26062  atanlogsublem  26065  efiatan2  26067  2efiatan  26068  tanatan  26069  atantayl2  26088  lgamgulmlem2  26179  lgamgulmlem3  26180  ftalem5  26226  basellem3  26232  basellem5  26234  logfaclbnd  26370  lgseisenlem2  26524  lgsquadlem1  26528  2sqlem4  26569  2sqmod  26584  vmadivsum  26630  rplogsumlem1  26632  dchrmusum2  26642  dchrvmasumiflem2  26650  rpvmasum2  26660  dchrisum0lem2a  26665  dchrisum0lem2  26666  rplogsum  26675  mulogsumlem  26679  mulogsum  26680  mulog2sumlem1  26682  mulog2sumlem2  26683  mulog2sumlem3  26684  vmalogdivsum2  26686  vmalogdivsum  26687  2vmadivsumlem  26688  logsqvma  26690  selberglem1  26693  selberglem2  26694  selberg2lem  26698  chpdifbndlem1  26701  selberg3lem1  26705  selberg4lem1  26708  selberg4  26709  pntrsumo1  26713  selbergr  26716  selberg3r  26717  selberg4r  26718  selberg34r  26719  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  pntrlog2bndlem6  26731  pntlemo  26755  ttgcontlem1  27252  brbtwn2  27273  colinearalglem1  27274  axcontlem8  27339  pjhthlem1  29753  knoppndvlem11  34702  knoppndvlem14  34705  knoppndvlem15  34706  knoppndvlem16  34707  bj-bary1lem  35481  bj-bary1lem1  35482  itgmulc2nclem2  35844  areacirclem1  35865  areacirclem4  35868  areacirc  35870  cntotbnd  35954  irrapxlem2  40645  irrapxlem3  40646  irrapxlem5  40648  pellexlem6  40656  pell1qrgaplem  40695  qirropth  40730  jm2.17a  40782  congmul  40789  jm2.18  40810  areaquad  41047  itgsinexp  43496  stoweidlem26  43567  stirlinglem7  43621  fourierdlem83  43730  etransclem46  43821  smfmullem1  44325  fmtnorec3  45000  fmtnorec4  45001  fppr2odd  45183  itcovalt2lem2lem2  46020  submuladdmuld  46047  affinecomb2  46049  itsclc0yqsollem1  46108  itsclc0yqsol  46110  itscnhlc0xyqsol  46111  itsclc0xyqsolr  46115  2itscplem3  46126  itscnhlinecirc02plem1  46128