Metamath Proof Explorer

Theorem fourierdlem41

Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem41.a 
|- ( ph -> A e. RR )
fourierdlem41.b 
|- ( ph -> B e. RR )
fourierdlem41.altb 
|- ( ph -> A < B )
fourierdlem41.t 
|- T = ( B - A )
fourierdlem41.dper 
|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
fourierdlem41.x 
|- ( ph -> X e. RR )
fourierdlem41.z 
|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
fourierdlem41.e 
|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
fourierdlem41.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 ) ) ) } )
fourierdlem41.m 
|- ( ph -> M e. NN )
fourierdlem41.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem41.qssd 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
Assertion fourierdlem41 
|- ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem41.a 
 |-  ( ph -> A e. RR )
2 fourierdlem41.b 
 |-  ( ph -> B e. RR )
3 fourierdlem41.altb 
 |-  ( ph -> A < B )
4 fourierdlem41.t 
 |-  T = ( B - A )
5 fourierdlem41.dper 
 |-  ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
6 fourierdlem41.x 
 |-  ( ph -> X e. RR )
7 fourierdlem41.z 
 |-  Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
8 fourierdlem41.e 
 |-  E = ( x e. RR |-> ( x + ( Z ` x ) ) )
9 fourierdlem41.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 ) ) ) } )
10 fourierdlem41.m 
 |-  ( ph -> M e. NN )
11 fourierdlem41.q 
 |-  ( ph -> Q e. ( P ` M ) )
12 fourierdlem41.qssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
13 simpr 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
14 9 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 ) ) ) ) ) )
15 10 14 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 ) ) ) ) ) )
16 11 15 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
17 16 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
18 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
19 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
20 17 18 19 3syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
21 20 adantr 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
22 fvelrnb 
 |-  ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
23 21 22 syl 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
24 13 23 mpbid 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
25 0zd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
26 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
27 26 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
28 1zzd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
29 27 28 zsubcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
30 simpll 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ph )
31 elfzle1 
 |-  ( j e. ( 0 ... M ) -> 0 <_ j )
32 31 anim1i 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 <_ j /\ -. 0 < j ) )
33 0red 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 e. RR )
34 26 zred 
 |-  ( j e. ( 0 ... M ) -> j e. RR )
35 34 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j e. RR )
36 33 35 eqleltd 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 = j <-> ( 0 <_ j /\ -. 0 < j ) ) )
37 32 36 mpbird 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 = j )
38 37 eqcomd 
 |-  ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j = 0 )
39 38 adantll 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> j = 0 )
40 fveq2 
 |-  ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
41 16 simprld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
42 41 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
43 40 42 sylan9eqr 
 |-  ( ( ph /\ j = 0 ) -> ( Q ` j ) = A )
44 30 39 43 syl2anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
45 44 3adantl3 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
46 simpr 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
47 1 rexrd 
 |-  ( ph -> A e. RR* )
48 2 rexrd 
 |-  ( ph -> B e. RR* )
49 eqid 
 |-  ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
50 1 2 3 4 49 fourierdlem4 
 |-  ( ph -> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) )
51 8 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
52 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
53 2 adantr 
 |-  ( ( ph /\ x e. RR ) -> B e. RR )
54 53 52 resubcld 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
55 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
56 4 55 eqeltrid 
 |-  ( ph -> T e. RR )
57 56 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. RR )
58 0red 
 |-  ( ph -> 0 e. RR )
59 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
60 3 59 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
61 4 eqcomi 
 |-  ( B - A ) = T
62 61 a1i 
 |-  ( ph -> ( B - A ) = T )
63 60 62 breqtrd 
 |-  ( ph -> 0 < T )
64 58 63 gtned 
 |-  ( ph -> T =/= 0 )
65 64 adantr 
 |-  ( ( ph /\ x e. RR ) -> T =/= 0 )
66 54 57 65 redivcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
67 66 flcld 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
68 67 zred 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
69 68 57 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
70 7 fvmpt2 
 |-  ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
71 52 69 70 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
72 71 oveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
73 72 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
74 51 73 eqtrd 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
75 74 feq1d 
 |-  ( ph -> ( E : RR --> ( A (,] B ) <-> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) ) )
76 50 75 mpbird 
 |-  ( ph -> E : RR --> ( A (,] B ) )
77 76 6 ffvelrnd 
 |-  ( ph -> ( E ` X ) e. ( A (,] B ) )
