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