Metamath Proof Explorer

Theorem omeoALTV

Description: The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by AV, 20-Jun-2020)

Ref Expression
Assertion omeoALTV ⊢ A ∈ Odd ∧ B ∈ Even → A − B ∈ Odd

Proof

Step Hyp Ref Expression
1 oddz ⊢ A ∈ Odd → A ∈ ℤ
2 1 zcnd ⊢ A ∈ Odd → A ∈ ℂ
3 evenz ⊢ B ∈ Even → B ∈ ℤ
4 3 zcnd ⊢ B ∈ Even → B ∈ ℂ
5 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 2 4 5 syl2an ⊢ A ∈ Odd ∧ B ∈ Even → A + − B = A − B
7 enege ⊢ B ∈ Even → − B ∈ Even
8 opeoALTV ⊢ A ∈ Odd ∧ − B ∈ Even → A + − B ∈ Odd
9 7 8 sylan2 ⊢ A ∈ Odd ∧ B ∈ Even → A + − B ∈ Odd
10 6 9 eqeltrrd ⊢ A ∈ Odd ∧ B ∈ Even → A − B ∈ Odd