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

Proof

Step	Hyp	Ref	Expression
1		iseven2	|- ( Z e. Even <-> ( Z e. ZZ /\ 2 || Z ) )
2		2nn	|- 2 e. NN
3		gcdzeq	|- ( ( 2 e. NN /\ Z e. ZZ ) -> ( ( 2 gcd Z ) = 2 <-> 2 || Z ) )
4	2 3	mpan	|- ( Z e. ZZ -> ( ( 2 gcd Z ) = 2 <-> 2 || Z ) )
5	4	bicomd	|- ( Z e. ZZ -> ( 2 || Z <-> ( 2 gcd Z ) = 2 ) )
6	5	pm5.32i	|- ( ( Z e. ZZ /\ 2 || Z ) <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 2 ) )
7	1 6	bitri	|- ( Z e. Even <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 2 ) )