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	|- ( Z e. ZZ -> ( 2 || Z <-> ( 2 gcd Z ) = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	|- 2 e. NN
2		gcdzeq	|- ( ( 2 e. NN /\ Z e. ZZ ) -> ( ( 2 gcd Z ) = 2 <-> 2 || Z ) )
3	1 2	mpan	|- ( Z e. ZZ -> ( ( 2 gcd Z ) = 2 <-> 2 || Z ) )
4	3	bicomd	|- ( Z e. ZZ -> ( 2 || Z <-> ( 2 gcd Z ) = 2 ) )