Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem78.f |
|- ( ph -> F : RR --> RR ) |
2 |
|
fourierdlem78.a |
|- ( ph -> A e. ( -u _pi [,] _pi ) ) |
3 |
|
fourierdlem78.b |
|- ( ph -> B e. ( -u _pi [,] _pi ) ) |
4 |
|
fourierdlem78.x |
|- ( ph -> X e. RR ) |
5 |
|
fourierdlem78.nxelab |
|- ( ph -> -. 0 e. ( A (,) B ) ) |
6 |
|
fourierdlem78.fcn |
|- ( ph -> ( F |` ( ( A + X ) (,) ( B + X ) ) ) e. ( ( ( A + X ) (,) ( B + X ) ) -cn-> CC ) ) |
7 |
|
fourierdlem78.y |
|- ( ph -> Y e. RR ) |
8 |
|
fourierdlem78.w |
|- ( ph -> W e. RR ) |
9 |
|
fourierdlem78.h |
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |
10 |
|
fourierdlem78.k |
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
11 |
|
fourierdlem78.u |
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) ) |
12 |
|
fourierdlem78.n |
|- ( ph -> N e. RR ) |
13 |
|
fourierdlem78.s |
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
14 |
|
fourierdlem78.g |
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |
15 |
14
|
a1i |
|- ( ph -> G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) ) |
16 |
15
|
reseq1d |
|- ( ph -> ( G |` ( A (,) B ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |` ( A (,) B ) ) ) |
17 |
|
pire |
|- _pi e. RR |
18 |
17
|
renegcli |
|- -u _pi e. RR |
19 |
18
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi e. RR ) |
20 |
17
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> _pi e. RR ) |
21 |
|
elioore |
|- ( s e. ( A (,) B ) -> s e. RR ) |
22 |
21
|
adantl |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR ) |
23 |
18
|
a1i |
|- ( ph -> -u _pi e. RR ) |
24 |
17
|
a1i |
|- ( ph -> _pi e. RR ) |
25 |
23 24
|
iccssred |
|- ( ph -> ( -u _pi [,] _pi ) C_ RR ) |
26 |
25 2
|
sseldd |
|- ( ph -> A e. RR ) |
27 |
26
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR ) |
28 |
18 17
|
elicc2i |
|- ( A e. ( -u _pi [,] _pi ) <-> ( A e. RR /\ -u _pi <_ A /\ A <_ _pi ) ) |
29 |
28
|
simp2bi |
|- ( A e. ( -u _pi [,] _pi ) -> -u _pi <_ A ) |
30 |
2 29
|
syl |
|- ( ph -> -u _pi <_ A ) |
31 |
30
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi <_ A ) |
32 |
27
|
rexrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* ) |
33 |
25 3
|
sseldd |
|- ( ph -> B e. RR ) |
34 |
33
|
rexrd |
|- ( ph -> B e. RR* ) |
35 |
34
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* ) |
36 |
|
simpr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) ) |
37 |
|
ioogtlb |
|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s ) |
38 |
32 35 36 37
|
syl3anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> A < s ) |
39 |
19 27 22 31 38
|
lelttrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi < s ) |
40 |
19 22 39
|
ltled |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi <_ s ) |
41 |
33
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR ) |
42 |
|
iooltub |
|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B ) |
43 |
32 35 36 42
|
syl3anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s < B ) |
44 |
18 17
|
elicc2i |
|- ( B e. ( -u _pi [,] _pi ) <-> ( B e. RR /\ -u _pi <_ B /\ B <_ _pi ) ) |
45 |
44
|
simp3bi |
|- ( B e. ( -u _pi [,] _pi ) -> B <_ _pi ) |
46 |
3 45
|
syl |
|- ( ph -> B <_ _pi ) |
47 |
46
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> B <_ _pi ) |
48 |
22 41 20 43 47
|
ltletrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s < _pi ) |
49 |
22 20 48
|
ltled |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s <_ _pi ) |
50 |
19 20 22 40 49
|
eliccd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) ) |
51 |
50
|
ex |
|- ( ph -> ( s e. ( A (,) B ) -> s e. ( -u _pi [,] _pi ) ) ) |
52 |
51
|
ssrdv |
|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) ) |
53 |
52
|
resmptd |
|- ( ph -> ( ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) ) |
54 |
16 53
|
eqtrd |
|- ( ph -> ( G |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) ) |
55 |
|
0red |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR ) |
56 |
1
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR ) |
57 |
4
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR ) |
58 |
57 22
|
readdcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR ) |
59 |
56 58
|
ffvelrnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR ) |
60 |
7 8
|
ifcld |
|- ( ph -> if ( 0 < s , Y , W ) e. RR ) |
61 |
60
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) e. RR ) |
62 |
59 61
|
resubcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. RR ) |
63 |
|
eleq1 |
|- ( s = 0 -> ( s e. ( A (,) B ) <-> 0 e. ( A (,) B ) ) ) |
64 |
63
|
biimpac |
|- ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) ) |
65 |
64
|
adantll |
|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) ) |
66 |
5
|
ad2antrr |
|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) ) |
67 |
65 66
|
pm2.65da |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 ) |
68 |
67
|
neqned |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 ) |
69 |
62 22 68
|
redivcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) e. RR ) |
70 |
55 69
|
ifcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. RR ) |
71 |
9
|
fvmpt2 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. RR ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |
72 |
50 70 71
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |
73 |
72 70
|
eqeltrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( H ` s ) e. RR ) |
74 |
|
1red |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. RR ) |
75 |
|
2re |
|- 2 e. RR |
76 |
75
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. RR ) |
77 |
22
|
rehalfcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR ) |
78 |
77
|
resincld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR ) |
79 |
76 78
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR ) |
80 |
76
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC ) |
81 |
78
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC ) |
82 |
|
2ne0 |
|- 2 =/= 0 |
83 |
82
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 ) |
84 |
|
fourierdlem44 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
85 |
50 68 84
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
86 |
80 81 83 85
|
mulne0d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 ) |
87 |
22 79 86
|
redivcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR ) |
88 |
74 87
|
ifcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. RR ) |
89 |
10
|
fvmpt2 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. RR ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
90 |
50 88 89
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
91 |
90 88
|
eqeltrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) e. RR ) |
92 |
73 91
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( H ` s ) x. ( K ` s ) ) e. RR ) |
93 |
11
|
fvmpt2 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ ( ( H ` s ) x. ( K ` s ) ) e. RR ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) ) |
94 |
50 92 93
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) ) |
95 |
94 92
|
eqeltrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( U ` s ) e. RR ) |
96 |
12
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> N e. RR ) |
97 |
76 83
|
rereccld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / 2 ) e. RR ) |
98 |
96 97
|
readdcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( N + ( 1 / 2 ) ) e. RR ) |
99 |
98 22
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. s ) e. RR ) |
100 |
99
|
resincld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) e. RR ) |
101 |
13
|
fvmpt2 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) e. RR ) -> ( S ` s ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
102 |
50 100 101
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( S ` s ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
103 |
102 100
|
eqeltrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( S ` s ) e. RR ) |
104 |
95 103
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( U ` s ) x. ( S ` s ) ) e. RR ) |
105 |
|
eqid |
|- ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) = ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |
106 |
104 105
|
fmptd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) : ( A (,) B ) --> RR ) |
107 |
|
ax-resscn |
|- RR C_ CC |
108 |
107
|
a1i |
|- ( ph -> RR C_ CC ) |
109 |
94
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( U ` s ) ) = ( s e. ( A (,) B ) |-> ( ( H ` s ) x. ( K ` s ) ) ) ) |
110 |
67
|
iffalsed |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) |
111 |
62
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC ) |
112 |
22
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC ) |
113 |
111 112 68
|
divrecd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) |
114 |
72 110 113
|
3eqtrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( H ` s ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) |
115 |
114
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( H ` s ) ) = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) ) |
116 |
59
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC ) |
117 |
61
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) e. CC ) |
118 |
116 117
|
negsubd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) |
119 |
118
|
eqcomd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) ) |
120 |
119
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) ) ) |
121 |
26 4
|
readdcld |
|- ( ph -> ( A + X ) e. RR ) |
122 |
121
|
rexrd |
|- ( ph -> ( A + X ) e. RR* ) |
123 |
122
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) e. RR* ) |
124 |
33 4
|
readdcld |
|- ( ph -> ( B + X ) e. RR ) |
125 |
124
|
rexrd |
|- ( ph -> ( B + X ) e. RR* ) |
126 |
125
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( B + X ) e. RR* ) |
127 |
26
|
recnd |
|- ( ph -> A e. CC ) |
128 |
4
|
recnd |
|- ( ph -> X e. CC ) |
129 |
127 128
|
addcomd |
|- ( ph -> ( A + X ) = ( X + A ) ) |
130 |
129
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) = ( X + A ) ) |
131 |
27 22 57 38
|
ltadd2dd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) ) |
132 |
130 131
|
eqbrtrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) < ( X + s ) ) |
133 |
22 41 57 43
|
ltadd2dd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) ) |
134 |
33
|
recnd |
|- ( ph -> B e. CC ) |
135 |
128 134
|
addcomd |
|- ( ph -> ( X + B ) = ( B + X ) ) |
136 |
135
|
adantr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) = ( B + X ) ) |
137 |
133 136
|
breqtrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( B + X ) ) |
138 |
123 126 58 132 137
|
eliood |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( A + X ) (,) ( B + X ) ) ) |
139 |
|
fvres |
|- ( ( X + s ) e. ( ( A + X ) (,) ( B + X ) ) -> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) ) |
140 |
138 139
|
syl |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) ) |
141 |
140
|
eqcomd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) ) |
142 |
141
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) ) ) |
143 |
|
ioosscn |
|- ( ( A + X ) (,) ( B + X ) ) C_ CC |
144 |
143
|
a1i |
|- ( ph -> ( ( A + X ) (,) ( B + X ) ) C_ CC ) |
145 |
|
ioosscn |
|- ( A (,) B ) C_ CC |
146 |
145
|
a1i |
|- ( ph -> ( A (,) B ) C_ CC ) |
147 |
144 6 146 128 138
|
fourierdlem23 |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
148 |
142 147
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
149 |
|
0red |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 e. RR ) |
150 |
26
|
ad2antrr |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> A e. RR ) |
151 |
21
|
adantl |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> s e. RR ) |
152 |
|
simplr |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 <_ A ) |
153 |
38
|
adantlr |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> A < s ) |
154 |
149 150 151 152 153
|
lelttrd |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 < s ) |
155 |
154
|
iftrued |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) = Y ) |
156 |
155
|
negeqd |
|- ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> -u if ( 0 < s , Y , W ) = -u Y ) |
157 |
156
|
mpteq2dva |
|- ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) = ( s e. ( A (,) B ) |-> -u Y ) ) |
158 |
7
|
renegcld |
|- ( ph -> -u Y e. RR ) |
159 |
158
|
recnd |
|- ( ph -> -u Y e. CC ) |
160 |
|
ssid |
|- CC C_ CC |
161 |
160
|
a1i |
|- ( ph -> CC C_ CC ) |
162 |
146 159 161
|
constcncfg |
|- ( ph -> ( s e. ( A (,) B ) |-> -u Y ) e. ( ( A (,) B ) -cn-> CC ) ) |
163 |
162
|
adantr |
|- ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u Y ) e. ( ( A (,) B ) -cn-> CC ) ) |
164 |
157 163
|
eqeltrd |
|- ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
165 |
|
simpl |
|- ( ( ph /\ -. 0 <_ A ) -> ph ) |
166 |
26
|
rexrd |
|- ( ph -> A e. RR* ) |
167 |
166
|
ad2antrr |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> A e. RR* ) |
168 |
34
|
ad2antrr |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> B e. RR* ) |
169 |
|
0red |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 e. RR ) |
170 |
|
simpr |
|- ( ( ph /\ -. 0 <_ A ) -> -. 0 <_ A ) |
171 |
26
|
adantr |
|- ( ( ph /\ -. 0 <_ A ) -> A e. RR ) |
172 |
|
0red |
|- ( ( ph /\ -. 0 <_ A ) -> 0 e. RR ) |
173 |
171 172
|
ltnled |
|- ( ( ph /\ -. 0 <_ A ) -> ( A < 0 <-> -. 0 <_ A ) ) |
174 |
170 173
|
mpbird |
|- ( ( ph /\ -. 0 <_ A ) -> A < 0 ) |
175 |
174
|
adantr |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> A < 0 ) |
176 |
|
simpr |
|- ( ( ph /\ -. B <_ 0 ) -> -. B <_ 0 ) |
177 |
|
0red |
|- ( ( ph /\ -. B <_ 0 ) -> 0 e. RR ) |
178 |
33
|
adantr |
|- ( ( ph /\ -. B <_ 0 ) -> B e. RR ) |
179 |
177 178
|
ltnled |
|- ( ( ph /\ -. B <_ 0 ) -> ( 0 < B <-> -. B <_ 0 ) ) |
180 |
176 179
|
mpbird |
|- ( ( ph /\ -. B <_ 0 ) -> 0 < B ) |
181 |
180
|
adantlr |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 < B ) |
182 |
167 168 169 175 181
|
eliood |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 e. ( A (,) B ) ) |
183 |
5
|
ad2antrr |
|- ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> -. 0 e. ( A (,) B ) ) |
184 |
182 183
|
condan |
|- ( ( ph /\ -. 0 <_ A ) -> B <_ 0 ) |
185 |
21
|
adantl |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s e. RR ) |
186 |
|
0red |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> 0 e. RR ) |
187 |
33
|
ad2antrr |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> B e. RR ) |
188 |
43
|
adantlr |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s < B ) |
189 |
|
simplr |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> B <_ 0 ) |
190 |
185 187 186 188 189
|
ltletrd |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s < 0 ) |
191 |
185 186 190
|
ltnsymd |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> -. 0 < s ) |
192 |
191
|
iffalsed |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) = W ) |
193 |
192
|
negeqd |
|- ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> -u if ( 0 < s , Y , W ) = -u W ) |
194 |
193
|
mpteq2dva |
|- ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) = ( s e. ( A (,) B ) |-> -u W ) ) |
195 |
8
|
recnd |
|- ( ph -> W e. CC ) |
196 |
195
|
negcld |
|- ( ph -> -u W e. CC ) |
197 |
146 196 161
|
constcncfg |
|- ( ph -> ( s e. ( A (,) B ) |-> -u W ) e. ( ( A (,) B ) -cn-> CC ) ) |
198 |
197
|
adantr |
|- ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u W ) e. ( ( A (,) B ) -cn-> CC ) ) |
199 |
194 198
|
eqeltrd |
|- ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
200 |
165 184 199
|
syl2anc |
|- ( ( ph /\ -. 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
201 |
164 200
|
pm2.61dan |
|- ( ph -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
202 |
148 201
|
addcncf |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
203 |
120 202
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
204 |
|
eqid |
|- ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) = ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) |
205 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
206 |
204
|
cdivcncf |
|- ( 1 e. CC -> ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) ) |
207 |
205 206
|
syl |
|- ( ph -> ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) ) |
208 |
|
velsn |
|- ( s e. { 0 } <-> s = 0 ) |
209 |
67 208
|
sylnibr |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -. s e. { 0 } ) |
210 |
112 209
|
eldifd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( CC \ { 0 } ) ) |
211 |
210
|
ralrimiva |
|- ( ph -> A. s e. ( A (,) B ) s e. ( CC \ { 0 } ) ) |
212 |
|
dfss3 |
|- ( ( A (,) B ) C_ ( CC \ { 0 } ) <-> A. s e. ( A (,) B ) s e. ( CC \ { 0 } ) ) |
213 |
211 212
|
sylibr |
|- ( ph -> ( A (,) B ) C_ ( CC \ { 0 } ) ) |
214 |
22 68
|
rereccld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / s ) e. RR ) |
215 |
214
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / s ) e. CC ) |
216 |
204 207 213 161 215
|
cncfmptssg |
|- ( ph -> ( s e. ( A (,) B ) |-> ( 1 / s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
217 |
203 216
|
mulcncf |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
218 |
115 217
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( H ` s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
219 |
67
|
iffalsed |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
220 |
79
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC ) |
221 |
112 220 86
|
divrecd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
222 |
90 219 221
|
3eqtrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
223 |
222
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( K ` s ) ) = ( s e. ( A (,) B ) |-> ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ) |
224 |
219 221
|
eqtr2d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
225 |
224
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( A (,) B ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ) |
226 |
|
eqid |
|- ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
227 |
|
cncfss |
|- ( ( RR C_ CC /\ CC C_ CC ) -> ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC ) ) |
228 |
107 160 227
|
mp2an |
|- ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC ) |
229 |
226
|
fourierdlem62 |
|- ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) |
230 |
229
|
a1i |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) ) |
231 |
228 230
|
sseldi |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) |
232 |
88
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC ) |
233 |
226 231 52 161 232
|
cncfmptssg |
|- ( ph -> ( s e. ( A (,) B ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
234 |
225 233
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( s x. ( 1 / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
235 |
223 234
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( K ` s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
236 |
218 235
|
mulcncf |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( H ` s ) x. ( K ` s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
237 |
109 236
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( U ` s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
238 |
102
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( S ` s ) ) = ( s e. ( A (,) B ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) ) |
239 |
|
sincn |
|- sin e. ( CC -cn-> CC ) |
240 |
239
|
a1i |
|- ( ph -> sin e. ( CC -cn-> CC ) ) |
241 |
|
halfre |
|- ( 1 / 2 ) e. RR |
242 |
241
|
a1i |
|- ( ph -> ( 1 / 2 ) e. RR ) |
243 |
12 242
|
readdcld |
|- ( ph -> ( N + ( 1 / 2 ) ) e. RR ) |
244 |
243
|
recnd |
|- ( ph -> ( N + ( 1 / 2 ) ) e. CC ) |
245 |
146 244 161
|
constcncfg |
|- ( ph -> ( s e. ( A (,) B ) |-> ( N + ( 1 / 2 ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
246 |
146 161
|
idcncfg |
|- ( ph -> ( s e. ( A (,) B ) |-> s ) e. ( ( A (,) B ) -cn-> CC ) ) |
247 |
245 246
|
mulcncf |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
248 |
240 247
|
cncfmpt1f |
|- ( ph -> ( s e. ( A (,) B ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
249 |
238 248
|
eqeltrd |
|- ( ph -> ( s e. ( A (,) B ) |-> ( S ` s ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
250 |
237 249
|
mulcncf |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) |
251 |
|
cncffvrn |
|- ( ( RR C_ CC /\ ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) e. ( ( A (,) B ) -cn-> CC ) ) -> ( ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) e. ( ( A (,) B ) -cn-> RR ) <-> ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) : ( A (,) B ) --> RR ) ) |
252 |
108 250 251
|
syl2anc |
|- ( ph -> ( ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) e. ( ( A (,) B ) -cn-> RR ) <-> ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) : ( A (,) B ) --> RR ) ) |
253 |
106 252
|
mpbird |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( U ` s ) x. ( S ` s ) ) ) e. ( ( A (,) B ) -cn-> RR ) ) |
254 |
54 253
|
eqeltrd |
|- ( ph -> ( G |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> RR ) ) |