Step |
Hyp |
Ref |
Expression |
1 |
|
isodd |
|- ( N e. Odd <-> ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) ) |
2 |
1
|
baib |
|- ( N e. ZZ -> ( N e. Odd <-> ( ( N + 1 ) / 2 ) e. ZZ ) ) |
3 |
|
peano2z |
|- ( N e. ZZ -> ( N + 1 ) e. ZZ ) |
4 |
3
|
biantrurd |
|- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N + 1 ) e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) ) ) |
5 |
2 4
|
bitrd |
|- ( N e. ZZ -> ( N e. Odd <-> ( ( N + 1 ) e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) ) ) |
6 |
|
iseven |
|- ( ( N + 1 ) e. Even <-> ( ( N + 1 ) e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) ) |
7 |
5 6
|
bitr4di |
|- ( N e. ZZ -> ( N e. Odd <-> ( N + 1 ) e. Even ) ) |