Theorem dfeven4

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

	Ref	Expression
Assertion	dfeven4	⊢ Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }

Proof

Step	Hyp	Ref	Expression
1		df-even	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ }
2		simpr	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ( 𝑧 / 2 ) ∈ ℤ )
3		oveq2	⊢ ( 𝑖 = ( 𝑧 / 2 ) → ( 2 · 𝑖 ) = ( 2 · ( 𝑧 / 2 ) ) )
4	3	eqeq2d	⊢ ( 𝑖 = ( 𝑧 / 2 ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ 𝑧 = ( 2 · ( 𝑧 / 2 ) ) ) )
5	4	adantl	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) ∧ 𝑖 = ( 𝑧 / 2 ) ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ 𝑧 = ( 2 · ( 𝑧 / 2 ) ) ) )
6		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 𝑧 ∈ ℂ )
8		2cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 2 ∈ ℂ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 2 ≠ 0 )
11	7 8 10	divcan2d	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ( 2 · ( 𝑧 / 2 ) ) = 𝑧 )
12	11	eqcomd	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 𝑧 = ( 2 · ( 𝑧 / 2 ) ) )
13	2 5 12	rspcedvd	⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) )
14	13	ex	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 / 2 ) ∈ ℤ → ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ) )
15		oveq1	⊢ ( 𝑧 = ( 2 · 𝑖 ) → ( 𝑧 / 2 ) = ( ( 2 · 𝑖 ) / 2 ) )
16		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
17	16	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
18		2cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
19	9	a1i	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ≠ 0 )
20	17 18 19	divcan3d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 )
21	15 20	sylan9eqr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → ( 𝑧 / 2 ) = 𝑖 )
22		simpr	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ )
23	22	adantr	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → 𝑖 ∈ ℤ )
24	21 23	eqeltrd	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → ( 𝑧 / 2 ) ∈ ℤ )
25	24	rexlimdva2	⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) → ( 𝑧 / 2 ) ∈ ℤ ) )
26	14 25	impbid	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 / 2 ) ∈ ℤ ↔ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ) )
27	26	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ } = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }
28	1 27	eqtri	⊢ Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }