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 biimtrdi ⊢ 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