This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ Fin
evensumodd.b ⊢ φ ∧ k ∈ A → B ∈ ℤ
evensumodd.o ⊢ φ ∧ k ∈ A → ¬ 2 ∥ B
oddsumodd.a ⊢ φ → ¬ 2 ∥ A
Assertion oddsumodd ⊢ φ → ¬ 2 ∥ ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 evensumodd.a ⊢ φ → A ∈ Fin
2 evensumodd.b ⊢ φ ∧ k ∈ A → B ∈ ℤ
3 evensumodd.o ⊢ φ ∧ k ∈ A → ¬ 2 ∥ B
4 oddsumodd.a ⊢ φ → ¬ 2 ∥ A
5 1 2 3 sumodd ⊢ φ → 2 ∥ A ↔ 2 ∥ ∑ k ∈ A B
6 4 5 mtbid ⊢ φ → ¬ 2 ∥ ∑ k ∈ A B