Theorem subdird 11605

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041   − cmin 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182  df-sub 11377

This theorem is referenced by:  mulsubfacd  11609  ltmul1a  12002  xp1d2m1eqxm1d2  12429  div4p1lem1div2  12430  lincmb01cmp  13446  iccf1o  13447  modmul1  13884  remullem  15088  mulcn2  15556  fsumparts  15767  pwdif  15831  geo2sum  15836  fallfacfwd  15999  bpoly4  16022  modprm0  16774  mul4sqlem  16922  vdwapun  16943  icopnfcnv  24934  itgconst  25811  itgmulc2lem2  25825  dvmulbr  25931  dvrec  25947  dvsincos  25973  cmvth  25983  dvcvx  26012  dvfsumlem1  26018  dvfsumlem2  26019  coeeulem  26214  abelthlem6  26426  tangtx  26494  tanarg  26608  logdivlti  26609  logcnlem4  26634  affineequiv  26812  affineequiv2  26813  chordthmlem2  26822  chordthmlem4  26824  mcubic  26836  dquartlem2  26841  quart1lem  26844  quart1  26845  quartlem1  26846  dvatan  26924  atantayl  26926  lgamcvg2  27043  wilthlem2  27057  logfaclbnd  27210  logexprlim  27213  perfectlem2  27218  dchrsum2  27256  sumdchr2  27258  bposlem9  27280  lgsquadlem1  27368  2sqmod  27424  chebbnd1lem3  27459  rpvmasumlem  27475  log2sumbnd  27532  chpdifbndlem1  27541  selberg3lem1  27545  selberg4lem1  27548  selbergr  27556  selberg3r  27557  selberg4r  27558  pntrlog2bndlem3  27567  pntrlog2bndlem5  27569  pntibndlem2  27579  pntlemo  27595  ttgcontlem1  28978  brbtwn2  28999  colinearalglem1  29000  axsegconlem9  29019  axcontlem2  29059  axcontlem7  29064  axcontlem8  29065  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  constrrecl  33960  sinccvglem  35907  bj-bary1lem  37677  bj-bary1lem1  37678  itgmulc2nclem2  38061  bfp  38198  pellexlem6  43286  congmul  43419  areaquad  43668  itgsinexp  46405  stoweidlem13  46463  stoweidlem14  46464  stoweidlem26  46476  fourierdlem6  46563  fourierdlem26  46583  fourierdlem42  46599  fourierdlem65  46621  fourierdlem95  46651  smfmullem1  47241  sigarmf  47304  cevathlem2  47318  sin3t  47341  cos3t  47342  sin5tlem2  47344  sin5tlem4  47346  sin5tlem5  47347  perfectALTVlem2  48220  submuladdmuld  49199  affinecomb2  49201  affineid  49202  rrx2linest  49240  itscnhlinecirc02plem2  49281  inlinecirc02p  49285  joinlmulsubmuld  50271