Theorem evensumodd

Description: If every term in a sum with an even number of terms is odd, then the sum is even. (Contributed by AV, 14-Aug-2021)

	Ref	Expression
Hypotheses	evensumodd.a	|- ( ph -> A e. Fin )
	evensumodd.b	|- ( ( ph /\ k e. A ) -> B e. ZZ )
	evensumodd.o	|- ( ( ph /\ k e. A ) -> -. 2 || B )
	evensumodd.e	|- ( ph -> 2 || ( # ` A ) )
Assertion	evensumodd	|- ( ph -> 2 || sum_ k e. A B )

Proof

Step	Hyp	Ref	Expression
1		evensumodd.a	|- ( ph -> A e. Fin )
2		evensumodd.b	|- ( ( ph /\ k e. A ) -> B e. ZZ )
3		evensumodd.o	|- ( ( ph /\ k e. A ) -> -. 2 || B )
4		evensumodd.e	|- ( ph -> 2 || ( # ` A ) )
5	1 2 3	sumodd	|- ( ph -> ( 2 || ( # ` A ) <-> 2 || sum_ k e. A B ) )
6	4 5	mpbid	|- ( ph -> 2 || sum_ k e. A B )