Description: No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of Apostol p. 28. This variant of zneo follows immediately from the fact that a contradiction implies anything, see pm2.21i . (Contributed by AV, 22-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | zeneo | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 || A /\ -. 2 || B ) -> A =/= B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nbrne1 | |- ( ( 2 || A /\ -. 2 || B ) -> A =/= B ) |
|
| 2 | 1 | a1i | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 || A /\ -. 2 || B ) -> A =/= B ) ) |