Metamath Proof Explorer


Theorem dfodd4

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

Ref Expression
Assertion dfodd4 Odd = z | z mod 2 = 1

Proof

Step Hyp Ref Expression
1 dfodd2 Odd = z | z 1 2
2 peano2zm z z 1
3 2 zred z z 1
4 2rp 2 +
5 mod0 z 1 2 + z 1 mod 2 = 0 z 1 2
6 3 4 5 sylancl z z 1 mod 2 = 0 z 1 2
7 zre z z
8 2re 2
9 8 a1i z 2
10 1lt2 1 < 2
11 10 a1i z 1 < 2
12 m1mod0mod1 z 2 1 < 2 z 1 mod 2 = 0 z mod 2 = 1
13 7 9 11 12 syl3anc z z 1 mod 2 = 0 z mod 2 = 1
14 6 13 bitr3d z z 1 2 z mod 2 = 1
15 14 rabbiia z | z 1 2 = z | z mod 2 = 1
16 1 15 eqtri Odd = z | z mod 2 = 1