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\in \mathrm{Even}\leftrightarrow \left(Z\in \mathbb{Z}\wedge 2\gcd Z=2\right)$$

Proof

Step	Hyp	Ref	Expression
1		iseven2	$$⊢Z\in \mathrm{Even}\leftrightarrow \left(Z\in \mathbb{Z}\wedge 2\parallel Z\right)$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		gcdzeq	$$⊢\left(2\in \mathbb{N}\wedge Z\in \mathbb{Z}\right)\to \left(2\gcd Z=2\leftrightarrow 2\parallel Z\right)$$
4	2 3	mpan	$$⊢Z\in \mathbb{Z}\to \left(2\gcd Z=2\leftrightarrow 2\parallel Z\right)$$
5	4	bicomd	$$⊢Z\in \mathbb{Z}\to \left(2\parallel Z\leftrightarrow 2\gcd Z=2\right)$$
6	5	pm5.32i	$$⊢\left(Z\in \mathbb{Z}\wedge 2\parallel Z\right)\leftrightarrow \left(Z\in \mathbb{Z}\wedge 2\gcd Z=2\right)$$
7	1 6	bitri	$$⊢Z\in \mathrm{Even}\leftrightarrow \left(Z\in \mathbb{Z}\wedge 2\gcd Z=2\right)$$