Metamath Proof Explorer

Theorem evenwodadd

Description: If an integer is multiplied by its sum with an odd number (thus changing its parity), the result is even. (Contributed by Ender Ting, 30-Apr-2025)

		Ref	Expression
	Hypotheses	evenwodadd.1	$⊢ φ \to i \in ℤ$
		evenwodadd.2	$⊢ φ \to j \in ℤ$
		evenwodadd.3	$⊢ φ \to \neg 2 ∥ j$
	Assertion	evenwodadd	$⊢ φ \to 2 ∥ i (i + j)$

Proof

Step	Hyp	Ref	Expression
1		evenwodadd.1	$⊢ φ \to i \in ℤ$
2		evenwodadd.2	$⊢ φ \to j \in ℤ$
3		evenwodadd.3	$⊢ φ \to \neg 2 ∥ j$
4		2z	$⊢ 2 \in ℤ$
5	4	a1i	$⊢ φ \to 2 \in ℤ$
6	1 2	zaddcld	$⊢ φ \to i + j \in ℤ$
7		dvdsmultr1	$⊢ (2 \in ℤ \land i \in ℤ \land i + j \in ℤ) \to (2 ∥ i \to 2 ∥ i (i + j))$
8	5 1 6 7	syl3anc	$⊢ φ \to (2 ∥ i \to 2 ∥ i (i + j))$
9		4anpull2	$⊢ ((i \in ℤ \land \neg 2 ∥ i) \land (j \in ℤ \land \neg 2 ∥ j)) \leftrightarrow ((i \in ℤ \land j \in ℤ \land \neg 2 ∥ j) \land \neg 2 ∥ i)$
10		opoe	$⊢ ((i \in ℤ \land \neg 2 ∥ i) \land (j \in ℤ \land \neg 2 ∥ j)) \to 2 ∥ (i + j)$
11	9 10	sylbir	$⊢ ((i \in ℤ \land j \in ℤ \land \neg 2 ∥ j) \land \neg 2 ∥ i) \to 2 ∥ (i + j)$
12	11	ex	$⊢ (i \in ℤ \land j \in ℤ \land \neg 2 ∥ j) \to (\neg 2 ∥ i \to 2 ∥ (i + j))$
13	1 2 3 12	syl3anc	$⊢ φ \to (\neg 2 ∥ i \to 2 ∥ (i + j))$
14		dvdsmultr2	$⊢ (2 \in ℤ \land i \in ℤ \land i + j \in ℤ) \to (2 ∥ (i + j) \to 2 ∥ i (i + j))$
15	5 1 6 14	syl3anc	$⊢ φ \to (2 ∥ (i + j) \to 2 ∥ i (i + j))$
16	13 15	syld	$⊢ φ \to (\neg 2 ∥ i \to 2 ∥ i (i + j))$
17	8 16	pm2.61d	$⊢ φ \to 2 ∥ i (i + j)$