Metamath Proof Explorer


Theorem divmul2

Description: Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006)

Ref Expression
Assertion divmul2 ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด / ๐ถ ) = ๐ต โ†” ๐ด = ( ๐ถ ยท ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 divmul โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด / ๐ถ ) = ๐ต โ†” ( ๐ถ ยท ๐ต ) = ๐ด ) )
2 eqcom โŠข ( ( ๐ถ ยท ๐ต ) = ๐ด โ†” ๐ด = ( ๐ถ ยท ๐ต ) )
3 1 2 bitrdi โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด / ๐ถ ) = ๐ต โ†” ๐ด = ( ๐ถ ยท ๐ต ) ) )