Theorem fsumcmp 7163

Description: If all of the terms of finite sums compare, so do the sums.

Assertion

Ref	Expression
fsumcmp	|- ((N e. (ZZ>` M) /\ A.k e. (M...N)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...N)A <_ sum_k e. (M...N)B)

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumcmp

Step	Hyp	Ref	Expression
1		ra4sbca 2040	. . . . . . 7 |- ((M e. (M...M) /\ A.k e. (M...M)A <_ B) -> [M / k]A <_ B)
2		elfz3 6551	. . . . . . 7 |- (M e. ZZ -> M e. (M...M))
3		3simp3 793	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A <_ B)
4	3	r19.20si 1744	. . . . . . 7 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)A <_ B)
5	1, 2, 4	syl2an 456	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> [M / k]A <_ B)
6		sbcbr12g 2714	. . . . . . 7 |- (M e. ZZ -> ([M / k]A <_ B <-> [_M / k]_A <_ [_M / k]_B))
7	6	adantr 389	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> ([M / k]A <_ B <-> [_M / k]_A <_ [_M / k]_B))
8	5, 7	mpbid 193	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> [_M / k]_A <_ [_M / k]_B)
9		fsum1s 7132	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)A e. RR) -> sum_k e. (M...M)A = [_M / k]_A)
10		3simp1 791	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. RR)
11	10	r19.20si 1744	. . . . . 6 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)A e. RR)
12	9, 11	sylan2 453	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)A = [_M / k]_A)
13		fsum1s 7132	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)B e. RR) -> sum_k e. (M...M)B = [_M / k]_B)
14		3simp2 792	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A <_ B) -> B e. RR)
15	14	r19.20si 1744	. . . . . 6 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)B e. RR)
16	13, 15	sylan2 453	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)B = [_M / k]_B)
17	8, 12, 16	3brtr4d 2695	. . . 4 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)A <_ sum_k e. (M...M)B)
18	17	ex 371	. . 3 |- (M e. ZZ -> (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...M)A <_ sum_k e. (M...M)B))
19		fzssp1 6566	. . . . . . . . 9 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
20		eluzel2 6484	. . . . . . . . 9 |- (m e. (ZZ>` M) -> M e. ZZ)
21		eluzelz 6483	. . . . . . . . 9 |- (m e. (ZZ>` M) -> m e. ZZ)
22	19, 20, 21	sylanc 473	. . . . . . . 8 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
23	22	sseld 2111	. . . . . . 7 |- (m e. (ZZ>` M) -> (k e. (M...m) -> k e. (M...(m + 1))))
24	23	imim1d 28	. . . . . 6 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> (A e. RR /\ B e. RR /\ A <_ B))))
25	24	r19.20dv2 1749	. . . . 5 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)(A e. RR /\ B e. RR /\ A <_ B)))
26	25	imim1d 28	. . . 4 |- (m e. (ZZ>` M) -> ((A.k e. (M...m)(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B)))
27		fsump1s 7136	. . . . . . . . . 10 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. RR) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
28	10	r19.20si 1744	. . . . . . . . . 10 |- (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...(m + 1))A e. RR)
29	27, 28	sylan2 453	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
30	29	adantr 389	. . . . . . . 8 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
31		pm3.27 321	. . . . . . . . 9 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B)
32		leadd1 5714	. . . . . . . . . 10 |- ((sum_k e. (M...m)A e. RR /\ sum_k e. (M...m)B e. RR /\ [_(m + 1) / k]_A e. RR) -> (sum_k e. (M...m)A <_ sum_k e. (M...m)B <-> (sum_k e. (M...m)A + [_(m + 1) / k]_A) <_ (sum_k e. (M...m)B + [_(m + 1) / k]_A)))
33	10	a1i 8	. . . . . . . . . . . . . . 15 |- (m e. (ZZ>` M) -> ((A e. RR /\ B e. RR /\ A <_ B) -> A e. RR))
34	23, 33	imim12d 29	. . . . . . . . . . . . . 14 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> A e. RR)))
35	34	r19.20dv2 1749	. . . . . . . . . . . . 13 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)A e. RR))
36	35	imp 348	. . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> A.k e. (M...m)A e. RR)
37		fsumrecl 7140	. . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...m)A e. RR) -> sum_k e. (M...m)A e. RR)
38	36, 37	syldan 469	. . . . . . . . . . 11 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...m)A e. RR)
39	38	adantr 389	. . . . . . . . . 10 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...m)A e. RR)
40	14	a1i 8	. . . . . . . . . . . . . . 15 |- (m e. (ZZ>` M) -> ((A e. RR /\ B e. RR /\ A <_ B) -> B e. RR))
41	23, 40	imim12d 29	. . . . . . . . . . . . . 14 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> B e. RR)))
42	41	r19.20dv2 1749	. . . . . . . . . . . . 13 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)B e. RR))
43	42	imp 348	. . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> A.k e. (M...m)B e. RR)
44		fsumrecl 7140	. . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...