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