Metamath Proof Explorer

Theorem fourierdlem49

Description: The given periodic function F has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem49.a 
|- ( ph -> A e. RR )
fourierdlem49.b 
|- ( ph -> B e. RR )
fourierdlem49.altb 
|- ( ph -> A < B )
fourierdlem49.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 ) ) ) } )
fourierdlem49.t 
|- T = ( B - A )
fourierdlem49.m 
|- ( ph -> M e. NN )
fourierdlem49.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem49.d 
|- ( ph -> D C_ RR )
fourierdlem49.f 
|- ( ph -> F : D --> RR )
fourierdlem49.dper 
|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
fourierdlem49.per 
|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
fourierdlem49.cn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem49.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem49.x 
|- ( ph -> X e. RR )
fourierdlem49.z 
|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
fourierdlem49.e 
|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
Assertion fourierdlem49 
|- ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )

Proof

Step Hyp Ref Expression
1 fourierdlem49.a 
 |-  ( ph -> A e. RR )
2 fourierdlem49.b 
 |-  ( ph -> B e. RR )
3 fourierdlem49.altb 
 |-  ( ph -> A < B )
4 fourierdlem49.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 ) ) ) } )
5 fourierdlem49.t 
 |-  T = ( B - A )
6 fourierdlem49.m 
 |-  ( ph -> M e. NN )
7 fourierdlem49.q 
 |-  ( ph -> Q e. ( P ` M ) )
8 fourierdlem49.d 
 |-  ( ph -> D C_ RR )
9 fourierdlem49.f 
 |-  ( ph -> F : D --> RR )
10 fourierdlem49.dper 
 |-  ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
11 fourierdlem49.per 
 |-  ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
12 fourierdlem49.cn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
13 fourierdlem49.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
14 fourierdlem49.x 
 |-  ( ph -> X e. RR )
15 fourierdlem49.z 
 |-  Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
16 fourierdlem49.e 
 |-  E = ( x e. RR |-> ( x + ( Z ` x ) ) )
17 ovex 
 |-  ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
18 15 fvmpt2 
 |-  ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
19 17 18 mpan2 
 |-  ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
20 19 oveq2d 
 |-  ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
21 20 mpteq2ia 
 |-  ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
22 16 21 eqtri 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
23 1 2 3 5 22 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
24 23 14 ffvelrnd 
 |-  ( ph -> ( E ` X ) e. ( A (,] B ) )
25 simpr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
26 4 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 ) ) ) ) ) )
27 6 26 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 ) ) ) ) ) )
28 7 27 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
29 28 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
30 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
31 29 30 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
32 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
33 31 32 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
34 33 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
35 fvelrnb 
 |-  ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
36 34 35 syl 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
37 25 36 mpbid 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
38 1zzd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
39 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
40 39 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
41 1e0p1 
 |-  1 = ( 0 + 1 )
42 41 a1i 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 = ( 0 + 1 ) )
43 40 zred 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
44 elfzle1 
 |-  ( j e. ( 0 ... M ) -> 0 <_ j )
45 44 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ j )
46 id 
 |-  ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
47 46 eqcomd 
 |-  ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
48 47 ad2antlr 
 |-  ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
49 fveq2 
 |-  ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
50 49 adantl 
 |-  ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
51 28 simprld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
52 51 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
54 48 50 53 3eqtrd 
 |-  ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
55 54 adantllr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
56 55 adantllr 
 |-  ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
57 1 adantr 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
58 1 rexrd 
 |-  ( ph -> A e. RR* )
59 58 adantr 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
60 2 rexrd 
 |-  ( ph -> B e. RR* )
61 60 adantr 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
62 simpr 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
63 iocgtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
64 59 61 62 63 syl3anc 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
65 57 64 gtned 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
66 65 neneqd 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
67 66 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> -. ( E ` X ) = A )
68 56 67 pm2.65da 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
69 68 neqned 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
70 43 45 69 ne0gt0d 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
71 0zd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
72 zltp1le 
 |-  ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
73 71 40 72 syl2anc 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
74 70 73 mpbid 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
75 42 74 eqbrtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
76 eluz2 
 |-  ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
77 38 40 75 76 syl3anbrc 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
78 nnuz 
 |-  NN = ( ZZ>= ` 1 )
79 77 78 eleqtrrdi 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
80 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
81 79 80 syl 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. NN0 )
82 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
83 82 a1i 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> NN0 = ( ZZ>= ` 0 ) )
84 81 83 eleqtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
85 6 nnzd 
 |-  ( ph -> M e. ZZ )
86 85 ad3antrrr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
87 peano2zm 
 |-  ( j e. ZZ -> ( j - 1 ) e. ZZ )
88 39 87 syl 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) e. ZZ )
89 88 zred 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
90 39 zred 
 |-  ( j e. ( 0 ... M ) -> j e. RR )
91 elfzel2 
 |-  ( j e. ( 0 ... M ) -> M e. ZZ )
92 91 zred 
 |-  ( j e. ( 0 ... M ) -> M e. RR )
93 90 ltm1d 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
94 elfzle2 
 |-  ( j e. ( 0 ... M ) -> j <_ M )
95 89 90 92 93 94 ltletrd 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
96 95 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
97 elfzo2 
 |-  ( ( j - 1 ) e. ( 0 ..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
98 84 86 96 97 syl3anbrc 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ..^ M ) )
99 31 ad3antrrr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
100 40 87 syl 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
101 81 nn0ge0d 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
102 89 92 95 ltled 
 |-  ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
103 102 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
104 71 86 100 101 103 elfzd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
105 99 104 ffvelrnd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
106 105 rexrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
107 31 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
108 107 rexrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
109 108 adantlr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
110 109 adantr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
111 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
112 58 2 111 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
113 112 sselda 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
114 113 rexrd 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
115 114 ad2antrr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
116 simplll 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
117 ovex 
 |-  ( j - 1 ) e. _V
118 eleq1 
 |-  ( i = ( j - 1 ) -> ( i e. ( 0 ..^ M ) <-> ( j - 1 ) e. ( 0 ..^ M ) ) )
119 118 anbi2d 
 |-  ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) ) )
120 fveq2 
 |-  ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
121 oveq1 
 |-  ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
122 121 fveq2d 
 |-  ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
123 120 122 breq12d 
 |-  ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
124 119 123 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 ) ) ) ) )
125 28 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
126 125 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
127 117 124 126 vtocl 
 |-  ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
128 116 98 127 syl2anc 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
129 39 zcnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
130 1cnd 
 |-  ( j e. ( 0 ... M ) -> 1 e. CC )
131 129 130 npcand 
 |-  ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
132 131 eqcomd 
 |-  ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
133 132 fveq2d 
 |-  ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
134 133 eqcomd 
 |-  ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
135 134 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
136 128 135 breqtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
137 simpr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
138 136 137 breqtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
139 112 24 sseldd 
 |-  ( ph -> ( E ` X ) e. RR )
140 139 leidd 
 |-  ( ph -> ( E ` X ) <_ ( E ` X ) )
141 140 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
142 47 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
143 141 142 breqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
144 143 adantllr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
145 106 110 115 138 144 eliocd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) )
146 133 oveq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
147 146 ad2antlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
148 145 147 eleqtrd 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
149 120 122 oveq12d 
 |-  ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
150 149 eleq2d 
 |-  ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
151 150 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 ) ) ) )
152 98 148 151 syl2anc 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
153 152 ex 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
154 153 adantlr 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] 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 ) ) ) ) )
155 154 rexlimdva 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] 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 ) ) ) ) )
156 37 155 mpd 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
157 6 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
158 31 ad2antrr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
159 iocssicc 
 |-  ( A (,] B ) C_ ( A [,] B )
160 52 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
161 51 simprd 
 |-  ( ph -> ( Q ` M ) = B )
162 161 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
163 160 162 oveq12d 
 |-  ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
164 159 163 sseqtrid 
 |-  ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
165 164 sselda 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
166 165 adantr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
167 simpr 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
168 fveq2 
 |-  ( k = j -> ( Q ` k ) = ( Q ` j ) )
169 168 breq1d 
 |-  ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
170 169 cbvrabv 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) }
171 170 supeq1i 
 |-  sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
172 157 158 166 167 171 fourierdlem25 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
173 ioossioc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
174 173 sseli 
 |-  ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
175 174 a1i 
 |-  ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( 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 ) ) ) ) )
176 175 reximdva 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( 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 ) ) ) ) )
177 172 176 mpd 
 |-  ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
178 156 177 pm2.61dan 
 |-  ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
179 24 178 mpdan 
 |-  ( ph -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
180 frel 
 |-  ( F : D --> RR -> Rel F )
181 9 180 syl 
 |-  ( ph -> Rel F )
182 resindm 
 |-  ( Rel F -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) ) )
183 182 eqcomd 
 |-  ( Rel F -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
184 181 183 syl 
 |-  ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
185 fdm 
 |-  ( F : D --> RR -> dom F = D )
186 9 185 syl 
 |-  ( ph -> dom F = D )
187 186 ineq2d 
 |-  ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
188 187 reseq2d 
 |-  ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
189 184 188 eqtrd 
 |-  ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
190 189 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
191 190 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) limCC ( E ` X ) ) )
192 ax-resscn 
 |-  RR C_ CC
193 192 a1i 
 |-  ( ph -> RR C_ CC )
194 9 193 fssd 
 |-  ( ph -> F : D --> CC )
195 194 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
196 inss2 
 |-  ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D
197 196 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D )
198 195 197 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) : ( ( -oo (,) ( E ` X ) ) i^i D ) --> CC )
199 mnfxr 
 |-  -oo e. RR*
200 199 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo e. RR* )
201 31 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
202 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
203 202 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
204 201 203 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
205 204 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
206 204 mnfltd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo < ( Q ` i ) )
207 200 205 206 xrltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( Q ` i ) )
208 iooss1 
 |-  ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
209 199 207 208 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
210 209 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
211 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
212 211 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
213 201 212 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
214 213 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
215 214 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
216 204 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
217 216 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
218 simp3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
219 iocleub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
220 217 215 218 219 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
221 iooss2 
 |-  ( ( ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) <_ ( Q ` ( i + 1 ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
222 215 220 221 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
223 cncff 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
224 fdm 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
225 12 223 224 3syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
226 ssdmres 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
227 225 226 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
228 186 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = D )
229 227 228 sseqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
230 229 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
231 222 230 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
232 210 231 ssind 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( -oo (,) ( E ` X ) ) i^i D ) )
233 8 193 sstrd 
 |-  ( ph -> D C_ CC )
234 233 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
235 196 234 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
236 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
237 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
238 139 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
239 238 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
240 iocgtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
241 217 215 218 240 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
242 238 leidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( E ` X ) )
243 217 239 239 241 242 eliocd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
244 ioounsn 
 |-  ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ ( Q ` i ) < ( E ` X ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
245 217 239 241 244 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
246 245 fveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) )
247 236 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
248 ovex 
 |-  ( -oo (,) ( E ` X ) ) e. _V
249 248 inex1 
 |-  ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
