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	$$⊢\phi \to A\in \mathrm{Fin}$$
	evensumodd.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \mathbb{Z}$$
	evensumodd.o	$$⊢\left(\phi \wedge k\in A\right)\to \neg 2\parallel B$$
	evensumodd.e	$$⊢\phi \to 2\parallel \left|A\right|$$
Assertion	evensumodd	$$⊢\phi \to 2\parallel \sum _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		evensumodd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
2		evensumodd.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \mathbb{Z}$$
3		evensumodd.o	$$⊢\left(\phi \wedge k\in A\right)\to \neg 2\parallel B$$
4		evensumodd.e	$$⊢\phi \to 2\parallel \left|A\right|$$
5	1 2 3	sumodd	$$⊢\phi \to \left(2\parallel \left|A\right|\leftrightarrow 2\parallel \sum _{k\in A}B\right)$$
6	4 5	mpbid	$$⊢\phi \to 2\parallel \sum _{k\in A}B$$