Theorem subdid 11088

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

Syntax hints:   → wi 4   = wceq 1530   ∈ wcel 2107  (class class class)co 7148  ℂcc 10527   · cmul 10534   − cmin 10862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-sub 10864

This theorem is referenced by:  muls1d  11092  addmulsub  11094  recextlem1  11262  cru  11622  cju  11626  zneo  12057  qbtwnre  12584  lincmb01cmp  12873  iccf1o  12874  intfracq  13219  modlt  13240  moddi  13299  modsubdir  13300  subsq  13564  expmulnbnd  13588  crre  14465  remullem  14479  mulcn2  14944  iseraltlem3  15032  fsumparts  15153  geoserg  15213  mertens  15234  bpolydiflem  15400  bpoly4  15405  fsumcube  15406  tanval3  15479  tanadd  15512  eirrlem  15549  bezoutlem3  15881  cncongr1  16003  eulerthlem2  16111  prmdiv  16114  prmdiveq  16115  4sqlem10  16275  mul4sqlem  16281  4sqlem17  16289  blcvx  23398  icopnfhmeo  23539  pcoass  23620  cphipval  23838  pjthlem1  24032  itgmulc2lem2  24425  dvmulbr  24528  cmvth  24580  dvcvx  24609  dvfsumle  24610  dvfsumabs  24612  dvfsumlem2  24616  aaliou3lem8  24926  abelthlem2  25012  tangtx  25083  tanregt0  25115  efif1olem2  25119  efif1olem4  25121  ang180lem5  25383  isosctrlem2  25389  isosctrlem3  25390  affineequiv  25393  heron  25408  dcubic1  25415  dquart  25423  quartlem1  25427  asinsin  25462  efiatan  25482  atanlogsublem  25485  efiatan2  25487  2efiatan  25488  tanatan  25489  atantayl2  25508  lgamgulmlem2  25599  lgamgulmlem3  25600  ftalem5  25646  basellem3  25652  basellem5  25654  logfaclbnd  25790  lgseisenlem2  25944  lgsquadlem1  25948  2sqlem4  25989  2sqmod  26004  vmadivsum  26050  rplogsumlem1  26052  dchrmusum2  26062  dchrvmasumiflem2  26070  rpvmasum2  26080  dchrisum0lem2a  26085  dchrisum0lem2  26086  rplogsum  26095  mulogsumlem  26099  mulogsum  26100  mulog2sumlem1  26102  mulog2sumlem2  26103  mulog2sumlem3  26104  vmalogdivsum2  26106  vmalogdivsum  26107  2vmadivsumlem  26108  logsqvma  26110  selberglem1  26113  selberglem2  26114  selberg2lem  26118  chpdifbndlem1  26121  selberg3lem1  26125  selberg4lem1  26128  selberg4  26129  pntrsumo1  26133  selbergr  26136  selberg3r  26137  selberg4r  26138  selberg34r  26139  pntrlog2bndlem4  26148  pntrlog2bndlem5  26149  pntrlog2bndlem6  26151  pntlemo  26175  ttgcontlem1  26663  brbtwn2  26683  colinearalglem1  26684  axcontlem8  26749  pjhthlem1  29160  knoppndvlem11  33854  knoppndvlem14  33857  knoppndvlem15  33858  knoppndvlem16  33859  bj-bary1lem  34583  bj-bary1lem1  34584  itgmulc2nclem2  34951  areacirclem1  34974  areacirclem4  34977  areacirc  34979  cntotbnd  35066  irrapxlem2  39410  irrapxlem3  39411  irrapxlem5  39413  pellexlem6  39421  pell1qrgaplem  39460  qirropth  39495  jm2.17a  39547  congmul  39554  jm2.18  39575  areaquad  39813  itgsinexp  42229  stoweidlem26  42301  stirlinglem7  42355  fourierdlem83  42464  etransclem46  42555  smfmullem1  43056  fmtnorec3  43700  fmtnorec4  43701  fppr2odd  43886  submuladdmuld  44678  affinecomb2  44680  itsclc0yqsollem1  44739  itsclc0yqsol  44741  itscnhlc0xyqsol  44742  itsclc0xyqsolr  44746  2itscplem3  44757  itscnhlinecirc02plem1  44759