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 ffvelrnd ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 sseldi ( ( 𝜑𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
104 102 103 ffvelrnd ( ( 𝜑𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹𝑧 ) ∈ ℂ )
105 20 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑅 ∈ ℂ )
106 41 101 sseldi ( ( 𝜑𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 ∈ ℂ )
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 sseldi ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 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 mulid1d ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 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 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺𝑥 ) ∈ ℂ )
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 ffvelrnda ( ( 𝜑𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺𝑧 ) ∈ ℂ )
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 ffvelrnda ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( 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 mulid1d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑅 · 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 𝑥 ) )