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 ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → ( 𝐴𝐵 ) ∈ Odd )

Proof

Step Hyp Ref Expression
1 evenz ( 𝐴 ∈ Even → 𝐴 ∈ ℤ )
2 1 zcnd ( 𝐴 ∈ Even → 𝐴 ∈ ℂ )
3 oddz ( 𝐵 ∈ Odd → 𝐵 ∈ ℤ )
4 3 zcnd ( 𝐵 ∈ Odd → 𝐵 ∈ ℂ )
5 negsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 ) )
6 2 4 5 syl2an ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 ) )
7 onego ( 𝐵 ∈ Odd → - 𝐵 ∈ Odd )
8 epoo ( ( 𝐴 ∈ Even ∧ - 𝐵 ∈ Odd ) → ( 𝐴 + - 𝐵 ) ∈ Odd )
9 7 8 sylan2 ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → ( 𝐴 + - 𝐵 ) ∈ Odd )
10 6 9 eqeltrrd ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → ( 𝐴𝐵 ) ∈ Odd )