dfodd4

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

		Ref	Expression
	Assertion	dfodd4	$⊢ Odd = \{z \in ℤ \| z \mod 2 = 1\}$

Step	Hyp	Ref	Expression
1		dfodd2	$⊢ Odd = \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\}$
2		peano2zm	$⊢ z \in ℤ \to z - 1 \in ℤ$
3	2	zred	$⊢ z \in ℤ \to z - 1 \in ℝ$
4		2rp	$⊢ 2 \in ℝ^{+}$
5		mod0	$⊢ (z - 1 \in ℝ \land 2 \in ℝ^{+}) \to ((z - 1) \mod 2 = 0 \leftrightarrow \frac{z - 1}{2} \in ℤ)$
6	3 4 5	sylancl	$⊢ z \in ℤ \to ((z - 1) \mod 2 = 0 \leftrightarrow \frac{z - 1}{2} \in ℤ)$
7		zre	$⊢ z \in ℤ \to z \in ℝ$
8		2re	$⊢ 2 \in ℝ$
9	8	a1i	$⊢ z \in ℤ \to 2 \in ℝ$
10		1lt2	$⊢ 1 < 2$
11	10	a1i	$⊢ z \in ℤ \to 1 < 2$
12		m1mod0mod1	$⊢ (z \in ℝ \land 2 \in ℝ \land 1 < 2) \to ((z - 1) \mod 2 = 0 \leftrightarrow z \mod 2 = 1)$
13	7 9 11 12	syl3anc	$⊢ z \in ℤ \to ((z - 1) \mod 2 = 0 \leftrightarrow z \mod 2 = 1)$
14	6 13	bitr3d	$⊢ z \in ℤ \to (\frac{z - 1}{2} \in ℤ \leftrightarrow z \mod 2 = 1)$
15	14	rabbiia	$⊢ \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\} = \{z \in ℤ \| z \mod 2 = 1\}$
16	1 15	eqtri	$⊢ Odd = \{z \in ℤ \| z \mod 2 = 1\}$

Metamath Proof Explorer