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 φ F : 0 +∞
itg2mulc.3 φ 2 F
itg2mulc.4 φ A 0 +∞
Assertion itg2mulc φ 2 × A × f F = A 2 F

Proof

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