Metamath Proof Explorer


Theorem fourierdlem57

Description: The derivative of O . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem57.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem57.xre ( 𝜑𝑋 ∈ ℝ )
fourierdlem57.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem57.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem57.fdv ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
fourierdlem57.ab ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
fourierdlem57.n0 ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
fourierdlem57.c ( 𝜑𝐶 ∈ ℝ )
fourierdlem57.o 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
Assertion fourierdlem57 ( ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) ) ∧ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem57.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
2 fourierdlem57.xre ( 𝜑𝑋 ∈ ℝ )
3 fourierdlem57.a ( 𝜑𝐴 ∈ ℝ )
4 fourierdlem57.b ( 𝜑𝐵 ∈ ℝ )
5 fourierdlem57.fdv ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
6 fourierdlem57.ab ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
7 fourierdlem57.n0 ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
8 fourierdlem57.c ( 𝜑𝐶 ∈ ℝ )
9 fourierdlem57.o 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
10 5 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
11 2 3 readdcld ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ )
12 11 rexrd ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ* )
13 12 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) ∈ ℝ* )
14 2 4 readdcld ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ )
15 14 rexrd ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ* )
16 15 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) ∈ ℝ* )
17 2 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
18 elioore ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
19 18 adantl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
20 17 19 readdcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
21 3 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
22 21 rexrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
23 4 rexrd ( 𝜑𝐵 ∈ ℝ* )
24 23 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
25 simpr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
26 ioogtlb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
27 22 24 25 26 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
28 21 19 17 27 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
29 4 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
30 iooltub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
31 22 24 25 30 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
32 19 29 17 31 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
33 13 16 20 28 32 eliood ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) )
34 10 33 ffvelrnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
35 2re 2 ∈ ℝ
36 35 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℝ )
37 rehalfcl ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) ∈ ℝ )
38 19 37 syl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℝ )
39 38 resincld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
40 36 39 remulcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
41 34 40 remulcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ )
42 38 recoscld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
43 1 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
44 43 20 ffvelrnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
45 8 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ )
46 44 45 resubcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℝ )
47 42 46 remulcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∈ ℝ )
48 41 47 resubcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) ∈ ℝ )
49 40 resqcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ∈ ℝ )
50 2cnd ( 𝑠 ∈ ℝ → 2 ∈ ℂ )
51 37 recnd ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) ∈ ℂ )
52 51 sincld ( 𝑠 ∈ ℝ → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
53 50 52 mulcld ( 𝑠 ∈ ℝ → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
54 19 53 syl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
55 2cnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
56 19 52 syl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
57 2ne0 2 ≠ 0
58 57 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
59 6 sselda ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
60 eqcom ( 𝑠 = 0 ↔ 0 = 𝑠 )
61 60 biimpi ( 𝑠 = 0 → 0 = 𝑠 )
62 61 adantl ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 = 𝑠 )
63 simpl ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
64 62 63 eqeltrd ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
65 64 adantll ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
66 7 ad2antrr ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
67 65 66 pm2.65da ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
68 67 neqned ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
69 fourierdlem44 ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
70 59 68 69 syl2anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
71 55 56 58 70 mulne0d ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
72 2z 2 ∈ ℤ
73 72 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℤ )
74 54 71 73 expne0d ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ≠ 0 )
75 48 49 74 redivcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ∈ ℝ )
76 eqid ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) )
77 75 76 fmptd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
78 9 a1i ( 𝜑𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
79 78 oveq2d ( 𝜑 → ( ℝ D 𝑂 ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
80 reelprrecn ℝ ∈ { ℝ , ℂ }
81 80 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
82 46 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
83 44 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
84 eqid ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
85 1 2 3 4 84 5 fourierdlem28 ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
86 45 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℂ )
87 0red ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
88 iooretop ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
89 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
90 89 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
91 88 90 eleqtri ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
92 91 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
93 8 recnd ( 𝜑𝐶 ∈ ℂ )
94 81 92 93 dvmptconst ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
95 81 83 34 85 86 87 94 dvmptsub ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) )
96 34 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
97 96 subid1d ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
98 97 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
99 95 98 eqtrd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
100 eldifsn ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ ∧ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 ) )
101 54 71 100 sylanbrc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
102 recn ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
103 57 a1i ( 𝑠 ∈ ℝ → 2 ≠ 0 )
104 102 50 103 divrec2d ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) = ( ( 1 / 2 ) · 𝑠 ) )
105 104 eqcomd ( 𝑠 ∈ ℝ → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) )
106 18 105 syl ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) )
107 106 fveq2d ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
108 halfcn ( 1 / 2 ) ∈ ℂ
109 108 a1i ( 𝑠 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
110 id ( 𝑠 ∈ ℂ → 𝑠 ∈ ℂ )
111 109 110 mulcld ( 𝑠 ∈ ℂ → ( ( 1 / 2 ) · 𝑠 ) ∈ ℂ )
112 111 coscld ( 𝑠 ∈ ℂ → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
113 18 102 112 3syl ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
114 107 113 eqeltrrd ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
115 114 adantl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
116 ioossre ( 𝐴 (,) 𝐵 ) ⊆ ℝ
117 resmpt ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
118 116 117 ax-mp ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
119 118 eqcomi ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
120 119 oveq2i ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
121 ax-resscn ℝ ⊆ ℂ
122 eqid ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
123 122 53 fmpti ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ
124 ssid ℝ ⊆ ℝ
125 89 90 dvres ( ( ( ℝ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) )
126 121 123 124 116 125 mp4an ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
127 resmpt ( ℝ ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
128 121 127 ax-mp ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
129 105 fveq2d ( 𝑠 ∈ ℝ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
130 129 oveq2d ( 𝑠 ∈ ℝ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
131 130 mpteq2ia ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
132 128 131 eqtr2i ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ )
133 132 oveq2i ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) )
134 ioontr ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )
135 133 134 reseq12i ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) ↾ ( 𝐴 (,) 𝐵 ) )
136 eqid ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
137 2cnd ( 𝑠 ∈ ℂ → 2 ∈ ℂ )
138 111 sincld ( 𝑠 ∈ ℂ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
139 137 138 mulcld ( 𝑠 ∈ ℂ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ )
140 136 139 fmpti ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ
141 ssid ℂ ⊆ ℂ
142 dmmptg ( ∀ 𝑠 ∈ ℂ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ → dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ℂ )
143 2cn 2 ∈ ℂ
144 143 108 mulcli ( 2 · ( 1 / 2 ) ) ∈ ℂ
145 144 a1i ( 𝑠 ∈ ℂ → ( 2 · ( 1 / 2 ) ) ∈ ℂ )
146 145 112 mulcld ( 𝑠 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ )
147 142 146 mprg dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ℂ
148 121 147 sseqtrri ℝ ⊆ dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
149 dvasinbx ( ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
150 143 108 149 mp2an ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
151 150 dmeqi dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
152 148 151 sseqtrri ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
153 dvres3 ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ) ) → ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) )
154 80 140 141 152 153 mp4an ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ )
155 154 reseq1i ( ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) )
156 150 reseq1i ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ )
157 156 reseq1i ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) )
158 resabs1 ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
159 116 158 ax-mp ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
160 ioosscn ( 𝐴 (,) 𝐵 ) ⊆ ℂ
161 resmpt ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
162 160 161 ax-mp ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
163 157 159 162 3eqtri ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
164 135 155 163 3eqtri ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
165 120 126 164 3eqtri ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
166 143 57 recidi ( 2 · ( 1 / 2 ) ) = 1
167 166 oveq1i ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) )
168 167 a1i ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
169 113 mulid2d ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) )
170 168 169 107 3eqtrd ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
171 170 mpteq2ia ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
172 165 171 eqtri ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
173 172 a1i ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )
174 81 82 34 99 101 115 173 dvmptdiv ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) )
175 79 174 eqtrd ( 𝜑 → ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) )
176 175 feq1d ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
177 77 176 mpbird ( 𝜑 → ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
178 177 175 jca ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) )
179 178 172 pm3.2i ( ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) ) ∧ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )