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	4	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
6	1 2	zaddcld	⊢ ( 𝜑 → ( 𝑖 + 𝑗 ) ∈ ℤ )
7		dvdsmultr1	⊢ ( ( 2 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ ( 𝑖 + 𝑗 ) ∈ ℤ ) → ( 2 ∥ 𝑖 → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) ) )
8	5 1 6 7	syl3anc	⊢ ( 𝜑 → ( 2 ∥ 𝑖 → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) ) )
9		4anpull2	⊢ ( ( ( 𝑖 ∈ ℤ ∧ ¬ 2 ∥ 𝑖 ) ∧ ( 𝑗 ∈ ℤ ∧ ¬ 2 ∥ 𝑗 ) ) ↔ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ¬ 2 ∥ 𝑗 ) ∧ ¬ 2 ∥ 𝑖 ) )
10		opoe	⊢ ( ( ( 𝑖 ∈ ℤ ∧ ¬ 2 ∥ 𝑖 ) ∧ ( 𝑗 ∈ ℤ ∧ ¬ 2 ∥ 𝑗 ) ) → 2 ∥ ( 𝑖 + 𝑗 ) )
11	9 10	sylbir	⊢ ( ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ¬ 2 ∥ 𝑗 ) ∧ ¬ 2 ∥ 𝑖 ) → 2 ∥ ( 𝑖 + 𝑗 ) )
12	11	ex	⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ¬ 2 ∥ 𝑗 ) → ( ¬ 2 ∥ 𝑖 → 2 ∥ ( 𝑖 + 𝑗 ) ) )
13	1 2 3 12	syl3anc	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑖 → 2 ∥ ( 𝑖 + 𝑗 ) ) )
14		dvdsmultr2	⊢ ( ( 2 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ ( 𝑖 + 𝑗 ) ∈ ℤ ) → ( 2 ∥ ( 𝑖 + 𝑗 ) → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) ) )
15	5 1 6 14	syl3anc	⊢ ( 𝜑 → ( 2 ∥ ( 𝑖 + 𝑗 ) → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) ) )
16	13 15	syld	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑖 → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) ) )
17	8 16	pm2.61d	⊢ ( 𝜑 → 2 ∥ ( 𝑖 · ( 𝑖 + 𝑗 ) ) )