Theorem adddirp1d 11167

Description: Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
adddirp1d.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
adddirp1d.b	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
adddirp1d	⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))

Proof of Theorem adddirp1d

Step	Hyp	Ref	Expression
1		adddirp1d.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		1cnd 11135	. . 3 ⊢ (𝜑 → 1 ∈ ℂ)
3		adddirp1d.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4	1, 2, 3	adddird 11166	. 2 ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + (1 · 𝐵)))
5	3	mullidd 11159	. . 3 ⊢ (𝜑 → (1 · 𝐵) = 𝐵)
6	5	oveq2d 7375	. 2 ⊢ (𝜑 → ((𝐴 · 𝐵) + (1 · 𝐵)) = ((𝐴 · 𝐵) + 𝐵))
7	4, 6	eqtrd 2776	1 ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  (class class class)co 7359  ℂcc 11032  1c1 11035   + caddc 11037   · cmul 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-mulcl 11096  ax-mulcom 11098  ax-mulass 11100  ax-distr 11101  ax-1rid 11104  ax-cnre 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362

This theorem is referenced by:  modvalp1  13844  pcexp  16825  mulgnnass  19080  cnfldmulg  21382  dgrcolem1  26259  abelthlem2  26418  2lgsoddprmlem3d  27397  chpdifbndlem1  27537  breprexplemc  34826  deg1pow  42639  fltnltalem  43125  lt3addmuld  45761  lt4addmuld  45766  itgsinexp  46410  fourierdlem19  46581  fourierdlem35  46597  fourierdlem51  46612  minusmodnep2tmod  47834  gpg3kgrtriexlem2  48587