Metamath Proof Explorer


Theorem dfodd2

Description: Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020)

Ref Expression
Assertion dfodd2
|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }

Proof

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 }