Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem80.f |
|- ( ph -> F : RR --> RR ) |
2 |
|
fourierdlem80.xre |
|- ( ph -> X e. RR ) |
3 |
|
fourierdlem80.a |
|- ( ph -> A e. RR ) |
4 |
|
fourierdlem80.b |
|- ( ph -> B e. RR ) |
5 |
|
fourierdlem80.ab |
|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) ) |
6 |
|
fourierdlem80.n0 |
|- ( ph -> -. 0 e. ( A [,] B ) ) |
7 |
|
fourierdlem80.c |
|- ( ph -> C e. RR ) |
8 |
|
fourierdlem80.o |
|- O = ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
9 |
|
fourierdlem80.i |
|- I = ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) |
10 |
|
fourierdlem80.fbdioo |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w ) |
11 |
|
fourierdlem80.fdvbdioo |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) |
12 |
|
fourierdlem80.sf |
|- ( ph -> S : ( 0 ... N ) --> ( A [,] B ) ) |
13 |
|
fourierdlem80.slt |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) ) |
14 |
|
fourierdlem80.sjss |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) ) |
15 |
|
fourierdlem80.relioo |
|- ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0 ..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) |
16 |
|
fdv |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` I ) ) : I --> RR ) |
17 |
|
fourierdlem80.y |
|- Y = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
18 |
|
fourierdlem80.ch |
|- ( ch <-> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) |
19 |
|
oveq2 |
|- ( s = t -> ( X + s ) = ( X + t ) ) |
20 |
19
|
fveq2d |
|- ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) ) |
21 |
20
|
oveq1d |
|- ( s = t -> ( ( F ` ( X + s ) ) - C ) = ( ( F ` ( X + t ) ) - C ) ) |
22 |
|
oveq1 |
|- ( s = t -> ( s / 2 ) = ( t / 2 ) ) |
23 |
22
|
fveq2d |
|- ( s = t -> ( sin ` ( s / 2 ) ) = ( sin ` ( t / 2 ) ) ) |
24 |
23
|
oveq2d |
|- ( s = t -> ( 2 x. ( sin ` ( s / 2 ) ) ) = ( 2 x. ( sin ` ( t / 2 ) ) ) ) |
25 |
21 24
|
oveq12d |
|- ( s = t -> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) |
26 |
25
|
cbvmptv |
|- ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) |
27 |
8 26
|
eqtr2i |
|- ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) = O |
28 |
27
|
oveq2i |
|- ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) = ( RR _D O ) |
29 |
28
|
dmeqi |
|- dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) = dom ( RR _D O ) |
30 |
29
|
ineq2i |
|- ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) = ( ran S i^i dom ( RR _D O ) ) |
31 |
30
|
sneqi |
|- { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } = { ( ran S i^i dom ( RR _D O ) ) } |
32 |
31
|
uneq1i |
|- ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
33 |
|
snfi |
|- { ( ran S i^i dom ( RR _D O ) ) } e. Fin |
34 |
|
fzofi |
|- ( 0 ..^ N ) e. Fin |
35 |
|
eqid |
|- ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
36 |
35
|
rnmptfi |
|- ( ( 0 ..^ N ) e. Fin -> ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin ) |
37 |
34 36
|
ax-mp |
|- ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin |
38 |
|
unfi |
|- ( ( { ( ran S i^i dom ( RR _D O ) ) } e. Fin /\ ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin ) -> ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin ) |
39 |
33 37 38
|
mp2an |
|- ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin |
40 |
39
|
a1i |
|- ( ph -> ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin ) |
41 |
32 40
|
eqeltrid |
|- ( ph -> ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin ) |
42 |
|
id |
|- ( s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
43 |
32
|
unieqi |
|- U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
44 |
42 43
|
eleqtrdi |
|- ( s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
45 |
|
simpl |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ph ) |
46 |
|
uniun |
|- U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
47 |
46
|
eleq2i |
|- ( s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> s e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
48 |
|
elun |
|- ( s e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
49 |
47 48
|
sylbb |
|- ( s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
50 |
49
|
adantl |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
51 |
|
ovex |
|- ( 0 ... N ) e. _V |
52 |
51
|
a1i |
|- ( ph -> ( 0 ... N ) e. _V ) |
53 |
12 52
|
fexd |
|- ( ph -> S e. _V ) |
54 |
|
rnexg |
|- ( S e. _V -> ran S e. _V ) |
55 |
|
inex1g |
|- ( ran S e. _V -> ( ran S i^i dom ( RR _D O ) ) e. _V ) |
56 |
|
unisng |
|- ( ( ran S i^i dom ( RR _D O ) ) e. _V -> U. { ( ran S i^i dom ( RR _D O ) ) } = ( ran S i^i dom ( RR _D O ) ) ) |
57 |
53 54 55 56
|
4syl |
|- ( ph -> U. { ( ran S i^i dom ( RR _D O ) ) } = ( ran S i^i dom ( RR _D O ) ) ) |
58 |
57
|
eleq2d |
|- ( ph -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } <-> s e. ( ran S i^i dom ( RR _D O ) ) ) ) |
59 |
58
|
adantr |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } <-> s e. ( ran S i^i dom ( RR _D O ) ) ) ) |
60 |
59
|
orbi1d |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) ) |
61 |
50 60
|
mpbid |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
62 |
|
dvf |
|- ( RR _D O ) : dom ( RR _D O ) --> CC |
63 |
62
|
a1i |
|- ( s e. ( ran S i^i dom ( RR _D O ) ) -> ( RR _D O ) : dom ( RR _D O ) --> CC ) |
64 |
|
elinel2 |
|- ( s e. ( ran S i^i dom ( RR _D O ) ) -> s e. dom ( RR _D O ) ) |
65 |
63 64
|
ffvelcdmd |
|- ( s e. ( ran S i^i dom ( RR _D O ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
66 |
65
|
adantl |
|- ( ( ph /\ s e. ( ran S i^i dom ( RR _D O ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
67 |
|
ovex |
|- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) e. _V |
68 |
67
|
dfiun3 |
|- U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
69 |
68
|
eleq2i |
|- ( s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) <-> s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
70 |
69
|
biimpri |
|- ( s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
71 |
70
|
adantl |
|- ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
72 |
|
eliun |
|- ( s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) <-> E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
73 |
71 72
|
sylib |
|- ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
74 |
|
nfv |
|- F/ j ph |
75 |
|
nfmpt1 |
|- F/_ j ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
76 |
75
|
nfrn |
|- F/_ j ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
77 |
76
|
nfuni |
|- F/_ j U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
78 |
77
|
nfcri |
|- F/ j s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
79 |
74 78
|
nfan |
|- F/ j ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
80 |
|
nfv |
|- F/ j ( ( RR _D O ) ` s ) e. CC |
81 |
62
|
a1i |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( RR _D O ) : dom ( RR _D O ) --> CC ) |
82 |
8
|
reseq1i |
|- ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
83 |
|
ioossicc |
|- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) |
84 |
83 14
|
sstrid |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) ) |
85 |
84
|
resmptd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
86 |
82 85
|
eqtrid |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
87 |
17 86
|
eqtr4id |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Y = ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
88 |
87
|
oveq2d |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D Y ) = ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
89 |
|
ax-resscn |
|- RR C_ CC |
90 |
89
|
a1i |
|- ( ph -> RR C_ CC ) |
91 |
1
|
adantr |
|- ( ( ph /\ s e. ( A [,] B ) ) -> F : RR --> RR ) |
92 |
2
|
adantr |
|- ( ( ph /\ s e. ( A [,] B ) ) -> X e. RR ) |
93 |
3 4
|
iccssred |
|- ( ph -> ( A [,] B ) C_ RR ) |
94 |
93
|
sselda |
|- ( ( ph /\ s e. ( A [,] B ) ) -> s e. RR ) |
95 |
92 94
|
readdcld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( X + s ) e. RR ) |
96 |
91 95
|
ffvelcdmd |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. RR ) |
97 |
96
|
recnd |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. CC ) |
98 |
7
|
recnd |
|- ( ph -> C e. CC ) |
99 |
98
|
adantr |
|- ( ( ph /\ s e. ( A [,] B ) ) -> C e. CC ) |
100 |
97 99
|
subcld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC ) |
101 |
|
2cnd |
|- ( ( ph /\ s e. ( A [,] B ) ) -> 2 e. CC ) |
102 |
93 90
|
sstrd |
|- ( ph -> ( A [,] B ) C_ CC ) |
103 |
102
|
sselda |
|- ( ( ph /\ s e. ( A [,] B ) ) -> s e. CC ) |
104 |
103
|
halfcld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( s / 2 ) e. CC ) |
105 |
104
|
sincld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( sin ` ( s / 2 ) ) e. CC ) |
106 |
101 105
|
mulcld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC ) |
107 |
|
2ne0 |
|- 2 =/= 0 |
108 |
107
|
a1i |
|- ( ( ph /\ s e. ( A [,] B ) ) -> 2 =/= 0 ) |
109 |
5
|
sselda |
|- ( ( ph /\ s e. ( A [,] B ) ) -> s e. ( -u _pi [,] _pi ) ) |
110 |
|
eqcom |
|- ( s = 0 <-> 0 = s ) |
111 |
110
|
biimpi |
|- ( s = 0 -> 0 = s ) |
112 |
111
|
adantl |
|- ( ( s e. ( A [,] B ) /\ s = 0 ) -> 0 = s ) |
113 |
|
simpl |
|- ( ( s e. ( A [,] B ) /\ s = 0 ) -> s e. ( A [,] B ) ) |
114 |
112 113
|
eqeltrd |
|- ( ( s e. ( A [,] B ) /\ s = 0 ) -> 0 e. ( A [,] B ) ) |
115 |
114
|
adantll |
|- ( ( ( ph /\ s e. ( A [,] B ) ) /\ s = 0 ) -> 0 e. ( A [,] B ) ) |
116 |
6
|
ad2antrr |
|- ( ( ( ph /\ s e. ( A [,] B ) ) /\ s = 0 ) -> -. 0 e. ( A [,] B ) ) |
117 |
115 116
|
pm2.65da |
|- ( ( ph /\ s e. ( A [,] B ) ) -> -. s = 0 ) |
118 |
117
|
neqned |
|- ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 ) |
119 |
|
fourierdlem44 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
120 |
109 118 119
|
syl2anc |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
121 |
101 105 108 120
|
mulne0d |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 ) |
122 |
100 106 121
|
divcld |
|- ( ( ph /\ s e. ( A [,] B ) ) -> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC ) |
123 |
122 8
|
fmptd |
|- ( ph -> O : ( A [,] B ) --> CC ) |
124 |
|
ioossre |
|- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR |
125 |
124
|
a1i |
|- ( ph -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR ) |
126 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
127 |
126
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
128 |
126 127
|
dvres |
|- ( ( ( RR C_ CC /\ O : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ RR /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR ) ) -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
129 |
90 123 93 125 128
|
syl22anc |
|- ( ph -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
130 |
|
ioontr |
|- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |
131 |
130
|
reseq2i |
|- ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
132 |
129 131
|
eqtrdi |
|- ( ph -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
133 |
132
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
134 |
88 133
|
eqtr2d |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( RR _D Y ) ) |
135 |
134
|
dmeqd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = dom ( RR _D Y ) ) |
136 |
1
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> F : RR --> RR ) |
137 |
2
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> X e. RR ) |
138 |
93
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ RR ) |
139 |
12
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> ( A [,] B ) ) |
140 |
|
elfzofz |
|- ( j e. ( 0 ..^ N ) -> j e. ( 0 ... N ) ) |
141 |
140
|
adantl |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ... N ) ) |
142 |
139 141
|
ffvelcdmd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. ( A [,] B ) ) |
143 |
138 142
|
sseldd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR ) |
144 |
|
fzofzp1 |
|- ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. ( 0 ... N ) ) |
145 |
144
|
adantl |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. ( 0 ... N ) ) |
146 |
139 145
|
ffvelcdmd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. ( A [,] B ) ) |
147 |
138 146
|
sseldd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR ) |
148 |
9
|
feq2i |
|- ( ( RR _D ( F |` I ) ) : I --> RR <-> ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR ) |
149 |
16 148
|
sylib |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR ) |
150 |
9
|
reseq2i |
|- ( F |` I ) = ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) |
151 |
150
|
oveq2i |
|- ( RR _D ( F |` I ) ) = ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) |
152 |
151
|
feq1i |
|- ( ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR <-> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR ) |
153 |
149 152
|
sylib |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR ) |
154 |
5
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ ( -u _pi [,] _pi ) ) |
155 |
84 154
|
sstrd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) ) |
156 |
6
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( A [,] B ) ) |
157 |
84 156
|
ssneldd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
158 |
7
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> C e. RR ) |
159 |
136 137 143 147 153 155 157 158 17
|
fourierdlem57 |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR /\ ( RR _D Y ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) ) /\ ( RR _D ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( cos ` ( s / 2 ) ) ) ) |
160 |
159
|
simpli |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR /\ ( RR _D Y ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) ) |
161 |
160
|
simpld |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR ) |
162 |
|
fdm |
|- ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
163 |
161 162
|
syl |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
164 |
135 163
|
eqtr2d |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
165 |
|
resss |
|- ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ ( RR _D O ) |
166 |
|
dmss |
|- ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ ( RR _D O ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ dom ( RR _D O ) ) |
167 |
165 166
|
mp1i |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ dom ( RR _D O ) ) |
168 |
164 167
|
eqsstrd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ dom ( RR _D O ) ) |
169 |
168
|
3adant3 |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ dom ( RR _D O ) ) |
170 |
|
simp3 |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
171 |
169 170
|
sseldd |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. dom ( RR _D O ) ) |
172 |
81 171
|
ffvelcdmd |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
173 |
172
|
3exp |
|- ( ph -> ( j e. ( 0 ..^ N ) -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) ) ) |
174 |
173
|
adantr |
|- ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( j e. ( 0 ..^ N ) -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) ) ) |
175 |
79 80 174
|
rexlimd |
|- ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) ) |
176 |
73 175
|
mpd |
|- ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
177 |
66 176
|
jaodan |
|- ( ( ph /\ ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
178 |
45 61 177
|
syl2anc |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) |
179 |
178
|
abscld |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) |
180 |
44 179
|
sylan2 |
|- ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) |
181 |
|
id |
|- ( r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
182 |
181 32
|
eleqtrdi |
|- ( r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
183 |
|
elsni |
|- ( r e. { ( ran S i^i dom ( RR _D O ) ) } -> r = ( ran S i^i dom ( RR _D O ) ) ) |
184 |
|
simpr |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> r = ( ran S i^i dom ( RR _D O ) ) ) |
185 |
|
fzfid |
|- ( ph -> ( 0 ... N ) e. Fin ) |
186 |
|
rnffi |
|- ( ( S : ( 0 ... N ) --> ( A [,] B ) /\ ( 0 ... N ) e. Fin ) -> ran S e. Fin ) |
187 |
12 185 186
|
syl2anc |
|- ( ph -> ran S e. Fin ) |
188 |
|
infi |
|- ( ran S e. Fin -> ( ran S i^i dom ( RR _D O ) ) e. Fin ) |
189 |
187 188
|
syl |
|- ( ph -> ( ran S i^i dom ( RR _D O ) ) e. Fin ) |
190 |
189
|
adantr |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> ( ran S i^i dom ( RR _D O ) ) e. Fin ) |
191 |
184 190
|
eqeltrd |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> r e. Fin ) |
192 |
|
nfv |
|- F/ s ph |
193 |
|
nfcv |
|- F/_ s ran S |
194 |
|
nfcv |
|- F/_ s RR |
195 |
|
nfcv |
|- F/_ s _D |
196 |
|
nfmpt1 |
|- F/_ s ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
197 |
8 196
|
nfcxfr |
|- F/_ s O |
198 |
194 195 197
|
nfov |
|- F/_ s ( RR _D O ) |
199 |
198
|
nfdm |
|- F/_ s dom ( RR _D O ) |
200 |
193 199
|
nfin |
|- F/_ s ( ran S i^i dom ( RR _D O ) ) |
201 |
200
|
nfeq2 |
|- F/ s r = ( ran S i^i dom ( RR _D O ) ) |
202 |
192 201
|
nfan |
|- F/ s ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) |
203 |
|
simpr |
|- ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. r ) |
204 |
|
simpl |
|- ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> r = ( ran S i^i dom ( RR _D O ) ) ) |
205 |
203 204
|
eleqtrd |
|- ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. ( ran S i^i dom ( RR _D O ) ) ) |
206 |
205 64
|
syl |
|- ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. dom ( RR _D O ) ) |
207 |
206
|
adantll |
|- ( ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) /\ s e. r ) -> s e. dom ( RR _D O ) ) |
208 |
62
|
ffvelcdmi |
|- ( s e. dom ( RR _D O ) -> ( ( RR _D O ) ` s ) e. CC ) |
209 |
208
|
abscld |
|- ( s e. dom ( RR _D O ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) |
210 |
207 209
|
syl |
|- ( ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) /\ s e. r ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) |
211 |
210
|
ex |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> ( s e. r -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) ) |
212 |
202 211
|
ralrimi |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) |
213 |
|
fimaxre3 |
|- ( ( r e. Fin /\ A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
214 |
191 212 213
|
syl2anc |
|- ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
215 |
183 214
|
sylan2 |
|- ( ( ph /\ r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
216 |
215
|
adantlr |
|- ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
217 |
|
simpll |
|- ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> ph ) |
218 |
|
elunnel1 |
|- ( ( r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
219 |
218
|
adantll |
|- ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
220 |
|
vex |
|- r e. _V |
221 |
35
|
elrnmpt |
|- ( r e. _V -> ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
222 |
220 221
|
ax-mp |
|- ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
223 |
222
|
biimpi |
|- ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
224 |
223
|
adantl |
|- ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
225 |
76
|
nfcri |
|- F/ j r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
226 |
74 225
|
nfan |
|- F/ j ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
227 |
|
nfv |
|- F/ j E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y |
228 |
|
reeanv |
|- ( E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) <-> ( E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w /\ E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) |
229 |
10 11 228
|
sylanbrc |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) |
230 |
|
simp1 |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ph /\ j e. ( 0 ..^ N ) ) ) |
231 |
|
simp2l |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> w e. RR ) |
232 |
|
simp2r |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> z e. RR ) |
233 |
230 231 232
|
jca31 |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) ) |
234 |
|
simp3l |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> A. t e. I ( abs ` ( F ` t ) ) <_ w ) |
235 |
|
simp3r |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) |
236 |
233 234 235
|
jca31 |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) |
237 |
236 18
|
sylibr |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ch ) |
238 |
18
|
biimpi |
|- ( ch -> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) |
239 |
|
simp-5l |
|- ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> ph ) |
240 |
238 239
|
syl |
|- ( ch -> ph ) |
241 |
240 1
|
syl |
|- ( ch -> F : RR --> RR ) |
242 |
240 2
|
syl |
|- ( ch -> X e. RR ) |
243 |
|
simp-4l |
|- ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> ( ph /\ j e. ( 0 ..^ N ) ) ) |
244 |
238 243
|
syl |
|- ( ch -> ( ph /\ j e. ( 0 ..^ N ) ) ) |
245 |
244 143
|
syl |
|- ( ch -> ( S ` j ) e. RR ) |
246 |
244 147
|
syl |
|- ( ch -> ( S ` ( j + 1 ) ) e. RR ) |
247 |
244 13
|
syl |
|- ( ch -> ( S ` j ) < ( S ` ( j + 1 ) ) ) |
248 |
14 154
|
sstrd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) ) |
249 |
244 248
|
syl |
|- ( ch -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) ) |
250 |
14 156
|
ssneldd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) ) |
251 |
244 250
|
syl |
|- ( ch -> -. 0 e. ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) ) |
252 |
244 153
|
syl |
|- ( ch -> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR ) |
253 |
|
simp-4r |
|- ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> w e. RR ) |
254 |
238 253
|
syl |
|- ( ch -> w e. RR ) |
255 |
238
|
simplrd |
|- ( ch -> A. t e. I ( abs ` ( F ` t ) ) <_ w ) |
256 |
|
id |
|- ( t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) -> t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) |
257 |
256 9
|
eleqtrrdi |
|- ( t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) -> t e. I ) |
258 |
|
rspa |
|- ( ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ t e. I ) -> ( abs ` ( F ` t ) ) <_ w ) |
259 |
255 257 258
|
syl2an |
|- ( ( ch /\ t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w ) |
260 |
|
simpllr |
|- ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> z e. RR ) |
261 |
238 260
|
syl |
|- ( ch -> z e. RR ) |
262 |
151
|
fveq1i |
|- ( ( RR _D ( F |` I ) ) ` t ) = ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) |
263 |
262
|
fveq2i |
|- ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) = ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) ) |
264 |
238
|
simprd |
|- ( ch -> A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) |
265 |
264
|
r19.21bi |
|- ( ( ch /\ t e. I ) -> ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) |
266 |
263 265
|
eqbrtrrid |
|- ( ( ch /\ t e. I ) -> ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) ) <_ z ) |
267 |
257 266
|
sylan2 |
|- ( ( ch /\ t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) ) <_ z ) |
268 |
240 7
|
syl |
|- ( ch -> C e. RR ) |
269 |
241 242 245 246 247 249 251 252 254 259 261 267 268 17
|
fourierdlem68 |
|- ( ch -> ( dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
270 |
269
|
simprd |
|- ( ch -> E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) |
271 |
269
|
simpld |
|- ( ch -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
272 |
271
|
raleqdv |
|- ( ch -> ( A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
273 |
272
|
rexbidv |
|- ( ch -> ( E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
274 |
270 273
|
mpbid |
|- ( ch -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) |
275 |
130
|
eqcomi |
|- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
276 |
275
|
reseq2i |
|- ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
277 |
276
|
fveq1i |
|- ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) |
278 |
|
fvres |
|- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( RR _D O ) ` s ) ) |
279 |
278
|
adantl |
|- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( RR _D O ) ` s ) ) |
280 |
244 84
|
syl |
|- ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) ) |
281 |
280
|
resmptd |
|- ( ch -> ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
282 |
82 281
|
eqtrid |
|- ( ch -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
283 |
17 282
|
eqtr4id |
|- ( ch -> Y = ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
284 |
283
|
oveq2d |
|- ( ch -> ( RR _D Y ) = ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
285 |
284
|
fveq1d |
|- ( ch -> ( ( RR _D Y ) ` s ) = ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) ) |
286 |
129
|
fveq1d |
|- ( ph -> ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) ) |
287 |
240 286
|
syl |
|- ( ch -> ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) ) |
288 |
285 287
|
eqtr2d |
|- ( ch -> ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( RR _D Y ) ` s ) ) |
289 |
288
|
adantr |
|- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( RR _D Y ) ` s ) ) |
290 |
277 279 289
|
3eqtr3a |
|- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( RR _D O ) ` s ) = ( ( RR _D Y ) ` s ) ) |
291 |
290
|
fveq2d |
|- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) = ( abs ` ( ( RR _D Y ) ` s ) ) ) |
292 |
291
|
breq1d |
|- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
293 |
292
|
ralbidva |
|- ( ch -> ( A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
294 |
293
|
rexbidv |
|- ( ch -> ( E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) ) |
295 |
274 294
|
mpbird |
|- ( ch -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
296 |
237 295
|
syl |
|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
297 |
296
|
3exp |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( w e. RR /\ z e. RR ) -> ( ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) ) |
298 |
297
|
rexlimdvv |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) |
299 |
229 298
|
mpd |
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
300 |
299
|
3adant3 |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
301 |
|
raleq |
|- ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) |
302 |
301
|
3ad2ant3 |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) |
303 |
302
|
rexbidv |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) |
304 |
300 303
|
mpbird |
|- ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
305 |
304
|
3exp |
|- ( ph -> ( j e. ( 0 ..^ N ) -> ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) ) |
306 |
305
|
adantr |
|- ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( j e. ( 0 ..^ N ) -> ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) ) |
307 |
226 227 306
|
rexlimd |
|- ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) |
308 |
224 307
|
mpd |
|- ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
309 |
217 219 308
|
syl2anc |
|- ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
310 |
216 309
|
pm2.61dan |
|- ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
311 |
182 310
|
sylan2 |
|- ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) |
312 |
|
pm3.22 |
|- ( ( r e. dom ( RR _D O ) /\ r e. ran S ) -> ( r e. ran S /\ r e. dom ( RR _D O ) ) ) |
313 |
|
elin |
|- ( r e. ( ran S i^i dom ( RR _D O ) ) <-> ( r e. ran S /\ r e. dom ( RR _D O ) ) ) |
314 |
312 313
|
sylibr |
|- ( ( r e. dom ( RR _D O ) /\ r e. ran S ) -> r e. ( ran S i^i dom ( RR _D O ) ) ) |
315 |
314
|
adantll |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> r e. ( ran S i^i dom ( RR _D O ) ) ) |
316 |
57
|
eqcomd |
|- ( ph -> ( ran S i^i dom ( RR _D O ) ) = U. { ( ran S i^i dom ( RR _D O ) ) } ) |
317 |
316
|
ad2antrr |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> ( ran S i^i dom ( RR _D O ) ) = U. { ( ran S i^i dom ( RR _D O ) ) } ) |
318 |
315 317
|
eleqtrd |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> r e. U. { ( ran S i^i dom ( RR _D O ) ) } ) |
319 |
318
|
orcd |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
320 |
|
simpll |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ph ) |
321 |
89
|
a1i |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> RR C_ CC ) |
322 |
123
|
adantr |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> O : ( A [,] B ) --> CC ) |
323 |
3
|
adantr |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> A e. RR ) |
324 |
4
|
adantr |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> B e. RR ) |
325 |
323 324
|
iccssred |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> ( A [,] B ) C_ RR ) |
326 |
321 322 325
|
dvbss |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> dom ( RR _D O ) C_ ( A [,] B ) ) |
327 |
|
simpr |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. dom ( RR _D O ) ) |
328 |
326 327
|
sseldd |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. ( A [,] B ) ) |
329 |
328
|
adantr |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> r e. ( A [,] B ) ) |
330 |
|
simpr |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> -. r e. ran S ) |
331 |
|
fveq2 |
|- ( j = k -> ( S ` j ) = ( S ` k ) ) |
332 |
|
oveq1 |
|- ( j = k -> ( j + 1 ) = ( k + 1 ) ) |
333 |
332
|
fveq2d |
|- ( j = k -> ( S ` ( j + 1 ) ) = ( S ` ( k + 1 ) ) ) |
334 |
331 333
|
oveq12d |
|- ( j = k -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) |
335 |
|
ovex |
|- ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) e. _V |
336 |
334 35 335
|
fvmpt |
|- ( k e. ( 0 ..^ N ) -> ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) = ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) |
337 |
336
|
eleq2d |
|- ( k e. ( 0 ..^ N ) -> ( r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) ) |
338 |
337
|
rexbiia |
|- ( E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> E. k e. ( 0 ..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) |
339 |
15 338
|
sylibr |
|- ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) |
340 |
67 35
|
dmmpti |
|- dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( 0 ..^ N ) |
341 |
340
|
rexeqi |
|- ( E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) |
342 |
339 341
|
sylibr |
|- ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) |
343 |
320 329 330 342
|
syl21anc |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) |
344 |
|
funmpt |
|- Fun ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) |
345 |
|
elunirn |
|- ( Fun ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) ) |
346 |
344 345
|
mp1i |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ( r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) ) |
347 |
343 346
|
mpbird |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) |
348 |
347
|
olcd |
|- ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
349 |
319 348
|
pm2.61dan |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
350 |
|
elun |
|- ( r e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
351 |
349 350
|
sylibr |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
352 |
351 46
|
eleqtrrdi |
|- ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
353 |
352
|
ralrimiva |
|- ( ph -> A. r e. dom ( RR _D O ) r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
354 |
|
dfss3 |
|- ( dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> A. r e. dom ( RR _D O ) r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
355 |
353 354
|
sylibr |
|- ( ph -> dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
356 |
355 43
|
sseqtrrdi |
|- ( ph -> dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) |
357 |
41 180 311 356
|
ssfiunibd |
|- ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) |