Metamath Proof Explorer


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