Metamath Proof Explorer

Theorem emoo

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

Ref Expression
Assertion emoo ⊢ 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 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 2 4 5 syl2an ⊢ A ∈ Even ∧ B ∈ Odd → A + − B = A − B
7 onego ⊢ B ∈ Odd → − B ∈ Odd
8 epoo ⊢ A ∈ Even ∧ − B ∈ Odd → A + − B ∈ Odd
9 7 8 sylan2 ⊢ A ∈ Even ∧ B ∈ Odd → A + − B ∈ Odd
10 6 9 eqeltrrd ⊢ A ∈ Even ∧ B ∈ Odd → A − B ∈ Odd