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. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 18-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | zneo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | halfnz | |
|
2 | 2cn | |
|
3 | zcn | |
|
4 | 3 | adantr | |
5 | mulcl | |
|
6 | 2 4 5 | sylancr | |
7 | zcn | |
|
8 | 7 | adantl | |
9 | mulcl | |
|
10 | 2 8 9 | sylancr | |
11 | 1cnd | |
|
12 | 6 10 11 | subaddd | |
13 | 2 | a1i | |
14 | 13 4 8 | subdid | |
15 | 14 | oveq1d | |
16 | zsubcl | |
|
17 | zcn | |
|
18 | 16 17 | syl | |
19 | 2ne0 | |
|
20 | 19 | a1i | |
21 | 18 13 20 | divcan3d | |
22 | 15 21 | eqtr3d | |
23 | 22 16 | eqeltrd | |
24 | oveq1 | |
|
25 | 24 | eleq1d | |
26 | 23 25 | syl5ibcom | |
27 | 12 26 | sylbird | |
28 | 27 | necon3bd | |
29 | 1 28 | mpi | |
30 | 29 | necomd | |