250 snex 
 |-  { ( E ` X ) } e. _V
251 249 250 unex 
 |-  ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
252 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top )
253 247 251 252 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
254 retop 
 |-  ( topGen ` ran (,) ) e. Top
255 254 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( topGen ` ran (,) ) e. Top )
256 251 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V )
257 iooretop 
 |-  ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) )
258 257 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) )
259 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V /\ ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
260 255 256 258 259 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
261 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
262 pnfxr 
 |-  +oo e. RR*
263 262 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> +oo e. RR* )
264 238 ltpnfd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
265 217 263 238 241 264 eliood 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
266 snidg 
 |-  ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
267 elun2 
 |-  ( ( E ` X ) e. { ( E ` X ) } -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
268 266 267 syl 
 |-  ( ( E ` X ) e. RR -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
269 139 268 syl 
 |-  ( ph -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
270 269 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
271 265 270 elind 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
272 271 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
273 261 272 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
274 273 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
275 217 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
276 262 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> +oo e. RR* )
277 205 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
278 139 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E ` X ) e. RR )
279 278 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
280 iocssre 
 |-  ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
281 277 279 280 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
282 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
283 281 282 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
284 283 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
285 279 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
286 iocgtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
287 277 285 282 286 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
288 287 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
289 284 ltpnfd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x < +oo )
290 275 276 284 288 289 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
291 290 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
292 199 a1i 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo e. RR* )
293 285 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
294 283 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
295 294 mnfltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
296 139 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
297 iocleub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
298 277 285 282 297 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
299 298 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
300 neqne 
 |-  ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
301 300 necomd 
 |-  ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
302 301 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
303 294 296 299 302 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
304 292 293 294 295 303 eliood 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
305 304 3adantll3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
306 230 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
307 275 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) e. RR* )
308 215 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
309 284 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
310 288 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) < x )
311 238 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
312 214 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
313 303 3adantll3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
314 220 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
315 309 311 312 313 314 ltletrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( Q ` ( i + 1 ) ) )
316 307 308 309 310 315 eliood 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
317 306 316 sseldd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. D )
318 305 317 elind 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
319 elun1 
 |-  ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
320 318 319 syl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
321 291 320 elind 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
322 274 321 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
323 217 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
324 239 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( E ` X ) e. RR* )
325 elinel1 
 |-  ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
326 elioore 
 |-  ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
327 326 rexrd 
 |-  ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR* )
328 325 327 syl 
 |-  ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. RR* )
329 328 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. RR* )
330 205 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
331 262 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> +oo e. RR* )
332 325 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
333 ioogtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ +oo e. RR* /\ x e. ( ( Q ` i ) (,) +oo ) ) -> ( Q ` i ) < x )
334 330 331 332 333 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
335 334 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
336 elinel2 
 |-  ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
337 elsni 
 |-  ( x e. { ( E ` X ) } -> x = ( E ` X ) )
338 337 adantl 
 |-  ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
339 140 adantr 
 |-  ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
340 338 339 eqbrtrd 
 |-  ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
341 340 adantlr 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
342 simpll 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> ph )
343 elunnel2 
 |-  ( ( x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
344 343 adantll 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
345 elinel1 
 |-  ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( -oo (,) ( E ` X ) ) )
346 elioore 
 |-  ( x e. ( -oo (,) ( E ` X ) ) -> x e. RR )
347 346 adantl 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. RR )
348 139 adantr 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR )
349 199 a1i 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> -oo e. RR* )
350 348 rexrd 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR* )
351 simpr 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. ( -oo (,) ( E ` X ) ) )
352 iooltub 
 |-  ( ( -oo e. RR* /\ ( E ` X ) e. RR* /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
353 349 350 351 352 syl3anc 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
354 347 348 353 ltled 
 |-  ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x <_ ( E ` X ) )
355 345 354 sylan2 
 |-  ( ( ph /\ x e. ( ( -oo (,) ( E ` X ) ) i^i D ) ) -> x <_ ( E ` X ) )
356 342 344 355 syl2anc 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
357 341 356 pm2.61dan 
 |-  ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
358 357 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
359 336 358 sylan2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
360 359 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
361 323 324 329 335 360 eliocd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
362 322 361 impbida 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( Q ` i ) (,] ( E ` X ) ) <-> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) )
363 362 eqrdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
364 ioossre 
 |-  ( -oo (,) ( E ` X ) ) C_ RR
365 ssinss1 
 |-  ( ( -oo (,) ( E ` X ) ) C_ RR -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
366 364 365 mp1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
367 238 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { ( E ` X ) } C_ RR )
368 366 367 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR )
369 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
370 236 369 rerest 
 |-  ( ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
371 368 370 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
372 260 363 371 3eltr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
373 isopn3i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top /\ ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
374 253 372 373 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
375 246 374 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
376 243 375 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
377 198 232 235 236 237 376 limcres 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) limCC ( E ` X ) ) )
378 232 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
379 378 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
380 191 377 379 3eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
381 186 feq2d 
 |-  ( ph -> ( F : dom F --> CC <-> F : D --> CC ) )
