Theorem 6even

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

	Ref	Expression
Assertion	6even	⊢ 6 ∈ Even

Proof

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