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 ∥ ( 𝐴 − 𝐵 ) )