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 Even A Even

Proof

Step Hyp Ref Expression
1 znegcl A A
2 1 adantr A A 2 A
3 znegcl A 2 A 2
4 3 adantl A A 2 A 2
5 zcn A A
6 2cnd A 2
7 2ne0 2 0
8 7 a1i A 2 0
9 5 6 8 3jca A A 2 2 0
10 9 adantr A A 2 A 2 2 0
11 divneg A 2 2 0 A 2 = A 2
12 11 eleq1d A 2 2 0 A 2 A 2
13 10 12 syl A A 2 A 2 A 2
14 4 13 mpbid A A 2 A 2
15 2 14 jca A A 2 A A 2
16 iseven A Even A A 2
17 iseven A Even A A 2
18 15 16 17 3imtr4i A Even A Even