Theorem fourierdlem39

Description: Integration by parts of S. ( A (,) B ) ( ( Fx ) x. ( sin( R x. x ) ) ) _d x (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem39.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem39.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem39.aleb	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	fourierdlem39.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
	fourierdlem39.g	⊢ 𝐺 = ( ℝ D 𝐹 )
	fourierdlem39.gcn	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
	fourierdlem39.gbd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 )
	fourierdlem39.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
Assertion	fourierdlem39	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) d 𝑥 = ( ( ( ( 𝐹 ‘ 𝐵 ) · - ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) ) − ( ( 𝐹 ‘ 𝐴 ) · - ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) ) ) − ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem39.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem39.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem39.aleb	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4		fourierdlem39.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
5		fourierdlem39.g	⊢ 𝐺 = ( ℝ D 𝐹 )
6		fourierdlem39.gcn	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
7		fourierdlem39.gbd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 )
8		fourierdlem39.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
9		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
10	4 9	syl	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
11	10	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
12	11	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
13	12 4	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
14		coscn	⊢ cos ∈ ( ℂ –cn→ ℂ )
15	14	a1i	⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) )
16	1 2	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
17		ax-resscn	⊢ ℝ ⊆ ℂ
18	16 17	sstrdi	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
19	8	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
20	19	recnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
21		ssid	⊢ ℂ ⊆ ℂ
22	21	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
23	18 20 22	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑅 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
24	18 22	idcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
25	23 24	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑅 · 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
26	15 25	cncfmpt1f	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( cos ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
27	8	rpcnne0d	⊢ ( 𝜑 → ( 𝑅 ∈ ℂ ∧ 𝑅 ≠ 0 ) )
28		eldifsn	⊢ ( 𝑅 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑅 ∈ ℂ ∧ 𝑅 ≠ 0 ) )
29	27 28	sylibr	⊢ ( 𝜑 → 𝑅 ∈ ( ℂ ∖ { 0 } ) )
30		difssd	⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
31	18 29 30	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑅 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
32	26 31	divcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
33	32	negcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
34		cncff	⊢ ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
35	6 34	syl	⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
36	35	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
37	36	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) = 𝐺 )
38	37 6	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
39		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
40	39	a1i	⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
41		ioosscn	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
42	41	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
43	42 20 22	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑅 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
44	42 22	idcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
45	43 44	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑅 · 𝑥 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
46	40 45	cncfmpt1f	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
47		ioombl	⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
48	47	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
49		volioo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
50	1 2 3 49	syl3anc	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
51	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
52	50 51	eqeltrd	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
53		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) )
54		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
55	54	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
56	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
57	55	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
58	56 57	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
59	53 13 55 22 58	cncfmptssg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
60	59 46	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
61		cniccbdd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
62	1 2 4 61	syl3anc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
63		nfra1	⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦
64	54	sseli	⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
65		rspa	⊢ ( ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
66	64 65	sylan2	⊢ ( ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
67	66	ex	⊢ ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) )
68	63 67	ralrimi	⊢ ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
69	68	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) )
70	69	reximdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) )
71	62 70	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
72		nfv	⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑦 ∈ ℝ )
73		nfra1	⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦
74	72 73	nfan	⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
75		simpll	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → ( 𝜑 ∧ 𝑦 ∈ ℝ ) )
76		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) )
77	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℝ )
78		elioore	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
79	78	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
80	77 79	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 · 𝑥 ) ∈ ℝ )
81	80	resincld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑅 · 𝑥 ) ) ∈ ℝ )
82	81	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑅 · 𝑥 ) ) ∈ ℂ )
83	58 82	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ℂ )
84	83	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ℂ )
85		dmmptg	⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ℂ → dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) = ( 𝐴 (,) 𝐵 ) )
86	84 85	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) = ( 𝐴 (,) 𝐵 ) )
87	86	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) = ( 𝐴 (,) 𝐵 ) )
88	76 87	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
89	88	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
90		simplr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
91	88	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
92		rspa	⊢ ( ( ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
93	90 91 92	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
94	93	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
95		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) )
96		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
97		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝑧 ) )
98	97	fveq2d	⊢ ( 𝑥 = 𝑧 → ( sin ‘ ( 𝑅 · 𝑥 ) ) = ( sin ‘ ( 𝑅 · 𝑧 ) ) )
99	96 98	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) )
100	99	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) )
101		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
102	10	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
103	54 101	sselid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
104	102 103	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
105	20	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℂ )
106	41 101	sselid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ℂ )
107	105 106	mulcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 · 𝑧 ) ∈ ℂ )
108	107	sincld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑅 · 𝑧 ) ) ∈ ℂ )
109	104 108	mulcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ∈ ℂ )
110	95 100 101 109	fvmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) )
111	110	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) )
112	104 108	absmuld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) )
113	111 112	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) )
114	113	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) )
115	114	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) )
116		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝜑 )
117		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
118	116 117 104	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
119	118	abscld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
120	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝑅 ∈ ℂ )
121	41 117	sselid	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝑧 ∈ ℂ )
122	120 121	mulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( 𝑅 · 𝑧 ) ∈ ℂ )
123	122	sincld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( sin ‘ ( 𝑅 · 𝑧 ) ) ∈ ℂ )
124	123	abscld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ∈ ℝ )
125	119 124	remulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) ∈ ℝ )
126		1red	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 1 ∈ ℝ )
127	119 126	remulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · 1 ) ∈ ℝ )
128		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
129	128 126	remulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( 𝑦 · 1 ) ∈ ℝ )
130	108	abscld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ∈ ℝ )
131		1red	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
132	104	abscld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
133	104	absge0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
134	19	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℝ )
135		elioore	⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → 𝑧 ∈ ℝ )
136	135	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ℝ )
137	134 136	remulcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 · 𝑧 ) ∈ ℝ )
138		abssinbd	⊢ ( ( 𝑅 · 𝑧 ) ∈ ℝ → ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ≤ 1 )
139	137 138	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ≤ 1 )
140	130 131 132 133 139	lemul2ad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · 1 ) )
141	140	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · 1 ) )
142	141	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · 1 ) )
143		0le1	⊢ 0 ≤ 1
144	143	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 0 ≤ 1 )
145		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 )
146	119 128 126 144 145	lemul1ad	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · 1 ) ≤ ( 𝑦 · 1 ) )
147	125 127 129 142 146	letrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( sin ‘ ( 𝑅 · 𝑧 ) ) ) ) ≤ ( 𝑦 · 1 ) )
148	115 147	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 · 1 ) )
149	128	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → 𝑦 ∈ ℂ )
150	149	mulridd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( 𝑦 · 1 ) = 𝑦 )
151	148 150	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 )
152	75 89 94 151	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 )
153	152	ex	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ( 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
154	74 153	ralrimi	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ) → ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 )
155	154	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
156	155	reximdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
157	71 156	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ‘ 𝑧 ) ) ≤ 𝑦 )
158	48 52 60 157	cnbdibl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) ) ∈ 𝐿1 )
159	15 45	cncfmpt1f	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑅 · 𝑥 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
160	42 29 30	constcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑅 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
161	159 160	divcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
162	161	negcncfg	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
163	38 162	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
164		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
165	19	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑅 ∈ ℝ )
166	8	rpne0d	⊢ ( 𝜑 → 𝑅 ≠ 0 )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑅 ≠ 0 )
168	164 165 167	redivcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 / 𝑅 ) ∈ ℝ )
169	168	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) → ( 𝑦 / 𝑅 ) ∈ ℝ )
170		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) )
171	35	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
172	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℂ )
173	78	recnd	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℂ )
174	173	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℂ )
175	172 174	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 · 𝑥 ) ∈ ℂ )
176	175	coscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑅 · 𝑥 ) ) ∈ ℂ )
177	166	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ≠ 0 )
178	176 172 177	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ∈ ℂ )
179	178	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ∈ ℂ )
180	171 179	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ℂ )
181	180	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ℂ )
182	181	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ℂ )
183		dmmptg	⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ∈ ℂ → dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝐴 (,) 𝐵 ) )
184	182 183	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝐴 (,) 𝐵 ) )
185	170 184	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
186	185	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
187		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) )
188		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) )
189	97	fveq2d	⊢ ( 𝑥 = 𝑧 → ( cos ‘ ( 𝑅 · 𝑥 ) ) = ( cos ‘ ( 𝑅 · 𝑧 ) ) )
190	189	oveq1d	⊢ ( 𝑥 = 𝑧 → ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) )
191	190	negeqd	⊢ ( 𝑥 = 𝑧 → - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) )
192	188 191	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) )
193	192	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) )
194	35	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
195	107	coscld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑅 · 𝑧 ) ) ∈ ℂ )
196	166	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ≠ 0 )
197	195 105 196	divcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ∈ ℂ )
198	197	negcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ∈ ℂ )
199	194 198	mulcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ∈ ℂ )
200	187 193 101 199	fvmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) )
201	200	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) )
202	201	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) )
203	35	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
204	203	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
205	204	abscld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
206		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ )
207	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℂ )
208	106	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ℂ )
209	207 208	mulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 · 𝑧 ) ∈ ℂ )
210	209	coscld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑅 · 𝑧 ) ) ∈ ℂ )
211	166	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ≠ 0 )
212	210 207 211	divcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ∈ ℂ )
213	212	negcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ∈ ℂ )
214	213	abscld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ∈ ℝ )
215	8	rprecred	⊢ ( 𝜑 → ( 1 / 𝑅 ) ∈ ℝ )
216	215	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑅 ) ∈ ℝ )
217	204	absge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
218	213	absge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) )
219	188	fveq2d	⊢ ( 𝑥 = 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
220	219	breq1d	⊢ ( 𝑥 = 𝑧 → ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) )
221	220	rspccva	⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 )
222	221	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 )
223	197	absnegd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) = ( abs ‘ ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) )
224	195 105 196	absdivd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) = ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / ( abs ‘ 𝑅 ) ) )
225	8	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝑅 )
226	19 225	absidd	⊢ ( 𝜑 → ( abs ‘ 𝑅 ) = 𝑅 )
227	226	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / ( abs ‘ 𝑅 ) ) = ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / 𝑅 ) )
228	227	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / ( abs ‘ 𝑅 ) ) = ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / 𝑅 ) )
229	223 224 228	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) = ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / 𝑅 ) )
230	195	abscld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) ∈ ℝ )
231	8	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℝ+ )
232		abscosbd	⊢ ( ( 𝑅 · 𝑧 ) ∈ ℝ → ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) ≤ 1 )
233	137 232	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) ≤ 1 )
234	230 131 231 233	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( cos ‘ ( 𝑅 · 𝑧 ) ) ) / 𝑅 ) ≤ ( 1 / 𝑅 ) )
235	229 234	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ≤ ( 1 / 𝑅 ) )
236	235	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ≤ ( 1 / 𝑅 ) )
237	205 206 214 216 217 218 222 236	lemul12ad	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) · ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) ≤ ( 𝑦 · ( 1 / 𝑅 ) ) )
238	194 198	absmuld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) = ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) · ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) )
239	238	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) = ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) · ( abs ‘ - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) )
240	206	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℂ )
241	240 207 211	divrecd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 / 𝑅 ) = ( 𝑦 · ( 1 / 𝑅 ) ) )
242	237 239 241	3brtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) · - ( ( cos ‘ ( 𝑅 · 𝑧 ) ) / 𝑅 ) ) ) ≤ ( 𝑦 / 𝑅 ) )
243	202 242	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) )
244	186 243	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) )
245	244	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) → ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) )
246		breq2	⊢ ( 𝑤 = ( 𝑦 / 𝑅 ) → ( ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ 𝑤 ↔ ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) ) )
247	246	ralbidv	⊢ ( 𝑤 = ( 𝑦 / 𝑅 ) → ( ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ 𝑤 ↔ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) ) )
248	247	rspcev	⊢ ( ( ( 𝑦 / 𝑅 ) ∈ ℝ ∧ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ ( 𝑦 / 𝑅 ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ 𝑤 )
249	169 245 248	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ 𝑤 )
250	249 7	r19.29a	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ( abs ‘ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ‘ 𝑧 ) ) ≤ 𝑤 )
251	48 52 163 250	cnbdibl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) ∈ 𝐿1 )
252	12	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ℝ D 𝐹 ) )
253	5	eqcomi	⊢ ( ℝ D 𝐹 ) = 𝐺
254	253	a1i	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )
255	252 254 36	3eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
256		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
257	256	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
258	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑅 ∈ ℂ )
259		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
260	259	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
261	258 260	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑅 · 𝑥 ) ∈ ℂ )
262	261	coscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( cos ‘ ( 𝑅 · 𝑥 ) ) ∈ ℂ )
263	166	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑅 ≠ 0 )
264	262 258 263	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ∈ ℂ )
265	264	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ∈ ℂ )
266	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑅 ∈ ℝ )
267		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
268	266 267	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑅 · 𝑥 ) ∈ ℝ )
269	268	resincld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( 𝑅 · 𝑥 ) ) ∈ ℝ )
270	269	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → - ( sin ‘ ( 𝑅 · 𝑥 ) ) ∈ ℝ )
271	270 266	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) ∈ ℝ )
272	271 266 263	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ∈ ℝ )
273	272	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ∈ ℝ )
274		recoscl	⊢ ( 𝑦 ∈ ℝ → ( cos ‘ 𝑦 ) ∈ ℝ )
275	274	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( cos ‘ 𝑦 ) ∈ ℝ )
276	275	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( cos ‘ 𝑦 ) ∈ ℂ )
277		resincl	⊢ ( 𝑦 ∈ ℝ → ( sin ‘ 𝑦 ) ∈ ℝ )
278	277	renegcld	⊢ ( 𝑦 ∈ ℝ → - ( sin ‘ 𝑦 ) ∈ ℝ )
279	278	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - ( sin ‘ 𝑦 ) ∈ ℝ )
280		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
281	257	dvmptid	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
282	257 260 280 281 20	dvmptcmul	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 𝑅 · 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑅 · 1 ) ) )
283	258	mulridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑅 · 1 ) = 𝑅 )
284	283	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝑅 · 1 ) ) = ( 𝑥 ∈ ℝ ↦ 𝑅 ) )
285	282 284	eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 𝑅 · 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ 𝑅 ) )
286		dvcosre	⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( cos ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ - ( sin ‘ 𝑦 ) )
287	286	a1i	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( cos ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ - ( sin ‘ 𝑦 ) ) )
288		fveq2	⊢ ( 𝑦 = ( 𝑅 · 𝑥 ) → ( cos ‘ 𝑦 ) = ( cos ‘ ( 𝑅 · 𝑥 ) ) )
289		fveq2	⊢ ( 𝑦 = ( 𝑅 · 𝑥 ) → ( sin ‘ 𝑦 ) = ( sin ‘ ( 𝑅 · 𝑥 ) ) )
290	289	negeqd	⊢ ( 𝑦 = ( 𝑅 · 𝑥 ) → - ( sin ‘ 𝑦 ) = - ( sin ‘ ( 𝑅 · 𝑥 ) ) )
291	257 257 268 266 276 279 285 287 288 290	dvmptco	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑅 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) ) )
292	257 262 271 291 20 166	dvmptdivc	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ) )
293	257 264 272 292	dvmptneg	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ) )
294		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
295	294	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
296		iccntr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
297	1 2 296	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
298	257 265 273 293 16 295 294 297	dvmptres2	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ) )
299	82 172	mulneg1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) = - ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) )
300	299	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = ( - ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) )
301	82 172	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) ∈ ℂ )
302	301 172 177	divnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = ( - ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) )
303	300 302	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = - ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) )
304	303	negeqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = - - ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) )
305	301 172 177	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ∈ ℂ )
306	305	negnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - - ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) )
307	82 172 177	divcan4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = ( sin ‘ ( 𝑅 · 𝑥 ) ) )
308	304 306 307	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) = ( sin ‘ ( 𝑅 · 𝑥 ) ) )
309	308	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( - ( sin ‘ ( 𝑅 · 𝑥 ) ) · 𝑅 ) / 𝑅 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( sin ‘ ( 𝑅 · 𝑥 ) ) ) )
310	298 309	eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( sin ‘ ( 𝑅 · 𝑥 ) ) ) )
311		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
312		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝐴 ) )
313	312	fveq2d	⊢ ( 𝑥 = 𝐴 → ( cos ‘ ( 𝑅 · 𝑥 ) ) = ( cos ‘ ( 𝑅 · 𝐴 ) ) )
314	313	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) )
315	314	negeqd	⊢ ( 𝑥 = 𝐴 → - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = - ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) )
316	311 315	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐹 ‘ 𝐴 ) · - ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) ) )
317	316	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐹 ‘ 𝐴 ) · - ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) ) )
318		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
319		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝐵 ) )
320	319	fveq2d	⊢ ( 𝑥 = 𝐵 → ( cos ‘ ( 𝑅 · 𝑥 ) ) = ( cos ‘ ( 𝑅 · 𝐵 ) ) )
321	320	oveq1d	⊢ ( 𝑥 = 𝐵 → ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) )
322	321	negeqd	⊢ ( 𝑥 = 𝐵 → - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) = - ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) )
323	318 322	oveq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐹 ‘ 𝐵 ) · - ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) ) )
324	323	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) = ( ( 𝐹 ‘ 𝐵 ) · - ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) ) )
325	1 2 3 13 33 38 46 158 251 255 310 317 324	itgparts	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑅 · 𝑥 ) ) ) d 𝑥 = ( ( ( ( 𝐹 ‘ 𝐵 ) · - ( ( cos ‘ ( 𝑅 · 𝐵 ) ) / 𝑅 ) ) − ( ( 𝐹 ‘ 𝐴 ) · - ( ( cos ‘ ( 𝑅 · 𝐴 ) ) / 𝑅 ) ) ) − ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐺 ‘ 𝑥 ) · - ( ( cos ‘ ( 𝑅 · 𝑥 ) ) / 𝑅 ) ) d 𝑥 ) )