fsumrev - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem fsumrev 6982

Description: Reversal of a finite sum. Warning: The HTML proof page is 0.6 MB in size.

**Assertion**
Ref	Expression
fsumrev	⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk ∈ ((K − N)...(K − M))[(K − k) / j]A)

Distinct variable groups: A,k j,k,K j,M,k j,N,k

**Proof of Theorem fsumrev**
Step	Hyp	Ref	Expression
1		nncant 5452	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ M ∈ ℂ) → (K − (K − M)) = M)
2		zcnt 6097	. . . . . . . . . 10 ⊢ (K ∈ ℤ → K ∈ ℂ)
3		zcnt 6097	. . . . . . . . . 10 ⊢ (M ∈ ℤ → M ∈ ℂ)
4	1, 2, 3	syl2an 454	. . . . . . . . 9 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → (K − (K − M)) = M)
5	4	csbeq1d 2001	. . . . . . . 8 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → [(K − (K − M)) / j]A = [M / j]A)
6	5	adantr 389	. . . . . . 7 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀j ∈ (M...M)A ∈ ℂ) → [(K − (K − M)) / j]A = [M / j]A)
7		fzrevralt 6464	. . . . . . . . . . 11 ⊢ ((M ∈ ℤ ⋀ M ∈ ℤ ⋀ K ∈ ℤ) → (∀j ∈ (M...M)A ∈ ℂ ↔ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ))
8		pm3.27 323	. . . . . . . . . . 11 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → M ∈ ℤ)
9		pm3.26 319	. . . . . . . . . . 11 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → K ∈ ℤ)
10	7, 8, 8, 9	syl3anc 857	. . . . . . . . . 10 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → (∀j ∈ (M...M)A ∈ ℂ ↔ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ))
11		oprex 3978	. . . . . . . . . . . 12 ⊢ (K − k) ∈ V
12		sbcel1g 2010	. . . . . . . . . . . 12 ⊢ ((K − k) ∈ V → ([(K − k) / j]A ∈ ℂ ↔ [(K − k) / j]A ∈ ℂ))
13	11, 12	ax-mp 7	. . . . . . . . . . 11 ⊢ ([(K − k) / j]A ∈ ℂ ↔ [(K − k) / j]A ∈ ℂ)
14	13	ralbii 1665	. . . . . . . . . 10 ⊢ (∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ ↔ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ)
15	10, 14	syl6bb 535	. . . . . . . . 9 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → (∀j ∈ (M...M)A ∈ ℂ ↔ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ))
16	15	biimpa 416	. . . . . . . 8 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀j ∈ (M...M)A ∈ ℂ) → ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ)
17		fsum1s 6962	. . . . . . . . . 10 ⊢ (((K − M) ∈ ℤ ⋀ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ) → Σk ∈ ((K − M)...(K − M))[(K − k) / j]A = [(K − M) / k][(K − k) / j]A)
18		oprex 3978	. . . . . . . . . . 11 ⊢ (K − M) ∈ V
19	11	ax-gen 962	. . . . . . . . . . 11 ⊢ ∀k(K − k) ∈ V
20		opreq2 3964	. . . . . . . . . . . 12 ⊢ (k = (K − M) → (K − k) = (K − (K − M)))
21	20	csbco3g 2037	. . . . . . . . . . 11 ⊢ (((K − M) ∈ V ⋀ ∀k(K − k) ∈ V) → [(K − M) / k][(K − k) / j]A = [(K − (K − M)) / j]A)
22	18, 19, 21	mp2an 696	. . . . . . . . . 10 ⊢ [(K − M) / k][(K − k) / j]A = [(K − (K − M)) / j]A
23	17, 22	syl6eq 1521	. . . . . . . . 9 ⊢ (((K − M) ∈ ℤ ⋀ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ) → Σk ∈ ((K − M)...(K − M))[(K − k) / j]A = [(K − (K − M)) / j]A)
24		zsubclt 6125	. . . . . . . . 9 ⊢ ((K ∈ ℤ ⋀ M ∈ ℤ) → (K − M) ∈ ℤ)
25	23, 24	sylan 448	. . . . . . . 8 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀k ∈ ((K − M)...(K − M))[(K − k) / j]A ∈ ℂ) → Σk ∈ ((K − M)...(K − M))[(K − k) / j]A = [(K − (K − M)) / j]A)
26	16, 25	syldan 467	. . . . . . 7 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σk ∈ ((K − M)...(K − M))[(K − k) / j]A = [(K − (K − M)) / j]A)
27		fsum1s 6962	. . . . . . . 8 ⊢ ((M ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σj ∈ (M...M)A = [M / j]A)
28	27	adantll 392	. . . . . . 7 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σj ∈ (M...M)A = [M / j]A)
29	6, 26, 28	3eqtr4rd 1516	. . . . . 6 ⊢ (((K ∈ ℤ ⋀ M ∈ ℤ) ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A)
30	29	anasss 440	. . . . 5 ⊢ ((K ∈ ℤ ⋀ (M ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ)) → Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A)
31	30	an1s 486	. . . 4 ⊢ ((M ∈ ℤ ⋀ (K ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ)) → Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A)
32	31	ex 373	. . 3 ⊢ (M ∈ ℤ → ((K ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A))
33		fzssp1t 6451	. . . . . . . . . 10 ⊢ ((M ∈ ℤ ⋀ n ∈ ℤ) → (M...n) ⊆ (M...(n + 1)))
34		eluzel2 6369	. . . . . . . . . 10 ⊢ (n ∈ (ℤ_≥ ‘M) → M ∈ ℤ)
35		eluzelz 6368	. . . . . . . . . 10 ⊢ (n ∈ (ℤ_≥ ‘M) → n ∈ ℤ)
36	33, 34, 35	sylanc 471	. . . . . . . . 9 ⊢ (n ∈ (ℤ_≥ ‘M) → (M...n) ⊆ (M...(n + 1)))
37	36	sseld 2064	. . . . . . . 8 ⊢ (n ∈ (ℤ_≥ ‘M) → (j ∈ (M...n) → j ∈ (M...(n + 1))))
38	37	imim1d 28	. . . . . . 7 ⊢ (n ∈ (ℤ_≥ ‘M) → ((j ∈ (M...(n + 1)) → A ∈ ℂ) → (j ∈ (M...n) → A ∈ ℂ)))
39	38	r19.20dv2 1709	. . . . . 6 ⊢ (n ∈ (ℤ_≥ ‘M) → (∀j ∈ (M...(n + 1))A ∈ ℂ → ∀j ∈ (M...n)A ∈ ℂ))
40	39	anim2d 560	. . . . 5 ⊢ (n ∈ (ℤ_≥ ‘M) → ((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → (K ∈ ℤ ⋀ ∀j ∈ (M...n)A ∈ ℂ)))
41	40	imim1d 28	. . . 4 ⊢ (n ∈ (ℤ_≥ ‘M) → (((K ∈ ℤ ⋀ ∀j ∈ (M...n)A ∈ ℂ) → Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → ((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A)))
42		nncant 5452	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℂ ⋀ (n + 1) ∈ ℂ) → (K − (K − (n + 1))) = (n + 1))
43		zcnt 6097	. . . . . . . . . . . . . . 15 ⊢ (n ∈ ℤ → n ∈ ℂ)
44		peano2cn 5327	. . . . . . . . . . . . . . 15 ⊢ (n ∈ ℂ → (n + 1) ∈ ℂ)
45	35, 43, 44	3syl 20	. . . . . . . . . . . . . 14 ⊢ (n ∈ (ℤ_≥ ‘M) → (n + 1) ∈ ℂ)
46	42, 2, 45	syl2an 454	. . . . . . . . . . . . 13 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − (K − (n + 1))) = (n + 1))
47	46	csbeq1d 2001	. . . . . . . . . . . 12 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → [(K − (K − (n + 1))) / j]A = [(n + 1) / j]A)
48		oprex 3978	. . . . . . . . . . . . 13 ⊢ (K − (n + 1)) ∈ V
49		opreq2 3964	. . . . . . . . . . . . . 14 ⊢ (k = (K − (n + 1)) → (K − k) = (K − (K − (n + 1))))
50	49	csbco3g 2037	. . . . . . . . . . . . 13 ⊢ (((K − (n + 1)) ∈ V ⋀ ∀k(K − k) ∈ V) → [(K − (n + 1)) / k][(K − k) / j]A = [(K − (K − (n + 1))) / j]A)
51	48, 19, 50	mp2an 696	. . . . . . . . . . . 12 ⊢ [(K − (n + 1)) / k][(K − k) / j]A = [(K − (K − (n + 1))) / j]A
52	47, 51	syl5req 1518	. . . . . . . . . . 11 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → [(n + 1) / j]A = [(K − (n + 1)) / k][(K − k) / j]A)
53	52	adantr 389	. . . . . . . . . 10 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → [(n + 1) / j]A = [(K − (n + 1)) / k][(K − k) / j]A)
54		id 59	. . . . . . . . . 10 ⊢ (Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A → Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A)
55	53, 54	opreqan12d 3974	. . . . . . . . 9 ⊢ ((((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) ⋀ Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → ([(n + 1) / j]A + Σj ∈ (M...n)A) = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ ((K − n)...(K − M))[(K − k) / j]A))
56		fsump1s 6966	. . . . . . . . . . . 12 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...(n + 1))A = (Σj ∈ (M...n)A + [(n + 1) / j]A))
57		axaddcom 5258	. . . . . . . . . . . . 13 ⊢ ((Σj ∈ (M...n)A ∈ ℂ ⋀ [(n + 1) / j]A ∈ ℂ) → (Σj ∈ (M...n)A + [(n + 1) / j]A) = ([(n + 1) / j]A + Σj ∈ (M...n)A))
58	39	imp 350	. . . . . . . . . . . . . 14 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → ∀j ∈ (M...n)A ∈ ℂ)
59		fsumclt 6968	. . . . . . . . . . . . . 14 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...n)A ∈ ℂ) → Σj ∈ (M...n)A ∈ ℂ)
60	58, 59	syldan 467	. . . . . . . . . . . . 13 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...n)A ∈ ℂ)
61		ra4csbela 2039	. . . . . . . . . . . . . 14 ⊢ (((n + 1) ∈ (M...(n + 1)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → [(n + 1) / j]A ∈ ℂ)
62		peano2uz 6392	. . . . . . . . . . . . . . 15 ⊢ (n ∈ (ℤ_≥ ‘M) → (n + 1) ∈ (ℤ_≥ ‘M))
63		eluzfz2t 6434	. . . . . . . . . . . . . . 15 ⊢ ((n + 1) ∈ (ℤ_≥ ‘M) → (n + 1) ∈ (M...(n + 1)))
64	62, 63	syl 10	. . . . . . . . . . . . . 14 ⊢ (n ∈ (ℤ_≥ ‘M) → (n + 1) ∈ (M...(n + 1)))
65	61, 64	sylan 448	. . . . . . . . . . . . 13 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → [(n + 1) / j]A ∈ ℂ)
66	57, 60, 65	sylanc 471	. . . . . . . . . . . 12 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → (Σj ∈ (M...n)A + [(n + 1) / j]A) = ([(n + 1) / j]A + Σj ∈ (M...n)A))
67	56, 66	eqtrd 1505	. . . . . . . . . . 11 ⊢ ((n ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...(n + 1))A = ([(n + 1) / j]A + Σj ∈ (M...n)A))
68	67	adantll 392	. . . . . . . . . 10 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...(n + 1))A = ([(n + 1) / j]A + Σj ∈ (M...n)A))
69	68	adantr 389	. . . . . . . . 9 ⊢ ((((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) ⋀ Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → Σj ∈ (M...(n + 1))A = ([(n + 1) / j]A + Σj ∈ (M...n)A))
70		fsum1ps 6971	. . . . . . . . . . . 12 ⊢ (((K − M) ∈ (ℤ_≥ ‘(K − (n + 1))) ⋀ (K − (n + 1)) < (K − M) ⋀ ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ) → Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ (((K − (n + 1)) + 1)...(K − M))[(K − k) / j]A))
71		letrp1t 5782	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℝ ⋀ n ∈ ℝ ⋀ M ≤ n) → M ≤ (n + 1))
72		zret 6096	. . . . . . . . . . . . . . . . . 18 ⊢ (M ∈ ℤ → M ∈ ℝ)
73	34, 72	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ_≥ ‘M) → M ∈ ℝ)
74		zret 6096	. . . . . . . . . . . . . . . . . 18 ⊢ (n ∈ ℤ → n ∈ ℝ)
75	35, 74	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ_≥ ‘M) → n ∈ ℝ)
76		eluzle 6370	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ_≥ ‘M) → M ≤ n)
77	71, 73, 75, 76	syl3anc 857	. . . . . . . . . . . . . . . 16 ⊢ (n ∈ (ℤ_≥ ‘M) → M ≤ (n + 1))
78	77	adantl 388	. . . . . . . . . . . . . . 15 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → M ≤ (n + 1))
79		lesub2t 5644	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℝ ⋀ (n + 1) ∈ ℝ ⋀ K ∈ ℝ) → (M ≤ (n + 1) ↔ (K − (n + 1)) ≤ (K − M)))
80		zret 6096	. . . . . . . . . . . . . . . . 17 ⊢ ((n + 1) ∈ ℤ → (n + 1) ∈ ℝ)
81		zret 6096	. . . . . . . . . . . . . . . . 17 ⊢ (K ∈ ℤ → K ∈ ℝ)
82	79, 72, 80, 81	syl3an 867	. . . . . . . . . . . . . . . 16 ⊢ ((M ∈ ℤ ⋀ (n + 1) ∈ ℤ ⋀ K ∈ ℤ) → (M ≤ (n + 1) ↔ (K − (n + 1)) ≤ (K − M)))
83	34	adantl 388	. . . . . . . . . . . . . . . 16 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → M ∈ ℤ)
84	35	peano2zd 6124	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ (ℤ_≥ ‘M) → (n + 1) ∈ ℤ)
85	84	adantl 388	. . . . . . . . . . . . . . . 16 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (n + 1) ∈ ℤ)
86		pm3.26 319	. . . . . . . . . . . . . . . 16 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → K ∈ ℤ)
87	82, 83, 85, 86	syl3anc 857	. . . . . . . . . . . . . . 15 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (M ≤ (n + 1) ↔ (K − (n + 1)) ≤ (K − M)))
88	78, 87	mpbid 195	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − (n + 1)) ≤ (K − M))
89		eluzt 6371	. . . . . . . . . . . . . . 15 ⊢ (((K − (n + 1)) ∈ ℤ ⋀ (K − M) ∈ ℤ) → ((K − M) ∈ (ℤ_≥ ‘(K − (n + 1))) ↔ (K − (n + 1)) ≤ (K − M)))
90		zsubclt 6125	. . . . . . . . . . . . . . . 16 ⊢ ((K ∈ ℤ ⋀ (n + 1) ∈ ℤ) → (K − (n + 1)) ∈ ℤ)
91	90, 84	sylan2 451	. . . . . . . . . . . . . . 15 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − (n + 1)) ∈ ℤ)
92	24, 34	sylan2 451	. . . . . . . . . . . . . . 15 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − M) ∈ ℤ)
93	89, 91, 92	sylanc 471	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → ((K − M) ∈ (ℤ_≥ ‘(K − (n + 1))) ↔ (K − (n + 1)) ≤ (K − M)))
94	88, 93	mpbird 196	. . . . . . . . . . . . 13 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − M) ∈ (ℤ_≥ ‘(K − (n + 1))))
95	94	adantr 389	. . . . . . . . . . . 12 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → (K − M) ∈ (ℤ_≥ ‘(K − (n + 1))))
96		zleltp1t 6139	. . . . . . . . . . . . . . . . 17 ⊢ ((M ∈ ℤ ⋀ n ∈ ℤ) → (M ≤ n ↔ M < (n + 1)))
97	96, 34, 35	sylanc 471	. . . . . . . . . . . . . . . 16 ⊢ (n ∈ (ℤ_≥ ‘M) → (M ≤ n ↔ M < (n + 1)))
98	76, 97	mpbid 195	. . . . . . . . . . . . . . 15 ⊢ (n ∈ (ℤ_≥ ‘M) → M < (n + 1))
99	98	adantl 388	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → M < (n + 1))
100		ltsub2t 5646	. . . . . . . . . . . . . . . 16 ⊢ ((M ∈ ℝ ⋀ (n + 1) ∈ ℝ ⋀ K ∈ ℝ) → (M < (n + 1) ↔ (K − (n + 1)) < (K − M)))
101	100, 72, 80, 81	syl3an 867	. . . . . . . . . . . . . . 15 ⊢ ((M ∈ ℤ ⋀ (n + 1) ∈ ℤ ⋀ K ∈ ℤ) → (M < (n + 1) ↔ (K − (n + 1)) < (K − M)))
102	101, 83, 85, 86	syl3anc 857	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (M < (n + 1) ↔ (K − (n + 1)) < (K − M)))
103	99, 102	mpbid 195	. . . . . . . . . . . . 13 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (K − (n + 1)) < (K − M))
104	103	adantr 389	. . . . . . . . . . . 12 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → (K − (n + 1)) < (K − M))
105		fzrevralt 6464	. . . . . . . . . . . . . . 15 ⊢ ((M ∈ ℤ ⋀ (n + 1) ∈ ℤ ⋀ K ∈ ℤ) → (∀j ∈ (M...(n + 1))A ∈ ℂ ↔ ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ))
106	105, 83, 85, 86	syl3anc 857	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (∀j ∈ (M...(n + 1))A ∈ ℂ ↔ ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ))
107	13	ralbii 1665	. . . . . . . . . . . . . 14 ⊢ (∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ ↔ ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ)
108	106, 107	syl6bb 535	. . . . . . . . . . . . 13 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (∀j ∈ (M...(n + 1))A ∈ ℂ ↔ ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ))
109	108	biimpa 416	. . . . . . . . . . . 12 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → ∀k ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A ∈ ℂ)
110	70, 95, 104, 109	syl3anc 857	. . . . . . . . . . 11 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ (((K − (n + 1)) + 1)...(K − M))[(K − k) / j]A))
111		ax1cn 5252	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
112		nppcan2t 5453	. . . . . . . . . . . . . . . . 17 ⊢ ((K ∈ ℂ ⋀ n ∈ ℂ ⋀ 1 ∈ ℂ) → ((K − (n + 1)) + 1) = (K − n))
113	111, 112	mp3an3 904	. . . . . . . . . . . . . . . 16 ⊢ ((K ∈ ℂ ⋀ n ∈ ℂ) → ((K − (n + 1)) + 1) = (K − n))
114	35, 43	syl 10	. . . . . . . . . . . . . . . 16 ⊢ (n ∈ (ℤ_≥ ‘M) → n ∈ ℂ)
115	113, 2, 114	syl2an 454	. . . . . . . . . . . . . . 15 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → ((K − (n + 1)) + 1) = (K − n))
116	115	opreq1d 3970	. . . . . . . . . . . . . 14 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → (((K − (n + 1)) + 1)...(K − M)) = ((K − n)...(K − M)))
117	116	sumeq1d 6943	. . . . . . . . . . . . 13 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → Σk ∈ (((K − (n + 1)) + 1)...(K − M))[(K − k) / j]A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A)
118	117	opreq2d 3971	. . . . . . . . . . . 12 ⊢ ((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) → ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ (((K − (n + 1)) + 1)...(K − M))[(K − k) / j]A) = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ ((K − n)...(K − M))[(K − k) / j]A))
119	118	adantr 389	. . . . . . . . . . 11 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ (((K − (n + 1)) + 1)...(K − M))[(K − k) / j]A) = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ ((K − n)...(K − M))[(K − k) / j]A))
120	110, 119	eqtrd 1505	. . . . . . . . . 10 ⊢ (((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ ((K − n)...(K − M))[(K − k) / j]A))
121	120	adantr 389	. . . . . . . . 9 ⊢ ((((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) ⋀ Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A = ([(K − (n + 1)) / k][(K − k) / j]A + Σk ∈ ((K − n)...(K − M))[(K − k) / j]A))
122	55, 69, 121	3eqtr4d 1515	. . . . . . . 8 ⊢ ((((K ∈ ℤ ⋀ n ∈ (ℤ_≥ ‘M)) ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) ⋀ Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A)
123	122	exp41 382	. . . . . . 7 ⊢ (K ∈ ℤ → (n ∈ (ℤ_≥ ‘M) → (∀j ∈ (M...(n + 1))A ∈ ℂ → (Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A))))
124	123	com12 11	. . . . . 6 ⊢ (n ∈ (ℤ_≥ ‘M) → (K ∈ ℤ → (∀j ∈ (M...(n + 1))A ∈ ℂ → (Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A))))
125	124	imp3a 361	. . . . 5 ⊢ (n ∈ (ℤ_≥ ‘M) → ((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → (Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A)))
126	125	a2d 13	. . . 4 ⊢ (n ∈ (ℤ_≥ ‘M) → (((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → ((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A)))
127	41, 126	syld 27	. . 3 ⊢ (n ∈ (ℤ_≥ ‘M) → (((K ∈ ℤ ⋀ ∀j ∈ (M...n)A ∈ ℂ) → Σj ∈ (M...n)A = Σk ∈ ((K − n)...(K − M))[(K − k) / j]A) → ((K ∈ ℤ ⋀ ∀j ∈ (M...(n + 1))A ∈ ℂ) → Σj ∈ (M...(n + 1))A = Σk ∈ ((K − (n + 1))...(K − M))[(K − k) / j]A)))
128		opreq2 3964	. . . . . 6 ⊢ (m = M → (M...m) = (M...M))
129	128	raleq1d 1787	. . . . 5 ⊢ (m = M → (∀j ∈ (M...m)A ∈ ℂ ↔ ∀j ∈ (M...M)A ∈ ℂ))
130	129	anbi2d 615	. . . 4 ⊢ (m = M → ((K ∈ ℤ ⋀ ∀j ∈ (M...m)A ∈ ℂ) ↔ (K ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ)))
131	128	sumeq1d 6943	. . . . 5 ⊢ (m = M → Σj ∈ (M...m)A = Σj ∈ (M...M)A)
132		opreq2 3964	. . . . . . 7 ⊢ (m = M → (K − m) = (K − M))
133	132	opreq1d 3970	. . . . . 6 ⊢ (m = M → ((K − m)...(K − M)) = ((K − M)...(K − M)))
134	133	sumeq1d 6943	. . . . 5 ⊢ (m = M → Σk ∈ ((K − m)...(K − M))[(K − k) / j]A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A)
135	131, 134	eqeq12d 1487	. . . 4 ⊢ (m = M → (Σj ∈ (M...m)A = Σk ∈ ((K − m)...(K − M))[(K − k) / j]A ↔ Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A))
136	130, 135	imbi12d 625	. . 3 ⊢ (m = M → (((K ∈ ℤ ⋀ ∀j ∈ (M...m)A ∈ ℂ) → Σj ∈ (M...m)A = Σk ∈ ((K − m)...(K − M))[(K − k) / j]A) ↔ ((K ∈ ℤ ⋀ ∀j ∈ (M...M)A ∈ ℂ) → Σj ∈ (M...M)A = Σk ∈ ((K − M)...(K − M))[(K − k) / j]A)))
137		opreq2 3964	. . . . . 6 ⊢ (m = n → (M...m) = (M...n))
138	137	raleq1d 1787	. . . . 5 ⊢ (m = n → (∀j ∈ (M...m)A ∈ ℂ ↔ ∀j ∈ (M...n)A ∈ ℂ))
139	138	anbi2d 615	. . . 4 ⊢ (m = n → ((K ∈ ℤ ⋀ ∀j ∈ (M...m)A ∈ ℂ) ↔ (K</