Metamath Proof Explorer

Theorem itg2mulc

Description: The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itg2mulc.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2mulc.3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2mulc.4 
|- ( ph -> A e. ( 0 [,) +oo ) )
Assertion itg2mulc 
|- ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) )

Proof

Step Hyp Ref Expression
1 itg2mulc.2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
2 itg2mulc.3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
3 itg2mulc.4 
 |-  ( ph -> A e. ( 0 [,) +oo ) )
4 1 adantr 
 |-  ( ( ph /\ 0 < A ) -> F : RR --> ( 0 [,) +oo ) )
5 2 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` F ) e. RR )
6 elrege0 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
7 3 6 sylib 
 |-  ( ph -> ( A e. RR /\ 0 <_ A ) )
8 7 simpld 
 |-  ( ph -> A e. RR )
9 8 anim1i 
 |-  ( ( ph /\ 0 < A ) -> ( A e. RR /\ 0 < A ) )
10 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
11 9 10 sylibr 
 |-  ( ( ph /\ 0 < A ) -> A e. RR+ )
12 4 5 11 itg2mulclem 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) )
13 ge0mulcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )
14 13 adantl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )
15 fconst6g 
 |-  ( A e. ( 0 [,) +oo ) -> ( RR X. { A } ) : RR --> ( 0 [,) +oo ) )
16 3 15 syl 
 |-  ( ph -> ( RR X. { A } ) : RR --> ( 0 [,) +oo ) )
17 reex 
 |-  RR e. _V
18 17 a1i 
 |-  ( ph -> RR e. _V )
19 inidm 
 |-  ( RR i^i RR ) = RR
20 14 16 1 18 18 19 off 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,) +oo ) )
21 20 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,) +oo ) )
22 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
23 fss 
 |-  ( ( ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) )
24 20 22 23 sylancl 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) )
25 24 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) )
26 8 2 remulcld 
 |-  ( ph -> ( A x. ( S.2 ` F ) ) e. RR )
27 26 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( A x. ( S.2 ` F ) ) e. RR )
28 itg2lecl 
 |-  ( ( ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) /\ ( A x. ( S.2 ` F ) ) e. RR /\ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. RR )
29 25 27 12 28 syl3anc 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. RR )
30 11 rpreccld 
 |-  ( ( ph /\ 0 < A ) -> ( 1 / A ) e. RR+ )
31 21 29 30 itg2mulclem 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` ( ( RR X. { ( 1 / A ) } ) oF x. ( ( RR X. { A } ) oF x. F ) ) ) <_ ( ( 1 / A ) x. ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) ) )
32 4 feqmptd 
 |-  ( ( ph /\ 0 < A ) -> F = ( y e. RR |-> ( F ` y ) ) )
33 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
34 ax-resscn 
 |-  RR C_ CC
35 33 34 sstri 
 |-  ( 0 [,) +oo ) C_ CC
36 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> F : RR --> CC )
37 1 35 36 sylancl 
 |-  ( ph -> F : RR --> CC )
38 37 adantr 
 |-  ( ( ph /\ 0 < A ) -> F : RR --> CC )
39 38 ffvelrnda 
 |-  ( ( ( ph /\ 0 < A ) /\ y e. RR ) -> ( F ` y ) e. CC )
40 39 mulid2d 
 |-  ( ( ( ph /\ 0 < A ) /\ y e. RR ) -> ( 1 x. ( F ` y ) ) = ( F ` y ) )
41 40 mpteq2dva 
 |-  ( ( ph /\ 0 < A ) -> ( y e. RR |-> ( 1 x. ( F ` y ) ) ) = ( y e. RR |-> ( F ` y ) ) )
42 32 41 eqtr4d 
 |-  ( ( ph /\ 0 < A ) -> F = ( y e. RR |-> ( 1 x. ( F ` y ) ) ) )
43 17 a1i 
 |-  ( ( ph /\ 0 < A ) -> RR e. _V )
44 1red 
 |-  ( ( ( ph /\ 0 < A ) /\ y e. RR ) -> 1 e. RR )
45 43 30 11 ofc12 
 |-  ( ( ph /\ 0 < A ) -> ( ( RR X. { ( 1 / A ) } ) oF x. ( RR X. { A } ) ) = ( RR X. { ( ( 1 / A ) x. A ) } ) )
46 fconstmpt 
 |-  ( RR X. { ( ( 1 / A ) x. A ) } ) = ( y e. RR |-> ( ( 1 / A ) x. A ) )
47 45 46 eqtrdi 
 |-  ( ( ph /\ 0 < A ) -> ( ( RR X. { ( 1 / A ) } ) oF x. ( RR X. { A } ) ) = ( y e. RR |-> ( ( 1 / A ) x. A ) ) )
48 8 recnd 
 |-  ( ph -> A e. CC )
49 48 adantr 
 |-  ( ( ph /\ 0 < A ) -> A e. CC )
50 11 rpne0d 
 |-  ( ( ph /\ 0 < A ) -> A =/= 0 )
51 49 50 recid2d 
 |-  ( ( ph /\ 0 < A ) -> ( ( 1 / A ) x. A ) = 1 )
52 51 mpteq2dv 
 |-  ( ( ph /\ 0 < A ) -> ( y e. RR |-> ( ( 1 / A ) x. A ) ) = ( y e. RR |-> 1 ) )
53 47 52 eqtrd 
 |-  ( ( ph /\ 0 < A ) -> ( ( RR X. { ( 1 / A ) } ) oF x. ( RR X. { A } ) ) = ( y e. RR |-> 1 ) )
54 43 44 39 53 32 offval2 
 |-  ( ( ph /\ 0 < A ) -> ( ( ( RR X. { ( 1 / A ) } ) oF x. ( RR X. { A } ) ) oF x. F ) = ( y e. RR |-> ( 1 x. ( F ` y ) ) ) )
55 30 rpcnd 
 |-  ( ( ph /\ 0 < A ) -> ( 1 / A ) e. CC )
56 fconst6g 
 |-  ( ( 1 / A ) e. CC -> ( RR X. { ( 1 / A ) } ) : RR --> CC )
57 55 56 syl 
 |-  ( ( ph /\ 0 < A ) -> ( RR X. { ( 1 / A ) } ) : RR --> CC )
58 fconst6g 
 |-  ( A e. CC -> ( RR X. { A } ) : RR --> CC )
59 49 58 syl 
 |-  ( ( ph /\ 0 < A ) -> ( RR X. { A } ) : RR --> CC )
60 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
61 60 adantl 
 |-  ( ( ( ph /\ 0 < A ) /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
62 43 57 59 38 61 caofass 
 |-  ( ( ph /\ 0 < A ) -> ( ( ( RR X. { ( 1 / A ) } ) oF x. ( RR X. { A } ) ) oF x. F ) = ( ( RR X. { ( 1 / A ) } ) oF x. ( ( RR X. { A } ) oF x. F ) ) )
63 42 54 62 3eqtr2d 
 |-  ( ( ph /\ 0 < A ) -> F = ( ( RR X. { ( 1 / A ) } ) oF x. ( ( RR X. { A } ) oF x. F ) ) )
64 63 fveq2d 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` F ) = ( S.2 ` ( ( RR X. { ( 1 / A ) } ) oF x. ( ( RR X. { A } ) oF x. F ) ) ) )
65 29 recnd 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. CC )
66 65 49 50 divrec2d 
 |-  ( ( ph /\ 0 < A ) -> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) / A ) = ( ( 1 / A ) x. ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) ) )
67 31 64 66 3brtr4d 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` F ) <_ ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) / A ) )
68 5 29 11 lemuldiv2d 
 |-  ( ( ph /\ 0 < A ) -> ( ( A x. ( S.2 ` F ) ) <_ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <-> ( S.2 ` F ) <_ ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) / A ) ) )
69 67 68 mpbird 
 |-  ( ( ph /\ 0 < A ) -> ( A x. ( S.2 ` F ) ) <_ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) )
70 itg2cl 
 |-  ( ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. RR* )
71 24 70 syl 
 |-  ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. RR* )
72 26 rexrd 
 |-  ( ph -> ( A x. ( S.2 ` F ) ) e. RR* )
73 xrletri3 
 |-  ( ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) e. RR* /\ ( A x. ( S.2 ` F ) ) e. RR* ) -> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) <-> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) /\ ( A x. ( S.2 ` F ) ) <_ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) ) ) )
74 71 72 73 syl2anc 
 |-  ( ph -> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) <-> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) /\ ( A x. ( S.2 ` F ) ) <_ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) ) ) )
75 74 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) <-> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) /\ ( A x. ( S.2 ` F ) ) <_ ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) ) ) )
76 12 69 75 mpbir2and 
 |-  ( ( ph /\ 0 < A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) )
77 17 a1i 
 |-  ( ( ph /\ 0 = A ) -> RR e. _V )
78 37 adantr 
 |-  ( ( ph /\ 0 = A ) -> F : RR --> CC )
79 8 adantr 
 |-  ( ( ph /\ 0 = A ) -> A e. RR )
80 0re 
 |-  0 e. RR
81 80 a1i 
 |-  ( ( ph /\ 0 = A ) -> 0 e. RR )
82 simplr 
 |-  ( ( ( ph /\ 0 = A ) /\ x e. CC ) -> 0 = A )
83 82 oveq1d 
 |-  ( ( ( ph /\ 0 = A ) /\ x e. CC ) -> ( 0 x. x ) = ( A x. x ) )
84 mul02 
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
85 84 adantl 
 |-  ( ( ( ph /\ 0 = A ) /\ x e. CC ) -> ( 0 x. x ) = 0 )
86 83 85 eqtr3d 
 |-  ( ( ( ph /\ 0 = A ) /\ x e. CC ) -> ( A x. x ) = 0 )
87 77 78 79 81 86 caofid2 
 |-  ( ( ph /\ 0 = A ) -> ( ( RR X. { A } ) oF x. F ) = ( RR X. { 0 } ) )
88 87 fveq2d 
 |-  ( ( ph /\ 0 = A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( S.2 ` ( RR X. { 0 } ) ) )
89 itg20 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = 0
90 88 89 eqtrdi 
 |-  ( ( ph /\ 0 = A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = 0 )
91 2 adantr 
 |-  ( ( ph /\ 0 = A ) -> ( S.2 ` F ) e. RR )
92 91 recnd 
 |-  ( ( ph /\ 0 = A ) -> ( S.2 ` F ) e. CC )
93 92 mul02d 
 |-  ( ( ph /\ 0 = A ) -> ( 0 x. ( S.2 ` F ) ) = 0 )
94 simpr 
 |-  ( ( ph /\ 0 = A ) -> 0 = A )
95 94 oveq1d 
 |-  ( ( ph /\ 0 = A ) -> ( 0 x. ( S.2 ` F ) ) = ( A x. ( S.2 ` F ) ) )
96 90 93 95 3eqtr2d 
 |-  ( ( ph /\ 0 = A ) -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) )
97 7 simprd 
 |-  ( ph -> 0 <_ A )
98 leloe 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
99 80 8 98 sylancr 
 |-  ( ph -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
100 97 99 mpbid 
 |-  ( ph -> ( 0 < A \/ 0 = A ) )
101 76 96 100 mpjaodan 
 |-  ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) )