Theorem jensenlem2 20779

Description: Lemma for jensen 20780. (Contributed by Mario Carneiro, 21-Jun-2015.)

Hypotheses

Ref	Expression
jensen.1	|- ( ph -> D C_ RR )
jensen.2	|- ( ph -> F : D --> RR )
jensen.3	|- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
jensen.4	|- ( ph -> A e. Fin )
jensen.5	|- ( ph -> T : A --> ( 0 [,) +oo ) )
jensen.6	|- ( ph -> X : A --> D )
jensen.7	|- ( ph -> 0 < (ℂfld gsumg T ) )
jensen.8	|- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
jensenlem.1	|- ( ph -> -. z e. B )
jensenlem.2	|- ( ph -> ( B u. { z } ) C_ A )
jensenlem.s	|- S = (ℂfld gsumg ( T |` B ) )
jensenlem.l	|- L = (ℂfld gsumg ( T |` ( B u. { z } ) ) )
jensenlem.3	|- ( ph -> S e. RR+ )
jensenlem.4	|- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) e. D )
jensenlem.5	|- ( ph -> ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) )

Assertion

Ref	Expression
jensenlem2	|- ( ph -> ( ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) e. D /\ ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) ) )

Distinct variable groups:   a, b, t, x, y, A   D, a, b, t, x, y   ph, a, b, t, x, y   F, a, b, t, x, y   T, a, b, t, x, y   X, a, b, t, x, y   z, a, B, b, t, x, y   t, L, x, y   S, a, b, t, x, y

Allowed substitution hints:   ph( z)   A( z)   D( z)   S( z)   T( z)   F( z)   L( z, a, b)   X( z)

Proof of Theorem jensenlem2

