Description: An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | oddp1even | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oddm1even | |
|
2 | 2z | |
|
3 | peano2zm | |
|
4 | dvdsadd | |
|
5 | 2 3 4 | sylancr | |
6 | 2cnd | |
|
7 | zcn | |
|
8 | 1cnd | |
|
9 | 6 7 8 | addsub12d | |
10 | 2m1e1 | |
|
11 | 10 | oveq2i | |
12 | 9 11 | eqtrdi | |
13 | 12 | breq2d | |
14 | 1 5 13 | 3bitrd | |