# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {F}:ℝ⟶\left[0,\mathrm{+\infty }\right)$
itg2mulc.3 ${⊢}{\phi }\to {\int }^{2}\left({F}\right)\in ℝ$
itg2mulc.4 ${⊢}{\phi }\to {A}\in \left[0,\mathrm{+\infty }\right)$
Assertion itg2mulc ${⊢}{\phi }\to {\int }^{2}\left(\left(ℝ×\left\{{A}\right\}\right){×}_{f}{F}\right)={A}{\int }^{2}\left({F}\right)$

### Proof

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