Theorem dfodd6

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

	Ref	Expression
Assertion	dfodd6	⊢ Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) }

Proof

Step	Hyp	Ref	Expression
1		dfodd2	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ }
2		simpr	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ )
3		oveq2	⊢ ( 𝑖 = ( ( 𝑧 − 1 ) / 2 ) → ( 2 · 𝑖 ) = ( 2 · ( ( 𝑧 − 1 ) / 2 ) ) )
4		peano2zm	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 − 1 ) ∈ ℤ )
5	4	zcnd	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 − 1 ) ∈ ℂ )
6		2cnd	⊢ ( 𝑧 ∈ ℤ → 2 ∈ ℂ )
7		2ne0	⊢ 2 ≠ 0
8	7	a1i	⊢ ( 𝑧 ∈ ℤ → 2 ≠ 0 )
9	5 6 8	3jca	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 − 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
10	9	adantr	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑧 − 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
11		divcan2	⊢ ( ( ( 𝑧 − 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( ( 𝑧 − 1 ) / 2 ) ) = ( 𝑧 − 1 ) )
12	10 11	syl	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → ( 2 · ( ( 𝑧 − 1 ) / 2 ) ) = ( 𝑧 − 1 ) )
13	3 12	sylan9eqr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) ∧ 𝑖 = ( ( 𝑧 − 1 ) / 2 ) ) → ( 2 · 𝑖 ) = ( 𝑧 − 1 ) )
14	13	oveq1d	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) ∧ 𝑖 = ( ( 𝑧 − 1 ) / 2 ) ) → ( ( 2 · 𝑖 ) + 1 ) = ( ( 𝑧 − 1 ) + 1 ) )
15		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
16		npcan1	⊢ ( 𝑧 ∈ ℂ → ( ( 𝑧 − 1 ) + 1 ) = 𝑧 )
17	15 16	syl	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 − 1 ) + 1 ) = 𝑧 )
18	17	adantr	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑧 − 1 ) + 1 ) = 𝑧 )
19	18	adantr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) ∧ 𝑖 = ( ( 𝑧 − 1 ) / 2 ) ) → ( ( 𝑧 − 1 ) + 1 ) = 𝑧 )
20	14 19	eqtrd	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) ∧ 𝑖 = ( ( 𝑧 − 1 ) / 2 ) ) → ( ( 2 · 𝑖 ) + 1 ) = 𝑧 )
21	20	eqeq2d	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) ∧ 𝑖 = ( ( 𝑧 − 1 ) / 2 ) ) → ( 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ↔ 𝑧 = 𝑧 ) )
22		eqidd	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → 𝑧 = 𝑧 )
23	2 21 22	rspcedvd	⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) → ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) )
24	23	ex	⊢ ( 𝑧 ∈ ℤ → ( ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ → ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) )
25		oveq1	⊢ ( 𝑧 = ( ( 2 · 𝑖 ) + 1 ) → ( 𝑧 − 1 ) = ( ( ( 2 · 𝑖 ) + 1 ) − 1 ) )
26		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
27		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 2 · 𝑖 ) ∈ ℂ )
28	6 26 27	syl2an	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 2 · 𝑖 ) ∈ ℂ )
29		pncan1	⊢ ( ( 2 · 𝑖 ) ∈ ℂ → ( ( ( 2 · 𝑖 ) + 1 ) − 1 ) = ( 2 · 𝑖 ) )
30	28 29	syl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( ( 2 · 𝑖 ) + 1 ) − 1 ) = ( 2 · 𝑖 ) )
31	25 30	sylan9eqr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → ( 𝑧 − 1 ) = ( 2 · 𝑖 ) )
32	31	oveq1d	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝑧 − 1 ) / 2 ) = ( ( 2 · 𝑖 ) / 2 ) )
33	26	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
34		2cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
35	7	a1i	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ≠ 0 )
36	33 34 35	divcan3d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 )
37	36	adantr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 )
38	32 37	eqtrd	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝑧 − 1 ) / 2 ) = 𝑖 )
39		simpr	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ )
40	39	adantr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → 𝑖 ∈ ℤ )
41	38 40	eqeltrd	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) → ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ )
42	41	rexlimdva2	⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) → ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ) )
43	24 42	impbid	⊢ ( 𝑧 ∈ ℤ → ( ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ↔ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ) )
44	43	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ } = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) }
45	1 44	eqtri	⊢ Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) }