Step	Hyp	Ref	Expression
1		cnfld0 16680	. . . . . . 7 |- 0 = ( 0g ` ℂfld )
2		cnrng 16678	. . . . . . . 8 |- ℂfld e. Ring
3		rngabl 15648	. . . . . . . 8 |- (ℂfld e. Ring -> ℂfld e. Abel )
4	2, 3	mp1i 12	. . . . . . 7 |- ( ph -> ℂfld e. Abel )
5		jensen.4	. . . . . . . 8 |- ( ph -> A e. Fin )
6		jensenlem.2	. . . . . . . . 9 |- ( ph -> ( B u. { z } ) C_ A )
7	6	unssad 3484	. . . . . . . 8 |- ( ph -> B C_ A )
8		ssfi 7288	. . . . . . . 8 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
9	5, 7, 8	syl2anc 643	. . . . . . 7 |- ( ph -> B e. Fin )
10		resubdrg 16705	. . . . . . . . 9 |- ( RR e. (SubRing ` ℂfld ) /\ (ℂfld ↾s RR ) e. DivRing )
11	10	simpli 445	. . . . . . . 8 |- RR e. (SubRing ` ℂfld )
12		subrgsubg 15829	. . . . . . . 8 |- ( RR e. (SubRing ` ℂfld ) -> RR e. (SubGrp ` ℂfld ) )
13	11, 12	mp1i 12	. . . . . . 7 |- ( ph -> RR e. (SubGrp ` ℂfld ) )
14		remulcl 9031	. . . . . . . . . 10 |- ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
15	14	adantl 453	. . . . . . . . 9 |- ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
16		jensen.5	. . . . . . . . . 10 |- ( ph -> T : A --> ( 0 [,) +oo ) )
17		0re 9047	. . . . . . . . . . 11 |- 0 e. RR
18		pnfxr 10669	. . . . . . . . . . 11 |- +oo e. RR*
19		icossre 10947	. . . . . . . . . . 11 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
20	17, 18, 19	mp2an 654	. . . . . . . . . 10 |- ( 0 [,) +oo ) C_ RR
21		fss 5558	. . . . . . . . . 10 |- ( ( T : A --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> T : A --> RR )
22	16, 20, 21	sylancl 644	. . . . . . . . 9 |- ( ph -> T : A --> RR )
23		jensen.6	. . . . . . . . . 10 |- ( ph -> X : A --> D )
24		jensen.1	. . . . . . . . . 10 |- ( ph -> D C_ RR )
25		fss 5558	. . . . . . . . . 10 |- ( ( X : A --> D /\ D C_ RR ) -> X : A --> RR )
26	23, 24, 25	syl2anc 643	. . . . . . . . 9 |- ( ph -> X : A --> RR )
27		inidm 3510	. . . . . . . . 9 |- ( A i^i A ) = A
28	15, 22, 26, 5, 5, 27	off 6279	. . . . . . . 8 |- ( ph -> ( T o F x. X ) : A --> RR )
29		fssres 5569	. . . . . . . 8 |- ( ( ( T o F x. X ) : A --> RR /\ B C_ A ) -> ( ( T o F x. X ) |` B ) : B --> RR )
30	28, 7, 29	syl2anc 643	. . . . . . 7 |- ( ph -> ( ( T o F x. X ) |` B ) : B --> RR )
31	9, 30	fisuppfi 14728	. . . . . . 7 |- ( ph -> ( `' ( ( T o F x. X ) |` B ) " ( _V \ { 0 } ) ) e. Fin )
32	1, 4, 9, 13, 30, 31	gsumsubgcl 15480	. . . . . 6 |- ( ph -> (ℂfld gsumg ( ( T o F x. X ) |` B ) ) e. RR )
33	32	recnd 9070	. . . . 5 |- ( ph -> (ℂfld gsumg ( ( T o F x. X ) |` B ) ) e. CC )
34		ax-resscn 9003	. . . . . . . 8 |- RR C_ CC
35	20, 34	sstri 3317	. . . . . . 7 |- ( 0 [,) +oo ) C_ CC
36	6	unssbd 3485	. . . . . . . . 9 |- ( ph -> { z } C_ A )
37		vex 2919	. . . . . . . . . 10 |- z e. _V
38	37	snss 3886	. . . . . . . . 9 |- ( z e. A <-> { z } C_ A )
39	36, 38	sylibr 204	. . . . . . . 8 |- ( ph -> z e. A )
40	16, 39	ffvelrnd 5830	. . . . . . 7 |- ( ph -> ( T ` z ) e. ( 0 [,) +oo ) )
41	35, 40	sseldi 3306	. . . . . 6 |- ( ph -> ( T ` z ) e. CC )
42	23, 39	ffvelrnd 5830	. . . . . . . 8 |- ( ph -> ( X ` z ) e. D )
43	24, 42	sseldd 3309	. . . . . . 7 |- ( ph -> ( X ` z ) e. RR )
44	43	recnd 9070	. . . . . 6 |- ( ph -> ( X ` z ) e. CC )
45	41, 44	mulcld 9064	. . . . 5 |- ( ph -> ( ( T ` z ) x. ( X ` z ) ) e. CC )
46		jensen.2	. . . . . . . 8 |- ( ph -> F : D --> RR )
47		jensen.3	. . . . . . . 8 |- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
48		jensen.7	. . . . . . . 8 |- ( ph -> 0 < (ℂfld gsumg T ) )
49		jensen.8	. . . . . . . 8 |- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
50		jensenlem.1	. . . . . . . 8 |- ( ph -> -. z e. B )
51		jensenlem.s	. . . . . . . 8 |- S = (ℂfld gsumg ( T |` B ) )
52		jensenlem.l	. . . . . . . 8 |- L = (ℂfld gsumg ( T |` ( B u. { z } ) ) )
53	24, 46, 47, 5, 16, 23, 48, 49, 50, 6, 51, 52	jensenlem1 20778	. . . . . . 7 |- ( ph -> L = ( S + ( T ` z ) ) )
54		jensenlem.3	. . . . . . . . 9 |- ( ph -> S e. RR+ )
55	54	rpred 10604	. . . . . . . 8 |- ( ph -> S e. RR )
56		elrege0 10963	. . . . . . . . . 10 |- ( ( T ` z ) e. ( 0 [,) +oo ) <-> ( ( T ` z ) e. RR /\ 0 <_ ( T ` z ) ) )
57	56	simplbi 447	. . . . . . . . 9 |- ( ( T ` z ) e. ( 0 [,) +oo ) -> ( T ` z ) e. RR )
58	40, 57	syl 16	. . . . . . . 8 |- ( ph -> ( T ` z ) e. RR )
59	55, 58	readdcld 9071	. . . . . . 7 |- ( ph -> ( S + ( T ` z ) ) e. RR )
60	53, 59	eqeltrd 2478	. . . . . 6 |- ( ph -> L e. RR )
61	60	recnd 9070	. . . . 5 |- ( ph -> L e. CC )
62	17	a1i 11	. . . . . . 7 |- ( ph -> 0 e. RR )
63	54	rpgt0d 10607	. . . . . . 7 |- ( ph -> 0 < S )
64	56	simprbi 451	. . . . . . . . . 10 |- ( ( T ` z ) e. ( 0 [,) +oo ) -> 0 <_ ( T ` z ) )
65	40, 64	syl 16	. . . . . . . . 9 |- ( ph -> 0 <_ ( T ` z ) )
66	55, 58	addge01d 9570	. . . . . . . . 9 |- ( ph -> ( 0 <_ ( T ` z ) <-> S <_ ( S + ( T ` z ) ) ) )
67	65, 66	mpbid 202	. . . . . . . 8 |- ( ph -> S <_ ( S + ( T ` z ) ) )
68	67, 53	breqtrrd 4198	. . . . . . 7 |- ( ph -> S <_ L )
69	62, 55, 60, 63, 68	ltletrd 9186	. . . . . 6 |- ( ph -> 0 < L )
70	69	gt0ne0d 9547	. . . . 5 |- ( ph -> L =/= 0 )
71	33, 45, 61, 70	divdird 9784	. . . 4 |- ( ph -> ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) + ( ( T ` z ) x. ( X ` z ) ) ) / L ) = ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / L ) + ( ( ( T ` z ) x. ( X ` z ) ) / L ) ) )
72		cnfldbas 16662	. . . . . . 7 |- CC = ( Base ` ℂfld )
73		cnfldadd 16663	. . . . . . 7 |- + = ( +g ` ℂfld )
74		rngcmn 15649	. . . . . . . 8 |- (ℂfld e. Ring -> ℂfld e. CMnd )
75	2, 74	mp1i 12	. . . . . . 7 |- ( ph -> ℂfld e. CMnd )
76	7	sselda 3308	. . . . . . . . . 10 |- ( ( ph /\ x e. B ) -> x e. A )
77	16	ffvelrnda 5829	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( T ` x ) e. ( 0 [,) +oo ) )
78	76, 77	syldan 457	. . . . . . . . 9 |- ( ( ph /\ x e. B ) -> ( T ` x ) e. ( 0 [,) +oo ) )
79	35, 78	sseldi 3306	. . . . . . . 8 |- ( ( ph /\ x e. B ) -> ( T ` x ) e. CC )
80	24	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ x e. B ) -> D C_ RR )
81	23	ffvelrnda 5829	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( X ` x ) e. D )
82	76, 81	syldan 457	. . . . . . . . . 10 |- ( ( ph /\ x e. B ) -> ( X ` x ) e. D )
83	80, 82	sseldd 3309	. . . . . . . . 9 |- ( ( ph /\ x e. B ) -> ( X ` x ) e. RR )
84	83	recnd 9070	. . . . . . . 8 |- ( ( ph /\ x e. B ) -> ( X ` x ) e. CC )
85	79, 84	mulcld 9064	. . . . . . 7 |- ( ( ph /\ x e. B ) -> ( ( T ` x ) x. ( X ` x ) ) e. CC )
86		fveq2 5687	. . . . . . . 8 |- ( x = z -> ( T ` x ) = ( T ` z ) )
87		fveq2 5687	. . . . . . . 8 |- ( x = z -> ( X ` x ) = ( X ` z ) )
88	86, 87	oveq12d 6058	. . . . . . 7 |- ( x = z -> ( ( T ` x ) x. ( X ` x ) ) = ( ( T ` z ) x. ( X ` z ) ) )
89	72, 73, 75, 9, 85, 39, 50, 45, 88	gsumunsn 15499	. . . . . 6 |- ( ph -> (ℂfld gsumg ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( X ` x ) ) ) ) = ( (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) ) + ( ( T ` z ) x. ( X ` z ) ) ) )
90	16	feqmptd 5738	. . . . . . . . . 10 |- ( ph -> T = ( x e. A |-> ( T ` x ) ) )
91	23	feqmptd 5738	. . . . . . . . . 10 |- ( ph -> X = ( x e. A |-> ( X ` x ) ) )
92	5, 77, 81, 90, 91	offval2 6281	. . . . . . . . 9 |- ( ph -> ( T o F x. X ) = ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) )
93	92	reseq1d 5104	. . . . . . . 8 |- ( ph -> ( ( T o F x. X ) |` ( B u. { z } ) ) = ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` ( B u. { z } ) ) )
94		resmpt 5150	. . . . . . . . 9 |- ( ( B u. { z } ) C_ A -> ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( X ` x ) ) ) )
95	6, 94	syl 16	. . . . . . . 8 |- ( ph -> ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( X ` x ) ) ) )
96	93, 95	eqtrd 2436	. . . . . . 7 |- ( ph -> ( ( T o F x. X ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( X ` x ) ) ) )
97	96	oveq2d 6056	. . . . . 6 |- ( ph -> (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) = (ℂfld gsumg ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( X ` x ) ) ) ) )
98	92	reseq1d 5104	. . . . . . . . 9 |- ( ph -> ( ( T o F x. X ) |` B ) = ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` B ) )
99		resmpt 5150	. . . . . . . . . 10 |- ( B C_ A -> ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) )
100	7, 99	syl 16	. . . . . . . . 9 |- ( ph -> ( ( x e. A |-> ( ( T ` x ) x. ( X ` x ) ) ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) )
101	98, 100	eqtrd 2436	. . . . . . . 8 |- ( ph -> ( ( T o F x. X ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) )
102	101	oveq2d 6056	. . . . . . 7 |- ( ph -> (ℂfld gsumg ( ( T o F x. X ) |` B ) ) = (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) ) )
103	102	oveq1d 6055	. . . . . 6 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) + ( ( T ` z ) x. ( X ` z ) ) ) = ( (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( X ` x ) ) ) ) + ( ( T ` z ) x. ( X ` z ) ) ) )
104	89, 97, 103	3eqtr4d 2446	. . . . 5 |- ( ph -> (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) + ( ( T ` z ) x. ( X ` z ) ) ) )
105	104	oveq1d 6055	. . . 4 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) = ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) + ( ( T ` z ) x. ( X ` z ) ) ) / L ) )
106	55	recnd 9070	. . . . . 6 |- ( ph -> S e. CC )
107	54	rpne0d 10609	. . . . . 6 |- ( ph -> S =/= 0 )
108	33, 106, 61, 107, 70	dmdcand 9775	. . . . 5 |- ( ph -> ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / L ) )
109	61, 106, 61, 70	divsubdird 9785	. . . . . . . 8 |- ( ph -> ( ( L - S ) / L ) = ( ( L / L ) - ( S / L ) ) )
110	53	oveq1d 6055	. . . . . . . . . 10 |- ( ph -> ( L - S ) = ( ( S + ( T ` z ) ) - S ) )
111	106, 41	pncan2d 9369	. . . . . . . . . 10 |- ( ph -> ( ( S + ( T ` z ) ) - S ) = ( T ` z ) )
112	110, 111	eqtrd 2436	. . . . . . . . 9 |- ( ph -> ( L - S ) = ( T ` z ) )
113	112	oveq1d 6055	. . . . . . . 8 |- ( ph -> ( ( L - S ) / L ) = ( ( T ` z ) / L ) )
114	61, 70	dividd 9744	. . . . . . . . 9 |- ( ph -> ( L / L ) = 1 )
115	114	oveq1d 6055	. . . . . . . 8 |- ( ph -> ( ( L / L ) - ( S / L ) ) = ( 1 - ( S / L ) ) )
116	109, 113, 115	3eqtr3rd 2445	. . . . . . 7 |- ( ph -> ( 1 - ( S / L ) ) = ( ( T ` z ) / L ) )
117	116	oveq1d 6055	. . . . . 6 |- ( ph -> ( ( 1 - ( S / L ) ) x. ( X ` z ) ) = ( ( ( T ` z ) / L ) x. ( X ` z ) ) )
118	41, 44, 61, 70	div23d 9783	. . . . . 6 |- ( ph -> ( ( ( T ` z ) x. ( X ` z ) ) / L ) = ( ( ( T ` z ) / L ) x. ( X ` z ) ) )
119	117, 118	eqtr4d 2439	. . . . 5 |- ( ph -> ( ( 1 - ( S / L ) ) x. ( X ` z ) ) = ( ( ( T ` z ) x. ( X ` z ) ) / L ) )
120	108, 119	oveq12d 6058	. . . 4 |- ( ph -> ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) = ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / L ) + ( ( ( T ` z ) x. ( X ` z ) ) / L ) ) )
121	71, 105, 120	3eqtr4d 2446	. . 3 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) = ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) )
122		jensenlem.4	. . . . 5 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) e. D )
123	55, 60, 70	redivcld 9798	. . . . . 6 |- ( ph -> ( S / L ) e. RR )
124	54	rpge0d 10608	. . . . . . 7 |- ( ph -> 0 <_ S )
125		divge0 9835	. . . . . . 7 |- ( ( ( S e. RR /\ 0 <_ S ) /\ ( L e. RR /\ 0 < L ) ) -> 0 <_ ( S / L ) )
126	55, 124, 60, 69, 125	syl22anc 1185	. . . . . 6 |- ( ph -> 0 <_ ( S / L ) )
127	61	mulid1d 9061	. . . . . . . 8 |- ( ph -> ( L x. 1 ) = L )
128	68, 127	breqtrrd 4198	. . . . . . 7 |- ( ph -> S <_ ( L x. 1 ) )
129		1re 9046	. . . . . . . . 9 |- 1 e. RR
130	129	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. RR )
131		ledivmul 9839	. . . . . . . 8 |- ( ( S e. RR /\ 1 e. RR /\ ( L e. RR /\ 0 < L ) ) -> ( ( S / L ) <_ 1 <-> S <_ ( L x. 1 ) ) )
132	55, 130, 60, 69, 131	syl112anc 1188	. . . . . . 7 |- ( ph -> ( ( S / L ) <_ 1 <-> S <_ ( L x. 1 ) ) )
133	128, 132	mpbird 224	. . . . . 6 |- ( ph -> ( S / L ) <_ 1 )
134	17, 129	elicc2i 10932	. . . . . 6 |- ( ( S / L ) e. ( 0 [,] 1 ) <-> ( ( S / L ) e. RR /\ 0 <_ ( S / L ) /\ ( S / L ) <_ 1 ) )
135	123, 126, 133, 134	syl3anbrc 1138	. . . . 5 |- ( ph -> ( S / L ) e. ( 0 [,] 1 ) )
136	122, 42, 135	3jca 1134	. . . 4 |- ( ph -> ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) e. D /\ ( X ` z ) e. D /\ ( S / L ) e. ( 0 [,] 1 ) ) )
137	24, 47	cvxcl 20776	. . . 4 |- ( ( ph /\ ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) e. D /\ ( X ` z ) e. D /\ ( S / L ) e. ( 0 [,] 1 ) ) ) -> ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) e. D )
138	136, 137	mpdan 650	. . 3 |- ( ph -> ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) e. D )
139	121, 138	eqeltrd 2478	. 2 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) e. D )
140	46, 138	ffvelrnd 5830	. . . 4 |- ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) e. RR )
141	46, 122	ffvelrnd 5830	. . . . . 6 |- ( ph -> ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) e. RR )
142	123, 141	remulcld 9072	. . . . 5 |- ( ph -> ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) e. RR )
143	46, 42	ffvelrnd 5830	. . . . . . 7 |- ( ph -> ( F ` ( X ` z ) ) e. RR )
144	58, 143	remulcld 9072	. . . . . 6 |- ( ph -> ( ( T ` z ) x. ( F ` ( X ` z ) ) ) e. RR )
145	144, 60, 70	redivcld 9798	. . . . 5 |- ( ph -> ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) e. RR )
146	142, 145	readdcld 9071	. . . 4 |- ( ph -> ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) e. RR )
147		fco 5559	. . . . . . . . . . 11 |- ( ( F : D --> RR /\ X : A --> D ) -> ( F o. X ) : A --> RR )
148	46, 23, 147	syl2anc 643	. . . . . . . . . 10 |- ( ph -> ( F o. X ) : A --> RR )
149	15, 22, 148, 5, 5, 27	off 6279	. . . . . . . . 9 |- ( ph -> ( T o F x. ( F o. X ) ) : A --> RR )
150		fssres 5569	. . . . . . . . 9 |- ( ( ( T o F x. ( F o. X ) ) : A --> RR /\ B C_ A ) -> ( ( T o F x. ( F o. X ) ) |` B ) : B --> RR )
151	149, 7, 150	syl2anc 643	. . . . . . . 8 |- ( ph -> ( ( T o F x. ( F o. X ) ) |` B ) : B --> RR )
152	9, 151	fisuppfi 14728	. . . . . . . 8 |- ( ph -> ( `' ( ( T o F x. ( F o. X ) ) |` B ) " ( _V \ { 0 } ) ) e. Fin )
153	1, 4, 9, 13, 151, 152	gsumsubgcl 15480	. . . . . . 7 |- ( ph -> (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) e. RR )
154	153, 55, 107	redivcld 9798	. . . . . 6 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) e. RR )
155	123, 154	remulcld 9072	. . . . 5 |- ( ph -> ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) e. RR )
156		resubcl 9321	. . . . . . 7 |- ( ( 1 e. RR /\ ( S / L ) e. RR ) -> ( 1 - ( S / L ) ) e. RR )
157	129, 123, 156	sylancr 645	. . . . . 6 |- ( ph -> ( 1 - ( S / L ) ) e. RR )
158	157, 143	remulcld 9072	. . . . 5 |- ( ph -> ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) e. RR )
159	155, 158	readdcld 9071	. . . 4 |- ( ph -> ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) e. RR )
160		oveq2 6048	. . . . . . . . . . . 12 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( t x. x ) = ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) )
161	160	oveq1d 6055	. . . . . . . . . . 11 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) = ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) )
162	161	fveq2d 5691	. . . . . . . . . 10 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) )
163		fveq2 5687	. . . . . . . . . . . 12 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( F ` x ) = ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) )
164	163	oveq2d 6056	. . . . . . . . . . 11 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( t x. ( F ` x ) ) = ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) )
165	164	oveq1d 6055	. . . . . . . . . 10 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
166	162, 165	breq12d 4185	. . . . . . . . 9 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) <-> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) )
167	166	imbi2d 308	. . . . . . . 8 |- ( x = ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) -> ( ( ph -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) <-> ( ph -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) ) )
168		oveq2 6048	. . . . . . . . . . . 12 |- ( y = ( X ` z ) -> ( ( 1 - t ) x. y ) = ( ( 1 - t ) x. ( X ` z ) ) )
169	168	oveq2d 6056	. . . . . . . . . . 11 |- ( y = ( X ` z ) -> ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) = ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) )
170	169	fveq2d 5691	. . . . . . . . . 10 |- ( y = ( X ` z ) -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) )
171		fveq2 5687	. . . . . . . . . . . 12 |- ( y = ( X ` z ) -> ( F ` y ) = ( F ` ( X ` z ) ) )
172	171	oveq2d 6056	. . . . . . . . . . 11 |- ( y = ( X ` z ) -> ( ( 1 - t ) x. ( F ` y ) ) = ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) )
173	172	oveq2d 6056	. . . . . . . . . 10 |- ( y = ( X ` z ) -> ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) )
174	170, 173	breq12d 4185	. . . . . . . . 9 |- ( y = ( X ` z ) -> ( ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) <-> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) ) )
175	174	imbi2d 308	. . . . . . . 8 |- ( y = ( X ` z ) -> ( ( ph -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) <-> ( ph -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) ) ) )
176		oveq1 6047	. . . . . . . . . . . 12 |- ( t = ( S / L ) -> ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) = ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) )
177		oveq2 6048	. . . . . . . . . . . . 13 |- ( t = ( S / L ) -> ( 1 - t ) = ( 1 - ( S / L ) ) )
178	177	oveq1d 6055	. . . . . . . . . . . 12 |- ( t = ( S / L ) -> ( ( 1 - t ) x. ( X ` z ) ) = ( ( 1 - ( S / L ) ) x. ( X ` z ) ) )
179	176, 178	oveq12d 6058	. . . . . . . . . . 11 |- ( t = ( S / L ) -> ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) = ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) )
180	179	fveq2d 5691	. . . . . . . . . 10 |- ( t = ( S / L ) -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) = ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) )
181		oveq1 6047	. . . . . . . . . . 11 |- ( t = ( S / L ) -> ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) = ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) )
182	177	oveq1d 6055	. . . . . . . . . . 11 |- ( t = ( S / L ) -> ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) = ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) )
183	181, 182	oveq12d 6058	. . . . . . . . . 10 |- ( t = ( S / L ) -> ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) = ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
184	180, 183	breq12d 4185	. . . . . . . . 9 |- ( t = ( S / L ) -> ( ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) <-> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) ) )
185	184	imbi2d 308	. . . . . . . 8 |- ( t = ( S / L ) -> ( ( ph -> ( F ` ( ( t x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - t ) x. ( X ` z ) ) ) ) <_ ( ( t x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - t ) x. ( F ` ( X ` z ) ) ) ) ) <-> ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) ) ) )
186	49	expcom 425	. . . . . . . 8 |- ( ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) -> ( ph -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) )
187	167, 175, 185, 186	vtocl3ga 2981	. . . . . . 7 |- ( ( ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) e. D /\ ( X ` z ) e. D /\ ( S / L ) e. ( 0 [,] 1 ) ) -> ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) ) )
188	122, 42, 135, 187	syl3anc 1184	. . . . . 6 |- ( ph -> ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) ) )
189	188	pm2.43i 45	. . . . 5 |- ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
190	116	oveq1d 6055	. . . . . . 7 |- ( ph -> ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) = ( ( ( T ` z ) / L ) x. ( F ` ( X ` z ) ) ) )
191	143	recnd 9070	. . . . . . . 8 |- ( ph -> ( F ` ( X ` z ) ) e. CC )
192	41, 191, 61, 70	div23d 9783	. . . . . . 7 |- ( ph -> ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) = ( ( ( T ` z ) / L ) x. ( F ` ( X ` z ) ) ) )
193	190, 192	eqtr4d 2439	. . . . . 6 |- ( ph -> ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) = ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) )
194	193	oveq2d 6056	. . . . 5 |- ( ph -> ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) = ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) )
195	189, 194	breqtrd 4196	. . . 4 |- ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) )
196	192, 190	eqtr4d 2439	. . . . . 6 |- ( ph -> ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) = ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) )
197	196	oveq2d 6056	. . . . 5 |- ( ph -> ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) = ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
198		jensenlem.5	. . . . . . 7 |- ( ph -> ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) )
199	55, 60, 63, 69	divgt0d 9902	. . . . . . . 8 |- ( ph -> 0 < ( S / L ) )
200		lemul2 9819	. . . . . . . 8 |- ( ( ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) e. RR /\ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) e. RR /\ ( ( S / L ) e. RR /\ 0 < ( S / L ) ) ) -> ( ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) <-> ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) <_ ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) ) )
201	141, 154, 123, 199, 200	syl112anc 1188	. . . . . . 7 |- ( ph -> ( ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) <-> ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) <_ ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) ) )
202	198, 201	mpbid 202	. . . . . 6 |- ( ph -> ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) <_ ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) )
203	142, 155, 158, 202	leadd1dd 9596	. . . . 5 |- ( ph -> ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
204	197, 203	eqbrtrd 4192	. . . 4 |- ( ph -> ( ( ( S / L ) x. ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) <_ ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
205	140, 146, 159, 195, 204	letrd 9183	. . 3 |- ( ph -> ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) <_ ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
206	121	fveq2d 5691	. . 3 |- ( ph -> ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) ) = ( F ` ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. X ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( X ` z ) ) ) ) )
207	153	recnd 9070	. . . . 5 |- ( ph -> (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) e. CC )
208	144	recnd 9070	. . . . 5 |- ( ph -> ( ( T ` z ) x. ( F ` ( X ` z ) ) ) e. CC )
209	207, 208, 61, 70	divdird 9784	. . . 4 |- ( ph -> ( ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) / L ) = ( ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / L ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) )
210	20, 77	sseldi 3306	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( T ` x ) e. RR )
211	46	ffvelrnda 5829	. . . . . . . . . . 11 |- ( ( ph /\ ( X ` x ) e. D ) -> ( F ` ( X ` x ) ) e. RR )
212	81, 211	syldan 457	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( F ` ( X ` x ) ) e. RR )
213	210, 212	remulcld 9072	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) e. RR )
214	213	recnd 9070	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) e. CC )
215	76, 214	syldan 457	. . . . . . 7 |- ( ( ph /\ x e. B ) -> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) e. CC )
216	87	fveq2d 5691	. . . . . . . 8 |- ( x = z -> ( F ` ( X ` x ) ) = ( F ` ( X ` z ) ) )
217	86, 216	oveq12d 6058	. . . . . . 7 |- ( x = z -> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) = ( ( T ` z ) x. ( F ` ( X ` z ) ) ) )
218	72, 73, 75, 9, 215, 39, 50, 208, 217	gsumunsn 15499	. . . . . 6 |- ( ph -> (ℂfld gsumg ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) ) = ( (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) )
219	46	feqmptd 5738	. . . . . . . . . . 11 |- ( ph -> F = ( y e. D |-> ( F ` y ) ) )
220		fveq2 5687	. . . . . . . . . . 11 |- ( y = ( X ` x ) -> ( F ` y ) = ( F ` ( X ` x ) ) )
221	81, 91, 219, 220	fmptco 5860	. . . . . . . . . 10 |- ( ph -> ( F o. X ) = ( x e. A |-> ( F ` ( X ` x ) ) ) )
222	5, 77, 212, 90, 221	offval2 6281	. . . . . . . . 9 |- ( ph -> ( T o F x. ( F o. X ) ) = ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
223	222	reseq1d 5104	. . . . . . . 8 |- ( ph -> ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) = ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` ( B u. { z } ) ) )
224		resmpt 5150	. . . . . . . . 9 |- ( ( B u. { z } ) C_ A -> ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
225	6, 224	syl 16	. . . . . . . 8 |- ( ph -> ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
226	223, 225	eqtrd 2436	. . . . . . 7 |- ( ph -> ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
227	226	oveq2d 6056	. . . . . 6 |- ( ph -> (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) = (ℂfld gsumg ( x e. ( B u. { z } ) |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) ) )
228	222	reseq1d 5104	. . . . . . . . 9 |- ( ph -> ( ( T o F x. ( F o. X ) ) |` B ) = ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` B ) )
229		resmpt 5150	. . . . . . . . . 10 |- ( B C_ A -> ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
230	7, 229	syl 16	. . . . . . . . 9 |- ( ph -> ( ( x e. A |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
231	228, 230	eqtrd 2436	. . . . . . . 8 |- ( ph -> ( ( T o F x. ( F o. X ) ) |` B ) = ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) )
232	231	oveq2d 6056	. . . . . . 7 |- ( ph -> (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) = (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) ) )
233	232	oveq1d 6055	. . . . . 6 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) = ( (ℂfld gsumg ( x e. B |-> ( ( T ` x ) x. ( F ` ( X ` x ) ) ) ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) )
234	218, 227, 233	3eqtr4d 2446	. . . . 5 |- ( ph -> (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) = ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) )
235	234	oveq1d 6055	. . . 4 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) = ( ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) + ( ( T ` z ) x. ( F ` ( X ` z ) ) ) ) / L ) )
236	207, 106, 61, 107, 70	dmdcand 9775	. . . . 5 |- ( ph -> ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) = ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / L ) )
237	236, 193	oveq12d 6058	. . . 4 |- ( ph -> ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) = ( ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / L ) + ( ( ( T ` z ) x. ( F ` ( X ` z ) ) ) / L ) ) )
238	209, 235, 237	3eqtr4d 2446	. . 3 |- ( ph -> ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) = ( ( ( S / L ) x. ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` B ) ) / S ) ) + ( ( 1 - ( S / L ) ) x. ( F ` ( X ` z ) ) ) ) )
239	205, 206, 238	3brtr4d 4202	. 2 |- ( ph -> ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) )
240	139, 239	jca 519	1 |- ( ph -> ( ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) e. D /\ ( F ` ( (ℂfld gsumg ( ( T o F x. X ) |` ( B u. { z } ) ) ) / L ) ) <_ ( (ℂfld gsumg ( ( T o F x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   _Vcvv 2916   \ cdif 3277   u. cun 3278   C_ wss 3280   {csn 3774   class class class wbr 4172   e. cmpt 4226   |` cres 4839   o. ccom 4841   -->wf 5409   ` cfv 5413  (class class class)co 6040   o Fcof 6262   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   +oocpnf 9073   RR*cxr 9075   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   RR+crp 10568   [,)cico 10874   [,]cicc 10875   ↾_s cress 13425   gsum_g cgsu 13679  SubGrpcsubg 14893  CMndccmn 15367   Abelcabel 15368   Ringcrg 15615   DivRingcdr 15790  SubRingcsubrg 15819  ℂ_fldccnfld 16658

This theorem is referenced by:  jensen  20780

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-rp 10569  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-grp 14767  df-minusg 14768  df-mulg 14770  df-subg 14896  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-oppr 15683  df-dvdsr 15701  df-unit 15702  df-invr 15732  df-dvr 15743  df-drng 15792  df-subrg 15821  df-cnfld 16659