Metamath Proof Explorer

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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
295 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
296 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
297 1 2 296 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
298 257 265 273 293 16 294 295 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 𝑥 ) )