Theorem isumcmpi 7158

Description: Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.)

Hypotheses

Ref	Expression
isumcmpi.1	|- A e. V
isumcmpi.2	|- B e. V
isumcmpi.3	|- F = {<.j, y>. | (j e. (ZZ>` M) /\ y = A)}
isumcmpi.4	|- G = {<.j, y>. | (j e. (ZZ>` M) /\ y = B)}
isumcmpi.5	|- (j e. (ZZ>` M) -> (A e. RR /\ B e. RR /\ A <_ B))

Assertion

Ref	Expression
isumcmpi	|- ((M e. ZZ /\ (E.x(<.M, + >. seq F) ~~> x /\ E.x(<.M, + >. seq G) ~~> x)) -> sum_j e. (ZZ>` M)A <_ sum_j e. (ZZ>` M)B)

Distinct variable groups:   x,y,A   x,B,y   x,F   x,G   x,j,y,M

Proof of Theorem isumcmpi

Step	Hyp	Ref	Expression
1		r19.26 1747	. . . . . . 7 |- (A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (F` k) <_ (G` k)) <-> (A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR) /\ A.k e. (ZZ>` M)(F` k) <_ (G` k)))
2		r19.26 1747	. . . . . . . 8 |- (A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR) <-> (A.k e. (ZZ>` M)(F` k) e. RR /\ A.k e. (ZZ>` M)(G` k) e. RR))
3		isumcmpi.5	. . . . . . . . . . . . 13 |- (j e. (ZZ>` M) -> (A e. RR /\ B e. RR /\ A <_ B))
4	3	3simp1d 793	. . . . . . . . . . . 12 |- (j e. (ZZ>` M) -> A e. RR)
5		fvopab2 3782	. . . . . . . . . . . . 13 |- ((j e. (ZZ>` M) /\ A e. RR) -> ({<.j, y>. | (j e. (ZZ>` M) /\ y = A)}` j) = A)
6		isumcmpi.3	. . . . . . . . . . . . . 14 |- F = {<.j, y>. | (j e. (ZZ>` M) /\ y = A)}
7	6	fveq1i 3716	. . . . . . . . . . . . 13 |- (F` j) = ({<.j, y>. | (j e. (ZZ>` M) /\ y = A)}` j)
8	5, 7	syl5eq 1516	. . . . . . . . . . . 12 |- ((j e. (ZZ>` M) /\ A e. RR) -> (F` j) = A)
9	4, 8	mpdan 703	. . . . . . . . . . 11 |- (j e. (ZZ>` M) -> (F` j) = A)
10	9, 4	eqeltrd 1545	. . . . . . . . . 10 |- (j e. (ZZ>` M) -> (F` j) e. RR)
11	10	rgen 1695	. . . . . . . . 9 |- A.j e. (ZZ>` M)(F` j) e. RR
12		ax-17 969	. . . . . . . . . 10 |- ((F` j) e. RR -> A.k(F` j) e. RR)
13		hbopab1 2808	. . . . . . . . . . . . 13 |- (x e. {<.j, y>. | (j e. (ZZ>` M) /\ y = A)} -> A.j x e. {<.j, y>. | (j e. (ZZ>` M) /\ y = A)})
14	6, 13	hbxfr 1560	. . . . . . . . . . . 12 |- (x e. F -> A.j x e. F)
15		ax-17 969	. . . . . . . . . . . 12 |- (x e. k -> A.j x e. k)
16	14, 15	hbfv 3720	. . . . . . . . . . 11 |- (x e. (F` k) -> A.j x e. (F` k))
17		ax-17 969	. . . . . . . . . . 11 |- (x e. RR -> A.j x e. RR)
18	16, 17	hbel 1563	. . . . . . . . . 10 |- ((F` k) e. RR -> A.j(F` k) e. RR)
19		fveq2 3715	. . . . . . . . . . 11 |- (j = k -> (F` j) = (F` k))
20	19	eleq1d 1537	. . . . . . . . . 10 |- (j = k -> ((F` j) e. RR <-> (F` k) e. RR))
21	12, 18, 20	cbvral 1794	. . . . . . . . 9 |- (A.j e. (ZZ>` M)(F` j) e. RR <-> A.k e. (ZZ>` M)(F` k) e. RR)
22	11, 21	mpbi 189	. . . . . . . 8 |- A.k e. (ZZ>` M)(F` k) e. RR
23	3	3simp2d 794	. . . . . . . . . . . 12 |- (j e. (ZZ>` M) -> B e. RR)
24		fvopab2 3782	. . . . . . . . . . . . 13 |- ((j e. (ZZ>` M) /\ B e. RR) -> ({<.j, y>. | (j e. (ZZ>` M) /\ y = B)}` j) = B)
25		isumcmpi.4	. . . . . . . . . . . . . 14 |- G = {<.j, y>. | (j e. (ZZ>` M) /\ y = B)}
26	25	fveq1i 3716	. . . . . . . . . . . . 13 |- (G` j) = ({<.j, y>. | (j e. (ZZ>` M) /\ y = B)}` j)
27	24, 26	syl5eq 1516	. . . . . . . . . . . 12 |- ((j e. (ZZ>` M) /\ B e. RR) -> (G` j) = B)
28	23, 27	mpdan 703	. . . . . . . . . . 11 |- (j e. (ZZ>` M) -> (G` j) = B)
29	28, 23	eqeltrd 1545	. . . . . . . . . 10 |- (j e. (ZZ>` M) -> (G` j) e. RR)
30	29	rgen 1695	. . . . . . . . 9 |- A.j e. (ZZ>` M)(G` j) e. RR
31		ax-17 969	. . . . . . . . . 10 |- ((G` j) e. RR -> A.k(G` j) e. RR)
32		hbopab1 2808	. . . . . . . . . . . . 13 |- (x e. {<.j, y>. | (j e. (ZZ>` M) /\ y = B)} -> A.j x e. {<.j, y>. | (j e. (ZZ>` M) /\ y = B)})
33	25, 32	hbxfr 1560	. . . . . . . . . . . 12 |- (x e. G -> A.j x e. G)
34	33, 15	hbfv 3720	. . . . . . . . . . 11 |- (x e. (G` k) -> A.j x e. (G` k))
35	34, 17	hbel 1563	. . . . . . . . . 10 |- ((G` k) e. RR -> A.j(G` k) e. RR)
36		fveq2 3715	. . . . . . . . . . 11 |- (j = k -> (G` j) = (G` k))
37	36	eleq1d 1537	. . . . . . . . . 10 |- (j = k -> ((G` j) e. RR <-> (G` k) e. RR))
38	31, 35, 37	cbvral 1794	. . . . . . . . 9 |- (A.j e. (ZZ>` M)(G` j) e. RR <-> A.k e. (ZZ>` M)(G` k) e. RR)
39	30, 38	mpbi 189	. . . . . . . 8 |- A.k e. (ZZ>` M)(G` k) e. RR
40	2, 22, 39	mpbir2an 729	. . . . . . 7 |- A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR)
41	3	3simp3d 795	. . . . . . . . . 10 |- (j e. (ZZ>` M) -> A <_ B)
42	41, 9, 28	3brtr4d 2640	. . . . . . . . 9 |- (j e. (ZZ>` M) -> (F` j) <_ (G` j))
43	42	rgen 1695	. . . . . . . 8 |- A.j e. (ZZ>` M)(F` j) <_ (G` j)
44		ax-17 969	. . . . . . . . 9 |- ((F` j) <_ (G` j) -> A.k(F` j) <_ (G` j))
45		ax-17 969	. . . . . . . . . 10 |- (x e. <_ -> A.j x e. <_ )
46	16, 45, 34	hbbr 2653	. . . . . . . . 9 |- ((F` k) <_ (G` k) -> A.j(F` k) <_ (G` k))
47	19, 36	breq12d 2626	. . . . . . . . 9 |- (j = k -> ((F` j) <_ (G` j) <-> (F` k) <_ (G` k)))
48	44, 46, 47	cbvral 1794	. . . . . . . 8 |- (A.j e. (ZZ>` M)(F` j) <_ (G` j) <-> A.k e. (ZZ>` M)(F` k) <_ (G` k))
49	43, 48	mpbi 189	. . . . . . 7 |- A.k e. (ZZ>` M)(F` k) <_ (G` k)
50	1, 40, 49	mpbir2an 729	. . . . . 6 |- A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (F` k) <_ (G` k))
51		df-3an 776	. . . . . . 7 |- (((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)) <-> (((F` k) e. RR /\ (G` k) e. RR) /\ (F` k) <_ (G` k)))
52	51	ralbii 1664	. . . . . 6 |- (A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)) <-> A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (F` k) <_ (G` k)))
53	50, 52	mpbir 190	. . . . 5 |- A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k))
54		sumex 6927	. . . . . 6 |- sum_j e. (ZZ>` M)A e. V
55		sumex 6927	. . . . . 6 |- sum_j e. (ZZ>` M)B e. V
56		fvex 3723	. . . . . . 7 |- (ZZ>` M) e. V
57	56, 6	fopabex2 3604	. . . . . 6 |- F e. V
58	56, 25	fopabex2 3604	. . . . . 6 |- G e. V
59	54, 55, 57, 58	iserzcmp 7086	. . . . 5 |- ((((<.M, + >. seq F) ~~> sum_j e. (ZZ>` M)A /\ (<.M, + >. seq G) ~~> sum_j e. (ZZ>` M)B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)))) -> sum_j e. (ZZ>` M)A <_ sum_j e. (ZZ>` M)B)
60	53, 59	mpanr2 709	. . . 4 |- ((((<.M, + >. seq F) ~~> sum_j e. (ZZ>` M)A /\ (<.M, + >. seq G) ~~> sum_j e. (ZZ>` M)B) /\ M e. ZZ) -> sum_j e. (ZZ>` M)A <_ sum_j e. (ZZ>` M)B)
61	60	expcom 374	. . 3 |- (M e. ZZ -> (((<.M, + >. seq F) ~~> sum_j e. (ZZ>` M)A /\ (<.M, + >. seq G) ~~> sum_j e. (ZZ>` M)B) -> sum_j e. (ZZ>` M)A <_ sum_j e. (ZZ>` M)B))
62		isumcmpi.1	. . . . 5 |- A e. V
63	62, 6	isumclim3t 7143	. . . 4 |- ((M e. ZZ /\ E.x(<.M, + >. seq F) ~~> x) -> (<.M, + >. seq F) ~~> sum_j e. (ZZ>` M)A)
64	63	ex 373	. . 3