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