Metamath Proof Explorer

Theorem fourierdlem68

Description: The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem68.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem68.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem68.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem68.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem68.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem68.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
fourierdlem68.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
fourierdlem68.fdv ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
fourierdlem68.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem68.fbd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝐷 )
fourierdlem68.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
fourierdlem68.fdvbd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) ) ≤ 𝐸 )
fourierdlem68.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem68.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
Assertion fourierdlem68 ( 𝜑 → ( dom ( ℝ D 𝑂 ) = ( 𝐴 (,) 𝐵 ) ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem68.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem68.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem68.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 fourierdlem68.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 fourierdlem68.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
6 fourierdlem68.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
7 fourierdlem68.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
8 fourierdlem68.fdv ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
9 fourierdlem68.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
10 fourierdlem68.fbd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝐷 )
11 fourierdlem68.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
12 fourierdlem68.fdvbd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) ) ≤ 𝐸 )
13 fourierdlem68.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
14 fourierdlem68.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
15 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
16 15 6 sstrid ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
17 15 sseli ⊢ ( 0 ∈ ( 𝐴 (,) 𝐵 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
18 7 17 nsyl ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
19 1 2 3 4 8 16 18 13 14 fourierdlem57 ⊢ ( ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) ) ∧ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )
20 19 simpli ⊢ ( 𝜑 → ( ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( ℝ D 𝑂 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) )
21 20 simpld ⊢ ( 𝜑 → ( ℝ D 𝑂 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
22 21 fdmd ⊢ ( 𝜑 → dom ( ℝ D 𝑂 ) = ( 𝐴 (,) 𝐵 ) )
23 eqid ⊢ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) )
24 3 4 5 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
25 2re ⊢ 2 ∈ ℝ
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ∈ ℝ )
27 3 4 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
28 27 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ℝ )
29 28 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 / 2 ) ∈ ℝ )
30 29 resincld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑡 / 2 ) ) ∈ ℝ )
31 26 30 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ∈ ℝ )
32 2cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ∈ ℂ )
33 30 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑡 / 2 ) ) ∈ ℂ )
34 2ne0 ⊢ 2 ≠ 0
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ≠ 0 )
36 6 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ( - π [,] π ) )
37 eqcom ⊢ ( 𝑡 = 0 ↔ 0 = 𝑡 )
38 37 biimpi ⊢ ( 𝑡 = 0 → 0 = 𝑡 )
39 38 adantl ⊢ ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑡 = 0 ) → 0 = 𝑡 )
40 simpl ⊢ ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑡 = 0 ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
41 39 40 eqeltrd ⊢ ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑡 = 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
42 41 adantll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 = 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
43 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 = 0 ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
44 42 43 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ¬ 𝑡 = 0 )
45 44 neqned ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ≠ 0 )
46 fourierdlem44 ⊢ ( ( 𝑡 ∈ ( - π [,] π ) ∧ 𝑡 ≠ 0 ) → ( sin ‘ ( 𝑡 / 2 ) ) ≠ 0 )
47 36 45 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑡 / 2 ) ) ≠ 0 )
48 32 33 35 47 mulne0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ≠ 0 )
49 eldifsn ⊢ ( ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ∈ ( ℝ ∖ { 0 } ) ↔ ( ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ∈ ℝ ∧ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ≠ 0 ) )
50 31 48 49 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ∈ ( ℝ ∖ { 0 } ) )
51 50 23 fmptd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) )
52 difss ⊢ ( ℝ ∖ { 0 } ) ⊆ ℝ
53 ax-resscn ⊢ ℝ ⊆ ℂ
54 52 53 sstri ⊢ ( ℝ ∖ { 0 } ) ⊆ ℂ
55 54 a1i ⊢ ( 𝜑 → ( ℝ ∖ { 0 } ) ⊆ ℂ )
56 27 53 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
57 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
58 ssid ⊢ ℂ ⊆ ℂ
59 58 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
60 56 57 59 constcncfg ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
61 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
62 61 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
63 56 59 idcncfg ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑡 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
64 eldifsn ⊢ ( 2 ∈ ( ℂ ∖ { 0 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
65 32 35 64 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ∈ ( ℂ ∖ { 0 } ) )
66 eqid ⊢ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 )
67 65 66 fmptd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℂ ∖ { 0 } ) )
68 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
69 cncffvrn ⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℂ ∖ { 0 } ) ) )
70 68 60 69 syl2anc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℂ ∖ { 0 } ) ) )
71 67 70 mpbird ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
72 63 71 divcncf ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑡 / 2 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
73 62 72 cncfmpt1f ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( sin ‘ ( 𝑡 / 2 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
74 60 73 mulcncf ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
75 cncffvrn ⊢ ( ( ( ℝ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) ) )
76 55 74 75 syl2anc ⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) ↔ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) ) )
77 51 76 mpbird ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) )
78 23 3 4 24 77 cncficcgt0 ⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) )
79 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
80 79 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ℝ ∈ { ℝ , ℂ } )
81 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
82 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
83 elioore ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
85 82 84 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
86 81 85 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
87 13 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ )
88 86 87 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℝ )
89 88 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
90 89 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
91 79 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
92 86 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
93 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
94 2 3 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ )
95 94 rexrd ⊢ ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ* )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) ∈ ℝ* )
97 2 4 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ )
98 97 rexrd ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ* )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) ∈ ℝ* )
100 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
101 100 rexrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
102 4 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
104 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
105 ioogtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
106 101 103 104 105 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
107 100 84 82 106 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
108 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
109 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
110 101 103 104 109 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
111 84 108 82 110 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
112 96 99 85 107 111 eliood ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) )
113 93 112 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
114 eqid ⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
115 1 2 3 4 114 8 fourierdlem28 ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
116 87 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℂ )
117 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
118 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
119 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
120 119 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
121 118 120 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
122 121 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
123 13 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
124 91 122 123 dvmptconst ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
125 91 92 113 115 116 117 124 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) )
126 113 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
127 126 subid1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
128 127 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) − 0 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
129 125 128 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
130 129 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
131 126 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
132 2cnd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 2 ∈ ℂ )
133 83 recnd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℂ )
134 133 halfcld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑠 / 2 ) ∈ ℂ )
135 134 sincld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
136 132 135 mulcld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
137 136 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
138 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → 𝐸 ∈ ℝ )
139 1re ⊢ 1 ∈ ℝ
140 25 139 remulcli ⊢ ( 2 · 1 ) ∈ ℝ
141 140 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ( 2 · 1 ) ∈ ℝ )
142 1red ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → 1 ∈ ℝ )
143 123 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
144 9 143 readdcld ⊢ ( 𝜑 → ( 𝐷 + ( abs ‘ 𝐶 ) ) ∈ ℝ )
145 144 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ( 𝐷 + ( abs ‘ 𝐶 ) ) ∈ ℝ )
146 simpl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝜑 )
147 146 112 jca ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
148 eleq1 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↔ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
149 148 anbi2d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ↔ ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) )
150 fveq2 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
151 150 fveq2d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
152 151 breq1d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐸 ) )
153 149 152 imbi12d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ 𝑡 ) ) ≤ 𝐸 ) ↔ ( ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐸 ) ) )
154 153 12 vtoclg ⊢ ( ( 𝑋 + 𝑠 ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐸 ) )
155 85 147 154 sylc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐸 )
156 155 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐸 )
157 132 135 absmuld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( abs ‘ 2 ) · ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
158 0le2 ⊢ 0 ≤ 2
159 absid ⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
160 25 158 159 mp2an ⊢ ( abs ‘ 2 ) = 2
161 160 oveq1i ⊢ ( ( abs ‘ 2 ) · ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 2 · ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) )
162 135 abscld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
163 1red ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 1 ∈ ℝ )
164 25 a1i ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 2 ∈ ℝ )
165 158 a1i ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 0 ≤ 2 )
166 83 rehalfcld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑠 / 2 ) ∈ ℝ )
167 abssinbd ⊢ ( ( 𝑠 / 2 ) ∈ ℝ → ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ≤ 1 )
168 166 167 syl ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ≤ 1 )
169 162 163 164 165 168 lemul2ad ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 2 · ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ) ≤ ( 2 · 1 ) )
170 161 169 eqbrtrid ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( abs ‘ 2 ) · ( abs ‘ ( sin ‘ ( 𝑠 / 2 ) ) ) ) ≤ ( 2 · 1 ) )
171 157 170 eqbrtrd ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ≤ ( 2 · 1 ) )
172 171 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ≤ ( 2 · 1 ) )
173 abscosbd ⊢ ( ( 𝑠 / 2 ) ∈ ℝ → ( abs ‘ ( cos ‘ ( 𝑠 / 2 ) ) ) ≤ 1 )
174 104 166 173 3syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( cos ‘ ( 𝑠 / 2 ) ) ) ≤ 1 )
175 174 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( cos ‘ ( 𝑠 / 2 ) ) ) ≤ 1 )
176 89 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∈ ℝ )
177 92 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ℝ )
178 116 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ 𝐶 ) ∈ ℝ )
179 177 178 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) + ( abs ‘ 𝐶 ) ) ∈ ℝ )
180 9 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ∈ ℝ )
181 180 178 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 + ( abs ‘ 𝐶 ) ) ∈ ℝ )
182 92 116 abs2dif2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) + ( abs ‘ 𝐶 ) ) )
183 fveq2 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
184 183 fveq2d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
185 184 breq1d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝐷 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐷 ) )
186 149 185 imbi12d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐷 ) ) )
187 186 10 vtoclg ⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) → ( ( 𝜑 ∧ ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐷 ) )
188 112 147 187 sylc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ≤ 𝐷 )
189 177 180 178 188 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) + ( abs ‘ 𝐶 ) ) ≤ ( 𝐷 + ( abs ‘ 𝐶 ) ) )
190 176 179 181 182 189 letrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ≤ ( 𝐷 + ( abs ‘ 𝐶 ) ) )
191 190 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ≤ ( 𝐷 + ( abs ‘ 𝐶 ) ) )
192 19 simpri ⊢ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
193 192 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )
194 134 coscld ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
195 194 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
196 simp2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → 𝑐 ∈ ℝ+ )
197 oveq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 / 2 ) = ( 𝑠 / 2 ) )
198 197 fveq2d ⊢ ( 𝑡 = 𝑠 → ( sin ‘ ( 𝑡 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
199 198 oveq2d ⊢ ( 𝑡 = 𝑠 → ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
200 199 fveq2d ⊢ ( 𝑡 = 𝑠 → ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) = ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
201 200 breq2d ⊢ ( 𝑡 = 𝑠 → ( 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ↔ 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
202 201 cbvralvw ⊢ ( ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ↔ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
203 nfv ⊢ Ⅎ 𝑠 𝜑
204 nfra1 ⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
205 203 204 nfan ⊢ Ⅎ 𝑠 ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
206 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
207 15 104 sseldi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
208 207 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
209 rspa ⊢ ( ( ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
210 206 208 209 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
211 210 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
212 205 211 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) → ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
213 202 212 sylan2b ⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
214 213 3adant2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
215 eqid ⊢ ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
216 80 90 130 131 137 138 141 142 145 156 172 175 191 193 195 196 214 215 dvdivbd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ+ ∧ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 )
217 216 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑐 ≤ ( abs ‘ ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
218 78 217 mpd ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 )
219 nfcv ⊢ Ⅎ 𝑠 ℝ
220 nfcv ⊢ Ⅎ 𝑠 D
221 nfmpt1 ⊢ Ⅎ 𝑠 ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
222 14 221 nfcxfr ⊢ Ⅎ 𝑠 𝑂
223 219 220 222 nfov ⊢ Ⅎ 𝑠 ( ℝ D 𝑂 )
224 223 nfdm ⊢ Ⅎ 𝑠 dom ( ℝ D 𝑂 )
225 nfcv ⊢ Ⅎ 𝑠 ( 𝐴 (,) 𝐵 )
226 224 225 raleqf ⊢ ( dom ( ℝ D 𝑂 ) = ( 𝐴 (,) 𝐵 ) → ( ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
227 22 226 syl ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
228 227 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
229 218 228 mpbird ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 )
230 14 a1i ⊢ ( 𝜑 → 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
231 230 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝑂 ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
232 231 fveq1d ⊢ ( 𝜑 → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) = ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) )
233 232 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) = ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) )
234 233 breq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
235 234 rexralbidv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ‘ 𝑠 ) ) ≤ 𝑏 ) )
236 229 235 mpbird ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 )
237 22 236 jca ⊢ ( 𝜑 → ( dom ( ℝ D 𝑂 ) = ( 𝐴 (,) 𝐵 ) ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 ) )