Metamath Proof Explorer

Theorem dfodd4

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

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

Proof

Step Hyp Ref Expression
1 dfodd2 
 |-  Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }
2 peano2zm 
 |-  ( z e. ZZ -> ( z - 1 ) e. ZZ )
3 2 zred 
 |-  ( z e. ZZ -> ( z - 1 ) e. RR )
4 2rp 
 |-  2 e. RR+
5 mod0 
 |-  ( ( ( z - 1 ) e. RR /\ 2 e. RR+ ) -> ( ( ( z - 1 ) mod 2 ) = 0 <-> ( ( z - 1 ) / 2 ) e. ZZ ) )
6 3 4 5 sylancl 
 |-  ( z e. ZZ -> ( ( ( z - 1 ) mod 2 ) = 0 <-> ( ( z - 1 ) / 2 ) e. ZZ ) )
7 zre 
 |-  ( z e. ZZ -> z e. RR )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( z e. ZZ -> 2 e. RR )
10 1lt2 
 |-  1 < 2
11 10 a1i 
 |-  ( z e. ZZ -> 1 < 2 )
12 m1mod0mod1 
 |-  ( ( z e. RR /\ 2 e. RR /\ 1 < 2 ) -> ( ( ( z - 1 ) mod 2 ) = 0 <-> ( z mod 2 ) = 1 ) )
13 7 9 11 12 syl3anc 
 |-  ( z e. ZZ -> ( ( ( z - 1 ) mod 2 ) = 0 <-> ( z mod 2 ) = 1 ) )
14 6 13 bitr3d 
 |-  ( z e. ZZ -> ( ( ( z - 1 ) / 2 ) e. ZZ <-> ( z mod 2 ) = 1 ) )
15 14 rabbiia 
 |-  { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } = { z e. ZZ | ( z mod 2 ) = 1 }
16 1 15 eqtri 
 |-  Odd = { z e. ZZ | ( z mod 2 ) = 1 }