Metamath Proof Explorer

Theorem omoeALTV

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

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

Proof

Step Hyp Ref Expression
1 oddz ⊢ A ∈ Odd → A ∈ ℤ
2 1 zcnd ⊢ A ∈ Odd → 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 ∈ Odd ∧ B ∈ Odd → A + − B = A − B
7 onego ⊢ B ∈ Odd → − B ∈ Odd
8 opoeALTV ⊢ A ∈ Odd ∧ − B ∈ Odd → A + − B ∈ Even
9 7 8 sylan2 ⊢ A ∈ Odd ∧ B ∈ Odd → A + − B ∈ Even
10 6 9 eqeltrrd ⊢ A ∈ Odd ∧ B ∈ Odd → A − B ∈ Even