Theorem fsumcom 6974

Description: Interchange order of summation. Warning: The HTML proof page is 0.6MB in size.

Assertion

Ref	Expression
fsumcom	⊢ ((K ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...K)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...K)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...K)A)

Distinct variable groups:   j,m,J   j,K,m   j,M,m   j,N,m

Proof of Theorem fsumcom

Step	Hyp	Ref	Expression
1		opreq2 3960	. . . . . 6 ⊢ (k = J → (J...k) = (J...J))
2	1	raleq1d 1786	. . . . 5 ⊢ (k = J → (∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ ↔ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ))
3	2	anbi2d 615	. . . 4 ⊢ (k = J → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) ↔ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)))
4	1	sumeq1d 6936	. . . . 5 ⊢ (k = J → Σj ∈ (J...k)Σm ∈ (M...N)A = Σj ∈ (J...J)Σm ∈ (M...N)A)
5	1	sumeq1d 6936	. . . . . 6 ⊢ (k = J → Σj ∈ (J...k)A = Σj ∈ (J...J)A)
6	5	sumeq2sdv 6939	. . . . 5 ⊢ (k = J → Σm ∈ (M...N)Σj ∈ (J...k)A = Σm ∈ (M...N)Σj ∈ (J...J)A)
7	4, 6	eqeq12d 1486	. . . 4 ⊢ (k = J → (Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A ↔ Σj ∈ (J...J)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...J)A))
8	3, 7	imbi12d 625	. . 3 ⊢ (k = J → (((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A) ↔ ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...J)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...J)A)))
9		opreq2 3960	. . . . . 6 ⊢ (k = n → (J...k) = (J...n))
10	9	raleq1d 1786	. . . . 5 ⊢ (k = n → (∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ ↔ ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ))
11	10	anbi2d 615	. . . 4 ⊢ (k = n → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) ↔ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ)))
12	9	sumeq1d 6936	. . . . 5 ⊢ (k = n → Σj ∈ (J...k)Σm ∈ (M...N)A = Σj ∈ (J...n)Σm ∈ (M...N)A)
13	9	sumeq1d 6936	. . . . . 6 ⊢ (k = n → Σj ∈ (J...k)A = Σj ∈ (J...n)A)
14	13	sumeq2sdv 6939	. . . . 5 ⊢ (k = n → Σm ∈ (M...N)Σj ∈ (J...k)A = Σm ∈ (M...N)Σj ∈ (J...n)A)
15	12, 14	eqeq12d 1486	. . . 4 ⊢ (k = n → (Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A ↔ Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A))
16	11, 15	imbi12d 625	. . 3 ⊢ (k = n → (((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A) ↔ ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A)))
17		opreq2 3960	. . . . . 6 ⊢ (k = (n + 1) → (J...k) = (J...(n + 1)))
18	17	raleq1d 1786	. . . . 5 ⊢ (k = (n + 1) → (∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ ↔ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ))
19	18	anbi2d 615	. . . 4 ⊢ (k = (n + 1) → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) ↔ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ)))
20	17	sumeq1d 6936	. . . . 5 ⊢ (k = (n + 1) → Σj ∈ (J...k)Σm ∈ (M...N)A = Σj ∈ (J...(n + 1))Σm ∈ (M...N)A)
21	17	sumeq1d 6936	. . . . . 6 ⊢ (k = (n + 1) → Σj ∈ (J...k)A = Σj ∈ (J...(n + 1))A)
22	21	sumeq2sdv 6939	. . . . 5 ⊢ (k = (n + 1) → Σm ∈ (M...N)Σj ∈ (J...k)A = Σm ∈ (M...N)Σj ∈ (J...(n + 1))A)
23	20, 22	eqeq12d 1486	. . . 4 ⊢ (k = (n + 1) → (Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A ↔ Σj ∈ (J...(n + 1))Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...(n + 1))A))
24	19, 23	imbi12d 625	. . 3 ⊢ (k = (n + 1) → (((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A) ↔ ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...(n + 1))Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...(n + 1))A)))
25		opreq2 3960	. . . . . 6 ⊢ (k = K → (J...k) = (J...K))
26	25	raleq1d 1786	. . . . 5 ⊢ (k = K → (∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ ↔ ∀j ∈ (J...K)∀m ∈ (M...N)A ∈ ℂ))
27	26	anbi2d 615	. . . 4 ⊢ (k = K → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) ↔ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...K)∀m ∈ (M...N)A ∈ ℂ)))
28	25	sumeq1d 6936	. . . . 5 ⊢ (k = K → Σj ∈ (J...k)Σm ∈ (M...N)A = Σj ∈ (J...K)Σm ∈ (M...N)A)
29	25	sumeq1d 6936	. . . . . 6 ⊢ (k = K → Σj ∈ (J...k)A = Σj ∈ (J...K)A)
30	29	sumeq2sdv 6939	. . . . 5 ⊢ (k = K → Σm ∈ (M...N)Σj ∈ (J...k)A = Σm ∈ (M...N)Σj ∈ (J...K)A)
31	28, 30	eqeq12d 1486	. . . 4 ⊢ (k = K → (Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A ↔ Σj ∈ (J...K)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...K)A))
32	27, 31	imbi12d 625	. . 3 ⊢ (k = K → (((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...k)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...k)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...k)A) ↔ ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...K)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...K)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...K)A)))
33		csbfsum 6973	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)[J / j]A ∈ ℂ) → [J / j]Σm ∈ (M...N)A = Σm ∈ (M...N)[J / j]A)
34		pm3.26 319	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → J ∈ ℤ)
35		simprl 414	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → N ∈ (ℤ≥ ‘M))
36		ra4csbela 2038	. . . . . . . . . . . 12 ⊢ ((J ∈ (J...J) ⋀ ∀j ∈ (J...J)A ∈ ℂ) → [J / j]A ∈ ℂ)
37		elfz3t 6431	. . . . . . . . . . . 12 ⊢ (J ∈ ℤ → J ∈ (J...J))
38	36, 37	sylan 448	. . . . . . . . . . 11 ⊢ ((J ∈ ℤ ⋀ ∀j ∈ (J...J)A ∈ ℂ) → [J / j]A ∈ ℂ)
39	38	ex 373	. . . . . . . . . 10 ⊢ (J ∈ ℤ → (∀j ∈ (J...J)A ∈ ℂ → [J / j]A ∈ ℂ))
40	39	r19.20sdv 1707	. . . . . . . . 9 ⊢ (J ∈ ℤ → (∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ → ∀m ∈ (M...N)[J / j]A ∈ ℂ))
41	40	imp 350	. . . . . . . 8 ⊢ ((J ∈ ℤ ⋀ ∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ) → ∀m ∈ (M...N)[J / j]A ∈ ℂ)
42		ralcom 1771	. . . . . . . 8 ⊢ (∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ)
43	41, 42	sylan2b 452	. . . . . . 7 ⊢ ((J ∈ ℤ ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ) → ∀m ∈ (M...N)[J / j]A ∈ ℂ)
44	43	adantrl 394	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → ∀m ∈ (M...N)[J / j]A ∈ ℂ)
45	33, 34, 35, 44	syl3anc 857	. . . . 5 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → [J / j]Σm ∈ (M...N)A = Σm ∈ (M...N)[J / j]A)
46		fsum1s 6955	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ ∀j ∈ (J...J)Σm ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...J)Σm ∈ (M...N)A = [J / j]Σm ∈ (M...N)A)
47		fsumclt 6961	. . . . . . . . 9 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)A ∈ ℂ) → Σm ∈ (M...N)A ∈ ℂ)
48	47	ex 373	. . . . . . . 8 ⊢ (N ∈ (ℤ≥ ‘M) → (∀m ∈ (M...N)A ∈ ℂ → Σm ∈ (M...N)A ∈ ℂ))
49	48	r19.20sdv 1707	. . . . . . 7 ⊢ (N ∈ (ℤ≥ ‘M) → (∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ → ∀j ∈ (J...J)Σm ∈ (M...N)A ∈ ℂ))
50	49	imp 350	. . . . . 6 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ) → ∀j ∈ (J...J)Σm ∈ (M...N)A ∈ ℂ)
51	46, 50	sylan2 451	. . . . 5 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → Σj ∈ (J...J)Σm ∈ (M...N)A = [J / j]Σm ∈ (M...N)A)
52		fsum1s 6955	. . . . . . . . . . 11 ⊢ ((J ∈ ℤ ⋀ ∀j ∈ (J...J)A ∈ ℂ) → Σj ∈ (J...J)A = [J / j]A)
53	52	ex 373	. . . . . . . . . 10 ⊢ (J ∈ ℤ → (∀j ∈ (J...J)A ∈ ℂ → Σj ∈ (J...J)A = [J / j]A))
54	53	r19.20sdv 1707	. . . . . . . . 9 ⊢ (J ∈ ℤ → (∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ → ∀m ∈ (M...N)Σj ∈ (J...J)A = [J / j]A))
55	54	imp 350	. . . . . . . 8 ⊢ ((J ∈ ℤ ⋀ ∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ) → ∀m ∈ (M...N)Σj ∈ (J...J)A = [J / j]A)
56	55	sumeq2d 6937	. . . . . . 7 ⊢ ((J ∈ ℤ ⋀ ∀m ∈ (M...N)∀j ∈ (J...J)A ∈ ℂ) → Σm ∈ (M...N)Σj ∈ (J...J)A = Σm ∈ (M...N)[J / j]A)
57	56, 42	sylan2b 452	. . . . . 6 ⊢ ((J ∈ ℤ ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ) → Σm ∈ (M...N)Σj ∈ (J...J)A = Σm ∈ (M...N)[J / j]A)
58	57	adantrl 394	. . . . 5 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → Σm ∈ (M...N)Σj ∈ (J...J)A = Σm ∈ (M...N)[J / j]A)
59	45, 51, 58	3eqtr4d 1514	. . . 4 ⊢ ((J ∈ ℤ ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ)) → Σj ∈ (J...J)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...J)A)
60	59	ex 373	. . 3 ⊢ (J ∈ ℤ → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...J)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...J)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...J)A))
61		fzssp1t 6446	. . . . . . . . . 10 ⊢ ((J ∈ ℤ ⋀ n ∈ ℤ) → (J...n) ⊆ (J...(n + 1)))
62		eluzel2 6364	. . . . . . . . . 10 ⊢ (n ∈ (ℤ≥ ‘J) → J ∈ ℤ)
63		eluzelz 6363	. . . . . . . . . 10 ⊢ (n ∈ (ℤ≥ ‘J) → n ∈ ℤ)
64	61, 62, 63	sylanc 471	. . . . . . . . 9 ⊢ (n ∈ (ℤ≥ ‘J) → (J...n) ⊆ (J...(n + 1)))
65	64	sseld 2063	. . . . . . . 8 ⊢ (n ∈ (ℤ≥ ‘J) → (j ∈ (J...n) → j ∈ (J...(n + 1))))
66	65	imim1d 28	. . . . . . 7 ⊢ (n ∈ (ℤ≥ ‘J) → ((j ∈ (J...(n + 1)) → ∀m ∈ (M...N)A ∈ ℂ) → (j ∈ (J...n) → ∀m ∈ (M...N)A ∈ ℂ)))
67	66	r19.20dv2 1708	. . . . . 6 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ → ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ))
68	67	anim2d 560	. . . . 5 ⊢ (n ∈ (ℤ≥ ‘J) → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → (N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ)))
69	68	imim1d 28	. . . 4 ⊢ (n ∈ (ℤ≥ ‘J) → (((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...n)∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A) → ((N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A)))
70		id 59	. . . . . . . . . 10 ⊢ (Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A → Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A)
71		oprex 3974	. . . . . . . . . . . 12 ⊢ (n + 1) ∈ V
72		csbfsum 6973	. . . . . . . . . . . 12 ⊢ (((n + 1) ∈ V ⋀ N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ) → [(n + 1) / j]Σm ∈ (M...N)A = Σm ∈ (M...N)[(n + 1) / j]A)
73	71, 72	mp3an1 901	. . . . . . . . . . 11 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ) → [(n + 1) / j]Σm ∈ (M...N)A = Σm ∈ (M...N)[(n + 1) / j]A)
74		simplr 413	. . . . . . . . . . 11 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → N ∈ (ℤ≥ ‘M))
75		ra4csbela 2038	. . . . . . . . . . . . . . . . 17 ⊢ (((n + 1) ∈ (J...(n + 1)) ⋀ ∀j ∈ (J...(n + 1))A ∈ ℂ) → [(n + 1) / j]A ∈ ℂ)
76		peano2uz 6387	. . . . . . . . . . . . . . . . . 18 ⊢ (n ∈ (ℤ≥ ‘J) → (n + 1) ∈ (ℤ≥ ‘J))
77		eluzfz2t 6429	. . . . . . . . . . . . . . . . . 18 ⊢ ((n + 1) ∈ (ℤ≥ ‘J) → (n + 1) ∈ (J...(n + 1)))
78	76, 77	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ≥ ‘J) → (n + 1) ∈ (J...(n + 1)))
79	75, 78	sylan 448	. . . . . . . . . . . . . . . 16 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀j ∈ (J...(n + 1))A ∈ ℂ) → [(n + 1) / j]A ∈ ℂ)
80	79	ex 373	. . . . . . . . . . . . . . 15 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))A ∈ ℂ → [(n + 1) / j]A ∈ ℂ))
81	80	r19.20sdv 1707	. . . . . . . . . . . . . 14 ⊢ (n ∈ (ℤ≥ ‘J) → (∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ → ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ))
82	81	imp 350	. . . . . . . . . . . . 13 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ)
83		ralcom 1771	. . . . . . . . . . . . 13 ⊢ (∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ)
84	82, 83	sylan2b 452	. . . . . . . . . . . 12 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ)
85	84	adantlr 393	. . . . . . . . . . 11 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → ∀m ∈ (M...N)[(n + 1) / j]A ∈ ℂ)
86	73, 74, 85	sylanc 471	. . . . . . . . . 10 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → [(n + 1) / j]Σm ∈ (M...N)A = Σm ∈ (M...N)[(n + 1) / j]A)
87	70, 86	opreqan12rd 3971	. . . . . . . . 9 ⊢ ((((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) ⋀ Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A) → (Σj ∈ (J...n)Σm ∈ (M...N)A + [(n + 1) / j]Σm ∈ (M...N)A) = (Σm ∈ (M...N)Σj ∈ (J...n)A + Σm ∈ (M...N)[(n + 1) / j]A))
88	87	anasss 440	. . . . . . . 8 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ (∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ ⋀ Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A)) → (Σj ∈ (J...n)Σm ∈ (M...N)A + [(n + 1) / j]Σm ∈ (M...N)A) = (Σm ∈ (M...N)Σj ∈ (J...n)A + Σm ∈ (M...N)[(n + 1) / j]A))
89		fsump1s 6959	. . . . . . . . . 10 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀j ∈ (J...(n + 1))Σm ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...(n + 1))Σm ∈ (M...N)A = (Σj ∈ (J...n)Σm ∈ (M...N)A + [(n + 1) / j]Σm ∈ (M...N)A))
90		simpll 412	. . . . . . . . . 10 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → n ∈ (ℤ≥ ‘J))
91	48	adantl 388	. . . . . . . . . . . 12 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) → (∀m ∈ (M...N)A ∈ ℂ → Σm ∈ (M...N)A ∈ ℂ))
92	91	r19.20sdv 1707	. . . . . . . . . . 11 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) → (∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ → ∀j ∈ (J...(n + 1))Σm ∈ (M...N)A ∈ ℂ))
93	92	imp 350	. . . . . . . . . 10 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → ∀j ∈ (J...(n + 1))Σm ∈ (M...N)A ∈ ℂ)
94	89, 90, 93	sylanc 471	. . . . . . . . 9 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ) → Σj ∈ (J...(n + 1))Σm ∈ (M...N)A = (Σj ∈ (J...n)Σm ∈ (M...N)A + [(n + 1) / j]Σm ∈ (M...N)A))
95	94	adantrr 395	. . . . . . . 8 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ (∀j ∈ (J...(n + 1))∀m ∈ (M...N)A ∈ ℂ ⋀ Σj ∈ (J...n)Σm ∈ (M...N)A = Σm ∈ (M...N)Σj ∈ (J...n)A)) → Σj ∈ (J...(n + 1))Σm ∈ (M...N)A = (Σj ∈ (J...n)Σm ∈ (M...N)A + [(n + 1) / j]Σm ∈ (M...N)A))
96		fsump1s 6959	. . . . . . . . . . . . . . . 16 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀j ∈ (J...(n + 1))A ∈ ℂ) → Σj ∈ (J...(n + 1))A = (Σj ∈ (J...n)A + [(n + 1) / j]A))
97	96	ex 373	. . . . . . . . . . . . . . 15 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))A ∈ ℂ → Σj ∈ (J...(n + 1))A = (Σj ∈ (J...n)A + [(n + 1) / j]A)))
98	97	r19.20sdv 1707	. . . . . . . . . . . . . 14 ⊢ (n ∈ (ℤ≥ ‘J) → (∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ → ∀m ∈ (M...N)Σj ∈ (J...(n + 1))A = (Σj ∈ (J...n)A + [(n + 1) / j]A)))
99	98	imp 350	. . . . . . . . . . . . 13 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → ∀m ∈ (M...N)Σj ∈ (J...(n + 1))A = (Σj ∈ (J...n)A + [(n + 1) / j]A))
100	99	sumeq2d 6937	. . . . . . . . . . . 12 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → Σm ∈ (M...N)Σj ∈ (J...(n + 1))A = Σm ∈ (M...N)(Σj ∈ (J...n)A + [(n + 1) / j]A))
101	100	adantlr 393	. . . . . . . . . . 11 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → Σm ∈ (M...N)Σj ∈ (J...(n + 1))A = Σm ∈ (M...N)(Σj ∈ (J...n)A + [(n + 1) / j]A))
102		fsumadd 6968	. . . . . . . . . . . 12 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)(Σj ∈ (J...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ)) → Σm ∈ (M...N)(Σj ∈ (J...n)A + [(n + 1) / j]A) = (Σm ∈ (M...N)Σj ∈ (J...n)A + Σm ∈ (M...N)[(n + 1) / j]A))
103		simplr 413	. . . . . . . . . . . 12 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → N ∈ (ℤ≥ ‘M))
104	65	imim1d 28	. . . . . . . . . . . . . . . . . 18 ⊢ (n ∈ (ℤ≥ ‘J) → ((j ∈ (J...(n + 1)) → A ∈ ℂ) → (j ∈ (J...n) → A ∈ ℂ)))
105	104	r19.20dv2 1708	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))A ∈ ℂ → ∀j ∈ (J...n)A ∈ ℂ))
106		fsumclt 6961	. . . . . . . . . . . . . . . . . 18 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀j ∈ (J...n)A ∈ ℂ) → Σj ∈ (J...n)A ∈ ℂ)
107	106	ex 373	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...n)A ∈ ℂ → Σj ∈ (J...n)A ∈ ℂ))
108	105, 107	syld 27	. . . . . . . . . . . . . . . 16 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))A ∈ ℂ → Σj ∈ (J...n)A ∈ ℂ))
109	108, 80	jcad 599	. . . . . . . . . . . . . . 15 ⊢ (n ∈ (ℤ≥ ‘J) → (∀j ∈ (J...(n + 1))A ∈ ℂ → (Σj ∈ (J...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ)))
110	109	r19.20sdv 1707	. . . . . . . . . . . . . 14 ⊢ (n ∈ (ℤ≥ ‘J) → (∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ → ∀m ∈ (M...N)(Σj ∈ (J...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ)))
111	110	imp 350	. . . . . . . . . . . . 13 ⊢ ((n ∈ (ℤ≥ ‘J) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → ∀m ∈ (M...N)(Σj ∈ (J...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ))
112	111	adantlr 393	. . . . . . . . . . . 12 ⊢ (((n ∈ (ℤ≥ ‘J) ⋀ N ∈ (ℤ≥ ‘M)) ⋀ ∀m ∈ (M...N)∀j ∈ (J...(n + 1))A ∈ ℂ) → ∀m ∈ (M...N)(Σj ∈ (J...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ))
113