opoeALTV

Description: The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by AV, 20-Jun-2020)

		Ref	Expression
	Assertion	opoeALTV	$⊢ (A \in Odd \land B \in Odd) \to A + B \in Even$

Proof

Step	Hyp	Ref	Expression
1		oddz	$⊢ A \in Odd \to A \in ℤ$
2		oddz	$⊢ B \in Odd \to B \in ℤ$
3		zaddcl	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
4	1 2 3	syl2an	$⊢ (A \in Odd \land B \in Odd) \to A + B \in ℤ$
5		eqeq1	$⊢ a = A \to (a = 2 i + 1 \leftrightarrow A = 2 i + 1)$
6	5	rexbidv	$⊢ a = A \to (\exists i \in ℤ a = 2 i + 1 \leftrightarrow \exists i \in ℤ A = 2 i + 1)$
7		dfodd6	$⊢ Odd = \{a \in ℤ \| \exists i \in ℤ a = 2 i + 1\}$
8	6 7	elrab2	$⊢ A \in Odd \leftrightarrow (A \in ℤ \land \exists i \in ℤ A = 2 i + 1)$
9		eqeq1	$⊢ b = B \to (b = 2 j + 1 \leftrightarrow B = 2 j + 1)$
10	9	rexbidv	$⊢ b = B \to (\exists j \in ℤ b = 2 j + 1 \leftrightarrow \exists j \in ℤ B = 2 j + 1)$
11		dfodd6	$⊢ Odd = \{b \in ℤ \| \exists j \in ℤ b = 2 j + 1\}$
12	10 11	elrab2	$⊢ B \in Odd \leftrightarrow (B \in ℤ \land \exists j \in ℤ B = 2 j + 1)$
13		zaddcl	$⊢ (i \in ℤ \land j \in ℤ) \to i + j \in ℤ$
14	13	ex	$⊢ i \in ℤ \to (j \in ℤ \to i + j \in ℤ)$
15	14	ad3antlr	$⊢ (((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \to (j \in ℤ \to i + j \in ℤ)$
16	15	imp	$⊢ ((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \to i + j \in ℤ$
17	16	adantr	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to i + j \in ℤ$
18	17	peano2zd	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to i + j + 1 \in ℤ$
19		oveq2	$⊢ n = i + j + 1 \to 2 n = 2 (i + j + 1)$
20	19	eqeq2d	$⊢ n = i + j + 1 \to (A + B = 2 n \leftrightarrow A + B = 2 (i + j + 1))$
21	20	adantl	$⊢ ((((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \land n = i + j + 1) \to (A + B = 2 n \leftrightarrow A + B = 2 (i + j + 1))$
22		oveq12	$⊢ (A = 2 i + 1 \land B = 2 j + 1) \to A + B = 2 i + 1 + 2 j + 1$
23	22	ex	$⊢ A = 2 i + 1 \to (B = 2 j + 1 \to A + B = 2 i + 1 + 2 j + 1)$
24	23	ad3antlr	$⊢ ((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \to (B = 2 j + 1 \to A + B = 2 i + 1 + 2 j + 1)$
25	24	imp	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to A + B = 2 i + 1 + 2 j + 1$
26		zcn	$⊢ i \in ℤ \to i \in ℂ$
27		zcn	$⊢ j \in ℤ \to j \in ℂ$
28		2cnd	$⊢ j \in ℂ \to 2 \in ℂ$
29	28	anim1i	$⊢ (j \in ℂ \land i \in ℂ) \to (2 \in ℂ \land i \in ℂ)$
30	29	ancoms	$⊢ (i \in ℂ \land j \in ℂ) \to (2 \in ℂ \land i \in ℂ)$
31		mulcl	$⊢ (2 \in ℂ \land i \in ℂ) \to 2 i \in ℂ$
32	30 31	syl	$⊢ (i \in ℂ \land j \in ℂ) \to 2 i \in ℂ$
33		1cnd	$⊢ (i \in ℂ \land j \in ℂ) \to 1 \in ℂ$
34		2cnd	$⊢ i \in ℂ \to 2 \in ℂ$
35		mulcl	$⊢ (2 \in ℂ \land j \in ℂ) \to 2 j \in ℂ$
36	34 35	sylan	$⊢ (i \in ℂ \land j \in ℂ) \to 2 j \in ℂ$
37	32 33 36 33	add4d	$⊢ (i \in ℂ \land j \in ℂ) \to 2 i + 1 + 2 j + 1 = 2 i + 2 j + 1 + 1$
38		2cnd	$⊢ (i \in ℂ \land j \in ℂ) \to 2 \in ℂ$
39		simpl	$⊢ (i \in ℂ \land j \in ℂ) \to i \in ℂ$
40		simpr	$⊢ (i \in ℂ \land j \in ℂ) \to j \in ℂ$
41	38 39 40	adddid	$⊢ (i \in ℂ \land j \in ℂ) \to 2 (i + j) = 2 i + 2 j$
42	41	oveq1d	$⊢ (i \in ℂ \land j \in ℂ) \to 2 (i + j) + 2 \cdot 1 = 2 i + 2 j + 2 \cdot 1$
43		addcl	$⊢ (i \in ℂ \land j \in ℂ) \to i + j \in ℂ$
44	38 43 33	adddid	$⊢ (i \in ℂ \land j \in ℂ) \to 2 (i + j + 1) = 2 (i + j) + 2 \cdot 1$
45		1p1e2	$⊢ 1 + 1 = 2$
46		2t1e2	$⊢ 2 \cdot 1 = 2$
47	45 46	eqtr4i	$⊢ 1 + 1 = 2 \cdot 1$
48	47	a1i	$⊢ (i \in ℂ \land j \in ℂ) \to 1 + 1 = 2 \cdot 1$
49	48	oveq2d	$⊢ (i \in ℂ \land j \in ℂ) \to 2 i + 2 j + 1 + 1 = 2 i + 2 j + 2 \cdot 1$
50	42 44 49	3eqtr4rd	$⊢ (i \in ℂ \land j \in ℂ) \to 2 i + 2 j + 1 + 1 = 2 (i + j + 1)$
51	37 50	eqtrd	$⊢ (i \in ℂ \land j \in ℂ) \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1)$
52	26 27 51	syl2an	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1)$
53	52	ex	$⊢ i \in ℤ \to (j \in ℤ \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1))$
54	53	ad3antlr	$⊢ (((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \to (j \in ℤ \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1))$
55	54	imp	$⊢ ((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1)$
56	55	adantr	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to 2 i + 1 + 2 j + 1 = 2 (i + j + 1)$
57	25 56	eqtrd	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to A + B = 2 (i + j + 1)$
58	18 21 57	rspcedvd	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j + 1) \to \exists n \in ℤ A + B = 2 n$
59	58	rexlimdva2	$⊢ (((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \to (\exists j \in ℤ B = 2 j + 1 \to \exists n \in ℤ A + B = 2 n)$
60	59	expimpd	$⊢ ((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \to ((B \in ℤ \land \exists j \in ℤ B = 2 j + 1) \to \exists n \in ℤ A + B = 2 n)$
61	60	rexlimdva2	$⊢ A \in ℤ \to (\exists i \in ℤ A = 2 i + 1 \to ((B \in ℤ \land \exists j \in ℤ B = 2 j + 1) \to \exists n \in ℤ A + B = 2 n))$
62	61	imp	$⊢ (A \in ℤ \land \exists i \in ℤ A = 2 i + 1) \to ((B \in ℤ \land \exists j \in ℤ B = 2 j + 1) \to \exists n \in ℤ A + B = 2 n)$
63	12 62	syl5bi	$⊢ (A \in ℤ \land \exists i \in ℤ A = 2 i + 1) \to (B \in Odd \to \exists n \in ℤ A + B = 2 n)$
64	8 63	sylbi	$⊢ A \in Odd \to (B \in Odd \to \exists n \in ℤ A + B = 2 n)$
65	64	imp	$⊢ (A \in Odd \land B \in Odd) \to \exists n \in ℤ A + B = 2 n$
66		eqeq1	$⊢ z = A + B \to (z = 2 n \leftrightarrow A + B = 2 n)$
67	66	rexbidv	$⊢ z = A + B \to (\exists n \in ℤ z = 2 n \leftrightarrow \exists n \in ℤ A + B = 2 n)$
68		dfeven4	$⊢ Even = \{z \in ℤ \| \exists n \in ℤ z = 2 n\}$
69	67 68	elrab2	$⊢ A + B \in Even \leftrightarrow (A + B \in ℤ \land \exists n \in ℤ A + B = 2 n)$
70	4 65 69	sylanbrc	$⊢ (A \in Odd \land B \in Odd) \to A + B \in Even$

Metamath Proof Explorer

Theorem opoeALTV

Proof