Metamath Proof Explorer


Theorem fourierdlem40

Description: H is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem40.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem40.a ( 𝜑𝐴 ∈ ( - π [,] π ) )
fourierdlem40.b ( 𝜑𝐵 ∈ ( - π [,] π ) )
fourierdlem40.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem40.nxelab ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
fourierdlem40.fcn ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ∈ ( ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) –cn→ ℂ ) )
fourierdlem40.y ( 𝜑𝑌 ∈ ℝ )
fourierdlem40.w ( 𝜑𝑊 ∈ ℝ )
fourierdlem40.h 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
Assertion fourierdlem40 ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem40.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
2 fourierdlem40.a ( 𝜑𝐴 ∈ ( - π [,] π ) )
3 fourierdlem40.b ( 𝜑𝐵 ∈ ( - π [,] π ) )
4 fourierdlem40.x ( 𝜑𝑋 ∈ ℝ )
5 fourierdlem40.nxelab ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
6 fourierdlem40.fcn ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ∈ ( ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) –cn→ ℂ ) )
7 fourierdlem40.y ( 𝜑𝑌 ∈ ℝ )
8 fourierdlem40.w ( 𝜑𝑊 ∈ ℝ )
9 fourierdlem40.h 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
10 9 reseq1i ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
11 10 a1i ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
12 pire π ∈ ℝ
13 12 renegcli - π ∈ ℝ
14 13 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ∈ ℝ )
15 12 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → π ∈ ℝ )
16 elioore ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
17 16 adantl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
18 13 a1i ( 𝜑 → - π ∈ ℝ )
19 12 a1i ( 𝜑 → π ∈ ℝ )
20 18 19 iccssred ( 𝜑 → ( - π [,] π ) ⊆ ℝ )
21 20 2 sseldd ( 𝜑𝐴 ∈ ℝ )
22 21 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
23 13 12 elicc2i ( 𝐴 ∈ ( - π [,] π ) ↔ ( 𝐴 ∈ ℝ ∧ - π ≤ 𝐴𝐴 ≤ π ) )
24 23 simp2bi ( 𝐴 ∈ ( - π [,] π ) → - π ≤ 𝐴 )
25 2 24 syl ( 𝜑 → - π ≤ 𝐴 )
26 25 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ≤ 𝐴 )
27 22 rexrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
28 20 3 sseldd ( 𝜑𝐵 ∈ ℝ )
29 28 rexrd ( 𝜑𝐵 ∈ ℝ* )
30 29 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
31 simpr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
32 ioogtlb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
33 27 30 31 32 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
34 14 22 17 26 33 lelttrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π < 𝑠 )
35 14 17 34 ltled ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ≤ 𝑠 )
36 28 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
37 iooltub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
38 27 30 31 37 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
39 13 12 elicc2i ( 𝐵 ∈ ( - π [,] π ) ↔ ( 𝐵 ∈ ℝ ∧ - π ≤ 𝐵𝐵 ≤ π ) )
40 39 simp3bi ( 𝐵 ∈ ( - π [,] π ) → 𝐵 ≤ π )
41 3 40 syl ( 𝜑𝐵 ≤ π )
42 41 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ≤ π )
43 17 36 15 38 42 ltletrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < π )
44 17 15 43 ltled ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≤ π )
45 14 15 17 35 44 eliccd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
46 45 ex ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ( - π [,] π ) ) )
47 46 ssrdv ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
48 47 resmptd ( 𝜑 → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) )
49 eleq1 ( 𝑠 = 0 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
50 49 biimpac ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
51 50 adantll ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
52 5 ad2antrr ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
53 51 52 pm2.65da ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
54 53 iffalsed ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
55 1 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
56 4 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
57 56 17 readdcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
58 55 57 ffvelrnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
59 7 8 ifcld ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
60 59 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
61 58 60 resubcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
62 61 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
63 17 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
64 53 neqned ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
65 62 63 64 divrecd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) )
66 54 65 eqtrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) )
67 66 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) )
68 11 48 67 3eqtrd ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) )
69 58 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
70 60 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
71 69 70 negsubd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) )
72 71 eqcomd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) )
73 72 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) )
74 21 4 readdcld ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ )
75 74 rexrd ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ* )
76 75 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
77 28 4 readdcld ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ )
78 77 rexrd ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ* )
79 78 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
80 21 recnd ( 𝜑𝐴 ∈ ℂ )
81 4 recnd ( 𝜑𝑋 ∈ ℂ )
82 80 81 addcomd ( 𝜑 → ( 𝐴 + 𝑋 ) = ( 𝑋 + 𝐴 ) )
83 82 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) = ( 𝑋 + 𝐴 ) )
84 22 17 56 33 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
85 83 84 eqbrtrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) < ( 𝑋 + 𝑠 ) )
86 17 36 56 38 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
87 28 recnd ( 𝜑𝐵 ∈ ℂ )
88 81 87 addcomd ( 𝜑 → ( 𝑋 + 𝐵 ) = ( 𝐵 + 𝑋 ) )
89 88 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) = ( 𝐵 + 𝑋 ) )
90 86 89 breqtrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝐵 + 𝑋 ) )
91 76 79 57 85 90 eliood ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) )
92 fvres ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
93 91 92 syl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
94 93 eqcomd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
95 94 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
96 ioosscn ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ⊆ ℂ
97 96 a1i ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ⊆ ℂ )
98 ioosscn ( 𝐴 (,) 𝐵 ) ⊆ ℂ
99 98 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
100 97 6 99 81 91 fourierdlem23 ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
101 95 100 eqeltrd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
102 0red ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
103 21 ad2antrr ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
104 16 adantl ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
105 simplr ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝐴 )
106 33 adantlr ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
107 102 103 104 105 106 lelttrd ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝑠 )
108 107 iftrued ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑌 )
109 108 negeqd ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = - 𝑌 )
110 109 mpteq2dva ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) )
111 7 renegcld ( 𝜑 → - 𝑌 ∈ ℝ )
112 111 recnd ( 𝜑 → - 𝑌 ∈ ℂ )
113 ssid ℂ ⊆ ℂ
114 113 a1i ( 𝜑 → ℂ ⊆ ℂ )
115 99 112 114 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
116 115 adantr ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
117 110 116 eqeltrd ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
118 21 rexrd ( 𝜑𝐴 ∈ ℝ* )
119 118 ad2antrr ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐴 ∈ ℝ* )
120 29 ad2antrr ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ* )
121 0red ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ℝ )
122 simpr ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ¬ 0 ≤ 𝐴 )
123 21 adantr ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
124 0red ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 0 ∈ ℝ )
125 123 124 ltnled ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
126 122 125 mpbird ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐴 < 0 )
127 126 adantr ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐴 < 0 )
128 simpr ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → ¬ 𝐵 ≤ 0 )
129 0red ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ℝ )
130 28 adantr ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ )
131 129 130 ltnled ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → ( 0 < 𝐵 ↔ ¬ 𝐵 ≤ 0 ) )
132 128 131 mpbird ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 0 < 𝐵 )
133 132 adantlr ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 < 𝐵 )
134 119 120 121 127 133 eliood ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
135 5 ad2antrr ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
136 134 135 condan ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐵 ≤ 0 )
137 16 adantl ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
138 0red ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
139 28 ad2antrr ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
140 38 adantlr ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
141 simplr ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ≤ 0 )
142 137 139 138 140 141 ltletrd ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 0 )
143 137 138 142 ltnsymd ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 < 𝑠 )
144 143 iffalsed ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 )
145 144 negeqd ( ( ( 𝜑𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = - 𝑊 )
146 145 mpteq2dva ( ( 𝜑𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) )
147 8 recnd ( 𝜑𝑊 ∈ ℂ )
148 147 negcld ( 𝜑 → - 𝑊 ∈ ℂ )
149 99 148 114 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
150 149 adantr ( ( 𝜑𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
151 146 150 eqeltrd ( ( 𝜑𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
152 136 151 syldan ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
153 117 152 pm2.61dan ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
154 101 153 addcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
155 73 154 eqeltrd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
156 eqid ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) = ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) )
157 1cnd ( 𝜑 → 1 ∈ ℂ )
158 156 cdivcncf ( 1 ∈ ℂ → ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
159 157 158 syl ( 𝜑 → ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
160 velsn ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
161 53 160 sylnibr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 ∈ { 0 } )
162 63 161 eldifd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
163 162 ralrimiva ( 𝜑 → ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
164 dfss3 ( ( 𝐴 (,) 𝐵 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
165 163 164 sylibr ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ℂ ∖ { 0 } ) )
166 17 64 rereccld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑠 ) ∈ ℝ )
167 166 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑠 ) ∈ ℂ )
168 156 159 165 114 167 cncfmptssg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
169 155 168 mulcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
170 68 169 eqeltrd ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )