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 ( 𝐴 ∈ 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 )