# 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 ${⊢}{\phi }\to {A}\in ℂ$
itgcoscmulx.b ${⊢}{\phi }\to {B}\in ℝ$
itgcoscmulx.c ${⊢}{\phi }\to {C}\in ℝ$
itgcoscmulx.blec ${⊢}{\phi }\to {B}\le {C}$
itgcoscmulx.an0 ${⊢}{\phi }\to {A}\ne 0$
Assertion itgcoscmulx ${⊢}{\phi }\to {\int }_{\left({B},{C}\right)}\mathrm{cos}{A}{x}d{x}=\frac{\mathrm{sin}{A}{C}-\mathrm{sin}{A}{B}}{{A}}$

### Proof

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