Theorem subdird 10904

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
subdird	⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))

Proof of Theorem subdird

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subdid.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		subdir 10881	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1352	1 ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  (class class class)co 6982  ℂcc 10339   · cmul 10346   − cmin 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285  ax-resscn 10398  ax-1cn 10399  ax-icn 10400  ax-addcl 10401  ax-addrcl 10402  ax-mulcl 10403  ax-mulrcl 10404  ax-mulcom 10405  ax-addass 10406  ax-mulass 10407  ax-distr 10408  ax-i2m1 10409  ax-1ne0 10410  ax-1rid 10411  ax-rnegex 10412  ax-rrecex 10413  ax-cnre 10414  ax-pre-lttri 10415  ax-pre-lttrn 10416  ax-pre-ltadd 10417

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-po 5330  df-so 5331  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-er 8095  df-en 8313  df-dom 8314  df-sdom 8315  df-pnf 10482  df-mnf 10483  df-ltxr 10485  df-sub 10678

This theorem is referenced by:  mulsubfacd  10908  ltmul1a  11296  xp1d2m1eqxm1d2  11707  div4p1lem1div2  11708  lincmb01cmp  12703  iccf1o  12704  modmul1  13113  remullem  14354  mulcn2  14819  fsumparts  15027  pwdif  15089  geo2sum  15095  fallfacfwd  15256  bpoly4  15279  modprm0  16004  mul4sqlem  16151  vdwapun  16172  icopnfcnv  23264  itgconst  24137  itgmulc2lem2  24151  dvmulbr  24254  dvrec  24270  dvsincos  24296  cmvth  24306  dvcvx  24335  dvfsumlem1  24341  dvfsumlem2  24342  coeeulem  24532  abelthlem6  24742  tangtx  24809  tanarg  24918  logdivlti  24919  logcnlem4  24944  affineequiv  25117  affineequiv2  25118  chordthmlem2  25127  chordthmlem4  25129  mcubic  25141  dquartlem2  25146  quart1lem  25149  quart1  25150  quartlem1  25151  dvatan  25229  atantayl  25231  lgamcvg2  25349  wilthlem2  25363  logfaclbnd  25515  logexprlim  25518  perfectlem2  25523  dchrsum2  25561  sumdchr2  25563  bposlem9  25585  lgsquadlem1  25673  2sqmod  25729  chebbnd1lem3  25764  rpvmasumlem  25780  log2sumbnd  25837  chpdifbndlem1  25846  selberg3lem1  25850  selberg4lem1  25853  selbergr  25861  selberg3r  25862  selberg4r  25863  pntrlog2bndlem3  25872  pntrlog2bndlem5  25874  pntibndlem2  25884  pntlemo  25900  ttgcontlem1  26389  brbtwn2  26409  colinearalglem1  26410  axsegconlem9  26429  axcontlem2  26469  axcontlem7  26474  axcontlem8  26475  sinccvglem  32475  bj-bary1lem  34079  bj-bary1lem1  34080  itgmulc2nclem2  34440  bfp  34584  pellexlem6  38868  congmul  39001  areaquad  39260  itgsinexp  41705  stoweidlem13  41764  stoweidlem14  41765  stoweidlem26  41777  fourierdlem6  41864  fourierdlem26  41884  fourierdlem42  41900  fourierdlem65  41922  fourierdlem95  41952  smfmullem1  42532  sigarmf  42577  cevathlem2  42591  perfectALTVlem2  43290  submuladdmuld  44091  affinecomb2  44093  affineid  44094  rrx2linest  44132  itscnhlinecirc02plem2  44173  inlinecirc02p  44177  joinlmulsubmuld  44277