78 iocgtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
79 47 48 77 78 syl3anc 
 |-  ( ph -> A < ( E ` X ) )
80 1 79 gtned 
 |-  ( ph -> ( E ` X ) =/= A )
81 80 adantr 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) =/= A )
82 46 81 eqnetrd 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) =/= A )
83 82 adantr 
 |-  ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
84 83 3adantl2 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
85 84 neneqd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> -. ( Q ` j ) = A )
86 45 85 condan 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
87 zltlem1 
 |-  ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
88 25 27 87 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
89 86 88 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
90 eluz2 
 |-  ( ( j - 1 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( j - 1 ) e. ZZ /\ 0 <_ ( j - 1 ) ) )
91 25 29 89 90 syl3anbrc 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
92 elfzel2 
 |-  ( j e. ( 0 ... M ) -> M e. ZZ )
93 92 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
94 1red 
 |-  ( j e. ( 0 ... M ) -> 1 e. RR )
95 34 94 resubcld 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
96 92 zred 
 |-  ( j e. ( 0 ... M ) -> M e. RR )
97 34 ltm1d 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
98 elfzle2 
 |-  ( j e. ( 0 ... M ) -> j <_ M )
99 95 34 96 97 98 ltletrd 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
100 99 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
101 elfzo2 
 |-  ( ( j - 1 ) e. ( 0 ..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
102 91 93 100 101 syl3anbrc 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ..^ M ) )
103 17 18 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
104 103 3ad2ant1 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
105 25 93 29 3jca 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
106 95 96 99 ltled 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
107 106 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
108 105 89 107 jca32 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
109 elfz2 
 |-  ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
110 108 109 sylibr 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
111 104 110 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
112 111 rexrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
113 34 recnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
114 1cnd 
 |-  ( j e. ( 0 ... M ) -> 1 e. CC )
115 113 114 npcand 
 |-  ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
116 115 fveq2d 
 |-  ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
117 116 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
118 103 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
119 118 rexrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
120 117 119 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
121 120 3adant3 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
122 id 
 |-  ( x = X -> x = X )
123 fveq2 
 |-  ( x = X -> ( Z ` x ) = ( Z ` X ) )
124 122 123 oveq12d 
 |-  ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
125 124 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
126 7 a1i 
 |-  ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
127 oveq2 
 |-  ( x = X -> ( B - x ) = ( B - X ) )
128 127 oveq1d 
 |-  ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
129 128 fveq2d 
 |-  ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
130 129 oveq1d 
 |-  ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
131 130 adantl 
 |-  ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
132 2 6 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
133 132 56 64 redivcld 
 |-  ( ph -> ( ( B - X ) / T ) e. RR )
134 133 flcld 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
135 134 zred 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
136 135 56 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
137 126 131 6 136 fvmptd 
 |-  ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
138 137 136 eqeltrd 
 |-  ( ph -> ( Z ` X ) e. RR )
