Description: The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | emoo | ⊢ ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → ( 𝐴 − 𝐵 ) ∈ Odd ) |
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 ) |