This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evensumeven

Description: If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020)

Ref Expression
Assertion evensumeven ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )

Proof

Step Hyp Ref Expression
1 epee ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + 𝐵 ) ∈ Even )
2 1 expcom ⊢ ( 𝐵 ∈ Even → ( 𝐴 ∈ Even → ( 𝐴 + 𝐵 ) ∈ Even ) )
3 2 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even → ( 𝐴 + 𝐵 ) ∈ Even ) )
4 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
5 evenz ⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℤ )
6 5 zcnd ⊢ ( 𝐵 ∈ Even → 𝐵 ∈ ℂ )
7 pncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
8 4 6 7 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
10 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → 𝐵 ∈ Even )
11 10 anim1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( 𝐵 ∈ Even ∧ ( 𝐴 + 𝐵 ) ∈ Even ) )
12 11 ancomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) ∈ Even ∧ 𝐵 ∈ Even ) )
13 emee ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ Even ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) ∈ Even )
14 12 13 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) ∈ Even )
15 9 14 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) ∧ ( 𝐴 + 𝐵 ) ∈ Even ) → 𝐴 ∈ Even )
16 15 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( ( 𝐴 + 𝐵 ) ∈ Even → 𝐴 ∈ Even ) )
17 3 16 impbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → ( 𝐴 ∈ Even ↔ ( 𝐴 + 𝐵 ) ∈ Even ) )