Description: An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 follows immediately from the principle of double negation, see notnotb . (Contributed by AV, 17-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | zeo4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb | |
|
2 | 1 | a1i | |