enege

Description: The negative of an even number is even. (Contributed by AV, 20-Jun-2020)

		Ref	Expression
	Assertion	enege	$⊢ A \in Even \to - A \in Even$

Step	Hyp	Ref	Expression
1		znegcl	$⊢ A \in ℤ \to - A \in ℤ$
2	1	adantr	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to - A \in ℤ$
3		znegcl	$⊢ \frac{A}{2} \in ℤ \to - \frac{A}{2} \in ℤ$
4	3	adantl	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to - \frac{A}{2} \in ℤ$
5		zcn	$⊢ A \in ℤ \to A \in ℂ$
6		2cnd	$⊢ A \in ℤ \to 2 \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8	7	a1i	$⊢ A \in ℤ \to 2 \neq 0$
9	5 6 8	3jca	$⊢ A \in ℤ \to (A \in ℂ \land 2 \in ℂ \land 2 \neq 0)$
10	9	adantr	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to (A \in ℂ \land 2 \in ℂ \land 2 \neq 0)$
11		divneg	$⊢ (A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{A}{2} = \frac{- A}{2}$
12	11	eleq1d	$⊢ (A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to (- \frac{A}{2} \in ℤ \leftrightarrow \frac{- A}{2} \in ℤ)$
13	10 12	syl	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to (- \frac{A}{2} \in ℤ \leftrightarrow \frac{- A}{2} \in ℤ)$
14	4 13	mpbid	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to \frac{- A}{2} \in ℤ$
15	2 14	jca	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to (- A \in ℤ \land \frac{- A}{2} \in ℤ)$
16		iseven	$⊢ A \in Even \leftrightarrow (A \in ℤ \land \frac{A}{2} \in ℤ)$
17		iseven	$⊢ - A \in Even \leftrightarrow (- A \in ℤ \land \frac{- A}{2} \in ℤ)$
18	15 16 17	3imtr4i	$⊢ A \in Even \to - A \in Even$

Metamath Proof Explorer