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

Proof

Step Hyp Ref Expression
1 odd2np1 ( 𝐴 ∈ ℤ → ( ¬ 2 ∥ 𝐴 ↔ ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ) )
2 2z 2 ∈ ℤ
3 divides ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 2 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℤ ( 𝑏 · 2 ) = 𝐵 ) )
4 2 3 mpan ( 𝐵 ∈ ℤ → ( 2 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℤ ( 𝑏 · 2 ) = 𝐵 ) )
5 1 4 bi2anan9 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( 𝑏 · 2 ) = 𝐵 ) ) )
6 reeanv ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( 𝑏 · 2 ) = 𝐵 ) )
7 zsubcl ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎𝑏 ) ∈ ℤ )
8 zcn ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
9 zcn ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
10 2cn 2 ∈ ℂ
11 subdi ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎𝑏 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
12 10 11 mp3an1 ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · ( 𝑎𝑏 ) ) = ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) )
13 12 oveq1d ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) = ( ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) + 1 ) )
14 mulcl ( ( 2 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 2 · 𝑎 ) ∈ ℂ )
15 10 14 mpan ( 𝑎 ∈ ℂ → ( 2 · 𝑎 ) ∈ ℂ )
16 mulcl ( ( 2 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · 𝑏 ) ∈ ℂ )
17 10 16 mpan ( 𝑏 ∈ ℂ → ( 2 · 𝑏 ) ∈ ℂ )
18 ax-1cn 1 ∈ ℂ
19 addsub ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( 2 · 𝑏 ) ) = ( ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) + 1 ) )
20 18 19 mp3an2 ( ( ( 2 · 𝑎 ) ∈ ℂ ∧ ( 2 · 𝑏 ) ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( 2 · 𝑏 ) ) = ( ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) + 1 ) )
21 15 17 20 syl2an ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( 2 · 𝑏 ) ) = ( ( ( 2 · 𝑎 ) − ( 2 · 𝑏 ) ) + 1 ) )
22 mulcom ( ( 2 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 2 · 𝑏 ) = ( 𝑏 · 2 ) )
23 10 22 mpan ( 𝑏 ∈ ℂ → ( 2 · 𝑏 ) = ( 𝑏 · 2 ) )
24 23 oveq2d ( 𝑏 ∈ ℂ → ( ( ( 2 · 𝑎 ) + 1 ) − ( 2 · 𝑏 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
25 24 adantl ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( 2 · 𝑏 ) ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
26 13 21 25 3eqtr2d ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
27 8 9 26 syl2an ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
28 oveq2 ( 𝑐 = ( 𝑎𝑏 ) → ( 2 · 𝑐 ) = ( 2 · ( 𝑎𝑏 ) ) )
29 28 oveq1d ( 𝑐 = ( 𝑎𝑏 ) → ( ( 2 · 𝑐 ) + 1 ) = ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) )
30 29 eqeq1d ( 𝑐 = ( 𝑎𝑏 ) → ( ( ( 2 · 𝑐 ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) ↔ ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) ) )
31 30 rspcev ( ( ( 𝑎𝑏 ) ∈ ℤ ∧ ( ( 2 · ( 𝑎𝑏 ) ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
32 7 27 31 syl2anc ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) )
33 oveq12 ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) → ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) = ( 𝐴𝐵 ) )
34 33 eqeq2d ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) → ( ( ( 2 · 𝑐 ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) ↔ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
35 34 rexbidv ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) → ( ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( ( ( 2 · 𝑎 ) + 1 ) − ( 𝑏 · 2 ) ) ↔ ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
36 32 35 syl5ibcom ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
37 36 rexlimivv ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ( 𝑏 · 2 ) = 𝐵 ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) )
38 6 37 sylbir ( ( ∃ 𝑎 ∈ ℤ ( ( 2 · 𝑎 ) + 1 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( 𝑏 · 2 ) = 𝐵 ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) )
39 5 38 syl6bi ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
40 39 imp ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ¬ 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) )
41 40 an4s ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ 2 ∥ 𝐵 ) ) → ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) )
42 zsubcl ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴𝐵 ) ∈ ℤ )
43 42 ad2ant2r ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ 2 ∥ 𝐵 ) ) → ( 𝐴𝐵 ) ∈ ℤ )
44 odd2np1 ( ( 𝐴𝐵 ) ∈ ℤ → ( ¬ 2 ∥ ( 𝐴𝐵 ) ↔ ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
45 43 44 syl ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ 2 ∥ 𝐵 ) ) → ( ¬ 2 ∥ ( 𝐴𝐵 ) ↔ ∃ 𝑐 ∈ ℤ ( ( 2 · 𝑐 ) + 1 ) = ( 𝐴𝐵 ) ) )
46 41 45 mpbird ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ 2 ∥ 𝐵 ) ) → ¬ 2 ∥ ( 𝐴𝐵 ) )