theorem zdvdmul2 (a b: nat): $ a |Z a *Z b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zdvdeq2 | b *Z a = a *Z b -> (a |Z b *Z a <-> a |Z a *Z b) |
|
2 | zmulcom | b *Z a = a *Z b |
|
3 | 1, 2 | ax_mp | a |Z b *Z a <-> a |Z a *Z b |
4 | zdvdmul1 | a |Z b *Z a |
|
5 | 3, 4 | mpbi | a |Z a *Z b |