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 ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem78.a ( 𝜑𝐴 ∈ ( - π [,] π ) )
fourierdlem78.b ( 𝜑𝐵 ∈ ( - π [,] π ) )
fourierdlem78.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem78.nxelab ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
fourierdlem78.fcn ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ∈ ( ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) –cn→ ℂ ) )
fourierdlem78.y ( 𝜑𝑌 ∈ ℝ )
fourierdlem78.w ( 𝜑𝑊 ∈ ℝ )
fourierdlem78.h 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem78.k 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem78.u 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻𝑠 ) · ( 𝐾𝑠 ) ) )
fourierdlem78.n ( 𝜑𝑁 ∈ ℝ )
fourierdlem78.s 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
fourierdlem78.g 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈𝑠 ) · ( 𝑆𝑠 ) ) )
Assertion fourierdlem78 ( 𝜑 → ( 𝐺 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )

Proof

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