fsum2dsub

Description: Lemma for breprexp - Re-index a double sum, using difference of the initial indices. (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	fzsum2sub.m	$⊢ φ \to M \in ℕ_{0}$
	fzsum2sub.n	$⊢ φ \to N \in ℕ_{0}$
	fzsum2sub.1	$⊢ i = k - j \to A = B$
	fzsum2sub.2	$⊢ (φ \land i \in ℤ_{\geq (- j)} \land j \in (1 \dots N)) \to A \in ℂ$
	fzsum2sub.3	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (M + j + 1 \dots M + N)) \to B = 0$
	fzsum2sub.4	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 ..^j)) \to B = 0$
Assertion	fsum2dsub	$⊢ φ \to \sum_{i = 0}^{M} \sum_{j = 1}^{N} A = \sum_{k = 0}^{M + N} \sum_{j = 1}^{N} B$

Proof

Step	Hyp	Ref	Expression
1		fzsum2sub.m	$⊢ φ \to M \in ℕ_{0}$
2		fzsum2sub.n	$⊢ φ \to N \in ℕ_{0}$
3		fzsum2sub.1	$⊢ i = k - j \to A = B$
4		fzsum2sub.2	$⊢ (φ \land i \in ℤ_{\geq (- j)} \land j \in (1 \dots N)) \to A \in ℂ$
5		fzsum2sub.3	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (M + j + 1 \dots M + N)) \to B = 0$
6		fzsum2sub.4	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 ..^j)) \to B = 0$
7		simpr	$⊢ (φ \land j \in (1 \dots N)) \to j \in (1 \dots N)$
8	7	elfzelzd	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℤ$
9		0zd	$⊢ (φ \land j \in (1 \dots N)) \to 0 \in ℤ$
10	1	nn0zd	$⊢ φ \to M \in ℤ$
11	10	adantr	$⊢ (φ \land j \in (1 \dots N)) \to M \in ℤ$
12		simpll	$⊢ ((φ \land j \in (1 \dots N)) \land i \in (0 \dots M)) \to φ$
13		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
14		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
15	13 14	sstri	$⊢ (1 \dots N) \subseteq ℕ_{0}$
16	15 7	sseldi	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ_{0}$
17		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
18	16 17	eleqtrdi	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℤ_{\geq 0}$
19		neg0	$⊢ - 0 = 0$
20		uzneg	$⊢ j \in ℤ_{\geq 0} \to - 0 \in ℤ_{\geq (- j)}$
21	19 20	eqeltrrid	$⊢ j \in ℤ_{\geq 0} \to 0 \in ℤ_{\geq (- j)}$
22		fzss1	$⊢ 0 \in ℤ_{\geq (- j)} \to (0 \dots M) \subseteq (- j \dots M)$
23	18 21 22	3syl	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots M) \subseteq (- j \dots M)$
24		fzssuz	$⊢ (- j \dots M) \subseteq ℤ_{\geq (- j)}$
25	23 24	sstrdi	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots M) \subseteq ℤ_{\geq (- j)}$
26	25	sselda	$⊢ ((φ \land j \in (1 \dots N)) \land i \in (0 \dots M)) \to i \in ℤ_{\geq (- j)}$
27	7	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land i \in (0 \dots M)) \to j \in (1 \dots N)$
28	12 26 27 4	syl3anc	$⊢ ((φ \land j \in (1 \dots N)) \land i \in (0 \dots M)) \to A \in ℂ$
29	8 9 11 28 3	fsumshft	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{i = 0}^{M} A = \sum_{k = 0 + j}^{M + j} B$
30	1	adantr	$⊢ (φ \land j \in (1 \dots N)) \to M \in ℕ_{0}$
31	13 7	sseldi	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
32	31	nnnn0d	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ_{0}$
33	30 32	nn0addcld	$⊢ (φ \land j \in (1 \dots N)) \to M + j \in ℕ_{0}$
34	33	nn0red	$⊢ (φ \land j \in (1 \dots N)) \to M + j \in ℝ$
35	34	ltp1d	$⊢ (φ \land j \in (1 \dots N)) \to M + j < M + j + 1$
36		fzdisj	$⊢ M + j < M + j + 1 \to (j \dots M + j) \cap (M + j + 1 \dots M + N) = \emptyset$
37	35 36	syl	$⊢ (φ \land j \in (1 \dots N)) \to (j \dots M + j) \cap (M + j + 1 \dots M + N) = \emptyset$
38	2	nn0zd	$⊢ φ \to N \in ℤ$
39	10 38	zaddcld	$⊢ φ \to M + N \in ℤ$
40	39	adantr	$⊢ (φ \land j \in (1 \dots N)) \to M + N \in ℤ$
41	33	nn0zd	$⊢ (φ \land j \in (1 \dots N)) \to M + j \in ℤ$
42	31	nnred	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℝ$
43		nn0addge2	$⊢ (j \in ℝ \land M \in ℕ_{0}) \to j \leq M + j$
44	42 30 43	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to j \leq M + j$
45	2	nn0red	$⊢ φ \to N \in ℝ$
46	45	adantr	$⊢ (φ \land j \in (1 \dots N)) \to N \in ℝ$
47	30	nn0red	$⊢ (φ \land j \in (1 \dots N)) \to M \in ℝ$
48		elfzle2	$⊢ j \in (1 \dots N) \to j \leq N$
49	48	adantl	$⊢ (φ \land j \in (1 \dots N)) \to j \leq N$
50	42 46 47 49	leadd2dd	$⊢ (φ \land j \in (1 \dots N)) \to M + j \leq M + N$
51	8 40 41 44 50	elfzd	$⊢ (φ \land j \in (1 \dots N)) \to M + j \in (j \dots M + N)$
52		fzsplit	$⊢ M + j \in (j \dots M + N) \to (j \dots M + N) = (j \dots M + j) \cup (M + j + 1 \dots M + N)$
53	51 52	syl	$⊢ (φ \land j \in (1 \dots N)) \to (j \dots M + N) = (j \dots M + j) \cup (M + j + 1 \dots M + N)$
54		fzfid	$⊢ (φ \land j \in (1 \dots N)) \to (j \dots M + N) \in Fin$
55		simpll	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to φ$
56	7	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to j \in (1 \dots N)$
57	15 56	sseldi	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to j \in ℕ_{0}$
58		fz2ssnn0	$⊢ j \in ℕ_{0} \to (j \dots M + N) \subseteq ℕ_{0}$
59	57 58	syl	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to (j \dots M + N) \subseteq ℕ_{0}$
60		simpr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to k \in (j \dots M + N)$
61	59 60	sseldd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to k \in ℕ_{0}$
62	3	eleq1d	$⊢ i = k - j \to (A \in ℂ \leftrightarrow B \in ℂ)$
63		simpll	$⊢ ((φ \land i \in ℤ_{\geq (- j)}) \land j \in (1 \dots N)) \to φ$
64		simplr	$⊢ ((φ \land i \in ℤ_{\geq (- j)}) \land j \in (1 \dots N)) \to i \in ℤ_{\geq (- j)}$
65		simpr	$⊢ ((φ \land i \in ℤ_{\geq (- j)}) \land j \in (1 \dots N)) \to j \in (1 \dots N)$
66	63 64 65 4	syl3anc	$⊢ ((φ \land i \in ℤ_{\geq (- j)}) \land j \in (1 \dots N)) \to A \in ℂ$
67	66	an32s	$⊢ ((φ \land j \in (1 \dots N)) \land i \in ℤ_{\geq (- j)}) \to A \in ℂ$
68	67	ralrimiva	$⊢ (φ \land j \in (1 \dots N)) \to \forall i \in ℤ_{\geq (- j)} A \in ℂ$
69	68	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to \forall i \in ℤ_{\geq (- j)} A \in ℂ$
70		nnsscn	$⊢ ℕ \subseteq ℂ$
71	13 70	sstri	$⊢ (1 \dots N) \subseteq ℂ$
72		simplr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to j \in (1 \dots N)$
73	71 72	sseldi	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to j \in ℂ$
74		simpr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
75	74	nn0cnd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to k \in ℂ$
76	73 75	negsubdi2d	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to - (j - k) = k - j$
77	72	elfzelzd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to j \in ℤ$
78		eluzmn	$⊢ (j \in ℤ \land k \in ℕ_{0}) \to j \in ℤ_{\geq (j - k)}$
79	77 74 78	syl2anc	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to j \in ℤ_{\geq (j - k)}$
80		uzneg	$⊢ j \in ℤ_{\geq (j - k)} \to - (j - k) \in ℤ_{\geq (- j)}$
81	79 80	syl	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to - (j - k) \in ℤ_{\geq (- j)}$
82	76 81	eqeltrrd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to k - j \in ℤ_{\geq (- j)}$
83	62 69 82	rspcdva	$⊢ ((φ \land j \in (1 \dots N)) \land k \in ℕ_{0}) \to B \in ℂ$
84	55 56 61 83	syl21anc	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (j \dots M + N)) \to B \in ℂ$
85	37 53 54 84	fsumsplit	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = j}^{M + N} B = \sum_{k = j}^{M + j} B + \sum_{k = M + j + 1}^{M + N} B$
86	8	zcnd	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℂ$
87	86	addid2d	$⊢ (φ \land j \in (1 \dots N)) \to 0 + j = j$
88	87	oveq1d	$⊢ (φ \land j \in (1 \dots N)) \to (0 + j \dots M + j) = (j \dots M + j)$
89	88	eqcomd	$⊢ (φ \land j \in (1 \dots N)) \to (j \dots M + j) = (0 + j \dots M + j)$
90	89	sumeq1d	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = j}^{M + j} B = \sum_{k = 0 + j}^{M + j} B$
91	5	sumeq2dv	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = M + j + 1}^{M + N} B = \sum_{k = M + j + 1}^{M + N} 0$
92		fzfi	$⊢ (M + j + 1 \dots M + N) \in Fin$
93		sumz	$⊢ ((M + j + 1 \dots M + N) \subseteq ℤ_{\geq 0} \lor (M + j + 1 \dots M + N) \in Fin) \to \sum_{k = M + j + 1}^{M + N} 0 = 0$
94	93	olcs	$⊢ (M + j + 1 \dots M + N) \in Fin \to \sum_{k = M + j + 1}^{M + N} 0 = 0$
95	92 94	ax-mp	$⊢ \sum_{k = M + j + 1}^{M + N} 0 = 0$
96	91 95	eqtrdi	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = M + j + 1}^{M + N} B = 0$
97	90 96	oveq12d	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = j}^{M + j} B + \sum_{k = M + j + 1}^{M + N} B = \sum_{k = 0 + j}^{M + j} B + 0$
98		fzfid	$⊢ (φ \land j \in (1 \dots N)) \to (0 + j \dots M + j) \in Fin$
99		simpll	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to φ$
100	7	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to j \in (1 \dots N)$
101		elfzuz3	$⊢ j \in (1 \dots N) \to N \in ℤ_{\geq j}$
102	101	adantl	$⊢ (φ \land j \in (1 \dots N)) \to N \in ℤ_{\geq j}$
103		eluzadd	$⊢ (N \in ℤ_{\geq j} \land M \in ℤ) \to N + M \in ℤ_{\geq (j + M)}$
104	102 11 103	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to N + M \in ℤ_{\geq (j + M)}$
105	2	nn0cnd	$⊢ φ \to N \in ℂ$
106	105	adantr	$⊢ (φ \land j \in (1 \dots N)) \to N \in ℂ$
107		zsscn	$⊢ ℤ \subseteq ℂ$
108	107 11	sseldi	$⊢ (φ \land j \in (1 \dots N)) \to M \in ℂ$
109	106 108	addcomd	$⊢ (φ \land j \in (1 \dots N)) \to N + M = M + N$
110	86 108	addcomd	$⊢ (φ \land j \in (1 \dots N)) \to j + M = M + j$
111	110	fveq2d	$⊢ (φ \land j \in (1 \dots N)) \to ℤ_{\geq (j + M)} = ℤ_{\geq (M + j)}$
112	104 109 111	3eltr3d	$⊢ (φ \land j \in (1 \dots N)) \to M + N \in ℤ_{\geq (M + j)}$
113	112	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to M + N \in ℤ_{\geq (M + j)}$
114		fzss2	$⊢ M + N \in ℤ_{\geq (M + j)} \to (j \dots M + j) \subseteq (j \dots M + N)$
115	113 114	syl	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to (j \dots M + j) \subseteq (j \dots M + N)$
116		simpr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to k \in (0 + j \dots M + j)$
117	88	adantr	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to (0 + j \dots M + j) = (j \dots M + j)$
118	116 117	eleqtrd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to k \in (j \dots M + j)$
119	115 118	sseldd	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to k \in (j \dots M + N)$
120	99 100 119 61	syl21anc	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to k \in ℕ_{0}$
121	99 100 120 83	syl21anc	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 + j \dots M + j)) \to B \in ℂ$
122	98 121	fsumcl	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = 0 + j}^{M + j} B \in ℂ$
123	122	addid1d	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = 0 + j}^{M + j} B + 0 = \sum_{k = 0 + j}^{M + j} B$
124	85 97 123	3eqtrrd	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = 0 + j}^{M + j} B = \sum_{k = j}^{M + N} B$
125		fzval3	$⊢ M + N \in ℤ \to (j \dots M + N) = (j ..^M + N + 1)$
126	40 125	syl	$⊢ (φ \land j \in (1 \dots N)) \to (j \dots M + N) = (j ..^M + N + 1)$
127	126	ineq2d	$⊢ (φ \land j \in (1 \dots N)) \to (0 ..^j) \cap (j \dots M + N) = (0 ..^j) \cap (j ..^M + N + 1)$
128		fzodisj	$⊢ (0 ..^j) \cap (j ..^M + N + 1) = \emptyset$
129	127 128	eqtrdi	$⊢ (φ \land j \in (1 \dots N)) \to (0 ..^j) \cap (j \dots M + N) = \emptyset$
130	40	peano2zd	$⊢ (φ \land j \in (1 \dots N)) \to M + N + 1 \in ℤ$
131	32	nn0ge0d	$⊢ (φ \land j \in (1 \dots N)) \to 0 \leq j$
132	130	zred	$⊢ (φ \land j \in (1 \dots N)) \to M + N + 1 \in ℝ$
133	40	zred	$⊢ (φ \land j \in (1 \dots N)) \to M + N \in ℝ$
134		nn0addge2	$⊢ (N \in ℝ \land M \in ℕ_{0}) \to N \leq M + N$
135	45 1 134	syl2anc	$⊢ φ \to N \leq M + N$
136	135	adantr	$⊢ (φ \land j \in (1 \dots N)) \to N \leq M + N$
137	133	lep1d	$⊢ (φ \land j \in (1 \dots N)) \to M + N \leq M + N + 1$
138	46 133 132 136 137	letrd	$⊢ (φ \land j \in (1 \dots N)) \to N \leq M + N + 1$
139	42 46 132 49 138	letrd	$⊢ (φ \land j \in (1 \dots N)) \to j \leq M + N + 1$
140	9 130 8 131 139	elfzd	$⊢ (φ \land j \in (1 \dots N)) \to j \in (0 \dots M + N + 1)$
141		fzosplit	$⊢ j \in (0 \dots M + N + 1) \to (0 ..^M + N + 1) = (0 ..^j) \cup (j ..^M + N + 1)$
142	140 141	syl	$⊢ (φ \land j \in (1 \dots N)) \to (0 ..^M + N + 1) = (0 ..^j) \cup (j ..^M + N + 1)$
143		fzval3	$⊢ M + N \in ℤ \to (0 \dots M + N) = (0 ..^M + N + 1)$
144	40 143	syl	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots M + N) = (0 ..^M + N + 1)$
145	126	uneq2d	$⊢ (φ \land j \in (1 \dots N)) \to (0 ..^j) \cup (j \dots M + N) = (0 ..^j) \cup (j ..^M + N + 1)$
146	142 144 145	3eqtr4d	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots M + N) = (0 ..^j) \cup (j \dots M + N)$
147		fzfid	$⊢ φ \to (0 \dots M + N) \in Fin$
148	147	adantr	$⊢ (φ \land j \in (1 \dots N)) \to (0 \dots M + N) \in Fin$
149		simpl	$⊢ (φ \land (k \in (0 \dots M + N) \land j \in (1 \dots N))) \to φ$
150	7	adantrl	$⊢ (φ \land (k \in (0 \dots M + N) \land j \in (1 \dots N))) \to j \in (1 \dots N)$
151		fz0ssnn0	$⊢ (0 \dots M + N) \subseteq ℕ_{0}$
152		simprl	$⊢ (φ \land (k \in (0 \dots M + N) \land j \in (1 \dots N))) \to k \in (0 \dots M + N)$
153	151 152	sseldi	$⊢ (φ \land (k \in (0 \dots M + N) \land j \in (1 \dots N))) \to k \in ℕ_{0}$
154	149 150 153 83	syl21anc	$⊢ (φ \land (k \in (0 \dots M + N) \land j \in (1 \dots N))) \to B \in ℂ$
155	154	anass1rs	$⊢ ((φ \land j \in (1 \dots N)) \land k \in (0 \dots M + N)) \to B \in ℂ$
156	129 146 148 155	fsumsplit	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = 0}^{M + N} B = \sum_{k \in (0 ..^j)} B + \sum_{k = j}^{M + N} B$
157	6	sumeq2dv	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k \in (0 ..^j)} B = \sum_{k \in (0 ..^j)} 0$
158		fzofi	$⊢ (0 ..^j) \in Fin$
159		sumz	$⊢ ((0 ..^j) \subseteq ℤ_{\geq 0} \lor (0 ..^j) \in Fin) \to \sum_{k \in (0 ..^j)} 0 = 0$
160	159	olcs	$⊢ (0 ..^j) \in Fin \to \sum_{k \in (0 ..^j)} 0 = 0$
161	158 160	ax-mp	$⊢ \sum_{k \in (0 ..^j)} 0 = 0$
162	157 161	eqtrdi	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k \in (0 ..^j)} B = 0$
163	162	oveq1d	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k \in (0 ..^j)} B + \sum_{k = j}^{M + N} B = 0 + \sum_{k = j}^{M + N} B$
164	54 84	fsumcl	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = j}^{M + N} B \in ℂ$
165	164	addid2d	$⊢ (φ \land j \in (1 \dots N)) \to 0 + \sum_{k = j}^{M + N} B = \sum_{k = j}^{M + N} B$
166	156 163 165	3eqtrrd	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = j}^{M + N} B = \sum_{k = 0}^{M + N} B$
167	124 166	eqtrd	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{k = 0 + j}^{M + j} B = \sum_{k = 0}^{M + N} B$
168	29 167	eqtrd	$⊢ (φ \land j \in (1 \dots N)) \to \sum_{i = 0}^{M} A = \sum_{k = 0}^{M + N} B$
169	168	sumeq2dv	$⊢ φ \to \sum_{j = 1}^{N} \sum_{i = 0}^{M} A = \sum_{j = 1}^{N} \sum_{k = 0}^{M + N} B$
170		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
171		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
172	28	anasss	$⊢ (φ \land (j \in (1 \dots N) \land i \in (0 \dots M))) \to A \in ℂ$
173	172	ancom2s	$⊢ (φ \land (i \in (0 \dots M) \land j \in (1 \dots N))) \to A \in ℂ$
174	170 171 173	fsumcom	$⊢ φ \to \sum_{i = 0}^{M} \sum_{j = 1}^{N} A = \sum_{j = 1}^{N} \sum_{i = 0}^{M} A$
175	147 171 154	fsumcom	$⊢ φ \to \sum_{k = 0}^{M + N} \sum_{j = 1}^{N} B = \sum_{j = 1}^{N} \sum_{k = 0}^{M + N} B$
176	169 174 175	3eqtr4d	$⊢ φ \to \sum_{i = 0}^{M} \sum_{j = 1}^{N} A = \sum_{k = 0}^{M + N} \sum_{j = 1}^{N} B$

Metamath Proof Explorer

Theorem fsum2dsub

Proof