Metamath Proof Explorer


Theorem enege

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

Ref Expression
Assertion enege ( 𝐴 ∈ Even → - 𝐴 ∈ Even )

Proof

Step Hyp Ref Expression
1 znegcl ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
2 1 adantr ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → - 𝐴 ∈ ℤ )
3 znegcl ( ( 𝐴 / 2 ) ∈ ℤ → - ( 𝐴 / 2 ) ∈ ℤ )
4 3 adantl ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → - ( 𝐴 / 2 ) ∈ ℤ )
5 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
6 2cnd ( 𝐴 ∈ ℤ → 2 ∈ ℂ )
7 2ne0 2 ≠ 0
8 7 a1i ( 𝐴 ∈ ℤ → 2 ≠ 0 )
9 5 6 8 3jca ( 𝐴 ∈ ℤ → ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
10 9 adantr ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
11 divneg ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 𝐴 / 2 ) = ( - 𝐴 / 2 ) )
12 11 eleq1d ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( - ( 𝐴 / 2 ) ∈ ℤ ↔ ( - 𝐴 / 2 ) ∈ ℤ ) )
13 10 12 syl ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - ( 𝐴 / 2 ) ∈ ℤ ↔ ( - 𝐴 / 2 ) ∈ ℤ ) )
14 4 13 mpbid ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - 𝐴 / 2 ) ∈ ℤ )
15 2 14 jca ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) → ( - 𝐴 ∈ ℤ ∧ ( - 𝐴 / 2 ) ∈ ℤ ) )
16 iseven ( 𝐴 ∈ Even ↔ ( 𝐴 ∈ ℤ ∧ ( 𝐴 / 2 ) ∈ ℤ ) )
17 iseven ( - 𝐴 ∈ Even ↔ ( - 𝐴 ∈ ℤ ∧ ( - 𝐴 / 2 ) ∈ ℤ ) )
18 15 16 17 3imtr4i ( 𝐴 ∈ Even → - 𝐴 ∈ Even )