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

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