Theorem evenz

Description: An even number is an integer. (Contributed by AV, 14-Jun-2020)

	Ref	Expression
Assertion	evenz	|- ( Z e. Even -> Z e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		iseven	|- ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
2	1	simplbi	|- ( Z e. Even -> Z e. ZZ )