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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
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 bilani ⊢ ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 = 𝑠 )
62 simpl ⊢ ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
63 61 62 eqeltrd ⊢ ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
64 63 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
65 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
66 64 65 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
67 66 neqned ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
68 fourierdlem44 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
69 59 67 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
70 55 56 58 69 mulne0d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
71 2z ⊢ 2 ∈ ℤ
72 71 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℤ )
73 54 70 72 expne0d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ≠ 0 )
74 48 49 73 redivcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ∈ ℝ )
75 eqid ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) )
76 74 75 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
77 9 a1i ⊢ ( 𝜑 → 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
78 77 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝑂 ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
79 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
80 79 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
81 46 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
82 44 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
83 eqid ⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
84 1 2 3 4 83 5 fourierdlem28 ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
85 45 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℂ )
86 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
87 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
88 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
89 87 88 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
90 89 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
91 8 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
92 80 90 91 dvmptconst ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
93 80 82 34 84 85 86 92 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) )
94 34 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
95 94 subid1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
96 95 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
97 93 96 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
98 eldifsn ⊢ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ ∧ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 ) )
99 54 70 98 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
100 recn ⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
101 57 a1i ⊢ ( 𝑠 ∈ ℝ → 2 ≠ 0 )
102 100 50 101 divrec2d ⊢ ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) = ( ( 1 / 2 ) · 𝑠 ) )
103 102 eqcomd ⊢ ( 𝑠 ∈ ℝ → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) )
104 18 103 syl ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) )
105 104 fveq2d ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
106 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
107 106 a1i ⊢ ( 𝑠 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
108 id ⊢ ( 𝑠 ∈ ℂ → 𝑠 ∈ ℂ )
109 107 108 mulcld ⊢ ( 𝑠 ∈ ℂ → ( ( 1 / 2 ) · 𝑠 ) ∈ ℂ )
110 109 coscld ⊢ ( 𝑠 ∈ ℂ → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
111 18 100 110 3syl ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
112 105 111 eqeltrrd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
114 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
115 resmpt ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
116 114 115 ax-mp ⊢ ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
117 116 eqcomi ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
118 117 oveq2i ⊢ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
119 ax-resscn ⊢ ℝ ⊆ ℂ
120 eqid ⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
121 120 53 fmpti ⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ
122 ssid ⊢ ℝ ⊆ ℝ
123 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
124 123 88 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) )
125 119 121 122 114 124 mp4an ⊢ ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
126 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
127 119 126 ax-mp ⊢ ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
128 103 fveq2d ⊢ ( 𝑠 ∈ ℝ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
129 128 oveq2d ⊢ ( 𝑠 ∈ ℝ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
130 129 mpteq2ia ⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
131 127 130 eqtr2i ⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ )
132 131 oveq2i ⊢ ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) )
133 ioontr ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )
134 132 133 reseq12i ⊢ ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) ↾ ( 𝐴 (,) 𝐵 ) )
135 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
136 2cnd ⊢ ( 𝑠 ∈ ℂ → 2 ∈ ℂ )
137 109 sincld ⊢ ( 𝑠 ∈ ℂ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ )
138 136 137 mulcld ⊢ ( 𝑠 ∈ ℂ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ )
139 135 138 fmpti ⊢ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ
140 ssid ⊢ ℂ ⊆ ℂ
141 dmmptg ⊢ ( ∀ 𝑠 ∈ ℂ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ → dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ℂ )
142 2cn ⊢ 2 ∈ ℂ
143 142 106 mulcli ⊢ ( 2 · ( 1 / 2 ) ) ∈ ℂ
144 143 a1i ⊢ ( 𝑠 ∈ ℂ → ( 2 · ( 1 / 2 ) ) ∈ ℂ )
145 144 110 mulcld ⊢ ( 𝑠 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ )
146 141 145 mprg ⊢ dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ℂ
147 119 146 sseqtrri ⊢ ℝ ⊆ dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
148 dvasinbx ⊢ ( ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
149 142 106 148 mp2an ⊢ ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
150 149 dmeqi ⊢ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = dom ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
151 147 150 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
152 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ) ) → ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) )
153 79 139 140 151 152 mp4an ⊢ ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ )
154 153 reseq1i ⊢ ( ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) )
155 149 reseq1i ⊢ ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ )
156 155 reseq1i ⊢ ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) )
157 resabs1 ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
158 114 157 ax-mp ⊢ ( ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
159 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
160 resmpt ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) )
161 159 160 ax-mp ⊢ ( ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
162 156 158 161 3eqtri ⊢ ( ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
163 134 154 162 3eqtri ⊢ ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
164 118 125 163 3eqtri ⊢ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
165 142 57 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
166 165 oveq1i ⊢ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) )
167 166 a1i ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) )
168 111 mullidd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 1 · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) )
169 167 168 105 3eqtrd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
170 169 mpteq2ia ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
171 164 170 eqtri ⊢ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
172 171 a1i ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )
173 80 81 34 97 99 113 172 dvmptdiv ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) )
174 78 173 eqtrd ⊢ ( 𝜑 → ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) )
175 174 feq1d ⊢ ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
176 76 175 mpbird ⊢ ( 𝜑 → ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
177 176 174 jca ⊢ ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) )
178 177 171 pm3.2i ⊢ ( ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) ) ∧ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )