Theorem 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	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumzrsum.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \mathbb{Z}$$
Assertion	gsumzrsum	$$⊢\phi \to \underset{k\in A}{{\sum }_{{\mathbb{Z}}_{\mathrm{ring}}}}B=\sum _{k\in A}B$$

Proof

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