Metamath Proof Explorer

Theorem opeo

Description: The sum 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 opeo ⊢ 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 zaddcl ⊢ a ∈ ℤ ∧ b ∈ ℤ → a + b ∈ ℤ
8 zcn ⊢ a ∈ ℤ → a ∈ ℂ
9 zcn ⊢ b ∈ ℤ → b ∈ ℂ
10 2cn ⊢ 2 ∈ ℂ
11 adddi ⊢ 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 add32 ⊢ 2 ⁢ a ∈ ℂ ∧ 2 ⁢ b ∈ ℂ ∧ 1 ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 = 2 ⁢ a + 1 + 2 ⁢ b
20 18 19 mp3an3 ⊢ 2 ⁢ a ∈ ℂ ∧ 2 ⁢ b ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 = 2 ⁢ a + 1 + 2 ⁢ b
21 15 17 20 syl2an ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 = 2 ⁢ a + 1 + 2 ⁢ b
22 mulcom ⊢ 2 ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ b = b ⋅ 2
23 10 22 mpan ⊢ b ∈ ℂ → 2 ⁢ b = b ⋅ 2
24 23 adantl ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ b = b ⋅ 2
25 24 oveq2d ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + 1 + 2 ⁢ b = 2 ⁢ a + 1 + b ⋅ 2
26 13 21 25 3eqtrd ⊢ 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 zaddcl ⊢ 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