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

Metamath Proof Explorer

Theorem omoe

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

Ref Expression
Assertion omoe ( ( ( 𝐴 ∈ ℤ ∧ ¬ 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 zsubcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 − 𝑏 ) ∈ ℤ )
7 dvdsmul1 ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑎 − 𝑏 ) ∈ ℤ ) → 2 ∥ ( 2 · ( 𝑎 − 𝑏 ) ) )
8 5 6 7 sylancr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( 2 · ( 𝑎 − 𝑏 ) ) )
9 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
10 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
11 2cn ⊢ 2 ∈ ℂ
12 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 2 · 𝑎 ) ∈ ℂ )
13 11 12 mpan ⊢ ( 𝑎 ∈ ℂ → ( 2 · 𝑎 ) ∈ ℂ )
14 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · 𝑏 ) ∈ ℂ )
15 11 14 mpan ⊢ ( 𝑏 ∈ ℂ → ( 2 · 𝑏 ) ∈ ℂ )
16 ax-1cn ⊢ 1 ∈ ℂ
17 pnpcan2 ⊢ ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
18 16 17 mp3an3 ⊢ ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
19 13 15 18 syl2an ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
20 subdi ⊢ ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 − 𝑏 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
21 11 20 mp3an1 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎 − 𝑏 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
22 19 21 eqtr4d ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( 2 · ( 𝑎 − 𝑏 ) ) )
23 9 10 22 syl2an ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( 2 · ( 𝑎 − 𝑏 ) ) )
24 8 23 breqtrrd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) )
25 oveq12 ⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) = ( 𝐴 − 𝐵 ) )
26 25 breq2d ⊢ ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → ( 2 ∥ ( ( ( 2 · 𝑎 ) + 1 ) − ( ( 2 · 𝑏 ) + 1 ) ) ↔ 2 ∥ ( 𝐴 − 𝐵 ) ) )
27 24 26 syl5ibcom ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 − 𝐵 ) ) )
28 27 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 − 𝐵 ) )
29 4 28 sylbir ⊢ ( ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( ( 2 · 𝑏 ) + 1 ) = 𝐵 ) → 2 ∥ ( 𝐴 − 𝐵 ) )
30 3 29 biimtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 − 𝐵 ) ) )
31 30 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 − 𝐵 ) )
32 31 an4s ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 − 𝐵 ) )