Theorem 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 ) )