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