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	syl6bi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 − 𝐵 ) ) )
31	30	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 − 𝐵 ) )
32	31	an4s	⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ) → 2 ∥ ( 𝐴 − 𝐵 ) )