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