Metamath Proof Explorer

Theorem fourierdlem46

Description: The function F has a limit at the bounds of every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem46.cn 
|- ( ph -> F e. ( dom F -cn-> CC ) )
fourierdlem46.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom F ) ) -> ( ( F |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierdlem46.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom F ) ) -> ( ( F |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierdlem46.qiso 
|- ( ph -> Q Isom < , < ( ( 0 ... M ) , H ) )
fourierdlem46.qf 
|- ( ph -> Q : ( 0 ... M ) --> H )
fourierdlem46.i 
|- ( ph -> I e. ( 0 ..^ M ) )
fourierdlem46.10 
|- ( ph -> ( Q ` I ) < ( Q ` ( I + 1 ) ) )
fourierdlem46.qiss 
|- ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( -u _pi (,) _pi ) )
fourierdlem46.c 
|- ( ph -> C e. RR )
fourierdlem46.h 
|- H = ( { -u _pi , _pi , C } u. ( ( -u _pi [,] _pi ) \ dom F ) )
fourierdlem46.ranq 
|- ( ph -> ran Q = H )
Assertion fourierdlem46 
|- ( ph -> ( ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) /\ ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem46.cn 
 |-  ( ph -> F e. ( dom F -cn-> CC ) )
2 fourierdlem46.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom F ) ) -> ( ( F |` ( x (,) +oo ) ) limCC x ) =/= (/) )
3 fourierdlem46.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom F ) ) -> ( ( F |` ( -oo (,) x ) ) limCC x ) =/= (/) )
4 fourierdlem46.qiso 
 |-  ( ph -> Q Isom < , < ( ( 0 ... M ) , H ) )
5 fourierdlem46.qf 
 |-  ( ph -> Q : ( 0 ... M ) --> H )
6 fourierdlem46.i 
 |-  ( ph -> I e. ( 0 ..^ M ) )
7 fourierdlem46.10 
 |-  ( ph -> ( Q ` I ) < ( Q ` ( I + 1 ) ) )
8 fourierdlem46.qiss 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( -u _pi (,) _pi ) )
9 fourierdlem46.c 
 |-  ( ph -> C e. RR )
10 fourierdlem46.h 
 |-  H = ( { -u _pi , _pi , C } u. ( ( -u _pi [,] _pi ) \ dom F ) )
11 fourierdlem46.ranq 
 |-  ( ph -> ran Q = H )
12 pire 
 |-  _pi e. RR
13 12 a1i 
 |-  ( ph -> _pi e. RR )
14 13 renegcld 
 |-  ( ph -> -u _pi e. RR )
15 tpssi 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ C e. RR ) -> { -u _pi , _pi , C } C_ RR )
16 14 13 9 15 syl3anc 
 |-  ( ph -> { -u _pi , _pi , C } C_ RR )
17 14 13 iccssred 
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
18 17 ssdifssd 
 |-  ( ph -> ( ( -u _pi [,] _pi ) \ dom F ) C_ RR )
19 16 18 unssd 
 |-  ( ph -> ( { -u _pi , _pi , C } u. ( ( -u _pi [,] _pi ) \ dom F ) ) C_ RR )
20 10 19 eqsstrid 
 |-  ( ph -> H C_ RR )
21 elfzofz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ( 0 ... M ) )
22 6 21 syl 
 |-  ( ph -> I e. ( 0 ... M ) )
23 5 22 ffvelrnd 
 |-  ( ph -> ( Q ` I ) e. H )
24 20 23 sseldd 
 |-  ( ph -> ( Q ` I ) e. RR )
25 24 adantr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( Q ` I ) e. RR )
26 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
27 6 26 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
28 5 27 ffvelrnd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. H )
29 20 28 sseldd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR )
30 29 rexrd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
31 30 adantr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. RR* )
32 7 adantr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( Q ` I ) < ( Q ` ( I + 1 ) ) )
33 simpr 
 |-  ( ( ( Q ` I ) e. dom F /\ x = ( Q ` I ) ) -> x = ( Q ` I ) )
