gsummptrev

Description: Revert ordering in a group sum. See also gsumwrev . (Contributed by Thierry Arnoux, 15-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		gsummptrev.1	$⊢ B = {Base}_{M}$
2		gsummptrev.2	$⊢ φ \to M \in CMnd$
3		gsummptrev.3	$⊢ φ \to N \in ℕ_{0}$
4		gsummptrev.4	$⊢ (φ \land k \in (0 \dots N)) \to X \in B$
5		gsummptrev.5	$⊢ ((φ \land l \in (0 \dots N)) \land k = N - l) \to X = Y$
6		nfcv	$⊢ \underline{Ⅎ} k Y$
7		eqid	$⊢ 0_{M} = 0_{M}$
8		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
9		ssidd	$⊢ φ \to B \subseteq B$
10		fznn0sub2	$⊢ l \in (0 \dots N) \to N - l \in (0 \dots N)$
11	10	adantl	$⊢ (φ \land l \in (0 \dots N)) \to N - l \in (0 \dots N)$
12		fznn0sub2	$⊢ k \in (0 \dots N) \to N - k \in (0 \dots N)$
13	12	adantl	$⊢ (φ \land k \in (0 \dots N)) \to N - k \in (0 \dots N)$
14		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
15	14	ad2antlr	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to k \in ℕ_{0}$
16	15	nn0cnd	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to k \in ℂ$
17		elfznn0	$⊢ l \in (0 \dots N) \to l \in ℕ_{0}$
18	17	adantl	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to l \in ℕ_{0}$
19	18	nn0cnd	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to l \in ℂ$
20	3	ad2antrr	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to N \in ℕ_{0}$
21	20	nn0cnd	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to N \in ℂ$
22	16 19 21	subexsub	$⊢ ((φ \land k \in (0 \dots N)) \land l \in (0 \dots N)) \to (k = N - l \leftrightarrow l = N - k)$
23	13 22	reu6dv	$⊢ (φ \land k \in (0 \dots N)) \to \exists! l \in (0 \dots N) k = N - l$
24	6 1 7 5 2 8 9 4 11 23	gsummptf1od	$⊢ φ \to {\sum_{M}}_{k = 0}^{N} X = {\sum_{M}}_{l = 0}^{N} Y$

Metamath Proof Explorer

Theorem gsummptrev

Proof