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

Theorem adddirp1d 11242
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 11211 . . 3 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
3 adddirp1d.b . . 3 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
41, 2, 3adddird 11241 . 2 (๐œ‘ โ†’ ((๐ด + 1) ยท ๐ต) = ((๐ด ยท ๐ต) + (1 ยท ๐ต)))
53mullidd 11234 . . 3 (๐œ‘ โ†’ (1 ยท ๐ต) = ๐ต)
65oveq2d 7427 . 2 (๐œ‘ โ†’ ((๐ด ยท ๐ต) + (1 ยท ๐ต)) = ((๐ด ยท ๐ต) + ๐ต))
74, 6eqtrd 2772 1 (๐œ‘ โ†’ ((๐ด + 1) ยท ๐ต) = ((๐ด ยท ๐ต) + ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1541   โˆˆ wcel 2106  (class class class)co 7411  โ„‚cc 11110  1c1 11113   + caddc 11115   ยท cmul 11117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414
This theorem is referenced by:  modvalp1  13857  pcexp  16794  mulgnnass  18991  cnfldmulg  20983  dgrcolem1  25794  abelthlem2  25951  2lgsoddprmlem3d  26923  chpdifbndlem1  27063  breprexplemc  33713  fltnltalem  41486  lt3addmuld  44090  lt4addmuld  44095  itgsinexp  44750  fourierdlem19  44921  fourierdlem35  44937  fourierdlem51  44952
  Copyright terms: Public domain W3C validator