34 simpl 
 |-  ( ( ( Q ` I ) e. dom F /\ x = ( Q ` I ) ) -> ( Q ` I ) e. dom F )
35 33 34 eqeltrd 
 |-  ( ( ( Q ` I ) e. dom F /\ x = ( Q ` I ) ) -> x e. dom F )
36 35 adantll 
 |-  ( ( ( ph /\ ( Q ` I ) e. dom F ) /\ x = ( Q ` I ) ) -> x e. dom F )
37 36 adantlr 
 |-  ( ( ( ( ph /\ ( Q ` I ) e. dom F ) /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ x = ( Q ` I ) ) -> x e. dom F )
38 ssun2 
 |-  ( ( -u _pi [,] _pi ) \ dom F ) C_ ( { -u _pi , _pi , C } u. ( ( -u _pi [,] _pi ) \ dom F ) )
39 38 10 sseqtrri 
 |-  ( ( -u _pi [,] _pi ) \ dom F ) C_ H
40 ioossicc 
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
41 8 40 sstrdi 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
42 41 sselda 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. ( -u _pi [,] _pi ) )
43 42 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. ( -u _pi [,] _pi ) )
44 simpr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> -. x e. dom F )
45 43 44 eldifd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. ( ( -u _pi [,] _pi ) \ dom F ) )
46 39 45 sselid 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. H )
47 11 eqcomd 
 |-  ( ph -> H = ran Q )
48 47 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> H = ran Q )
49 46 48 eleqtrd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. ran Q )
50 simpr 
 |-  ( ( ph /\ x e. ran Q ) -> x e. ran Q )
51 ffn 
 |-  ( Q : ( 0 ... M ) --> H -> Q Fn ( 0 ... M ) )
52 5 51 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
53 52 adantr 
 |-  ( ( ph /\ x e. ran Q ) -> Q Fn ( 0 ... M ) )
54 fvelrnb 
 |-  ( Q Fn ( 0 ... M ) -> ( x e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = x ) )
55 53 54 syl 
 |-  ( ( ph /\ x e. ran Q ) -> ( x e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = x ) )
56 50 55 mpbid 
 |-  ( ( ph /\ x e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = x )
57 56 adantlr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ x e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = x )
58 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
59 58 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ x e. ran Q ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> j e. ZZ )
60 simplll 
 |-  ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> ph )
61 simplr 
 |-  ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> j e. ( 0 ... M ) )
62 simpr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ ( Q ` j ) = x ) -> ( Q ` j ) = x )
63 simplr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ ( Q ` j ) = x ) -> x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
64 62 63 eqeltrd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ ( Q ` j ) = x ) -> ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
65 64 adantlr 
 |-  ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
66 elfzoelz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ZZ )
67 6 66 syl 
 |-  ( ph -> I e. ZZ )
68 67 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> I e. ZZ )
69 24 rexrd 
 |-  ( ph -> ( Q ` I ) e. RR* )
70 69 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) e. RR* )
71 30 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
72 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
73 ioogtlb 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < ( Q ` j ) )
74 70 71 72 73 syl3anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < ( Q ` j ) )
75 4 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> Q Isom < , < ( ( 0 ... M ) , H ) )
76 22 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> I e. ( 0 ... M ) )
77 simplr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> j e. ( 0 ... M ) )
78 isorel 
 |-  ( ( Q Isom < , < ( ( 0 ... M ) , H ) /\ ( I e. ( 0 ... M ) /\ j e. ( 0 ... M ) ) ) -> ( I < j <-> ( Q ` I ) < ( Q ` j ) ) )
79 75 76 77 78 syl12anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( I < j <-> ( Q ` I ) < ( Q ` j ) ) )
80 74 79 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> I < j )
81 iooltub 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` j ) < ( Q ` ( I + 1 ) ) )
82 70 71 72 81 syl3anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` j ) < ( Q ` ( I + 1 ) ) )
83 27 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( I + 1 ) e. ( 0 ... M ) )
84 isorel 
 |-  ( ( Q Isom < , < ( ( 0 ... M ) , H ) /\ ( j e. ( 0 ... M ) /\ ( I + 1 ) e. ( 0 ... M ) ) ) -> ( j < ( I + 1 ) <-> ( Q ` j ) < ( Q ` ( I + 1 ) ) ) )
