Theorem adddii 11257

Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
adddii	⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))

Proof of Theorem adddii

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		adddi 11228	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	mp3an 1458	1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11137   + caddc 11142   · cmul 11144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  addrid  11425  3t3e9  12410  numltc  12734  numsucc  12748  numma  12752  decmul10add  12777  4t3lem  12805  9t11e99  12838  decbin2  12849  binom2i  14208  3dec  14258  faclbnd4lem1  14285  3dvds2dec  16310  mod2xnegi  17040  decsplit  17052  log2ublem1  26891  log2ublem2  26892  bposlem8  27237  ax5seglem7  28759  ip0i  30648  ip1ilem  30649  ipasslem10  30662  normlem0  30932  polid2i  30980  lnopunilem1  31833  dfdec100  32606  dpmul10  32631  dpmul  32649  dpmul4  32650  sn-1ne2  41840  sqmid3api  41857  ipiiie0  41992  sn-0tie0  41994  fourierswlem  45618  3exp4mod41  46956  2t6m3t4e0  47412

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »