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	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
	evenwodadd.2	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	evenwodadd.3	⊢ ( 𝜑 → ¬ 2 ∥ 𝐽 )
Assertion	evenwodadd	⊢ ( 𝜑 → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evenwodadd.1	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
2		evenwodadd.2	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
3		evenwodadd.3	⊢ ( 𝜑 → ¬ 2 ∥ 𝐽 )
4		2z	⊢ 2 ∈ ℤ
5	1 2	zaddcld	⊢ ( 𝜑 → ( 𝐼 + 𝐽 ) ∈ ℤ )
6		dvdsmultr1	⊢ ( ( 2 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ( 𝐼 + 𝐽 ) ∈ ℤ ) → ( 2 ∥ 𝐼 → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) ) )
7	4 1 5 6	mp3an2i	⊢ ( 𝜑 → ( 2 ∥ 𝐼 → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) ) )
8		4anpull2	⊢ ( ( ( 𝐼 ∈ ℤ ∧ ¬ 2 ∥ 𝐼 ) ∧ ( 𝐽 ∈ ℤ ∧ ¬ 2 ∥ 𝐽 ) ) ↔ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ¬ 2 ∥ 𝐽 ) ∧ ¬ 2 ∥ 𝐼 ) )
9		opoe	⊢ ( ( ( 𝐼 ∈ ℤ ∧ ¬ 2 ∥ 𝐼 ) ∧ ( 𝐽 ∈ ℤ ∧ ¬ 2 ∥ 𝐽 ) ) → 2 ∥ ( 𝐼 + 𝐽 ) )
10	8 9	sylbir	⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ¬ 2 ∥ 𝐽 ) ∧ ¬ 2 ∥ 𝐼 ) → 2 ∥ ( 𝐼 + 𝐽 ) )
11	10	ex	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ¬ 2 ∥ 𝐽 ) → ( ¬ 2 ∥ 𝐼 → 2 ∥ ( 𝐼 + 𝐽 ) ) )
12	1 2 3 11	syl3anc	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝐼 → 2 ∥ ( 𝐼 + 𝐽 ) ) )
13		dvdsmultr2	⊢ ( ( 2 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ( 𝐼 + 𝐽 ) ∈ ℤ ) → ( 2 ∥ ( 𝐼 + 𝐽 ) → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) ) )
14	4 1 5 13	mp3an2i	⊢ ( 𝜑 → ( 2 ∥ ( 𝐼 + 𝐽 ) → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) ) )
15	12 14	syld	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝐼 → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) ) )
16	7 15	pm2.61d	⊢ ( 𝜑 → 2 ∥ ( 𝐼 · ( 𝐼 + 𝐽 ) ) )