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

Theorem adddird 10277
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 10243 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1477 1 (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6814  cc 10146   + caddc 10151   · cmul 10153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-addcl 10208  ax-mulcom 10212  ax-distr 10215
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817
This theorem is referenced by:  adddirp1d  10278  joinlmuladdmuld  10279  recextlem1  10869  divdir  10922  ltdifltdiv  12849  subsq  13186  subsq2  13187  binom3  13199  discr1  13214  cshweqrep  13787  remullem  14087  sqrlem7  14208  binomlem  14780  arisum  14811  binomfallfaclem2  14990  pwp1fsum  15336  smumullem  15436  bezoutlem3  15480  bezoutlem4  15481  pcexp  15786  mul4sqlem  15879  vdwapun  15900  mulgnnass  17797  mulgnnassOLD  17798  cnfldmulg  20000  nn0srg  20038  rge0srg  20039  nmotri  22764  blcvx  22822  cphipval2  23260  itg1addlem5  23686  mbfi1fseqlem4  23704  itgconst  23804  itgmulc2  23819  dvexp  23935  dvcvx  24002  plyaddlem1  24188  dgrcolem1  24248  abelthlem2  24405  abelthlem7  24411  tangtx  24477  cxpadd  24645  dcubic  24793  binom4  24797  dquartlem2  24799  dquart  24800  quart1lem  24802  quart1  24803  cvxcl  24931  scvxcvx  24932  basellem9  25035  bposlem9  25237  lgsquad2lem1  25329  2sqlem4  25366  2sqblem  25376  dchrisumlem2  25399  dchrisum0lem1  25425  mudivsum  25439  chpdifbndlem1  25462  pntrlog2bndlem2  25487  pntlemr  25511  pntlemk  25515  ostth2lem2  25543  brbtwn2  26005  ax5seglem3  26031  ax5seglem5  26033  axbtwnid  26039  axeuclidlem  26062  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  axcontlem8  26071  ex-ind-dvds  27650  smcnlem  27882  circlemeth  31048  hgt750lemd  31056  logdivsqrle  31058  subfacp1lem6  31495  subfacval2  31497  subfaclim  31498  cvxsconn  31553  resconn  31556  fwddifnp1  32599  itg2addnclem3  33794  itgmulc2nc  33809  rrnequiv  33965  jm2.19lem3  38078  jm2.25  38086  jm3.1lem2  38105  inductionexd  38973  int-leftdistd  39002  binomcxplemwb  39067  binomcxplemnotnn0  39075  sineq0ALT  39690  fperiodmullem  40034  xralrple2  40086  coskpi2  40598  cosknegpi  40601  dvnmul  40679  stoweidlem11  40749  stoweidlem13  40751  stirlinglem1  40812  stirlinglem4  40815  dirkerper  40834  dirkertrigeqlem1  40836  dirkertrigeqlem2  40837  dirkertrigeqlem3  40838  dirkercncflem2  40842  fourierdlem41  40886  fourierdlem42  40887  fourierdlem64  40908  fourierswlem  40968  hoidmvlelem2  41334  sigaraf  41566  fmtnorec3  41988
  Copyright terms: Public domain W3C validator