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∈ℤ∧A2∈ℤ→−A∈ℤ
3 znegcl ⊢A2∈ℤ→−A2∈ℤ
4 3 adantl ⊢A∈ℤ∧A2∈ℤ→−A2∈ℤ
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∈ℤ∧A2∈ℤ→A∈ℂ∧2∈ℂ∧2≠0
11 divneg ⊢A∈ℂ∧2∈ℂ∧2≠0→−A2=−A2
12 11 eleq1d ⊢A∈ℂ∧2∈ℂ∧2≠0→−A2∈ℤ↔−A2∈ℤ
13 10 12 syl ⊢A∈ℤ∧A2∈ℤ→−A2∈ℤ↔−A2∈ℤ
14 4 13 mpbid ⊢A∈ℤ∧A2∈ℤ→−A2∈ℤ
15 2 14 jca ⊢A∈ℤ∧A2∈ℤ→−A∈ℤ∧−A2∈ℤ
16 iseven ⊢A∈Even↔A∈ℤ∧A2∈ℤ
17 iseven ⊢−A∈Even↔−A∈ℤ∧−A2∈ℤ
18 15 16 17 3imtr4i ⊢A∈Even→−A∈Even