Metamath Proof Explorer

Theorem epoo

Description: The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020)

Ref Expression
Assertion epoo ⊢ A ∈ Even ∧ B ∈ Odd → A + B ∈ Odd

Proof

Step Hyp Ref Expression
1 evenz ⊢ A ∈ Even → A ∈ ℤ
2 1 zcnd ⊢ A ∈ Even → A ∈ ℂ
3 oddz ⊢ B ∈ Odd → B ∈ ℤ
4 3 zcnd ⊢ B ∈ Odd → B ∈ ℂ
5 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
6 2 4 5 syl2an ⊢ A ∈ Even ∧ B ∈ Odd → A + B = B + A
7 opeoALTV ⊢ B ∈ Odd ∧ A ∈ Even → B + A ∈ Odd
8 7 ancoms ⊢ A ∈ Even ∧ B ∈ Odd → B + A ∈ Odd
9 6 8 eqeltrd ⊢ A ∈ Even ∧ B ∈ Odd → A + B ∈ Odd