Metamath Proof Explorer

Theorem fourierdlem50

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem50.xre 
|- ( ph -> X e. RR )
fourierdlem50.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem50.m 
|- ( ph -> M e. NN )
fourierdlem50.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem50.a 
|- ( ph -> A e. RR )
fourierdlem50.b 
|- ( ph -> B e. RR )
fourierdlem50.altb 
|- ( ph -> A < B )
fourierdlem50.ab 
|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
fourierdlem50.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem50.t 
|- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
fourierdlem50.n 
|- N = ( ( # ` T ) - 1 )
fourierdlem50.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem50.j 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem50.u 
|- U = ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
fourierdlem50.ch 
|- ( ch <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
Assertion fourierdlem50 
|- ( ph -> ( U e. ( 0 ..^ M ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem50.xre 
 |-  ( ph -> X e. RR )
2 fourierdlem50.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
3 fourierdlem50.m 
 |-  ( ph -> M e. NN )
4 fourierdlem50.v 
 |-  ( ph -> V e. ( P ` M ) )
5 fourierdlem50.a 
 |-  ( ph -> A e. RR )
6 fourierdlem50.b 
 |-  ( ph -> B e. RR )
7 fourierdlem50.altb 
 |-  ( ph -> A < B )
8 fourierdlem50.ab 
 |-  ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
9 fourierdlem50.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
10 fourierdlem50.t 
 |-  T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
11 fourierdlem50.n 
 |-  N = ( ( # ` T ) - 1 )
12 fourierdlem50.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
13 fourierdlem50.j 
 |-  ( ph -> J e. ( 0 ..^ N ) )
14 fourierdlem50.u 
 |-  U = ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
15 fourierdlem50.ch 
 |-  ( ch <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
16 5 6 7 ltled 
 |-  ( ph -> A <_ B )
17 2 3 4 fourierdlem15 
 |-  ( ph -> V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) )
18 pire 
 |-  _pi e. RR
19 18 renegcli 
 |-  -u _pi e. RR
20 19 a1i 
 |-  ( ph -> -u _pi e. RR )
21 20 1 readdcld 
 |-  ( ph -> ( -u _pi + X ) e. RR )
22 18 a1i 
 |-  ( ph -> _pi e. RR )
23 22 1 readdcld 
 |-  ( ph -> ( _pi + X ) e. RR )
24 21 23 iccssred 
 |-  ( ph -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
25 17 24 fssd 
 |-  ( ph -> V : ( 0 ... M ) --> RR )
26 25 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. RR )
27 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
28 26 27 resubcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. RR )
29 28 9 fmptd 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
30 9 a1i 
 |-  ( ph -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
31 fveq2 
 |-  ( i = 0 -> ( V ` i ) = ( V ` 0 ) )
32 31 oveq1d 
 |-  ( i = 0 -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
33 32 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
34 nnssnn0 
 |-  NN C_ NN0
35 34 a1i 
 |-  ( ph -> NN C_ NN0 )
36 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
37 35 36 sseqtrdi 
 |-  ( ph -> NN C_ ( ZZ>= ` 0 ) )
38 37 3 sseldd 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
39 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
40 38 39 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
41 25 40 ffvelrnd 
 |-  ( ph -> ( V ` 0 ) e. RR )
42 41 1 resubcld 
 |-  ( ph -> ( ( V ` 0 ) - X ) e. RR )
43 30 33 40 42 fvmptd 
 |-  ( ph -> ( Q ` 0 ) = ( ( V ` 0 ) - X ) )
44 2 fourierdlem2 
 |-  ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
45 3 44 syl 
 |-  ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
46 4 45 mpbid 
 |-  ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
47 46 simprd 
 |-  ( ph -> ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) )
48 47 simpld 
 |-  ( ph -> ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) )
49 48 simpld 
 |-  ( ph -> ( V ` 0 ) = ( -u _pi + X ) )
50 49 oveq1d 
 |-  ( ph -> ( ( V ` 0 ) - X ) = ( ( -u _pi + X ) - X ) )
51 20 recnd 
 |-  ( ph -> -u _pi e. CC )
52 1 recnd 
 |-  ( ph -> X e. CC )
53 51 52 pncand 
 |-  ( ph -> ( ( -u _pi + X ) - X ) = -u _pi )
54 43 50 53 3eqtrd 
 |-  ( ph -> ( Q ` 0 ) = -u _pi )
55 20 rexrd 
 |-  ( ph -> -u _pi e. RR* )
56 22 rexrd 
 |-  ( ph -> _pi e. RR* )
57 5 leidd 
 |-  ( ph -> A <_ A )
58 5 6 5 57 16 eliccd 
 |-  ( ph -> A e. ( A [,] B ) )
59 8 58 sseldd 
 |-  ( ph -> A e. ( -u _pi [,] _pi ) )
60 iccgelb 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ A e. ( -u _pi [,] _pi ) ) -> -u _pi <_ A )
61 55 56 59 60 syl3anc 
 |-  ( ph -> -u _pi <_ A )
62 54 61 eqbrtrd 
 |-  ( ph -> ( Q ` 0 ) <_ A )
63 6 leidd 
 |-  ( ph -> B <_ B )
64 5 6 6 16 63 eliccd 
 |-  ( ph -> B e. ( A [,] B ) )
65 8 64 sseldd 
 |-  ( ph -> B e. ( -u _pi [,] _pi ) )
66 iccleub 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ B e. ( -u _pi [,] _pi ) ) -> B <_ _pi )
67 55 56 65 66 syl3anc 
 |-  ( ph -> B <_ _pi )
68 fveq2 
 |-  ( i = M -> ( V ` i ) = ( V ` M ) )
69 68 oveq1d 
 |-  ( i = M -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
70 69 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( V ` i ) - X ) = ( ( V ` M ) - X ) )
71 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
72 38 71 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
73 25 72 ffvelrnd 
 |-  ( ph -> ( V ` M ) e. RR )
74 73 1 resubcld 
 |-  ( ph -> ( ( V ` M ) - X ) e. RR )
75 30 70 72 74 fvmptd 
 |-  ( ph -> ( Q ` M ) = ( ( V ` M ) - X ) )
76 48 simprd 
 |-  ( ph -> ( V ` M ) = ( _pi + X ) )
77 76 oveq1d 
 |-  ( ph -> ( ( V ` M ) - X ) = ( ( _pi + X ) - X ) )
78 22 recnd 
 |-  ( ph -> _pi e. CC )
79 78 52 pncand 
 |-  ( ph -> ( ( _pi + X ) - X ) = _pi )
80 75 77 79 3eqtrrd 
 |-  ( ph -> _pi = ( Q ` M ) )
81 67 80 breqtrd 
 |-  ( ph -> B <_ ( Q ` M ) )
82 prfi 
 |-  { A , B } e. Fin
83 82 a1i 
 |-  ( ph -> { A , B } e. Fin )
84 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
85 9 rnmptfi 
 |-  ( ( 0 ... M ) e. Fin -> ran Q e. Fin )
86 84 85 syl 
 |-  ( ph -> ran Q e. Fin )
87 infi 
 |-  ( ran Q e. Fin -> ( ran Q i^i ( A (,) B ) ) e. Fin )
88 86 87 syl 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) e. Fin )
89 unfi 
 |-  ( ( { A , B } e. Fin /\ ( ran Q i^i ( A (,) B ) ) e. Fin ) -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
90 83 88 89 syl2anc 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
91 10 90 eqeltrid 
 |-  ( ph -> T e. Fin )
92 5 6 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
93 prssg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
94 5 6 93 syl2anc 
 |-  ( ph -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
95 92 94 mpbid 
 |-  ( ph -> { A , B } C_ RR )
96 inss2 
 |-  ( ran Q i^i ( A (,) B ) ) C_ ( A (,) B )
97 ioossre 
 |-  ( A (,) B ) C_ RR
98 96 97 sstri 
 |-  ( ran Q i^i ( A (,) B ) ) C_ RR
99 98 a1i 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) C_ RR )
100 95 99 unssd 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ RR )
101 10 100 eqsstrid 
 |-  ( ph -> T C_ RR )
102 91 101 12 11 fourierdlem36 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
103 eqid 
 |-  sup ( { x e. ( 0 ..^ M ) | ( Q ` x ) <_ ( S ` J ) } , RR , < ) = sup ( { x e. ( 0 ..^ M ) | ( Q ` x ) <_ ( S ` J ) } , RR , < )
104 3 5 6 16 29 62 81 13 10 102 103 fourierdlem20 
 |-  ( ph -> E. i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
105 15 biimpi 
 |-  ( ch -> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
106 simp-4l 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> ph )
107 105 106 syl 
 |-  ( ch -> ph )
108 simplr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> k e. ( 0 ..^ M ) )
109 105 108 syl 
 |-  ( ch -> k e. ( 0 ..^ M ) )
110 107 109 jca 
 |-  ( ch -> ( ph /\ k e. ( 0 ..^ M ) ) )
111 simp-4r 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
112 105 111 syl 
 |-  ( ch -> i e. ( 0 ..^ M ) )
113 elfzofz 
 |-  ( k e. ( 0 ..^ M ) -> k e. ( 0 ... M ) )
114 113 ad2antlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> k e. ( 0 ... M ) )
115 105 114 syl 
 |-  ( ch -> k e. ( 0 ... M ) )
116 107 25 syl 
 |-  ( ch -> V : ( 0 ... M ) --> RR )
117 116 115 ffvelrnd 
 |-  ( ch -> ( V ` k ) e. RR )
118 107 1 syl 
 |-  ( ch -> X e. RR )
119 117 118 resubcld 
 |-  ( ch -> ( ( V ` k ) - X ) e. RR )
120 fveq2 
 |-  ( i = k -> ( V ` i ) = ( V ` k ) )
121 120 oveq1d 
 |-  ( i = k -> ( ( V ` i ) - X ) = ( ( V ` k ) - X ) )
122 121 9 fvmptg 
 |-  ( ( k e. ( 0 ... M ) /\ ( ( V ` k ) - X ) e. RR ) -> ( Q ` k ) = ( ( V ` k ) - X ) )
123 115 119 122 syl2anc 
 |-  ( ch -> ( Q ` k ) = ( ( V ` k ) - X ) )
124 123 119 eqeltrd 
 |-  ( ch -> ( Q ` k ) e. RR )
125 29 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
126 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
127 126 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
128 125 127 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
129 107 112 128 syl2anc 
 |-  ( ch -> ( Q ` ( i + 1 ) ) e. RR )
130 isof1o 
 |-  ( S Isom < , < ( ( 0 ... N ) , T ) -> S : ( 0 ... N ) -1-1-onto-> T )
131 102 130 syl 
 |-  ( ph -> S : ( 0 ... N ) -1-1-onto-> T )
132 f1of 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) --> T )
133 131 132 syl 
 |-  ( ph -> S : ( 0 ... N ) --> T )
134 fzofzp1 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
135 13 134 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... N ) )
136 133 135 ffvelrnd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. T )
137 101 136 sseldd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR )
138 107 137 syl 
 |-  ( ch -> ( S ` ( J + 1 ) ) e. RR )
139 elfzofz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) )
140 13 139 syl 
 |-  ( ph -> J e. ( 0 ... N ) )
141 133 140 ffvelrnd 
 |-  ( ph -> ( S ` J ) e. T )
142 101 141 sseldd 
 |-  ( ph -> ( S ` J ) e. RR )
143 107 142 syl 
 |-  ( ch -> ( S ` J ) e. RR )
144 105 simprd 
 |-  ( ch -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
145 124 rexrd 
 |-  ( ch -> ( Q ` k ) e. RR* )
146 29 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
147 fzofzp1 
 |-  ( k e. ( 0 ..^ M ) -> ( k + 1 ) e. ( 0 ... M ) )
148 147 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( k + 1 ) e. ( 0 ... M ) )
149 146 148 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` ( k + 1 ) ) e. RR )
150 149 rexrd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` ( k + 1 ) ) e. RR* )
151 110 150 syl 
 |-  ( ch -> ( Q ` ( k + 1 ) ) e. RR* )
152 143 rexrd 
 |-  ( ch -> ( S ` J ) e. RR* )
153 138 rexrd 
 |-  ( ch -> ( S ` ( J + 1 ) ) e. RR* )
154 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
155 154 zred 
 |-  ( J e. ( 0 ..^ N ) -> J e. RR )
156 155 ltp1d 
 |-  ( J e. ( 0 ..^ N ) -> J < ( J + 1 ) )
157 13 156 syl 
 |-  ( ph -> J < ( J + 1 ) )
158 isoeq5 
 |-  ( T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) -> ( S Isom < , < ( ( 0 ... N ) , T ) <-> S Isom < , < ( ( 0 ... N ) , ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) ) ) )
159 10 158 ax-mp 
 |-  ( S Isom < , < ( ( 0 ... N ) , T ) <-> S Isom < , < ( ( 0 ... N ) , ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) ) )
160 102 159 sylib 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) ) )
161 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) ) /\ ( J e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( J < ( J + 1 ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
162 160 140 135 161 syl12anc 
 |-  ( ph -> ( J < ( J + 1 ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
163 157 162 mpbid 
 |-  ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
164 107 163 syl 
 |-  ( ch -> ( S ` J ) < ( S ` ( J + 1 ) ) )
165 145 151 152 153 164 ioossioobi 
 |-  ( ch -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> ( ( Q ` k ) <_ ( S ` J ) /\ ( S ` ( J + 1 ) ) <_ ( Q ` ( k + 1 ) ) ) ) )
166 144 165 mpbid 
 |-  ( ch -> ( ( Q ` k ) <_ ( S ` J ) /\ ( S ` ( J + 1 ) ) <_ ( Q ` ( k + 1 ) ) ) )
167 166 simpld 
 |-  ( ch -> ( Q ` k ) <_ ( S ` J ) )
168 124 143 138 167 164 lelttrd 
 |-  ( ch -> ( Q ` k ) < ( S ` ( J + 1 ) ) )
169 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
170 169 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ... M ) )
171 170 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> i e. ( 0 ... M ) )
172 105 171 syl 
 |-  ( ch -> i e. ( 0 ... M ) )
173 107 172 28 syl2anc 
 |-  ( ch -> ( ( V ` i ) - X ) e. RR )
174 9 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
175 172 173 174 syl2anc 
 |-  ( ch -> ( Q ` i ) = ( ( V ` i ) - X ) )
176 175 173 eqeltrd 
 |-  ( ch -> ( Q ` i ) e. RR )
177 simpllr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
178 105 177 syl 
 |-  ( ch -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
179 176 129 143 138 164 178 fourierdlem10 
 |-  ( ch -> ( ( Q ` i ) <_ ( S ` J ) /\ ( S ` ( J + 1 ) ) <_ ( Q ` ( i + 1 ) ) ) )
180 179 simprd 
 |-  ( ch -> ( S ` ( J + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
181 124 138 129 168 180 ltletrd 
 |-  ( ch -> ( Q ` k ) < ( Q ` ( i + 1 ) ) )
182 124 129 118 181 ltadd2dd 
 |-  ( ch -> ( X + ( Q ` k ) ) < ( X + ( Q ` ( i + 1 ) ) ) )
183 123 oveq2d 
 |-  ( ch -> ( X + ( Q ` k ) ) = ( X + ( ( V ` k ) - X ) ) )
184 107 52 syl 
 |-  ( ch -> X e. CC )
185 117 recnd 
 |-  ( ch -> ( V ` k ) e. CC )
186 184 185 pncan3d 
 |-  ( ch -> ( X + ( ( V ` k ) - X ) ) = ( V ` k ) )
187 183 186 eqtr2d 
 |-  ( ch -> ( V ` k ) = ( X + ( Q ` k ) ) )
188 112 126 syl 
 |-  ( ch -> ( i + 1 ) e. ( 0 ... M ) )
189 25 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
190 189 127 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
191 107 112 190 syl2anc 
 |-  ( ch -> ( V ` ( i + 1 ) ) e. RR )
192 191 118 resubcld 
 |-  ( ch -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
193 188 192 jca 
 |-  ( ch -> ( ( i + 1 ) e. ( 0 ... M ) /\ ( ( V ` ( i + 1 ) ) - X ) e. RR ) )
194 eleq1 
 |-  ( k = ( i + 1 ) -> ( k e. ( 0 ... M ) <-> ( i + 1 ) e. ( 0 ... M ) ) )
195 fveq2 
 |-  ( k = ( i + 1 ) -> ( V ` k ) = ( V ` ( i + 1 ) ) )
196 195 oveq1d 
 |-  ( k = ( i + 1 ) -> ( ( V ` k ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
197 196 eleq1d 
 |-  ( k = ( i + 1 ) -> ( ( ( V ` k ) - X ) e. RR <-> ( ( V ` ( i + 1 ) ) - X ) e. RR ) )
198 194 197 anbi12d 
 |-  ( k = ( i + 1 ) -> ( ( k e. ( 0 ... M ) /\ ( ( V ` k ) - X ) e. RR ) <-> ( ( i + 1 ) e. ( 0 ... M ) /\ ( ( V ` ( i + 1 ) ) - X ) e. RR ) ) )
199 fveq2 
 |-  ( k = ( i + 1 ) -> ( Q ` k ) = ( Q ` ( i + 1 ) ) )
200 199 196 eqeq12d 
 |-  ( k = ( i + 1 ) -> ( ( Q ` k ) = ( ( V ` k ) - X ) <-> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) ) )
201 198 200 imbi12d 
 |-  ( k = ( i + 1 ) -> ( ( ( k e. ( 0 ... M ) /\ ( ( V ` k ) - X ) e. RR ) -> ( Q ` k ) = ( ( V ` k ) - X ) ) <-> ( ( ( i + 1 ) e. ( 0 ... M ) /\ ( ( V ` ( i + 1 ) ) - X ) e. RR ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) ) ) )
202 201 122 vtoclg 
 |-  ( ( i + 1 ) e. ( 0 ... M ) -> ( ( ( i + 1 ) e. ( 0 ... M ) /\ ( ( V ` ( i + 1 ) ) - X ) e. RR ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) ) )
203 188 193 202 sylc 
 |-  ( ch -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
204 203 oveq2d 
 |-  ( ch -> ( X + ( Q ` ( i + 1 ) ) ) = ( X + ( ( V ` ( i + 1 ) ) - X ) ) )
205 191 recnd 
 |-  ( ch -> ( V ` ( i + 1 ) ) e. CC )
206 184 205 pncan3d 
 |-  ( ch -> ( X + ( ( V ` ( i + 1 ) ) - X ) ) = ( V ` ( i + 1 ) ) )
207 204 206 eqtr2d 
 |-  ( ch -> ( V ` ( i + 1 ) ) = ( X + ( Q ` ( i + 1 ) ) ) )
208 182 187 207 3brtr4d 
 |-  ( ch -> ( V ` k ) < ( V ` ( i + 1 ) ) )
209 eleq1w 
 |-  ( l = i -> ( l e. ( 0 ..^ M ) <-> i e. ( 0 ..^ M ) ) )
210 209 anbi2d 
 |-  ( l = i -> ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i e. ( 0 ..^ M ) ) ) )
211 oveq1 
 |-  ( l = i -> ( l + 1 ) = ( i + 1 ) )
212 211 fveq2d 
 |-  ( l = i -> ( V ` ( l + 1 ) ) = ( V ` ( i + 1 ) ) )
213 212 breq2d 
 |-  ( l = i -> ( ( V ` k ) < ( V ` ( l + 1 ) ) <-> ( V ` k ) < ( V ` ( i + 1 ) ) ) )
214 210 213 anbi12d 
 |-  ( l = i -> ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) <-> ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( i + 1 ) ) ) ) )
215 fveq2 
 |-  ( l = i -> ( V ` l ) = ( V ` i ) )
216 215 breq2d 
 |-  ( l = i -> ( ( V ` k ) <_ ( V ` l ) <-> ( V ` k ) <_ ( V ` i ) ) )
217 214 216 imbi12d 
 |-  ( l = i -> ( ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) -> ( V ` k ) <_ ( V ` l ) ) <-> ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( i + 1 ) ) ) -> ( V ` k ) <_ ( V ` i ) ) ) )
218 eleq1w 
 |-  ( h = k -> ( h e. ( 0 ..^ M ) <-> k e. ( 0 ..^ M ) ) )
219 218 anbi2d 
 |-  ( h = k -> ( ( ph /\ h e. ( 0 ..^ M ) ) <-> ( ph /\ k e. ( 0 ..^ M ) ) ) )
220 219 anbi1d 
 |-  ( h = k -> ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) ) )
221 fveq2 
 |-  ( h = k -> ( V ` h ) = ( V ` k ) )
222 221 breq1d 
 |-  ( h = k -> ( ( V ` h ) < ( V ` ( l + 1 ) ) <-> ( V ` k ) < ( V ` ( l + 1 ) ) ) )
223 220 222 anbi12d 
 |-  ( h = k -> ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) <-> ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) ) )
224 221 breq1d 
 |-  ( h = k -> ( ( V ` h ) <_ ( V ` l ) <-> ( V ` k ) <_ ( V ` l ) ) )
225 223 224 imbi12d 
 |-  ( h = k -> ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( V ` h ) <_ ( V ` l ) ) <-> ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) -> ( V ` k ) <_ ( V ` l ) ) ) )
226 elfzoelz 
 |-  ( h e. ( 0 ..^ M ) -> h e. ZZ )
227 226 ad3antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> h e. ZZ )
228 elfzoelz 
 |-  ( l e. ( 0 ..^ M ) -> l e. ZZ )
229 228 ad2antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> l e. ZZ )
230 simplr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ -. h < ( l + 1 ) ) -> ( V ` h ) < ( V ` ( l + 1 ) ) )
231 25 adantr 
 |-  ( ( ph /\ l e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
232 fzofzp1 
 |-  ( l e. ( 0 ..^ M ) -> ( l + 1 ) e. ( 0 ... M ) )
233 232 adantl 
 |-  ( ( ph /\ l e. ( 0 ..^ M ) ) -> ( l + 1 ) e. ( 0 ... M ) )
234 231 233 ffvelrnd 
 |-  ( ( ph /\ l e. ( 0 ..^ M ) ) -> ( V ` ( l + 1 ) ) e. RR )
235 234 adantlr 
 |-  ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) -> ( V ` ( l + 1 ) ) e. RR )
236 235 adantr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( V ` ( l + 1 ) ) e. RR )
237 25 adantr 
 |-  ( ( ph /\ h e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
238 elfzofz 
 |-  ( h e. ( 0 ..^ M ) -> h e. ( 0 ... M ) )
239 238 adantl 
 |-  ( ( ph /\ h e. ( 0 ..^ M ) ) -> h e. ( 0 ... M ) )
240 237 239 ffvelrnd 
 |-  ( ( ph /\ h e. ( 0 ..^ M ) ) -> ( V ` h ) e. RR )
241 240 ad2antrr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( V ` h ) e. RR )
242 228 zred 
 |-  ( l e. ( 0 ..^ M ) -> l e. RR )
243 peano2re 
 |-  ( l e. RR -> ( l + 1 ) e. RR )
244 242 243 syl 
 |-  ( l e. ( 0 ..^ M ) -> ( l + 1 ) e. RR )
245 244 ad2antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( l + 1 ) e. RR )
246 226 zred 
 |-  ( h e. ( 0 ..^ M ) -> h e. RR )
247 246 ad3antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> h e. RR )
248 simpr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> -. h < ( l + 1 ) )
249 245 247 248 nltled 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( l + 1 ) <_ h )
250 228 peano2zd 
 |-  ( l e. ( 0 ..^ M ) -> ( l + 1 ) e. ZZ )
251 250 ad2antlr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> ( l + 1 ) e. ZZ )
252 226 ad2antrr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> h e. ZZ )
253 simpr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> ( l + 1 ) <_ h )
254 eluz2 
 |-  ( h e. ( ZZ>= ` ( l + 1 ) ) <-> ( ( l + 1 ) e. ZZ /\ h e. ZZ /\ ( l + 1 ) <_ h ) )
255 251 252 253 254 syl3anbrc 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> h e. ( ZZ>= ` ( l + 1 ) ) )
256 255 adantlll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> h e. ( ZZ>= ` ( l + 1 ) ) )
257 simplll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> ph )
258 0zd 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 e. ZZ )
259 elfzoel2 
 |-  ( h e. ( 0 ..^ M ) -> M e. ZZ )
260 259 ad2antrr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> M e. ZZ )
261 elfzelz 
 |-  ( i e. ( ( l + 1 ) ... h ) -> i e. ZZ )
262 261 adantl 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. ZZ )
263 258 260 262 3jca 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ i e. ZZ ) )
264 0red 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 e. RR )
265 261 zred 
 |-  ( i e. ( ( l + 1 ) ... h ) -> i e. RR )
266 265 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. RR )
267 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l e. RR )
268 elfzole1 
 |-  ( l e. ( 0 ..^ M ) -> 0 <_ l )
269 268 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ l )
270 267 243 syl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( l + 1 ) e. RR )
271 267 ltp1d 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l < ( l + 1 ) )
272 elfzle1 
 |-  ( i e. ( ( l + 1 ) ... h ) -> ( l + 1 ) <_ i )
273 272 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( l + 1 ) <_ i )
274 267 270 266 271 273 ltletrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l < i )
275 264 267 266 269 274 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 < i )
276 264 266 275 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ i )
277 276 adantll 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ i )
278 265 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. RR )
279 259 zred 
 |-  ( h e. ( 0 ..^ M ) -> M e. RR )
280 279 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> M e. RR )
281 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> h e. RR )
282 elfzle2 
 |-  ( i e. ( ( l + 1 ) ... h ) -> i <_ h )
283 282 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ h )
284 elfzolt2 
 |-  ( h e. ( 0 ..^ M ) -> h < M )
285 284 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> h < M )
286 278 281 280 283 285 lelttrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i < M )
287 278 280 286 ltled 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ M )
288 287 adantlr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ M )
289 263 277 288 jca32 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ M ) ) )
290 elfz2 
 |-  ( i e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ M ) ) )
291 289 290 sylibr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. ( 0 ... M ) )
292 291 adantlll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. ( 0 ... M ) )
293 257 292 26 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( V ` i ) e. RR )
294 293 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( V ` i ) e. RR )
295 simplll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ph )
296 0zd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 e. ZZ )
297 elfzelz 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i e. ZZ )
298 297 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ZZ )
299 0red 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 e. RR )
300 298 zred 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. RR )
301 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l e. RR )
302 268 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 <_ l )
303 301 243 syl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( l + 1 ) e. RR )
304 301 ltp1d 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l < ( l + 1 ) )
305 elfzle1 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> ( l + 1 ) <_ i )
306 305 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( l + 1 ) <_ i )
307 301 303 300 304 306 ltletrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l < i )
308 299 301 300 302 307 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 < i )
309 299 300 308 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 <_ i )
310 eluz2 
 |-  ( i e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ i e. ZZ /\ 0 <_ i ) )
311 296 298 309 310 syl3anbrc 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
312 311 adantll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
313 elfzoel2 
 |-  ( l e. ( 0 ..^ M ) -> M e. ZZ )
314 313 ad2antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> M e. ZZ )
315 297 zred 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i e. RR )
316 315 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. RR )
317 peano2rem 
 |-  ( h e. RR -> ( h - 1 ) e. RR )
318 246 317 syl 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) e. RR )
319 318 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( h - 1 ) e. RR )
320 279 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> M e. RR )
321 elfzle2 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i <_ ( h - 1 ) )
322 321 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i <_ ( h - 1 ) )
323 246 ltm1d 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) < h )
324 318 246 279 323 284 lttrd 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) < M )
325 324 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( h - 1 ) < M )
326 316 319 320 322 325 lelttrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
327 326 adantll 
 |-  ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
328 327 adantlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
329 elfzo2 
 |-  ( i e. ( 0 ..^ M ) <-> ( i e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ i < M ) )
330 312 314 328 329 syl3anbrc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( 0 ..^ M ) )
331 169 26 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
332 47 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
333 332 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
334 331 190 333 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
335 295 330 334 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
336 335 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
337 256 294 336 monoord 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> ( V ` ( l + 1 ) ) <_ ( V ` h ) )
338 249 337 syldan 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( V ` ( l + 1 ) ) <_ ( V ` h ) )
339 236 241 338 lensymd 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> -. ( V ` h ) < ( V ` ( l + 1 ) ) )
340 339 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ -. h < ( l + 1 ) ) -> -. ( V ` h ) < ( V ` ( l + 1 ) ) )
341 230 340 condan 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> h < ( l + 1 ) )
342 zleltp1 
 |-  ( ( h e. ZZ /\ l e. ZZ ) -> ( h <_ l <-> h < ( l + 1 ) ) )
343 227 229 342 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( h <_ l <-> h < ( l + 1 ) ) )
344 341 343 mpbird 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> h <_ l )
345 eluz2 
 |-  ( l e. ( ZZ>= ` h ) <-> ( h e. ZZ /\ l e. ZZ /\ h <_ l ) )
346 227 229 344 345 syl3anbrc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> l e. ( ZZ>= ` h ) )
347 25 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> V : ( 0 ... M ) --> RR )
348 0zd 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> 0 e. ZZ )
349 259 ad2antrr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> M e. ZZ )
350 elfzelz 
 |-  ( i e. ( h ... l ) -> i e. ZZ )
351 350 adantl 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ZZ )
352 348 349 351 3jca 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ i e. ZZ ) )
353 0red 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 e. RR )
354 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> h e. RR )
355 350 zred 
 |-  ( i e. ( h ... l ) -> i e. RR )
356 355 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i e. RR )
357 elfzole1 
 |-  ( h e. ( 0 ..^ M ) -> 0 <_ h )
358 357 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 <_ h )
359 elfzle1 
 |-  ( i e. ( h ... l ) -> h <_ i )
360 359 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> h <_ i )
361 353 354 356 358 360 letrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 <_ i )
362 361 adantlr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> 0 <_ i )
363 355 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i e. RR )
364 313 zred 
 |-  ( l e. ( 0 ..^ M ) -> M e. RR )
365 364 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> M e. RR )
366 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> l e. RR )
367 elfzle2 
 |-  ( i e. ( h ... l ) -> i <_ l )
368 367 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i <_ l )
369 elfzolt2 
 |-  ( l e. ( 0 ..^ M ) -> l < M )
370 369 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> l < M )
371 363 366 365 368 370 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i < M )
372 363 365 371 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i <_ M )
373 372 adantll 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i <_ M )
374 352 362 373 jca32 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ M ) ) )
375 374 290 sylibr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ( 0 ... M ) )
376 375 adantlll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ( 0 ... M ) )
377 347 376 ffvelrnd 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> ( V ` i ) e. RR )
378 377 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... l ) ) -> ( V ` i ) e. RR )
379 simp-4l 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> ph )
380 0zd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 e. ZZ )
381 elfzelz 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i e. ZZ )
382 381 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ZZ )
383 0red 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 e. RR )
384 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> h e. RR )
385 382 zred 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. RR )
386 357 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 <_ h )
387 elfzle1 
 |-  ( i e. ( h ... ( l - 1 ) ) -> h <_ i )
388 387 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> h <_ i )
389 383 384 385 386 388 letrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 <_ i )
390 380 382 389 310 syl3anbrc 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
391 390 adantll 
 |-  ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
392 391 ad4ant14 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
393 313 ad3antlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> M e. ZZ )
394 381 zred 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i e. RR )
395 394 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. RR )
396 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> l e. RR )
397 364 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> M e. RR )
398 elfzle2 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i <_ ( l - 1 ) )
399 398 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i <_ ( l - 1 ) )
400 zltlem1 
 |-  ( ( i e. ZZ /\ l e. ZZ ) -> ( i < l <-> i <_ ( l - 1 ) ) )
401 381 228 400 syl2anr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> ( i < l <-> i <_ ( l - 1 ) ) )
402 399 401 mpbird 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < l )
403 369 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> l < M )
404 395 396 397 402 403 lttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
405 404 adantll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
406 405 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
407 392 393 406 329 syl3anbrc 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( 0 ..^ M ) )
408 379 407 334 syl2anc 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
409 346 378 408 monoord 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( V ` h ) <_ ( V ` l ) )
410 225 409 chvarvv 
 |-  ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) -> ( V ` k ) <_ ( V ` l ) )
411 217 410 chvarvv 
 |-  ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( i + 1 ) ) ) -> ( V ` k ) <_ ( V ` i ) )
412 110 112 208 411 syl21anc 
 |-  ( ch -> ( V ` k ) <_ ( V ` i ) )
413 107 112 jca 
 |-  ( ch -> ( ph /\ i e. ( 0 ..^ M ) ) )
414 110 149 syl 
 |-  ( ch -> ( Q ` ( k + 1 ) ) e. RR )
415 179 simpld 
 |-  ( ch -> ( Q ` i ) <_ ( S ` J ) )
416 176 143 138 415 164 lelttrd 
 |-  ( ch -> ( Q ` i ) < ( S ` ( J + 1 ) ) )
417 166 simprd 
 |-  ( ch -> ( S ` ( J + 1 ) ) <_ ( Q ` ( k + 1 ) ) )
418 176 138 414 416 417 ltletrd 
 |-  ( ch -> ( Q ` i ) < ( Q ` ( k + 1 ) ) )
419 176 414 118 418 ltadd2dd 
 |-  ( ch -> ( X + ( Q ` i ) ) < ( X + ( Q ` ( k + 1 ) ) ) )
420 175 oveq2d 
 |-  ( ch -> ( X + ( Q ` i ) ) = ( X + ( ( V ` i ) - X ) ) )
421 107 172 26 syl2anc 
 |-  ( ch -> ( V ` i ) e. RR )
422 421 recnd 
 |-  ( ch -> ( V ` i ) e. CC )
423 184 422 pncan3d 
 |-  ( ch -> ( X + ( ( V ` i ) - X ) ) = ( V ` i ) )
424 420 423 eqtr2d 
 |-  ( ch -> ( V ` i ) = ( X + ( Q ` i ) ) )
425 9 a1i 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
426 fveq2 
 |-  ( i = ( k + 1 ) -> ( V ` i ) = ( V ` ( k + 1 ) ) )
427 426 oveq1d 
 |-  ( i = ( k + 1 ) -> ( ( V ` i ) - X ) = ( ( V ` ( k + 1 ) ) - X ) )
428 427 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i = ( k + 1 ) ) -> ( ( V ` i ) - X ) = ( ( V ` ( k + 1 ) ) - X ) )
429 25 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
430 429 148 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( V ` ( k + 1 ) ) e. RR )
431 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> X e. RR )
432 430 431 resubcld 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( ( V ` ( k + 1 ) ) - X ) e. RR )
433 425 428 148 432 fvmptd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` ( k + 1 ) ) = ( ( V ` ( k + 1 ) ) - X ) )
434 107 109 433 syl2anc 
 |-  ( ch -> ( Q ` ( k + 1 ) ) = ( ( V ` ( k + 1 ) ) - X ) )
435 434 oveq2d 
 |-  ( ch -> ( X + ( Q ` ( k + 1 ) ) ) = ( X + ( ( V ` ( k + 1 ) ) - X ) ) )
436 110 430 syl 
 |-  ( ch -> ( V ` ( k + 1 ) ) e. RR )
437 436 recnd 
 |-  ( ch -> ( V ` ( k + 1 ) ) e. CC )
438 184 437 pncan3d 
 |-  ( ch -> ( X + ( ( V ` ( k + 1 ) ) - X ) ) = ( V ` ( k + 1 ) ) )
439 435 438 eqtr2d 
 |-  ( ch -> ( V ` ( k + 1 ) ) = ( X + ( Q ` ( k + 1 ) ) ) )
440 419 424 439 3brtr4d 
 |-  ( ch -> ( V ` i ) < ( V ` ( k + 1 ) ) )
441 eleq1w 
 |-  ( l = k -> ( l e. ( 0 ..^ M ) <-> k e. ( 0 ..^ M ) ) )
442 441 anbi2d 
 |-  ( l = k -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) ) )
443 oveq1 
 |-  ( l = k -> ( l + 1 ) = ( k + 1 ) )
444 443 fveq2d 
 |-  ( l = k -> ( V ` ( l + 1 ) ) = ( V ` ( k + 1 ) ) )
445 444 breq2d 
 |-  ( l = k -> ( ( V ` i ) < ( V ` ( l + 1 ) ) <-> ( V ` i ) < ( V ` ( k + 1 ) ) ) )
446 442 445 anbi12d 
 |-  ( l = k -> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( k + 1 ) ) ) ) )
447 fveq2 
 |-  ( l = k -> ( V ` l ) = ( V ` k ) )
448 447 breq2d 
 |-  ( l = k -> ( ( V ` i ) <_ ( V ` l ) <-> ( V ` i ) <_ ( V ` k ) ) )
449 446 448 imbi12d 
 |-  ( l = k -> ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) -> ( V ` i ) <_ ( V ` l ) ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( k + 1 ) ) ) -> ( V ` i ) <_ ( V ` k ) ) ) )
450 eleq1w 
 |-  ( h = i -> ( h e. ( 0 ..^ M ) <-> i e. ( 0 ..^ M ) ) )
451 450 anbi2d 
 |-  ( h = i -> ( ( ph /\ h e. ( 0 ..^ M ) ) <-> ( ph /\ i e. ( 0 ..^ M ) ) ) )
452 451 anbi1d 
 |-  ( h = i -> ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) ) )
453 fveq2 
 |-  ( h = i -> ( V ` h ) = ( V ` i ) )
454 453 breq1d 
 |-  ( h = i -> ( ( V ` h ) < ( V ` ( l + 1 ) ) <-> ( V ` i ) < ( V ` ( l + 1 ) ) ) )
455 452 454 anbi12d 
 |-  ( h = i -> ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) ) )
456 453 breq1d 
 |-  ( h = i -> ( ( V ` h ) <_ ( V ` l ) <-> ( V ` i ) <_ ( V ` l ) ) )
457 455 456 imbi12d 
 |-  ( h = i -> ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( V ` h ) <_ ( V ` l ) ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) -> ( V ` i ) <_ ( V ` l ) ) ) )
458 457 409 chvarvv 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) -> ( V ` i ) <_ ( V ` l ) )
459 449 458 chvarvv 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( k + 1 ) ) ) -> ( V ` i ) <_ ( V ` k ) )
460 413 109 440 459 syl21anc 
 |-  ( ch -> ( V ` i ) <_ ( V ` k ) )
461 117 421 letri3d 
 |-  ( ch -> ( ( V ` k ) = ( V ` i ) <-> ( ( V ` k ) <_ ( V ` i ) /\ ( V ` i ) <_ ( V ` k ) ) ) )
462 412 460 461 mpbir2and 
 |-  ( ch -> ( V ` k ) = ( V ` i ) )
463 2 3 4 fourierdlem34 
 |-  ( ph -> V : ( 0 ... M ) -1-1-> RR )
464 107 463 syl 
 |-  ( ch -> V : ( 0 ... M ) -1-1-> RR )
465 f1fveq 
 |-  ( ( V : ( 0 ... M ) -1-1-> RR /\ ( k e. ( 0 ... M ) /\ i e. ( 0 ... M ) ) ) -> ( ( V ` k ) = ( V ` i ) <-> k = i ) )
466 464 115 172 465 syl12anc 
 |-  ( ch -> ( ( V ` k ) = ( V ` i ) <-> k = i ) )
467 462 466 mpbid 
 |-  ( ch -> k = i )
468 15 467 sylbir 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) -> k = i )
469 468 ex 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) -> k = i ) )
470 simpl 
 |-  ( ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ k = i ) -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
471 fveq2 
 |-  ( k = i -> ( Q ` k ) = ( Q ` i ) )
472 oveq1 
 |-  ( k = i -> ( k + 1 ) = ( i + 1 ) )
473 472 fveq2d 
 |-  ( k = i -> ( Q ` ( k + 1 ) ) = ( Q ` ( i + 1 ) ) )
474 471 473 oveq12d 
 |-  ( k = i -> ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
475 474 eqcomd 
 |-  ( k = i -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
476 475 adantl 
 |-  ( ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ k = i ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
477 470 476 sseqtrd 
 |-  ( ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ k = i ) -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
478 477 ex 
 |-  ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( k = i -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
479 478 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) -> ( k = i -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
480 469 479 impbid 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ( 0 ..^ M ) ) -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) )
481 480 ralrimiva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A. k e. ( 0 ..^ M ) ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) )
482 481 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> A. k e. ( 0 ..^ M ) ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) ) )
483 482 reximdva 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ M ) A. k e. ( 0 ..^ M ) ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) ) )
484 104 483 mpd 
 |-  ( ph -> E. i e. ( 0 ..^ M ) A. k e. ( 0 ..^ M ) ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) )
485 reu6 
 |-  ( E! k e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> E. i e. ( 0 ..^ M ) A. k e. ( 0 ..^ M ) ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) <-> k = i ) )
486 484 485 sylibr 
 |-  ( ph -> E! k e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
487 fveq2 
 |-  ( i = k -> ( Q ` i ) = ( Q ` k ) )
488 oveq1 
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
489 488 fveq2d 
 |-  ( i = k -> ( Q ` ( i + 1 ) ) = ( Q ` ( k + 1 ) ) )
490 487 489 oveq12d 
 |-  ( i = k -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
491 490 sseq2d 
 |-  ( i = k -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) ) )
492 491 cbvreuvw 
 |-  ( E! i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> E! k e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
493 486 492 sylibr 
 |-  ( ph -> E! i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
494 riotacl 
 |-  ( E! i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( 0 ..^ M ) )
495 493 494 syl 
 |-  ( ph -> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( 0 ..^ M ) )
496 14 495 eqeltrid 
 |-  ( ph -> U e. ( 0 ..^ M ) )
497 14 eqcomi 
 |-  ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U
498 497 a1i 
 |-  ( ph -> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U )
499 fveq2 
 |-  ( i = U -> ( Q ` i ) = ( Q ` U ) )
500 oveq1 
 |-  ( i = U -> ( i + 1 ) = ( U + 1 ) )
501 500 fveq2d 
 |-  ( i = U -> ( Q ` ( i + 1 ) ) = ( Q ` ( U + 1 ) ) )
502 499 501 oveq12d 
 |-  ( i = U -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
503 502 sseq2d 
 |-  ( i = U -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )
504 503 riota2 
 |-  ( ( U e. ( 0 ..^ M ) /\ E! i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) <-> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U ) )
505 496 493 504 syl2anc 
 |-  ( ph -> ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) <-> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U ) )
506 498 505 mpbird 
 |-  ( ph -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
507 496 506 jca 
 |-  ( ph -> ( U e. ( 0 ..^ M ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )