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	1 2	zaddcld	|- ( ph -> ( I + J ) e. ZZ )
6		dvdsmultr1	|- ( ( 2 e. ZZ /\ I e. ZZ /\ ( I + J ) e. ZZ ) -> ( 2 || I -> 2 || ( I x. ( I + J ) ) ) )
7	4 1 5 6	mp3an2i	|- ( ph -> ( 2 || I -> 2 || ( I x. ( I + J ) ) ) )
8		4anpull2	|- ( ( ( I e. ZZ /\ -. 2 || I ) /\ ( J e. ZZ /\ -. 2 || J ) ) <-> ( ( I e. ZZ /\ J e. ZZ /\ -. 2 || J ) /\ -. 2 || I ) )
9		opoe	|- ( ( ( I e. ZZ /\ -. 2 || I ) /\ ( J e. ZZ /\ -. 2 || J ) ) -> 2 || ( I + J ) )
10	8 9	sylbir	|- ( ( ( I e. ZZ /\ J e. ZZ /\ -. 2 || J ) /\ -. 2 || I ) -> 2 || ( I + J ) )
11	10	ex	|- ( ( I e. ZZ /\ J e. ZZ /\ -. 2 || J ) -> ( -. 2 || I -> 2 || ( I + J ) ) )
12	1 2 3 11	syl3anc	|- ( ph -> ( -. 2 || I -> 2 || ( I + J ) ) )
13		dvdsmultr2	|- ( ( 2 e. ZZ /\ I e. ZZ /\ ( I + J ) e. ZZ ) -> ( 2 || ( I + J ) -> 2 || ( I x. ( I + J ) ) ) )
14	4 1 5 13	mp3an2i	|- ( ph -> ( 2 || ( I + J ) -> 2 || ( I x. ( I + J ) ) ) )
15	12 14	syld	|- ( ph -> ( -. 2 || I -> 2 || ( I x. ( I + J ) ) ) )
16	7 15	pm2.61d	|- ( ph -> 2 || ( I x. ( I + J ) ) )