382 194 381 mpbird 
 |-  ( ph -> F : dom F --> CC )
383 382 adantr 
 |-  ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> F : dom F --> CC )
384 383 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> F : dom F --> CC )
385 ioosscn 
 |-  ( ( Q ` i ) (,) ( E ` X ) ) C_ CC
386 385 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ CC )
387 186 eqcomd 
 |-  ( ph -> D = dom F )
388 387 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D = dom F )
389 231 388 sseqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
390 389 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
391 15 a1i 
 |-  ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
392 oveq2 
 |-  ( x = X -> ( B - x ) = ( B - X ) )
393 392 oveq1d 
 |-  ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
394 393 fveq2d 
 |-  ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
395 394 oveq1d 
 |-  ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
396 395 adantl 
 |-  ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
397 2 14 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
398 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
399 5 398 eqeltrid 
 |-  ( ph -> T e. RR )
400 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
401 3 400 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
402 5 eqcomi 
 |-  ( B - A ) = T
403 402 a1i 
 |-  ( ph -> ( B - A ) = T )
404 401 403 breqtrd 
 |-  ( ph -> 0 < T )
405 404 gt0ne0d 
 |-  ( ph -> T =/= 0 )
406 397 399 405 redivcld 
 |-  ( ph -> ( ( B - X ) / T ) e. RR )
407 406 flcld 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
408 407 zred 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
409 408 399 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
410 391 396 14 409 fvmptd 
 |-  ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
411 410 409 eqeltrd 
 |-  ( ph -> ( Z ` X ) e. RR )
412 411 recnd 
 |-  ( ph -> ( Z ` X ) e. CC )
413 412 adantr 
 |-  ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
414 413 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
415 414 negcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> -u ( Z ` X ) e. CC )
416 eqid 
 |-  { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) }
417 ioosscn 
 |-  ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC
418 417 sseli 
 |-  ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. CC )
419 418 adantl 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. CC )
420 412 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. CC )
421 419 420 pncand 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = y )
422 421 eqcomd 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) - ( Z ` X ) ) )
423 422 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 ) ) - ( Z ` X ) ) )
424 410 oveq2d 
 |-  ( ph -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
425 424 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
426 419 420 addcld 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. CC )
427 409 recnd 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
428 427 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
429 426 428 negsubd 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
430 407 zcnd 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
431 399 recnd 
 |-  ( ph -> T e. CC )
432 430 431 mulneg1d 
 |-  ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
433 432 eqcomd 
 |-  ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
434 433 oveq2d 
 |-  ( ph -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
435 434 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
436 425 429 435 3eqtr2d 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
437 436 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
438 407 znegcld 
 |-  ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
439 438 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
440 439 3ad2antl1 
 |-  ( ( ( 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 )
441 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
442 231 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
443 205 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
444 139 rexrd 
 |-  ( ph -> ( E ` X ) e. RR* )
445 444 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR* )
446 elioore 
 |-  ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
447 446 adantl 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
448 411 adantr 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
449 447 448 readdcld 
 |-  ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
450 449 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
451 411 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. RR )
452 204 451 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
453 452 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
454 453 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
455 14 rexrd 
 |-  ( ph -> X e. RR* )
456 455 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
457 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
458 ioogtlb 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
459 454 456 457 458 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
460 204 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
461 451 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
462 446 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
463 460 461 462 ltsubaddd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
464 459 463 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
465 14 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
466 iooltub 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
467 454 456 457 466 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
468 462 465 461 467 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
469 16 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
470 id 
 |-  ( x = X -> x = X )
