Metamath Proof Explorer

Theorem omeo

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

Ref Expression
Assertion omeo ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A−B

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢A∈ℤ→¬2∥A↔∃a∈ℤ2⁢a+1=A
2 2z ⊢2∈ℤ
3 divides ⊢2∈ℤ∧B∈ℤ→2∥B↔∃b∈ℤb⋅2=B
4 2 3 mpan ⊢B∈ℤ→2∥B↔∃b∈ℤb⋅2=B
5 1 4 bi2anan9 ⊢A∈ℤ∧B∈ℤ→¬2∥A∧2∥B↔∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B
6 reeanv ⊢∃a∈ℤ∃b∈ℤ2⁢a+1=A∧b⋅2=B↔∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B
7 zsubcl ⊢a∈ℤ∧b∈ℤ→a−b∈ℤ
8 zcn ⊢a∈ℤ→a∈ℂ
9 zcn ⊢b∈ℤ→b∈ℂ
10 2cn ⊢2∈ℂ
11 subdi ⊢2∈ℂ∧a∈ℂ∧b∈ℂ→2⁢a−b=2⁢a−2⁢b
12 10 11 mp3an1 ⊢a∈ℂ∧b∈ℂ→2⁢a−b=2⁢a−2⁢b
13 12 oveq1d ⊢a∈ℂ∧b∈ℂ→2⁢a−b+1=2⁢a-2⁢b+1
14 mulcl ⊢2∈ℂ∧a∈ℂ→2⁢a∈ℂ
15 10 14 mpan ⊢a∈ℂ→2⁢a∈ℂ
16 mulcl ⊢2∈ℂ∧b∈ℂ→2⁢b∈ℂ
17 10 16 mpan ⊢b∈ℂ→2⁢b∈ℂ
18 ax-1cn ⊢1∈ℂ
19 addsub ⊢2⁢a∈ℂ∧1∈ℂ∧2⁢b∈ℂ→2⁢a+1-2⁢b=2⁢a-2⁢b+1
20 18 19 mp3an2 ⊢2⁢a∈ℂ∧2⁢b∈ℂ→2⁢a+1-2⁢b=2⁢a-2⁢b+1
21 15 17 20 syl2an ⊢a∈ℂ∧b∈ℂ→2⁢a+1-2⁢b=2⁢a-2⁢b+1
22 mulcom ⊢2∈ℂ∧b∈ℂ→2⁢b=b⋅2
23 10 22 mpan ⊢b∈ℂ→2⁢b=b⋅2
24 23 oveq2d ⊢b∈ℂ→2⁢a+1-2⁢b=2⁢a+1-b⋅2
25 24 adantl ⊢a∈ℂ∧b∈ℂ→2⁢a+1-2⁢b=2⁢a+1-b⋅2
26 13 21 25 3eqtr2d ⊢a∈ℂ∧b∈ℂ→2⁢a−b+1=2⁢a+1-b⋅2
27 8 9 26 syl2an ⊢a∈ℤ∧b∈ℤ→2⁢a−b+1=2⁢a+1-b⋅2
28 oveq2 ⊢c=a−b→2⁢c=2⁢a−b
29 28 oveq1d ⊢c=a−b→2⁢c+1=2⁢a−b+1
30 29 eqeq1d ⊢c=a−b→2⁢c+1=2⁢a+1-b⋅2↔2⁢a−b+1=2⁢a+1-b⋅2
31 30 rspcev ⊢a−b∈ℤ∧2⁢a−b+1=2⁢a+1-b⋅2→∃c∈ℤ2⁢c+1=2⁢a+1-b⋅2
32 7 27 31 syl2anc ⊢a∈ℤ∧b∈ℤ→∃c∈ℤ2⁢c+1=2⁢a+1-b⋅2
33 oveq12 ⊢2⁢a+1=A∧b⋅2=B→2⁢a+1-b⋅2=A−B
34 33 eqeq2d ⊢2⁢a+1=A∧b⋅2=B→2⁢c+1=2⁢a+1-b⋅2↔2⁢c+1=A−B
35 34 rexbidv ⊢2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=2⁢a+1-b⋅2↔∃c∈ℤ2⁢c+1=A−B
36 32 35 syl5ibcom ⊢a∈ℤ∧b∈ℤ→2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=A−B
37 36 rexlimivv ⊢∃a∈ℤ∃b∈ℤ2⁢a+1=A∧b⋅2=B→∃c∈ℤ2⁢c+1=A−B
38 6 37 sylbir ⊢∃a∈ℤ2⁢a+1=A∧∃b∈ℤb⋅2=B→∃c∈ℤ2⁢c+1=A−B
39 5 38 syl6bi ⊢A∈ℤ∧B∈ℤ→¬2∥A∧2∥B→∃c∈ℤ2⁢c+1=A−B
40 39 imp ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧2∥B→∃c∈ℤ2⁢c+1=A−B
41 40 an4s ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→∃c∈ℤ2⁢c+1=A−B
42 zsubcl ⊢A∈ℤ∧B∈ℤ→A−B∈ℤ
43 42 ad2ant2r ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→A−B∈ℤ
44 odd2np1 ⊢A−B∈ℤ→¬2∥A−B↔∃c∈ℤ2⁢c+1=A−B
45 43 44 syl ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A−B↔∃c∈ℤ2⁢c+1=A−B
46 41 45 mpbird ⊢A∈ℤ∧¬2∥A∧B∈ℤ∧2∥B→¬2∥A−B