Metamath Proof Explorer

Theorem fourierdlem64

Description: The partition V is finer than Q , when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem64.t 
|- T = ( B - A )
fourierdlem64.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem64.m 
|- ( ph -> M e. NN )
fourierdlem64.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem64.c 
|- ( ph -> C e. RR )
fourierdlem64.d 
|- ( ph -> D e. RR )
fourierdlem64.cltd 
|- ( ph -> C < D )
fourierdlem64.h 
|- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
fourierdlem64.n 
|- N = ( ( # ` H ) - 1 )
fourierdlem64.v 
|- V = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem64.j 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem64.l 
|- L = sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < )
fourierdlem64.i 
|- I = sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < )
Assertion fourierdlem64 
|- ( ph -> ( ( I e. ( 0 ..^ M ) /\ L e. ZZ ) /\ E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem64.t 
 |-  T = ( B - A )
2 fourierdlem64.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
3 fourierdlem64.m 
 |-  ( ph -> M e. NN )
4 fourierdlem64.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem64.c 
 |-  ( ph -> C e. RR )
6 fourierdlem64.d 
 |-  ( ph -> D e. RR )
7 fourierdlem64.cltd 
 |-  ( ph -> C < D )
8 fourierdlem64.h 
 |-  H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
9 fourierdlem64.n 
 |-  N = ( ( # ` H ) - 1 )
10 fourierdlem64.v 
 |-  V = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
11 fourierdlem64.j 
 |-  ( ph -> J e. ( 0 ..^ N ) )
12 fourierdlem64.l 
 |-  L = sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < )
13 fourierdlem64.i 
 |-  I = sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < )
14 ssrab2 
 |-  { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ ( 0 ..^ M )
15 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
16 fzssz 
 |-  ( 0 ... M ) C_ ZZ
17 15 16 sstri 
 |-  ( 0 ..^ M ) C_ ZZ
18 14 17 sstri 
 |-  { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ ZZ
19 18 a1i 
 |-  ( ph -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ ZZ )
20 0zd 
 |-  ( ph -> 0 e. ZZ )
21 3 nnzd 
 |-  ( ph -> M e. ZZ )
22 3 nngt0d 
 |-  ( ph -> 0 < M )
23 fzolb 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
24 20 21 22 23 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
25 ssrab2 
 |-  { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ ZZ
26 25 a1i 
 |-  ( ph -> { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ ZZ )
27 prssi 
 |-  ( ( C e. RR /\ D e. RR ) -> { C , D } C_ RR )
28 5 6 27 syl2anc 
 |-  ( ph -> { C , D } C_ RR )
29 ssrab2 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } C_ ( C [,] D )
30 29 a1i 
 |-  ( ph -> { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } C_ ( C [,] D ) )
31 5 6 iccssred 
 |-  ( ph -> ( C [,] D ) C_ RR )
32 30 31 sstrd 
 |-  ( ph -> { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } C_ RR )
33 28 32 unssd 
 |-  ( ph -> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) C_ RR )
34 8 33 eqsstrid 
 |-  ( ph -> H C_ RR )
35 eqid 
 |-  ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
36 1 2 3 4 5 6 7 35 8 9 10 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ V e. ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) ) /\ V Isom < , < ( ( 0 ... N ) , H ) ) )
37 36 simprd 
 |-  ( ph -> V Isom < , < ( ( 0 ... N ) , H ) )
38 isof1o 
 |-  ( V Isom < , < ( ( 0 ... N ) , H ) -> V : ( 0 ... N ) -1-1-onto-> H )
39 f1of 
 |-  ( V : ( 0 ... N ) -1-1-onto-> H -> V : ( 0 ... N ) --> H )
40 37 38 39 3syl 
 |-  ( ph -> V : ( 0 ... N ) --> H )
41 elfzofz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) )
42 11 41 syl 
 |-  ( ph -> J e. ( 0 ... N ) )
43 40 42 ffvelrnd 
 |-  ( ph -> ( V ` J ) e. H )
44 34 43 sseldd 
 |-  ( ph -> ( V ` J ) e. RR )
45 2 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
46 3 45 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
47 4 46 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
48 47 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
49 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
50 48 49 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
51 3 nnnn0d 
 |-  ( ph -> M e. NN0 )
52 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
53 51 52 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
54 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
55 53 54 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
56 50 55 ffvelrnd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
57 44 56 resubcld 
 |-  ( ph -> ( ( V ` J ) - ( Q ` 0 ) ) e. RR )
58 2 3 4 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
59 58 simp2d 
 |-  ( ph -> B e. RR )
60 58 simp1d 
 |-  ( ph -> A e. RR )
61 59 60 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
62 1 61 eqeltrid 
 |-  ( ph -> T e. RR )
63 58 simp3d 
 |-  ( ph -> A < B )
64 60 59 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
65 63 64 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
66 65 1 breqtrrdi 
 |-  ( ph -> 0 < T )
67 66 gt0ne0d 
 |-  ( ph -> T =/= 0 )
68 57 62 67 redivcld 
 |-  ( ph -> ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) e. RR )
69 btwnz 
 |-  ( ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) e. RR -> ( E. k e. ZZ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) /\ E. z e. ZZ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) < z ) )
70 68 69 syl 
 |-  ( ph -> ( E. k e. ZZ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) /\ E. z e. ZZ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) < z ) )
71 70 simpld 
 |-  ( ph -> E. k e. ZZ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
72 zre 
 |-  ( k e. ZZ -> k e. RR )
73 56 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( Q ` 0 ) e. RR )
74 simplr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> k e. RR )
75 62 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> T e. RR )
76 74 75 remulcld 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( k x. T ) e. RR )
77 73 76 readdcld 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( Q ` 0 ) + ( k x. T ) ) e. RR )
78 44 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( V ` J ) e. RR )
79 simpr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
80 57 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( V ` J ) - ( Q ` 0 ) ) e. RR )
81 62 66 elrpd 
 |-  ( ph -> T e. RR+ )
82 81 ad2antrr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> T e. RR+ )
83 74 80 82 ltmuldivd 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( k x. T ) < ( ( V ` J ) - ( Q ` 0 ) ) <-> k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) )
84 79 83 mpbird 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( k x. T ) < ( ( V ` J ) - ( Q ` 0 ) ) )
85 56 adantr 
 |-  ( ( ph /\ k e. RR ) -> ( Q ` 0 ) e. RR )
86 simpr 
 |-  ( ( ph /\ k e. RR ) -> k e. RR )
87 62 adantr 
 |-  ( ( ph /\ k e. RR ) -> T e. RR )
88 86 87 remulcld 
 |-  ( ( ph /\ k e. RR ) -> ( k x. T ) e. RR )
89 44 adantr 
 |-  ( ( ph /\ k e. RR ) -> ( V ` J ) e. RR )
90 85 88 89 ltaddsub2d 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( Q ` 0 ) + ( k x. T ) ) < ( V ` J ) <-> ( k x. T ) < ( ( V ` J ) - ( Q ` 0 ) ) ) )
91 90 adantr 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( ( Q ` 0 ) + ( k x. T ) ) < ( V ` J ) <-> ( k x. T ) < ( ( V ` J ) - ( Q ` 0 ) ) ) )
92 84 91 mpbird 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( Q ` 0 ) + ( k x. T ) ) < ( V ` J ) )
93 77 78 92 ltled 
 |-  ( ( ( ph /\ k e. RR ) /\ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) )
94 93 ex 
 |-  ( ( ph /\ k e. RR ) -> ( k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) -> ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) ) )
95 72 94 sylan2 
 |-  ( ( ph /\ k e. ZZ ) -> ( k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) -> ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) ) )
96 95 reximdva 
 |-  ( ph -> ( E. k e. ZZ k < ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) -> E. k e. ZZ ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) ) )
97 71 96 mpd 
 |-  ( ph -> E. k e. ZZ ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) )
98 rabn0 
 |-  ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } =/= (/) <-> E. k e. ZZ ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) )
99 97 98 sylibr 
 |-  ( ph -> { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } =/= (/) )
100 simpl 
 |-  ( ( ph /\ j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } ) -> ph )
101 26 sselda 
 |-  ( ( ph /\ j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } ) -> j e. ZZ )
102 oveq1 
 |-  ( k = j -> ( k x. T ) = ( j x. T ) )
103 102 oveq2d 
 |-  ( k = j -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( j x. T ) ) )
104 103 breq1d 
 |-  ( k = j -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) )
105 104 elrab 
 |-  ( j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } <-> ( j e. ZZ /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) )
106 105 simprbi 
 |-  ( j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } -> ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) )
107 106 adantl 
 |-  ( ( ph /\ j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } ) -> ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) )
108 zre 
 |-  ( j e. ZZ -> j e. RR )
109 simpr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) )
110 56 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( Q ` 0 ) e. RR )
111 simpr 
 |-  ( ( ph /\ j e. RR ) -> j e. RR )
112 62 adantr 
 |-  ( ( ph /\ j e. RR ) -> T e. RR )
113 111 112 remulcld 
 |-  ( ( ph /\ j e. RR ) -> ( j x. T ) e. RR )
114 113 adantr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( j x. T ) e. RR )
115 44 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( V ` J ) e. RR )
116 110 114 115 leaddsub2d 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) <-> ( j x. T ) <_ ( ( V ` J ) - ( Q ` 0 ) ) ) )
117 109 116 mpbid 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( j x. T ) <_ ( ( V ` J ) - ( Q ` 0 ) ) )
118 simplr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> j e. RR )
119 57 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( ( V ` J ) - ( Q ` 0 ) ) e. RR )
120 81 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> T e. RR+ )
121 118 119 120 lemuldivd 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> ( ( j x. T ) <_ ( ( V ` J ) - ( Q ` 0 ) ) <-> j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) )
122 117 121 mpbid 
 |-  ( ( ( ph /\ j e. RR ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
123 108 122 sylanl2 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( ( Q ` 0 ) + ( j x. T ) ) <_ ( V ` J ) ) -> j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
124 100 101 107 123 syl21anc 
 |-  ( ( ph /\ j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } ) -> j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
125 124 ralrimiva 
 |-  ( ph -> A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) )
126 breq2 
 |-  ( b = ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) -> ( j <_ b <-> j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) )
127 126 ralbidv 
 |-  ( b = ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) -> ( A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b <-> A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) )
128 127 rspcev 
 |-  ( ( ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) e. RR /\ A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ ( ( ( V ` J ) - ( Q ` 0 ) ) / T ) ) -> E. b e. RR A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b )
129 68 125 128 syl2anc 
 |-  ( ph -> E. b e. RR A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b )
130 suprzcl 
 |-  ( ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ ZZ /\ { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } =/= (/) /\ E. b e. RR A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b ) -> sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } )
131 26 99 129 130 syl3anc 
 |-  ( ph -> sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } )
132 12 131 eqeltrid 
 |-  ( ph -> L e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } )
133 oveq1 
 |-  ( k = L -> ( k x. T ) = ( L x. T ) )
134 133 oveq2d 
 |-  ( k = L -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( L x. T ) ) )
135 134 breq1d 
 |-  ( k = L -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) ) )
136 135 elrab 
 |-  ( L e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } <-> ( L e. ZZ /\ ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) ) )
137 132 136 sylib 
 |-  ( ph -> ( L e. ZZ /\ ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) ) )
138 137 simprd 
 |-  ( ph -> ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) )
139 fveq2 
 |-  ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
140 139 oveq1d 
 |-  ( j = 0 -> ( ( Q ` j ) + ( L x. T ) ) = ( ( Q ` 0 ) + ( L x. T ) ) )
141 140 breq1d 
 |-  ( j = 0 -> ( ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) ) )
142 141 elrab 
 |-  ( 0 e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } <-> ( 0 e. ( 0 ..^ M ) /\ ( ( Q ` 0 ) + ( L x. T ) ) <_ ( V ` J ) ) )
143 24 138 142 sylanbrc 
 |-  ( ph -> 0 e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } )
144 ne0i 
 |-  ( 0 e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } =/= (/) )
145 143 144 syl 
 |-  ( ph -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } =/= (/) )
146 3 nnred 
 |-  ( ph -> M e. RR )
147 14 a1i 
 |-  ( ph -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ ( 0 ..^ M ) )
148 147 sselda 
 |-  ( ( ph /\ k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } ) -> k e. ( 0 ..^ M ) )
149 elfzoelz 
 |-  ( k e. ( 0 ..^ M ) -> k e. ZZ )
150 149 zred 
 |-  ( k e. ( 0 ..^ M ) -> k e. RR )
151 150 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> k e. RR )
152 146 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> M e. RR )
153 elfzolt2 
 |-  ( k e. ( 0 ..^ M ) -> k < M )
154 153 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> k < M )
155 151 152 154 ltled 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> k <_ M )
156 148 155 syldan 
 |-  ( ( ph /\ k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } ) -> k <_ M )
157 156 ralrimiva 
 |-  ( ph -> A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ M )
158 breq2 
 |-  ( b = M -> ( k <_ b <-> k <_ M ) )
159 158 ralbidv 
 |-  ( b = M -> ( A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b <-> A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ M ) )
160 159 rspcev 
 |-  ( ( M e. RR /\ A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ M ) -> E. b e. RR A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b )
161 146 157 160 syl2anc 
 |-  ( ph -> E. b e. RR A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b )
162 suprzcl 
 |-  ( ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ ZZ /\ { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } =/= (/) /\ E. b e. RR A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b ) -> sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < ) e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } )
163 19 145 161 162 syl3anc 
 |-  ( ph -> sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < ) e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } )
164 14 163 sselid 
 |-  ( ph -> sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < ) e. ( 0 ..^ M ) )
165 13 164 eqeltrid 
 |-  ( ph -> I e. ( 0 ..^ M ) )
166 25 131 sselid 
 |-  ( ph -> sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. ZZ )
167 12 166 eqeltrid 
 |-  ( ph -> L e. ZZ )
168 15 165 sselid 
 |-  ( ph -> I e. ( 0 ... M ) )
169 50 168 ffvelrnd 
 |-  ( ph -> ( Q ` I ) e. RR )
170 167 zred 
 |-  ( ph -> L e. RR )
171 170 62 remulcld 
 |-  ( ph -> ( L x. T ) e. RR )
172 169 171 readdcld 
 |-  ( ph -> ( ( Q ` I ) + ( L x. T ) ) e. RR )
173 172 rexrd 
 |-  ( ph -> ( ( Q ` I ) + ( L x. T ) ) e. RR* )
174 173 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` I ) + ( L x. T ) ) e. RR* )
175 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
176 165 175 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
177 50 176 ffvelrnd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR )
178 177 171 readdcld 
 |-  ( ph -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
179 178 rexrd 
 |-  ( ph -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR* )
180 179 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR* )
181 elioore 
 |-  ( x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -> x e. RR )
182 181 adantl 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x e. RR )
183 172 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` I ) + ( L x. T ) ) e. RR )
184 44 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` J ) e. RR )
185 13 163 eqeltrid 
 |-  ( ph -> I e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } )
186 fveq2 
 |-  ( j = I -> ( Q ` j ) = ( Q ` I ) )
187 186 oveq1d 
 |-  ( j = I -> ( ( Q ` j ) + ( L x. T ) ) = ( ( Q ` I ) + ( L x. T ) ) )
188 187 breq1d 
 |-  ( j = I -> ( ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) <-> ( ( Q ` I ) + ( L x. T ) ) <_ ( V ` J ) ) )
189 188 elrab 
 |-  ( I e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } <-> ( I e. ( 0 ..^ M ) /\ ( ( Q ` I ) + ( L x. T ) ) <_ ( V ` J ) ) )
190 185 189 sylib 
 |-  ( ph -> ( I e. ( 0 ..^ M ) /\ ( ( Q ` I ) + ( L x. T ) ) <_ ( V ` J ) ) )
191 190 simprd 
 |-  ( ph -> ( ( Q ` I ) + ( L x. T ) ) <_ ( V ` J ) )
192 191 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` I ) + ( L x. T ) ) <_ ( V ` J ) )
193 184 rexrd 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` J ) e. RR* )
194 fzofzp1 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
195 11 194 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... N ) )
196 40 195 ffvelrnd 
 |-  ( ph -> ( V ` ( J + 1 ) ) e. H )
197 34 196 sseldd 
 |-  ( ph -> ( V ` ( J + 1 ) ) e. RR )
198 197 rexrd 
 |-  ( ph -> ( V ` ( J + 1 ) ) e. RR* )
199 198 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` ( J + 1 ) ) e. RR* )
200 simpr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) )
201 ioogtlb 
 |-  ( ( ( V ` J ) e. RR* /\ ( V ` ( J + 1 ) ) e. RR* /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` J ) < x )
202 193 199 200 201 syl3anc 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` J ) < x )
203 183 184 182 192 202 lelttrd 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` I ) + ( L x. T ) ) < x )
204 zssre 
 |-  ZZ C_ RR
205 25 204 sstri 
 |-  { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ RR
206 205 a1i 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ RR )
207 99 ad2antrr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } =/= (/) )
208 129 ad2antrr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> E. b e. RR A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b )
209 167 peano2zd 
 |-  ( ph -> ( L + 1 ) e. ZZ )
210 209 ad2antrr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( L + 1 ) e. ZZ )
211 oveq1 
 |-  ( I = ( M - 1 ) -> ( I + 1 ) = ( ( M - 1 ) + 1 ) )
212 146 recnd 
 |-  ( ph -> M e. CC )
213 1cnd 
 |-  ( ph -> 1 e. CC )
214 212 213 npcand 
 |-  ( ph -> ( ( M - 1 ) + 1 ) = M )
215 211 214 sylan9eqr 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( I + 1 ) = M )
216 215 fveq2d 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( Q ` ( I + 1 ) ) = ( Q ` M ) )
217 47 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
218 217 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
219 218 simprd 
 |-  ( ph -> ( Q ` M ) = B )
220 219 adantr 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( Q ` M ) = B )
221 59 recnd 
 |-  ( ph -> B e. CC )
222 60 recnd 
 |-  ( ph -> A e. CC )
223 221 222 npcand 
 |-  ( ph -> ( ( B - A ) + A ) = B )
224 223 eqcomd 
 |-  ( ph -> B = ( ( B - A ) + A ) )
225 1 eqcomi 
 |-  ( B - A ) = T
226 225 a1i 
 |-  ( ph -> ( B - A ) = T )
227 226 oveq1d 
 |-  ( ph -> ( ( B - A ) + A ) = ( T + A ) )
228 218 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
229 228 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
230 229 oveq2d 
 |-  ( ph -> ( T + A ) = ( T + ( Q ` 0 ) ) )
231 224 227 230 3eqtrd 
 |-  ( ph -> B = ( T + ( Q ` 0 ) ) )
232 231 adantr 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> B = ( T + ( Q ` 0 ) ) )
233 216 220 232 3eqtrd 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( Q ` ( I + 1 ) ) = ( T + ( Q ` 0 ) ) )
234 62 recnd 
 |-  ( ph -> T e. CC )
235 228 222 eqeltrd 
 |-  ( ph -> ( Q ` 0 ) e. CC )
236 234 235 addcomd 
 |-  ( ph -> ( T + ( Q ` 0 ) ) = ( ( Q ` 0 ) + T ) )
237 236 adantr 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( T + ( Q ` 0 ) ) = ( ( Q ` 0 ) + T ) )
238 233 237 eqtrd 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( Q ` ( I + 1 ) ) = ( ( Q ` 0 ) + T ) )
239 238 oveq1d 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( ( ( Q ` 0 ) + T ) + ( L x. T ) ) )
240 171 recnd 
 |-  ( ph -> ( L x. T ) e. CC )
241 235 234 240 addassd 
 |-  ( ph -> ( ( ( Q ` 0 ) + T ) + ( L x. T ) ) = ( ( Q ` 0 ) + ( T + ( L x. T ) ) ) )
242 234 mulid2d 
 |-  ( ph -> ( 1 x. T ) = T )
243 242 234 eqeltrd 
 |-  ( ph -> ( 1 x. T ) e. CC )
244 243 240 addcomd 
 |-  ( ph -> ( ( 1 x. T ) + ( L x. T ) ) = ( ( L x. T ) + ( 1 x. T ) ) )
245 242 eqcomd 
 |-  ( ph -> T = ( 1 x. T ) )
246 245 oveq1d 
 |-  ( ph -> ( T + ( L x. T ) ) = ( ( 1 x. T ) + ( L x. T ) ) )
247 170 recnd 
 |-  ( ph -> L e. CC )
248 247 213 234 adddird 
 |-  ( ph -> ( ( L + 1 ) x. T ) = ( ( L x. T ) + ( 1 x. T ) ) )
249 244 246 248 3eqtr4d 
 |-  ( ph -> ( T + ( L x. T ) ) = ( ( L + 1 ) x. T ) )
250 249 oveq2d 
 |-  ( ph -> ( ( Q ` 0 ) + ( T + ( L x. T ) ) ) = ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) )
251 241 250 eqtrd 
 |-  ( ph -> ( ( ( Q ` 0 ) + T ) + ( L x. T ) ) = ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) )
252 251 adantr 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( ( ( Q ` 0 ) + T ) + ( L x. T ) ) = ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) )
253 239 252 eqtr2d 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
254 253 adantr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
255 simpr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) )
256 254 255 eqbrtrd 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) <_ ( V ` J ) )
257 oveq1 
 |-  ( k = ( L + 1 ) -> ( k x. T ) = ( ( L + 1 ) x. T ) )
258 257 oveq2d 
 |-  ( k = ( L + 1 ) -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) )
259 258 breq1d 
 |-  ( k = ( L + 1 ) -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) <_ ( V ` J ) ) )
260 259 elrab 
 |-  ( ( L + 1 ) e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } <-> ( ( L + 1 ) e. ZZ /\ ( ( Q ` 0 ) + ( ( L + 1 ) x. T ) ) <_ ( V ` J ) ) )
261 210 256 260 sylanbrc 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( L + 1 ) e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } )
262 suprub 
 |-  ( ( ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } C_ RR /\ { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } =/= (/) /\ E. b e. RR A. j e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } j <_ b ) /\ ( L + 1 ) e. { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } ) -> ( L + 1 ) <_ sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) )
263 206 207 208 261 262 syl31anc 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( L + 1 ) <_ sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) )
264 263 12 breqtrrdi 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( L + 1 ) <_ L )
265 170 ltp1d 
 |-  ( ph -> L < ( L + 1 ) )
266 peano2re 
 |-  ( L e. RR -> ( L + 1 ) e. RR )
267 170 266 syl 
 |-  ( ph -> ( L + 1 ) e. RR )
268 170 267 ltnled 
 |-  ( ph -> ( L < ( L + 1 ) <-> -. ( L + 1 ) <_ L ) )
269 265 268 mpbid 
 |-  ( ph -> -. ( L + 1 ) <_ L )
270 269 ad2antrr 
 |-  ( ( ( ph /\ I = ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> -. ( L + 1 ) <_ L )
271 264 270 pm2.65da 
 |-  ( ( ph /\ I = ( M - 1 ) ) -> -. ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) )
272 17 165 sselid 
 |-  ( ph -> I e. ZZ )
273 272 zred 
 |-  ( ph -> I e. RR )
274 273 adantr 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> I e. RR )
275 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
276 146 275 syl 
 |-  ( ph -> ( M - 1 ) e. RR )
277 276 adantr 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> ( M - 1 ) e. RR )
278 elfzolt2 
 |-  ( I e. ( 0 ..^ M ) -> I < M )
279 elfzoelz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ZZ )
280 elfzoel2 
 |-  ( I e. ( 0 ..^ M ) -> M e. ZZ )
281 zltlem1 
 |-  ( ( I e. ZZ /\ M e. ZZ ) -> ( I < M <-> I <_ ( M - 1 ) ) )
282 279 280 281 syl2anc 
 |-  ( I e. ( 0 ..^ M ) -> ( I < M <-> I <_ ( M - 1 ) ) )
283 278 282 mpbid 
 |-  ( I e. ( 0 ..^ M ) -> I <_ ( M - 1 ) )
284 165 283 syl 
 |-  ( ph -> I <_ ( M - 1 ) )
285 284 adantr 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> I <_ ( M - 1 ) )
286 neqne 
 |-  ( -. I = ( M - 1 ) -> I =/= ( M - 1 ) )
287 286 necomd 
 |-  ( -. I = ( M - 1 ) -> ( M - 1 ) =/= I )
288 287 adantl 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> ( M - 1 ) =/= I )
289 274 277 285 288 leneltd 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> I < ( M - 1 ) )
290 18 204 sstri 
 |-  { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ RR
291 290 a1i 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ RR )
292 145 ad2antrr 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } =/= (/) )
293 161 ad2antrr 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> E. b e. RR A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b )
294 176 adantr 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( I + 1 ) e. ( 0 ... M ) )
295 273 adantr 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> I e. RR )
296 276 adantr 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( M - 1 ) e. RR )
297 1red 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> 1 e. RR )
298 simpr 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> I < ( M - 1 ) )
299 295 296 297 298 ltadd1dd 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( I + 1 ) < ( ( M - 1 ) + 1 ) )
300 214 adantr 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) = M )
301 299 300 breqtrd 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( I + 1 ) < M )
302 elfzfzo 
 |-  ( ( I + 1 ) e. ( 0 ..^ M ) <-> ( ( I + 1 ) e. ( 0 ... M ) /\ ( I + 1 ) < M ) )
303 294 301 302 sylanbrc 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> ( I + 1 ) e. ( 0 ..^ M ) )
304 303 anim1i 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( ( I + 1 ) e. ( 0 ..^ M ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) )
305 fveq2 
 |-  ( j = ( I + 1 ) -> ( Q ` j ) = ( Q ` ( I + 1 ) ) )
306 305 oveq1d 
 |-  ( j = ( I + 1 ) -> ( ( Q ` j ) + ( L x. T ) ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
307 306 breq1d 
 |-  ( j = ( I + 1 ) -> ( ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) <-> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) )
308 307 elrab 
 |-  ( ( I + 1 ) e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } <-> ( ( I + 1 ) e. ( 0 ..^ M ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) )
309 304 308 sylibr 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( I + 1 ) e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } )
310 suprub 
 |-  ( ( ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } C_ RR /\ { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } =/= (/) /\ E. b e. RR A. k e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } k <_ b ) /\ ( I + 1 ) e. { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } ) -> ( I + 1 ) <_ sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < ) )
311 291 292 293 309 310 syl31anc 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( I + 1 ) <_ sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < ) )
312 311 13 breqtrrdi 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> ( I + 1 ) <_ I )
313 273 ltp1d 
 |-  ( ph -> I < ( I + 1 ) )
314 peano2re 
 |-  ( I e. RR -> ( I + 1 ) e. RR )
315 273 314 syl 
 |-  ( ph -> ( I + 1 ) e. RR )
316 273 315 ltnled 
 |-  ( ph -> ( I < ( I + 1 ) <-> -. ( I + 1 ) <_ I ) )
317 313 316 mpbid 
 |-  ( ph -> -. ( I + 1 ) <_ I )
318 317 ad2antrr 
 |-  ( ( ( ph /\ I < ( M - 1 ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) -> -. ( I + 1 ) <_ I )
319 312 318 pm2.65da 
 |-  ( ( ph /\ I < ( M - 1 ) ) -> -. ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) )
320 289 319 syldan 
 |-  ( ( ph /\ -. I = ( M - 1 ) ) -> -. ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) )
321 271 320 pm2.61dan 
 |-  ( ph -> -. ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) )
322 44 178 ltnled 
 |-  ( ph -> ( ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <-> -. ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ ( V ` J ) ) )
323 321 322 mpbird 
 |-  ( ph -> ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
324 197 adantr 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) e. RR )
325 6 adantr 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> D e. RR )
326 178 adantr 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
327 5 rexrd 
 |-  ( ph -> C e. RR* )
328 6 rexrd 
 |-  ( ph -> D e. RR* )
329 5 6 7 ltled 
 |-  ( ph -> C <_ D )
330 lbicc2 
 |-  ( ( C e. RR* /\ D e. RR* /\ C <_ D ) -> C e. ( C [,] D ) )
331 327 328 329 330 syl3anc 
 |-  ( ph -> C e. ( C [,] D ) )
332 ubicc2 
 |-  ( ( C e. RR* /\ D e. RR* /\ C <_ D ) -> D e. ( C [,] D ) )
333 327 328 329 332 syl3anc 
 |-  ( ph -> D e. ( C [,] D ) )
334 331 333 jca 
 |-  ( ph -> ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) )
335 prssg 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) <-> { C , D } C_ ( C [,] D ) ) )
336 5 6 335 syl2anc 
 |-  ( ph -> ( ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) <-> { C , D } C_ ( C [,] D ) ) )
337 334 336 mpbid 
 |-  ( ph -> { C , D } C_ ( C [,] D ) )
338 337 30 unssd 
 |-  ( ph -> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) C_ ( C [,] D ) )
339 8 338 eqsstrid 
 |-  ( ph -> H C_ ( C [,] D ) )
340 339 196 sseldd 
 |-  ( ph -> ( V ` ( J + 1 ) ) e. ( C [,] D ) )
341 iccleub 
 |-  ( ( C e. RR* /\ D e. RR* /\ ( V ` ( J + 1 ) ) e. ( C [,] D ) ) -> ( V ` ( J + 1 ) ) <_ D )
342 327 328 340 341 syl3anc 
 |-  ( ph -> ( V ` ( J + 1 ) ) <_ D )
343 342 adantr 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ D )
344 simpr 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
345 324 325 326 343 344 letrd 
 |-  ( ( ph /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
346 345 adantlr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
347 simpr 
 |-  ( ( ph /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
348 178 adantr 
 |-  ( ( ph /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
349 6 adantr 
 |-  ( ( ph /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> D e. RR )
350 348 349 ltnled 
 |-  ( ( ph /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D <-> -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
351 347 350 mpbird 
 |-  ( ( ph /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D )
352 351 adantlr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D )
353 simpll 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
354 simpr 
 |-  ( ( ph /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
355 178 adantr 
 |-  ( ( ph /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
356 197 adantr 
 |-  ( ( ph /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) e. RR )
357 355 356 ltnled 
 |-  ( ( ph /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) <-> -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
358 354 357 mpbird 
 |-  ( ( ph /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) )
359 358 ad4ant14 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) )
360 5 ad2antrr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> C e. RR )
361 6 ad2antrr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> D e. RR )
362 178 ad2antrr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
363 5 adantr 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> C e. RR )
364 178 adantr 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
365 44 adantr 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) e. RR )
366 339 43 sseldd 
 |-  ( ph -> ( V ` J ) e. ( C [,] D ) )
367 iccgelb 
 |-  ( ( C e. RR* /\ D e. RR* /\ ( V ` J ) e. ( C [,] D ) ) -> C <_ ( V ` J ) )
368 327 328 366 367 syl3anc 
 |-  ( ph -> C <_ ( V ` J ) )
369 368 adantr 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> C <_ ( V ` J ) )
370 simpr 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
371 363 365 364 369 370 lelttrd 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> C < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
372 363 364 371 ltled 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> C <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
373 372 adantr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> C <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
374 178 adantr 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
375 6 adantr 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> D e. RR )
376 simpr 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D )
377 374 375 376 ltled 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ D )
378 377 adantlr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) <_ D )
379 360 361 362 373 378 eliccd 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. ( C [,] D ) )
380 167 znegcld 
 |-  ( ph -> -u L e. ZZ )
