Metamath Proof Explorer

Theorem fourierdlem78

Description: G is continuous when restricted on an interval not containing 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem78.f 
|- ( ph -> F : RR --> RR )
fourierdlem78.a 
|- ( ph -> A e. ( -u _pi [,] _pi ) )
fourierdlem78.b 
|- ( ph -> B e. ( -u _pi [,] _pi ) )
fourierdlem78.x 
|- ( ph -> X e. RR )
fourierdlem78.nxelab 
|- ( ph -> -. 0 e. ( A (,) B ) )
fourierdlem78.fcn 
|- ( ph -> ( F |` ( ( A + X ) (,) ( B + X ) ) ) e. ( ( ( A + X ) (,) ( B + X ) ) -cn-> CC ) )
fourierdlem78.y 
|- ( ph -> Y e. RR )
fourierdlem78.w 
|- ( ph -> W e. RR )
fourierdlem78.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem78.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem78.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem78.n 
|- ( ph -> N e. RR )
fourierdlem78.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
fourierdlem78.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
Assertion fourierdlem78 
|- ( ph -> ( G |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> RR ) )

Proof

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