Metamath Proof Explorer
Description: 2 is an even number. (Contributed by AV, 12-Feb-2020) (Revised by AV, 18-Jun-2020)
|
|
Ref |
Expression |
|
Assertion |
2evenALTV |
⊢ 2 ∈ Even |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
2z |
⊢ 2 ∈ ℤ |
2 |
|
2div2e1 |
⊢ ( 2 / 2 ) = 1 |
3 |
|
1z |
⊢ 1 ∈ ℤ |
4 |
2 3
|
eqeltri |
⊢ ( 2 / 2 ) ∈ ℤ |
5 |
|
iseven |
⊢ ( 2 ∈ Even ↔ ( 2 ∈ ℤ ∧ ( 2 / 2 ) ∈ ℤ ) ) |
6 |
1 4 5
|
mpbir2an |
⊢ 2 ∈ Even |