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

Theorem adddird 10658
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 10624 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1365 1 (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  (class class class)co 7148  cc 10527   + caddc 10532   · cmul 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-addcl 10589  ax-mulcom 10593  ax-distr 10596
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151
This theorem is referenced by:  adddirp1d  10659  joinlmuladdmuld  10660  addmulsub  11094  recextlem1  11262  divdir  11315  subsq  13564  subsq2  13565  binom3  13577  discr1  13592  cshweqrep  14175  remullem  14479  sqrlem7  14600  binomlem  15176  binomfallfaclem2  15386  pwp1fsum  15734  smumullem  15833  mul4sqlem  16281  vdwapun  16302  nn0srg  20607  rge0srg  20608  nmotri  23340  blcvx  23398  cphipval2  23836  itg1addlem5  24293  itgconst  24411  dvexp  24542  dvcvx  24609  plyaddlem1  24795  abelthlem7  25018  cxpadd  25254  dcubic  25416  binom4  25420  dquartlem2  25422  dquart  25423  quart1lem  25425  quart1  25426  cvxcl  25554  scvxcvx  25555  basellem9  25658  bposlem9  25860  lgsquad2lem1  25952  2sqlem4  25989  2sqblem  25999  dchrisumlem2  26058  dchrisum0lem1  26084  mudivsum  26098  chpdifbndlem1  26121  pntrlog2bndlem2  26146  pntlemr  26170  pntlemk  26174  ostth2lem2  26202  brbtwn2  26683  ax5seglem3  26709  ax5seglem5  26711  axbtwnid  26717  axeuclidlem  26740  axcontlem2  26743  axcontlem4  26745  axcontlem7  26748  ex-ind-dvds  28232  smcnlem  28466  ccfldsrarelvec  31049  circlemeth  31904  hgt750lemd  31912  logdivsqrle  31914  subfacp1lem6  32425  subfacval2  32427  subfaclim  32428  cvxsconn  32483  resconn  32486  fwddifnp1  33619  itg2addnclem3  34937  itgmulc2nc  34952  rrnequiv  35105  fltnlta  39265  cu3addd  39267  3cubeslem2  39272  3cubeslem3r  39274  jm2.19lem3  39578  jm2.25  39586  jm3.1lem2  39605  inductionexd  40495  int-leftdistd  40522  binomcxplemwb  40670  binomcxplemnotnn0  40678  sineq0ALT  41261  fperiodmullem  41559  xralrple2  41611  coskpi2  42136  cosknegpi  42139  dvnmul  42217  stoweidlem11  42286  stoweidlem13  42288  stirlinglem1  42349  stirlinglem4  42352  dirkerper  42371  dirkertrigeqlem1  42373  dirkertrigeqlem2  42374  dirkertrigeqlem3  42375  dirkercncflem2  42379  fourierdlem41  42423  fourierdlem42  42424  fourierdlem64  42445  fourierswlem  42505  hoidmvlelem2  42868  sigaraf  43100  fmtnorec3  43700  itscnhlc0yqe  44736  itsclc0yqsollem1  44739  itscnhlc0xyqsol  44742  itsclc0xyqsolr  44746  itsclquadb  44753  2itscplem3  44757  itscnhlinecirc02plem1  44759
  Copyright terms: Public domain W3C validator