Theorem oddsumodd

Description: If every term in a sum with an odd number of terms is odd, then the sum is odd. (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 )
	oddsumodd.a	|- ( ph -> -. 2 || ( # ` A ) )
Assertion	oddsumodd	|- ( 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		oddsumodd.a	|- ( ph -> -. 2 || ( # ` A ) )
5	1 2 3	sumodd	|- ( ph -> ( 2 || ( # ` A ) <-> 2 || sum_ k e. A B ) )
6	4 5	mtbid	|- ( ph -> -. 2 || sum_ k e. A B )