139 6 138 readdcld 
 |-  ( ph -> ( X + ( Z ` X ) ) e. RR )
140 51 125 6 139 fvmptd 
 |-  ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
141 140 139 eqeltrd 
 |-  ( ph -> ( E ` X ) e. RR )
142 141 rexrd 
 |-  ( ph -> ( E ` X ) e. RR* )
143 142 3ad2ant1 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
144 simp1 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
145 ovex 
 |-  ( j - 1 ) e. _V
146 eleq1 
 |-  ( i = ( j - 1 ) -> ( i e. ( 0 ..^ M ) <-> ( j - 1 ) e. ( 0 ..^ M ) ) )
147 146 anbi2d 
 |-  ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) ) )
148 fveq2 
 |-  ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
149 oveq1 
 |-  ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
150 149 fveq2d 
 |-  ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
151 148 150 breq12d 
 |-  ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
152 147 151 imbi12d 
 |-  ( i = ( j - 1 ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
153 16 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
154 153 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
155 145 152 154 vtocl 
 |-  ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
156 144 102 155 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
157 116 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
158 156 157 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
159 simp3 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
160 158 159 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
161 141 leidd 
 |-  ( ph -> ( E ` X ) <_ ( E ` X ) )
162 161 adantr 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
163 46 eqcomd 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
164 162 163 breqtrd 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
165 164 3adant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
166 115 eqcomd 
 |-  ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
167 166 fveq2d 
 |-  ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
168 167 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
169 165 168 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( ( j - 1 ) + 1 ) ) )
170 112 121 143 160 169 eliocd 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
171 148 150 oveq12d 
 |-  ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
172 171 eleq2d 
 |-  ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
173 172 rspcev 
 |-  ( ( ( j - 1 ) e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
174 102 170 173 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
175 174 3exp 
 |-  ( ph -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) ) )
176 175 adantr 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) ) )
177 176 rexlimdv 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
178 24 177 mpd 
 |-  ( ( ph /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
179 10 adantr 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
180 103 adantr 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
181 iocssicc 
 |-  ( ( Q ` 0 ) (,] ( Q ` M ) ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) )
182 41 simprd 
 |-  ( ph -> ( Q ` M ) = B )
183 42 182 oveq12d 
 |-  ( ph -> ( ( Q ` 0 ) (,] ( Q ` M ) ) = ( A (,] B ) )
184 77 183 eleqtrrd 
 |-  ( ph -> ( E ` X ) e. ( ( Q ` 0 ) (,] ( Q ` M ) ) )
185 181 184 sseldi 
 |-  ( ph -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
186 185 adantr 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
187 simpr 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
188 fveq2 
 |-  ( k = j -> ( Q ` k ) = ( Q ` j ) )
189 188 breq1d 
 |-  ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
190 189 cbvrabv 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) }
191 190 supeq1i 
 |-  sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
192 179 180 186 187 191 fourierdlem25 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
193 ioossioc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
194 193 a1i 
 |-  ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
195 194 sseld 
 |-  ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
196 195 reximdva 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
197 192 196 mpd 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
198 178 197 pm2.61dan 
 |-  ( ph -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
199 103 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
200 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
201 200 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
202 199 201 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
203 202 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
204 138 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
205 203 204 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
206 141 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
207 203 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
208 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
209 208 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
210 199 209 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
211 210 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
212 211 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
213 simp3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
214 iocgtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
215 207 212 213 214 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
216 203 206 204 215 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < ( ( E ` X ) - ( Z ` X ) ) )
217 140 oveq1d 
 |-  ( ph -> ( ( E ` X ) - ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
218 6 recnd 
 |-  ( ph -> X e. CC )
219 138 recnd 
 |-  ( ph -> ( Z ` X ) e. CC )
220 218 219 pncand 
 |-  ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
221 217 220 eqtrd 
 |-  ( ph -> ( ( E ` X ) - ( Z ` X ) ) = X )
222 221 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
223 216 222 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
224 elioore 
 |-  ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
225 137 oveq2d 
 |-  ( ph -> ( y + ( Z ` X ) ) = ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
226 135 recnd 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
227 56 recnd 
 |-  ( ph -> T e. CC )
228 226 227 mulneg1d 
 |-  ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
229 225 228 oveq12d 
 |-  ( ph -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
230 229 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
231 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
232 136 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
233 231 232 readdcld 
 |-  ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
234 233 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. CC )
235 232 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
236 234 235 negsubd 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
237 231 recnd 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
238 237 235 pncand 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = y )
239 230 236 238 3eqtrrd 
 |-  ( ( ph /\ y e. RR ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
240 224 239 sylan2 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
241 240 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
242 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
243 12 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
244 243 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
245 207 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
246 212 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
247 224 adantl 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
248 138 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
249 247 248 readdcld 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
250 249 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
251 138 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. RR )
252 202 251 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
253 252 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
254 253 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
255 6 rexrd 
 |-  ( ph -> X e. RR* )
256 255 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
257 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
258 ioogtlb 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
259 254 256 257 258 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
260 202 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
261 138 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
262 224 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
263 260 261 262 ltsubaddd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
264 259 263 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
265 264 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
266 242 141 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR )
267 210 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
268 267 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
269 6 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
270 iooltub 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
271 254 256 257 270 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
272 262 269 261 271 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
273 140 eqcomd 
 |-  ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
274 273 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
275 272 274 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
276 275 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
277 iocleub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
278 207 212 213 277 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
279 278 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
280 250 266 268 276 279 ltletrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
281 245 246 250 265 280 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
282 244 281 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. D )
283 242 133 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( B - X ) / T ) e. RR )
284 283 flcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
285 284 znegcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
286 negex 
 |-  -u ( |_ ` ( ( B - X ) / T ) ) e. _V
287 eleq1 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
288 287 3anbi3d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
289 oveq1 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
290 289 oveq2d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
291 290 eleq1d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
292 288 291 imbi12d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) ) )
293 ovex 
 |-  ( y + ( Z ` X ) ) e. _V
294 eleq1 
 |-  ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
295 294 3anbi2d 
 |-  ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
296 oveq1 
 |-  ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
297 296 eleq1d 
 |-  ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
298 295 297 imbi12d 
 |-  ( x = ( y + ( Z ` X ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) ) )
299 293 298 5 vtocl 
 |-  ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
300 286 292 299 vtocl 
 |-  ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
301 242 282 285 300 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
302 241 301 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
303 302 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
304 dfss3 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
305 303 304 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
306 breq1 
 |-  ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y < X <-> ( ( Q ` i ) - ( Z ` X ) ) < X ) )
307 oveq1 
 |-  ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y (,) X ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
308 307 sseq1d 
 |-  ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y (,) X ) C_ D <-> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) )
309 306 308 anbi12d 
 |-  ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y < X /\ ( y (,) X ) C_ D ) <-> ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) ) )
310 309 rspcev 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR /\ ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
311 205 223 305 310 syl12anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
312 311 3exp 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) ) ) )
313 312 rexlimdv 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) ) )
314 198 313 mpd 
 |-  ( ph -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
315 0zd 
 |-  ( ph -> 0 e. ZZ )
316 10 nnzd 
 |-  ( ph -> M e. ZZ )
317 1zzd 
 |-  ( ph -> 1 e. ZZ )
318 315 316 317 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) )
319 0le1 
 |-  0 <_ 1
320 319 a1i 
 |-  ( ph -> 0 <_ 1 )
321 10 nnge1d 
 |-  ( ph -> 1 <_ M )
322 318 320 321 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
323 elfz2 
 |-  ( 1 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
324 322 323 sylibr 
 |-  ( ph -> 1 e. ( 0 ... M ) )
325 103 324 ffvelrnd 
 |-  ( ph -> ( Q ` 1 ) e. RR )
326 138 56 resubcld 
 |-  ( ph -> ( ( Z ` X ) - T ) e. RR )
327 325 326 resubcld 
 |-  ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
328 327 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
329 1 recnd 
 |-  ( ph -> A e. CC )
330 329 227 pncand 
 |-  ( ph -> ( ( A + T ) - T ) = A )
331 330 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( A + T ) - T ) = A )
332 4 oveq2i 
 |-  ( A + T ) = ( A + ( B - A ) )
333 332 a1i 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( A + T ) = ( A + ( B - A ) ) )
334 2 recnd 
 |-  ( ph -> B e. CC )
335 329 334 pncan3d 
 |-  ( ph -> ( A + ( B - A ) ) = B )
336 335 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( A + ( B - A ) ) = B )
337 id 
 |-  ( ( E ` X ) = B -> ( E ` X ) = B )
338 337 eqcomd 
 |-  ( ( E ` X ) = B -> B = ( E ` X ) )
339 338 adantl 
 |-  ( ( ph /\ ( E ` X ) = B ) -> B = ( E ` X ) )
340 333 336 339 3eqtrrd 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( E ` X ) = ( A + T ) )
341 340 oveq1d 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( ( A + T ) - T ) )
342 42 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = A )
343 331 341 342 3eqtr4rd 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( ( E ` X ) - T ) )
344 343 oveq1d 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) = ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) )
345 141 recnd 
 |-  ( ph -> ( E ` X ) e. CC )
346 345 219 227 nnncan2d 
 |-  ( ph -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
347 346 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
348 221 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
349 344 347 348 3eqtrrd 
 |-  ( ( ph /\ ( E ` X ) = B ) -> X = ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) )
350 42 1 eqeltrd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
351 10 nngt0d 
 |-  ( ph -> 0 < M )
352 fzolb 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
353 315 316 351 352 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
354 0re 
 |-  0 e. RR
355 eleq1 
 |-  ( i = 0 -> ( i e. ( 0 ..^ M ) <-> 0 e. ( 0 ..^ M ) ) )
356 355 anbi2d 
 |-  ( i = 0 -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ 0 e. ( 0 ..^ M ) ) ) )
357 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
358 oveq1 
 |-  ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
359 358 fveq2d 
 |-  ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
360 357 359 breq12d 
 |-  ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
361 356 360 imbi12d 
 |-  ( i = 0 -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
362 361 154 vtoclg 
 |-  ( 0 e. RR -> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
363 354 362 ax-mp 
 |-  ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
364 353 363 mpdan 
 |-  ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
365 0p1e1 
 |-  ( 0 + 1 ) = 1
366 365 fveq2i 
 |-  ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
367 366 a1i 
 |-  ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
368 364 367 breqtrd 
 |-  ( ph -> ( Q ` 0 ) < ( Q ` 1 ) )
369 350 325 326 368 ltsub1dd 
 |-  ( ph -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
370 369 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
371 349 370 eqbrtrd 
 |-  ( ( ph /\ ( E ` X ) = B ) -> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
372 elioore 
 |-  ( y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) -> y e. RR )
373 137 eqcomd 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( Z ` X ) )
374 373 negeqd 
 |-  ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
375 228 374 eqtrd 
 |-  ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
376 227 mulid2d 
 |-  ( ph -> ( 1 x. T ) = T )
377 375 376 oveq12d 
 |-  ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) = ( -u ( Z ` X ) + T ) )
378 226 negcld 
 |-  ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. CC )
379 1cnd 
 |-  ( ph -> 1 e. CC )
380 378 379 227 adddird 
 |-  ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) )
381 219 227 negsubdid 
 |-  ( ph -> -u ( ( Z ` X ) - T ) = ( -u ( Z ` X ) + T ) )
382 377 380 381 3eqtr4d 
 |-  ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = -u ( ( Z ` X ) - T ) )
383 382 oveq2d 
 |-  ( ph -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
384 383 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
385 326 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. RR )
386 231 385 readdcld 
 |-  ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
387 386 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. CC )
388 385 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. CC )
389 387 388 negsubd 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) = ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) )
390 237 388 pncand 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) = y )
391 384 389 390 3eqtrrd 
 |-  ( ( ph /\ y e. RR ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
392 372 391 sylan2 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
393 392 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
394 simpll 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ph )
395 367 eqcomd 
 |-  ( ph -> ( Q ` 1 ) = ( Q ` ( 0 + 1 ) ) )
396 395 oveq2d 
 |-  ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
397 357 359 oveq12d 
 |-  ( i = 0 -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
398 397 sseq1d 
 |-  ( i = 0 -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D <-> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
399 356 398 imbi12d 
 |-  ( i = 0 -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D ) <-> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) ) )
400 399 12 vtoclg 
 |-  ( 0 e. RR -> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
401 354 400 ax-mp 
 |-  ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
402 353 401 mpdan 
 |-  ( ph -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
403 396 402 eqsstrd 
 |-  ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
404 403 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
405 42 47 eqeltrd 
 |-  ( ph -> ( Q ` 0 ) e. RR* )
