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	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2mulc.3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2mulc.4	$⊢ φ \to A \in [0, +∞)$
Assertion	itg2mulc	$⊢ φ \to \int^{2} ((ℝ \times \{A\}) \times_{f} F) = A \int^{2} (F)$

Proof

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

Metamath Proof Explorer

Theorem itg2mulc

Proof