gsummptp1

Description: Reindex a zero-based sum as a one-base sum. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummptp1.1	$⊢ B = {Base}_{R}$
	gsummptp1.2	$⊢ φ \to R \in CMnd$
	gsummptp1.3	$⊢ φ \to N \in ℕ_{0}$
	gsummptp1.4	$⊢ (φ \land l \in (1 \dots N)) \to Y \in B$
	gsummptp1.5	$⊢ ((φ \land k \in (0 ..^N)) \land l = k + 1) \to Y = X$
Assertion	gsummptp1	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} X = {\sum_{R}}_{l = 1}^{N} Y$

Proof

Step	Hyp	Ref	Expression
1		gsummptp1.1	$⊢ B = {Base}_{R}$
2		gsummptp1.2	$⊢ φ \to R \in CMnd$
3		gsummptp1.3	$⊢ φ \to N \in ℕ_{0}$
4		gsummptp1.4	$⊢ (φ \land l \in (1 \dots N)) \to Y \in B$
5		gsummptp1.5	$⊢ ((φ \land k \in (0 ..^N)) \land l = k + 1) \to Y = X$
6		nfcsb1v	$⊢ \underline{Ⅎ} l ⦋ (k + 1) / l ⦌ Y$
7		eqid	$⊢ 0_{R} = 0_{R}$
8		csbeq1a	$⊢ l = k + 1 \to Y = ⦋ (k + 1) / l ⦌ Y$
9		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
10		ssidd	$⊢ φ \to B \subseteq B$
11		fz0add1fz1	$⊢ (N \in ℕ_{0} \land k \in (0 ..^N)) \to k + 1 \in (1 \dots N)$
12	3 11	sylan	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (1 \dots N)$
13		fz1fzo0m1	$⊢ l \in (1 \dots N) \to l - 1 \in (0 ..^N)$
14	13	adantl	$⊢ (φ \land l \in (1 \dots N)) \to l - 1 \in (0 ..^N)$
15		eqcom	$⊢ k + 1 = l \leftrightarrow l = k + 1$
16		elfzonn0	$⊢ k \in (0 ..^N) \to k \in ℕ_{0}$
17	16	adantl	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to k \in ℕ_{0}$
18	17	nn0cnd	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to k \in ℂ$
19		1cnd	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to 1 \in ℂ$
20		elfznn	$⊢ l \in (1 \dots N) \to l \in ℕ$
21	20	ad2antlr	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to l \in ℕ$
22	21	nncnd	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to l \in ℂ$
23	18 19 22	addlsub	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to (k + 1 = l \leftrightarrow k = l - 1)$
24	15 23	bitr3id	$⊢ ((φ \land l \in (1 \dots N)) \land k \in (0 ..^N)) \to (l = k + 1 \leftrightarrow k = l - 1)$
25	14 24	reu6dv	$⊢ (φ \land l \in (1 \dots N)) \to \exists! k \in (0 ..^N) l = k + 1$
26	6 1 7 8 2 9 10 4 12 25	gsummptf1o	$⊢ φ \to {\sum_{R}}_{l = 1}^{N} Y = \underset{k \in (0 ..^N)}{\sum_{R}} ⦋ (k + 1) / l ⦌ Y$
27	12 5	csbied	$⊢ (φ \land k \in (0 ..^N)) \to ⦋ (k + 1) / l ⦌ Y = X$
28	27	mpteq2dva	$⊢ φ \to (k \in (0 ..^N) ⟼ ⦋ (k + 1) / l ⦌ Y) = (k \in (0 ..^N) ⟼ X)$
29	28	oveq2d	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} ⦋ (k + 1) / l ⦌ Y = \underset{k \in (0 ..^N)}{\sum_{R}} X$
30	26 29	eqtr2d	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} X = {\sum_{R}}_{l = 1}^{N} Y$

Metamath Proof Explorer

Theorem gsummptp1

Proof