This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 0red 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 e. RR )
264 261 zred 
 |-  ( i e. ( ( l + 1 ) ... h ) -> i e. RR )
265 264 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. RR )
266 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l e. RR )
267 elfzole1 
 |-  ( l e. ( 0 ..^ M ) -> 0 <_ l )
268 267 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ l )
269 266 243 syl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( l + 1 ) e. RR )
270 266 ltp1d 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l < ( l + 1 ) )
271 elfzle1 
 |-  ( i e. ( ( l + 1 ) ... h ) -> ( l + 1 ) <_ i )
272 271 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( l + 1 ) <_ i )
273 266 269 265 270 272 ltletrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> l < i )
274 263 266 265 268 273 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 < i )
275 263 265 274 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ i )
276 275 adantll 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> 0 <_ i )
277 264 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. RR )
278 259 zred 
 |-  ( h e. ( 0 ..^ M ) -> M e. RR )
279 278 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> M e. RR )
280 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> h e. RR )
281 elfzle2 
 |-  ( i e. ( ( l + 1 ) ... h ) -> i <_ h )
282 281 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ h )
283 elfzolt2 
 |-  ( h e. ( 0 ..^ M ) -> h < M )
284 283 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> h < M )
285 277 280 279 282 284 lelttrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i < M )
286 277 279 285 ltled 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ M )
287 286 adantlr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i <_ M )
288 258 260 262 276 287 elfzd 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. ( 0 ... M ) )
289 288 adantlll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> i e. ( 0 ... M ) )
290 257 289 26 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( V ` i ) e. RR )
291 290 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) /\ i e. ( ( l + 1 ) ... h ) ) -> ( V ` i ) e. RR )
292 simplll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ph )
293 0zd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 e. ZZ )
294 elfzelz 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i e. ZZ )
295 294 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ZZ )
296 0red 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 e. RR )
297 295 zred 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. RR )
298 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l e. RR )
299 267 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 <_ l )
300 298 243 syl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( l + 1 ) e. RR )
301 298 ltp1d 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l < ( l + 1 ) )
302 elfzle1 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> ( l + 1 ) <_ i )
303 302 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( l + 1 ) <_ i )
304 298 300 297 301 303 ltletrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> l < i )
305 296 298 297 299 304 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 < i )
306 296 297 305 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> 0 <_ i )
307 eluz2 
 |-  ( i e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ i e. ZZ /\ 0 <_ i ) )
308 293 295 306 307 syl3anbrc 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
309 308 adantll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
310 elfzoel2 
 |-  ( l e. ( 0 ..^ M ) -> M e. ZZ )
311 310 ad2antlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> M e. ZZ )
312 294 zred 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i e. RR )
313 312 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. RR )
314 peano2rem 
 |-  ( h e. RR -> ( h - 1 ) e. RR )
315 246 314 syl 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) e. RR )
316 315 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( h - 1 ) e. RR )
317 278 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> M e. RR )
318 elfzle2 
 |-  ( i e. ( ( l + 1 ) ... ( h - 1 ) ) -> i <_ ( h - 1 ) )
319 318 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i <_ ( h - 1 ) )
320 246 ltm1d 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) < h )
321 315 246 278 320 283 lttrd 
 |-  ( h e. ( 0 ..^ M ) -> ( h - 1 ) < M )
322 321 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( h - 1 ) < M )
323 313 316 317 319 322 lelttrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
324 323 adantll 
 |-  ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
325 324 adantlr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i < M )
326 elfzo2 
 |-  ( i e. ( 0 ..^ M ) <-> ( i e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ i < M ) )
327 309 311 325 326 syl3anbrc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> i e. ( 0 ..^ M ) )
328 169 26 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
329 47 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
330 329 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
331 328 190 330 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
332 292 327 331 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
333 332 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) /\ i e. ( ( l + 1 ) ... ( h - 1 ) ) ) -> ( V ` i ) <_ ( V ` ( i + 1 ) ) )
334 256 291 333 monoord 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( l + 1 ) <_ h ) -> ( V ` ( l + 1 ) ) <_ ( V ` h ) )
335 249 334 syldan 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> ( V ` ( l + 1 ) ) <_ ( V ` h ) )
336 236 241 335 lensymd 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ -. h < ( l + 1 ) ) -> -. ( V ` h ) < ( V ` ( l + 1 ) ) )
337 336 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ -. h < ( l + 1 ) ) -> -. ( V ` h ) < ( V ` ( l + 1 ) ) )
338 230 337 condan 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> h < ( l + 1 ) )
339 zleltp1 
 |-  ( ( h e. ZZ /\ l e. ZZ ) -> ( h <_ l <-> h < ( l + 1 ) ) )
340 227 229 339 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( h <_ l <-> h < ( l + 1 ) ) )
341 338 340 mpbird 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> h <_ l )
342 eluz2 
 |-  ( l e. ( ZZ>= ` h ) <-> ( h e. ZZ /\ l e. ZZ /\ h <_ l ) )
343 227 229 341 342 syl3anbrc 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> l e. ( ZZ>= ` h ) )
344 25 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> V : ( 0 ... M ) --> RR )
345 0zd 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> 0 e. ZZ )
346 259 ad2antrr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> M e. ZZ )
347 elfzelz 
 |-  ( i e. ( h ... l ) -> i e. ZZ )
348 347 adantl 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ZZ )
349 0red 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 e. RR )
350 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> h e. RR )
351 347 zred 
 |-  ( i e. ( h ... l ) -> i e. RR )
352 351 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i e. RR )
353 elfzole1 
 |-  ( h e. ( 0 ..^ M ) -> 0 <_ h )
354 353 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 <_ h )
355 elfzle1 
 |-  ( i e. ( h ... l ) -> h <_ i )
356 355 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> h <_ i )
357 349 350 352 354 356 letrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> 0 <_ i )
358 357 adantlr 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> 0 <_ i )
359 351 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i e. RR )
360 310 zred 
 |-  ( l e. ( 0 ..^ M ) -> M e. RR )
361 360 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> M e. RR )
362 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> l e. RR )
363 elfzle2 
 |-  ( i e. ( h ... l ) -> i <_ l )
364 363 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i <_ l )
365 elfzolt2 
 |-  ( l e. ( 0 ..^ M ) -> l < M )
366 365 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> l < M )
367 359 362 361 364 366 lelttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i < M )
368 359 361 367 ltled 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... l ) ) -> i <_ M )
369 368 adantll 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i <_ M )
370 345 346 348 358 369 elfzd 
 |-  ( ( ( h e. ( 0 ..^ M ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ( 0 ... M ) )
371 370 adantlll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> i e. ( 0 ... M ) )
372 344 371 ffvelcdmd 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... l ) ) -> ( V ` i ) e. RR )
373 372 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... l ) ) -> ( V ` i ) e. RR )
374 simp-4l 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> ph )
375 0zd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 e. ZZ )
376 elfzelz 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i e. ZZ )
377 376 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ZZ )
378 0red 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 e. RR )
379 246 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> h e. RR )
380 377 zred 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. RR )
381 353 adantr 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 <_ h )
382 elfzle1 
 |-  ( i e. ( h ... ( l - 1 ) ) -> h <_ i )
383 382 adantl 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> h <_ i )
384 378 379 380 381 383 letrd 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> 0 <_ i )
385 375 377 384 307 syl3anbrc 
 |-  ( ( h e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
386 385 adantll 
 |-  ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
387 386 ad4ant14 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( ZZ>= ` 0 ) )
388 310 ad3antlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> M e. ZZ )
389 376 zred 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i e. RR )
390 389 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. RR )
391 242 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> l e. RR )
392 360 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> M e. RR )
393 elfzle2 
 |-  ( i e. ( h ... ( l - 1 ) ) -> i <_ ( l - 1 ) )
394 393 adantl 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i <_ ( l - 1 ) )
395 zltlem1 
 |-  ( ( i e. ZZ /\ l e. ZZ ) -> ( i < l <-> i <_ ( l - 1 ) ) )
396 376 228 395 syl2anr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> ( i < l <-> i <_ ( l - 1 ) ) )
397 394 396 mpbird 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < l )
398 365 adantr 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> l < M )
399 390 391 392 397 398 lttrd 
 |-  ( ( l e. ( 0 ..^ M ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
400 399 adantll 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
401 400 adantlr 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i < M )
402 387 388 401 326 syl3anbrc 
 |-  ( ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) /\ i e. ( h ... ( l - 1 ) ) ) -> i e. ( 0 ..^ M ) )
403 374 402 331 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 ) ) )
404 343 373 403 monoord 
 |-  ( ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` h ) < ( V ` ( l + 1 ) ) ) -> ( V ` h ) <_ ( V ` l ) )
405 225 404 chvarvv 
 |-  ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( l + 1 ) ) ) -> ( V ` k ) <_ ( V ` l ) )
406 217 405 chvarvv 
 |-  ( ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i e. ( 0 ..^ M ) ) /\ ( V ` k ) < ( V ` ( i + 1 ) ) ) -> ( V ` k ) <_ ( V ` i ) )
407 110 112 208 406 syl21anc 
 |-  ( ch -> ( V ` k ) <_ ( V ` i ) )
408 107 112 jca 
 |-  ( ch -> ( ph /\ i e. ( 0 ..^ M ) ) )
409 110 149 syl 
 |-  ( ch -> ( Q ` ( k + 1 ) ) e. RR )
410 179 simpld 
 |-  ( ch -> ( Q ` i ) <_ ( S ` J ) )
411 176 143 138 410 164 lelttrd 
 |-  ( ch -> ( Q ` i ) < ( S ` ( J + 1 ) ) )
412 166 simprd 
 |-  ( ch -> ( S ` ( J + 1 ) ) <_ ( Q ` ( k + 1 ) ) )
413 176 138 409 411 412 ltletrd 
 |-  ( ch -> ( Q ` i ) < ( Q ` ( k + 1 ) ) )
414 176 409 118 413 ltadd2dd 
 |-  ( ch -> ( X + ( Q ` i ) ) < ( X + ( Q ` ( k + 1 ) ) ) )
415 175 oveq2d 
 |-  ( ch -> ( X + ( Q ` i ) ) = ( X + ( ( V ` i ) - X ) ) )
416 107 172 26 syl2anc 
 |-  ( ch -> ( V ` i ) e. RR )
417 416 recnd 
 |-  ( ch -> ( V ` i ) e. CC )
418 184 417 pncan3d 
 |-  ( ch -> ( X + ( ( V ` i ) - X ) ) = ( V ` i ) )
419 415 418 eqtr2d 
 |-  ( ch -> ( V ` i ) = ( X + ( Q ` i ) ) )
420 9 a1i 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
421 fveq2 
 |-  ( i = ( k + 1 ) -> ( V ` i ) = ( V ` ( k + 1 ) ) )
422 421 oveq1d 
 |-  ( i = ( k + 1 ) -> ( ( V ` i ) - X ) = ( ( V ` ( k + 1 ) ) - X ) )
423 422 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ..^ M ) ) /\ i = ( k + 1 ) ) -> ( ( V ` i ) - X ) = ( ( V ` ( k + 1 ) ) - X ) )
424 25 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
425 424 148 ffvelcdmd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( V ` ( k + 1 ) ) e. RR )
426 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> X e. RR )
427 425 426 resubcld 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( ( V ` ( k + 1 ) ) - X ) e. RR )
428 420 423 148 427 fvmptd 
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` ( k + 1 ) ) = ( ( V ` ( k + 1 ) ) - X ) )
429 107 109 428 syl2anc 
 |-  ( ch -> ( Q ` ( k + 1 ) ) = ( ( V ` ( k + 1 ) ) - X ) )
430 429 oveq2d 
 |-  ( ch -> ( X + ( Q ` ( k + 1 ) ) ) = ( X + ( ( V ` ( k + 1 ) ) - X ) ) )
431 110 425 syl 
 |-  ( ch -> ( V ` ( k + 1 ) ) e. RR )
432 431 recnd 
 |-  ( ch -> ( V ` ( k + 1 ) ) e. CC )
433 184 432 pncan3d 
 |-  ( ch -> ( X + ( ( V ` ( k + 1 ) ) - X ) ) = ( V ` ( k + 1 ) ) )
434 430 433 eqtr2d 
 |-  ( ch -> ( V ` ( k + 1 ) ) = ( X + ( Q ` ( k + 1 ) ) ) )
435 414 419 434 3brtr4d 
 |-  ( ch -> ( V ` i ) < ( V ` ( k + 1 ) ) )
436 eleq1w 
 |-  ( l = k -> ( l e. ( 0 ..^ M ) <-> k e. ( 0 ..^ M ) ) )
437 436 anbi2d 
 |-  ( l = k -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) ) )
438 oveq1 
 |-  ( l = k -> ( l + 1 ) = ( k + 1 ) )
439 438 fveq2d 
 |-  ( l = k -> ( V ` ( l + 1 ) ) = ( V ` ( k + 1 ) ) )
440 439 breq2d 
 |-  ( l = k -> ( ( V ` i ) < ( V ` ( l + 1 ) ) <-> ( V ` i ) < ( V ` ( k + 1 ) ) ) )
441 437 440 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 ) ) ) ) )
442 fveq2 
 |-  ( l = k -> ( V ` l ) = ( V ` k ) )
443 442 breq2d 
 |-  ( l = k -> ( ( V ` i ) <_ ( V ` l ) <-> ( V ` i ) <_ ( V ` k ) ) )
444 441 443 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 ) ) ) )
445 eleq1w 
 |-  ( h = i -> ( h e. ( 0 ..^ M ) <-> i e. ( 0 ..^ M ) ) )
446 445 anbi2d 
 |-  ( h = i -> ( ( ph /\ h e. ( 0 ..^ M ) ) <-> ( ph /\ i e. ( 0 ..^ M ) ) ) )
447 446 anbi1d 
 |-  ( h = i -> ( ( ( ph /\ h e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) <-> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) ) )
448 fveq2 
 |-  ( h = i -> ( V ` h ) = ( V ` i ) )
449 448 breq1d 
 |-  ( h = i -> ( ( V ` h ) < ( V ` ( l + 1 ) ) <-> ( V ` i ) < ( V ` ( l + 1 ) ) ) )
450 447 449 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 ) ) ) ) )
451 448 breq1d 
 |-  ( h = i -> ( ( V ` h ) <_ ( V ` l ) <-> ( V ` i ) <_ ( V ` l ) ) )
452 450 451 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 ) ) ) )
453 452 404 chvarvv 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ l e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( l + 1 ) ) ) -> ( V ` i ) <_ ( V ` l ) )
454 444 453 chvarvv 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ k e. ( 0 ..^ M ) ) /\ ( V ` i ) < ( V ` ( k + 1 ) ) ) -> ( V ` i ) <_ ( V ` k ) )
455 408 109 435 454 syl21anc 
 |-  ( ch -> ( V ` i ) <_ ( V ` k ) )
456 117 416 letri3d 
 |-  ( ch -> ( ( V ` k ) = ( V ` i ) <-> ( ( V ` k ) <_ ( V ` i ) /\ ( V ` i ) <_ ( V ` k ) ) ) )
457 407 455 456 mpbir2and 
 |-  ( ch -> ( V ` k ) = ( V ` i ) )
458 2 3 4 fourierdlem34 
 |-  ( ph -> V : ( 0 ... M ) -1-1-> RR )
459 107 458 syl 
 |-  ( ch -> V : ( 0 ... M ) -1-1-> RR )
460 f1fveq 
 |-  ( ( V : ( 0 ... M ) -1-1-> RR /\ ( k e. ( 0 ... M ) /\ i e. ( 0 ... M ) ) ) -> ( ( V ` k ) = ( V ` i ) <-> k = i ) )
461 459 115 172 460 syl12anc 
 |-  ( ch -> ( ( V ` k ) = ( V ` i ) <-> k = i ) )
462 457 461 mpbid 
 |-  ( ch -> k = i )
463 15 462 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 )
464 463 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 ) )
465 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 ) ) ) )
466 fveq2 
 |-  ( k = i -> ( Q ` k ) = ( Q ` i ) )
467 oveq1 
 |-  ( k = i -> ( k + 1 ) = ( i + 1 ) )
468 467 fveq2d 
 |-  ( k = i -> ( Q ` ( k + 1 ) ) = ( Q ` ( i + 1 ) ) )
469 466 468 oveq12d 
 |-  ( k = i -> ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
470 469 eqcomd 
 |-  ( k = i -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
471 470 adantl 
 |-  ( ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ k = i ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
472 465 471 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 ) ) ) )
473 472 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 ) ) ) ) )
474 473 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 ) ) ) ) )
475 464 474 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 ) )
476 475 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 ) )
477 476 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 ) ) )
478 477 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 ) ) )
479 104 478 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 ) )
480 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 ) )
481 479 480 sylibr 
 |-  ( ph -> E! k e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
482 fveq2 
 |-  ( i = k -> ( Q ` i ) = ( Q ` k ) )
483 oveq1 
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
484 483 fveq2d 
 |-  ( i = k -> ( Q ` ( i + 1 ) ) = ( Q ` ( k + 1 ) ) )
485 482 484 oveq12d 
 |-  ( i = k -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` k ) (,) ( Q ` ( k + 1 ) ) ) )
486 485 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 ) ) ) ) )
487 486 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 ) ) ) )
488 481 487 sylibr 
 |-  ( ph -> E! i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
489 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 ) )
490 488 489 syl 
 |-  ( ph -> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( 0 ..^ M ) )
491 14 490 eqeltrid 
 |-  ( ph -> U e. ( 0 ..^ M ) )
492 14 eqcomi 
 |-  ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U
493 492 a1i 
 |-  ( ph -> ( iota_ i e. ( 0 ..^ M ) ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = U )
494 fveq2 
 |-  ( i = U -> ( Q ` i ) = ( Q ` U ) )
495 oveq1 
 |-  ( i = U -> ( i + 1 ) = ( U + 1 ) )
496 495 fveq2d 
 |-  ( i = U -> ( Q ` ( i + 1 ) ) = ( Q ` ( U + 1 ) ) )
497 494 496 oveq12d 
 |-  ( i = U -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
498 497 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 ) ) ) ) )
499 498 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 ) )
500 491 488 499 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 ) )
501 493 500 mpbird 
 |-  ( ph -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
502 491 501 jca 
 |-  ( ph -> ( U e. ( 0 ..^ M ) /\ ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )