MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subdird Structured version   Visualization version   GIF version

Theorem subdird 11085
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
StepHypRef Expression
1 mulm1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mulnegd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 subdid.3 . 2 (𝜑𝐶 ∈ ℂ)
4 subdir 11062 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1363 1 (𝜑 → ((𝐴𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   · cmul 10530  cmin 10858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  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 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668  df-sub 10860
This theorem is referenced by:  mulsubfacd  11089  ltmul1a  11477  xp1d2m1eqxm1d2  11879  div4p1lem1div2  11880  lincmb01cmp  12869  iccf1o  12870  modmul1  13280  remullem  14475  mulcn2  14940  fsumparts  15149  pwdif  15211  geo2sum  15217  fallfacfwd  15378  bpoly4  15401  modprm0  16130  mul4sqlem  16277  vdwapun  16298  icopnfcnv  23473  itgconst  24346  itgmulc2lem2  24360  dvmulbr  24463  dvrec  24479  dvsincos  24505  cmvth  24515  dvcvx  24544  dvfsumlem1  24550  dvfsumlem2  24551  coeeulem  24741  abelthlem6  24951  tangtx  25018  tanarg  25129  logdivlti  25130  logcnlem4  25155  affineequiv  25328  affineequiv2  25329  chordthmlem2  25338  chordthmlem4  25340  mcubic  25352  dquartlem2  25357  quart1lem  25360  quart1  25361  quartlem1  25362  dvatan  25440  atantayl  25442  lgamcvg2  25559  wilthlem2  25573  logfaclbnd  25725  logexprlim  25728  perfectlem2  25733  dchrsum2  25771  sumdchr2  25773  bposlem9  25795  lgsquadlem1  25883  2sqmod  25939  chebbnd1lem3  25974  rpvmasumlem  25990  log2sumbnd  26047  chpdifbndlem1  26056  selberg3lem1  26060  selberg4lem1  26063  selbergr  26071  selberg3r  26072  selberg4r  26073  pntrlog2bndlem3  26082  pntrlog2bndlem5  26084  pntibndlem2  26094  pntlemo  26110  ttgcontlem1  26598  brbtwn2  26618  colinearalglem1  26619  axsegconlem9  26638  axcontlem2  26678  axcontlem7  26683  axcontlem8  26684  sinccvglem  32812  bj-bary1lem  34479  bj-bary1lem1  34480  itgmulc2nclem2  34840  bfp  34983  pellexlem6  39309  congmul  39442  areaquad  39701  itgsinexp  42116  stoweidlem13  42175  stoweidlem14  42176  stoweidlem26  42188  fourierdlem6  42275  fourierdlem26  42295  fourierdlem42  42311  fourierdlem65  42333  fourierdlem95  42363  smfmullem1  42943  sigarmf  42988  cevathlem2  43002  perfectALTVlem2  43764  submuladdmuld  44616  affinecomb2  44618  affineid  44619  rrx2linest  44657  itscnhlinecirc02plem2  44698  inlinecirc02p  44702  joinlmulsubmuld  44803
  Copyright terms: Public domain W3C validator