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 
|- ( ph -> A e. CC )
itgcoscmulx.b 
|- ( ph -> B e. RR )
itgcoscmulx.c 
|- ( ph -> C e. RR )
itgcoscmulx.blec 
|- ( ph -> B <_ C )
itgcoscmulx.an0 
|- ( ph -> A =/= 0 )
Assertion itgcoscmulx 
|- ( ph -> S. ( B (,) C ) ( cos ` ( A x. x ) ) _d x = ( ( ( sin ` ( A x. C ) ) - ( sin ` ( A x. B ) ) ) / A ) )

Proof

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