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		cncfcdm	⊢ ( ( ( ℂ ∖ { 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		cncfcdm	⊢ ( ( ( ℝ ∖ { 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ 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	sselid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
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 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 ) )