This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2evenALTV

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