This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢ ( 𝐴 ∈ ℤ → ( ¬ 2 ∥ 𝐴 ↔ ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ) )
2 odd2np1 ⊢ ( 𝐵 ∈ ℤ → ( ¬ 2 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) )
3 1 2 bi2anan9 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) ) )
4 reeanv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) )
5 2z ⊢ 2 ∈ ℤ
6 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
7 6 peano2zd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( 𝑎 + 𝑏 ) + 1 ) ∈ ℤ )
8 dvdsmul1 ⊢ ( ( 2 ∈ ℤ ∧ ( ( 𝑎 + 𝑏 ) + 1 ) ∈ ℤ ) → 2 ∥ ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) )
9 5 7 8 sylancr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) )
10 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
11 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
12 addcl ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 + 𝑏 ) ∈ ℂ )
13 2cn ⊢ 2 ∈ ℂ
14 ax-1cn ⊢ 1 ∈ ℂ
15 adddi ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑎 + 𝑏 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
16 13 14 15 mp3an13 ⊢ ( ( 𝑎 + 𝑏 ) ∈ ℂ → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
17 12 16 syl ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) )
18 adddi ⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 + 𝑏 ) ) = ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) )
19 13 18 mp3an1 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 + 𝑏 ) ) = ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) )
20 19 oveq1d ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 2 · ( 𝑎 + 𝑏 ) ) + ( 2 · 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 2 · 1 ) ) )
21 17 20 eqtrd ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 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 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 2 · 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) )
26 21 25 eqtrdi ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) )
27 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 2 · 𝑎 ) ∈ ℂ )
28 13 27 mpan ⊢ ( 𝑎 ∈ ℂ → ( 2 · 𝑎 ) ∈ ℂ )
29 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · 𝑏 ) ∈ ℂ )
30 13 29 mpan ⊢ ( 𝑏 ∈ ℂ → ( 2 · 𝑏 ) ∈ ℂ )
31 add4 ⊢ ( ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) ∧ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
32 14 14 31 mpanr12 ⊢ ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
33 28 30 32 syl2an ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + ( 2 · 𝑏 ) ) + ( 1 + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
34 26 33 eqtrd ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
35 10 11 34 syl2an ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 2 · ( ( 𝑎 + 𝑏 ) + 1 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
36 9 35 breqtrd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) )
37 oveq12 ⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) = ( 𝐴 + 𝐵 ) )
38 37 breq2d ⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) + ( ( 2 · 𝑏 ) + 1 ) ) ↔ 2 ∥ ( 𝐴 + 𝐵 ) ) )
39 36 38 syl5ibcom ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) ) )
40 39 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) )
41 4 40 sylbir ⊢ ( ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) )
42 3 41 biimtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 + 𝐵 ) ) )
43 42 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )
44 43 an4s ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 + 𝐵 ) )