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