This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary prime number theory Coprimality and Euclid's lemma (cont.) isevengcd2
Description: The predicate "is an even number". An even number and 2 have 2 as
greatest common divisor. (Contributed by AV , 1-Jul-2020) (Revised by AV , 8-Aug-2021)
Ref
Expression
Assertion
isevengcd2 ⊢ ( 𝑍 ∈ ℤ → ( 2 ∥ 𝑍 ↔ ( 2 gcd 𝑍 ) = 2 ) )
Proof
Step
Hyp
Ref
Expression
1
2nn ⊢ 2 ∈ ℕ
2
gcdzeq ⊢ ( ( 2 ∈ ℕ ∧ 𝑍 ∈ ℤ ) → ( ( 2 gcd 𝑍 ) = 2 ↔ 2 ∥ 𝑍 ) )
3
1 2
mpan ⊢ ( 𝑍 ∈ ℤ → ( ( 2 gcd 𝑍 ) = 2 ↔ 2 ∥ 𝑍 ) )
4
3
bicomd ⊢ ( 𝑍 ∈ ℤ → ( 2 ∥ 𝑍 ↔ ( 2 gcd 𝑍 ) = 2 ) )