381 247 234 mulneg1d 
 |-  ( ph -> ( -u L x. T ) = -u ( L x. T ) )
382 381 oveq2d 
 |-  ( ph -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) = ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + -u ( L x. T ) ) )
383 178 recnd 
 |-  ( ph -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. CC )
384 383 240 negsubd 
 |-  ( ph -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + -u ( L x. T ) ) = ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) - ( L x. T ) ) )
385 177 recnd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. CC )
386 385 240 pncand 
 |-  ( ph -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) - ( L x. T ) ) = ( Q ` ( I + 1 ) ) )
387 382 384 386 3eqtrd 
 |-  ( ph -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) = ( Q ` ( I + 1 ) ) )
388 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
389 50 388 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
390 fnfvelrn 
 |-  ( ( Q Fn ( 0 ... M ) /\ ( I + 1 ) e. ( 0 ... M ) ) -> ( Q ` ( I + 1 ) ) e. ran Q )
391 389 176 390 syl2anc 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. ran Q )
392 387 391 eqeltrd 
 |-  ( ph -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) e. ran Q )
393 oveq1 
 |-  ( k = -u L -> ( k x. T ) = ( -u L x. T ) )
394 393 oveq2d 
 |-  ( k = -u L -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) = ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) )
395 394 eleq1d 
 |-  ( k = -u L -> ( ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) e. ran Q ) )
396 395 rspcev 
 |-  ( ( -u L e. ZZ /\ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( -u L x. T ) ) e. ran Q ) -> E. k e. ZZ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q )
397 380 392 396 syl2anc 
 |-  ( ph -> E. k e. ZZ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q )
398 397 ad2antrr 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> E. k e. ZZ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q )
399 oveq1 
 |-  ( y = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( y + ( k x. T ) ) = ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) )
400 399 eleq1d 
 |-  ( y = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( ( y + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q ) )
401 400 rexbidv 
 |-  ( y = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q ) )
402 401 elrab 
 |-  ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } <-> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. ( C [,] D ) /\ E. k e. ZZ ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) + ( k x. T ) ) e. ran Q ) )
403 379 398 402 sylanbrc 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
404 elun2 
 |-  ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
405 403 404 syl 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
406 8 eqcomi 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = H
407 405 406 eleqtrdi 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H )
408 407 adantr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H )
409 f1ofo 
 |-  ( V : ( 0 ... N ) -1-1-onto-> H -> V : ( 0 ... N ) -onto-> H )
410 37 38 409 3syl 
 |-  ( ph -> V : ( 0 ... N ) -onto-> H )
411 foelrn 
 |-  ( ( V : ( 0 ... N ) -onto-> H /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> E. j e. ( 0 ... N ) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) )
412 410 411 sylan 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> E. j e. ( 0 ... N ) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) )
413 id 
 |-  ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) )
414 413 eqcomd 
 |-  ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) -> ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
415 414 a1i 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) -> ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
416 415 reximdv 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> ( E. j e. ( 0 ... N ) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) -> E. j e. ( 0 ... N ) ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
417 412 416 mpd 
 |-  ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> E. j e. ( 0 ... N ) ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
418 417 ad4ant14 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> E. j e. ( 0 ... N ) ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
419 simpl 
 |-  ( ( ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
420 413 eqcoms 
 |-  ( ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) )
421 420 adantl 
 |-  ( ( ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) = ( V ` j ) )
422 419 421 breqtrd 
 |-  ( ( ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) < ( V ` j ) )
423 422 adantll 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) < ( V ` j ) )
424 423 adantlr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` J ) < ( V ` j ) )
425 37 ad3antrrr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> V Isom < , < ( ( 0 ... N ) , H ) )
426 42 ad3antrrr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> J e. ( 0 ... N ) )
427 simplr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> j e. ( 0 ... N ) )
428 isorel 
 |-  ( ( V Isom < , < ( ( 0 ... N ) , H ) /\ ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( J < j <-> ( V ` J ) < ( V ` j ) ) )
429 425 426 427 428 syl12anc 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( J < j <-> ( V ` J ) < ( V ` j ) ) )
430 424 429 mpbird 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> J < j )
431 430 adantllr 
 |-  ( ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> J < j )
432 simpr 
 |-  ( ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
433 simpl 
 |-  ( ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) )
434 432 433 eqbrtrd 
 |-  ( ( ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` j ) < ( V ` ( J + 1 ) ) )
435 434 adantll 
 |-  ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` j ) < ( V ` ( J + 1 ) ) )
