theorem elnel (a b: nat): $ a e. b <-> odd (shr b a) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | _1 = a -> _1 = a |
|
| 2 | 1 | shreq2d | _1 = a -> shr b _1 = shr b a |
| 3 | 2 | oddeqd | _1 = a -> (odd (shr b _1) <-> odd (shr b a)) |
| 4 | 3 | elabe | a e. {_1 | odd (shr b _1)} <-> odd (shr b a) |
| 5 | 4 | conv ns | a e. b <-> odd (shr b a) |