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

Metamath Proof Explorer

Theorem fsumzcl2

Description: A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsumzcl2 ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )

Proof

Step Hyp Ref Expression
1 csbeq1a ⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑥 / 𝑘 ⦌ 𝐵 )
2 nfcv ⊢ Ⅎ 𝑥 𝐵
3 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐵
4 1 2 3 cbvsum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐵
5 simpl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → 𝐴 ∈ Fin )
6 rspcsbela ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
7 6 expcom ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ → ( 𝑥 ∈ 𝐴 → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
8 7 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( 𝑥 ∈ 𝐴 → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
10 5 9 fsumzcl ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ )
11 4 10 eqeltrid ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )