Metamath Proof Explorer

Theorem itg2mulclem

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

Ref Expression
Hypotheses itg2mulc.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2mulc.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2mulclem.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
Assertion itg2mulclem ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 itg2mulc.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
2 itg2mulc.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
3 itg2mulclem.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
4 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
5 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
6 1 4 5 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝑓 ∈ dom ∫1 )
9 3 rpreccld ⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℝ+ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 1 / 𝐴 ) ∈ ℝ+ )
11 10 rpred ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 1 / 𝐴 ) ∈ ℝ )
12 8 11 i1fmulc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∈ dom ∫1 )
13 itg2ub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∈ dom ∫1 ∧ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
14 13 3expia ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∈ dom ∫1 ) → ( ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∘r ≤ 𝐹 → ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
15 7 12 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∘r ≤ 𝐹 → ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
16 i1ff ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝑓 : ℝ ⟶ ℝ )
18 17 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑓 ‘ 𝑦 ) ∈ ℝ )
19 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
20 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
21 1 19 20 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐹 : ℝ ⟶ ℝ )
23 22 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
24 3 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℝ )
26 3 rpgt0d ⊢ ( 𝜑 → 0 < 𝐴 )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → 0 < 𝐴 )
28 ledivmul ⊢ ( ( ( 𝑓 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( ( 𝑓 ‘ 𝑦 ) / 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
29 18 23 25 27 28 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑓 ‘ 𝑦 ) / 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
30 18 recnd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑓 ‘ 𝑦 ) ∈ ℂ )
31 25 recnd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ )
32 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐴 ∈ ℝ+ )
33 32 rpne0d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐴 ≠ 0 )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → 𝐴 ≠ 0 )
35 30 31 34 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑦 ) / 𝐴 ) = ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) )
36 35 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑓 ‘ 𝑦 ) / 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
37 29 36 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑦 ) ≤ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
38 37 ralbidva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∀ 𝑦 ∈ ℝ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℝ ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
39 reex ⊢ ℝ ∈ V
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ℝ ∈ V )
41 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ V )
42 17 feqmptd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝑓 = ( 𝑦 ∈ ℝ ↦ ( 𝑓 ‘ 𝑦 ) ) )
43 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℝ+ )
44 fconstmpt ⊢ ( ℝ × { 𝐴 } ) = ( 𝑦 ∈ ℝ ↦ 𝐴 )
45 44 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ℝ × { 𝐴 } ) = ( 𝑦 ∈ ℝ ↦ 𝐴 ) )
46 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
48 40 43 23 45 47 offval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) = ( 𝑦 ∈ ℝ ↦ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
49 40 18 41 42 48 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
50 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ∈ V )
51 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 1 / 𝐴 ) ∈ ℝ+ )
52 fconstmpt ⊢ ( ℝ × { ( 1 / 𝐴 ) } ) = ( 𝑦 ∈ ℝ ↦ ( 1 / 𝐴 ) )
53 52 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ℝ × { ( 1 / 𝐴 ) } ) = ( 𝑦 ∈ ℝ ↦ ( 1 / 𝐴 ) ) )
54 40 51 18 53 42 offval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ) )
55 40 50 23 54 47 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ ( ( 1 / 𝐴 ) · ( 𝑓 ‘ 𝑦 ) ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
56 38 49 55 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ↔ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ∘r ≤ 𝐹 ) )
57 8 11 itg1mulc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) = ( ( 1 / 𝐴 ) · ( ∫1 ‘ 𝑓 ) ) )
58 itg1cl ⊢ ( 𝑓 ∈ dom ∫1 → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
60 59 recnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫1 ‘ 𝑓 ) ∈ ℂ )
61 24 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐴 ∈ ℝ )
62 61 recnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐴 ∈ ℂ )
63 60 62 33 divrec2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝑓 ) / 𝐴 ) = ( ( 1 / 𝐴 ) · ( ∫1 ‘ 𝑓 ) ) )
64 57 63 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) = ( ( ∫1 ‘ 𝑓 ) / 𝐴 ) )
65 64 breq1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ( ∫1 ‘ 𝑓 ) / 𝐴 ) ≤ ( ∫2 ‘ 𝐹 ) ) )
66 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
67 26 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 0 < 𝐴 )
68 ledivmul ⊢ ( ( ( ∫1 ‘ 𝑓 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( ( ∫1 ‘ 𝑓 ) / 𝐴 ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) )
69 59 66 61 67 68 syl112anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ( ∫1 ‘ 𝑓 ) / 𝐴 ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) )
70 65 69 bitr2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ( ∫1 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · 𝑓 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
71 15 56 70 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) → ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) )
72 71 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) → ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) )
73 ge0mulcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
75 fconstg ⊢ ( 𝐴 ∈ ℝ+ → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
76 3 75 syl ⊢ ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
77 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
78 rpge0 ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )
79 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
80 77 78 79 sylanbrc ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( 0 [,) +∞ ) )
81 3 80 syl ⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,) +∞ ) )
82 81 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 0 [,) +∞ ) )
83 76 82 fssd ⊢ ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ ( 0 [,) +∞ ) )
84 39 a1i ⊢ ( 𝜑 → ℝ ∈ V )
85 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
86 74 83 1 84 84 85 off ⊢ ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) )
87 fss ⊢ ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) )
88 86 4 87 sylancl ⊢ ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) )
89 24 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ )
90 89 rexrd ⊢ ( 𝜑 → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ* )
91 itg2leub ⊢ ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) → ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) ) )
92 88 90 91 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) → ( ∫1 ‘ 𝑓 ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) ) )
93 72 92 mpbird ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )