Description: An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | oddm1even | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | 1 | zcnd | |
3 | 1cnd | |
|
4 | 2cnd | |
|
5 | simpr | |
|
6 | 5 | zcnd | |
7 | 4 6 | mulcld | |
8 | 2 3 7 | subadd2d | |
9 | eqcom | |
|
10 | 4 6 | mulcomd | |
11 | 10 | eqeq1d | |
12 | 9 11 | syl5bb | |
13 | 8 12 | bitr3d | |
14 | 13 | rexbidva | |
15 | odd2np1 | |
|
16 | 2z | |
|
17 | peano2zm | |
|
18 | divides | |
|
19 | 16 17 18 | sylancr | |
20 | 14 15 19 | 3bitr4d | |