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	$⊢ ((A \in ℤ \land \neg 2 ∥ A) \land (B \in ℤ \land \neg 2 ∥ B)) \to 2 ∥ (A - B)$

Proof

Step	Hyp	Ref	Expression
1		odd2np1	$⊢ A \in ℤ \to (\neg 2 ∥ A \leftrightarrow \exists a \in ℤ 2 a + 1 = A)$
2		odd2np1	$⊢ B \in ℤ \to (\neg 2 ∥ B \leftrightarrow \exists b \in ℤ 2 b + 1 = B)$
3	1 2	bi2anan9	$⊢ (A \in ℤ \land B \in ℤ) \to ((\neg 2 ∥ A \land \neg 2 ∥ B) \leftrightarrow (\exists a \in ℤ 2 a + 1 = A \land \exists b \in ℤ 2 b + 1 = B))$
4		reeanv	$⊢ \exists a \in ℤ \exists b \in ℤ (2 a + 1 = A \land 2 b + 1 = B) \leftrightarrow (\exists a \in ℤ 2 a + 1 = A \land \exists b \in ℤ 2 b + 1 = B)$
5		2z	$⊢ 2 \in ℤ$
6		zsubcl	$⊢ (a \in ℤ \land b \in ℤ) \to a - b \in ℤ$
7		dvdsmul1	$⊢ (2 \in ℤ \land a - b \in ℤ) \to 2 ∥ 2 (a - b)$
8	5 6 7	sylancr	$⊢ (a \in ℤ \land b \in ℤ) \to 2 ∥ 2 (a - b)$
9		zcn	$⊢ a \in ℤ \to a \in ℂ$
10		zcn	$⊢ b \in ℤ \to b \in ℂ$
11		2cn	$⊢ 2 \in ℂ$
12		mulcl	$⊢ (2 \in ℂ \land a \in ℂ) \to 2 a \in ℂ$
13	11 12	mpan	$⊢ a \in ℂ \to 2 a \in ℂ$
14		mulcl	$⊢ (2 \in ℂ \land b \in ℂ) \to 2 b \in ℂ$
15	11 14	mpan	$⊢ b \in ℂ \to 2 b \in ℂ$
16		ax-1cn	$⊢ 1 \in ℂ$
17		pnpcan2	$⊢ (2 a \in ℂ \land 2 b \in ℂ \land 1 \in ℂ) \to 2 a + 1 - (2 b + 1) = 2 a - 2 b$
18	16 17	mp3an3	$⊢ (2 a \in ℂ \land 2 b \in ℂ) \to 2 a + 1 - (2 b + 1) = 2 a - 2 b$
19	13 15 18	syl2an	$⊢ (a \in ℂ \land b \in ℂ) \to 2 a + 1 - (2 b + 1) = 2 a - 2 b$
20		subdi	$⊢ (2 \in ℂ \land a \in ℂ \land b \in ℂ) \to 2 (a - b) = 2 a - 2 b$
21	11 20	mp3an1	$⊢ (a \in ℂ \land b \in ℂ) \to 2 (a - b) = 2 a - 2 b$
22	19 21	eqtr4d	$⊢ (a \in ℂ \land b \in ℂ) \to 2 a + 1 - (2 b + 1) = 2 (a - b)$
23	9 10 22	syl2an	$⊢ (a \in ℤ \land b \in ℤ) \to 2 a + 1 - (2 b + 1) = 2 (a - b)$
24	8 23	breqtrrd	$⊢ (a \in ℤ \land b \in ℤ) \to 2 ∥ (2 a + 1 - (2 b + 1))$
25		oveq12	$⊢ (2 a + 1 = A \land 2 b + 1 = B) \to 2 a + 1 - (2 b + 1) = A - B$
26	25	breq2d	$⊢ (2 a + 1 = A \land 2 b + 1 = B) \to (2 ∥ (2 a + 1 - (2 b + 1)) \leftrightarrow 2 ∥ (A - B))$
27	24 26	syl5ibcom	$⊢ (a \in ℤ \land b \in ℤ) \to ((2 a + 1 = A \land 2 b + 1 = B) \to 2 ∥ (A - B))$
28	27	rexlimivv	$⊢ \exists a \in ℤ \exists b \in ℤ (2 a + 1 = A \land 2 b + 1 = B) \to 2 ∥ (A - B)$
29	4 28	sylbir	$⊢ (\exists a \in ℤ 2 a + 1 = A \land \exists b \in ℤ 2 b + 1 = B) \to 2 ∥ (A - B)$
30	3 29	biimtrdi	$⊢ (A \in ℤ \land B \in ℤ) \to ((\neg 2 ∥ A \land \neg 2 ∥ B) \to 2 ∥ (A - B))$
31	30	imp	$⊢ ((A \in ℤ \land B \in ℤ) \land (\neg 2 ∥ A \land \neg 2 ∥ B)) \to 2 ∥ (A - B)$
32	31	an4s	$⊢ ((A \in ℤ \land \neg 2 ∥ A) \land (B \in ℤ \land \neg 2 ∥ B)) \to 2 ∥ (A - B)$

Metamath Proof Explorer

Theorem omoe

Proof