Theorem dfodd4

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

	Ref	Expression
Assertion	dfodd4	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 1 }

Proof

Step	Hyp	Ref	Expression
1		dfodd2	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ }
2		peano2zm	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 − 1 ) ∈ ℤ )
3	2	zred	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 − 1 ) ∈ ℝ )
4		2rp	⊢ 2 ∈ ℝ+
5		mod0	⊢ ( ( ( 𝑧 − 1 ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( ( 𝑧 − 1 ) mod 2 ) = 0 ↔ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) )
6	3 4 5	sylancl	⊢ ( 𝑧 ∈ ℤ → ( ( ( 𝑧 − 1 ) mod 2 ) = 0 ↔ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) )
7		zre	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
8		2re	⊢ 2 ∈ ℝ
9	8	a1i	⊢ ( 𝑧 ∈ ℤ → 2 ∈ ℝ )
10		1lt2	⊢ 1 < 2
11	10	a1i	⊢ ( 𝑧 ∈ ℤ → 1 < 2 )
12		m1mod0mod1	⊢ ( ( 𝑧 ∈ ℝ ∧ 2 ∈ ℝ ∧ 1 < 2 ) → ( ( ( 𝑧 − 1 ) mod 2 ) = 0 ↔ ( 𝑧 mod 2 ) = 1 ) )
13	7 9 11 12	syl3anc	⊢ ( 𝑧 ∈ ℤ → ( ( ( 𝑧 − 1 ) mod 2 ) = 0 ↔ ( 𝑧 mod 2 ) = 1 ) )
14	6 13	bitr3d	⊢ ( 𝑧 ∈ ℤ → ( ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ↔ ( 𝑧 mod 2 ) = 1 ) )
15	14	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ } = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 1 }
16	1 15	eqtri	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 1 }