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 sseldi
 |-  ( ( ( 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 ) ) ) =/= (/) ) )