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	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑓 ‘ 𝑦 ) ∈ ℝ )
19		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
20		fss	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
21	1 19 20	sylancl	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → 𝐹 : ℝ ⟶ ℝ )
23	22	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 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 ‘ 𝐹 ) ) )