Description: Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | divmul2 | โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง ๐ถ โ 0 ) ) โ ( ( ๐ด / ๐ถ ) = ๐ต โ ๐ด = ( ๐ถ ยท ๐ต ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divmul | โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง ๐ถ โ 0 ) ) โ ( ( ๐ด / ๐ถ ) = ๐ต โ ( ๐ถ ยท ๐ต ) = ๐ด ) ) | |
2 | eqcom | โข ( ( ๐ถ ยท ๐ต ) = ๐ด โ ๐ด = ( ๐ถ ยท ๐ต ) ) | |
3 | 1 2 | bitrdi | โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง ๐ถ โ 0 ) ) โ ( ( ๐ด / ๐ถ ) = ๐ต โ ๐ด = ( ๐ถ ยท ๐ต ) ) ) |