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