Step |
Hyp |
Ref |
Expression |
1 |
|
isodd2 |
|- ( x e. Odd <-> ( x e. ZZ /\ ( ( x - 1 ) / 2 ) e. ZZ ) ) |
2 |
|
oveq1 |
|- ( z = x -> ( z - 1 ) = ( x - 1 ) ) |
3 |
2
|
oveq1d |
|- ( z = x -> ( ( z - 1 ) / 2 ) = ( ( x - 1 ) / 2 ) ) |
4 |
3
|
eleq1d |
|- ( z = x -> ( ( ( z - 1 ) / 2 ) e. ZZ <-> ( ( x - 1 ) / 2 ) e. ZZ ) ) |
5 |
4
|
elrab |
|- ( x e. { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } <-> ( x e. ZZ /\ ( ( x - 1 ) / 2 ) e. ZZ ) ) |
6 |
1 5
|
bitr4i |
|- ( x e. Odd <-> x e. { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } ) |
7 |
6
|
eqriv |
|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } |