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

Theorem adddirp1d 11287
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
StepHypRef Expression
1 adddirp1d.a . . 3 (𝜑𝐴 ∈ ℂ)
2 1cnd 11256 . . 3 (𝜑 → 1 ∈ ℂ)
3 adddirp1d.b . . 3 (𝜑𝐵 ∈ ℂ)
41, 2, 3adddird 11286 . 2 (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + (1 · 𝐵)))
53mullidd 11279 . . 3 (𝜑 → (1 · 𝐵) = 𝐵)
65oveq2d 7447 . 2 (𝜑 → ((𝐴 · 𝐵) + (1 · 𝐵)) = ((𝐴 · 𝐵) + 𝐵))
74, 6eqtrd 2777 1 (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  (class class class)co 7431  cc 11153  1c1 11156   + caddc 11158   · cmul 11160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434
This theorem is referenced by:  modvalp1  13930  pcexp  16897  mulgnnass  19127  cnfldmulg  21416  dgrcolem1  26313  abelthlem2  26476  2lgsoddprmlem3d  27457  chpdifbndlem1  27597  breprexplemc  34647  deg1pow  42142  fltnltalem  42672  lt3addmuld  45313  lt4addmuld  45318  itgsinexp  45970  fourierdlem19  46141  fourierdlem35  46157  fourierdlem51  46172  minusmodnep2tmod  47355  gpg3kgrtriexlem2  48040
  Copyright terms: Public domain W3C validator