dfodd6

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

		Ref	Expression
	Assertion	dfodd6	$⊢ Odd = \{z \in ℤ \| \exists i \in ℤ z = 2 i + 1\}$

Proof

Step	Hyp	Ref	Expression
1		dfodd2	$⊢ Odd = \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\}$
2		simpr	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to \frac{z - 1}{2} \in ℤ$
3		oveq2	$⊢ i = \frac{z - 1}{2} \to 2 i = 2 (\frac{z - 1}{2})$
4		peano2zm	$⊢ z \in ℤ \to z - 1 \in ℤ$
5	4	zcnd	$⊢ z \in ℤ \to z - 1 \in ℂ$
6		2cnd	$⊢ z \in ℤ \to 2 \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8	7	a1i	$⊢ z \in ℤ \to 2 \neq 0$
9	5 6 8	3jca	$⊢ z \in ℤ \to (z - 1 \in ℂ \land 2 \in ℂ \land 2 \neq 0)$
10	9	adantr	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to (z - 1 \in ℂ \land 2 \in ℂ \land 2 \neq 0)$
11		divcan2	$⊢ (z - 1 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{z - 1}{2}) = z - 1$
12	10 11	syl	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to 2 (\frac{z - 1}{2}) = z - 1$
13	3 12	sylan9eqr	$⊢ ((z \in ℤ \land \frac{z - 1}{2} \in ℤ) \land i = \frac{z - 1}{2}) \to 2 i = z - 1$
14	13	oveq1d	$⊢ ((z \in ℤ \land \frac{z - 1}{2} \in ℤ) \land i = \frac{z - 1}{2}) \to 2 i + 1 = z - 1 + 1$
15		zcn	$⊢ z \in ℤ \to z \in ℂ$
16		npcan1	$⊢ z \in ℂ \to z - 1 + 1 = z$
17	15 16	syl	$⊢ z \in ℤ \to z - 1 + 1 = z$
18	17	adantr	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to z - 1 + 1 = z$
19	18	adantr	$⊢ ((z \in ℤ \land \frac{z - 1}{2} \in ℤ) \land i = \frac{z - 1}{2}) \to z - 1 + 1 = z$
20	14 19	eqtrd	$⊢ ((z \in ℤ \land \frac{z - 1}{2} \in ℤ) \land i = \frac{z - 1}{2}) \to 2 i + 1 = z$
21	20	eqeq2d	$⊢ ((z \in ℤ \land \frac{z - 1}{2} \in ℤ) \land i = \frac{z - 1}{2}) \to (z = 2 i + 1 \leftrightarrow z = z)$
22		eqidd	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to z = z$
23	2 21 22	rspcedvd	$⊢ (z \in ℤ \land \frac{z - 1}{2} \in ℤ) \to \exists i \in ℤ z = 2 i + 1$
24	23	ex	$⊢ z \in ℤ \to (\frac{z - 1}{2} \in ℤ \to \exists i \in ℤ z = 2 i + 1)$
25		oveq1	$⊢ z = 2 i + 1 \to z - 1 = 2 i + 1 - 1$
26		zcn	$⊢ i \in ℤ \to i \in ℂ$
27		mulcl	$⊢ (2 \in ℂ \land i \in ℂ) \to 2 i \in ℂ$
28	6 26 27	syl2an	$⊢ (z \in ℤ \land i \in ℤ) \to 2 i \in ℂ$
29		pncan1	$⊢ 2 i \in ℂ \to 2 i + 1 - 1 = 2 i$
30	28 29	syl	$⊢ (z \in ℤ \land i \in ℤ) \to 2 i + 1 - 1 = 2 i$
31	25 30	sylan9eqr	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to z - 1 = 2 i$
32	31	oveq1d	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to \frac{z - 1}{2} = \frac{2 i}{2}$
33	26	adantl	$⊢ (z \in ℤ \land i \in ℤ) \to i \in ℂ$
34		2cnd	$⊢ (z \in ℤ \land i \in ℤ) \to 2 \in ℂ$
35	7	a1i	$⊢ (z \in ℤ \land i \in ℤ) \to 2 \neq 0$
36	33 34 35	divcan3d	$⊢ (z \in ℤ \land i \in ℤ) \to \frac{2 i}{2} = i$
37	36	adantr	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to \frac{2 i}{2} = i$
38	32 37	eqtrd	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to \frac{z - 1}{2} = i$
39		simpr	$⊢ (z \in ℤ \land i \in ℤ) \to i \in ℤ$
40	39	adantr	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to i \in ℤ$
41	38 40	eqeltrd	$⊢ ((z \in ℤ \land i \in ℤ) \land z = 2 i + 1) \to \frac{z - 1}{2} \in ℤ$
42	41	rexlimdva2	$⊢ z \in ℤ \to (\exists i \in ℤ z = 2 i + 1 \to \frac{z - 1}{2} \in ℤ)$
43	24 42	impbid	$⊢ z \in ℤ \to (\frac{z - 1}{2} \in ℤ \leftrightarrow \exists i \in ℤ z = 2 i + 1)$
44	43	rabbiia	$⊢ \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\} = \{z \in ℤ \| \exists i \in ℤ z = 2 i + 1\}$
45	1 44	eqtri	$⊢ Odd = \{z \in ℤ \| \exists i \in ℤ z = 2 i + 1\}$

Metamath Proof Explorer

Theorem dfodd6

Proof