theorem b1neb0 (a b: nat): $ b1 a != b0 b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | b1odd | odd (b1 a) |
|
2 | oddeq | b1 a = b0 b -> (odd (b1 a) <-> odd (b0 b)) |
|
3 | 1, 2 | mpbii | b1 a = b0 b -> odd (b0 b) |
4 | b0odd | ~odd (b0 b) |
|
5 | 3, 4 | mt | ~b1 a = b0 b |
6 | 5 | conv ne | b1 a != b0 b |