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	1 2	zaddcld	$⊢ φ \to I + J \in ℤ$
6		dvdsmultr1	$⊢ (2 \in ℤ \land I \in ℤ \land I + J \in ℤ) \to (2 ∥ I \to 2 ∥ I (I + J))$
7	4 1 5 6	mp3an2i	$⊢ φ \to (2 ∥ I \to 2 ∥ I (I + J))$
8		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)$
9		opoe	$⊢ ((I \in ℤ \land \neg 2 ∥ I) \land (J \in ℤ \land \neg 2 ∥ J)) \to 2 ∥ (I + J)$
10	8 9	sylbir	$⊢ ((I \in ℤ \land J \in ℤ \land \neg 2 ∥ J) \land \neg 2 ∥ I) \to 2 ∥ (I + J)$
11	10	ex	$⊢ (I \in ℤ \land J \in ℤ \land \neg 2 ∥ J) \to (\neg 2 ∥ I \to 2 ∥ (I + J))$
12	1 2 3 11	syl3anc	$⊢ φ \to (\neg 2 ∥ I \to 2 ∥ (I + J))$
13		dvdsmultr2	$⊢ (2 \in ℤ \land I \in ℤ \land I + J \in ℤ) \to (2 ∥ (I + J) \to 2 ∥ I (I + J))$
14	4 1 5 13	mp3an2i	$⊢ φ \to (2 ∥ (I + J) \to 2 ∥ I (I + J))$
15	12 14	syld	$⊢ φ \to (\neg 2 ∥ I \to 2 ∥ I (I + J))$
16	7 15	pm2.61d	$⊢ φ \to 2 ∥ I (I + J)$