406 405 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) e. RR* )
407 325 rexrd 
 |-  ( ph -> ( Q ` 1 ) e. RR* )
408 407 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR* )
409 372 386 sylan2 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
410 409 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
411 345 218 219 subaddd 
 |-  ( ph -> ( ( ( E ` X ) - X ) = ( Z ` X ) <-> ( X + ( Z ` X ) ) = ( E ` X ) ) )
412 273 411 mpbird 
 |-  ( ph -> ( ( E ` X ) - X ) = ( Z ` X ) )
413 oveq1 
 |-  ( ( E ` X ) = B -> ( ( E ` X ) - X ) = ( B - X ) )
414 412 413 sylan9req 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( Z ` X ) = ( B - X ) )
415 414 oveq1d 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( Z ` X ) - T ) = ( ( B - X ) - T ) )
416 415 oveq2d 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( Z ` X ) - T ) ) = ( X + ( ( B - X ) - T ) ) )
417 132 recnd 
 |-  ( ph -> ( B - X ) e. CC )
418 218 417 227 addsubassd 
 |-  ( ph -> ( ( X + ( B - X ) ) - T ) = ( X + ( ( B - X ) - T ) ) )
419 418 eqcomd 
 |-  ( ph -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
420 419 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
421 334 227 329 subsub23d 
 |-  ( ph -> ( ( B - T ) = A <-> ( B - A ) = T ) )
422 62 421 mpbird 
 |-  ( ph -> ( B - T ) = A )
423 218 334 pncan3d 
 |-  ( ph -> ( X + ( B - X ) ) = B )
424 423 oveq1d 
 |-  ( ph -> ( ( X + ( B - X ) ) - T ) = ( B - T ) )
425 422 424 42 3eqtr4d 
 |-  ( ph -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
426 425 adantr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
427 416 420 426 3eqtrrd 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
428 427 adantr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
429 6 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR )
430 372 adantl 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. RR )
431 326 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Z ` X ) - T ) e. RR )
432 255 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR* )
433 327 rexrd 
 |-  ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
434 433 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
435 simpr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
436 ioogtlb 
 |-  ( ( X e. RR* /\ ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X < y )
437 432 434 435 436 syl3anc 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X < y )
438 429 430 431 437 ltadd1dd 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( X + ( ( Z ` X ) - T ) ) < ( y + ( ( Z ` X ) - T ) ) )
439 438 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( X + ( ( Z ` X ) - T ) ) < ( y + ( ( Z ` X ) - T ) ) )
440 428 439 eqbrtrd 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) < ( y + ( ( Z ` X ) - T ) ) )
441 iooltub 
 |-  ( ( X e. RR* /\ ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
442 432 434 435 441 syl3anc 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
443 325 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR )
444 430 431 443 ltaddsubd 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) <-> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
445 442 444 mpbird 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) )
446 445 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) )
447 406 408 410 440 446 eliood 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. ( ( Q ` 0 ) (,) ( Q ` 1 ) ) )
448 404 447 sseldd 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. D )
449 134 znegcld 
 |-  ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
450 449 peano2zd 
 |-  ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ )
451 450 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ )
452 ovex 
 |-  ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. _V
453 eleq1 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( k e. ZZ <-> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) )
454 453 3anbi3d 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) ) )
455 oveq1 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( k x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) )
456 455 oveq2d 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
457 456 eleq1d 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D <-> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D ) )
458 454 457 imbi12d 
 |-  ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D ) ) )
459 ovex 
 |-  ( y + ( ( Z ` X ) - T ) ) e. _V
460 eleq1 
 |-  ( x = ( y + ( ( Z ` X ) - T ) ) -> ( x e. D <-> ( y + ( ( Z ` X ) - T ) ) e. D ) )
461 460 3anbi2d 
 |-  ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) ) )
462 oveq1 
 |-  ( x = ( y + ( ( Z ` X ) - T ) ) -> ( x + ( k x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) )
463 462 eleq1d 
 |-  ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) )
464 461 463 imbi12d 
 |-  ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) ) )
465 459 464 5 vtocl 
 |-  ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D )
466 452 458 465 vtocl 
 |-  ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D )
467 394 448 451 466 syl3anc 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D )
468 393 467 eqeltrd 
 |-  ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. D )
469 468 ralrimiva 
 |-  ( ( ph /\ ( E ` X ) = B ) -> A. y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) y e. D )
470 dfss3 
 |-  ( ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D <-> A. y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) y e. D )
471 469 470 sylibr 
 |-  ( ( ph /\ ( E ` X ) = B ) -> ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D )
472 breq2 
 |-  ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( X < y <-> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
473 oveq2 
 |-  ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( X (,) y ) = ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
474 473 sseq1d 
 |-  ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( ( X (,) y ) C_ D <-> ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) )
475 472 474 anbi12d 
 |-  ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( ( X < y /\ ( X (,) y ) C_ D ) <-> ( X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) /\ ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) ) )
476 475 rspcev 
 |-  ( ( ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR /\ ( X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) /\ ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
477 328 371 471 476 syl12anc 
 |-  ( ( ph /\ ( E ` X ) = B ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
478 24 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
479 simp2 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( 0 ... M ) )
480 34 3ad2ant2 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
481 96 3ad2ant2 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. RR )
482 98 3ad2ant2 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j <_ M )
483 id 
 |-  ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
484 483 eqcomd 
 |-  ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
485 484 adantr 
 |-  ( ( ( Q ` j ) = ( E ` X ) /\ M = j ) -> ( E ` X ) = ( Q ` j ) )
486 485 3ad2antl3 
 |-  ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( E ` X ) = ( Q ` j ) )
487 fveq2 
 |-  ( M = j -> ( Q ` M ) = ( Q ` j ) )
488 487 eqcomd 
 |-  ( M = j -> ( Q ` j ) = ( Q ` M ) )
489 488 adantl 
 |-  ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( Q ` j ) = ( Q ` M ) )
490 182 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ M = j ) -> ( Q ` M ) = B )
491 490 3ad2antl1 
 |-  ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( Q ` M ) = B )
492 486 489 491 3eqtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( E ` X ) = B )
493 neneq 
 |-  ( ( E ` X ) =/= B -> -. ( E ` X ) = B )
494 493 ad2antlr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ M = j ) -> -. ( E ` X ) = B )
495 494 3ad2antl1 
 |-  ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> -. ( E ` X ) = B )
496 492 495 pm2.65da 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> -. M = j )
497 496 neqned 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M =/= j )
498 480 481 482 497 leneltd 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j < M )
499 elfzfzo 
 |-  ( j e. ( 0 ..^ M ) <-> ( j e. ( 0 ... M ) /\ j < M ) )
500 479 498 499 sylanbrc 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( 0 ..^ M ) )
501 119 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
502 501 3adant3 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
503 simp1l 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
504 103 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
505 fzofzp1 
 |-  ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
506 505 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
507 504 506 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
508 507 rexrd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
509 503 500 508 syl2anc 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
510 143 3adant1r 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
511 46 162 eqbrtrd 
 |-  ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
512 511 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
513 512 3adant2 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
514 484 3ad2ant3 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
515 eleq1 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
516 515 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ j e. ( 0 ..^ M ) ) ) )
517 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
518 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
519 518 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
520 517 519 breq12d 
 |-  ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
521 516 520 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) ) )
522 521 154 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
523 503 500 522 syl2anc 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
524 514 523 eqbrtrd 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) < ( Q ` ( j + 1 ) ) )
525 502 509 510 513 524 elicod 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
526 517 519 oveq12d 
 |-  ( i = j -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
527 526 eleq2d 
 |-  ( i = j -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) )
528 527 rspcev 
 |-  ( ( j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
529 500 525 528 syl2anc 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
530 529 3exp 
 |-  ( ( ph /\ ( E ` X ) =/= B ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) ) )
531 530 adantr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) ) )
532 531 rexlimdv 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
533 478 532 mpd 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
534 ioossico 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) )
535 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
536 534 535 sseldi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
537 536 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
538 537 adantlr 
 |-  ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
539 538 reximdva 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
540 192 539 mpd 
 |-  ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
541 540 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) =/= B ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
542 533 541 pm2.61dan 
 |-  ( ( ph /\ ( E ` X ) =/= B ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
543 210 251 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
544 543 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
545 221 eqcomd 
 |-  ( ph -> X = ( ( E ` X ) - ( Z ` X ) ) )
546 545 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> X = ( ( E ` X ) - ( Z ` X ) ) )
547 141 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
548 210 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
549 138 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
550 202 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
551 550 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
552 211 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
553 simp3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
554 icoltub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < ( Q ` ( i + 1 ) ) )
555 551 552 553 554 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < ( Q ` ( i + 1 ) ) )
556 547 548 549 555 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
557 546 556 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
558 elioore 
 |-  ( y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) -> y e. RR )
559 558 239 sylan2 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
560 559 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
561 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ph )
562 12 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
563 562 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
564 551 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) e. RR* )
565 552 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
566 558 adantl 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. RR )
567 138 adantr 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Z ` X ) e. RR )
568 566 567 readdcld 
 |-  ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. RR )
569 568 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. RR )
570 202 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
571 570 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) e. RR )
572 561 141 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) e. RR )
573 icogelb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
574 551 552 553 573 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
575 574 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
576 140 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
577 6 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X e. RR )
578 558 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. RR )
579 138 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Z ` X ) e. RR )
580 255 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X e. RR* )
581 543 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* )
582 581 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* )
583 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
584 ioogtlb 
 |-  ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X < y )
585 580 582 583 584 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X < y )
586 577 578 579 585 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( X + ( Z ` X ) ) < ( y + ( Z ` X ) ) )
587 576 586 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) < ( y + ( Z ` X ) ) )
588 587 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) < ( y + ( Z ` X ) ) )
589 571 572 569 575 588 lelttrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
590 543 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
591 iooltub 
 |-  ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
592 580 582 583 591 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
593 578 590 579 592 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) )
594 210 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
595 219 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. CC )
596 594 595 npcand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` ( i + 1 ) ) )
597 596 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` ( i + 1 ) ) )
598 593 597 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
599 598 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
600 564 565 569 589 599 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
601 563 600 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. D )
602 561 449 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
603 561 601 602 300 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
604 560 603 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. D )
605 604 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) y e. D )
606 dfss3 
 |-  ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D <-> A. y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) y e. D )
607 605 606 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D )
608 breq2 
 |-  ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( X < y <-> X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
609 oveq2 
 |-  ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( X (,) y ) = ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
610 609 sseq1d 
 |-  ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( ( X (,) y ) C_ D <-> ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) )
611 608 610 anbi12d 
 |-  ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( ( X < y /\ ( X (,) y ) C_ D ) <-> ( X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) /\ ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) ) )
612 611 rspcev 
 |-  ( ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR /\ ( X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) /\ ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
613 544 557 607 612 syl12anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
614 613 3exp 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) ) )
615 614 adantr 
 |-  ( ( ph /\ ( E ` X ) =/= B ) -> ( i e. ( 0 ..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) ) )
616 615 rexlimdv 
 |-  ( ( ph /\ ( E ` X ) =/= B ) -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )
617 542 616 mpd 
 |-  ( ( ph /\ ( E ` X ) =/= B ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
618 477 617 pm2.61dane 
 |-  ( ph -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
619 314 618 jca 
 |-  ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )