Metamath Proof Explorer

Theorem iseven5

Description: The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020)

Ref Expression
Assertion iseven5 ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ 2 gcd Z = 2

Proof

Step Hyp Ref Expression
1 iseven2 ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ 2 ∥ Z
2 2nn ⊢ 2 ∈ ℕ
3 gcdzeq ⊢ 2 ∈ ℕ ∧ Z ∈ ℤ → 2 gcd Z = 2 ↔ 2 ∥ Z
4 2 3 mpan ⊢ Z ∈ ℤ → 2 gcd Z = 2 ↔ 2 ∥ Z
5 4 bicomd ⊢ Z ∈ ℤ → 2 ∥ Z ↔ 2 gcd Z = 2
6 5 pm5.32i ⊢ Z ∈ ℤ ∧ 2 ∥ Z ↔ Z ∈ ℤ ∧ 2 gcd Z = 2
7 1 6 bitri ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ 2 gcd Z = 2