Theorem fsumabs 6932

Description: Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values.

Assertion

Ref	Expression
fsumabs	|- ((N e. (ZZ>` M) /\ A.k e. (M...N)A e. CC) -> (abs` sum_k e. (M...N)A) <_ sum_k e. (M...N)(abs` A))

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumabs

Step	Hyp	Ref	Expression
1		opreq2 3908	. . . . 5 |- (j = M -> (M...j) = (M...M))
2	1	raleq1d 1765	. . . 4 |- (j = M -> (A.k e. (M...j)A e. CC <-> A.k e. (M...M)A e. CC))
3	1	sumeq1d 6879	. . . . . 6 |- (j = M -> sum_k e. (M...j)A = sum_k e. (M...M)A)
4	3	fveq2d 3667	. . . . 5 |- (j = M -> (abs` sum_k e. (M...j)A) = (abs` sum_k e. (M...M)A))
5	1	sumeq1d 6879	. . . . 5 |- (j = M -> sum_k e. (M...j)(abs` A) = sum_k e. (M...M)(abs` A))
6	4, 5	breq12d 2599	. . . 4 |- (j = M -> ((abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A) <-> (abs` sum_k e. (M...M)A) <_ sum_k e. (M...M)(abs` A)))
7	2, 6	imbi12d 624	. . 3 |- (j = M -> ((A.k e. (M...j)A e. CC -> (abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A)) <-> (A.k e. (M...M)A e. CC -> (abs` sum_k e. (M...M)A) <_ sum_k e. (M...M)(abs` A))))
8		opreq2 3908	. . . . 5 |- (j = m -> (M...j) = (M...m))
9	8	raleq1d 1765	. . . 4 |- (j = m -> (A.k e. (M...j)A e. CC <-> A.k e. (M...m)A e. CC))
10	8	sumeq1d 6879	. . . . . 6 |- (j = m -> sum_k e. (M...j)A = sum_k e. (M...m)A)
11	10	fveq2d 3667	. . . . 5 |- (j = m -> (abs` sum_k e. (M...j)A) = (abs` sum_k e. (M...m)A))
12	8	sumeq1d 6879	. . . . 5 |- (j = m -> sum_k e. (M...j)(abs` A) = sum_k e. (M...m)(abs` A))
13	11, 12	breq12d 2599	. . . 4 |- (j = m -> ((abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A) <-> (abs` sum_k e. (M...m)A) <_ sum_k e. (M...m)(abs` A)))
14	9, 13	imbi12d 624	. . 3 |- (j = m -> ((A.k e. (M...j)A e. CC -> (abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A)) <-> (A.k e. (M...m)A e. CC -> (abs` sum_k e. (M...m)A) <_ sum_k e. (M...m)(abs` A))))
15		opreq2 3908	. . . . 5 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
16	15	raleq1d 1765	. . . 4 |- (j = (m + 1) -> (A.k e. (M...j)A e. CC <-> A.k e. (M...(m + 1))A e. CC))
17	15	sumeq1d 6879	. . . . . 6 |- (j = (m + 1) -> sum_k e. (M...j)A = sum_k e. (M...(m + 1))A)
18	17	fveq2d 3667	. . . . 5 |- (j = (m + 1) -> (abs` sum_k e. (M...j)A) = (abs` sum_k e. (M...(m + 1))A))
19	15	sumeq1d 6879	. . . . 5 |- (j = (m + 1) -> sum_k e. (M...j)(abs` A) = sum_k e. (M...(m + 1))(abs` A))
20	18, 19	breq12d 2599	. . . 4 |- (j = (m + 1) -> ((abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A) <-> (abs` sum_k e. (M...(m + 1))A) <_ sum_k e. (M...(m + 1))(abs` A)))
21	16, 20	imbi12d 624	. . 3 |- (j = (m + 1) -> ((A.k e. (M...j)A e. CC -> (abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A)) <-> (A.k e. (M...(m + 1))A e. CC -> (abs` sum_k e. (M...(m + 1))A) <_ sum_k e. (M...(m + 1))(abs` A))))
22		opreq2 3908	. . . . 5 |- (j = N -> (M...j) = (M...N))
23	22	raleq1d 1765	. . . 4 |- (j = N -> (A.k e. (M...j)A e. CC <-> A.k e. (M...N)A e. CC))
24	22	sumeq1d 6879	. . . . . 6 |- (j = N -> sum_k e. (M...j)A = sum_k e. (M...N)A)
25	24	fveq2d 3667	. . . . 5 |- (j = N -> (abs` sum_k e. (M...j)A) = (abs` sum_k e. (M...N)A))
26	22	sumeq1d 6879	. . . . 5 |- (j = N -> sum_k e. (M...j)(abs` A) = sum_k e. (M...N)(abs` A))
27	25, 26	breq12d 2599	. . . 4 |- (j = N -> ((abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A) <-> (abs` sum_k e. (M...N)A) <_ sum_k e. (M...N)(abs` A)))
28	23, 27	imbi12d 624	. . 3 |- (j = N -> ((A.k e. (M...j)A e. CC -> (abs` sum_k e. (M...j)A) <_ sum_k e. (M...j)(abs` A)) <-> (A.k e. (M...N)A e. CC -> (abs` sum_k e. (M...N)A) <_ sum_k e. (M...N)(abs` A))))
29		csbfv2g 3682	. . . . . . 7 |- (M e. ZZ -> [_M / k]_(abs` A) = (abs` [_M / k]_A))
30	29	adantr 389	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> [_M / k]_(abs` A) = (abs` [_M / k]_A))
31		ra4csbela 2013	. . . . . . . 8 |- ((M e. (M...M) /\ A.k e. (M...M)(abs` A) e. RR) -> [_M / k]_(abs` A) e. RR)
32		elfz3t 6374	. . . . . . . 8 |- (M e. ZZ -> M e. (M...M))
33		absclt 6719	. . . . . . . . 9 |- (A e. CC -> (abs` A) e. RR)
34	33	r19.20si 1682	. . . . . . . 8 |- (A.k e. (M...M)A e. CC -> A.k e. (M...M)(abs` A) e. RR)
35	31, 32, 34	syl2an 454	. . . . . . 7 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> [_M / k]_(abs` A) e. RR)
36		leidt 5455	. . . . . . 7 |- ([_M / k]_(abs` A) e. RR -> [_M / k]_(abs` A) <_ [_M / k]_(abs` A))
37	35, 36	syl 10	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> [_M / k]_(abs` A) <_ [_M / k]_(abs` A))
38	30, 37	eqbrtrrd 2605	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> (abs` [_M / k]_A) <_ [_M / k]_(abs` A))
39		fsum1s 6898	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> sum_k e. (M...M)A = [_M / k]_A)
40	39	fveq2d 3667	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> (abs` sum_k e. (M...M)A) = (abs` [_M / k]_A))
41		fsum1s 6898	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(abs` A) e. CC) -> sum_k e. (M...M)(abs` A) = [_M / k]_(abs` A))
42	33	recnd 5238	. . . . . . 7 |- (A e. CC -> (abs` A) e. CC)
43	42	r19.20si 1682	. . . . . 6 |- (A.k e. (M...M)A e. CC -> A.k e. (M...M)(abs` A) e. CC)
44	41, 43	sylan2 451	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> sum_k e. (M...M)(abs` A) = [_M / k]_(abs` A))
45	38, 40, 44	3brtr4d 2613	. . . 4 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> (abs` sum_k e. (M...M)A) <_ sum_k e. (M...M)(abs` A))
46	45	ex 373	. . 3 |- (M e. ZZ -> (A.k e. (M...M)A e. CC -> (abs` sum_k e. (M...M)A) <_ sum_k e. (M...M)(abs` A)))
47		fzssp1t 6389	. . . . . . . . 9 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
48		eluzel2 6307	. . . . . . . . 9 |- (m e. (ZZ>` M) -> M e. ZZ)
49		eluzelz 6306	. . . . . . . . 9 |- (m e. (ZZ>` M) -> m e. ZZ)
50	47, 48, 49	sylanc 471	. . . . . . . 8 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
51	50	sseld 2038	. . . . . . 7