fsumshft - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem fsumshft 6984

Description: Index shift of a finite sum.

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

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

**Proof of Theorem fsumshft**
Step	Hyp	Ref	Expression
1		0z 6103	. . . 4 ⊢ 0 ∈ ℤ
2		fsumrev 6982	. . . 4 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ 0 ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σm ∈ ((0 − N)...(0 − M))[(0 − m) / j]A)
3	1, 2	mp3an2 903	. . 3 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σm ∈ ((0 − N)...(0 − M))[(0 − m) / j]A)
4	3	3adant2 797	. 2 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σm ∈ ((0 − N)...(0 − M))[(0 − m) / j]A)
5		fsumrev 6982	. . 3 ⊢ (((0 − M) ∈ (ℤ_≥ ‘(0 − N)) ⋀ K ∈ ℤ ⋀ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ) → Σm ∈ ((0 − N)...(0 − M))[(0 − m) / j]A = Σk ∈ ((K − (0 − M))...(K − (0 − N)))[(K − k) / m][(0 − m) / j]A)
6		uznegit 6374	. . . . 5 ⊢ (N ∈ (ℤ_≥ ‘M) → -M ∈ (ℤ_≥ ‘-N))
7		df-neg 5341	. . . . . 6 ⊢ -M = (0 − M)
8		df-neg 5341	. . . . . . 7 ⊢ -N = (0 − N)
9	8	fveq2i 3722	. . . . . 6 ⊢ (ℤ_≥ ‘-N) = (ℤ_≥ ‘(0 − N))
10	7, 9	eleq12i 1537	. . . . 5 ⊢ (-M ∈ (ℤ_≥ ‘-N) ↔ (0 − M) ∈ (ℤ_≥ ‘(0 − N)))
11	6, 10	sylib 198	. . . 4 ⊢ (N ∈ (ℤ_≥ ‘M) → (0 − M) ∈ (ℤ_≥ ‘(0 − N)))
12	11	3ad2ant1 799	. . 3 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → (0 − M) ∈ (ℤ_≥ ‘(0 − N)))
13		3simp2 788	. . 3 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → K ∈ ℤ)
14		fzrevralt 6464	. . . . . . . 8 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ ⋀ 0 ∈ ℤ) → (∀j ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ))
15	1, 14	mp3an3 904	. . . . . . 7 ⊢ ((M ∈ ℤ ⋀ N ∈ ℤ) → (∀j ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ))
16		eluzel2 6369	. . . . . . 7 ⊢ (N ∈ (ℤ_≥ ‘M) → M ∈ ℤ)
17		eluzelz 6368	. . . . . . 7 ⊢ (N ∈ (ℤ_≥ ‘M) → N ∈ ℤ)
18	15, 16, 17	sylanc 471	. . . . . 6 ⊢ (N ∈ (ℤ_≥ ‘M) → (∀j ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ))
19		oprex 3978	. . . . . . . 8 ⊢ (0 − m) ∈ V
20		sbcel1g 2010	. . . . . . . 8 ⊢ ((0 − m) ∈ V → ([(0 − m) / j]A ∈ ℂ ↔ [(0 − m) / j]A ∈ ℂ))
21	19, 20	ax-mp 7	. . . . . . 7 ⊢ ([(0 − m) / j]A ∈ ℂ ↔ [(0 − m) / j]A ∈ ℂ)
22	21	ralbii 1665	. . . . . 6 ⊢ (∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ ↔ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ)
23	18, 22	syl6bb 535	. . . . 5 ⊢ (N ∈ (ℤ_≥ ‘M) → (∀j ∈ (M...N)A ∈ ℂ ↔ ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ))
24	23	biimpa 416	. . . 4 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ ∀j ∈ (M...N)A ∈ ℂ) → ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ)
25	24	3adant2 797	. . 3 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → ∀m ∈ ((0 − N)...(0 − M))[(0 − m) / j]A ∈ ℂ)
26	5, 12, 13, 25	syl3anc 857	. 2 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σm ∈ ((0 − N)...(0 − M))[(0 − m) / j]A = Σk ∈ ((K − (0 − M))...(K − (0 − N)))[(K − k) / m][(0 − m) / j]A)
27		subnegt 5377	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ M ∈ ℂ) → (K − -M) = (K + M))
28		axaddcom 5258	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ M ∈ ℂ) → (K + M) = (M + K))
29	27, 28	eqtrd 1505	. . . . . . . . 9 ⊢ ((K ∈ ℂ ⋀ M ∈ ℂ) → (K − -M) = (M + K))
30	7	opreq2i 3967	. . . . . . . . 9 ⊢ (K − -M) = (K − (0 − M))
31	29, 30	syl5eqr 1519	. . . . . . . 8 ⊢ ((K ∈ ℂ ⋀ M ∈ ℂ) → (K − (0 − M)) = (M + K))
32	31	adantrr 395	. . . . . . 7 ⊢ ((K ∈ ℂ ⋀ (M ∈ ℂ ⋀ N ∈ ℂ)) → (K − (0 − M)) = (M + K))
33		subnegt 5377	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ N ∈ ℂ) → (K − -N) = (K + N))
34		axaddcom 5258	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ N ∈ ℂ) → (K + N) = (N + K))
35	33, 34	eqtrd 1505	. . . . . . . . 9 ⊢ ((K ∈ ℂ ⋀ N ∈ ℂ) → (K − -N) = (N + K))
36	8	opreq2i 3967	. . . . . . . . 9 ⊢ (K − -N) = (K − (0 − N))
37	35, 36	syl5eqr 1519	. . . . . . . 8 ⊢ ((K ∈ ℂ ⋀ N ∈ ℂ) → (K − (0 − N)) = (N + K))
38	37	adantrl 394	. . . . . . 7 ⊢ ((K ∈ ℂ ⋀ (M ∈ ℂ ⋀ N ∈ ℂ)) → (K − (0 − N)) = (N + K))
39	32, 38	opreq12d 3973	. . . . . 6 ⊢ ((K ∈ ℂ ⋀ (M ∈ ℂ ⋀ N ∈ ℂ)) → ((K − (0 − M))...(K − (0 − N))) = ((M + K)...(N + K)))
40		zcnt 6097	. . . . . 6 ⊢ (K ∈ ℤ → K ∈ ℂ)
41		zcnt 6097	. . . . . . . 8 ⊢ (M ∈ ℤ → M ∈ ℂ)
42	16, 41	syl 10	. . . . . . 7 ⊢ (N ∈ (ℤ_≥ ‘M) → M ∈ ℂ)
43		zcnt 6097	. . . . . . . 8 ⊢ (N ∈ ℤ → N ∈ ℂ)
44	17, 43	syl 10	. . . . . . 7 ⊢ (N ∈ (ℤ_≥ ‘M) → N ∈ ℂ)
45	42, 44	jca 288	. . . . . 6 ⊢ (N ∈ (ℤ_≥ ‘M) → (M ∈ ℂ ⋀ N ∈ ℂ))
46	39, 40, 45	syl2an 454	. . . . 5 ⊢ ((K ∈ ℤ ⋀ N ∈ (ℤ_≥ ‘M)) → ((K − (0 − M))...(K − (0 − N))) = ((M + K)...(N + K)))
47	46	ancoms 436	. . . 4 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ) → ((K − (0 − M))...(K − (0 − N))) = ((M + K)...(N + K)))
48		negsubdi2t 5441	. . . . . . . . . 10 ⊢ ((K ∈ ℂ ⋀ k ∈ ℂ) → -(K − k) = (k − K))
49		zcnt 6097	. . . . . . . . . 10 ⊢ (k ∈ ℤ → k ∈ ℂ)
50	48, 40, 49	syl2an 454	. . . . . . . . 9 ⊢ ((K ∈ ℤ ⋀ k ∈ ℤ) → -(K − k) = (k − K))
51		df-neg 5341	. . . . . . . . 9 ⊢ -(K − k) = (0 − (K − k))
52	50, 51	syl5eqr 1519	. . . . . . . 8 ⊢ ((K ∈ ℤ ⋀ k ∈ ℤ) → (0 − (K − k)) = (k − K))
53	52	csbeq1d 2001	. . . . . . 7 ⊢ ((K ∈ ℤ ⋀ k ∈ ℤ) → [(0 − (K − k)) / j]A = [(k − K) / j]A)
54		oprex 3978	. . . . . . . 8 ⊢ (K − k) ∈ V
55	19	ax-gen 962	. . . . . . . 8 ⊢ ∀m(0 − m) ∈ V
56		opreq2 3964	. . . . . . . . 9 ⊢ (m = (K − k) → (0 − m) = (0 − (K − k)))
57	56	csbco3g 2037	. . . . . . . 8 ⊢ (((K − k) ∈ V ⋀ ∀m(0 − m) ∈ V) → [(K − k) / m][(0 − m) / j]A = [(0 − (K − k)) / j]A)
58	54, 55, 57	mp2an 696	. . . . . . 7 ⊢ [(K − k) / m][(0 − m) / j]A = [(0 − (K − k)) / j]A
59	53, 58	syl5eq 1517	. . . . . 6 ⊢ ((K ∈ ℤ ⋀ k ∈ ℤ) → [(K − k) / m][(0 − m) / j]A = [(k − K) / j]A)
60		elfzelz 6427	. . . . . 6 ⊢ (k ∈ ((K − (0 − M))...(K − (0 − N))) → k ∈ ℤ)
61	59, 60	sylan2 451	. . . . 5 ⊢ ((K ∈ ℤ ⋀ k ∈ ((K − (0 − M))...(K − (0 − N)))) → [(K − k) / m][(0 − m) / j]A = [(k − K) / j]A)
62	61	adantll 392	. . . 4 ⊢ (((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ) ⋀ k ∈ ((K − (0 − M))...(K − (0 − N)))) → [(K − k) / m][(0 − m) / j]A = [(k − K) / j]A)
63	47, 62	sumeq12dv 6948	. . 3 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ) → Σk ∈ ((K − (0 − M))...(K − (0 − N)))[(K − k) / m][(0 − m) / j]A = Σk ∈ ((M + K)...(N + K))[(k − K) / j]A)
64	63	3adant3 798	. 2 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σk ∈ ((K − (0 − M))...(K − (0 − N)))[(K − k) / m][(0 − m) / j]A = Σk ∈ ((M + K)...(N + K))[(k − K) / j]A)
65	4, 26, 64	3eqtrd 1509	1 ⊢ ((N ∈ (ℤ_≥ ‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk ∈ ((M + K)...(N + K))[(k − K) / j]A)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ⋀ w3a 774 ∀wal 953 = wceq 955 ∈ wcel 957 [wsbc 1169 ∀wral 1643 Vcvv 1808 [csb 1998 ‘cfv 3178 (class class class)co 3958 ℂcc 5215 0cc0 5217 + caddc 5220 − cmin 5275 -cneg 5276 ℤcz 5281 ℤ_≥cuz 6362 ...cfz 6412 Σcsu 6932

This theorem is referenced by: fsumshftm 6985 binomlem2 7020 iserzshft2 7060 fnsmntlem 7177

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-9 964 ax-10 965 ax-11 966 ax-12 967 ax-13 968 ax-14 969 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1209 ax-11o 1217 ax-ext 1458 ax-rep 2689 ax-sep 2699 ax-nul 2706 ax-pow 2738 ax-pr 2775 ax-un 2862 ax-inf2 4608

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 980 df-sb 1171 df-eu 1381 df-mo 1382 df-clab 1463 df-cleq 1468 df-clel 1471 df-ne 1585 df-nel 1586 df-ral 1647 df-rex 1648 df-reu 1649 df-rab 1650 df-v 1809 df-sbc 1939 df-csb 1999 df-dif 2046 df-un 2047 df-in 2048 df-ss 2050 df-pss 2052 df-nul 2278 df-if 2359 df-pw 2399 df-sn 2409 df-pr 2410 df-tp 2412 df-op 2413 df-uni 2500 df-int 2530 df-iun 2564 df-br 2616 df-opab 2663 df-tr 2677 df-eprel 2828 df-id 2831 df-po 2836 df-so 2846 df-fr 2913 df-we 2930 df-ord 2947 df-on 2948 df-lim 2949 df-suc 2950 df-om 3128 df-xp 3180 df-rel 3181 df-cnv 3182 df-co 3183 df-dm 3184 df-rn 3185 df-res 3186 df-ima 3187 df-fun 3188 df-fn 3189 df-f 3190 df-f1 3191 df-fo 3192 df-f1o 3193 df-fv 3194 df-rdg 3927 df-opr 3960 df-oprab 3961 df-1st 4072 df-2nd 4073 df-1o 4126 df-oadd 4128 df-omul 4129 df-er 4254 df-ec 4256 df-qs 4259 df-en 4360 df-dom 4361 df-sdom 4362 df-ni 4983 df-pli 4984 df-mi 4985 df-lti 4986 df-plpq 5018 df-mpq 5019 df-enq 5020 df-nq 5021 df-plq 5022 df-mq 5023 df-rq 5024 df-ltq 5025 df-1q 5026 df-np 5069 df-1p 5070 df-plp 5071 df-mp 5072 df-ltp 5073 df-plpr 5147 df-mpr 5148 df-enr 5149 df-nr 5150 df-plr 5151 df-mr 5152 df-ltr 5153 df-0r 5154 df-1r 5155 df-m1r 5156 df-c 5223 df-0 5224 df-1 5225 df-i 5226 df-r 5227 df-plus 5228 df-mul 5229 df-lt 5230 df-sub 5339 df-neg 5341 df-pnf 5470 df-mnf 5471 df-xr 5472 df-ltxr 5473 df-le 5474 df-n 5883 df-n0 6057 df-z 6093 df-seq1 6258 df-shft 6291 df-uz 6363 df-fz 6413 df-seqz 6478 df-sum 6933