Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem54.t |
|- T = ( B - A ) |
2 |
|
fourierdlem54.p |
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
3 |
|
fourierdlem54.m |
|- ( ph -> M e. NN ) |
4 |
|
fourierdlem54.q |
|- ( ph -> Q e. ( P ` M ) ) |
5 |
|
fourierdlem54.c |
|- ( ph -> C e. RR ) |
6 |
|
fourierdlem54.d |
|- ( ph -> D e. RR ) |
7 |
|
fourierdlem54.cd |
|- ( ph -> C < D ) |
8 |
|
fourierdlem54.o |
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
9 |
|
fourierdlem54.h |
|- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) |
10 |
|
fourierdlem54.n |
|- N = ( ( # ` H ) - 1 ) |
11 |
|
fourierdlem54.s |
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) ) |
12 |
|
2z |
|- 2 e. ZZ |
13 |
12
|
a1i |
|- ( ph -> 2 e. ZZ ) |
14 |
|
prid1g |
|- ( C e. RR -> C e. { C , D } ) |
15 |
|
elun1 |
|- ( C e. { C , D } -> C e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
16 |
5 14 15
|
3syl |
|- ( ph -> C e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
17 |
16 9
|
eleqtrrdi |
|- ( ph -> C e. H ) |
18 |
17
|
ne0d |
|- ( ph -> H =/= (/) ) |
19 |
|
prfi |
|- { C , D } e. Fin |
20 |
2 3 4
|
fourierdlem11 |
|- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) ) |
21 |
20
|
simp1d |
|- ( ph -> A e. RR ) |
22 |
20
|
simp2d |
|- ( ph -> B e. RR ) |
23 |
20
|
simp3d |
|- ( ph -> A < B ) |
24 |
2 3 4
|
fourierdlem15 |
|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) ) |
25 |
|
frn |
|- ( Q : ( 0 ... M ) --> ( A [,] B ) -> ran Q C_ ( A [,] B ) ) |
26 |
24 25
|
syl |
|- ( ph -> ran Q C_ ( A [,] B ) ) |
27 |
2
|
fourierdlem2 |
|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
28 |
3 27
|
syl |
|- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
29 |
4 28
|
mpbid |
|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) |
30 |
29
|
simpld |
|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) ) |
31 |
|
elmapi |
|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR ) |
32 |
|
ffn |
|- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) ) |
33 |
30 31 32
|
3syl |
|- ( ph -> Q Fn ( 0 ... M ) ) |
34 |
|
fzfid |
|- ( ph -> ( 0 ... M ) e. Fin ) |
35 |
|
fnfi |
|- ( ( Q Fn ( 0 ... M ) /\ ( 0 ... M ) e. Fin ) -> Q e. Fin ) |
36 |
33 34 35
|
syl2anc |
|- ( ph -> Q e. Fin ) |
37 |
|
rnfi |
|- ( Q e. Fin -> ran Q e. Fin ) |
38 |
36 37
|
syl |
|- ( ph -> ran Q e. Fin ) |
39 |
29
|
simprd |
|- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
40 |
39
|
simpld |
|- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) ) |
41 |
40
|
simpld |
|- ( ph -> ( Q ` 0 ) = A ) |
42 |
3
|
nnnn0d |
|- ( ph -> M e. NN0 ) |
43 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
44 |
42 43
|
eleqtrdi |
|- ( ph -> M e. ( ZZ>= ` 0 ) ) |
45 |
|
eluzfz1 |
|- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) ) |
46 |
44 45
|
syl |
|- ( ph -> 0 e. ( 0 ... M ) ) |
47 |
|
fnfvelrn |
|- ( ( Q Fn ( 0 ... M ) /\ 0 e. ( 0 ... M ) ) -> ( Q ` 0 ) e. ran Q ) |
48 |
33 46 47
|
syl2anc |
|- ( ph -> ( Q ` 0 ) e. ran Q ) |
49 |
41 48
|
eqeltrrd |
|- ( ph -> A e. ran Q ) |
50 |
40
|
simprd |
|- ( ph -> ( Q ` M ) = B ) |
51 |
|
eluzfz2 |
|- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) ) |
52 |
44 51
|
syl |
|- ( ph -> M e. ( 0 ... M ) ) |
53 |
|
fnfvelrn |
|- ( ( Q Fn ( 0 ... M ) /\ M e. ( 0 ... M ) ) -> ( Q ` M ) e. ran Q ) |
54 |
33 52 53
|
syl2anc |
|- ( ph -> ( Q ` M ) e. ran Q ) |
55 |
50 54
|
eqeltrrd |
|- ( ph -> B e. ran Q ) |
56 |
|
eqid |
|- ( abs o. - ) = ( abs o. - ) |
57 |
|
eqid |
|- ( ( ran Q X. ran Q ) \ _I ) = ( ( ran Q X. ran Q ) \ _I ) |
58 |
|
eqid |
|- ran ( ( abs o. - ) |` ( ( ran Q X. ran Q ) \ _I ) ) = ran ( ( abs o. - ) |` ( ( ran Q X. ran Q ) \ _I ) ) |
59 |
|
eqid |
|- inf ( ran ( ( abs o. - ) |` ( ( ran Q X. ran Q ) \ _I ) ) , RR , < ) = inf ( ran ( ( abs o. - ) |` ( ( ran Q X. ran Q ) \ _I ) ) , RR , < ) |
60 |
|
eqid |
|- ( topGen ` ran (,) ) = ( topGen ` ran (,) ) |
61 |
|
eqid |
|- ( ( topGen ` ran (,) ) |`t ( C [,] D ) ) = ( ( topGen ` ran (,) ) |`t ( C [,] D ) ) |
62 |
|
oveq1 |
|- ( x = w -> ( x + ( k x. T ) ) = ( w + ( k x. T ) ) ) |
63 |
62
|
eleq1d |
|- ( x = w -> ( ( x + ( k x. T ) ) e. ran Q <-> ( w + ( k x. T ) ) e. ran Q ) ) |
64 |
63
|
rexbidv |
|- ( x = w -> ( E. k e. ZZ ( x + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( w + ( k x. T ) ) e. ran Q ) ) |
65 |
64
|
cbvrabv |
|- { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } = { w e. ( C [,] D ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } |
66 |
|
oveq1 |
|- ( i = j -> ( i x. T ) = ( j x. T ) ) |
67 |
66
|
oveq2d |
|- ( i = j -> ( y + ( i x. T ) ) = ( y + ( j x. T ) ) ) |
68 |
67
|
eleq1d |
|- ( i = j -> ( ( y + ( i x. T ) ) e. ran Q <-> ( y + ( j x. T ) ) e. ran Q ) ) |
69 |
68
|
anbi1d |
|- ( i = j -> ( ( ( y + ( i x. T ) ) e. ran Q /\ ( z + ( l x. T ) ) e. ran Q ) <-> ( ( y + ( j x. T ) ) e. ran Q /\ ( z + ( l x. T ) ) e. ran Q ) ) ) |
70 |
|
oveq1 |
|- ( l = k -> ( l x. T ) = ( k x. T ) ) |
71 |
70
|
oveq2d |
|- ( l = k -> ( z + ( l x. T ) ) = ( z + ( k x. T ) ) ) |
72 |
71
|
eleq1d |
|- ( l = k -> ( ( z + ( l x. T ) ) e. ran Q <-> ( z + ( k x. T ) ) e. ran Q ) ) |
73 |
72
|
anbi2d |
|- ( l = k -> ( ( ( y + ( j x. T ) ) e. ran Q /\ ( z + ( l x. T ) ) e. ran Q ) <-> ( ( y + ( j x. T ) ) e. ran Q /\ ( z + ( k x. T ) ) e. ran Q ) ) ) |
74 |
69 73
|
cbvrex2vw |
|- ( E. i e. ZZ E. l e. ZZ ( ( y + ( i x. T ) ) e. ran Q /\ ( z + ( l x. T ) ) e. ran Q ) <-> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. ran Q /\ ( z + ( k x. T ) ) e. ran Q ) ) |
75 |
74
|
anbi2i |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) /\ E. i e. ZZ E. l e. ZZ ( ( y + ( i x. T ) ) e. ran Q /\ ( z + ( l x. T ) ) e. ran Q ) ) <-> ( ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. ran Q /\ ( z + ( k x. T ) ) e. ran Q ) ) ) |
76 |
21 22 23 1 26 38 49 55 56 57 58 59 5 6 60 61 65 75
|
fourierdlem42 |
|- ( ph -> { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } e. Fin ) |
77 |
|
unfi |
|- ( ( { C , D } e. Fin /\ { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } e. Fin ) -> ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) e. Fin ) |
78 |
19 76 77
|
sylancr |
|- ( ph -> ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) e. Fin ) |
79 |
9 78
|
eqeltrid |
|- ( ph -> H e. Fin ) |
80 |
|
hashnncl |
|- ( H e. Fin -> ( ( # ` H ) e. NN <-> H =/= (/) ) ) |
81 |
79 80
|
syl |
|- ( ph -> ( ( # ` H ) e. NN <-> H =/= (/) ) ) |
82 |
18 81
|
mpbird |
|- ( ph -> ( # ` H ) e. NN ) |
83 |
82
|
nnzd |
|- ( ph -> ( # ` H ) e. ZZ ) |
84 |
5 7
|
ltned |
|- ( ph -> C =/= D ) |
85 |
|
hashprg |
|- ( ( C e. RR /\ D e. RR ) -> ( C =/= D <-> ( # ` { C , D } ) = 2 ) ) |
86 |
5 6 85
|
syl2anc |
|- ( ph -> ( C =/= D <-> ( # ` { C , D } ) = 2 ) ) |
87 |
84 86
|
mpbid |
|- ( ph -> ( # ` { C , D } ) = 2 ) |
88 |
87
|
eqcomd |
|- ( ph -> 2 = ( # ` { C , D } ) ) |
89 |
|
ssun1 |
|- { C , D } C_ ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) |
90 |
89
|
a1i |
|- ( ph -> { C , D } C_ ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
91 |
90 9
|
sseqtrrdi |
|- ( ph -> { C , D } C_ H ) |
92 |
|
hashssle |
|- ( ( H e. Fin /\ { C , D } C_ H ) -> ( # ` { C , D } ) <_ ( # ` H ) ) |
93 |
79 91 92
|
syl2anc |
|- ( ph -> ( # ` { C , D } ) <_ ( # ` H ) ) |
94 |
88 93
|
eqbrtrd |
|- ( ph -> 2 <_ ( # ` H ) ) |
95 |
|
eluz2 |
|- ( ( # ` H ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` H ) e. ZZ /\ 2 <_ ( # ` H ) ) ) |
96 |
13 83 94 95
|
syl3anbrc |
|- ( ph -> ( # ` H ) e. ( ZZ>= ` 2 ) ) |
97 |
|
uz2m1nn |
|- ( ( # ` H ) e. ( ZZ>= ` 2 ) -> ( ( # ` H ) - 1 ) e. NN ) |
98 |
96 97
|
syl |
|- ( ph -> ( ( # ` H ) - 1 ) e. NN ) |
99 |
10 98
|
eqeltrid |
|- ( ph -> N e. NN ) |
100 |
|
prssg |
|- ( ( C e. RR /\ D e. RR ) -> ( ( C e. RR /\ D e. RR ) <-> { C , D } C_ RR ) ) |
101 |
5 6 100
|
syl2anc |
|- ( ph -> ( ( C e. RR /\ D e. RR ) <-> { C , D } C_ RR ) ) |
102 |
5 6 101
|
mpbi2and |
|- ( ph -> { C , D } C_ RR ) |
103 |
|
ssrab2 |
|- { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } C_ ( C [,] D ) |
104 |
5 6
|
iccssred |
|- ( ph -> ( C [,] D ) C_ RR ) |
105 |
103 104
|
sstrid |
|- ( ph -> { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } C_ RR ) |
106 |
102 105
|
unssd |
|- ( ph -> ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) C_ RR ) |
107 |
9 106
|
eqsstrid |
|- ( ph -> H C_ RR ) |
108 |
79 107 11 10
|
fourierdlem36 |
|- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) ) |
109 |
|
df-isom |
|- ( S Isom < , < ( ( 0 ... N ) , H ) <-> ( S : ( 0 ... N ) -1-1-onto-> H /\ A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) ) ) |
110 |
108 109
|
sylib |
|- ( ph -> ( S : ( 0 ... N ) -1-1-onto-> H /\ A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) ) ) |
111 |
110
|
simpld |
|- ( ph -> S : ( 0 ... N ) -1-1-onto-> H ) |
112 |
|
f1of |
|- ( S : ( 0 ... N ) -1-1-onto-> H -> S : ( 0 ... N ) --> H ) |
113 |
111 112
|
syl |
|- ( ph -> S : ( 0 ... N ) --> H ) |
114 |
113 107
|
fssd |
|- ( ph -> S : ( 0 ... N ) --> RR ) |
115 |
|
reex |
|- RR e. _V |
116 |
|
ovex |
|- ( 0 ... N ) e. _V |
117 |
116
|
a1i |
|- ( ph -> ( 0 ... N ) e. _V ) |
118 |
|
elmapg |
|- ( ( RR e. _V /\ ( 0 ... N ) e. _V ) -> ( S e. ( RR ^m ( 0 ... N ) ) <-> S : ( 0 ... N ) --> RR ) ) |
119 |
115 117 118
|
sylancr |
|- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) <-> S : ( 0 ... N ) --> RR ) ) |
120 |
114 119
|
mpbird |
|- ( ph -> S e. ( RR ^m ( 0 ... N ) ) ) |
121 |
|
df-f1o |
|- ( S : ( 0 ... N ) -1-1-onto-> H <-> ( S : ( 0 ... N ) -1-1-> H /\ S : ( 0 ... N ) -onto-> H ) ) |
122 |
111 121
|
sylib |
|- ( ph -> ( S : ( 0 ... N ) -1-1-> H /\ S : ( 0 ... N ) -onto-> H ) ) |
123 |
122
|
simprd |
|- ( ph -> S : ( 0 ... N ) -onto-> H ) |
124 |
|
dffo3 |
|- ( S : ( 0 ... N ) -onto-> H <-> ( S : ( 0 ... N ) --> H /\ A. h e. H E. y e. ( 0 ... N ) h = ( S ` y ) ) ) |
125 |
123 124
|
sylib |
|- ( ph -> ( S : ( 0 ... N ) --> H /\ A. h e. H E. y e. ( 0 ... N ) h = ( S ` y ) ) ) |
126 |
125
|
simprd |
|- ( ph -> A. h e. H E. y e. ( 0 ... N ) h = ( S ` y ) ) |
127 |
|
eqeq1 |
|- ( h = C -> ( h = ( S ` y ) <-> C = ( S ` y ) ) ) |
128 |
|
eqcom |
|- ( C = ( S ` y ) <-> ( S ` y ) = C ) |
129 |
127 128
|
bitrdi |
|- ( h = C -> ( h = ( S ` y ) <-> ( S ` y ) = C ) ) |
130 |
129
|
rexbidv |
|- ( h = C -> ( E. y e. ( 0 ... N ) h = ( S ` y ) <-> E. y e. ( 0 ... N ) ( S ` y ) = C ) ) |
131 |
130
|
rspcv |
|- ( C e. H -> ( A. h e. H E. y e. ( 0 ... N ) h = ( S ` y ) -> E. y e. ( 0 ... N ) ( S ` y ) = C ) ) |
132 |
17 126 131
|
sylc |
|- ( ph -> E. y e. ( 0 ... N ) ( S ` y ) = C ) |
133 |
|
fveq2 |
|- ( y = 0 -> ( S ` y ) = ( S ` 0 ) ) |
134 |
133
|
eqcomd |
|- ( y = 0 -> ( S ` 0 ) = ( S ` y ) ) |
135 |
134
|
adantl |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` 0 ) = ( S ` y ) ) |
136 |
|
simplr |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` y ) = C ) |
137 |
135 136
|
eqtrd |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` 0 ) = C ) |
138 |
5
|
ad2antrr |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> C e. RR ) |
139 |
137 138
|
eqeltrd |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` 0 ) e. RR ) |
140 |
139 137
|
eqled |
|- ( ( ( ph /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` 0 ) <_ C ) |
141 |
140
|
3adantl2 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ y = 0 ) -> ( S ` 0 ) <_ C ) |
142 |
5
|
rexrd |
|- ( ph -> C e. RR* ) |
143 |
6
|
rexrd |
|- ( ph -> D e. RR* ) |
144 |
5 6 7
|
ltled |
|- ( ph -> C <_ D ) |
145 |
|
lbicc2 |
|- ( ( C e. RR* /\ D e. RR* /\ C <_ D ) -> C e. ( C [,] D ) ) |
146 |
142 143 144 145
|
syl3anc |
|- ( ph -> C e. ( C [,] D ) ) |
147 |
|
ubicc2 |
|- ( ( C e. RR* /\ D e. RR* /\ C <_ D ) -> D e. ( C [,] D ) ) |
148 |
142 143 144 147
|
syl3anc |
|- ( ph -> D e. ( C [,] D ) ) |
149 |
|
prssg |
|- ( ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) -> ( ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) <-> { C , D } C_ ( C [,] D ) ) ) |
150 |
146 148 149
|
syl2anc |
|- ( ph -> ( ( C e. ( C [,] D ) /\ D e. ( C [,] D ) ) <-> { C , D } C_ ( C [,] D ) ) ) |
151 |
146 148 150
|
mpbi2and |
|- ( ph -> { C , D } C_ ( C [,] D ) ) |
152 |
103
|
a1i |
|- ( ph -> { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } C_ ( C [,] D ) ) |
153 |
151 152
|
unssd |
|- ( ph -> ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) C_ ( C [,] D ) ) |
154 |
9 153
|
eqsstrid |
|- ( ph -> H C_ ( C [,] D ) ) |
155 |
|
nnm1nn0 |
|- ( ( # ` H ) e. NN -> ( ( # ` H ) - 1 ) e. NN0 ) |
156 |
82 155
|
syl |
|- ( ph -> ( ( # ` H ) - 1 ) e. NN0 ) |
157 |
10 156
|
eqeltrid |
|- ( ph -> N e. NN0 ) |
158 |
157 43
|
eleqtrdi |
|- ( ph -> N e. ( ZZ>= ` 0 ) ) |
159 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) ) |
160 |
158 159
|
syl |
|- ( ph -> 0 e. ( 0 ... N ) ) |
161 |
113 160
|
ffvelrnd |
|- ( ph -> ( S ` 0 ) e. H ) |
162 |
154 161
|
sseldd |
|- ( ph -> ( S ` 0 ) e. ( C [,] D ) ) |
163 |
104 162
|
sseldd |
|- ( ph -> ( S ` 0 ) e. RR ) |
164 |
163
|
adantr |
|- ( ( ph /\ -. y = 0 ) -> ( S ` 0 ) e. RR ) |
165 |
164
|
3ad2antl1 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( S ` 0 ) e. RR ) |
166 |
5
|
adantr |
|- ( ( ph /\ -. y = 0 ) -> C e. RR ) |
167 |
166
|
3ad2antl1 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> C e. RR ) |
168 |
|
elfzelz |
|- ( y e. ( 0 ... N ) -> y e. ZZ ) |
169 |
168
|
zred |
|- ( y e. ( 0 ... N ) -> y e. RR ) |
170 |
169
|
adantr |
|- ( ( y e. ( 0 ... N ) /\ -. y = 0 ) -> y e. RR ) |
171 |
|
elfzle1 |
|- ( y e. ( 0 ... N ) -> 0 <_ y ) |
172 |
171
|
adantr |
|- ( ( y e. ( 0 ... N ) /\ -. y = 0 ) -> 0 <_ y ) |
173 |
|
neqne |
|- ( -. y = 0 -> y =/= 0 ) |
174 |
173
|
adantl |
|- ( ( y e. ( 0 ... N ) /\ -. y = 0 ) -> y =/= 0 ) |
175 |
170 172 174
|
ne0gt0d |
|- ( ( y e. ( 0 ... N ) /\ -. y = 0 ) -> 0 < y ) |
176 |
175
|
3ad2antl2 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> 0 < y ) |
177 |
|
simpl1 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ph ) |
178 |
|
simpl2 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> y e. ( 0 ... N ) ) |
179 |
110
|
simprd |
|- ( ph -> A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) ) |
180 |
|
breq1 |
|- ( x = 0 -> ( x < y <-> 0 < y ) ) |
181 |
|
fveq2 |
|- ( x = 0 -> ( S ` x ) = ( S ` 0 ) ) |
182 |
181
|
breq1d |
|- ( x = 0 -> ( ( S ` x ) < ( S ` y ) <-> ( S ` 0 ) < ( S ` y ) ) ) |
183 |
180 182
|
bibi12d |
|- ( x = 0 -> ( ( x < y <-> ( S ` x ) < ( S ` y ) ) <-> ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) ) |
184 |
183
|
ralbidv |
|- ( x = 0 -> ( A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) <-> A. y e. ( 0 ... N ) ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) ) |
185 |
184
|
rspcv |
|- ( 0 e. ( 0 ... N ) -> ( A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) -> A. y e. ( 0 ... N ) ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) ) |
186 |
160 179 185
|
sylc |
|- ( ph -> A. y e. ( 0 ... N ) ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) |
187 |
186
|
r19.21bi |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) |
188 |
177 178 187
|
syl2anc |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( 0 < y <-> ( S ` 0 ) < ( S ` y ) ) ) |
189 |
176 188
|
mpbid |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( S ` 0 ) < ( S ` y ) ) |
190 |
|
simpl3 |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( S ` y ) = C ) |
191 |
189 190
|
breqtrd |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( S ` 0 ) < C ) |
192 |
165 167 191
|
ltled |
|- ( ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) /\ -. y = 0 ) -> ( S ` 0 ) <_ C ) |
193 |
141 192
|
pm2.61dan |
|- ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = C ) -> ( S ` 0 ) <_ C ) |
194 |
193
|
rexlimdv3a |
|- ( ph -> ( E. y e. ( 0 ... N ) ( S ` y ) = C -> ( S ` 0 ) <_ C ) ) |
195 |
132 194
|
mpd |
|- ( ph -> ( S ` 0 ) <_ C ) |
196 |
|
elicc2 |
|- ( ( C e. RR /\ D e. RR ) -> ( ( S ` 0 ) e. ( C [,] D ) <-> ( ( S ` 0 ) e. RR /\ C <_ ( S ` 0 ) /\ ( S ` 0 ) <_ D ) ) ) |
197 |
5 6 196
|
syl2anc |
|- ( ph -> ( ( S ` 0 ) e. ( C [,] D ) <-> ( ( S ` 0 ) e. RR /\ C <_ ( S ` 0 ) /\ ( S ` 0 ) <_ D ) ) ) |
198 |
162 197
|
mpbid |
|- ( ph -> ( ( S ` 0 ) e. RR /\ C <_ ( S ` 0 ) /\ ( S ` 0 ) <_ D ) ) |
199 |
198
|
simp2d |
|- ( ph -> C <_ ( S ` 0 ) ) |
200 |
163 5
|
letri3d |
|- ( ph -> ( ( S ` 0 ) = C <-> ( ( S ` 0 ) <_ C /\ C <_ ( S ` 0 ) ) ) ) |
201 |
195 199 200
|
mpbir2and |
|- ( ph -> ( S ` 0 ) = C ) |
202 |
|
eluzfz2 |
|- ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) ) |
203 |
158 202
|
syl |
|- ( ph -> N e. ( 0 ... N ) ) |
204 |
113 203
|
ffvelrnd |
|- ( ph -> ( S ` N ) e. H ) |
205 |
154 204
|
sseldd |
|- ( ph -> ( S ` N ) e. ( C [,] D ) ) |
206 |
|
elicc2 |
|- ( ( C e. RR /\ D e. RR ) -> ( ( S ` N ) e. ( C [,] D ) <-> ( ( S ` N ) e. RR /\ C <_ ( S ` N ) /\ ( S ` N ) <_ D ) ) ) |
207 |
5 6 206
|
syl2anc |
|- ( ph -> ( ( S ` N ) e. ( C [,] D ) <-> ( ( S ` N ) e. RR /\ C <_ ( S ` N ) /\ ( S ` N ) <_ D ) ) ) |
208 |
205 207
|
mpbid |
|- ( ph -> ( ( S ` N ) e. RR /\ C <_ ( S ` N ) /\ ( S ` N ) <_ D ) ) |
209 |
208
|
simp3d |
|- ( ph -> ( S ` N ) <_ D ) |
210 |
|
prid2g |
|- ( D e. RR -> D e. { C , D } ) |
211 |
|
elun1 |
|- ( D e. { C , D } -> D e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
212 |
6 210 211
|
3syl |
|- ( ph -> D e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
213 |
212 9
|
eleqtrrdi |
|- ( ph -> D e. H ) |
214 |
|
eqeq1 |
|- ( h = D -> ( h = ( S ` y ) <-> D = ( S ` y ) ) ) |
215 |
|
eqcom |
|- ( D = ( S ` y ) <-> ( S ` y ) = D ) |
216 |
214 215
|
bitrdi |
|- ( h = D -> ( h = ( S ` y ) <-> ( S ` y ) = D ) ) |
217 |
216
|
rexbidv |
|- ( h = D -> ( E. y e. ( 0 ... N ) h = ( S ` y ) <-> E. y e. ( 0 ... N ) ( S ` y ) = D ) ) |
218 |
217
|
rspcv |
|- ( D e. H -> ( A. h e. H E. y e. ( 0 ... N ) h = ( S ` y ) -> E. y e. ( 0 ... N ) ( S ` y ) = D ) ) |
219 |
213 126 218
|
sylc |
|- ( ph -> E. y e. ( 0 ... N ) ( S ` y ) = D ) |
220 |
215
|
biimpri |
|- ( ( S ` y ) = D -> D = ( S ` y ) ) |
221 |
220
|
3ad2ant3 |
|- ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = D ) -> D = ( S ` y ) ) |
222 |
114
|
ffvelrnda |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> ( S ` y ) e. RR ) |
223 |
104 205
|
sseldd |
|- ( ph -> ( S ` N ) e. RR ) |
224 |
223
|
adantr |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> ( S ` N ) e. RR ) |
225 |
169
|
adantl |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> y e. RR ) |
226 |
|
elfzel2 |
|- ( y e. ( 0 ... N ) -> N e. ZZ ) |
227 |
226
|
zred |
|- ( y e. ( 0 ... N ) -> N e. RR ) |
228 |
227
|
adantl |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> N e. RR ) |
229 |
|
elfzle2 |
|- ( y e. ( 0 ... N ) -> y <_ N ) |
230 |
229
|
adantl |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> y <_ N ) |
231 |
225 228 230
|
lensymd |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> -. N < y ) |
232 |
|
breq1 |
|- ( x = N -> ( x < y <-> N < y ) ) |
233 |
|
fveq2 |
|- ( x = N -> ( S ` x ) = ( S ` N ) ) |
234 |
233
|
breq1d |
|- ( x = N -> ( ( S ` x ) < ( S ` y ) <-> ( S ` N ) < ( S ` y ) ) ) |
235 |
232 234
|
bibi12d |
|- ( x = N -> ( ( x < y <-> ( S ` x ) < ( S ` y ) ) <-> ( N < y <-> ( S ` N ) < ( S ` y ) ) ) ) |
236 |
235
|
ralbidv |
|- ( x = N -> ( A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) <-> A. y e. ( 0 ... N ) ( N < y <-> ( S ` N ) < ( S ` y ) ) ) ) |
237 |
236
|
rspcv |
|- ( N e. ( 0 ... N ) -> ( A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) -> A. y e. ( 0 ... N ) ( N < y <-> ( S ` N ) < ( S ` y ) ) ) ) |
238 |
203 179 237
|
sylc |
|- ( ph -> A. y e. ( 0 ... N ) ( N < y <-> ( S ` N ) < ( S ` y ) ) ) |
239 |
238
|
r19.21bi |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> ( N < y <-> ( S ` N ) < ( S ` y ) ) ) |
240 |
231 239
|
mtbid |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> -. ( S ` N ) < ( S ` y ) ) |
241 |
222 224 240
|
nltled |
|- ( ( ph /\ y e. ( 0 ... N ) ) -> ( S ` y ) <_ ( S ` N ) ) |
242 |
241
|
3adant3 |
|- ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = D ) -> ( S ` y ) <_ ( S ` N ) ) |
243 |
221 242
|
eqbrtrd |
|- ( ( ph /\ y e. ( 0 ... N ) /\ ( S ` y ) = D ) -> D <_ ( S ` N ) ) |
244 |
243
|
rexlimdv3a |
|- ( ph -> ( E. y e. ( 0 ... N ) ( S ` y ) = D -> D <_ ( S ` N ) ) ) |
245 |
219 244
|
mpd |
|- ( ph -> D <_ ( S ` N ) ) |
246 |
223 6
|
letri3d |
|- ( ph -> ( ( S ` N ) = D <-> ( ( S ` N ) <_ D /\ D <_ ( S ` N ) ) ) ) |
247 |
209 245 246
|
mpbir2and |
|- ( ph -> ( S ` N ) = D ) |
248 |
|
elfzoelz |
|- ( i e. ( 0 ..^ N ) -> i e. ZZ ) |
249 |
248
|
zred |
|- ( i e. ( 0 ..^ N ) -> i e. RR ) |
250 |
249
|
ltp1d |
|- ( i e. ( 0 ..^ N ) -> i < ( i + 1 ) ) |
251 |
250
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> i < ( i + 1 ) ) |
252 |
179
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) ) |
253 |
|
elfzofz |
|- ( i e. ( 0 ..^ N ) -> i e. ( 0 ... N ) ) |
254 |
253
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ... N ) ) |
255 |
|
fzofzp1 |
|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) ) |
256 |
255
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) ) |
257 |
|
breq1 |
|- ( x = i -> ( x < y <-> i < y ) ) |
258 |
|
fveq2 |
|- ( x = i -> ( S ` x ) = ( S ` i ) ) |
259 |
258
|
breq1d |
|- ( x = i -> ( ( S ` x ) < ( S ` y ) <-> ( S ` i ) < ( S ` y ) ) ) |
260 |
257 259
|
bibi12d |
|- ( x = i -> ( ( x < y <-> ( S ` x ) < ( S ` y ) ) <-> ( i < y <-> ( S ` i ) < ( S ` y ) ) ) ) |
261 |
|
breq2 |
|- ( y = ( i + 1 ) -> ( i < y <-> i < ( i + 1 ) ) ) |
262 |
|
fveq2 |
|- ( y = ( i + 1 ) -> ( S ` y ) = ( S ` ( i + 1 ) ) ) |
263 |
262
|
breq2d |
|- ( y = ( i + 1 ) -> ( ( S ` i ) < ( S ` y ) <-> ( S ` i ) < ( S ` ( i + 1 ) ) ) ) |
264 |
261 263
|
bibi12d |
|- ( y = ( i + 1 ) -> ( ( i < y <-> ( S ` i ) < ( S ` y ) ) <-> ( i < ( i + 1 ) <-> ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) |
265 |
260 264
|
rspc2v |
|- ( ( i e. ( 0 ... N ) /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) -> ( i < ( i + 1 ) <-> ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) |
266 |
254 256 265
|
syl2anc |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( A. x e. ( 0 ... N ) A. y e. ( 0 ... N ) ( x < y <-> ( S ` x ) < ( S ` y ) ) -> ( i < ( i + 1 ) <-> ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) |
267 |
252 266
|
mpd |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i < ( i + 1 ) <-> ( S ` i ) < ( S ` ( i + 1 ) ) ) ) |
268 |
251 267
|
mpbid |
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) ) |
269 |
268
|
ralrimiva |
|- ( ph -> A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) |
270 |
201 247 269
|
jca31 |
|- ( ph -> ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) |
271 |
8
|
fourierdlem2 |
|- ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) ) |
272 |
99 271
|
syl |
|- ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) ) |
273 |
120 270 272
|
mpbir2and |
|- ( ph -> S e. ( O ` N ) ) |
274 |
99 273 108
|
jca31 |
|- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) ) |