Metamath Proof Explorer


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 ( 𝜑𝐴 ∈ Fin )
evensumodd.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℤ )
evensumodd.o ( ( 𝜑𝑘𝐴 ) → ¬ 2 ∥ 𝐵 )
evensumodd.e ( 𝜑 → 2 ∥ ( ♯ ‘ 𝐴 ) )
Assertion evensumodd ( 𝜑 → 2 ∥ Σ 𝑘𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 evensumodd.a ( 𝜑𝐴 ∈ Fin )
2 evensumodd.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℤ )
3 evensumodd.o ( ( 𝜑𝑘𝐴 ) → ¬ 2 ∥ 𝐵 )
4 evensumodd.e ( 𝜑 → 2 ∥ ( ♯ ‘ 𝐴 ) )
5 1 2 3 sumodd ( 𝜑 → ( 2 ∥ ( ♯ ‘ 𝐴 ) ↔ 2 ∥ Σ 𝑘𝐴 𝐵 ) )
6 4 5 mpbid ( 𝜑 → 2 ∥ Σ 𝑘𝐴 𝐵 )