Theorem dfeven3

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

	Ref	Expression
Assertion	dfeven3	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 0 }

Proof

Step	Hyp	Ref	Expression
1		df-even	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ }
2		zre	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
3		2rp	⊢ 2 ∈ ℝ+
4		mod0	⊢ ( ( 𝑧 ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( 𝑧 mod 2 ) = 0 ↔ ( 𝑧 / 2 ) ∈ ℤ ) )
5	2 3 4	sylancl	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 mod 2 ) = 0 ↔ ( 𝑧 / 2 ) ∈ ℤ ) )
6	5	bicomd	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 / 2 ) ∈ ℤ ↔ ( 𝑧 mod 2 ) = 0 ) )
7	6	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ } = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 0 }
8	1 7	eqtri	⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 0 }