85 75 77 83 84 syl12anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( j < ( I + 1 ) <-> ( Q ` j ) < ( Q ` ( I + 1 ) ) ) )
86 82 85 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> j < ( I + 1 ) )
87 btwnnz 
 |-  ( ( I e. ZZ /\ I < j /\ j < ( I + 1 ) ) -> -. j e. ZZ )
88 68 80 86 87 syl3anc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> -. j e. ZZ )
89 60 61 65 88 syl21anc 
 |-  ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> -. j e. ZZ )
90 89 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ x e. ran Q ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = x ) -> -. j e. ZZ )
91 59 90 pm2.65da 
 |-  ( ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ x e. ran Q ) /\ j e. ( 0 ... M ) ) -> -. ( Q ` j ) = x )
92 91 nrexdv 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ x e. ran Q ) -> -. E. j e. ( 0 ... M ) ( Q ` j ) = x )
93 57 92 pm2.65da 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> -. x e. ran Q )
94 93 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) /\ -. x e. dom F ) -> -. x e. ran Q )
95 49 94 condan 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. dom F )
96 95 ralrimiva 
 |-  ( ph -> A. x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) x e. dom F )
97 dfss3 
 |-  ( ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ dom F <-> A. x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) x e. dom F )
98 96 97 sylibr 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ dom F )
99 98 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ dom F )
100 69 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( Q ` I ) e. RR* )
101 30 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
102 icossre 
 |-  ( ( ( Q ` I ) e. RR /\ ( Q ` ( I + 1 ) ) e. RR* ) -> ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) C_ RR )
103 24 30 102 syl2anc 
 |-  ( ph -> ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) C_ RR )
104 103 sselda 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> x e. RR )
105 104 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x e. RR )
106 24 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( Q ` I ) e. RR )
107 69 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) e. RR* )
108 30 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
109 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) )
110 icogelb 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) <_ x )
111 107 108 109 110 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) <_ x )
112 111 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( Q ` I ) <_ x )
113 neqne 
 |-  ( -. x = ( Q ` I ) -> x =/= ( Q ` I ) )
114 113 adantl 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x =/= ( Q ` I ) )
115 106 105 112 114 leneltd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> ( Q ` I ) < x )
116 icoltub 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> x < ( Q ` ( I + 1 ) ) )
117 107 108 109 116 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> x < ( Q ` ( I + 1 ) ) )
118 117 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x < ( Q ` ( I + 1 ) ) )
119 100 101 105 115 118 eliood 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
120 99 119 sseldd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x e. dom F )
121 120 adantllr 
 |-  ( ( ( ( ph /\ ( Q ` I ) e. dom F ) /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` I ) ) -> x e. dom F )
122 37 121 pm2.61dan 
 |-  ( ( ( ph /\ ( Q ` I ) e. dom F ) /\ x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) -> x e. dom F )
123 122 ralrimiva 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> A. x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) x e. dom F )
124 dfss3 
 |-  ( ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) C_ dom F <-> A. x e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) x e. dom F )
125 123 124 sylibr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) C_ dom F )
126 1 adantr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> F e. ( dom F -cn-> CC ) )
127 rescncf 
 |-  ( ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) C_ dom F -> ( F e. ( dom F -cn-> CC ) -> ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) e. ( ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) -cn-> CC ) ) )
128 125 126 127 sylc 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) e. ( ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) -cn-> CC ) )
129 25 31 32 128 icocncflimc 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) ` ( Q ` I ) ) e. ( ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
130 24 leidd 
 |-  ( ph -> ( Q ` I ) <_ ( Q ` I ) )
131 69 30 69 130 7 elicod 
 |-  ( ph -> ( Q ` I ) e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) )
132 fvres 
 |-  ( ( Q ` I ) e. ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) -> ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) ` ( Q ` I ) ) = ( F ` ( Q ` I ) ) )
133 131 132 syl 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) ` ( Q ` I ) ) = ( F ` ( Q ` I ) ) )
134 133 eqcomd 
 |-  ( ph -> ( F ` ( Q ` I ) ) = ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) ` ( Q ` I ) ) )
135 134 adantr 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( F ` ( Q ` I ) ) = ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) ` ( Q ` I ) ) )
136 ioossico 
 |-  ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) )
137 136 a1i 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) )
138 137 resabs1d 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
139 138 eqcomd 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
140 139 oveq1d 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) = ( ( ( F |` ( ( Q ` I ) [,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
141 129 135 140 3eltr4d 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( F ` ( Q ` I ) ) e. ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
142 141 ne0d 
 |-  ( ( ph /\ ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) )
143 pnfxr 
 |-  +oo e. RR*
144 143 a1i 
 |-  ( ph -> +oo e. RR* )
145 29 ltpnfd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) < +oo )
146 30 144 145 xrltled 
 |-  ( ph -> ( Q ` ( I + 1 ) ) <_ +oo )
147 iooss2 
 |-  ( ( +oo e. RR* /\ ( Q ` ( I + 1 ) ) <_ +oo ) -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) (,) +oo ) )
148 143 146 147 sylancr 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) (,) +oo ) )
149 148 resabs1d 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
150 149 oveq1d 
 |-  ( ph -> ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) = ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
151 150 eqcomd 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) = ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
152 151 adantr 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) = ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) )
153 limcresi 
 |-  ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) C_ ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) )
154 24 adantr 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( Q ` I ) e. RR )
155 simpl 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ph )
156 12 renegcli 
 |-  -u _pi e. RR
157 156 rexri 
 |-  -u _pi e. RR*
158 157 a1i 
 |-  ( ph -> -u _pi e. RR* )
159 12 rexri 
 |-  _pi e. RR*
160 159 a1i 
 |-  ( ph -> _pi e. RR* )
161 14 13 24 29 7 8 fourierdlem10 
 |-  ( ph -> ( -u _pi <_ ( Q ` I ) /\ ( Q ` ( I + 1 ) ) <_ _pi ) )
162 161 simpld 
 |-  ( ph -> -u _pi <_ ( Q ` I ) )
163 161 simprd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) <_ _pi )
164 24 29 13 7 163 ltletrd 
 |-  ( ph -> ( Q ` I ) < _pi )
165 158 160 69 162 164 elicod 
 |-  ( ph -> ( Q ` I ) e. ( -u _pi [,) _pi ) )
166 165 adantr 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( Q ` I ) e. ( -u _pi [,) _pi ) )
167 simpr 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> -. ( Q ` I ) e. dom F )
168 166 167 eldifd 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) )
169 155 168 jca 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( ph /\ ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) ) )
170 eleq1 
 |-  ( x = ( Q ` I ) -> ( x e. ( ( -u _pi [,) _pi ) \ dom F ) <-> ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) ) )
171 170 anbi2d 
 |-  ( x = ( Q ` I ) -> ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom F ) ) <-> ( ph /\ ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) ) ) )
172 oveq1 
 |-  ( x = ( Q ` I ) -> ( x (,) +oo ) = ( ( Q ` I ) (,) +oo ) )
173 172 reseq2d 
 |-  ( x = ( Q ` I ) -> ( F |` ( x (,) +oo ) ) = ( F |` ( ( Q ` I ) (,) +oo ) ) )
174 id 
 |-  ( x = ( Q ` I ) -> x = ( Q ` I ) )
175 173 174 oveq12d 
 |-  ( x = ( Q ` I ) -> ( ( F |` ( x (,) +oo ) ) limCC x ) = ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) )
176 175 neeq1d 
 |-  ( x = ( Q ` I ) -> ( ( ( F |` ( x (,) +oo ) ) limCC x ) =/= (/) <-> ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) =/= (/) ) )
177 171 176 imbi12d 
 |-  ( x = ( Q ` I ) -> ( ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom F ) ) -> ( ( F |` ( x (,) +oo ) ) limCC x ) =/= (/) ) <-> ( ( ph /\ ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) ) -> ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) =/= (/) ) ) )
178 177 2 vtoclg 
 |-  ( ( Q ` I ) e. RR -> ( ( ph /\ ( Q ` I ) e. ( ( -u _pi [,) _pi ) \ dom F ) ) -> ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) =/= (/) ) )
179 154 169 178 sylc 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) =/= (/) )
180 ssn0 
 |-  ( ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) C_ ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) /\ ( ( F |` ( ( Q ` I ) (,) +oo ) ) limCC ( Q ` I ) ) =/= (/) ) -> ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) )
181 153 179 180 sylancr 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( ( ( F |` ( ( Q ` I ) (,) +oo ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) )
182 152 181 eqnetrd 
 |-  ( ( ph /\ -. ( Q ` I ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) )
183 142 182 pm2.61dan 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) )
184 69 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` I ) e. RR* )
185 29 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. RR )
186 7 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` I ) < ( Q ` ( I + 1 ) ) )
187 simpr 
 |-  ( ( ( Q ` ( I + 1 ) ) e. dom F /\ x = ( Q ` ( I + 1 ) ) ) -> x = ( Q ` ( I + 1 ) ) )
188 simpl 
 |-  ( ( ( Q ` ( I + 1 ) ) e. dom F /\ x = ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. dom F )
189 187 188 eqeltrd 
 |-  ( ( ( Q ` ( I + 1 ) ) e. dom F /\ x = ( Q ` ( I + 1 ) ) ) -> x e. dom F )
190 189 adantll 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) /\ x = ( Q ` ( I + 1 ) ) ) -> x e. dom F )
191 190 adantlr 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ x = ( Q ` ( I + 1 ) ) ) -> x e. dom F )
192 98 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ dom F )
193 69 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( Q ` I ) e. RR* )
194 30 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
195 69 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) e. RR* )
196 29 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) e. RR )
197 iocssre 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR ) -> ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) C_ RR )
198 195 196 197 syl2anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) C_ RR )
199 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) )
200 198 199 sseldd 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> x e. RR )
201 200 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x e. RR )
202 30 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
203 iocgtlb 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < x )
204 195 202 199 203 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < x )
205 204 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( Q ` I ) < x )
206 29 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. RR )
207 iocleub 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> x <_ ( Q ` ( I + 1 ) ) )
208 195 202 199 207 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> x <_ ( Q ` ( I + 1 ) ) )
209 208 adantr 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x <_ ( Q ` ( I + 1 ) ) )
210 neqne 
 |-  ( -. x = ( Q ` ( I + 1 ) ) -> x =/= ( Q ` ( I + 1 ) ) )
211 210 necomd 
 |-  ( -. x = ( Q ` ( I + 1 ) ) -> ( Q ` ( I + 1 ) ) =/= x )
212 211 adantl 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) =/= x )
213 201 206 209 212 leneltd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x < ( Q ` ( I + 1 ) ) )
214 193 194 201 205 213 eliood 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
215 192 214 sseldd 
 |-  ( ( ( ph /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x e. dom F )
216 215 adantllr 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) /\ -. x = ( Q ` ( I + 1 ) ) ) -> x e. dom F )
217 191 216 pm2.61dan 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) /\ x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) -> x e. dom F )
218 217 ralrimiva 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> A. x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) x e. dom F )
219 dfss3 
 |-  ( ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) C_ dom F <-> A. x e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) x e. dom F )
220 218 219 sylibr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) C_ dom F )
221 1 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> F e. ( dom F -cn-> CC ) )
222 rescncf 
 |-  ( ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) C_ dom F -> ( F e. ( dom F -cn-> CC ) -> ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) e. ( ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) -cn-> CC ) ) )
223 220 221 222 sylc 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) e. ( ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) -cn-> CC ) )
224 184 185 186 223 ioccncflimc 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) e. ( ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) )
225 29 leidd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) <_ ( Q ` ( I + 1 ) ) )
226 69 30 30 7 225 eliocd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) )
227 fvres 
 |-  ( ( Q ` ( I + 1 ) ) e. ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) -> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) = ( F ` ( Q ` ( I + 1 ) ) ) )
228 226 227 syl 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) = ( F ` ( Q ` ( I + 1 ) ) ) )
229 228 eqcomd 
 |-  ( ph -> ( F ` ( Q ` ( I + 1 ) ) ) = ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) )
230 ioossioc 
 |-  ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) )
231 resabs1 
 |-  ( ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) -> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
232 230 231 ax-mp 
 |-  ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
233 232 eqcomi 
 |-  ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
234 233 oveq1i 
 |-  ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) = ( ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) )
235 234 a1i 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) = ( ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) )
236 229 235 eleq12d 
 |-  ( ph -> ( ( F ` ( Q ` ( I + 1 ) ) ) e. ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) <-> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) e. ( ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) ) )
237 236 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F ` ( Q ` ( I + 1 ) ) ) e. ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) <-> ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) ` ( Q ` ( I + 1 ) ) ) e. ( ( ( F |` ( ( Q ` I ) (,] ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) ) )
238 224 237 mpbird 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( F ` ( Q ` ( I + 1 ) ) ) e. ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) )
239 238 ne0d 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
240 mnfxr 
 |-  -oo e. RR*
241 240 a1i 
 |-  ( ph -> -oo e. RR* )
242 24 mnfltd 
 |-  ( ph -> -oo < ( Q ` I ) )
243 241 69 242 xrltled 
 |-  ( ph -> -oo <_ ( Q ` I ) )
244 iooss1 
 |-  ( ( -oo e. RR* /\ -oo <_ ( Q ` I ) ) -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( -oo (,) ( Q ` ( I + 1 ) ) ) )
245 240 243 244 sylancr 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( -oo (,) ( Q ` ( I + 1 ) ) ) )
246 245 resabs1d 
 |-  ( ph -> ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
247 246 eqcomd 
 |-  ( ph -> ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
248 247 adantr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) = ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
249 248 oveq1d 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) = ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) )
250 limcresi 
 |-  ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) C_ ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) )
251 29 adantr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. RR )
252 simpl 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ph )
253 157 a1i 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> -u _pi e. RR* )
254 159 a1i 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> _pi e. RR* )
255 30 adantr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. RR* )
256 14 24 29 162 7 lelttrd 
 |-  ( ph -> -u _pi < ( Q ` ( I + 1 ) ) )
257 256 adantr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> -u _pi < ( Q ` ( I + 1 ) ) )
258 163 adantr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) <_ _pi )
259 253 254 255 257 258 eliocd 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. ( -u _pi (,] _pi ) )
260 simpr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> -. ( Q ` ( I + 1 ) ) e. dom F )
261 259 260 eldifd 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) )
262 252 261 jca 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( ph /\ ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) ) )
263 eleq1 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( x e. ( ( -u _pi (,] _pi ) \ dom F ) <-> ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) ) )
264 263 anbi2d 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom F ) ) <-> ( ph /\ ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) ) ) )
265 oveq2 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( -oo (,) x ) = ( -oo (,) ( Q ` ( I + 1 ) ) ) )
266 265 reseq2d 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( F |` ( -oo (,) x ) ) = ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) )
267 id 
 |-  ( x = ( Q ` ( I + 1 ) ) -> x = ( Q ` ( I + 1 ) ) )
268 266 267 oveq12d 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( ( F |` ( -oo (,) x ) ) limCC x ) = ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) )
269 268 neeq1d 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( ( ( F |` ( -oo (,) x ) ) limCC x ) =/= (/) <-> ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) )
270 264 269 imbi12d 
 |-  ( x = ( Q ` ( I + 1 ) ) -> ( ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom F ) ) -> ( ( F |` ( -oo (,) x ) ) limCC x ) =/= (/) ) <-> ( ( ph /\ ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) ) -> ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) ) )
271 270 3 vtoclg 
 |-  ( ( Q ` ( I + 1 ) ) e. RR -> ( ( ph /\ ( Q ` ( I + 1 ) ) e. ( ( -u _pi (,] _pi ) \ dom F ) ) -> ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) )
272 251 262 271 sylc 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
273 ssn0 
 |-  ( ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) C_ ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) /\ ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) -> ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
274 250 272 273 sylancr 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( ( F |` ( -oo (,) ( Q ` ( I + 1 ) ) ) ) |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
275 249 274 eqnetrd 
 |-  ( ( ph /\ -. ( Q ` ( I + 1 ) ) e. dom F ) -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
276 239 275 pm2.61dan 
 |-  ( ph -> ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) )
277 183 276 jca 
 |-  ( ph -> ( ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` I ) ) =/= (/) /\ ( ( F |` ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) limCC ( Q ` ( I + 1 ) ) ) =/= (/) ) )