Theorem subdird 11675

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117   − cmin 11448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450

This theorem is referenced by:  mulsubfacd  11679  ltmul1a  12067  xp1d2m1eqxm1d2  12470  div4p1lem1div2  12471  lincmb01cmp  13476  iccf1o  13477  modmul1  13893  remullem  15079  mulcn2  15544  fsumparts  15756  pwdif  15818  geo2sum  15823  fallfacfwd  15984  bpoly4  16007  modprm0  16742  mul4sqlem  16890  vdwapun  16911  icopnfcnv  24687  itgconst  25568  itgmulc2lem2  25582  dvmulbr  25689  dvmulbrOLD  25690  dvrec  25707  dvsincos  25733  cmvth  25743  dvcvx  25772  dvfsumlem1  25778  dvfsumlem2  25779  coeeulem  25973  abelthlem6  26184  tangtx  26251  tanarg  26363  logdivlti  26364  logcnlem4  26389  affineequiv  26564  affineequiv2  26565  chordthmlem2  26574  chordthmlem4  26576  mcubic  26588  dquartlem2  26593  quart1lem  26596  quart1  26597  quartlem1  26598  dvatan  26676  atantayl  26678  lgamcvg2  26795  wilthlem2  26809  logfaclbnd  26961  logexprlim  26964  perfectlem2  26969  dchrsum2  27007  sumdchr2  27009  bposlem9  27031  lgsquadlem1  27119  2sqmod  27175  chebbnd1lem3  27210  rpvmasumlem  27226  log2sumbnd  27283  chpdifbndlem1  27292  selberg3lem1  27296  selberg4lem1  27299  selbergr  27307  selberg3r  27308  selberg4r  27309  pntrlog2bndlem3  27318  pntrlog2bndlem5  27320  pntibndlem2  27330  pntlemo  27346  ttgcontlem1  28409  brbtwn2  28430  colinearalglem1  28431  axsegconlem9  28450  axcontlem2  28490  axcontlem7  28495  axcontlem8  28496  sinccvglem  34955  gg-cmvth  35466  gg-dvfsumlem2  35469  bj-bary1lem  36494  bj-bary1lem1  36495  itgmulc2nclem2  36858  bfp  36995  pellexlem6  41874  congmul  42008  areaquad  42267  itgsinexp  44969  stoweidlem13  45027  stoweidlem14  45028  stoweidlem26  45040  fourierdlem6  45127  fourierdlem26  45147  fourierdlem42  45163  fourierdlem65  45185  fourierdlem95  45215  smfmullem1  45805  sigarmf  45868  cevathlem2  45882  perfectALTVlem2  46688  submuladdmuld  47474  affinecomb2  47476  affineid  47477  rrx2linest  47515  itscnhlinecirc02plem2  47556  inlinecirc02p  47560  joinlmulsubmuld  47908