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	|- ( ph -> i e. ZZ )
	evenwodadd.2	|- ( ph -> j e. ZZ )
	evenwodadd.3	|- ( ph -> -. 2 || j )
Assertion	evenwodadd	|- ( ph -> 2 || ( i x. ( i + j ) ) )

Proof

Step	Hyp	Ref	Expression
1		evenwodadd.1	|- ( ph -> i e. ZZ )
2		evenwodadd.2	|- ( ph -> j e. ZZ )
3		evenwodadd.3	|- ( ph -> -. 2 || j )
4		2z	|- 2 e. ZZ
5	4	a1i	|- ( ph -> 2 e. ZZ )
6	1 2	zaddcld	|- ( ph -> ( i + j ) e. ZZ )
7		dvdsmultr1	|- ( ( 2 e. ZZ /\ i e. ZZ /\ ( i + j ) e. ZZ ) -> ( 2 || i -> 2 || ( i x. ( i + j ) ) ) )
8	5 1 6 7	syl3anc	|- ( ph -> ( 2 || i -> 2 || ( i x. ( i + j ) ) ) )
9		4anpull2	|- ( ( ( i e. ZZ /\ -. 2 || i ) /\ ( j e. ZZ /\ -. 2 || j ) ) <-> ( ( i e. ZZ /\ j e. ZZ /\ -. 2 || j ) /\ -. 2 || i ) )
10		opoe	|- ( ( ( i e. ZZ /\ -. 2 || i ) /\ ( j e. ZZ /\ -. 2 || j ) ) -> 2 || ( i + j ) )
11	9 10	sylbir	|- ( ( ( i e. ZZ /\ j e. ZZ /\ -. 2 || j ) /\ -. 2 || i ) -> 2 || ( i + j ) )
12	11	ex	|- ( ( i e. ZZ /\ j e. ZZ /\ -. 2 || j ) -> ( -. 2 || i -> 2 || ( i + j ) ) )
13	1 2 3 12	syl3anc	|- ( ph -> ( -. 2 || i -> 2 || ( i + j ) ) )
14		dvdsmultr2	|- ( ( 2 e. ZZ /\ i e. ZZ /\ ( i + j ) e. ZZ ) -> ( 2 || ( i + j ) -> 2 || ( i x. ( i + j ) ) ) )
15	5 1 6 14	syl3anc	|- ( ph -> ( 2 || ( i + j ) -> 2 || ( i x. ( i + j ) ) ) )
16	13 15	syld	|- ( ph -> ( -. 2 || i -> 2 || ( i x. ( i + j ) ) ) )
17	8 16	pm2.61d	|- ( ph -> 2 || ( i x. ( i + j ) ) )