Theorem fsumcmpndx2 7042

Description: A shorter sum of nonnegative terms is smaller than a longer one.

Assertion

Ref	Expression
fsumcmpndx2	|- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ (A.k e. (M...K)(A e. RR /\ 0 <_ A) /\ J <_ K)) -> sum_k e. (M...J)A <_ sum_k e. (M...K)A)

Distinct variable groups:   k,J   k,K   k,M

Proof of Theorem fsumcmpndx2

Step	Hyp	Ref	Expression
1		leloet 5518	. . . . . . 7 |- ((J e. RR /\ K e. RR) -> (J <_ K <-> (J < K \/ J = K)))
2		zret 6139	. . . . . . 7 |- (J e. ZZ -> J e. RR)
3		zret 6139	. . . . . . 7 |- (K e. ZZ -> K e. RR)
4	1, 2, 3	syl2an 454	. . . . . 6 |- ((J e. ZZ /\ K e. ZZ) -> (J <_ K <-> (J < K \/ J = K)))
5		eluzelz 6423	. . . . . 6 |- (J e. (ZZ>` M) -> J e. ZZ)
6		eluzelz 6423	. . . . . 6 |- (K e. (ZZ>` M) -> K e. ZZ)
7	4, 5, 6	syl2an 454	. . . . 5 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> (J <_ K <-> (J < K \/ J = K)))
8	7	biimpa 416	. . . 4 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J <_ K) -> (J < K \/ J = K))
9	8	adantlr 393	. . 3 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J <_ K) -> (J < K \/ J = K))
10		fsumcmp0 7041	. . . . . . 7 |- ((K e. (ZZ>` (J + 1)) /\ A.k e. ((J + 1)...K)(A e. RR /\ 0 <_ A)) -> 0 <_ sum_k e. ((J + 1)...K)A)
11		zltp1let 6181	. . . . . . . . . . 11 |- ((J e. ZZ /\ K e. ZZ) -> (J < K <-> (J + 1) <_ K))
12		eluzt 6426	. . . . . . . . . . . 12 |- (((J + 1) e. ZZ /\ K e. ZZ) -> (K e. (ZZ>` (J + 1)) <-> (J + 1) <_ K))
13		peano2z 6166	. . . . . . . . . . . 12 |- (J e. ZZ -> (J + 1) e. ZZ)
14	12, 13	sylan 448	. . . . . . . . . . 11 |- ((J e. ZZ /\ K e. ZZ) -> (K e. (ZZ>` (J + 1)) <-> (J + 1) <_ K))
15	11, 14	bitr4d 531	. . . . . . . . . 10 |- ((J e. ZZ /\ K e. ZZ) -> (J < K <-> K e. (ZZ>` (J + 1))))
16	15, 5, 6	syl2an 454	. . . . . . . . 9 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> (J < K <-> K e. (ZZ>` (J + 1))))
17	16	biimpa 416	. . . . . . . 8 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> K e. (ZZ>` (J + 1)))
18	17	adantlr 393	. . . . . . 7 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> K e. (ZZ>` (J + 1)))
19		fzss1t 6503	. . . . . . . . . . . . 13 |- (((J + 1) e. (ZZ>` M) /\ K e. ZZ) -> ((J + 1)...K) (_ (M...K))
20		peano2uz 6447	. . . . . . . . . . . . 13 |- (J e. (ZZ>` M) -> (J + 1) e. (ZZ>` M))
21	19, 20, 6	syl2an 454	. . . . . . . . . . . 12 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> ((J + 1)...K) (_ (M...K))
22	21	sseld 2067	. . . . . . . . . . 11 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> (k e. ((J + 1)...K) -> k e. (M...K)))
23	22	imim1d 28	. . . . . . . . . 10 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> ((k e. (M...K) -> (A e. RR /\ 0 <_ A)) -> (k e. ((J + 1)...K) -> (A e. RR /\ 0 <_ A))))
24	23	r19.20dv2 1711	. . . . . . . . 9 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> (A.k e. (M...K)(A e. RR /\ 0 <_ A) -> A.k e. ((J + 1)...K)(A e. RR /\ 0 <_ A)))
25	24	imp 350	. . . . . . . 8 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) -> A.k e. ((J + 1)...K)(A e. RR /\ 0 <_ A))
26	25	adantr 389	. . . . . . 7 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> A.k e. ((J + 1)...K)(A e. RR /\ 0 <_ A))
27	10, 18, 26	sylanc 471	. . . . . 6 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> 0 <_ sum_k e. ((J + 1)...K)A)
28		addge01t 5672	. . . . . . 7 |- ((sum_k e. (M...J)A e. RR /\ sum_k e. ((J + 1)...K)A e. RR) -> (0 <_ sum_k e. ((J + 1)...K)A <-> sum_k e. (M...J)A <_ (sum_k e. (M...J)A + sum_k e. ((J + 1)...K)A)))
29		fsumreclt 7017	. . . . . . . 8 |- ((J e. (ZZ>` M) /\ A.k e. (M...J)A e. RR) -> sum_k e. (M...J)A e. RR)
30		pm3.26 319	. . . . . . . . 9 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> J e. (ZZ>` M))
31	30	ad2antrr 404	. . . . . . . 8 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> J e. (ZZ>` M))
32		fzss2t 6504	. . . . . . . . . . . . . 14 |- ((K e. (ZZ>` J) /\ M e. ZZ) -> (M...J) (_ (M...K))
33		ltlet 5520	. . . . . . . . . . . . . . . . . 18 |- ((J e. RR /\ K e. RR) -> (J < K -> J <_ K))
34	33, 2, 3	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((J e. ZZ /\ K e. ZZ) -> (J < K -> J <_ K))
35		eluzt 6426	. . . . . . . . . . . . . . . . 17 |- ((J e. ZZ /\ K e. ZZ) -> (K e. (ZZ>` J) <-> J <_ K))
36	34, 35	sylibrd 204	. . . . . . . . . . . . . . . 16 |- ((J e. ZZ /\ K e. ZZ) -> (J < K -> K e. (ZZ>` J)))
37	36, 5, 6	syl2an 454	. . . . . . . . . . . . . . 15 |- ((J e. (ZZ>` M) /\ K e. (ZZ>` M)) -> (J < K -> K e. (ZZ>` J)))
38	37	imp 350	. . . . . . . . . . . . . 14 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> K e. (ZZ>` J))
39		eluzel2 6424	. . . . . . . . . . . . . . 15 |- (J e. (ZZ>` M) -> M e. ZZ)
40	39	ad2antrr 404	. . . . . . . . . . . . . 14 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> M e. ZZ)
41	32, 38, 40	sylanc 471	. . . . . . . . . . . . 13 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> (M...J) (_ (M...K))
42	41	sseld 2067	. . . . . . . . . . . 12 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> (k e. (M...J) -> k e. (M...K)))
43		pm3.26 319	. . . . . . . . . . . . 13 |- ((A e. RR /\ 0 <_ A) -> A e. RR)
44	43	a1i 8	. . . . . . . . . . . 12 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> ((A e. RR /\ 0 <_ A) -> A e. RR))
45	42, 44	imim12d 29	. . . . . . . . . . 11 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> ((k e. (M...K) -> (A e. RR /\ 0 <_ A)) -> (k e. (M...J) -> A e. RR)))
46	45	r19.20dv2 1711	. . . . . . . . . 10 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> (A.k e. (M...K)(A e. RR /\ 0 <_ A) -> A.k e. (M...J)A e. RR))
47	46	imp 350	. . . . . . . . 9 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) -> A.k e. (M...J)A e. RR)
48	47	an1rs 489	. . . . . . . 8 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> A.k e. (M...J)A e. RR)
49	29, 31, 48	sylanc 471	. . . . . . 7 |- ((((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ A.k e. (M...K)(A e. RR /\ 0 <_ A)) /\ J < K) -> sum_k e. (M...J)A e. RR)
50		fsumreclt 7017	. . . . . . . 8 |- ((K e. (ZZ>` (J + 1)) /\ A.k e. ((J + 1)...K)A e. RR) -> sum_k e. ((J + 1)...K)A e. RR)
51	22	adantr 389	. . . . . . . . . . . 12 |- (((J e. (ZZ>` M) /\ K e. (ZZ>` M)) /\ J < K) -> (k