# Metamath Proof Explorer

## Theorem omoe

Description: The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion omoe ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge ¬2\parallel {B}\right)\right)\to 2\parallel \left({A}-{B}\right)$

### Proof

Step Hyp Ref Expression
1 odd2np1 ${⊢}{A}\in ℤ\to \left(¬2\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\right)$
2 odd2np1 ${⊢}{B}\in ℤ\to \left(¬2\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}2{b}+1={B}\right)$
3 1 2 bi2anan9 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left(¬2\parallel {A}\wedge ¬2\parallel {B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}2{b}+1={B}\right)\right)$
4 reeanv ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left(2{a}+1={A}\wedge 2{b}+1={B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}2{b}+1={B}\right)$
5 2z ${⊢}2\in ℤ$
6 zsubcl ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}-{b}\in ℤ$
7 dvdsmul1 ${⊢}\left(2\in ℤ\wedge {a}-{b}\in ℤ\right)\to 2\parallel 2\left({a}-{b}\right)$
8 5 6 7 sylancr ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to 2\parallel 2\left({a}-{b}\right)$
9 zcn ${⊢}{a}\in ℤ\to {a}\in ℂ$
10 zcn ${⊢}{b}\in ℤ\to {b}\in ℂ$
11 2cn ${⊢}2\in ℂ$
12 mulcl ${⊢}\left(2\in ℂ\wedge {a}\in ℂ\right)\to 2{a}\in ℂ$
13 11 12 mpan ${⊢}{a}\in ℂ\to 2{a}\in ℂ$
14 mulcl ${⊢}\left(2\in ℂ\wedge {b}\in ℂ\right)\to 2{b}\in ℂ$
15 11 14 mpan ${⊢}{b}\in ℂ\to 2{b}\in ℂ$
16 ax-1cn ${⊢}1\in ℂ$
17 pnpcan2 ${⊢}\left(2{a}\in ℂ\wedge 2{b}\in ℂ\wedge 1\in ℂ\right)\to 2{a}+1-\left(2{b}+1\right)=2{a}-2{b}$
18 16 17 mp3an3 ${⊢}\left(2{a}\in ℂ\wedge 2{b}\in ℂ\right)\to 2{a}+1-\left(2{b}+1\right)=2{a}-2{b}$
19 13 15 18 syl2an ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2{a}+1-\left(2{b}+1\right)=2{a}-2{b}$
20 subdi ${⊢}\left(2\in ℂ\wedge {a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}-{b}\right)=2{a}-2{b}$
21 11 20 mp3an1 ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2\left({a}-{b}\right)=2{a}-2{b}$
22 19 21 eqtr4d ${⊢}\left({a}\in ℂ\wedge {b}\in ℂ\right)\to 2{a}+1-\left(2{b}+1\right)=2\left({a}-{b}\right)$
23 9 10 22 syl2an ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to 2{a}+1-\left(2{b}+1\right)=2\left({a}-{b}\right)$
24 8 23 breqtrrd ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to 2\parallel \left(2{a}+1-\left(2{b}+1\right)\right)$
25 oveq12 ${⊢}\left(2{a}+1={A}\wedge 2{b}+1={B}\right)\to 2{a}+1-\left(2{b}+1\right)={A}-{B}$
26 25 breq2d ${⊢}\left(2{a}+1={A}\wedge 2{b}+1={B}\right)\to \left(2\parallel \left(2{a}+1-\left(2{b}+1\right)\right)↔2\parallel \left({A}-{B}\right)\right)$
27 24 26 syl5ibcom ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left(\left(2{a}+1={A}\wedge 2{b}+1={B}\right)\to 2\parallel \left({A}-{B}\right)\right)$
28 27 rexlimivv ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left(2{a}+1={A}\wedge 2{b}+1={B}\right)\to 2\parallel \left({A}-{B}\right)$
29 4 28 sylbir ${⊢}\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}2{a}+1={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}2{b}+1={B}\right)\to 2\parallel \left({A}-{B}\right)$
30 3 29 syl6bi ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left(¬2\parallel {A}\wedge ¬2\parallel {B}\right)\to 2\parallel \left({A}-{B}\right)\right)$
31 30 imp ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left(¬2\parallel {A}\wedge ¬2\parallel {B}\right)\right)\to 2\parallel \left({A}-{B}\right)$
32 31 an4s ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left({B}\in ℤ\wedge ¬2\parallel {B}\right)\right)\to 2\parallel \left({A}-{B}\right)$