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 ffvelrnd 
 |-  ( ph -> ( A ` Z ) e. RR )
24 7 22 ffvelrnd 
 |-  ( 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 ffvelrnda 
 |-  ( ( 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 ffvelrnda 
 |-  ( ( 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 alrimiv 
 |-  ( ph -> A. w ( E. u e. U w = ( u - ( A ` Z ) ) -> w e. RR ) )
179 abss 
 |-  ( { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR <-> A. w ( E. u e. U w = ( u - ( A ` Z ) ) -> w e. RR ) )
180 178 179 sylibr 
 |-  ( ph -> { w | E. u e. U w = ( u - ( A ` Z ) ) } C_ RR )
181 32 eqcomd 
 |-  ( ph -> 0 = ( ( A ` Z ) - ( A ` Z ) ) )
182 oveq1 
 |-  ( u = ( A ` Z ) -> ( u - ( A ` Z ) ) = ( ( A ` Z ) - ( A ` Z ) ) )
183 182 rspceeqv 
 |-  ( ( ( A ` Z ) e. U /\ 0 = ( ( A ` Z ) - ( A ` Z ) ) ) -> E. u e. U 0 = ( u - ( A ` Z ) ) )
184 119 181 183 syl2anc 
 |-  ( ph -> E. u e. U 0 = ( u - ( A ` Z ) ) )
185 eqeq1 
 |-  ( w = 0 -> ( w = ( u - ( A ` Z ) ) <-> 0 = ( u - ( A ` Z ) ) ) )
186 185 rexbidv 
 |-  ( w = 0 -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U 0 = ( u - ( A ` Z ) ) ) )
187 50 184 186 elabd 
 |-  ( ph -> 0 e. { w | E. u e. U w = ( u - ( A ` Z ) ) } )
188 ne0i 
 |-  ( 0 e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) )
189 187 188 syl 
 |-  ( ph -> { w | E. u e. U w = ( u - ( A ` Z ) ) } =/= (/) )
190 24 23 resubcld 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) e. RR )
191 vex 
 |-  s e. _V
192 eqeq1 
 |-  ( w = s -> ( w = ( u - ( A ` Z ) ) <-> s = ( u - ( A ` Z ) ) ) )
193 192 rexbidv 
 |-  ( w = s -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U s = ( u - ( A ` Z ) ) ) )
194 191 193 elab 
 |-  ( s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } <-> E. u e. U s = ( u - ( A ` Z ) ) )
195 194 biimpi 
 |-  ( s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> E. u e. U s = ( u - ( A ` Z ) ) )
196 195 adantl 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> E. u e. U s = ( u - ( A ` Z ) ) )
197 nfcv 
 |-  F/_ u s
198 197 147 nfel 
 |-  F/ u s e. { w | E. u e. U w = ( u - ( A ` Z ) ) }
199 144 198 nfan 
 |-  F/ u ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } )
200 nfv 
 |-  F/ u s <_ ( ( B ` Z ) - ( A ` Z ) )
201 simp3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> s = ( u - ( A ` Z ) ) )
202 159 3adant3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( A ` Z ) e. RR )
203 24 3ad2ant1 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( B ` Z ) e. RR )
204 155 3adant3 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> u e. ( ( A ` Z ) [,] ( B ` Z ) ) )
205 30 3ad2ant1 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( A ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) )
206 202 203 204 205 iccsuble 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) <_ ( ( B ` Z ) - ( A ` Z ) ) )
207 201 206 eqbrtrd 
 |-  ( ( ph /\ u e. U /\ s = ( u - ( A ` Z ) ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) )
208 207 3exp 
 |-  ( ph -> ( u e. U -> ( s = ( u - ( A ` Z ) ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) ) ) )
209 208 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 ) ) ) ) )
210 199 200 209 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 ) ) ) )
211 196 210 mpd 
 |-  ( ( ph /\ s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> s <_ ( ( B ` Z ) - ( A ` Z ) ) )
212 211 ralrimiva 
 |-  ( ph -> A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ ( ( B ` Z ) - ( A ` Z ) ) )
213 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 )
214 190 212 213 syl2anc 
 |-  ( ph -> E. r e. RR A. s e. { w | E. u e. U w = ( u - ( A ` Z ) ) } s <_ r )
215 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 ) }
216 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 ) ) )
217 215 216 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 , < ) )
218 43 137 171 180 189 214 217 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 , < ) )
219 125 134 218 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 , < ) )
220 vex 
 |-  c e. _V
221 eqeq1 
 |-  ( v = c -> ( v = ( G x. t ) <-> c = ( G x. t ) ) )
222 221 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 ) ) )
223 220 222 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 ) )
224 223 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 ) )
225 nfv 
 |-  F/ t E. u e. U c = ( G x. ( u - ( A ` Z ) ) )
226 vex 
 |-  t e. _V
227 eqeq1 
 |-  ( w = t -> ( w = ( u - ( A ` Z ) ) <-> t = ( u - ( A ` Z ) ) ) )
228 227 rexbidv 
 |-  ( w = t -> ( E. u e. U w = ( u - ( A ` Z ) ) <-> E. u e. U t = ( u - ( A ` Z ) ) ) )
229 226 228 elab 
 |-  ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } <-> E. u e. U t = ( u - ( A ` Z ) ) )
230 229 biimpi 
 |-  ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> E. u e. U t = ( u - ( A ` Z ) ) )
231 230 adantr 
 |-  ( ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } /\ c = ( G x. t ) ) -> E. u e. U t = ( u - ( A ` Z ) ) )
232 simpl 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> c = ( G x. t ) )
233 oveq2 
 |-  ( t = ( u - ( A ` Z ) ) -> ( G x. t ) = ( G x. ( u - ( A ` Z ) ) ) )
234 233 adantl 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> ( G x. t ) = ( G x. ( u - ( A ` Z ) ) ) )
235 232 234 eqtrd 
 |-  ( ( c = ( G x. t ) /\ t = ( u - ( A ` Z ) ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) )
236 235 ex 
 |-  ( c = ( G x. t ) -> ( t = ( u - ( A ` Z ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) ) )
237 236 reximdv 
 |-  ( c = ( G x. t ) -> ( E. u e. U t = ( u - ( A ` Z ) ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) ) )
238 237 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 ) ) ) ) )
239 231 238 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 ) ) ) )
240 239 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 ) ) ) ) )
241 225 240 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 ) ) ) )
242 241 a1i 
 |-  ( 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 ) -> E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) ) )
243 224 242 mpd 
 |-  ( 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 ) ) ) )
244 243 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 ) ) ) )
245 simp3 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> c = ( G x. ( u - ( A ` Z ) ) ) )
246 43 adantr 
 |-  ( ( ph /\ u e. U ) -> G e. RR )
247 246 173 remulcld 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) e. RR )
248 49 adantr 
 |-  ( ( ph /\ u e. U ) -> ( 1 + E ) e. RR )
249 56 a1i 
 |-  ( ( ph /\ u e. U ) -> NN e. _V )
250 64 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> W e. Fin )
251 67 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( C ` j ) : W --> RR )
252 158 adantr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> u e. RR )
253 80 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( D ` j ) : W --> RR )
254 76 252 250 253 hsphoif 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( H ` u ) ` ( D ` j ) ) : W --> RR )
255 1 250 251 254 hoidmvcl 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
256 58 255 sselid 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
257 256 fmpttd 
 |-  ( ( ph /\ u e. U ) -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) : NN --> ( 0 [,] +oo ) )
258 249 257 sge0cl 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
259 249 257 sge0xrcl 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. RR* )
260 87 a1i 
 |-  ( ( ph /\ u e. U ) -> +oo e. RR* )
261 89 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
262 nfv 
 |-  F/ j ( ph /\ u e. U )
263 92 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
264 95 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> Z e. ( W \ Y ) )
265 1 250 264 5 252 76 251 253 hsphoidmvle 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
266 262 249 256 263 265 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 ) ) ) ) )
267 98 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
268 259 261 260 266 267 xrlelttrd 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) < +oo )
269 259 260 268 xrltned 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) =/= +oo )
270 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 )
271 258 269 270 syl2anc 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) e. RR )
272 248 271 remulcld 
 |-  ( ( ph /\ u e. U ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) e. RR )
273 126 123 sseldd 
 |-  ( ph -> S e. RR )
274 1 35 94 5 8 9 10 11 273 sge0hsphoire 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
275 49 274 remulcld 
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
276 275 adantr 
 |-  ( ( ph /\ u e. U ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
277 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 ) ) ) ) ) ) } )
278 277 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 ) ) ) ) ) ) } )
279 oveq1 
 |-  ( z = u -> ( z - ( A ` Z ) ) = ( u - ( A ` Z ) ) )
280 279 oveq2d 
 |-  ( z = u -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( u - ( A ` Z ) ) ) )
