Metamath Proof Explorer

Theorem hoidmvlelem1

Description: The supremum of U belongs to U . Step (c) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem1.l 
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
hoidmvlelem1.x 
|- ( ph -> X e. Fin )
hoidmvlelem1.y 
|- ( ph -> Y C_ X )
hoidmvlelem1.z 
|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem1.w 
|- W = ( Y u. { Z } )
hoidmvlelem1.a 
|- ( ph -> A : W --> RR )
hoidmvlelem1.b 
|- ( ph -> B : W --> RR )
hoidmvlelem1.c 
|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem1.d 
|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem1.r 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
hoidmvlelem1.h 
|- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
hoidmvlelem1.g 
|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
hoidmvlelem1.e 
|- ( ph -> E e. RR+ )
hoidmvlelem1.u 
|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
hoidmvlelem1.s 
|- S = sup ( U , RR , < )
hoidmvlelem1.ab 
|- ( ph -> ( A ` Z ) < ( B ` Z ) )
Assertion hoidmvlelem1 
|- ( ph -> S e. U )

Proof

Step Hyp Ref Expression
1 hoidmvlelem1.l 
 |-  L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
2 hoidmvlelem1.x 
 |-  ( ph -> X e. Fin )
3 hoidmvlelem1.y 
 |-  ( ph -> Y C_ X )
4 hoidmvlelem1.z 
 |-  ( ph -> Z e. ( X \ Y ) )
5 hoidmvlelem1.w 
 |-  W = ( Y u. { Z } )
6 hoidmvlelem1.a 
 |-  ( ph -> A : W --> RR )
7 hoidmvlelem1.b 
 |-  ( ph -> B : W --> RR )
8 hoidmvlelem1.c 
 |-  ( ph -> C : NN --> ( RR ^m W ) )
9 hoidmvlelem1.d 
 |-  ( ph -> D : NN --> ( RR ^m W ) )
10 hoidmvlelem1.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
11 hoidmvlelem1.h 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
12 hoidmvlelem1.g 
 |-  G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
13 hoidmvlelem1.e 
 |-  ( ph -> E e. RR+ )
14 hoidmvlelem1.u 
 |-  U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
15 hoidmvlelem1.s 
 |-  S = sup ( U , RR , < )
16 hoidmvlelem1.ab 
 |-  ( ph -> ( A ` Z ) < ( B ` Z ) )
17 15 a1i 
 |-  ( ph -> S = sup ( U , RR , < ) )
18 snidg 
 |-  ( Z e. ( X \ Y ) -> Z e. { Z } )
19 4 18 syl 
 |-  ( ph -> Z e. { Z } )
20 elun2 
 |-  ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
21 19 20 syl 
 |-  ( ph -> Z e. ( Y u. { Z } ) )
22 21 5 eleqtrrdi 
 |-  ( ph -> Z e. W )
23 6 22 ffvelcdmd 
 |-  ( ph -> ( A ` Z ) e. RR )
24 7 22 ffvelcdmd 
 |-  ( ph -> ( B ` Z ) e. RR )
25 ssrab2 
 |-  { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
26 14 25 eqsstri 
 |-  U C_ ( ( A ` Z ) [,] ( B ` Z ) )
27 26 a1i 
 |-  ( ph -> U C_ ( ( A ` Z ) [,] ( B ` Z ) ) )
28 23 leidd 
 |-  ( ph -> ( A ` Z ) <_ ( A ` Z ) )
29 23 24 16 ltled 
 |-  ( ph -> ( A ` Z ) <_ ( B ` Z ) )
30 23 24 23 28 29 eliccd 
 |-  ( ph -> ( A ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) )
31 23 recnd 
 |-  ( ph -> ( A ` Z ) e. CC )
32 31 subidd 
 |-  ( ph -> ( ( A ` Z ) - ( A ` Z ) ) = 0 )
33 32 oveq2d 
 |-  ( ph -> ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) = ( G x. 0 ) )
34 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
35 2 3 ssfid 
 |-  ( ph -> Y e. Fin )
36 ssun1 
 |-  Y C_ ( Y u. { Z } )
37 36 5 sseqtrri 
 |-  Y C_ W
38 37 a1i 
 |-  ( ph -> Y C_ W )
39 6 38 fssresd 
 |-  ( ph -> ( A |` Y ) : Y --> RR )
40 7 38 fssresd 
 |-  ( ph -> ( B |` Y ) : Y --> RR )
41 1 35 39 40 hoidmvcl 
 |-  ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
42 12 41 eqeltrid 
 |-  ( ph -> G e. ( 0 [,) +oo ) )
43 34 42 sselid 
 |-  ( ph -> G e. RR )
44 43 recnd 
 |-  ( ph -> G e. CC )
45 44 mul01d 
 |-  ( ph -> ( G x. 0 ) = 0 )
46 33 45 eqtrd 
 |-  ( ph -> ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) = 0 )
47 1red 
 |-  ( ph -> 1 e. RR )
48 13 rpred 
 |-  ( ph -> E e. RR )
49 47 48 readdcld 
 |-  ( ph -> ( 1 + E ) e. RR )
50 0red 
 |-  ( ph -> 0 e. RR )
51 0lt1 
 |-  0 < 1
52 51 a1i 
 |-  ( ph -> 0 < 1 )
53 47 13 ltaddrpd 
 |-  ( ph -> 1 < ( 1 + E ) )
54 50 47 49 52 53 lttrd 
 |-  ( ph -> 0 < ( 1 + E ) )
55 50 49 54 ltled 
 |-  ( ph -> 0 <_ ( 1 + E ) )
56 nnex 
 |-  NN e. _V
57 56 a1i 
 |-  ( ph -> NN e. _V )
58 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
59 snfi 
 |-  { Z } e. Fin
60 59 a1i 
 |-  ( ph -> { Z } e. Fin )
61 unfi 
 |-  ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
62 35 60 61 syl2anc 
 |-  ( ph -> ( Y u. { Z } ) e. Fin )
63 5 62 eqeltrid 
 |-  ( ph -> W e. Fin )
64 63 adantr 
 |-  ( ( ph /\ j e. NN ) -> W e. Fin )
65 8 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
66 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
67 65 66 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
68 eleq1w 
 |-  ( j = h -> ( j e. Y <-> h e. Y ) )
69 fveq2 
 |-  ( j = h -> ( c ` j ) = ( c ` h ) )
70 69 breq1d 
 |-  ( j = h -> ( ( c ` j ) <_ x <-> ( c ` h ) <_ x ) )
71 70 69 ifbieq1d 
 |-  ( j = h -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` h ) <_ x , ( c ` h ) , x ) )
72 68 69 71 ifbieq12d 
 |-  ( j = h -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
73 72 cbvmptv 
 |-  ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
74 73 mpteq2i 
 |-  ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) = ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) )
75 74 mpteq2i 
 |-  ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
76 11 75 eqtri 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
77 23 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( A ` Z ) e. RR )
78 9 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
79 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
80 78 79 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
81 76 77 64 80 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) : W --> RR )
82 1 64 67 81 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
83 58 82 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
84 83 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) : NN --> ( 0 [,] +oo ) )
85 57 84 sge0cl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
86 57 84 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR* )
87 pnfxr 
 |-  +oo e. RR*
88 87 a1i 
 |-  ( ph -> +oo e. RR* )
89 10 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
90 nfv 
 |-  F/ j ph
91 1 64 67 80 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,) +oo ) )
92 58 91 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
93 4 eldifbd 
 |-  ( ph -> -. Z e. Y )
94 22 93 eldifd 
 |-  ( ph -> Z e. ( W \ Y ) )
95 94 adantr 
 |-  ( ( ph /\ j e. NN ) -> Z e. ( W \ Y ) )
96 1 64 95 5 77 76 67 80 hsphoidmvle 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
97 90 57 83 92 96 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
98 10 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
99 86 89 88 97 98 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) < +oo )
100 86 88 99 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) =/= +oo )
101 ge0xrre 
 |-  ( ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) =/= +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR )
102 85 100 101 syl2anc 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR )
103 57 84 sge0ge0 
 |-  ( ph -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) )
104 mulge0 
 |-  ( ( ( ( 1 + E ) e. RR /\ 0 <_ ( 1 + E ) ) /\ ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR /\ 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) -> 0 <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
105 49 55 102 103 104 syl22anc 
 |-  ( ph -> 0 <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
106 46 105 eqbrtrd 
 |-  ( ph -> ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
107 30 106 jca 
 |-  ( ph -> ( ( A ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
108 oveq1 
 |-  ( z = ( A ` Z ) -> ( z - ( A ` Z ) ) = ( ( A ` Z ) - ( A ` Z ) ) )
109 108 oveq2d 
 |-  ( z = ( A ` Z ) -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) )
110 fveq2 
 |-  ( z = ( A ` Z ) -> ( H ` z ) = ( H ` ( A ` Z ) ) )
111 110 fveq1d 
 |-  ( z = ( A ` Z ) -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) )
112 111 oveq2d 
 |-  ( z = ( A ` Z ) -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) )
113 112 mpteq2dv 
 |-  ( z = ( A ` Z ) -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) )
114 113 fveq2d 
 |-  ( z = ( A ` Z ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) )
115 114 oveq2d 
 |-  ( z = ( A ` Z ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
116 109 115 breq12d 
 |-  ( z = ( A ` Z ) -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
117 116 elrab 
 |-  ( ( A ` Z ) e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> ( ( A ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( ( A ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( A ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
118 107 117 sylibr 
 |-  ( ph -> ( A ` Z ) e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
119 118 14 eleqtrrdi 
 |-  ( ph -> ( A ` Z ) e. U )
120 ne0i 
 |-  ( ( A ` Z ) e. U -> U =/= (/) )
121 119 120 syl 
 |-  ( ph -> U =/= (/) )
122 23 24 27 121 supicc 
 |-  ( ph -> sup ( U , RR , < ) e. ( ( A ` Z ) [,] ( B ` Z ) ) )
123 17 122 eqeltrd 
 |-  ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
124 17 oveq1d 
 |-  ( ph -> ( S - ( A ` Z ) ) = ( sup ( U , RR , < ) - ( A ` Z ) ) )
125 124 oveq2d 
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) = ( G x. ( sup ( U , RR , < ) - ( A ` Z ) ) ) )
126 23 24 iccssred 
 |-  ( ph -> ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR )
127 27 126 sstrd 
 |-  ( ph -> U C_ RR )
128 23 24 jca 
 |-  ( ph -> ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) )
129 iccsupr 
 |-  ( ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) /\ U C_ ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( A ` Z ) e. U ) -> ( U C_ RR /\ U =/= (/) /\ E. y e. RR A. z e. U z <_ y ) )
130 128 27 119 129 syl3anc 
 |-  ( ph -> ( U C_ RR /\ U =/= (/) /\ E. y e. RR A. z e. U z <_ y ) )
131 130 simp3d 
 |-  ( ph -> E. y e. RR A. z e. U z <_ y )
132 eqid 
 |-  { w | E. u e. U w = ( u - ( A ` Z ) ) } = { w | E. u e. U w = ( u - ( A ` Z ) ) }
133 127 121 131 23 132 supsubc 
 |-  ( ph -> ( sup ( U , RR , < ) - ( A ` Z ) ) = sup ( { w | E. u e. U w = ( u - ( A ` Z ) ) } , RR , < ) )
134 133 oveq2d 
 |-  ( ph -> ( G x. ( sup ( U , RR , < ) - ( A ` Z ) ) ) = ( G x. sup ( { w | E. u e. U w = ( u - ( A ` Z ) ) } , RR , < ) ) )
135 50 rexrd 
 |-  ( ph -> 0 e. RR* )
136 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ G e. ( 0 [,) +oo ) ) -> 0 <_ G )
137 135 88 42 136 syl3anc 
 |-  ( ph -> 0 <_ G )
138 vex 
 |-  r e. _V
139 eqeq1 
 |-  ( w = r -> ( w = ( u - ( A ` Z ) ) <-> r = ( u - ( A ` Z ) ) ) )
140 139 rexbidv 
 |-  ( w = r -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U r = ( u - ( A ` Z ) ) ) )
141 138 140 elab 
 |-  ( r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } <-> E. u e. U r = ( u - ( A ` Z ) ) )
142 141 biimpi 
 |-  ( r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> E. u e. U r = ( u - ( A ` Z ) ) )
143 142 adantl 
 |-  ( ( ph /\ r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> E. u e. U r = ( u - ( A ` Z ) ) )
144 nfv 
 |-  F/ u ph
145 nfcv 
 |-  F/_ u r
146 nfre1 
 |-  F/ u E. u e. U w = ( u - ( A ` Z ) )
147 146 nfab 
 |-  F/_ u { w | E. u e. U w = ( u - ( A ` Z ) ) }
148 145 147 nfel 
 |-  F/ u r e. { w | E. u e. U w = ( u - ( A ` Z ) ) }
149 144 148 nfan 
 |-  F/ u ( ph /\ r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } )
150 nfv 
 |-  F/ u 0 <_ r
151 23 rexrd 
 |-  ( ph -> ( A ` Z ) e. RR* )
152 151 adantr 
 |-  ( ( ph /\ u e. U ) -> ( A ` Z ) e. RR* )
153 24 rexrd 
 |-  ( ph -> ( B ` Z ) e. RR* )
154 153 adantr 
 |-  ( ( ph /\ u e. U ) -> ( B ` Z ) e. RR* )
155 27 sselda 
 |-  ( ( ph /\ u e. U ) -> u e. ( ( A ` Z ) [,] ( B ` Z ) ) )
156 iccgelb 
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ u e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ u )
157 152 154 155 156 syl3anc 
 |-  ( ( ph /\ u e. U ) -> ( A ` Z ) <_ u )
158 127 sselda 
 |-  ( ( ph /\ u e. U ) -> u e. RR )
159 23 adantr 
 |-  ( ( ph /\ u e. U ) -> ( A ` Z ) e. RR )
160 158 159 subge0d 
 |-  ( ( ph /\ u e. U ) -> ( 0 <_ ( u - ( A ` Z ) ) <-> ( A ` Z ) <_ u ) )
161 157 160 mpbird 
 |-  ( ( ph /\ u e. U ) -> 0 <_ ( u - ( A ` Z ) ) )
162 161 3adant3 
 |-  ( ( ph /\ u e. U /\ r = ( u - ( A ` Z ) ) ) -> 0 <_ ( u - ( A ` Z ) ) )
163 id 
 |-  ( r = ( u - ( A ` Z ) ) -> r = ( u - ( A ` Z ) ) )
164 163 eqcomd 
 |-  ( r = ( u - ( A ` Z ) ) -> ( u - ( A ` Z ) ) = r )
165 164 3ad2ant3 
 |-  ( ( ph /\ u e. U /\ r = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) = r )
166 162 165 breqtrd 
 |-  ( ( ph /\ u e. U /\ r = ( u - ( A ` Z ) ) ) -> 0 <_ r )
167 166 3exp 
 |-  ( ph -> ( u e. U -> ( r = ( u - ( A ` Z ) ) -> 0 <_ r ) ) )
168 167 adantr 
 |-  ( ( ph /\ r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( u e. U -> ( r = ( u - ( A ` Z ) ) -> 0 <_ r ) ) )
169 149 150 168 rexlimd 
 |-  ( ( ph /\ r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( E. u e. U r = ( u - ( A ` Z ) ) -> 0 <_ r ) )
170 143 169 mpd 
 |-  ( ( ph /\ r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> 0 <_ r )
171 170 ralrimiva 
 |-  ( ph -> A. r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 <_ r )
172 simp3 
 |-  ( ( ph /\ u e. U /\ w = ( u - ( A ` Z ) ) ) -> w = ( u - ( A ` Z ) ) )
173 158 159 resubcld 
 |-  ( ( ph /\ u e. U ) -> ( u - ( A ` Z ) ) e. RR )
174 173 3adant3 
 |-  ( ( ph /\ u e. U /\ w = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) e. RR )
175 172 174 eqeltrd 
 |-  ( ( ph /\ u e. U /\ w = ( u - ( A ` Z ) ) ) -> w e. RR )
176 175 3exp 
 |-  ( ph -> ( u e. U -> ( w = ( u - ( A ` Z ) ) -> w e. RR ) ) )
177 176 rexlimdv 
 |-  ( ph -> ( E. u e. U w = ( u - ( A ` Z ) ) -> w e. RR ) )
178 177 abssdv 
 |-  ( ph -> { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR )
179 32 eqcomd 
 |-  ( ph -> 0 = ( ( A ` Z ) - ( A ` Z ) ) )
180 oveq1 
 |-  ( u = ( A ` Z ) -> ( u - ( A ` Z ) ) = ( ( A ` Z ) - ( A ` Z ) ) )
181 180 rspceeqv 
 |-  ( ( ( A ` Z ) e. U /\ 0 = ( ( A ` Z ) - ( A ` Z ) ) ) -> E. u e. U 0 = ( u - ( A ` Z ) ) )
182 119 179 181 syl2anc 
 |-  ( ph -> E. u e. U 0 = ( u - ( A ` Z ) ) )
183 eqeq1 
 |-  ( w = 0 -> ( w = ( u - ( A ` Z ) ) <-> 0 = ( u - ( A ` Z ) ) ) )
184 183 rexbidv 
 |-  ( w = 0 -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U 0 = ( u - ( A ` Z ) ) ) )
185 50 182 184 elabd 
 |-  ( ph -> 0 e. { w | E. u e. U w = ( u - ( A ` Z ) ) } )
186 ne0i 
 |-  ( 0 e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) )
187 185 186 syl 
 |-  ( ph -> { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) )
188 24 23 resubcld 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) e. RR )
189 vex 
 |-  s e. _V
190 eqeq1 
 |-  ( w = s -> ( w = ( u - ( A ` Z ) ) <-> s = ( u - ( A ` Z ) ) ) )
191 190 rexbidv 
 |-  ( w = s -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U s = ( u - ( A ` Z ) ) ) )
192 189 191 elab 
 |-  ( s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } <-> E. u e. U s = ( u - ( A ` Z ) ) )
193 192 biimpi 
 |-  ( s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> E. u e. U s = ( u - ( A ` Z ) ) )
194 193 adantl 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> E. u e. U s = ( u - ( A ` Z ) ) )
195 nfcv 
 |-  F/_ u s
196 195 147 nfel 
 |-  F/ u s e. { w | E. u e. U w = ( u - ( A ` Z ) ) }
197 144 196 nfan 
 |-  F/ u ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } )
198 nfv 
 |-  F/ u s <_ ( ( B ` Z ) - ( A ` Z ) )
199 simp3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> s = ( u - ( A ` Z ) ) )
200 159 3adant3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( A ` Z ) e. RR )
201 24 3ad2ant1 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( B ` Z ) e. RR )
202 155 3adant3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> u e. ( ( A ` Z ) [,] ( B ` Z ) ) )
203 30 3ad2ant1 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( A ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) )
204 200 201 202 203 iccsuble 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) <_ ( ( B ` Z ) - ( A ` Z ) ) )
205 199 204 eqbrtrd 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) )
206 205 3exp 
 |-  ( ph -> ( u e. U -> ( s = ( u - ( A ` Z ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) ) ) )
207 206 adantr 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( u e. U -> ( s = ( u - ( A ` Z ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) ) ) )
208 197 198 207 rexlimd 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( E. u e. U s = ( u - ( A ` Z ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) ) )
209 194 208 mpd 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) )
210 209 ralrimiva 
 |-  ( ph -> A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ ( ( B ` Z ) - ( A ` Z ) ) )
211 brralrspcev 
 |-  ( ( ( ( B ` Z ) - ( A ` Z ) ) e. RR /\ A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ ( ( B ` Z ) - ( A ` Z ) ) ) -> E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r )
212 188 210 211 syl2anc 
 |-  ( ph -> E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r )
213 eqid 
 |-  { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } = { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) }
214 biid 
 |-  ( ( ( G e. RR /\ 0 <_ G /\ A. r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 <_ r ) /\ ( { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR /\ { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) /\ E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r ) ) <-> ( ( G e. RR /\ 0 <_ G /\ A. r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 <_ r ) /\ ( { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR /\ { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) /\ E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r ) ) )
215 213 214 supmul1 
 |-  ( ( ( G e. RR /\ 0 <_ G /\ A. r e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 <_ r ) /\ ( { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR /\ { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) /\ E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r ) ) -> ( G x. sup ( { w | E. u e. U w = ( u - ( A ` Z ) ) } , RR , < ) ) = sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) )
216 43 137 171 178 187 212 215 syl33anc 
 |-  ( ph -> ( G x. sup ( { w | E. u e. U w = ( u - ( A ` Z ) ) } , RR , < ) ) = sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) )
217 125 134 216 3eqtrd 
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) = sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) )
218 vex 
 |-  c e. _V
219 eqeq1 
 |-  ( v = c -> ( v = ( G x. t ) <-> c = ( G x. t ) ) )
220 219 rexbidv 
 |-  ( v = c -> ( E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) <-> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) ) )
221 218 220 elab 
 |-  ( c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } <-> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) )
222 221 biimpi 
 |-  ( c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } -> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) )
223 nfv 
 |-  F/ t E. u e. U c = ( G x. ( u - ( A ` Z ) ) )
224 vex 
 |-  t e. _V
225 eqeq1 
 |-  ( w = t -> ( w = ( u - ( A ` Z ) ) <-> t = ( u - ( A ` Z ) ) ) )
226 225 rexbidv 
 |-  ( w = t -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U t = ( u - ( A ` Z ) ) ) )
227 224 226 elab 
 |-  ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } <-> E. u e. U t = ( u - ( A ` Z ) ) )
228 227 biimpi 
 |-  ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> E. u e. U t = ( u - ( A ` Z ) ) )
229 228 adantr 
 |-  ( ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } /\ c = ( G x. t ) ) -> E. u e. U t = ( u - ( A ` Z ) ) )
230 simpl 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> c = ( G x. t ) )
231 oveq2 
 |-  ( t = ( u - ( A ` Z ) ) -> ( G x. t ) = ( G x. ( u - ( A ` Z ) ) ) )
232 231 adantl 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> ( G x. t ) = ( G x. ( u - ( A ` Z ) ) ) )
233 230 232 eqtrd 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) )
234 233 ex 
 |-  ( c = ( G x. t ) -> ( t = ( u - ( A ` Z ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) ) )
235 234 reximdv 
 |-  ( c = ( G x. t ) -> ( E. u e. U t = ( u - ( A ` Z ) ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) ) )
236 235 adantl 
 |-  ( ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } /\ c = ( G x. t ) ) -> ( E. u e. U t = ( u - ( A ` Z ) ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) ) )
237 229 236 mpd 
 |-  ( ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } /\ c = ( G x. t ) ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) )
238 237 ex 
 |-  ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> ( c = ( G x. t ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) ) )
239 223 238 rexlimi 
 |-  ( E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) )
240 222 239 syl 
 |-  ( c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) )
241 240 adantl 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) )
242 simp3 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) )
243 43 adantr 
 |-  ( ( ph /\ u e. U ) -> G e. RR )
244 243 173 remulcld 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) e. RR )
245 49 adantr 
 |-  ( ( ph /\ u e. U ) -> ( 1 + E ) e. RR )
246 56 a1i 
 |-  ( ( ph /\ u e. U ) -> NN e. _V )
247 64 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> W e. Fin )
248 67 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( C ` j ) : W --> RR )
249 158 adantr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> u e. RR )
250 80 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( D ` j ) : W --> RR )
251 76 249 247 250 hsphoif 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( H ` u ) ` ( D ` j ) ) : W --> RR )
252 1 247 248 251 hoidmvcl 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
253 58 252 sselid 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
254 253 fmpttd 
 |-  ( ( ph /\ u e. U ) -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) : NN --> ( 0 [,] +oo ) )
255 246 254 sge0cl 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
256 246 254 sge0xrcl 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. RR* )
257 87 a1i 
 |-  ( ( ph /\ u e. U ) -> +oo e. RR* )
258 89 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
259 nfv 
 |-  F/ j ( ph /\ u e. U )
260 92 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
261 95 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> Z e. ( W \ Y ) )
262 1 247 261 5 249 76 248 250 hsphoidmvle 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
263 259 246 253 260 262 sge0lempt 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
264 98 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
265 256 258 257 263 264 xrlelttrd 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) < +oo )
266 256 257 265 xrltned 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) =/= +oo )
267 ge0xrre 
 |-  ( ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) =/= +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. RR )
268 255 266 267 syl2anc 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. RR )
269 245 268 remulcld 
 |-  ( ( ph /\ u e. U ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) e. RR )
270 126 123 sseldd 
 |-  ( ph -> S e. RR )
271 1 35 94 5 8 9 10 11 270 sge0hsphoire 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
272 49 271 remulcld 
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
273 272 adantr 
 |-  ( ( ph /\ u e. U ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
274 14 eleq2i 
 |-  ( u e. U <-> u e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
275 274 biimpi 
 |-  ( u e. U -> u e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
276 oveq1 
 |-  ( z = u -> ( z - ( A ` Z ) ) = ( u - ( A ` Z ) ) )
277 276 oveq2d 
 |-  ( z = u -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( u - ( A ` Z ) ) ) )
278 fveq2 
 |-  ( z = u -> ( H ` z ) = ( H ` u ) )
279 278 fveq1d 
 |-  ( z = u -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` u ) ` ( D ` j ) ) )
280 279 oveq2d 
 |-  ( z = u -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) )
281 280 mpteq2dv 
 |-  ( z = u -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) )
282 281 fveq2d 
 |-  ( z = u -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) )
283 282 oveq2d 
 |-  ( z = u -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) )
284 277 283 breq12d 
 |-  ( z = u -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) ) )
285 284 elrab 
 |-  ( u e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> ( u e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) ) )
286 275 285 sylib 
 |-  ( u e. U -> ( u e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) ) )
287 286 simprd 
 |-  ( u e. U -> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) )
288 287 adantl 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) )
289 271 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
290 55 adantr 
 |-  ( ( ph /\ u e. U ) -> 0 <_ ( 1 + E ) )
291 270 adantr 
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
292 76 291 64 80 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
293 1 64 67 292 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
294 58 293 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
295 294 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
296 291 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> S e. RR )
297 127 adantr 
 |-  ( ( ph /\ u e. U ) -> U C_ RR )
298 121 adantr 
 |-  ( ( ph /\ u e. U ) -> U =/= (/) )
299 131 adantr 
 |-  ( ( ph /\ u e. U ) -> E. y e. RR A. z e. U z <_ y )
300 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
301 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. y e. RR A. z e. U z <_ y ) /\ u e. U ) -> u <_ sup ( U , RR , < ) )
302 297 298 299 300 301 syl31anc 
 |-  ( ( ph /\ u e. U ) -> u <_ sup ( U , RR , < ) )
303 302 15 breqtrrdi 
 |-  ( ( ph /\ u e. U ) -> u <_ S )
304 303 adantr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> u <_ S )
305 1 247 261 5 249 296 304 76 248 250 hsphoidmvle2 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
306 259 246 253 295 305 sge0lempt 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
307 268 289 245 290 306 lemul2ad 
 |-  ( ( ph /\ u e. U ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
308 244 269 273 288 307 letrd 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
309 308 3adant3 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
310 242 309 eqbrtrd 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
311 310 3exp 
 |-  ( ph -> ( u e. U -> ( c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) ) )
312 311 rexlimdv 
 |-  ( ph -> ( E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
313 312 adantr 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> ( E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
314 241 313 mpd 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
315 314 ralrimiva 
 |-  ( ph -> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
316 222 adantl 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) )
317 nfv 
 |-  F/ t ph
318 nfcv 
 |-  F/_ t c
319 nfre1 
 |-  F/ t E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t )
320 319 nfab 
 |-  F/_ t { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) }
321 318 320 nfel 
 |-  F/ t c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) }
322 317 321 nfan 
 |-  F/ t ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } )
323 nfv 
 |-  F/ t c e. RR
324 228 adantl 
 |-  ( ( ph /\ t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> E. u e. U t = ( u - ( A ` Z ) ) )