471 fveq2 
 |-  ( x = X -> ( Z ` x ) = ( Z ` X ) )
472 470 471 oveq12d 
 |-  ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
473 472 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
474 14 411 readdcld 
 |-  ( ph -> ( X + ( Z ` X ) ) e. RR )
475 469 473 14 474 fvmptd 
 |-  ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
476 475 eqcomd 
 |-  ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
477 476 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
478 468 477 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
479 443 445 450 464 478 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( E ` X ) ) )
480 479 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. ( ( Q ` i ) (,) ( E ` X ) ) )
481 442 480 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 )
482 441 481 440 3jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
483 eleq1 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
484 483 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 ) ) )
485 oveq1 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
486 485 oveq2d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
487 486 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 ) )
488 484 487 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 ) ) )
489 ovex 
 |-  ( y + ( Z ` X ) ) e. _V
490 eleq1 
 |-  ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
491 490 3anbi2d 
 |-  ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
492 oveq1 
 |-  ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
493 492 eleq1d 
 |-  ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
494 491 493 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 ) ) )
495 489 494 10 vtocl 
 |-  ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
496 488 495 vtoclg 
 |-  ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
497 440 482 496 sylc 
 |-  ( ( ( 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 )
498 437 497 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) e. D )
499 423 498 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
500 499 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 )
501 dfss3 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
502 500 501 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
503 204 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
504 412 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. CC )
505 503 504 negsubd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + -u ( Z ` X ) ) = ( ( Q ` i ) - ( Z ` X ) ) )
506 505 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) = ( ( Q ` i ) + -u ( Z ` X ) ) )
507 475 oveq1d 
 |-  ( ph -> ( ( E ` X ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) )
508 474 recnd 
 |-  ( ph -> ( X + ( Z ` X ) ) e. CC )
509 508 412 negsubd 
 |-  ( ph -> ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
510 14 recnd 
 |-  ( ph -> X e. CC )
511 510 412 pncand 
 |-  ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
512 507 509 511 3eqtrrd 
 |-  ( ph -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
513 512 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
514 506 513 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) = ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) )
515 451 renegcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u ( Z ` X ) e. RR )
516 204 278 515 iooshift 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } )
517 514 516 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
518 517 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
519 186 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> dom F = D )
520 502 518 519 3sstr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
521 520 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
522 410 negeqd 
 |-  ( ph -> -u ( Z ` X ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
523 522 433 eqtrd 
 |-  ( ph -> -u ( Z ` X ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
524 523 oveq2d 
 |-  ( ph -> ( x + -u ( Z ` X ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
525 524 fveq2d 
 |-  ( ph -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
526 525 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
527 526 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
528 438 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
529 528 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
530 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ph )
531 231 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> x e. D )
532 530 531 529 3jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
533 483 3anbi3d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
534 485 oveq2d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
535 534 fveq2d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
536 535 eqeq1d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
537 533 536 imbi12d 
 |-  ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
538 537 11 vtoclg 
 |-  ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
539 529 532 538 sylc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
540 527 539 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
541 540 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
542 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
543 384 386 390 415 416 521 541 542 limcperiod 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) )
544 517 reseq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
545 513 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) + -u ( Z ` X ) ) = X )
546 544 545 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
547 546 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
548 547 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
549 543 548 eleqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
550 382 adantr 
 |-  ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> F : dom F --> CC )
551 550 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> F : dom F --> CC )
552 417 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC )
553 502 519 sseqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
554 553 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
555 412 adantr 
 |-  ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( Z ` X ) e. CC )