281 fveq2 
 |-  ( z = u -> ( H ` z ) = ( H ` u ) )
282 281 fveq1d 
 |-  ( z = u -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` u ) ` ( D ` j ) ) )
283 282 oveq2d 
 |-  ( z = u -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) )
284 283 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 ) ) ) ) )
285 284 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 ) ) ) ) ) )
286 285 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 ) ) ) ) ) ) )
287 280 286 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 ) ) ) ) ) ) ) )
288 287 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 ) ) ) ) ) ) ) )
289 278 288 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 ) ) ) ) ) ) ) )
290 289 simprd 
 |-  ( u e. U -> ( G x. ( u - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) ) ) ) )
291 290 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 ) ) ) ) ) ) )
292 274 adantr 
 |-  ( ( ph /\ u e. U ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
293 55 adantr 
 |-  ( ( ph /\ u e. U ) -> 0 <_ ( 1 + E ) )
294 273 adantr 
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
295 76 294 64 80 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
296 1 64 67 295 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
297 58 296 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
298 297 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
299 294 adantlr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> S e. RR )
300 127 adantr 
 |-  ( ( ph /\ u e. U ) -> U C_ RR )
301 121 adantr 
 |-  ( ( ph /\ u e. U ) -> U =/= (/) )
302 131 adantr 
 |-  ( ( ph /\ u e. U ) -> E. y e. RR A. z e. U z <_ y )
303 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
304 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. y e. RR A. z e. U z <_ y ) /\ u e. U ) -> u <_ sup ( U , RR , < ) )
305 300 301 302 303 304 syl31anc 
 |-  ( ( ph /\ u e. U ) -> u <_ sup ( U , RR , < ) )
306 305 15 breqtrrdi 
 |-  ( ( ph /\ u e. U ) -> u <_ S )
307 306 adantr 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> u <_ S )
308 1 250 264 5 252 299 307 76 251 253 hsphoidmvle2 
 |-  ( ( ( ph /\ u e. U ) /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` u ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
309 262 249 256 298 308 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 ) ) ) ) ) )
310 271 292 248 293 309 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 ) ) ) ) ) ) )
311 247 272 276 291 310 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 ) ) ) ) ) ) )
312 311 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 ) ) ) ) ) ) )
313 245 312 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 ) ) ) ) ) ) )
314 313 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 ) ) ) ) ) ) ) ) )
315 314 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 ) ) ) ) ) ) ) )
316 315 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 ) ) ) ) ) ) ) )
317 244 316 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 ) ) ) ) ) ) )
318 317 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 ) ) ) ) ) ) )
319 224 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 ) )
320 nfv 
 |-  F/ t ph
321 nfcv 
 |-  F/_ t c
322 nfre1 
 |-  F/ t E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t )
323 322 nfab 
 |-  F/_ t { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) }
324 321 323 nfel 
 |-  F/ t c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) }
325 320 324 nfan 
 |-  F/ t ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } )
326 nfv 
 |-  F/ t c e. RR
327 230 adantl 
 |-  ( ( ph /\ t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> E. u e. U t = ( u - ( A ` Z ) ) )
328 simpr 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> c = ( G x. t ) )
329 246 3adant3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> G e. RR )
330 simp3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> t = ( u - ( A ` Z ) ) )
331 173 3adant3 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( u - ( A ` Z ) ) e. RR )
332 330 331 eqeltrd 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> t e. RR )
333 329 332 remulcld 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( G x. t ) e. RR )
334 333 adantr 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> ( G x. t ) e. RR )
335 328 334 eqeltrd 
 |-  ( ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) /\ c = ( G x. t ) ) -> c e. RR )
336 335 ex 
 |-  ( ( ph /\ u e. U /\ t = ( u - ( A ` Z ) ) ) -> ( c = ( G x. t ) -> c e. RR ) )
