This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }