Metamath Proof Explorer

Theorem itg2mulclem

Description: Lemma for itg2mulc . (Contributed by Mario Carneiro, 8-Jul-2014)

Ref Expression
Hypotheses itg2mulc.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2mulc.3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2mulclem.4 
|- ( ph -> A e. RR+ )
Assertion itg2mulclem 
|- ( 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 itg2mulclem.4 
 |-  ( ph -> A e. RR+ )
4 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
5 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
6 1 4 5 sylancl 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
7 6 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> F : RR --> ( 0 [,] +oo ) )
8 simpr 
 |-  ( ( ph /\ f e. dom S.1 ) -> f e. dom S.1 )
9 3 rpreccld 
 |-  ( ph -> ( 1 / A ) e. RR+ )
10 9 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( 1 / A ) e. RR+ )
11 10 rpred 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( 1 / A ) e. RR )
12 8 11 i1fmulc 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( RR X. { ( 1 / A ) } ) oF x. f ) e. dom S.1 )
13 itg2ub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( ( RR X. { ( 1 / A ) } ) oF x. f ) e. dom S.1 /\ ( ( RR X. { ( 1 / A ) } ) oF x. f ) oR <_ F ) -> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) <_ ( S.2 ` F ) )
14 13 3expia 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( ( RR X. { ( 1 / A ) } ) oF x. f ) e. dom S.1 ) -> ( ( ( RR X. { ( 1 / A ) } ) oF x. f ) oR <_ F -> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) <_ ( S.2 ` F ) ) )
15 7 12 14 syl2anc 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( ( RR X. { ( 1 / A ) } ) oF x. f ) oR <_ F -> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) <_ ( S.2 ` F ) ) )
16 i1ff 
 |-  ( f e. dom S.1 -> f : RR --> RR )
17 16 adantl 
 |-  ( ( ph /\ f e. dom S.1 ) -> f : RR --> RR )
18 17 ffvelrnda 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( f ` y ) e. RR )
19 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
20 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
21 1 19 20 sylancl 
 |-  ( ph -> F : RR --> RR )
22 21 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> F : RR --> RR )
23 22 ffvelrnda 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( F ` y ) e. RR )
24 3 rpred 
 |-  ( ph -> A e. RR )
25 24 ad2antrr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> A e. RR )
26 3 rpgt0d 
 |-  ( ph -> 0 < A )
27 26 ad2antrr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> 0 < A )
28 ledivmul 
 |-  ( ( ( f ` y ) e. RR /\ ( F ` y ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( ( f ` y ) / A ) <_ ( F ` y ) <-> ( f ` y ) <_ ( A x. ( F ` y ) ) ) )
29 18 23 25 27 28 syl112anc 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( ( ( f ` y ) / A ) <_ ( F ` y ) <-> ( f ` y ) <_ ( A x. ( F ` y ) ) ) )
30 18 recnd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( f ` y ) e. CC )
31 25 recnd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> A e. CC )
32 3 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> A e. RR+ )
33 32 rpne0d 
 |-  ( ( ph /\ f e. dom S.1 ) -> A =/= 0 )
34 33 adantr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> A =/= 0 )
35 30 31 34 divrec2d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( ( f ` y ) / A ) = ( ( 1 / A ) x. ( f ` y ) ) )
36 35 breq1d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( ( ( f ` y ) / A ) <_ ( F ` y ) <-> ( ( 1 / A ) x. ( f ` y ) ) <_ ( F ` y ) ) )
37 29 36 bitr3d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( ( f ` y ) <_ ( A x. ( F ` y ) ) <-> ( ( 1 / A ) x. ( f ` y ) ) <_ ( F ` y ) ) )
38 37 ralbidva 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( A. y e. RR ( f ` y ) <_ ( A x. ( F ` y ) ) <-> A. y e. RR ( ( 1 / A ) x. ( f ` y ) ) <_ ( F ` y ) ) )
39 reex 
 |-  RR e. _V
40 39 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> RR e. _V )
41 ovexd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( A x. ( F ` y ) ) e. _V )
42 17 feqmptd 
 |-  ( ( ph /\ f e. dom S.1 ) -> f = ( y e. RR |-> ( f ` y ) ) )
43 3 ad2antrr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> A e. RR+ )
44 fconstmpt 
 |-  ( RR X. { A } ) = ( y e. RR |-> A )
45 44 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( RR X. { A } ) = ( y e. RR |-> A ) )
46 1 feqmptd 
 |-  ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
47 46 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> F = ( y e. RR |-> ( F ` y ) ) )
48 40 43 23 45 47 offval2 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( RR X. { A } ) oF x. F ) = ( y e. RR |-> ( A x. ( F ` y ) ) ) )
49 40 18 41 42 48 ofrfval2 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ ( ( RR X. { A } ) oF x. F ) <-> A. y e. RR ( f ` y ) <_ ( A x. ( F ` y ) ) ) )
50 ovexd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( ( 1 / A ) x. ( f ` y ) ) e. _V )
51 9 ad2antrr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ y e. RR ) -> ( 1 / A ) e. RR+ )
52 fconstmpt 
 |-  ( RR X. { ( 1 / A ) } ) = ( y e. RR |-> ( 1 / A ) )
53 52 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( RR X. { ( 1 / A ) } ) = ( y e. RR |-> ( 1 / A ) ) )
54 40 51 18 53 42 offval2 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( RR X. { ( 1 / A ) } ) oF x. f ) = ( y e. RR |-> ( ( 1 / A ) x. ( f ` y ) ) ) )
55 40 50 23 54 47 ofrfval2 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( ( RR X. { ( 1 / A ) } ) oF x. f ) oR <_ F <-> A. y e. RR ( ( 1 / A ) x. ( f ` y ) ) <_ ( F ` y ) ) )
56 38 49 55 3bitr4d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ ( ( RR X. { A } ) oF x. F ) <-> ( ( RR X. { ( 1 / A ) } ) oF x. f ) oR <_ F ) )
57 8 11 itg1mulc 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) = ( ( 1 / A ) x. ( S.1 ` f ) ) )
58 itg1cl 
 |-  ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
59 58 adantl 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.1 ` f ) e. RR )
60 59 recnd 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.1 ` f ) e. CC )
61 24 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> A e. RR )
62 61 recnd 
 |-  ( ( ph /\ f e. dom S.1 ) -> A e. CC )
63 60 62 33 divrec2d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( S.1 ` f ) / A ) = ( ( 1 / A ) x. ( S.1 ` f ) ) )
64 57 63 eqtr4d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) = ( ( S.1 ` f ) / A ) )
65 64 breq1d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) <_ ( S.2 ` F ) <-> ( ( S.1 ` f ) / A ) <_ ( S.2 ` F ) ) )
66 2 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.2 ` F ) e. RR )
67 26 adantr 
 |-  ( ( ph /\ f e. dom S.1 ) -> 0 < A )
68 ledivmul 
 |-  ( ( ( S.1 ` f ) e. RR /\ ( S.2 ` F ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( ( S.1 ` f ) / A ) <_ ( S.2 ` F ) <-> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) )
69 59 66 61 67 68 syl112anc 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( ( S.1 ` f ) / A ) <_ ( S.2 ` F ) <-> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) )
70 65 69 bitr2d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) <-> ( S.1 ` ( ( RR X. { ( 1 / A ) } ) oF x. f ) ) <_ ( S.2 ` F ) ) )
71 15 56 70 3imtr4d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ ( ( RR X. { A } ) oF x. F ) -> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) )
72 71 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ ( ( RR X. { A } ) oF x. F ) -> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) )
73 ge0mulcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )
74 73 adantl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )
75 fconstg 
 |-  ( A e. RR+ -> ( RR X. { A } ) : RR --> { A } )
76 3 75 syl 
 |-  ( ph -> ( RR X. { A } ) : RR --> { A } )
77 rpre 
 |-  ( A e. RR+ -> A e. RR )
78 rpge0 
 |-  ( A e. RR+ -> 0 <_ A )
79 elrege0 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
80 77 78 79 sylanbrc 
 |-  ( A e. RR+ -> A e. ( 0 [,) +oo ) )
81 3 80 syl 
 |-  ( ph -> A e. ( 0 [,) +oo ) )
82 81 snssd 
 |-  ( ph -> { A } C_ ( 0 [,) +oo ) )
83 76 82 fssd 
 |-  ( ph -> ( RR X. { A } ) : RR --> ( 0 [,) +oo ) )
84 39 a1i 
 |-  ( ph -> RR e. _V )
85 inidm 
 |-  ( RR i^i RR ) = RR
86 74 83 1 84 84 85 off 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,) +oo ) )
87 fss 
 |-  ( ( ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) )
88 86 4 87 sylancl 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> ( 0 [,] +oo ) )
89 24 2 remulcld 
 |-  ( ph -> ( A x. ( S.2 ` F ) ) e. RR )
90 89 rexrd 
 |-  ( ph -> ( A x. ( S.2 ` F ) ) e. RR* )
91 itg2leub 
 |-  ( ( ( ( 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 ) ) <-> A. f e. dom S.1 ( f oR <_ ( ( RR X. { A } ) oF x. F ) -> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) ) )
92 88 90 91 syl2anc 
 |-  ( ph -> ( ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) <-> A. f e. dom S.1 ( f oR <_ ( ( RR X. { A } ) oF x. F ) -> ( S.1 ` f ) <_ ( A x. ( S.2 ` F ) ) ) ) )
93 72 92 mpbird 
 |-  ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) )