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

Proof

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