Metamath Proof Explorer

Theorem iseven

Description: The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020)

Ref Expression
Assertion iseven ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ Z 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ z = Z → z 2 = Z 2
2 1 eleq1d ⊢ z = Z → z 2 ∈ ℤ ↔ Z 2 ∈ ℤ
3 df-even ⊢ Even = z ∈ ℤ | z 2 ∈ ℤ
4 2 3 elrab2 ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ Z 2 ∈ ℤ