Metamath Proof Explorer

Theorem itgsincmulx

Description: Exercise: the integral of x |-> sin a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsincmulx.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
itgsincmulx.an0 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
itgsincmulx.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
itgsincmulx.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
itgsincmulx.blec ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
Assertion itgsincmulx ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( sin ‘ ( 𝐴 · 𝑥 ) ) d 𝑥 = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 itgsincmulx.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 itgsincmulx.an0 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 itgsincmulx.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 itgsincmulx.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 itgsincmulx.blec ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
6 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) = ( 𝑦 ∈ ℂ ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
9 7 8 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
10 9 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
11 10 negcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐴 ≠ 0 )
13 11 7 12 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ∈ ℂ )
14 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
15 14 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
16 9 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
17 16 negcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
18 7 17 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ )
19 18 negcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ )
20 dvcosax ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
21 1 20 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
22 15 10 18 21 dvmptneg ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ - ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
23 15 11 19 22 1 2 dvmptdivc ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) )
24 18 7 12 divnegd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - ( ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = ( - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) )
25 24 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = - ( ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) )
26 17 7 12 divcan3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
27 26 negeqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - ( ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = - - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
28 16 negnegd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → - - ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝑦 ) ) )
29 25 27 28 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = ( sin ‘ ( 𝐴 · 𝑦 ) ) )
30 29 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( - ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) = ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
31 23 30 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
32 6 13 31 16 3 4 dvmptresicc ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
33 32 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑥 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑥 ) )
35 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
36 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑥 ) )
37 36 fveq2d ⊢ ( 𝑦 = 𝑥 → ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝑥 ) ) )
38 37 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) ∧ 𝑦 = 𝑥 ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝑥 ) ) )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝐵 (,) 𝐶 ) )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝐴 ∈ ℂ )
41 ioosscn ⊢ ( 𝐵 (,) 𝐶 ) ⊆ ℂ
42 41 39 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ℂ )
43 40 42 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
44 43 sincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( sin ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
45 35 38 39 44 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑥 ) = ( sin ‘ ( 𝐴 · 𝑥 ) ) )
46 34 45 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( sin ‘ ( 𝐴 · 𝑥 ) ) = ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) )
47 46 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( sin ‘ ( 𝐴 · 𝑥 ) ) d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) d 𝑥 )
48 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
49 48 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
50 41 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ℂ )
51 ssid ⊢ ℂ ⊆ ℂ
52 51 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
53 50 1 52 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
54 50 52 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝑦 ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
55 53 54 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( 𝐴 · 𝑦 ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
56 49 55 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
57 32 56 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
58 ioossicc ⊢ ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐵 [,] 𝐶 )
59 58 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐵 [,] 𝐶 ) )
60 ioombl ⊢ ( 𝐵 (,) 𝐶 ) ∈ dom vol
61 60 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ∈ dom vol )
62 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐴 ∈ ℂ )
63 3 4 iccssred ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
64 ax-resscn ⊢ ℝ ⊆ ℂ
65 63 64 sstrdi ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℂ )
66 65 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑦 ∈ ℂ )
67 62 66 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
68 67 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
69 65 1 52 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
70 65 52 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝑦 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
71 69 70 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( 𝐴 · 𝑦 ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
72 49 71 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
73 cniccibl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) ) → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
74 3 4 72 73 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
75 59 61 68 74 iblss ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
76 32 75 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ∈ 𝐿1 )
77 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
78 77 a1i ⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) )
79 78 71 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
80 79 negcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ - ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
81 2 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = 0 )
82 elsng ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 ) )
83 1 82 syl ⊢ ( 𝜑 → ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 ) )
84 81 83 mtbird ⊢ ( 𝜑 → ¬ 𝐴 ∈ { 0 } )
85 1 84 eldifd ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
86 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
87 65 85 86 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ( ℂ ∖ { 0 } ) ) )
88 80 87 divcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
89 3 4 5 57 76 88 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) )
90 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) = ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) )
91 oveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐶 ) )
92 91 fveq2d ⊢ ( 𝑦 = 𝐶 → ( cos ‘ ( 𝐴 · 𝑦 ) ) = ( cos ‘ ( 𝐴 · 𝐶 ) ) )
93 92 negeqd ⊢ ( 𝑦 = 𝐶 → - ( cos ‘ ( 𝐴 · 𝑦 ) ) = - ( cos ‘ ( 𝐴 · 𝐶 ) ) )
94 93 oveq1d ⊢ ( 𝑦 = 𝐶 → ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
95 94 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐶 ) → ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
96 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
97 4 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
98 ubicc2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ( 𝐵 [,] 𝐶 ) )
99 96 97 5 98 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 [,] 𝐶 ) )
100 ovexd ⊢ ( 𝜑 → ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ∈ V )
101 90 95 99 100 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) = ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
102 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐵 ) )
103 102 fveq2d ⊢ ( 𝑦 = 𝐵 → ( cos ‘ ( 𝐴 · 𝑦 ) ) = ( cos ‘ ( 𝐴 · 𝐵 ) ) )
104 103 negeqd ⊢ ( 𝑦 = 𝐵 → - ( cos ‘ ( 𝐴 · 𝑦 ) ) = - ( cos ‘ ( 𝐴 · 𝐵 ) ) )
105 104 oveq1d ⊢ ( 𝑦 = 𝐵 → ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
107 lbicc2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
108 96 97 5 107 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
109 ovexd ⊢ ( 𝜑 → ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ∈ V )
110 90 106 108 109 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) = ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
111 101 110 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) = ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
112 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
113 1 112 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
114 113 coscld ⊢ ( 𝜑 → ( cos ‘ ( 𝐴 · 𝐵 ) ) ∈ ℂ )
115 114 1 2 divnegd ⊢ ( 𝜑 → - ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
116 115 eqcomd ⊢ ( 𝜑 → ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) = - ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
117 116 oveq2d ⊢ ( 𝜑 → ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − ( - ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) = ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − - ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
118 4 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
119 1 118 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
120 119 coscld ⊢ ( 𝜑 → ( cos ‘ ( 𝐴 · 𝐶 ) ) ∈ ℂ )
121 120 negcld ⊢ ( 𝜑 → - ( cos ‘ ( 𝐴 · 𝐶 ) ) ∈ ℂ )
122 121 1 2 divcld ⊢ ( 𝜑 → ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ∈ ℂ )
123 114 1 2 divcld ⊢ ( 𝜑 → ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ∈ ℂ )
124 122 123 subnegd ⊢ ( 𝜑 → ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − - ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) = ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) + ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
125 111 117 124 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) = ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) + ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
126 122 123 addcomd ⊢ ( 𝜑 → ( ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) + ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) + ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) )
127 120 1 2 divnegd ⊢ ( 𝜑 → - ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) = ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
128 127 eqcomd ⊢ ( 𝜑 → ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) = - ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
129 128 oveq2d ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) + ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) + - ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) )
130 120 1 2 divcld ⊢ ( 𝜑 → ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ∈ ℂ )
131 123 130 negsubd ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) + - ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) − ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) )
132 114 120 1 2 divsubdird ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) − ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) )
133 132 eqcomd ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) − ( ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) )
134 129 131 133 3eqtrd ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) + ( - ( cos ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) )
135 125 126 134 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( - ( cos ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) )
136 47 89 135 3eqtrd ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( sin ‘ ( 𝐴 · 𝑥 ) ) d 𝑥 = ( ( ( cos ‘ ( 𝐴 · 𝐵 ) ) − ( cos ‘ ( 𝐴 · 𝐶 ) ) ) / 𝐴 ) )