This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )