Theorem dfeven2

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

	Ref	Expression
Assertion	dfeven2	⊢ Even = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }

Proof

Step	Hyp	Ref	Expression
1		dfeven4	⊢ Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }
2		eqcom	⊢ ( 𝑧 = ( 2 · 𝑖 ) ↔ ( 2 · 𝑖 ) = 𝑧 )
3		2cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
4		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
5	4	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
6	3 5	mulcomd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 2 · 𝑖 ) = ( 𝑖 · 2 ) )
7	6	eqeq1d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 2 · 𝑖 ) = 𝑧 ↔ ( 𝑖 · 2 ) = 𝑧 ) )
8	2 7	bitrid	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ ( 𝑖 · 2 ) = 𝑧 ) )
9	8	rexbidva	⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
10		2z	⊢ 2 ∈ ℤ
11		divides	⊢ ( ( 2 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 2 ∥ 𝑧 ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
12	10 11	mpan	⊢ ( 𝑧 ∈ ℤ → ( 2 ∥ 𝑧 ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
13	9 12	bitr4d	⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ↔ 2 ∥ 𝑧 ) )
14	13	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) } = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }
15	1 14	eqtri	⊢ Even = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }