Theorem enege

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

	Ref	Expression
Assertion	enege	⊢ ( 𝐴 ∈ Even → - 𝐴 ∈ Even )

Proof

Step	Hyp	Ref	Expression
1		znegcl	⊢ ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → - 𝐴 ∈ ℤ )
3		znegcl	⊢ ( ( 𝐴 / 2 ) ∈ ℤ → - ( 𝐴 / 2 ) ∈ ℤ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → - ( 𝐴 / 2 ) ∈ ℤ )
5		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
6		2cnd	⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℂ )
7		2ne0	⊢ 2 ≠ 0
8	7	a1i	⊢ ( 𝐴 ∈ ℤ → 2 ≠ 0 )
9	5 6 8	3jca	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
11		divneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 𝐴 / 2 ) = ( - 𝐴 / 2 ) )
12	11	eleq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( - ( 𝐴 / 2 ) ∈ ℤ ↔ ( - 𝐴 / 2 ) ∈ ℤ ) )
13	10 12	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - ( 𝐴 / 2 ) ∈ ℤ ↔ ( - 𝐴 / 2 ) ∈ ℤ ) )
14	4 13	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - 𝐴 / 2 ) ∈ ℤ )
15	2 14	jca	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - 𝐴 ∈ ℤ ∧ ( - 𝐴 / 2 ) ∈ ℤ ) )
16		iseven	⊢ ( 𝐴 ∈ Even ↔ ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) )
17		iseven	⊢ ( - 𝐴 ∈ Even ↔ ( - 𝐴 ∈ ℤ ∧ ( - 𝐴 / 2 ) ∈ ℤ ) )
18	15 16 17	3imtr4i	⊢ ( 𝐴 ∈ Even → - 𝐴 ∈ Even )