fsumzcl2

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

		Ref	Expression
	Assertion	fsumzcl2	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B \in ℤ$

Step	Hyp	Ref	Expression
1		csbeq1a	$⊢ k = x \to B = ⦋ x / k ⦌ B$
2		nfcv	$⊢ \underline{Ⅎ} x B$
3		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ x / k ⦌ B$
4	1 2 3	cbvsum	$⊢ \sum_{k \in A} B = \sum_{x \in A} ⦋ x / k ⦌ B$
5		simpl	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to A \in Fin$
6		rspcsbela	$⊢ (x \in A \land \forall k \in A B \in ℤ) \to ⦋ x / k ⦌ B \in ℤ$
7	6	expcom	$⊢ \forall k \in A B \in ℤ \to (x \in A \to ⦋ x / k ⦌ B \in ℤ)$
8	7	adantl	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to (x \in A \to ⦋ x / k ⦌ B \in ℤ)$
9	8	imp	$⊢ ((A \in Fin \land \forall k \in A B \in ℤ) \land x \in A) \to ⦋ x / k ⦌ B \in ℤ$
10	5 9	fsumzcl	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to \sum_{x \in A} ⦋ x / k ⦌ B \in ℤ$
11	4 10	eqeltrid	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B \in ℤ$

Metamath Proof Explorer