325 simpr 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> c = ( G x. t ) )
326 243 3adant3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> G e. RR )
327 simp3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> t = ( u - ( A ` Z ) ) )
328 173 3adant3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) e. RR )
329 327 328 eqeltrd 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> t e. RR )
330 326 329 remulcld 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( G x. t ) e. RR )
331 330 adantr 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> ( G x. t ) e. RR )
332 325 331 eqeltrd 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> c e. RR )
333 332 ex 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( c = ( G x. t ) -> c e. RR ) )
334 333 3exp 
 |-  ( ph -> ( u e. U -> ( t = ( u - ( A ` Z ) ) -> ( c = ( G x. t ) -> c e. RR ) ) ) )
335 334 rexlimdv 
 |-  ( ph -> ( E. u e. U t = ( u - ( A ` Z ) ) -> ( c = ( G x. t ) -> c e. RR ) ) )
336 335 adantr 
 |-  ( ( ph /\ t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( E. u e. U t = ( u - ( A ` Z ) ) -> ( c = ( G x. t ) -> c e. RR ) ) )
337 324 336 mpd 
 |-  ( ( ph /\ t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( c = ( G x. t ) -> c e. RR ) )
338 337 ex 
 |-  ( ph -> ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> ( c = ( G x. t ) -> c e. RR ) ) )
