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 ⊢ A ∈ ℤ ∧ B ∈ Even → A ∈ Even ↔ A + B ∈ Even

Proof

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