This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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