Metamath Proof Explorer

Theorem opoe

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

Ref Expression
Assertion opoe ⊢ 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 odd2np1 ⊢ B ∈ ℤ → ¬ 2 ∥ B ↔ ∃ b ∈ ℤ 2 ⁢ b + 1 = B
3 1 2 bi2anan9 ⊢ A ∈ ℤ ∧ B ∈ ℤ → ¬ 2 ∥ A ∧ ¬ 2 ∥ B ↔ ∃ a ∈ ℤ 2 ⁢ a + 1 = A ∧ ∃ b ∈ ℤ 2 ⁢ b + 1 = B
4 reeanv ⊢ ∃ a ∈ ℤ ∃ b ∈ ℤ 2 ⁢ a + 1 = A ∧ 2 ⁢ b + 1 = B ↔ ∃ a ∈ ℤ 2 ⁢ a + 1 = A ∧ ∃ b ∈ ℤ 2 ⁢ b + 1 = B
5 2z ⊢ 2 ∈ ℤ
6 zaddcl ⊢ a ∈ ℤ ∧ b ∈ ℤ → a + b ∈ ℤ
7 6 peano2zd ⊢ a ∈ ℤ ∧ b ∈ ℤ → a + b + 1 ∈ ℤ
8 dvdsmul1 ⊢ 2 ∈ ℤ ∧ a + b + 1 ∈ ℤ → 2 ∥ 2 ⁢ a + b + 1
9 5 7 8 sylancr ⊢ a ∈ ℤ ∧ b ∈ ℤ → 2 ∥ 2 ⁢ a + b + 1
10 zcn ⊢ a ∈ ℤ → a ∈ ℂ
11 zcn ⊢ b ∈ ℤ → b ∈ ℂ
12 addcl ⊢ a ∈ ℂ ∧ b ∈ ℂ → a + b ∈ ℂ
13 2cn ⊢ 2 ∈ ℂ
14 ax-1cn ⊢ 1 ∈ ℂ
15 adddi ⊢ 2 ∈ ℂ ∧ a + b ∈ ℂ ∧ 1 ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + b + 2 ⋅ 1
16 13 14 15 mp3an13 ⊢ a + b ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + b + 2 ⋅ 1
17 12 16 syl ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + b + 2 ⋅ 1
18 adddi ⊢ 2 ∈ ℂ ∧ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b = 2 ⁢ a + 2 ⁢ b
19 13 18 mp3an1 ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b = 2 ⁢ a + 2 ⁢ b
20 19 oveq1d ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b + 2 ⋅ 1 = 2 ⁢ a + 2 ⁢ b + 2 ⋅ 1
21 17 20 eqtrd ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + 2 ⁢ b + 2 ⋅ 1
22 2t1e2 ⊢ 2 ⋅ 1 = 2
23 df-2 ⊢ 2 = 1 + 1
24 22 23 eqtri ⊢ 2 ⋅ 1 = 1 + 1
25 24 oveq2i ⊢ 2 ⁢ a + 2 ⁢ b + 2 ⋅ 1 = 2 ⁢ a + 2 ⁢ b + 1 + 1
26 21 25 eqtrdi ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + 2 ⁢ b + 1 + 1
27 mulcl ⊢ 2 ∈ ℂ ∧ a ∈ ℂ → 2 ⁢ a ∈ ℂ
28 13 27 mpan ⊢ a ∈ ℂ → 2 ⁢ a ∈ ℂ
29 mulcl ⊢ 2 ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ b ∈ ℂ
30 13 29 mpan ⊢ b ∈ ℂ → 2 ⁢ b ∈ ℂ
31 add4 ⊢ 2 ⁢ a ∈ ℂ ∧ 2 ⁢ b ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 + 1 = 2 ⁢ a + 1 + 2 ⁢ b + 1
32 14 14 31 mpanr12 ⊢ 2 ⁢ a ∈ ℂ ∧ 2 ⁢ b ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 + 1 = 2 ⁢ a + 1 + 2 ⁢ b + 1
33 28 30 32 syl2an ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + 2 ⁢ b + 1 + 1 = 2 ⁢ a + 1 + 2 ⁢ b + 1
34 26 33 eqtrd ⊢ a ∈ ℂ ∧ b ∈ ℂ → 2 ⁢ a + b + 1 = 2 ⁢ a + 1 + 2 ⁢ b + 1
35 10 11 34 syl2an ⊢ a ∈ ℤ ∧ b ∈ ℤ → 2 ⁢ a + b + 1 = 2 ⁢ a + 1 + 2 ⁢ b + 1
36 9 35 breqtrd ⊢ a ∈ ℤ ∧ b ∈ ℤ → 2 ∥ 2 ⁢ a + 1 + 2 ⁢ b + 1
37 oveq12 ⊢ 2 ⁢ a + 1 = A ∧ 2 ⁢ b + 1 = B → 2 ⁢ a + 1 + 2 ⁢ b + 1 = A + B
38 37 breq2d ⊢ 2 ⁢ a + 1 = A ∧ 2 ⁢ b + 1 = B → 2 ∥ 2 ⁢ a + 1 + 2 ⁢ b + 1 ↔ 2 ∥ A + B
39 36 38 syl5ibcom ⊢ a ∈ ℤ ∧ b ∈ ℤ → 2 ⁢ a + 1 = A ∧ 2 ⁢ b + 1 = B → 2 ∥ A + B
40 39 rexlimivv ⊢ ∃ a ∈ ℤ ∃ b ∈ ℤ 2 ⁢ a + 1 = A ∧ 2 ⁢ b + 1 = B → 2 ∥ A + B
41 4 40 sylbir ⊢ ∃ a ∈ ℤ 2 ⁢ a + 1 = A ∧ ∃ b ∈ ℤ 2 ⁢ b + 1 = B → 2 ∥ A + B
42 3 41 biimtrdi ⊢ A ∈ ℤ ∧ B ∈ ℤ → ¬ 2 ∥ A ∧ ¬ 2 ∥ B → 2 ∥ A + B
43 42 imp ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → 2 ∥ A + B
44 43 an4s ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A ∧ B ∈ ℤ ∧ ¬ 2 ∥ B → 2 ∥ A + B