Metamath Proof Explorer


Theorem muls1d

Description: Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017)

Ref Expression
Hypotheses muls1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
muls1d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
Assertion muls1d ( ๐œ‘ โ†’ ( ๐ด ยท ( ๐ต โˆ’ 1 ) ) = ( ( ๐ด ยท ๐ต ) โˆ’ ๐ด ) )

Proof

Step Hyp Ref Expression
1 muls1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 muls1d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
3 1cnd โŠข ( ๐œ‘ โ†’ 1 โˆˆ โ„‚ )
4 1 2 3 subdid โŠข ( ๐œ‘ โ†’ ( ๐ด ยท ( ๐ต โˆ’ 1 ) ) = ( ( ๐ด ยท ๐ต ) โˆ’ ( ๐ด ยท 1 ) ) )
5 1 mulridd โŠข ( ๐œ‘ โ†’ ( ๐ด ยท 1 ) = ๐ด )
6 5 oveq2d โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ต ) โˆ’ ( ๐ด ยท 1 ) ) = ( ( ๐ด ยท ๐ต ) โˆ’ ๐ด ) )
7 4 6 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ด ยท ( ๐ต โˆ’ 1 ) ) = ( ( ๐ด ยท ๐ต ) โˆ’ ๐ด ) )