Theorem fsumsplit 6958

Description: Split a finite sum into two parts. Warning: The HTML proof page is 0.6 megabyte in size.

Assertion

Ref	Expression
fsumsplit	⊢ ((N ∈ ℤ ⋀ K ∈ (M...(N − 1)) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...K)A + Σk ∈ ((K + 1)...N)A))

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumsplit

Step	Hyp	Ref	Expression
1		breq1 2612	. . . . . . . . 9 ⊢ (j = M → (j < N ↔ M < N))
2	1	anbi2d 614	. . . . . . . 8 ⊢ (j = M → ((N ∈ ℤ ⋀ j < N) ↔ (N ∈ ℤ ⋀ M < N)))
3	2	anbi1d 615	. . . . . . 7 ⊢ (j = M → (((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) ↔ ((N ∈ ℤ ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
4		opreq2 3954	. . . . . . . . . 10 ⊢ (j = M → (M...j) = (M...M))
5	4	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = M → Σk ∈ (M...j)A = Σk ∈ (M...M)A)
6		opreq1 3953	. . . . . . . . . . 11 ⊢ (j = M → (j + 1) = (M + 1))
7	6	opreq1d 3960	. . . . . . . . . 10 ⊢ (j = M → ((j + 1)...N) = ((M + 1)...N))
8	7	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = M → Σk ∈ ((j + 1)...N)A = Σk ∈ ((M + 1)...N)A)
9	5, 8	opreq12d 3963	. . . . . . . 8 ⊢ (j = M → (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A))
10	9	eqeq2d 1478	. . . . . . 7 ⊢ (j = M → (Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) ↔ Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A)))
11	3, 10	imbi12d 624	. . . . . 6 ⊢ (j = M → ((((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A)) ↔ (((N ∈ ℤ ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A))))
12		breq1 2612	. . . . . . . . 9 ⊢ (j = m → (j < N ↔ m < N))
13	12	anbi2d 614	. . . . . . . 8 ⊢ (j = m → ((N ∈ ℤ ⋀ j < N) ↔ (N ∈ ℤ ⋀ m < N)))
14	13	anbi1d 615	. . . . . . 7 ⊢ (j = m → (((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) ↔ ((N ∈ ℤ ⋀ m < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
15		opreq2 3954	. . . . . . . . . 10 ⊢ (j = m → (M...j) = (M...m))
16	15	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = m → Σk ∈ (M...j)A = Σk ∈ (M...m)A)
17		opreq1 3953	. . . . . . . . . . 11 ⊢ (j = m → (j + 1) = (m + 1))
18	17	opreq1d 3960	. . . . . . . . . 10 ⊢ (j = m → ((j + 1)...N) = ((m + 1)...N))
19	18	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = m → Σk ∈ ((j + 1)...N)A = Σk ∈ ((m + 1)...N)A)
20	16, 19	opreq12d 3963	. . . . . . . 8 ⊢ (j = m → (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A))
21	20	eqeq2d 1478	. . . . . . 7 ⊢ (j = m → (Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) ↔ Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A)))
22	14, 21	imbi12d 624	. . . . . 6 ⊢ (j = m → ((((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A)) ↔ (((N ∈ ℤ ⋀ m < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A))))
23		breq1 2612	. . . . . . . . 9 ⊢ (j = (m + 1) → (j < N ↔ (m + 1) < N))
24	23	anbi2d 614	. . . . . . . 8 ⊢ (j = (m + 1) → ((N ∈ ℤ ⋀ j < N) ↔ (N ∈ ℤ ⋀ (m + 1) < N)))
25	24	anbi1d 615	. . . . . . 7 ⊢ (j = (m + 1) → (((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) ↔ ((N ∈ ℤ ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
26		opreq2 3954	. . . . . . . . . 10 ⊢ (j = (m + 1) → (M...j) = (M...(m + 1)))
27	26	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = (m + 1) → Σk ∈ (M...j)A = Σk ∈ (M...(m + 1))A)
28		opreq1 3953	. . . . . . . . . . 11 ⊢ (j = (m + 1) → (j + 1) = ((m + 1) + 1))
29	28	opreq1d 3960	. . . . . . . . . 10 ⊢ (j = (m + 1) → ((j + 1)...N) = (((m + 1) + 1)...N))
30	29	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = (m + 1) → Σk ∈ ((j + 1)...N)A = Σk ∈ (((m + 1) + 1)...N)A)
31	27, 30	opreq12d 3963	. . . . . . . 8 ⊢ (j = (m + 1) → (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) = (Σk ∈ (M...(m + 1))A + Σk ∈ (((m + 1) + 1)...N)A))
32	31	eqeq2d 1478	. . . . . . 7 ⊢ (j = (m + 1) → (Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) ↔ Σk ∈ (M...N)A = (Σk ∈ (M...(m + 1))A + Σk ∈ (((m + 1) + 1)...N)A)))
33	25, 32	imbi12d 624	. . . . . 6 ⊢ (j = (m + 1) → ((((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A)) ↔ (((N ∈ ℤ ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...(m + 1))A + Σk ∈ (((m + 1) + 1)...N)A))))
34		breq1 2612	. . . . . . . . 9 ⊢ (j = K → (j < N ↔ K < N))
35	34	anbi2d 614	. . . . . . . 8 ⊢ (j = K → ((N ∈ ℤ ⋀ j < N) ↔ (N ∈ ℤ ⋀ K < N)))
36	35	anbi1d 615	. . . . . . 7 ⊢ (j = K → (((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) ↔ ((N ∈ ℤ ⋀ K < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
37		opreq2 3954	. . . . . . . . . 10 ⊢ (j = K → (M...j) = (M...K))
38	37	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = K → Σk ∈ (M...j)A = Σk ∈ (M...K)A)
39		opreq1 3953	. . . . . . . . . . 11 ⊢ (j = K → (j + 1) = (K + 1))
40	39	opreq1d 3960	. . . . . . . . . 10 ⊢ (j = K → ((j + 1)...N) = ((K + 1)...N))
41	40	sumeq1d 6928	. . . . . . . . 9 ⊢ (j = K → Σk ∈ ((j + 1)...N)A = Σk ∈ ((K + 1)...N)A)
42	38, 41	opreq12d 3963	. . . . . . . 8 ⊢ (j = K → (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) = (Σk ∈ (M...K)A + Σk ∈ ((K + 1)...N)A))
43	42	eqeq2d 1478	. . . . . . 7 ⊢ (j = K → (Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A) ↔ Σk ∈ (M...N)A = (Σk ∈ (M...K)A + Σk ∈ ((K + 1)...N)A)))
44	36, 43	imbi12d 624	. . . . . 6 ⊢ (j = K → ((((N ∈ ℤ ⋀ j < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...j)A + Σk ∈ ((j + 1)...N)A)) ↔ (((N ∈ ℤ ⋀ K < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...K)A + Σk ∈ ((K + 1)...N)A))))
45		fsum1ps 6956	. . . . . . . . . . 11 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ M < N ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = ([M / k]A + Σk ∈ ((M + 1)...N)A))
46	45	3expa 831	. . . . . . . . . 10 ⊢ (((N ∈ (ℤ≥ ‘M) ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = ([M / k]A + Σk ∈ ((M + 1)...N)A))
47		eluzel2 6356	. . . . . . . . . . . . . . . . . 18 ⊢ (N ∈ (ℤ≥ ‘M) → M ∈ ℤ)
48		fzss2t 6436	. . . . . . . . . . . . . . . . . 18 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ M ∈ ℤ) → (M...M) ⊆ (M...N))
49	47, 48	mpdan 702	. . . . . . . . . . . . . . . . 17 ⊢ (N ∈ (ℤ≥ ‘M) → (M...M) ⊆ (M...N))
50	49	sseld 2057	. . . . . . . . . . . . . . . 16 ⊢ (N ∈ (ℤ≥ ‘M) → (k ∈ (M...M) → k ∈ (M...N)))
51	50	imim1d 28	. . . . . . . . . . . . . . 15 ⊢ (N ∈ (ℤ≥ ‘M) → ((k ∈ (M...N) → A ∈ ℂ) → (k ∈ (M...M) → A ∈ ℂ)))
52	51	r19.20dv2 1703	. . . . . . . . . . . . . 14 ⊢ (N ∈ (ℤ≥ ‘M) → (∀k ∈ (M...N)A ∈ ℂ → ∀k ∈ (M...M)A ∈ ℂ))
53	52	imp 350	. . . . . . . . . . . . 13 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ (M...M)A ∈ ℂ)
54		fsum1s 6947	. . . . . . . . . . . . . 14 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → Σk ∈ (M...M)A = [M / k]A)
55	54, 47	sylan 448	. . . . . . . . . . . . 13 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...M)A ∈ ℂ) → Σk ∈ (M...M)A = [M / k]A)
56	53, 55	syldan 467	. . . . . . . . . . . 12 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...M)A = [M / k]A)
57	56	adantlr 393	. . . . . . . . . . 11 ⊢ (((N ∈ (ℤ≥ ‘M) ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...M)A = [M / k]A)
58	57	opreq1d 3960	. . . . . . . . . 10 ⊢ (((N ∈ (ℤ≥ ‘M) ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A) = ([M / k]A + Σk ∈ ((M + 1)...N)A))
59	46, 58	eqtr4d 1502	. . . . . . . . 9 ⊢ (((N ∈ (ℤ≥ ‘M) ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A))
60		ltlet 5493	. . . . . . . . . . . 12 ⊢ ((M ∈ ℝ ⋀ N ∈ ℝ) → (M < N → M ≤ N))
61		zret 6086	. . . . . . . . . . . 12 ⊢ (M ∈ ℤ → M ∈ ℝ)
62		zret 6086	. . . . . . . . . . . 12 ⊢ (N ∈ ℤ → N ∈ ℝ)
63	60, 61, 62	syl2an 454	. . . . . . . . . . 11 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (M < N → M ≤ N))
64		eluzt 6358	. . . . . . . . . . 11 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (N ∈ (ℤ≥ ‘M) ↔ M ≤ N))
65	63, 64	sylibrd 204	. . . . . . . . . 10 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (M < N → N ∈ (ℤ≥ ‘M)))
66	65	impac 387	. . . . . . . . 9 ⊢ (((M ∈ ℤ ⋀ N ∈ ℤ) ⋀ M < N) → (N ∈ (ℤ≥ ‘M) ⋀ M < N))
67	59, 66	sylan 448	. . . . . . . 8 ⊢ ((((M ∈ ℤ ⋀ N ∈ ℤ) ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A))
68	67	exp41 382	. . . . . . 7 ⊢ (M ∈ ℤ → (N ∈ ℤ → (M < N → (∀k ∈ (M...N)A ∈ ℂ → Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A)))))
69	68	imp4c 366	. . . . . 6 ⊢ (M ∈ ℤ → (((N ∈ ℤ ⋀ M < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...M)A + Σk ∈ ((M + 1)...N)A)))
70		eluzelz 6355	. . . . . . . . . . 11 ⊢ (m ∈ (ℤ≥ ‘M) → m ∈ ℤ)
71		ltp1t 5767	. . . . . . . . . . . . . . 15 ⊢ (m ∈ ℝ → m < (m + 1))
72	71	adantr 389	. . . . . . . . . . . . . 14 ⊢ ((m ∈ ℝ ⋀ N ∈ ℝ) → m < (m + 1))
73		axlttrn 5476	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ ℝ ⋀ (m + 1) ∈ ℝ ⋀ N ∈ ℝ) → ((m < (m + 1) ⋀ (m + 1) < N) → m < N))
74	73	3expa 831	. . . . . . . . . . . . . . 15 ⊢ (((m ∈ ℝ ⋀ (m + 1) ∈ ℝ) ⋀ N ∈ ℝ) → ((m < (m + 1) ⋀ (m + 1) < N) → m < N))
75		peano2re 5408	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ ℝ → (m + 1) ∈ ℝ)
76	75	ancli 296	. . . . . . . . . . . . . . 15 ⊢ (m ∈ ℝ → (m ∈ ℝ ⋀ (m + 1) ∈ ℝ))
77	74, 76	sylan 448	. . . . . . . . . . . . . 14 ⊢ ((m ∈ ℝ ⋀ N ∈ ℝ) → ((m < (m + 1) ⋀ (m + 1) < N) → m < N))
78	72, 77	mpand 699	. . . . . . . . . . . . 13 ⊢ ((m ∈ ℝ ⋀ N ∈ ℝ) → ((m + 1) < N → m < N))
79		zret 6086	. . . . . . . . . . . . 13 ⊢ (m ∈ ℤ → m ∈ ℝ)
80	78, 79, 62	syl2an 454	. . . . . . . . . . . 12 ⊢ ((m ∈ ℤ ⋀ N ∈ ℤ) → ((m + 1) < N → m < N))
81	80	ex 373	. . . . . . . . . . 11 ⊢ (m ∈ ℤ → (N ∈ ℤ → ((m + 1) < N → m < N)))
82	70, 81	syl 10	. . . . . . . . . 10 ⊢ (m ∈ (ℤ≥ ‘M) → (N ∈ ℤ → ((m + 1) < N → m < N)))
83	82	imdistand 445	. . . . . . . . 9 ⊢ (m ∈ (ℤ≥ ‘M) → ((N ∈ ℤ ⋀ (m + 1) < N) → (N ∈ ℤ ⋀ m < N)))
84	83	anim1d 558	. . . . . . . 8 ⊢ (m ∈ (ℤ≥ ‘M) → (((N ∈ ℤ ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ((N ∈ ℤ ⋀ m < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
85	84	imim1d 28	. . . . . . 7 ⊢ (m ∈ (ℤ≥ ‘M) → ((((N ∈ ℤ ⋀ m < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A)) → (((N ∈ ℤ ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A))))
86		id 59	. . . . . . . . . . . 12 ⊢ (Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A) → Σk ∈ (M...N)A = (Σk ∈ (M...m)A + Σk ∈ ((m + 1)...N)A))
87		fsump1s 6951	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
88		pm3.26 319	. . . . . . . . . . . . . . . 16 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → m ∈ (ℤ≥ ‘M))
89	88	ad2antrr 404	. . . . . . . . . . . . . . 15 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → m ∈ (ℤ≥ ‘M))
90		fzss2t 6436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((N ∈ (ℤ≥ ‘(m + 1)) ⋀ M ∈ ℤ) → (M...(m + 1)) ⊆ (M...N))
91		ltlet 5493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m + 1) ∈ ℝ ⋀ N ∈ ℝ) → ((m + 1) < N → (m + 1) ≤ N))
92		zret 6086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((m + 1) ∈ ℤ → (m + 1) ∈ ℝ)
93	91, 92, 62	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((m + 1) ∈ ℤ ⋀ N ∈ ℤ) → ((m + 1) < N → (m + 1) ≤ N))
94	93	imp 350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((m + 1) ∈ ℤ ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (m + 1) ≤ N)
95		eluzt 6358	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((m + 1) ∈ ℤ ⋀ N ∈ ℤ) → (N ∈ (ℤ≥ ‘(m + 1)) ↔ (m + 1) ≤ N))
96	95	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((m + 1) ∈ ℤ ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (N ∈ (ℤ≥ ‘(m + 1)) ↔ (m + 1) ≤ N))
97	94, 96	mpbird 196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((m + 1) ∈ ℤ ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → N ∈ (ℤ≥ ‘(m + 1)))
98	70	peano2zd 6114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ ℤ)
99	97, 98	sylanl1 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → N ∈ (ℤ≥ ‘(m + 1)))
100		eluzel2 6356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (m ∈ (ℤ≥ ‘M) → M ∈ ℤ)
101	100	ad2antrr 404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → M ∈ ℤ)
102	90, 99, 101	sylanc 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (M...(m + 1)) ⊆ (M...N))
103	102	sseld 2057	. . . . . . . . . . . . . . . . . 18 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (k ∈ (M...(m + 1)) → k ∈ (M...N)))
104	103	imim1d 28	. . . . . . . . . . . . . . . . 17 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → ((k ∈ (M...N) → A ∈ ℂ) → (k ∈ (M...(m + 1)) → A ∈ ℂ)))
105	104	r19.20dv2 1703	. . . . . . . . . . . . . . . 16 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (∀k ∈ (M...N)A ∈ ℂ → ∀k ∈ (M...(m + 1))A ∈ ℂ))
106	105	imp 350	. . . . . . . . . . . . . . 15 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ (M...(m + 1))A ∈ ℂ)
107	87, 89, 106	sylanc 471	. . . . . . . . . . . . . 14 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
108		fsum1ps 6956	. . . . . . . . . . . . . . . . . 18 ⊢ ((N ∈ (ℤ≥ ‘(m + 1)) ⋀ (m + 1) < N ⋀ ∀k ∈ ((m + 1)...N)A ∈ ℂ) → Σk ∈ ((m + 1)...N)A = ([(m + 1) / k]A + Σk ∈ (((m + 1) + 1)...N)A))
109	93, 95	sylibrd 204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((m + 1) ∈ ℤ ⋀ N ∈ ℤ) → ((m + 1) < N → N ∈ (ℤ≥ ‘(m + 1))))
110	109, 98	sylan 448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((m + 1) < N → N ∈ (ℤ≥ ‘(m + 1))))
111	110	imp 350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → N ∈ (ℤ≥ ‘(m + 1)))
112	111	adantr 389	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → N ∈ (ℤ≥ ‘(m + 1)))
113		simplr 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (m + 1) < N)
114		fzss1t 6435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((m + 1)...N) ⊆ (M...N))
115		peano2uz 6379	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ (ℤ≥ ‘M))
116	114, 115	sylan 448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((m + 1)...N) ⊆ (M...N))
117	116	sseld 2057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (k ∈ ((m + 1)...N) → k ∈ (M...N)))
118	117	imim1d 28	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((k ∈ (M...N) → A ∈ ℂ) → (k ∈ ((m + 1)...N) → A ∈ ℂ)))
119	118	r19.20dv2 1703	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (∀k ∈ (M...N)A ∈ ℂ → ∀k ∈ ((m + 1)...N)A ∈ ℂ))
120	119	imp 350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ ((m + 1)...N)A ∈ ℂ)
121	120	adantlr 393	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ ((m + 1)...N)A ∈ ℂ)
122	108, 112, 113, 121	syl3anc 856	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ ((m + 1)...N)A = ([(m + 1) / k]A + Σk ∈ (((m + 1) + 1)...N)A))
123	122	eqcomd 1472	. . . . . . . . . . . . . . . 16 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ([(m + 1) / k]A + Σk ∈ (((m + 1) + 1)...N)A) = Σk ∈ ((m + 1)...N)A)
124		subaddt 5347	. . . . . . . . . . . . . . . . 17 ⊢ ((Σk ∈ ((m + 1)...N)A ∈ ℂ ⋀ [(m + 1) / k]A ∈ ℂ ⋀ Σk ∈ (((m + 1) + 1)...N)A ∈ ℂ) → ((Σk ∈ ((m + 1)...N)A − [(m + 1) / k]A) = Σk ∈ (((m + 1) + 1)...N)A ↔ ([(m + 1) / k]A + Σk ∈ (((m + 1) + 1)...N)A) = Σk ∈ ((m + 1)...N)A))
125		fsumclt 6953	. . . . . . . . . . . . . . . . . . 19 ⊢ ((N ∈ (ℤ≥ ‘(m + 1)) ⋀ ∀k ∈ ((m + 1)...N)A ∈ ℂ) → Σk ∈ ((m + 1)...N)A ∈ ℂ)
126	125, 99	sylan 448	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ ((m + 1)...N)A ∈ ℂ) → Σk ∈ ((m + 1)...N)A ∈ ℂ)
127	121, 126	syldan 467	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ ((m + 1)...N)A ∈ ℂ)
128		ra4csbela 2032	. . . . . . . . . . . . . . . . . 18 ⊢ (((m + 1) ∈ (M...N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → [(m + 1) / k]A ∈ ℂ)
129		eluzfzt 6409	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ (ℤ≥ ‘(m + 1))) → (m + 1) ∈ (M...N))
130	115	ad2antrr 404	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (m + 1) ∈ (ℤ≥ ‘M))
131	129, 130, 99	sylanc 471	. . . . . . . . . . . . . . . . . 18 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (m + 1) ∈ (M...N))
132	128, 131	sylan 448	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → [(m + 1) / k]A ∈ ℂ)
133		fzss1t 6435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((m + 1) + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (((m + 1) + 1)...N) ⊆ (M...N))
134		peano2uz 6379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((m + 1) ∈ (ℤ≥ ‘M) → ((m + 1) + 1) ∈ (ℤ≥ ‘M))
135	133, 134	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (((m + 1) + 1)...N) ⊆ (M...N))
136	135	sseld 2057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (k ∈ (((m + 1) + 1)...N) → k ∈ (M...N)))
137	136	imim1d 28	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((k ∈ (M...N) → A ∈ ℂ) → (k ∈ (((m + 1) + 1)...N) → A ∈ ℂ)))
138	137	r19.20dv2 1703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (∀k ∈ (M...N)A ∈ ℂ → ∀k ∈ (((m + 1) + 1)...N)A ∈ ℂ))
139	138	imp 350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ (((m + 1) + 1)...N)A ∈ ℂ)
140	139	adantlr 393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ((m + 1) + 1) ≤ N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → ∀k ∈ (((m + 1) + 1)...N)A ∈ ℂ)
141		fsumclt 6953	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((N ∈ (ℤ≥ ‘((m + 1) + 1)) ⋀ ∀k ∈ (((m + 1) + 1)...N)A ∈ ℂ) → Σk ∈ (((m + 1) + 1)...N)A ∈ ℂ)
142		eluzt 6358	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((m + 1) + 1) ∈ ℤ ⋀ N ∈ ℤ) → (N ∈ (ℤ≥ ‘((m + 1) + 1)) ↔ ((m + 1) + 1) ≤ N))
143		eluzelz 6355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((m + 1) ∈ (ℤ≥ ‘M) → (m + 1) ∈ ℤ)
144	143	peano2zd 6114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((m + 1) ∈ (ℤ≥ ‘M) → ((m + 1) + 1) ∈ ℤ)
145	142, 144	sylan 448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → (N ∈ (ℤ≥ ‘((m + 1) + 1)) ↔ ((m + 1) + 1) ≤ N))
146	145	biimpar 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ((m + 1) + 1) ≤ N) → N ∈ (ℤ≥ ‘((m + 1) + 1)))
147	141, 146	sylan 448	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ((m + 1) + 1) ≤ N) ⋀ ∀k ∈ (((m + 1) + 1)...N)A ∈ ℂ) → Σk ∈ (((m + 1) + 1)...N)A ∈ ℂ)
148	140, 147	syldan 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ((m + 1) + 1) ≤ N) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (((m + 1) + 1)...N)A ∈ ℂ)
149		pm3.26 319	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → ((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ))
150		zltp1let 6128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((m + 1) ∈ ℤ ⋀ N ∈ ℤ) → ((m + 1) < N ↔ ((m + 1) + 1) ≤ N))
151	150, 143	sylan 448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) → ((m + 1) < N ↔ ((m + 1) + 1) ≤ N))
152	151	biimpa 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → ((m + 1) + 1) ≤ N)
153	149, 152	jca 288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (((m + 1) ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ ((m + 1) + 1) ≤ N))
154	153, 115	sylanl1 460	. . . . . . . . . . . . . . . . . 18 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ N ∈ ℤ) ⋀ (m + 1) < N) → (((