Theorem fsummulc1 6971

Description: A finite sum multiplied by a constant.

Assertion

Ref	Expression
fsummulc1	⊢ ((N ∈ (ℤ≥ ‘M) ⋀ C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (C · Σk ∈ (M...N)A) = Σk ∈ (M...N)(C · A))

Distinct variable groups:   C,k   k,M   k,N

Proof of Theorem fsummulc1

Step	Hyp	Ref	Expression
1		csbopr2g 3974	. . . . . 6 ⊢ (M ∈ ℤ → [M / k](C · A) = (C · [M / k]A))
2	1	adantr 389	. . . . 5 ⊢ ((M ∈ ℤ ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)) → [M / k](C · A) = (C · [M / k]A))
3		fsum1s 6947	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(C · A) ∈ ℂ) → Σk ∈ (M...M)(C · A) = [M / k](C · A))
4		r19.28av 1747	. . . . . . 7 ⊢ ((C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → ∀k ∈ (M...M)(C ∈ ℂ ⋀ A ∈ ℂ))
5		axmulcl 5245	. . . . . . . 8 ⊢ ((C ∈ ℂ ⋀ A ∈ ℂ) → (C · A) ∈ ℂ)
6	5	r19.20si 1698	. . . . . . 7 ⊢ (∀k ∈ (M...M)(C ∈ ℂ ⋀ A ∈ ℂ) → ∀k ∈ (M...M)(C · A) ∈ ℂ)
7	4, 6	syl 10	. . . . . 6 ⊢ ((C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → ∀k ∈ (M...M)(C · A) ∈ ℂ)
8	3, 7	sylan2 451	. . . . 5 ⊢ ((M ∈ ℤ ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)) → Σk ∈ (M...M)(C · A) = [M / k](C · A))
9		fsum1s 6947	. . . . . . 7 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → Σk ∈ (M...M)A = [M / k]A)
10	9	adantrl 394	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)) → Σk ∈ (M...M)A = [M / k]A)
11	10	opreq2d 3961	. . . . 5 ⊢ ((M ∈ ℤ ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)) → (C · Σk ∈ (M...M)A) = (C · [M / k]A))
12	2, 8, 11	3eqtr4rd 1510	. . . 4 ⊢ ((M ∈ ℤ ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)) → (C · Σk ∈ (M...M)A) = Σk ∈ (M...M)(C · A))
13	12	ex 373	. . 3 ⊢ (M ∈ ℤ → ((C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → (C · Σk ∈ (M...M)A) = Σk ∈ (M...M)(C · A)))
14		fzssp1t 6438	. . . . . . . . . 10 ⊢ ((M ∈ ℤ ⋀ m ∈ ℤ) → (M...m) ⊆ (M...(m + 1)))
15		eluzel2 6356	. . . . . . . . . 10 ⊢ (m ∈ (ℤ≥ ‘M) → M ∈ ℤ)
16		eluzelz 6355	. . . . . . . . . 10 ⊢ (m ∈ (ℤ≥ ‘M) → m ∈ ℤ)
17	14, 15, 16	sylanc 471	. . . . . . . . 9 ⊢ (m ∈ (ℤ≥ ‘M) → (M...m) ⊆ (M...(m + 1)))
18	17	sseld 2057	. . . . . . . 8 ⊢ (m ∈ (ℤ≥ ‘M) → (k ∈ (M...m) → k ∈ (M...(m + 1))))
19	18	imim1d 28	. . . . . . 7 ⊢ (m ∈ (ℤ≥ ‘M) → ((k ∈ (M...(m + 1)) → A ∈ ℂ) → (k ∈ (M...m) → A ∈ ℂ)))
20	19	r19.20dv2 1703	. . . . . 6 ⊢ (m ∈ (ℤ≥ ‘M) → (∀k ∈ (M...(m + 1))A ∈ ℂ → ∀k ∈ (M...m)A ∈ ℂ))
21	20	anim2d 559	. . . . 5 ⊢ (m ∈ (ℤ≥ ‘M) → ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C ∈ ℂ ⋀ ∀k ∈ (M...m)A ∈ ℂ)))
22	21	imim1d 28	. . . 4 ⊢ (m ∈ (ℤ≥ ‘M) → (((C ∈ ℂ ⋀ ∀k ∈ (M...m)A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) → ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))))
23		axdistr 5251	. . . . . . . . 9 ⊢ ((C ∈ ℂ ⋀ Σk ∈ (M...m)A ∈ ℂ ⋀ [(m + 1) / k]A ∈ ℂ) → (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)) = ((C · Σk ∈ (M...m)A) + (C · [(m + 1) / k]A)))
24		simprl 414	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → C ∈ ℂ)
25	20	imp 350	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → ∀k ∈ (M...m)A ∈ ℂ)
26		fsumclt 6953	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...m)A ∈ ℂ) → Σk ∈ (M...m)A ∈ ℂ)
27	25, 26	syldan 467	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → Σk ∈ (M...m)A ∈ ℂ)
28	27	adantrl 394	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → Σk ∈ (M...m)A ∈ ℂ)
29		ra4csbela 2032	. . . . . . . . . . 11 ⊢ (((m + 1) ∈ (M...(m + 1)) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → [(m + 1) / k]A ∈ ℂ)
30		peano2uz 6379	. . . . . . . . . . . 12 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ (ℤ≥ ‘M))
31		eluzfz2t 6421	. . . . . . . . . . . 12 ⊢ ((m + 1) ∈ (ℤ≥ ‘M) → (m + 1) ∈ (M...(m + 1)))
32	30, 31	syl 10	. . . . . . . . . . 11 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ (M...(m + 1)))
33	29, 32	sylan 448	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → [(m + 1) / k]A ∈ ℂ)
34	33	adantrl 394	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → [(m + 1) / k]A ∈ ℂ)
35	23, 24, 28, 34	syl3anc 856	. . . . . . . 8 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)) = ((C · Σk ∈ (M...m)A) + (C · [(m + 1) / k]A)))
36	35	adantlr 393	. . . . . . 7 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)) = ((C · Σk ∈ (M...m)A) + (C · [(m + 1) / k]A)))
37		id 59	. . . . . . . . . 10 ⊢ (((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) → ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)))
38	37	imp 350	. . . . . . . . 9 ⊢ ((((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))
39		oprex 3968	. . . . . . . . . . . 12 ⊢ (m + 1) ∈ V
40		csbopr2g 3974	. . . . . . . . . . . 12 ⊢ ((m + 1) ∈ V → [(m + 1) / k](C · A) = (C · [(m + 1) / k]A))
41	39, 40	ax-mp 7	. . . . . . . . . . 11 ⊢ [(m + 1) / k](C · A) = (C · [(m + 1) / k]A)
42	41	eqcomi 1471	. . . . . . . . . 10 ⊢ (C · [(m + 1) / k]A) = [(m + 1) / k](C · A)
43	42	a1i 8	. . . . . . . . 9 ⊢ ((((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · [(m + 1) / k]A) = [(m + 1) / k](C · A))
44	38, 43	opreq12d 3963	. . . . . . . 8 ⊢ ((((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → ((C · Σk ∈ (M...m)A) + (C · [(m + 1) / k]A)) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
45	44	adantll 392	. . . . . . 7 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → ((C · Σk ∈ (M...m)A) + (C · [(m + 1) / k]A)) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
46	36, 45	eqtrd 1499	. . . . . 6 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
47		fsump1s 6951	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
48	47	adantrl 394	. . . . . . . 8 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
49	48	opreq2d 3961	. . . . . . 7 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · Σk ∈ (M...(m + 1))A) = (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)))
50	49	adantlr 393	. . . . . 6 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · Σk ∈ (M...(m + 1))A) = (C · (Σk ∈ (M...m)A + [(m + 1) / k]A)))
51		fsump1s 6951	. . . . . . . 8 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(C · A) ∈ ℂ) → Σk ∈ (M...(m + 1))(C · A) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
52		r19.28av 1747	. . . . . . . . 9 ⊢ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → ∀k ∈ (M...(m + 1))(C ∈ ℂ ⋀ A ∈ ℂ))
53	5	r19.20si 1698	. . . . . . . . 9 ⊢ (∀k ∈ (M...(m + 1))(C ∈ ℂ ⋀ A ∈ ℂ) → ∀k ∈ (M...(m + 1))(C · A) ∈ ℂ)
54	52, 53	syl 10	. . . . . . . 8 ⊢ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → ∀k ∈ (M...(m + 1))(C · A) ∈ ℂ)
55	51, 54	sylan2 451	. . . . . . 7 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → Σk ∈ (M...(m + 1))(C · A) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
56	55	adantlr 393	. . . . . 6 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → Σk ∈ (M...(m + 1))(C · A) = (Σk ∈ (M...m)(C · A) + [(m + 1) / k](C · A)))
57	46, 50, 56	3eqtr4d 1509	. . . . 5 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))) ⋀ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)) → (C · Σk ∈ (M...(m + 1))A) = Σk ∈ (M...(m + 1))(C · A))
58	57	exp31 376	. . . 4 ⊢ (m ∈ (ℤ≥ ‘M) → (((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) → ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...(m + 1))A) = Σk ∈ (M...(m + 1))(C · A))))
59	22, 58	syld 27	. . 3 ⊢ (m ∈ (ℤ≥ ‘M) → (((C ∈ ℂ ⋀ ∀k ∈ (M...m)A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)) → ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...(m + 1))A) = Σk ∈ (M...(m + 1))(C · A))))
60		opreq2 3954	. . . . . 6 ⊢ (j = M → (M...j) = (M...M))
61	60	raleq1d 1781	. . . . 5 ⊢ (j = M → (∀k ∈ (M...j)A ∈ ℂ ↔ ∀k ∈ (M...M)A ∈ ℂ))
62	61	anbi2d 614	. . . 4 ⊢ (j = M → ((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) ↔ (C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ)))
63	60	sumeq1d 6928	. . . . . 6 ⊢ (j = M → Σk ∈ (M...j)A = Σk ∈ (M...M)A)
64	63	opreq2d 3961	. . . . 5 ⊢ (j = M → (C · Σk ∈ (M...j)A) = (C · Σk ∈ (M...M)A))
65	60	sumeq1d 6928	. . . . 5 ⊢ (j = M → Σk ∈ (M...j)(C · A) = Σk ∈ (M...M)(C · A))
66	64, 65	eqeq12d 1481	. . . 4 ⊢ (j = M → ((C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A) ↔ (C · Σk ∈ (M...M)A) = Σk ∈ (M...M)(C · A)))
67	62, 66	imbi12d 624	. . 3 ⊢ (j = M → (((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) → (C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A)) ↔ ((C ∈ ℂ ⋀ ∀k ∈ (M...M)A ∈ ℂ) → (C · Σk ∈ (M...M)A) = Σk ∈ (M...M)(C · A))))
68		opreq2 3954	. . . . . 6 ⊢ (j = m → (M...j) = (M...m))
69	68	raleq1d 1781	. . . . 5 ⊢ (j = m → (∀k ∈ (M...j)A ∈ ℂ ↔ ∀k ∈ (M...m)A ∈ ℂ))
70	69	anbi2d 614	. . . 4 ⊢ (j = m → ((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) ↔ (C ∈ ℂ ⋀ ∀k ∈ (M...m)A ∈ ℂ)))
71	68	sumeq1d 6928	. . . . . 6 ⊢ (j = m → Σk ∈ (M...j)A = Σk ∈ (M...m)A)
72	71	opreq2d 3961	. . . . 5 ⊢ (j = m → (C · Σk ∈ (M...j)A) = (C · Σk ∈ (M...m)A))
73	68	sumeq1d 6928	. . . . 5 ⊢ (j = m → Σk ∈ (M...j)(C · A) = Σk ∈ (M...m)(C · A))
74	72, 73	eqeq12d 1481	. . . 4 ⊢ (j = m → ((C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A) ↔ (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A)))
75	70, 74	imbi12d 624	. . 3 ⊢ (j = m → (((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) → (C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A)) ↔ ((C ∈ ℂ ⋀ ∀k ∈ (M...m)A ∈ ℂ) → (C · Σk ∈ (M...m)A) = Σk ∈ (M...m)(C · A))))
76		opreq2 3954	. . . . . 6 ⊢ (j = (m + 1) → (M...j) = (M...(m + 1)))
77	76	raleq1d 1781	. . . . 5 ⊢ (j = (m + 1) → (∀k ∈ (M...j)A ∈ ℂ ↔ ∀k ∈ (M...(m + 1))A ∈ ℂ))
78	77	anbi2d 614	. . . 4 ⊢ (j = (m + 1) → ((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) ↔ (C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ)))
79	76	sumeq1d 6928	. . . . . 6 ⊢ (j = (m + 1) → Σk ∈ (M...j)A = Σk ∈ (M...(m + 1))A)
80	79	opreq2d 3961	. . . . 5 ⊢ (j = (m + 1) → (C · Σk ∈ (M...j)A) = (C · Σk ∈ (M...(m + 1))A))
81	76	sumeq1d 6928	. . . . 5 ⊢ (j = (m + 1) → Σk ∈ (M...j)(C · A) = Σk ∈ (M...(m + 1))(C · A))
82	80, 81	eqeq12d 1481	. . . 4 ⊢ (j = (m + 1) → ((C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A) ↔ (C · Σk ∈ (M...(m + 1))A) = Σk ∈ (M...(m + 1))(C · A)))
83	78, 82	imbi12d 624	. . 3 ⊢ (j = (m + 1) → (((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) → (C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A)) ↔ ((C ∈ ℂ ⋀ ∀k ∈ (M...(m + 1))A ∈ ℂ) → (C · Σk ∈ (M...(m + 1))A) = Σk ∈ (M...(m + 1))(C · A))))
84		opreq2 3954	. . . . . 6 ⊢ (j = N → (M...j) = (M...N))
85	84	raleq1d 1781	. . . . 5 ⊢ (j = N → (∀k ∈ (M...j)A ∈ ℂ ↔ ∀k ∈ (M...N)A ∈ ℂ))
86	85	anbi2d 614	. . . 4 ⊢ (j = N → ((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) ↔ (C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ)))
87	84	sumeq1d 6928	. . . . . 6 ⊢ (j = N → Σk ∈ (M...j)A = Σk ∈ (M...N)A)
88	87	opreq2d 3961	. . . . 5 ⊢ (j = N → (C · Σk ∈ (M...j)A) = (C · Σk ∈ (M...N)A))
89	84	sumeq1d 6928	. . . . 5 ⊢ (j = N → Σk ∈ (M...j)(C · A) = Σk ∈ (M...N)(C · A))
90	88, 89	eqeq12d 1481	. . . 4 ⊢ (j = N → ((C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A) ↔ (C · Σk ∈ (M...N)A) = Σk ∈ (M...N)(C · A)))
91	86, 90	imbi12d 624	. . 3 ⊢ (j = N → (((C ∈ ℂ ⋀ ∀k ∈ (M...j)A ∈ ℂ) → (C · Σk ∈ (M...j)A) = Σk ∈ (M...j)(C · A)) ↔ ((C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (C · Σk ∈ (M...N)A) = Σk ∈ (M...N)(C · A))))
92	13, 59, 67, 75, 83, 91	uzind4ALT 6383	. 2 ⊢ (N ∈ (ℤ≥ ‘M) → ((C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (C · Σk ∈ (M...N)A) = Σk ∈ (M...N)(C · A)))
93	92	3impib 829	1 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (C · Σk ∈ (M...N)A) = Σk ∈ (M...N)(C · A))

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 773   = wceq 953   ∈ wcel 955  ∀wral 1637  Vcvv 1802  [csb 1991   ⊆ wss 2037   ‘cfv 3172  (class class class)co 3948  ℂcc 5204  1c1 5207   + caddc 5209   · cmul 5211  ℤcz 5270  ℤ_≥cuz 6349  ...cfz 6399  Σcsu 6917

This theorem is referenced by:  fsummulc2 6972  fsum2mul 6975  serzmulc1 6995  fnsmnt 7161  fsum0diag3 7195  eirrlem2 7331

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-oadd 4119  df-omul 4120  df-er 4245  df-ec 4247  df-qs 4250  df-en 4351  df-dom 4352  df-sdom 4353  df-ni 4972  df-pli 4973  df-mi 4974  df-lti 4975  df-plpq 5007  df-mpq 5008  df-enq 5009  df-nq 5010  df-plq 5011  df-mq 5012  df-rq 5013  df-ltq 5014  df-1q 5015  df-np 5058  df-1p 5059  df-plp 5060  df-mp 5061  df-ltp 5062  df-plpr 5136  df-mpr 5137  df-enr 5138  df-nr 5139  df-plr 5140  df-mr 5141  df-ltr 5142  df-0r 5143  df-1r 5144  df-m1r 5145  df-c 5212  df-0 5213  df-1 5214  df-i 5215  df-r 5216  df-plus 5217  df-mul 5218  df-lt 5219  df-sub 5328  df-neg 5330  df-pnf 5459  df-mnf 5460  df-xr 5461  df-ltxr 5462  df-le 5463  df-n 5873  df-n0 6047  df-z 6083  df-seq1 6245  df-shft 6278  df-uz 6350  df-fz 6400  df-seqz 6465  df-sum 6918

Copyright terms: Public domain