Metamath Proof Explorer

Theorem fourierdlem20

Description: Every interval in the partition S is included in an interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem20.m 
|- ( ph -> M e. NN )
fourierdlem20.a 
|- ( ph -> A e. RR )
fourierdlem20.b 
|- ( ph -> B e. RR )
fourierdlem20.aleb 
|- ( ph -> A <_ B )
fourierdlem20.q 
|- ( ph -> Q : ( 0 ... M ) --> RR )
fourierdlem20.q0 
|- ( ph -> ( Q ` 0 ) <_ A )
fourierdlem20.qm 
|- ( ph -> B <_ ( Q ` M ) )
fourierdlem20.j 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem20.t 
|- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
fourierdlem20.s 
|- ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem20.i 
|- I = sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < )
Assertion fourierdlem20 
|- ( ph -> E. i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem20.m 
 |-  ( ph -> M e. NN )
2 fourierdlem20.a 
 |-  ( ph -> A e. RR )
3 fourierdlem20.b 
 |-  ( ph -> B e. RR )
4 fourierdlem20.aleb 
 |-  ( ph -> A <_ B )
5 fourierdlem20.q 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
6 fourierdlem20.q0 
 |-  ( ph -> ( Q ` 0 ) <_ A )
7 fourierdlem20.qm 
 |-  ( ph -> B <_ ( Q ` M ) )
8 fourierdlem20.j 
 |-  ( ph -> J e. ( 0 ..^ N ) )
9 fourierdlem20.t 
 |-  T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
10 fourierdlem20.s 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
11 fourierdlem20.i 
 |-  I = sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < )
12 ssrab2 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ ( 0 ..^ M )
13 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
14 fzssz 
 |-  ( 0 ... M ) C_ ZZ
15 13 14 sstri 
 |-  ( 0 ..^ M ) C_ ZZ
16 12 15 sstri 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ ZZ
17 16 a1i 
 |-  ( ph -> { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ ZZ )
18 0z 
 |-  0 e. ZZ
19 0le0 
 |-  0 <_ 0
20 eluz2 
 |-  ( 0 e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ 0 e. ZZ /\ 0 <_ 0 ) )
21 18 18 19 20 mpbir3an 
 |-  0 e. ( ZZ>= ` 0 )
22 21 a1i 
 |-  ( ph -> 0 e. ( ZZ>= ` 0 ) )
23 1 nnzd 
 |-  ( ph -> M e. ZZ )
24 1 nngt0d 
 |-  ( ph -> 0 < M )
25 elfzo2 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ 0 < M ) )
26 22 23 24 25 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
27 13 26 sselid 
 |-  ( ph -> 0 e. ( 0 ... M ) )
28 5 27 ffvelcdmd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
29 2 rexrd 
 |-  ( ph -> A e. RR* )
30 3 rexrd 
 |-  ( ph -> B e. RR* )
31 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
32 29 30 4 31 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
33 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
34 29 30 4 33 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
35 32 34 jca 
 |-  ( ph -> ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) )
36 prssg 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
37 29 30 36 syl2anc 
 |-  ( ph -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
38 35 37 mpbid 
 |-  ( ph -> { A , B } C_ ( A [,] B ) )
39 inss2 
 |-  ( ran Q i^i ( A (,) B ) ) C_ ( A (,) B )
40 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
41 39 40 sstri 
 |-  ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B )
42 41 a1i 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B ) )
43 38 42 unssd 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ ( A [,] B ) )
44 9 43 eqsstrid 
 |-  ( ph -> T C_ ( A [,] B ) )
45 2 3 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
46 44 45 sstrd 
 |-  ( ph -> T C_ RR )
47 isof1o 
 |-  ( S Isom < , < ( ( 0 ... N ) , T ) -> S : ( 0 ... N ) -1-1-onto-> T )
48 f1of 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) --> T )
49 10 47 48 3syl 
 |-  ( ph -> S : ( 0 ... N ) --> T )
50 elfzofz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) )
51 8 50 syl 
 |-  ( ph -> J e. ( 0 ... N ) )
52 49 51 ffvelcdmd 
 |-  ( ph -> ( S ` J ) e. T )
53 46 52 sseldd 
 |-  ( ph -> ( S ` J ) e. RR )
54 44 52 sseldd 
 |-  ( ph -> ( S ` J ) e. ( A [,] B ) )
55 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` J ) e. ( A [,] B ) ) -> A <_ ( S ` J ) )
56 29 30 54 55 syl3anc 
 |-  ( ph -> A <_ ( S ` J ) )
57 28 2 53 6 56 letrd 
 |-  ( ph -> ( Q ` 0 ) <_ ( S ` J ) )
58 fveq2 
 |-  ( k = 0 -> ( Q ` k ) = ( Q ` 0 ) )
59 58 breq1d 
 |-  ( k = 0 -> ( ( Q ` k ) <_ ( S ` J ) <-> ( Q ` 0 ) <_ ( S ` J ) ) )
60 59 elrab 
 |-  ( 0 e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } <-> ( 0 e. ( 0 ..^ M ) /\ ( Q ` 0 ) <_ ( S ` J ) ) )
61 26 57 60 sylanbrc 
 |-  ( ph -> 0 e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } )
62 61 ne0d 
 |-  ( ph -> { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } =/= (/) )
63 1 nnred 
 |-  ( ph -> M e. RR )
64 12 sseli 
 |-  ( j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } -> j e. ( 0 ..^ M ) )
65 elfzo0le 
 |-  ( j e. ( 0 ..^ M ) -> j <_ M )
66 64 65 syl 
 |-  ( j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } -> j <_ M )
67 66 adantl 
 |-  ( ( ph /\ j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } ) -> j <_ M )
68 67 ralrimiva 
 |-  ( ph -> A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ M )
69 breq2 
 |-  ( x = M -> ( j <_ x <-> j <_ M ) )
70 69 ralbidv 
 |-  ( x = M -> ( A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x <-> A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ M ) )
71 70 rspcev 
 |-  ( ( M e. RR /\ A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ M ) -> E. x e. RR A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x )
72 63 68 71 syl2anc 
 |-  ( ph -> E. x e. RR A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x )
73 suprzcl 
 |-  ( ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ ZZ /\ { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } =/= (/) /\ E. x e. RR A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x ) -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } )
74 17 62 72 73 syl3anc 
 |-  ( ph -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } )
75 12 74 sselid 
 |-  ( ph -> sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < ) e. ( 0 ..^ M ) )
76 11 75 eqeltrid 
 |-  ( ph -> I e. ( 0 ..^ M ) )
77 13 76 sselid 
 |-  ( ph -> I e. ( 0 ... M ) )
78 5 77 ffvelcdmd 
 |-  ( ph -> ( Q ` I ) e. RR )
79 78 rexrd 
 |-  ( ph -> ( Q ` I ) e. RR* )
80 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
81 76 80 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
82 5 81 ffvelcdmd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR )
83 82 rexrd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
84 11 74 eqeltrid 
 |-  ( ph -> I e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } )
85 nfrab1 
 |-  F/_ k { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) }
86 nfcv 
 |-  F/_ k RR
87 nfcv 
 |-  F/_ k <
88 85 86 87 nfsup 
 |-  F/_ k sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < )
89 11 88 nfcxfr 
 |-  F/_ k I
90 nfcv 
 |-  F/_ k ( 0 ..^ M )
91 nfcv 
 |-  F/_ k Q
92 91 89 nffv 
 |-  F/_ k ( Q ` I )
93 nfcv 
 |-  F/_ k <_
94 nfcv 
 |-  F/_ k ( S ` J )
95 92 93 94 nfbr 
 |-  F/ k ( Q ` I ) <_ ( S ` J )
96 fveq2 
 |-  ( k = I -> ( Q ` k ) = ( Q ` I ) )
97 96 breq1d 
 |-  ( k = I -> ( ( Q ` k ) <_ ( S ` J ) <-> ( Q ` I ) <_ ( S ` J ) ) )
98 89 90 95 97 elrabf 
 |-  ( I e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } <-> ( I e. ( 0 ..^ M ) /\ ( Q ` I ) <_ ( S ` J ) ) )
99 84 98 sylib 
 |-  ( ph -> ( I e. ( 0 ..^ M ) /\ ( Q ` I ) <_ ( S ` J ) ) )
100 99 simprd 
 |-  ( ph -> ( Q ` I ) <_ ( S ` J ) )
101 simpr 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) )
102 83 adantr 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
103 iccssxr 
 |-  ( A [,] B ) C_ RR*
104 44 103 sstrdi 
 |-  ( ph -> T C_ RR* )
105 fzofzp1 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
106 8 105 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... N ) )
107 49 106 ffvelcdmd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. T )
108 104 107 sseldd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR* )
109 108 adantr 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> ( S ` ( J + 1 ) ) e. RR* )
110 xrltnle 
 |-  ( ( ( Q ` ( I + 1 ) ) e. RR* /\ ( S ` ( J + 1 ) ) e. RR* ) -> ( ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) <-> -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) )
111 102 109 110 syl2anc 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> ( ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) <-> -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) )
112 101 111 mpbird 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) )
113 fzssz 
 |-  ( 0 ... N ) C_ ZZ
114 f1ofo 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) -onto-> T )
115 10 47 114 3syl 
 |-  ( ph -> S : ( 0 ... N ) -onto-> T )
116 115 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> S : ( 0 ... N ) -onto-> T )
117 ffun 
 |-  ( Q : ( 0 ... M ) --> RR -> Fun Q )
118 5 117 syl 
 |-  ( ph -> Fun Q )
119 5 fdmd 
 |-  ( ph -> dom Q = ( 0 ... M ) )
120 119 eqcomd 
 |-  ( ph -> ( 0 ... M ) = dom Q )
121 81 120 eleqtrd 
 |-  ( ph -> ( I + 1 ) e. dom Q )
122 fvelrn 
 |-  ( ( Fun Q /\ ( I + 1 ) e. dom Q ) -> ( Q ` ( I + 1 ) ) e. ran Q )
123 118 121 122 syl2anc 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. ran Q )
124 123 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. ran Q )
125 29 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> A e. RR* )
126 30 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> B e. RR* )
127 82 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. RR )
128 45 54 sseldd 
 |-  ( ph -> ( S ` J ) e. RR )
129 14 sseli 
 |-  ( I e. ( 0 ... M ) -> I e. ZZ )
130 zre 
 |-  ( I e. ZZ -> I e. RR )
131 77 129 130 3syl 
 |-  ( ph -> I e. RR )
132 131 adantr 
 |-  ( ( ph /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> I e. RR )
133 132 ltp1d 
 |-  ( ( ph /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> I < ( I + 1 ) )
134 133 adantlr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> I < ( I + 1 ) )
135 simplr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. RR )
136 128 ad2antrr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> ( S ` J ) e. RR )
137 simpr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> -. ( S ` J ) < ( Q ` ( I + 1 ) ) )
138 135 136 137 nltled 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> ( Q ` ( I + 1 ) ) <_ ( S ` J ) )
139 131 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> I e. RR )
140 1red 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> 1 e. RR )
141 139 140 readdcld 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( I + 1 ) e. RR )
142 elfzoelz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ZZ )
143 142 zred 
 |-  ( j e. ( 0 ..^ M ) -> j e. RR )
144 143 ssriv 
 |-  ( 0 ..^ M ) C_ RR
145 12 144 sstri 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ RR
146 145 a1i 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ RR )
147 62 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } =/= (/) )
148 72 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> E. x e. RR A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x )
149 82 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( Q ` ( I + 1 ) ) e. RR )
150 128 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( S ` J ) e. RR )
151 3 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> B e. RR )
152 simpr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( Q ` ( I + 1 ) ) <_ ( S ` J ) )
153 46 107 sseldd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR )
154 153 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( S ` ( J + 1 ) ) e. RR )
155 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
156 zre 
 |-  ( J e. ZZ -> J e. RR )
157 8 155 156 3syl 
 |-  ( ph -> J e. RR )
158 157 ltp1d 
 |-  ( ph -> J < ( J + 1 ) )
159 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( J e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( J < ( J + 1 ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
160 10 51 106 159 syl12anc 
 |-  ( ph -> ( J < ( J + 1 ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
161 158 160 mpbid 
 |-  ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
162 161 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
163 44 107 sseldd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. ( A [,] B ) )
164 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` ( J + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( J + 1 ) ) <_ B )
165 29 30 163 164 syl3anc 
 |-  ( ph -> ( S ` ( J + 1 ) ) <_ B )
166 165 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( S ` ( J + 1 ) ) <_ B )
167 150 154 151 162 166 ltletrd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( S ` J ) < B )
168 149 150 151 152 167 lelttrd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( Q ` ( I + 1 ) ) < B )
169 168 adantr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( I + 1 ) ) < B )
170 3 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> B e. RR )
171 82 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( I + 1 ) ) e. RR )
172 7 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> B <_ ( Q ` M ) )
173 23 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> M e. ZZ )
174 81 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( 0 ... M ) )
175 fzval3 
 |-  ( M e. ZZ -> ( 0 ... M ) = ( 0 ..^ ( M + 1 ) ) )
176 23 175 syl 
 |-  ( ph -> ( 0 ... M ) = ( 0 ..^ ( M + 1 ) ) )
177 176 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( 0 ... M ) = ( 0 ..^ ( M + 1 ) ) )
178 174 177 eleqtrd 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( 0 ..^ ( M + 1 ) ) )
179 simpr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> -. ( I + 1 ) e. ( 0 ..^ M ) )
180 178 179 jca 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( ( I + 1 ) e. ( 0 ..^ ( M + 1 ) ) /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) )
181 elfzonelfzo 
 |-  ( M e. ZZ -> ( ( ( I + 1 ) e. ( 0 ..^ ( M + 1 ) ) /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( M ..^ ( M + 1 ) ) ) )
182 173 180 181 sylc 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( M ..^ ( M + 1 ) ) )
183 fzval3 
 |-  ( M e. ZZ -> ( M ... M ) = ( M ..^ ( M + 1 ) ) )
184 23 183 syl 
 |-  ( ph -> ( M ... M ) = ( M ..^ ( M + 1 ) ) )
185 184 eqcomd 
 |-  ( ph -> ( M ..^ ( M + 1 ) ) = ( M ... M ) )
186 185 adantr 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( M ..^ ( M + 1 ) ) = ( M ... M ) )
187 182 186 eleqtrd 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( M ... M ) )
188 elfz1eq 
 |-  ( ( I + 1 ) e. ( M ... M ) -> ( I + 1 ) = M )
189 187 188 syl 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( I + 1 ) = M )
190 189 eqcomd 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> M = ( I + 1 ) )
191 190 fveq2d 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> ( Q ` M ) = ( Q ` ( I + 1 ) ) )
192 172 191 breqtrd 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> B <_ ( Q ` ( I + 1 ) ) )
193 170 171 192 lensymd 
 |-  ( ( ph /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> -. ( Q ` ( I + 1 ) ) < B )
194 193 adantlr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) /\ -. ( I + 1 ) e. ( 0 ..^ M ) ) -> -. ( Q ` ( I + 1 ) ) < B )
195 169 194 condan 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( I + 1 ) e. ( 0 ..^ M ) )
196 nfcv 
 |-  F/_ k +
197 nfcv 
 |-  F/_ k 1
198 89 196 197 nfov 
 |-  F/_ k ( I + 1 )
199 91 198 nffv 
 |-  F/_ k ( Q ` ( I + 1 ) )
200 199 93 94 nfbr 
 |-  F/ k ( Q ` ( I + 1 ) ) <_ ( S ` J )
201 fveq2 
 |-  ( k = ( I + 1 ) -> ( Q ` k ) = ( Q ` ( I + 1 ) ) )
202 201 breq1d 
 |-  ( k = ( I + 1 ) -> ( ( Q ` k ) <_ ( S ` J ) <-> ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) )
203 198 90 200 202 elrabf 
 |-  ( ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } <-> ( ( I + 1 ) e. ( 0 ..^ M ) /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) )
204 195 152 203 sylanbrc 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } )
205 suprub 
 |-  ( ( ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } C_ RR /\ { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } =/= (/) /\ E. x e. RR A. j e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } j <_ x ) /\ ( I + 1 ) e. { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } ) -> ( I + 1 ) <_ sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < ) )
206 146 147 148 204 205 syl31anc 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( I + 1 ) <_ sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) <_ ( S ` J ) } , RR , < ) )
207 206 11 breqtrrdi 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> ( I + 1 ) <_ I )
208 141 139 207 lensymd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> -. I < ( I + 1 ) )
209 208 adantlr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ ( Q ` ( I + 1 ) ) <_ ( S ` J ) ) -> -. I < ( I + 1 ) )
210 138 209 syldan 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) /\ -. ( S ` J ) < ( Q ` ( I + 1 ) ) ) -> -. I < ( I + 1 ) )
211 134 210 condan 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) e. RR ) -> ( S ` J ) < ( Q ` ( I + 1 ) ) )
212 82 211 mpdan 
 |-  ( ph -> ( S ` J ) < ( Q ` ( I + 1 ) ) )
213 2 128 82 56 212 lelttrd 
 |-  ( ph -> A < ( Q ` ( I + 1 ) ) )
214 213 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> A < ( Q ` ( I + 1 ) ) )
215 153 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( S ` ( J + 1 ) ) e. RR )
216 3 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> B e. RR )
217 simpr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) )
218 165 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( S ` ( J + 1 ) ) <_ B )
219 127 215 216 217 218 ltletrd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) < B )
220 125 126 127 214 219 eliood 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. ( A (,) B ) )
221 124 220 elind 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. ( ran Q i^i ( A (,) B ) ) )
222 elun2 
 |-  ( ( Q ` ( I + 1 ) ) e. ( ran Q i^i ( A (,) B ) ) -> ( Q ` ( I + 1 ) ) e. ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) )
223 221 222 syl 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) )
224 223 9 eleqtrrdi 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( Q ` ( I + 1 ) ) e. T )
225 foelrn 
 |-  ( ( S : ( 0 ... N ) -onto-> T /\ ( Q ` ( I + 1 ) ) e. T ) -> E. j e. ( 0 ... N ) ( Q ` ( I + 1 ) ) = ( S ` j ) )
226 116 224 225 syl2anc 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> E. j e. ( 0 ... N ) ( Q ` ( I + 1 ) ) = ( S ` j ) )
227 212 adantr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` J ) < ( Q ` ( I + 1 ) ) )
228 simpr 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( Q ` ( I + 1 ) ) = ( S ` j ) )
229 227 228 breqtrd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` J ) < ( S ` j ) )
230 229 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` J ) < ( S ` j ) )
231 10 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> S Isom < , < ( ( 0 ... N ) , T ) )
232 51 anim1i 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) )
233 232 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) )
234 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
235 231 233 234 syl2anc 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) )
236 230 235 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> J < j )
237 236 adantllr 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> J < j )
238 eqcom 
 |-  ( ( Q ` ( I + 1 ) ) = ( S ` j ) <-> ( S ` j ) = ( Q ` ( I + 1 ) ) )
239 238 biimpi 
 |-  ( ( Q ` ( I + 1 ) ) = ( S ` j ) -> ( S ` j ) = ( Q ` ( I + 1 ) ) )
240 239 adantl 
 |-  ( ( ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` j ) = ( Q ` ( I + 1 ) ) )
241 simpl 
 |-  ( ( ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) )
242 240 241 eqbrtrd 
 |-  ( ( ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
243 242 adantll 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
244 243 adantlr 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) )
245 10 ad2antrr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> S Isom < , < ( ( 0 ... N ) , T ) )
246 simpr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> j e. ( 0 ... N ) )
247 106 ad2antrr 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> ( J + 1 ) e. ( 0 ... N ) )
248 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( j e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
249 245 246 247 248 syl12anc 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
250 249 adantr 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) )
251 244 250 mpbird 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> j < ( J + 1 ) )
252 237 251 jca 
 |-  ( ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) /\ ( Q ` ( I + 1 ) ) = ( S ` j ) ) -> ( J < j /\ j < ( J + 1 ) ) )
253 252 ex 
 |-  ( ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( Q ` ( I + 1 ) ) = ( S ` j ) -> ( J < j /\ j < ( J + 1 ) ) ) )
254 253 reximdva 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> ( E. j e. ( 0 ... N ) ( Q ` ( I + 1 ) ) = ( S ` j ) -> E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) ) )
255 226 254 mpd 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) )
256 ssrexv 
 |-  ( ( 0 ... N ) C_ ZZ -> ( E. j e. ( 0 ... N ) ( J < j /\ j < ( J + 1 ) ) -> E. j e. ZZ ( J < j /\ j < ( J + 1 ) ) ) )
257 113 255 256 mpsyl 
 |-  ( ( ph /\ ( Q ` ( I + 1 ) ) < ( S ` ( J + 1 ) ) ) -> E. j e. ZZ ( J < j /\ j < ( J + 1 ) ) )
258 112 257 syldan 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> E. j e. ZZ ( J < j /\ j < ( J + 1 ) ) )
259 simplr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> j e. ZZ )
260 8 155 syl 
 |-  ( ph -> J e. ZZ )
261 260 ad2antrr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> J e. ZZ )
262 simprl 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> J < j )
263 simprr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> j < ( J + 1 ) )
264 btwnnz 
 |-  ( ( J e. ZZ /\ J < j /\ j < ( J + 1 ) ) -> -. j e. ZZ )
265 261 262 263 264 syl3anc 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( J < j /\ j < ( J + 1 ) ) ) -> -. j e. ZZ )
266 259 265 pm2.65da 
 |-  ( ( ph /\ j e. ZZ ) -> -. ( J < j /\ j < ( J + 1 ) ) )
267 266 nrexdv 
 |-  ( ph -> -. E. j e. ZZ ( J < j /\ j < ( J + 1 ) ) )
268 267 adantr 
 |-  ( ( ph /\ -. ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) -> -. E. j e. ZZ ( J < j /\ j < ( J + 1 ) ) )
269 258 268 condan 
 |-  ( ph -> ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) )
270 ioossioo 
 |-  ( ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* ) /\ ( ( Q ` I ) <_ ( S ` J ) /\ ( S ` ( J + 1 ) ) <_ ( Q ` ( I + 1 ) ) ) ) -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
271 79 83 100 269 270 syl22anc 
 |-  ( ph -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
272 fveq2 
 |-  ( i = I -> ( Q ` i ) = ( Q ` I ) )
273 oveq1 
 |-  ( i = I -> ( i + 1 ) = ( I + 1 ) )
274 273 fveq2d 
 |-  ( i = I -> ( Q ` ( i + 1 ) ) = ( Q ` ( I + 1 ) ) )
275 272 274 oveq12d 
 |-  ( i = I -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
276 275 sseq2d 
 |-  ( i = I -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
277 276 rspcev 
 |-  ( ( I e. ( 0 ..^ M ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> E. i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
278 76 271 277 syl2anc 
 |-  ( ph -> E. i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )