Metamath Proof Explorer

Theorem itgcoscmulx

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

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

Proof

Step Hyp Ref Expression
1 itgcoscmulx.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 itgcoscmulx.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 itgcoscmulx.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 itgcoscmulx.blec ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
5 itgcoscmulx.an0 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
6 2 3 iccssred ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
7 6 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ↾ ( 𝐵 [,] 𝐶 ) ) = ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) )
8 7 eqcomd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) = ( ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ↾ ( 𝐵 [,] 𝐶 ) ) )
9 8 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ↾ ( 𝐵 [,] 𝐶 ) ) ) )
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 10 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
12 11 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
15 13 14 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
16 15 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐴 ≠ 0 )
18 16 13 17 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ∈ ℂ )
19 12 18 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ∈ ℂ )
20 19 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) : ℝ ⟶ ℂ )
21 ssidd ⊢ ( 𝜑 → ℝ ⊆ ℝ )
22 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
23 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
24 22 23 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐵 [,] 𝐶 ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ↾ ( 𝐵 [,] 𝐶 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) ) )
25 11 20 21 6 24 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ↾ ( 𝐵 [,] 𝐶 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) ) )
26 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
27 26 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
28 12 16 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
29 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ )
30 29 12 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
31 30 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
32 29 31 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ )
33 11 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
34 33 eqcomd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) = ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) )
35 34 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) ) )
36 16 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) : ℂ ⟶ ℂ )
37 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
38 dvsinax ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
39 1 38 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
40 39 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
41 15 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
42 13 41 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ )
43 42 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℂ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ )
44 dmmptg ⊢ ( ∀ 𝑦 ∈ ℂ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ℂ → dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ℂ )
45 43 44 syl ⊢ ( 𝜑 → dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ℂ )
46 40 45 eqtr2d ⊢ ( 𝜑 → ℂ = dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
47 10 46 sseqtrid ⊢ ( 𝜑 → ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
48 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) ) ) → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) ↾ ℝ ) )
49 27 36 37 47 48 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) ↾ ℝ ) )
50 39 reseq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) ↾ ℝ ) = ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) ↾ ℝ ) )
51 11 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
52 49 50 51 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ↾ ℝ ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
53 35 52 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
54 27 28 32 53 1 5 dvmptdivc ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) )
55 iccntr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) = ( 𝐵 (,) 𝐶 ) )
56 2 3 55 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) = ( 𝐵 (,) 𝐶 ) )
57 54 56 reseq12d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) ↾ ( 𝐵 (,) 𝐶 ) ) )
58 ioossre ⊢ ( 𝐵 (,) 𝐶 ) ⊆ ℝ
59 resmpt ⊢ ( ( 𝐵 (,) 𝐶 ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) ↾ ( 𝐵 (,) 𝐶 ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) )
60 58 59 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) ↾ ( 𝐵 (,) 𝐶 ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) )
61 elioore ⊢ ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) → 𝑦 ∈ ℝ )
62 61 recnd ⊢ ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) → 𝑦 ∈ ℂ )
63 62 41 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
64 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝐴 ∈ ℂ )
65 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝐴 ≠ 0 )
66 63 64 65 divcan3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ) → ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) = ( cos ‘ ( 𝐴 · 𝑦 ) ) )
67 66 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) / 𝐴 ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) )
68 57 60 67 3eqtrd ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 [,] 𝐶 ) ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) )
69 9 25 68 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) = ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) )
71 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑥 ) )
72 71 fveq2d ⊢ ( 𝑦 = 𝑥 → ( cos ‘ ( 𝐴 · 𝑦 ) ) = ( cos ‘ ( 𝐴 · 𝑥 ) ) )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) ∧ 𝑦 = 𝑥 ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) = ( cos ‘ ( 𝐴 · 𝑥 ) ) )
74 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝐵 (,) 𝐶 ) )
75 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝐴 ∈ ℂ )
76 58 11 sstrid ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ℂ )
77 76 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ℂ )
78 75 77 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
79 78 coscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( cos ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
80 70 73 74 79 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) = ( cos ‘ ( 𝐴 · 𝑥 ) ) )
81 80 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → ( cos ‘ ( 𝐴 · 𝑥 ) ) = ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) )
82 81 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( cos ‘ ( 𝐴 · 𝑥 ) ) d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) d 𝑥 )
83 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) = ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) )
84 oveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐶 ) )
85 84 fveq2d ⊢ ( 𝑦 = 𝐶 → ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝐶 ) ) )
86 85 oveq1d ⊢ ( 𝑦 = 𝐶 → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐶 ) → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
88 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
89 3 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
90 ubicc2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ( 𝐵 [,] 𝐶 ) )
91 88 89 4 90 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 [,] 𝐶 ) )
92 3 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
93 1 92 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
94 93 sincld ⊢ ( 𝜑 → ( sin ‘ ( 𝐴 · 𝐶 ) ) ∈ ℂ )
95 94 1 5 divcld ⊢ ( 𝜑 → ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) ∈ ℂ )
96 83 87 91 95 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) = ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) )
97 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐵 ) )
98 97 fveq2d ⊢ ( 𝑦 = 𝐵 → ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝐵 ) ) )
99 98 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
100 99 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) = ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
101 lbicc2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
102 88 89 4 101 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
103 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
104 1 103 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
105 104 sincld ⊢ ( 𝜑 → ( sin ‘ ( 𝐴 · 𝐵 ) ) ∈ ℂ )
106 105 1 5 divcld ⊢ ( 𝜑 → ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ∈ ℂ )
107 83 100 102 106 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) = ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) )
108 96 107 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) = ( ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
109 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
110 109 a1i ⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) )
111 76 1 37 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
112 76 37 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝑦 ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
113 111 112 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( 𝐴 · 𝑦 ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
114 110 113 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
115 69 114 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ∈ ( ( 𝐵 (,) 𝐶 ) –cn→ ℂ ) )
116 ioossicc ⊢ ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐵 [,] 𝐶 )
117 116 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐵 [,] 𝐶 ) )
118 ioombl ⊢ ( 𝐵 (,) 𝐶 ) ∈ dom vol
119 118 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ∈ dom vol )
120 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐴 ∈ ℂ )
121 6 10 sstrdi ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℂ )
122 121 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑦 ∈ ℂ )
123 120 122 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
124 123 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ) → ( cos ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
125 121 1 37 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
126 121 37 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝑦 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
127 125 126 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( 𝐴 · 𝑦 ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
128 110 127 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
129 cniccibl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) ) → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
130 2 3 128 129 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
131 117 119 124 130 iblss ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 (,) 𝐶 ) ↦ ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ∈ 𝐿1 )
132 69 131 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ∈ 𝐿1 )
133 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
134 133 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
135 134 127 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
136 neneq ⊢ ( 𝐴 ≠ 0 → ¬ 𝐴 = 0 )
137 elsni ⊢ ( 𝐴 ∈ { 0 } → 𝐴 = 0 )
138 137 con3i ⊢ ( ¬ 𝐴 = 0 → ¬ 𝐴 ∈ { 0 } )
139 5 136 138 3syl ⊢ ( 𝜑 → ¬ 𝐴 ∈ { 0 } )
140 1 139 eldifd ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
141 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
142 121 140 141 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐴 ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ( ℂ ∖ { 0 } ) ) )
143 135 142 divcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ∈ ( ( 𝐵 [,] 𝐶 ) –cn→ ℂ ) )
144 2 3 4 115 132 143 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐶 ) − ( ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ‘ 𝐵 ) ) )
145 94 105 1 5 divsubdird ⊢ ( 𝜑 → ( ( ( sin ‘ ( 𝐴 · 𝐶 ) ) − ( sin ‘ ( 𝐴 · 𝐵 ) ) ) / 𝐴 ) = ( ( ( sin ‘ ( 𝐴 · 𝐶 ) ) / 𝐴 ) − ( ( sin ‘ ( 𝐴 · 𝐵 ) ) / 𝐴 ) ) )
146 108 144 145 3eqtr4d ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( ( ℝ D ( 𝑦 ∈ ( 𝐵 [,] 𝐶 ) ↦ ( ( sin ‘ ( 𝐴 · 𝑦 ) ) / 𝐴 ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( sin ‘ ( 𝐴 · 𝐶 ) ) − ( sin ‘ ( 𝐴 · 𝐵 ) ) ) / 𝐴 ) )
147 82 146 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) ( cos ‘ ( 𝐴 · 𝑥 ) ) d 𝑥 = ( ( ( sin ‘ ( 𝐴 · 𝐶 ) ) − ( sin ‘ ( 𝐴 · 𝐵 ) ) ) / 𝐴 ) )