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

Theorem adddird 10012
Description: Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
addassd.3 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
adddird (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))

Proof of Theorem adddird
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 adddir 9978 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1323 1 (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  (class class class)co 6607  cc 9881   + caddc 9886   · cmul 9888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-addcl 9943  ax-mulcom 9947  ax-distr 9950
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-iota 5812  df-fv 5857  df-ov 6610
This theorem is referenced by:  adddirp1d  10013  joinlmuladdmuld  10014  recextlem1  10604  divdir  10657  ltdifltdiv  12578  subsq  12915  subsq2  12916  binom3  12928  discr1  12943  cshweqrep  13507  remullem  13805  sqrlem7  13926  binomlem  14489  arisum  14520  binomfallfaclem2  14699  pwp1fsum  15041  smumullem  15141  bezoutlem3  15185  bezoutlem4  15186  pcexp  15491  mul4sqlem  15584  vdwapun  15605  mulgnnass  17500  mulgnnassOLD  17501  cnfldmulg  19700  nn0srg  19738  rge0srg  19739  nmotri  22456  blcvx  22514  cphipval2  22953  itg1addlem5  23380  mbfi1fseqlem4  23398  itgconst  23498  itgmulc2  23513  dvexp  23629  dvcvx  23694  plyaddlem1  23880  dgrcolem1  23940  abelthlem2  24097  abelthlem7  24103  tangtx  24168  cxpadd  24332  dcubic  24480  binom4  24484  dquartlem2  24486  dquart  24487  quart1lem  24489  quart1  24490  cvxcl  24618  scvxcvx  24619  basellem9  24722  bposlem9  24924  lgsquad2lem1  25016  2sqlem4  25053  2sqblem  25063  dchrisumlem2  25086  dchrisum0lem1  25112  mudivsum  25126  chpdifbndlem1  25149  pntrlog2bndlem2  25174  pntlemr  25198  pntlemk  25202  ostth2lem2  25230  brbtwn2  25692  ax5seglem3  25718  ax5seglem5  25720  axbtwnid  25726  axeuclidlem  25749  axcontlem2  25752  axcontlem4  25754  axcontlem7  25757  axcontlem8  25758  ex-ind-dvds  27179  smcnlem  27413  subfacp1lem6  30896  subfacval2  30898  subfaclim  30899  cvxsconn  30954  resconn  30957  fwddifnp1  31935  itg2addnclem3  33116  itgmulc2nc  33131  rrnequiv  33287  jm2.19lem3  37059  jm2.25  37067  jm3.1lem2  37086  inductionexd  37956  int-leftdistd  37985  binomcxplemwb  38050  binomcxplemnotnn0  38058  sineq0ALT  38677  fperiodmullem  38999  xralrple2  39052  coskpi2  39398  cosknegpi  39401  dvnmul  39481  stoweidlem11  39551  stoweidlem13  39553  stirlinglem1  39614  stirlinglem4  39617  dirkerper  39636  dirkertrigeqlem1  39638  dirkertrigeqlem2  39639  dirkertrigeqlem3  39640  dirkercncflem2  39644  fourierdlem41  39688  fourierdlem42  39689  fourierdlem64  39710  fourierswlem  39770  hoidmvlelem2  40133  sigaraf  40362  fmtnorec3  40775
  Copyright terms: Public domain W3C validator