337 336 3exp 
 |-  ( ph -> ( u e. U -> ( t = ( u - ( A ` Z ) ) -> ( c = ( G x. t ) -> c e. RR ) ) ) )
338 337 rexlimdv 
 |-  ( ph -> ( E. u e. U t = ( u - ( A ` Z ) ) -> ( c = ( G x. t ) -> c e. RR ) ) )
339 338 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 ) ) )
340 327 339 mpd 
 |-  ( ( ph /\ t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } ) -> ( c = ( G x. t ) -> c e. RR ) )
341 340 ex 
 |-  ( ph -> ( t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } -> ( c = ( G x. t ) -> c e. RR ) ) )
342 341 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 ) ) )
343 325 326 342 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 ) )
344 319 343 mpd 
 |-  ( ( ph /\ c e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } ) -> c e. RR )
345 344 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 )
346 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 )
347 345 346 sylibr 
 |-  ( ph -> { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } C_ RR )
348 45 eqcomd 
 |-  ( ph -> 0 = ( G x. 0 ) )
349 oveq2 
 |-  ( t = 0 -> ( G x. t ) = ( G x. 0 ) )
350 349 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 ) )
351 187 348 350 syl2anc 
 |-  ( ph -> E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } 0 = ( G x. t ) )
352 eqeq1 
 |-  ( v = 0 -> ( v = ( G x. t ) <-> 0 = ( G x. t ) ) )
353 352 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 ) ) )
354 50 351 353 elabd 
 |-  ( ph -> 0 e. { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } )
355 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 ) } =/= (/) )
356 354 355 syl 
 |-  ( ph -> { v | E. t e. { w | E. u e. U w = ( u - ( A ` Z ) ) } v = ( G x. t ) } =/= (/) )
357 43 190 remulcld 
 |-  ( ph -> ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) e. RR )
358 190 adantr 
 |-  ( ( ph /\ u e. U ) -> ( ( B ` Z ) - ( A ` Z ) ) e. RR )
359 137 adantr 
 |-  ( ( ph /\ u e. U ) -> 0 <_ G )
360 24 adantr 
 |-  ( ( ph /\ u e. U ) -> ( B ` Z ) e. RR )
361 iccleub 
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ u e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> u <_ ( B ` Z ) )
362 152 154 155 361 syl3anc 
 |-  ( ( ph /\ u e. U ) -> u <_ ( B ` Z ) )
363 158 360 159 362 lesub1dd 
 |-  ( ( ph /\ u e. U ) -> ( u - ( A ` Z ) ) <_ ( ( B ` Z ) - ( A ` Z ) ) )
364 173 358 246 359 363 lemul2ad 
 |-  ( ( ph /\ u e. U ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
365 364 3adant3 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> ( G x. ( u - ( A ` Z ) ) ) <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
366 245 365 eqbrtrd 
 |-  ( ( ph /\ u e. U /\ c = ( G x. ( u - ( A ` Z ) ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
367 366 3exp 
 |-  ( ph -> ( u e. U -> ( c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) ) )
368 367 rexlimdv 
 |-  ( ph -> ( E. u e. U c = ( G x. ( u - ( A ` Z ) ) ) -> c <_ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) ) )
369 368 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 ) ) ) ) )
370 244 369 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 ) ) ) )
371 370 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 ) ) ) )
372 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 )
373 357 371 372 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 )
374 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 ) ) ) ) ) ) ) )
375 347 356 373 275 374 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 ) ) ) ) ) ) ) )
376 318 375 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 ) ) ) ) ) ) )
377 219 376 eqbrtrd 
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
378 123 377 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 ) ) ) ) ) ) ) )
379 oveq1 
 |-  ( z = S -> ( z - ( A ` Z ) ) = ( S - ( A ` Z ) ) )
380 379 oveq2d 
 |-  ( z = S -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( S - ( A ` Z ) ) ) )
381 fveq2 
 |-  ( z = S -> ( H ` z ) = ( H ` S ) )
382 381 fveq1d 
 |-  ( z = S -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` S ) ` ( D ` j ) ) )
383 382 oveq2d 
 |-  ( z = S -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
384 383 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 ) ) ) ) )
385 384 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 ) ) ) ) ) )
386 385 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 ) ) ) ) ) ) )
387 380 386 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 ) ) ) ) ) ) ) )
388 387 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 ) ) ) ) ) ) ) )
389 378 388 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 ) ) ) ) ) ) } )
390 389 14 eleqtrrdi 
 |-  ( ph -> S e. U )