436 435 adantlr 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` j ) < ( V ` ( J + 1 ) ) )
437 37 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> V Isom < , < ( ( 0 ... N ) , H ) )
438 simplr 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> j e. ( 0 ... N ) )
439 195 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( J + 1 ) e. ( 0 ... N ) )
440 isorel 
 |-  ( ( V Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( J + 1 ) <-> ( V ` j ) < ( V ` ( J + 1 ) ) ) )
441 437 438 439 440 syl12anc 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( j < ( J + 1 ) <-> ( V ` j ) < ( V ` ( J + 1 ) ) ) )
442 436 441 mpbird 
 |-  ( ( ( ( ph /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> j < ( J + 1 ) )
443 442 adantl3r 
 |-  ( ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> j < ( J + 1 ) )
444 431 443 jca 
 |-  ( ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( J < j /\ j < ( J + 1 ) ) )
445 444 ex 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( J < j /\ j < ( J + 1 ) ) ) )
446 445 adantlr 
 |-  ( ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) /\ j e. ( 0 ... N ) ) -> ( ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> ( J < j /\ j < ( J + 1 ) ) ) )
447 446 reximdva 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> ( E. j e. ( 0 ... N ) ( V ` j ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) -> E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) ) )
448 418 447 mpd 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < ( V ` ( J + 1 ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. H ) -> E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) )
449 353 359 408 448 syl21anc 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) )
450 elfzelz 
 |-  ( j e. ( 0 ... N ) -> j e. ZZ )
451 450 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> j e. ZZ )
452 elfzelz 
 |-  ( J e. ( 0 ... N ) -> J e. ZZ )
453 42 452 syl 
 |-  ( ph -> J e. ZZ )
454 453 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> J e. ZZ )
455 simprl 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> J < j )
456 simprr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> j < ( J + 1 ) )
457 btwnnz 
 |-  ( ( J e. ZZ /\ J < j /\ j < ( J + 1 ) ) -> -. j e. ZZ )
458 454 455 456 457 syl3anc 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> -. j e. ZZ )
459 451 458 pm2.65da 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> -. ( J < j /\ j < ( J + 1 ) ) )
460 459 nrexdv 
 |-  ( ph -> -. E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) )
461 460 ad3antrrr 
 |-  ( ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) /\ -. ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> -. E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) )
462 449 461 condan 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) < D ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
463 352 462 syldan 
 |-  ( ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) /\ -. D <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
464 346 463 pm2.61dan 
 |-  ( ( ph /\ ( V ` J ) < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
465 323 464 mpdan 
 |-  ( ph -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
466 465 adantr 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
467 182 adantr 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> x e. RR )
468 197 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) e. RR )
469 178 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) e. RR )
470 iooltub 
 |-  ( ( ( V ` J ) e. RR* /\ ( V ` ( J + 1 ) ) e. RR* /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x < ( V ` ( J + 1 ) ) )
471 193 199 200 470 syl3anc 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x < ( V ` ( J + 1 ) ) )
472 471 adantr 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> x < ( V ` ( J + 1 ) ) )
473 simpr 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
474 467 468 469 472 473 ltletrd 
 |-  ( ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) /\ ( V ` ( J + 1 ) ) <_ ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) -> x < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
475 466 474 mpdan 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x < ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
476 174 180 182 203 475 eliood 
 |-  ( ( ph /\ x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> x e. ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
477 476 ralrimiva 
 |-  ( ph -> A. x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) x e. ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
478 dfss3 
 |-  ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) <-> A. x e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) x e. ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
479 477 478 sylibr 
 |-  ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
480 fveq2 
 |-  ( i = I -> ( Q ` i ) = ( Q ` I ) )
481 480 oveq1d 
 |-  ( i = I -> ( ( Q ` i ) + ( l x. T ) ) = ( ( Q ` I ) + ( l x. T ) ) )
482 oveq1 
 |-  ( i = I -> ( i + 1 ) = ( I + 1 ) )
483 482 fveq2d 
 |-  ( i = I -> ( Q ` ( i + 1 ) ) = ( Q ` ( I + 1 ) ) )
484 483 oveq1d 
 |-  ( i = I -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) = ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) )
485 481 484 oveq12d 
 |-  ( i = I -> ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) = ( ( ( Q ` I ) + ( l x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) ) )
486 485 sseq2d 
 |-  ( i = I -> ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) <-> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( l x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) ) ) )
487 oveq1 
 |-  ( l = L -> ( l x. T ) = ( L x. T ) )
488 487 oveq2d 
 |-  ( l = L -> ( ( Q ` I ) + ( l x. T ) ) = ( ( Q ` I ) + ( L x. T ) ) )
489 487 oveq2d 
 |-  ( l = L -> ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) = ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) )
490 488 489 oveq12d 
 |-  ( l = L -> ( ( ( Q ` I ) + ( l x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) ) = ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) )
491 490 sseq2d 
 |-  ( l = L -> ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( l x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( l x. T ) ) ) <-> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) ) )
492 486 491 rspc2ev 
 |-  ( ( I e. ( 0 ..^ M ) /\ L e. ZZ /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` I ) + ( L x. T ) ) (,) ( ( Q ` ( I + 1 ) ) + ( L x. T ) ) ) ) -> E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
493 165 167 479 492 syl3anc 
 |-  ( ph -> E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
494 165 167 493 jca31 
 |-  ( ph -> ( ( I e. ( 0 ..^ M ) /\ L e. ZZ ) /\ E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )