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 ) ) ) ) ) |