opeoALTV

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

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

Proof

Step	Hyp	Ref	Expression
1		oddz	$⊢ A \in Odd \to A \in ℤ$
2		evenz	$⊢ B \in Even \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 Even) \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 \leftrightarrow B = 2 j)$
10	9	rexbidv	$⊢ b = B \to (\exists j \in ℤ b = 2 j \leftrightarrow \exists j \in ℤ B = 2 j)$
11		dfeven4	$⊢ Even = \{b \in ℤ \| \exists j \in ℤ b = 2 j\}$
12	10 11	elrab2	$⊢ B \in Even \leftrightarrow (B \in ℤ \land \exists j \in ℤ B = 2 j)$
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) \to i + j \in ℤ$
18		oveq2	$⊢ n = i + j \to 2 n = 2 (i + j)$
19	18	oveq1d	$⊢ n = i + j \to 2 n + 1 = 2 (i + j) + 1$
20	19	eqeq2d	$⊢ n = i + j \to (A + B = 2 n + 1 \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) \land n = i + j) \to (A + B = 2 n + 1 \leftrightarrow A + B = 2 (i + j) + 1)$
22		oveq12	$⊢ (A = 2 i + 1 \land B = 2 j) \to A + B = 2 i + 1 + 2 j$
23	22	ex	$⊢ A = 2 i + 1 \to (B = 2 j \to A + B = 2 i + 1 + 2 j)$
24	23	ad3antlr	$⊢ ((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \to (B = 2 j \to A + B = 2 i + 1 + 2 j)$
25	24	imp	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j) \to A + B = 2 i + 1 + 2 j$
26		2cnd	$⊢ (j \in ℤ \land i \in ℤ) \to 2 \in ℂ$
27		zcn	$⊢ i \in ℤ \to i \in ℂ$
28	27	adantl	$⊢ (j \in ℤ \land i \in ℤ) \to i \in ℂ$
29	26 28	mulcld	$⊢ (j \in ℤ \land i \in ℤ) \to 2 i \in ℂ$
30	29	ancoms	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i \in ℂ$
31		1cnd	$⊢ (i \in ℤ \land j \in ℤ) \to 1 \in ℂ$
32		2cnd	$⊢ i \in ℤ \to 2 \in ℂ$
33		zcn	$⊢ j \in ℤ \to j \in ℂ$
34		mulcl	$⊢ (2 \in ℂ \land j \in ℂ) \to 2 j \in ℂ$
35	32 33 34	syl2an	$⊢ (i \in ℤ \land j \in ℤ) \to 2 j \in ℂ$
36	30 31 35	add32d	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i + 1 + 2 j = 2 i + 2 j + 1$
37		2cnd	$⊢ (i \in ℤ \land j \in ℤ) \to 2 \in ℂ$
38	27	adantr	$⊢ (i \in ℤ \land j \in ℤ) \to i \in ℂ$
39	33	adantl	$⊢ (i \in ℤ \land j \in ℤ) \to j \in ℂ$
40	37 38 39	adddid	$⊢ (i \in ℤ \land j \in ℤ) \to 2 (i + j) = 2 i + 2 j$
41	40	eqcomd	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i + 2 j = 2 (i + j)$
42	41	oveq1d	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i + 2 j + 1 = 2 (i + j) + 1$
43	36 42	eqtrd	$⊢ (i \in ℤ \land j \in ℤ) \to 2 i + 1 + 2 j = 2 (i + j) + 1$
44	43	ex	$⊢ i \in ℤ \to (j \in ℤ \to 2 i + 1 + 2 j = 2 (i + j) + 1)$
45	44	ad3antlr	$⊢ (((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \to (j \in ℤ \to 2 i + 1 + 2 j = 2 (i + j) + 1)$
46	45	imp	$⊢ ((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \to 2 i + 1 + 2 j = 2 (i + j) + 1$
47	46	adantr	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j) \to 2 i + 1 + 2 j = 2 (i + j) + 1$
48	25 47	eqtrd	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j) \to A + B = 2 (i + j) + 1$
49	17 21 48	rspcedvd	$⊢ (((((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \land j \in ℤ) \land B = 2 j) \to \exists n \in ℤ A + B = 2 n + 1$
50	49	rexlimdva2	$⊢ (((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \land B \in ℤ) \to (\exists j \in ℤ B = 2 j \to \exists n \in ℤ A + B = 2 n + 1)$
51	50	expimpd	$⊢ ((A \in ℤ \land i \in ℤ) \land A = 2 i + 1) \to ((B \in ℤ \land \exists j \in ℤ B = 2 j) \to \exists n \in ℤ A + B = 2 n + 1)$
52	51	r19.29an	$⊢ (A \in ℤ \land \exists i \in ℤ A = 2 i + 1) \to ((B \in ℤ \land \exists j \in ℤ B = 2 j) \to \exists n \in ℤ A + B = 2 n + 1)$
53	12 52	biimtrid	$⊢ (A \in ℤ \land \exists i \in ℤ A = 2 i + 1) \to (B \in Even \to \exists n \in ℤ A + B = 2 n + 1)$
54	8 53	sylbi	$⊢ A \in Odd \to (B \in Even \to \exists n \in ℤ A + B = 2 n + 1)$
55	54	imp	$⊢ (A \in Odd \land B \in Even) \to \exists n \in ℤ A + B = 2 n + 1$
56		eqeq1	$⊢ z = A + B \to (z = 2 n + 1 \leftrightarrow A + B = 2 n + 1)$
57	56	rexbidv	$⊢ z = A + B \to (\exists n \in ℤ z = 2 n + 1 \leftrightarrow \exists n \in ℤ A + B = 2 n + 1)$
58		dfodd6	$⊢ Odd = \{z \in ℤ \| \exists n \in ℤ z = 2 n + 1\}$
59	57 58	elrab2	$⊢ A + B \in Odd \leftrightarrow (A + B \in ℤ \land \exists n \in ℤ A + B = 2 n + 1)$
60	4 55 59	sylanbrc	$⊢ (A \in Odd \land B \in Even) \to A + B \in Odd$

Metamath Proof Explorer

Theorem opeoALTV

Proof