556 555 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( Z ` X ) e. CC )
557 eqid 
 |-  { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) }
558 503 504 npcand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` i ) )
559 558 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) )
560 475 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
561 559 560 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) )
562 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
563 452 562 451 iooshift 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } )
564 561 563 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
565 564 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
566 231 565 519 3sstr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
567 566 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
568 410 oveq2d 
 |-  ( ph -> ( x + ( Z ` X ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
569 568 fveq2d 
 |-  ( ph -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
570 569 adantr 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
571 570 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
572 407 adantr 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
573 572 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
574 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
575 502 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. D )
576 574 575 573 3jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
577 eleq1 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
578 577 3anbi3d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
579 oveq1 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
580 579 oveq2d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
581 580 fveq2d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
582 581 eqeq1d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
583 578 582 imbi12d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
584 583 11 vtoclg 
 |-  ( ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
585 573 576 584 sylc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
586 571 585 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
587 586 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
588 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
589 551 552 554 556 557 567 587 588 limcperiod 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) )
590 564 reseq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
591 476 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
592 590 591 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
593 592 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
594 593 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
595 589 594 eleqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
596 549 595 impbida 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) <-> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) )
597 596 eqrdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
598 resindm 
 |-  ( Rel F -> ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( -oo (,) X ) ) )
599 598 eqcomd 
 |-  ( Rel F -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i dom F ) ) )
600 181 599 syl 
 |-  ( ph -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i dom F ) ) )
601 186 ineq2d 
 |-  ( ph -> ( ( -oo (,) X ) i^i dom F ) = ( ( -oo (,) X ) i^i D ) )
602 601 reseq2d 
 |-  ( ph -> ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
603 600 602 eqtrd 
 |-  ( ph -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
604 603 oveq1d 
 |-  ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
605 604 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
606 inss2 
 |-  ( ( -oo (,) X ) i^i D ) C_ D
607 606 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ D )
608 195 607 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) X ) i^i D ) ) : ( ( -oo (,) X ) i^i D ) --> CC )
609 452 mnfltd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo < ( ( Q ` i ) - ( Z ` X ) ) )
610 200 453 609 xrltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( ( Q ` i ) - ( Z ` X ) ) )
611 iooss1 
 |-  ( ( -oo e. RR* /\ -oo <_ ( ( Q ` i ) - ( Z ` X ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
612 199 610 611 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
613 612 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
614 613 502 ssind 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( ( -oo (,) X ) i^i D ) )
615 606 234 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ CC )
616 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
617 453 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
618 455 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR* )
619 475 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
620 241 619 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + ( Z ` X ) ) )
621 411 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
622 14 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
623 216 621 622 ltsubaddd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < X <-> ( Q ` i ) < ( X + ( Z ` X ) ) ) )
624 620 623 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
625 14 leidd 
 |-  ( ph -> X <_ X )
626 625 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X <_ X )
627 617 618 618 624 626 eliocd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
628 ioounsn 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ ( ( Q ` i ) - ( Z ` X ) ) < X ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
629 617 618 624 628 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
630 629 fveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) )
631 ovex 
 |-  ( -oo (,) X ) e. _V
632 631 inex1 
 |-  ( ( -oo (,) X ) i^i D ) e. _V
633 snex 
 |-  { X } e. _V
634 632 633 unex 
 |-  ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V
635 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top )
636 247 634 635 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top
637 634 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V )
638 iooretop 
 |-  ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) )
639 638 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) )
640 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
641 255 637 639 640 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
642 453 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
643 262 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> +oo e. RR* )
644 14 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR )
645 iocssre 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
646 642 644 645 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
647 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
648 646 647 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. RR )
649 455 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR* )
650 iocgtlb 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
651 642 649 647 650 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
652 648 ltpnfd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x < +oo )
653 642 643 648 651 652 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
654 653 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
655 eqvisset 
 |-  ( x = X -> X e. _V )
656 snidg 
 |-  ( X e. _V -> X e. { X } )
657 655 656 syl 
 |-  ( x = X -> X e. { X } )
658 470 657 eqeltrd 
 |-  ( x = X -> x e. { X } )
659 elun2 
 |-  ( x e. { X } -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
660 658 659 syl 
 |-  ( x = X -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
661 660 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
662 simpll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
663 642 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
664 455 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR* )
665 648 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. RR )
666 651 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
667 14 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR )
668 iocleub 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x <_ X )
669 642 649 647 668 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x <_ X )
670 669 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x <_ X )
671 470 eqcoms 
 |-  ( X = x -> x = X )
