Theorem enege

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

	Ref	Expression
Assertion	enege	|- ( A e. Even -> -u A e. Even )

Proof

Step	Hyp	Ref	Expression
1		znegcl	|- ( A e. ZZ -> -u A e. ZZ )
2	1	adantr	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> -u A e. ZZ )
3		znegcl	|- ( ( A / 2 ) e. ZZ -> -u ( A / 2 ) e. ZZ )
4	3	adantl	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> -u ( A / 2 ) e. ZZ )
5		zcn	|- ( A e. ZZ -> A e. CC )
6		2cnd	|- ( A e. ZZ -> 2 e. CC )
7		2ne0	|- 2 =/= 0
8	7	a1i	|- ( A e. ZZ -> 2 =/= 0 )
9	5 6 8	3jca	|- ( A e. ZZ -> ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
10	9	adantr	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
11		divneg	|- ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( A / 2 ) = ( -u A / 2 ) )
12	11	eleq1d	|- ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( -u ( A / 2 ) e. ZZ <-> ( -u A / 2 ) e. ZZ ) )
13	10 12	syl	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> ( -u ( A / 2 ) e. ZZ <-> ( -u A / 2 ) e. ZZ ) )
14	4 13	mpbid	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> ( -u A / 2 ) e. ZZ )
15	2 14	jca	|- ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> ( -u A e. ZZ /\ ( -u A / 2 ) e. ZZ ) )
16		iseven	|- ( A e. Even <-> ( A e. ZZ /\ ( A / 2 ) e. ZZ ) )
17		iseven	|- ( -u A e. Even <-> ( -u A e. ZZ /\ ( -u A / 2 ) e. ZZ ) )
18	15 16 17	3imtr4i	|- ( A e. Even -> -u A e. Even )