Theorem 8even

Description: 8 is an even number. (Contributed by AV, 23-Jul-2020)

	Ref	Expression
Assertion	8even	⊢ 8 ∈ Even

Proof

Step	Hyp	Ref	Expression
1		8nn	⊢ 8 ∈ ℕ
2	1	nnzi	⊢ 8 ∈ ℤ
3		4t2e8	⊢ ( 4 · 2 ) = 8
4	3	eqcomi	⊢ 8 = ( 4 · 2 )
5	4	oveq1i	⊢ ( 8 / 2 ) = ( ( 4 · 2 ) / 2 )
6		4cn	⊢ 4 ∈ ℂ
7		2cn	⊢ 2 ∈ ℂ
8		2ne0	⊢ 2 ≠ 0
9	6 7 8	divcan4i	⊢ ( ( 4 · 2 ) / 2 ) = 4
10	5 9	eqtri	⊢ ( 8 / 2 ) = 4
11		4z	⊢ 4 ∈ ℤ
12	10 11	eqeltri	⊢ ( 8 / 2 ) ∈ ℤ
13		iseven	⊢ ( 8 ∈ Even ↔ ( 8 ∈ ℤ ∧ ( 8 / 2 ) ∈ ℤ ) )
14	2 12 13	mpbir2an	⊢ 8 ∈ Even