itg2mulclem

	Ref	Expression
Hypotheses	itg2mulc.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2mulc.3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2mulclem.4	$⊢ φ \to A \in ℝ^{+}$
Assertion	itg2mulclem	$⊢ φ \to \int^{2} ((ℝ \times \{A\}) \times_{f} F) \leq A \int^{2} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg2mulc.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
2		itg2mulc.3	$⊢ φ \to \int^{2} (F) \in ℝ$
3		itg2mulclem.4	$⊢ φ \to A \in ℝ^{+}$
4		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
5		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
6	1 4 5	sylancl	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
7	6	adantr	$⊢ (φ \land f \in dom \int^{1}) \to F : ℝ ⟶ [0, +∞]$
8		simpr	$⊢ (φ \land f \in dom \int^{1}) \to f \in dom \int^{1}$
9	3	rpreccld	$⊢ φ \to \frac{1}{A} \in ℝ^{+}$
10	9	adantr	$⊢ (φ \land f \in dom \int^{1}) \to \frac{1}{A} \in ℝ^{+}$
11	10	rpred	$⊢ (φ \land f \in dom \int^{1}) \to \frac{1}{A} \in ℝ$
12	8 11	i1fmulc	$⊢ (φ \land f \in dom \int^{1}) \to (ℝ \times \{\frac{1}{A}\}) \times_{f} f \in dom \int^{1}$
13		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land (ℝ \times \{\frac{1}{A}\}) \times_{f} f \in dom \int^{1} \land ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq_{f} F) \to \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq \int^{2} (F)$
14	13	3expia	$⊢ (F : ℝ ⟶ [0, +∞] \land (ℝ \times \{\frac{1}{A}\}) \times_{f} f \in dom \int^{1}) \to (((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq_{f} F \to \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq \int^{2} (F))$
15	7 12 14	syl2anc	$⊢ (φ \land f \in dom \int^{1}) \to (((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq_{f} F \to \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq \int^{2} (F))$
16		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
17	16	adantl	$⊢ (φ \land f \in dom \int^{1}) \to f : ℝ ⟶ ℝ$
18	17	ffvelcdmda	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to f (y) \in ℝ$
19		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
20		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℝ ⟶ ℝ$
21	1 19 20	sylancl	$⊢ φ \to F : ℝ ⟶ ℝ$
22	21	adantr	$⊢ (φ \land f \in dom \int^{1}) \to F : ℝ ⟶ ℝ$
23	22	ffvelcdmda	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to F (y) \in ℝ$
24	3	rpred	$⊢ φ \to A \in ℝ$
25	24	ad2antrr	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to A \in ℝ$
26	3	rpgt0d	$⊢ φ \to 0 < A$
27	26	ad2antrr	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to 0 < A$
28		ledivmul	$⊢ (f (y) \in ℝ \land F (y) \in ℝ \land (A \in ℝ \land 0 < A)) \to (\frac{f (y)}{A} \leq F (y) \leftrightarrow f (y) \leq A F (y))$
29	18 23 25 27 28	syl112anc	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to (\frac{f (y)}{A} \leq F (y) \leftrightarrow f (y) \leq A F (y))$
30	18	recnd	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to f (y) \in ℂ$
31	25	recnd	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to A \in ℂ$
32	3	adantr	$⊢ (φ \land f \in dom \int^{1}) \to A \in ℝ^{+}$
33	32	rpne0d	$⊢ (φ \land f \in dom \int^{1}) \to A \neq 0$
34	33	adantr	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to A \neq 0$
35	30 31 34	divrec2d	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to \frac{f (y)}{A} = (\frac{1}{A}) f (y)$
36	35	breq1d	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to (\frac{f (y)}{A} \leq F (y) \leftrightarrow (\frac{1}{A}) f (y) \leq F (y))$
37	29 36	bitr3d	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to (f (y) \leq A F (y) \leftrightarrow (\frac{1}{A}) f (y) \leq F (y))$
38	37	ralbidva	$⊢ (φ \land f \in dom \int^{1}) \to (\forall y \in ℝ f (y) \leq A F (y) \leftrightarrow \forall y \in ℝ (\frac{1}{A}) f (y) \leq F (y))$
39		reex	$⊢ ℝ \in V$
40	39	a1i	$⊢ (φ \land f \in dom \int^{1}) \to ℝ \in V$
41		ovexd	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to A F (y) \in V$
42	17	feqmptd	$⊢ (φ \land f \in dom \int^{1}) \to f = (y \in ℝ ⟼ f (y))$
43	3	ad2antrr	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to A \in ℝ^{+}$
44		fconstmpt	$⊢ ℝ \times \{A\} = (y \in ℝ ⟼ A)$
45	44	a1i	$⊢ (φ \land f \in dom \int^{1}) \to ℝ \times \{A\} = (y \in ℝ ⟼ A)$
46	1	feqmptd	$⊢ φ \to F = (y \in ℝ ⟼ F (y))$
47	46	adantr	$⊢ (φ \land f \in dom \int^{1}) \to F = (y \in ℝ ⟼ F (y))$
48	40 43 23 45 47	offval2	$⊢ (φ \land f \in dom \int^{1}) \to (ℝ \times \{A\}) \times_{f} F = (y \in ℝ ⟼ A F (y))$
49	40 18 41 42 48	ofrfval2	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \leftrightarrow \forall y \in ℝ f (y) \leq A F (y))$
50		ovexd	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to (\frac{1}{A}) f (y) \in V$
51	9	ad2antrr	$⊢ ((φ \land f \in dom \int^{1}) \land y \in ℝ) \to \frac{1}{A} \in ℝ^{+}$
52		fconstmpt	$⊢ ℝ \times \{\frac{1}{A}\} = (y \in ℝ ⟼ \frac{1}{A})$
53	52	a1i	$⊢ (φ \land f \in dom \int^{1}) \to ℝ \times \{\frac{1}{A}\} = (y \in ℝ ⟼ \frac{1}{A})$
54	40 51 18 53 42	offval2	$⊢ (φ \land f \in dom \int^{1}) \to (ℝ \times \{\frac{1}{A}\}) \times_{f} f = (y \in ℝ ⟼ (\frac{1}{A}) f (y))$
55	40 50 23 54 47	ofrfval2	$⊢ (φ \land f \in dom \int^{1}) \to (((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq_{f} F \leftrightarrow \forall y \in ℝ (\frac{1}{A}) f (y) \leq F (y))$
56	38 49 55	3bitr4d	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \leftrightarrow ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq_{f} F)$
57	8 11	itg1mulc	$⊢ (φ \land f \in dom \int^{1}) \to \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) = (\frac{1}{A}) \int^{1} (f)$
58		itg1cl	$⊢ f \in dom \int^{1} \to \int^{1} (f) \in ℝ$
59	58	adantl	$⊢ (φ \land f \in dom \int^{1}) \to \int^{1} (f) \in ℝ$
60	59	recnd	$⊢ (φ \land f \in dom \int^{1}) \to \int^{1} (f) \in ℂ$
61	24	adantr	$⊢ (φ \land f \in dom \int^{1}) \to A \in ℝ$
62	61	recnd	$⊢ (φ \land f \in dom \int^{1}) \to A \in ℂ$
63	60 62 33	divrec2d	$⊢ (φ \land f \in dom \int^{1}) \to \frac{\int^{1} (f)}{A} = (\frac{1}{A}) \int^{1} (f)$
64	57 63	eqtr4d	$⊢ (φ \land f \in dom \int^{1}) \to \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) = \frac{\int^{1} (f)}{A}$
65	64	breq1d	$⊢ (φ \land f \in dom \int^{1}) \to (\int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq \int^{2} (F) \leftrightarrow \frac{\int^{1} (f)}{A} \leq \int^{2} (F))$
66	2	adantr	$⊢ (φ \land f \in dom \int^{1}) \to \int^{2} (F) \in ℝ$
67	26	adantr	$⊢ (φ \land f \in dom \int^{1}) \to 0 < A$
68		ledivmul	$⊢ (\int^{1} (f) \in ℝ \land \int^{2} (F) \in ℝ \land (A \in ℝ \land 0 < A)) \to (\frac{\int^{1} (f)}{A} \leq \int^{2} (F) \leftrightarrow \int^{1} (f) \leq A \int^{2} (F))$
69	59 66 61 67 68	syl112anc	$⊢ (φ \land f \in dom \int^{1}) \to (\frac{\int^{1} (f)}{A} \leq \int^{2} (F) \leftrightarrow \int^{1} (f) \leq A \int^{2} (F))$
70	65 69	bitr2d	$⊢ (φ \land f \in dom \int^{1}) \to (\int^{1} (f) \leq A \int^{2} (F) \leftrightarrow \int^{1} ((ℝ \times \{\frac{1}{A}\}) \times_{f} f) \leq \int^{2} (F))$
71	15 56 70	3imtr4d	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \to \int^{1} (f) \leq A \int^{2} (F))$
72	71	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \to \int^{1} (f) \leq A \int^{2} (F))$
73		ge0mulcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x y \in [0, +∞)$
74	73	adantl	$⊢ (φ \land (x \in [0, +∞) \land y \in [0, +∞))) \to x y \in [0, +∞)$
75		fconstg	$⊢ A \in ℝ^{+} \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
76	3 75	syl	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
77		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
78		rpge0	$⊢ A \in ℝ^{+} \to 0 \leq A$
79		elrege0	$⊢ A \in [0, +∞) \leftrightarrow (A \in ℝ \land 0 \leq A)$
80	77 78 79	sylanbrc	$⊢ A \in ℝ^{+} \to A \in [0, +∞)$
81	3 80	syl	$⊢ φ \to A \in [0, +∞)$
82	81	snssd	$⊢ φ \to \{A\} \subseteq [0, +∞)$
83	76 82	fssd	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ [0, +∞)$
84	39	a1i	$⊢ φ \to ℝ \in V$
85		inidm	$⊢ ℝ \cap ℝ = ℝ$
86	74 83 1 84 84 85	off	$⊢ φ \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ [0, +∞)$
87		fss	$⊢ (((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ [0, +∞]$
88	86 4 87	sylancl	$⊢ φ \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ [0, +∞]$
89	24 2	remulcld	$⊢ φ \to A \int^{2} (F) \in ℝ$
90	89	rexrd	$⊢ φ \to A \int^{2} (F) \in ℝ^{*}$
91		itg2leub	$⊢ (((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ [0, +∞] \land A \int^{2} (F) \in ℝ^{*}) \to (\int^{2} ((ℝ \times \{A\}) \times_{f} F) \leq A \int^{2} (F) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \to \int^{1} (f) \leq A \int^{2} (F)))$
92	88 90 91	syl2anc	$⊢ φ \to (\int^{2} ((ℝ \times \{A\}) \times_{f} F) \leq A \int^{2} (F) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} ((ℝ \times \{A\}) \times_{f} F) \to \int^{1} (f) \leq A \int^{2} (F)))$
93	72 92	mpbird	$⊢ φ \to \int^{2} ((ℝ \times \{A\}) \times_{f} F) \leq A \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2mulclem

Proof