Description: 6 is an even number. (Contributed by AV, 20-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | 6even | ⊢ 6 ∈ Even |
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 |