theorem idvd2 (a b c: nat): $ a * c = b -> a || b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 | a * c = c * a -> (a * c = b <-> c * a = b) |
|
| 2 | mulcom | a * c = c * a |
|
| 3 | 1, 2 | ax_mp | a * c = b <-> c * a = b |
| 4 | idvd | c * a = b -> a || b |
|
| 5 | 3, 4 | sylbi | a * c = b -> a || b |