339 338 adantr 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> ( c = ( G x. t ) -> c e. RR ) ) )
340 322 323 339 rexlimd 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> ( E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } c = ( G x. t ) -> c e. RR ) )
341 316 340 mpd 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> c e. RR )
342 341 ralrimiva 
 |-  ( ph -> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c e. RR )
343 dfss3 
 |-  ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } C_ RR <-> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c e. RR )
344 342 343 sylibr 
 |-  ( ph -> { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } C_ RR )
345 45 eqcomd 
 |-  ( ph -> 0 = ( G x. 0 ) )
346 oveq2 
 |-  ( t = 0 -> ( G x. t ) = ( G x. 0 ) )
347 346 rspceeqv 
 |-  ( ( 0 e. { w | E. u e. U w = ( u - ( A ` Z ) ) } /\ 0 = ( G x. 0 ) ) -> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 = ( G x. t ) )
348 185 345 347 syl2anc 
 |-  ( ph -> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 = ( G x. t ) )
349 eqeq1 
 |-  ( v = 0 -> ( v = ( G x. t ) <-> 0 = ( G x. t ) ) )
350 349 rexbidv 
 |-  ( v = 0 -> ( E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) <-> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 = ( G x. t ) ) )
351 50 348 350 elabd 
 |-  ( ph -> 0 e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } )
352 ne0i 
 |-  ( 0 e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } -> { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } =/= (/) )
353 351 352 syl 
 |-  ( ph -> { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } =/= (/) )
354 43 188 remulcld 
 |-  ( ph -> ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) e. RR )
355 188 adantr 
 |-  ( ( ph /\ u e. U ) -> ( ( B ` Z ) - ( A ` Z ) ) e. RR )
356 137 adantr 
 |-  ( ( ph /\ u e. U ) -> 0 <_ G )
357 24 adantr 
 |-  ( ( ph /\ u e. U ) -> ( B ` Z ) e. RR )
358 iccleub 
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ u e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> u <_ ( B ` Z ) )
359 152 154 155 358 syl3anc 
 |-  ( ( ph /\ u e. U ) -> u <_ ( B ` Z ) )
360 158 357 159 359 lesub1dd 
 |-  ( ( ph /\ u e. U ) -> ( u - ( A ` Z ) ) <_ ( ( B ` Z ) - ( A ` Z ) ) )
361 173 355 243 356 360 lemul2ad 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
362 361 3adant3 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
363 242 362 eqbrtrd 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
364 363 3exp 
 |-  ( ph -> ( u e. U -> ( c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) ) )
365 364 rexlimdv 
 |-  ( ph -> ( E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) )
366 365 adantr 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> ( E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) )
367 241 366 mpd 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
368 367 ralrimiva 
 |-  ( ph -> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
369 brralrspcev 
 |-  ( ( ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) e. RR /\ A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) -> E. y e. RR A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ y )
370 354 368 369 syl2anc 
 |-  ( ph -> E. y e. RR A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ y )
371 suprleub 
 |-  ( ( ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } C_ RR /\ { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } =/= (/) /\ E. y e. RR A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ y ) /\ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR ) -> ( sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) <-> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
372 344 353 370 272 371 syl31anc 
 |-  ( ph -> ( sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) <-> A. c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } c <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
373 315 372 mpbird 
 |-  ( ph -> sup ( { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } , RR , < ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
374 217 373 eqbrtrd 
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
375 123 374 jca 
 |-  ( ph -> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
376 oveq1 
 |-  ( z = S -> ( z - ( A ` Z ) ) = ( S - ( A ` Z ) ) )
377 376 oveq2d 
 |-  ( z = S -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( S - ( A ` Z ) ) ) )
378 fveq2 
 |-  ( z = S -> ( H ` z ) = ( H ` S ) )
379 378 fveq1d 
 |-  ( z = S -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` S ) ` ( D ` j ) ) )
380 379 oveq2d 
 |-  ( z = S -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
381 380 mpteq2dv 
 |-  ( z = S -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
382 381 fveq2d 
 |-  ( z = S -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
383 382 oveq2d 
 |-  ( z = S -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
384 377 383 breq12d 
 |-  ( z = S -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
385 384 elrab 
 |-  ( S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
386 375 385 sylibr 
 |-  ( ph -> S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
387 386 14 eleqtrrdi 
 |-  ( ph -> S e. U )