672 671 necon3bi 
 |-  ( -. x = X -> X =/= x )
673 672 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X =/= x )
674 665 667 670 673 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x < X )
675 663 664 665 666 674 eliood 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
676 675 3adantll3 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
677 614 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( -oo (,) X ) i^i D ) )
678 elun1 
 |-  ( x e. ( ( -oo (,) X ) i^i D ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
679 677 678 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
680 662 676 679 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
681 661 680 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
682 654 681 elind 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
683 617 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
684 618 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> X e. RR* )
685 elinel1 
 |-  ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
686 elioore 
 |-  ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) -> x e. RR )
687 685 686 syl 
 |-  ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR )
688 687 rexrd 
 |-  ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR* )
689 688 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. RR* )
690 453 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
691 262 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> +oo e. RR* )
692 685 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
693 ioogtlb 
 |-  ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ +oo e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
694 690 691 692 693 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
695 694 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
696 elinel2 
 |-  ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
697 elsni 
 |-  ( x e. { X } -> x = X )
698 697 adantl 
 |-  ( ( ph /\ x e. { X } ) -> x = X )
699 625 adantr 
 |-  ( ( ph /\ x e. { X } ) -> X <_ X )
700 698 699 eqbrtrd 
 |-  ( ( ph /\ x e. { X } ) -> x <_ X )
701 700 adantlr 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ x e. { X } ) -> x <_ X )
702 simpll 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> ph )
703 elunnel2 
 |-  ( ( x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
704 703 adantll 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
705 elinel1 
 |-  ( x e. ( ( -oo (,) X ) i^i D ) -> x e. ( -oo (,) X ) )
706 704 705 syl 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( -oo (,) X ) )
707 elioore 
 |-  ( x e. ( -oo (,) X ) -> x e. RR )
708 707 adantl 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. RR )
709 14 adantr 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR )
710 199 a1i 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> -oo e. RR* )
711 455 adantr 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR* )
712 simpr 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. ( -oo (,) X ) )
713 iooltub 
 |-  ( ( -oo e. RR* /\ X e. RR* /\ x e. ( -oo (,) X ) ) -> x < X )
714 710 711 712 713 syl3anc 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> x < X )
715 708 709 714 ltled 
 |-  ( ( ph /\ x e. ( -oo (,) X ) ) -> x <_ X )
716 702 706 715 syl2anc 
 |-  ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x <_ X )
717 701 716 pm2.61dan 
 |-  ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x <_ X )
718 696 717 sylan2 
 |-  ( ( ph /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
719 718 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
720 683 684 689 695 719 eliocd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
721 682 720 impbida 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) <-> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) )
722 721 eqrdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
723 606 8 sstrid 
 |-  ( ph -> ( ( -oo (,) X ) i^i D ) C_ RR )
724 14 snssd 
 |-  ( ph -> { X } C_ RR )
725 723 724 unssd 
 |-  ( ph -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
726 725 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
727 236 369 rerest 
 |-  ( ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
728 726 727 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
729 641 722 728 3eltr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
730 isopn3i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
731 636 729 730 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
732 630 731 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
733 627 732 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
734 608 614 615 236 616 733 limcres 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
735 734 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) = ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
736 614 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
737 736 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
738 605 735 737 3eqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X ) )
739 380 597 738 3eqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
740 739 rexlimdv3a 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) )
741 179 740 mpd 
 |-  ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
742 126 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
743 12 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
744 13 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
745 eqid 
 |-  if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) = if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) )
746 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
747 216 214 742 743 744 216 238 241 222 745 746 fourierdlem33 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
748 222 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
749 748 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
750 747 749 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
751 ne0i 
 |-  ( if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
752 750 751 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
753 380 752 eqnetrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
754 753 rexlimdv3a 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) ) )
755 179 754 mpd 
 |-  ( ph -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
756 741 755 eqnetrd 
 |-  ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )