gsumzrsum

Description: Relate a group sum on ZZring to a finite sum on the complex numbers. See also gsumfsum . (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumzrsum.1	$⊢ φ \to A \in Fin$
	gsumzrsum.2	$⊢ (φ \land k \in A) \to B \in ℤ$
Assertion	gsumzrsum	$⊢ φ \to \underset{k \in A}{\sum_{ℤ_{ring}}} B = \sum_{k \in A} B$

Step	Hyp	Ref	Expression
1		gsumzrsum.1	$⊢ φ \to A \in Fin$
2		gsumzrsum.2	$⊢ (φ \land k \in A) \to B \in ℤ$
3		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
4		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
5		df-zring	$⊢ ℤ_{ring} = ℂ_{fld} ↾_{𝑠} ℤ$
6		cnfldex	$⊢ ℂ_{fld} \in V$
7	6	a1i	$⊢ φ \to ℂ_{fld} \in V$
8		zsscn	$⊢ ℤ \subseteq ℂ$
9	8	a1i	$⊢ φ \to ℤ \subseteq ℂ$
10	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℤ$
11		0zd	$⊢ φ \to 0 \in ℤ$
12		addlid	$⊢ k \in ℂ \to 0 + k = k$
13		addrid	$⊢ k \in ℂ \to k + 0 = k$
14	12 13	jca	$⊢ k \in ℂ \to (0 + k = k \land k + 0 = k)$
15	14	adantl	$⊢ (φ \land k \in ℂ) \to (0 + k = k \land k + 0 = k)$
16	3 4 5 7 1 9 10 11 15	gsumress	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \underset{k \in A}{\sum_{ℤ_{ring}}} B$
17	2	zcnd	$⊢ (φ \land k \in A) \to B \in ℂ$
18	1 17	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$
19	16 18	eqtr3d	$⊢ φ \to \underset{k \in A}{\sum_{ℤ_{ring}}} B = \sum_{k \in A} B$

Metamath Proof Explorer