Metamath Proof Explorer


Theorem iblmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 φC
itgmulc2.2 φxABV
itgmulc2.3 φxAB𝐿1
Assertion iblmulc2 φxACB𝐿1

Proof

Step Hyp Ref Expression
1 itgmulc2.1 φC
2 itgmulc2.2 φxABV
3 itgmulc2.3 φxAB𝐿1
4 iblmbf xAB𝐿1xABMblFn
5 3 4 syl φxABMblFn
6 1 2 5 mbfmulc2 φxACBMblFn
7 ifan ifxA0CBikCBik0=ifxAif0CBikCBik00
8 1 adantr φxAC
9 5 2 mbfmptcl φxAB
10 8 9 mulcld φxACB
11 10 adantlr φk03xACB
12 ax-icn i
13 ine0 i0
14 elfzelz k03k
15 14 ad2antlr φk03xAk
16 expclz ii0kik
17 12 13 15 16 mp3an12i φk03xAik
18 expne0i ii0kik0
19 12 13 15 18 mp3an12i φk03xAik0
20 11 17 19 divcld φk03xACBik
21 20 recld φk03xACBik
22 0re 0
23 ifcl CBik0if0CBikCBik0
24 21 22 23 sylancl φk03xAif0CBikCBik0
25 24 rexrd φk03xAif0CBikCBik0*
26 max1 0CBik0if0CBikCBik0
27 22 21 26 sylancr φk03xA0if0CBikCBik0
28 elxrge0 if0CBikCBik00+∞if0CBikCBik0*0if0CBikCBik0
29 25 27 28 sylanbrc φk03xAif0CBikCBik00+∞
30 0e0iccpnf 00+∞
31 30 a1i φk03¬xA00+∞
32 29 31 ifclda φk03ifxAif0CBikCBik000+∞
33 32 adantr φk03xifxAif0CBikCBik000+∞
34 7 33 eqeltrid φk03xifxA0CBikCBik00+∞
35 34 fmpttd φk03xifxA0CBikCBik0:0+∞
36 reex V
37 36 a1i φV
38 1 abscld φC
39 38 adantr φxC
40 9 abscld φxAB
41 9 absge0d φxA0B
42 elrege0 B0+∞B0B
43 40 41 42 sylanbrc φxAB0+∞
44 0e0icopnf 00+∞
45 44 a1i φ¬xA00+∞
46 43 45 ifclda φifxAB00+∞
47 46 adantr φxifxAB00+∞
48 fconstmpt ×C=xC
49 48 a1i φ×C=xC
50 eqidd φxifxAB0=xifxAB0
51 37 39 47 49 50 offval2 φ×C×fxifxAB0=xCifxAB0
52 ovif2 CifxAB0=ifxACBC0
53 8 9 absmuld φxACB=CB
54 53 ifeq1da φifxACBC0=ifxACBC0
55 38 recnd φC
56 55 mul01d φC0=0
57 56 ifeq2d φifxACBC0=ifxACB0
58 54 57 eqtr3d φifxACBC0=ifxACB0
59 52 58 eqtrid φCifxAB0=ifxACB0
60 59 mpteq2dv φxCifxAB0=xifxACB0
61 51 60 eqtrd φ×C×fxifxAB0=xifxACB0
62 61 fveq2d φ2×C×fxifxAB0=2xifxACB0
63 47 fmpttd φxifxAB0:0+∞
64 2 3 iblabs φxAB𝐿1
65 40 41 iblpos φxAB𝐿1xABMblFn2xifxAB0
66 64 65 mpbid φxABMblFn2xifxAB0
67 66 simprd φ2xifxAB0
68 abscl CC
69 absge0 C0C
70 elrege0 C0+∞C0C
71 68 69 70 sylanbrc CC0+∞
72 1 71 syl φC0+∞
73 63 67 72 itg2mulc φ2×C×fxifxAB0=C2xifxAB0
74 62 73 eqtr3d φ2xifxACB0=C2xifxAB0
75 38 67 remulcld φC2xifxAB0
76 74 75 eqeltrd φ2xifxACB0
77 76 adantr φk032xifxACB0
78 10 abscld φxACB
79 78 rexrd φxACB*
80 10 absge0d φxA0CB
81 elxrge0 CB0+∞CB*0CB
82 79 80 81 sylanbrc φxACB0+∞
83 30 a1i φ¬xA00+∞
84 82 83 ifclda φifxACB00+∞
85 84 adantr φxifxACB00+∞
86 85 fmpttd φxifxACB0:0+∞
87 86 adantr φk03xifxACB0:0+∞
88 20 releabsd φk03xACBikCBik
89 11 17 19 absdivd φk03xACBik=CBik
90 elfznn0 k03k0
91 90 ad2antlr φk03xAk0
92 absexp ik0ik=ik
93 12 91 92 sylancr φk03xAik=ik
94 absi i=1
95 94 oveq1i ik=1k
96 1exp k1k=1
97 15 96 syl φk03xA1k=1
98 95 97 eqtrid φk03xAik=1
99 93 98 eqtrd φk03xAik=1
100 99 oveq2d φk03xACBik=CB1
101 78 recnd φxACB
102 101 adantlr φk03xACB
103 102 div1d φk03xACB1=CB
104 89 100 103 3eqtrd φk03xACBik=CB
105 88 104 breqtrd φk03xACBikCB
106 80 adantlr φk03xA0CB
107 breq1 CBik=if0CBikCBik0CBikCBif0CBikCBik0CB
108 breq1 0=if0CBikCBik00CBif0CBikCBik0CB
109 107 108 ifboth CBikCB0CBif0CBikCBik0CB
110 105 106 109 syl2anc φk03xAif0CBikCBik0CB
111 iftrue xAifxAif0CBikCBik00=if0CBikCBik0
112 111 adantl φk03xAifxAif0CBikCBik00=if0CBikCBik0
113 iftrue xAifxACB0=CB
114 113 adantl φk03xAifxACB0=CB
115 110 112 114 3brtr4d φk03xAifxAif0CBikCBik00ifxACB0
116 115 ex φk03xAifxAif0CBikCBik00ifxACB0
117 0le0 00
118 117 a1i ¬xA00
119 iffalse ¬xAifxAif0CBikCBik00=0
120 iffalse ¬xAifxACB0=0
121 118 119 120 3brtr4d ¬xAifxAif0CBikCBik00ifxACB0
122 116 121 pm2.61d1 φk03ifxAif0CBikCBik00ifxACB0
123 7 122 eqbrtrid φk03ifxA0CBikCBik0ifxACB0
124 123 ralrimivw φk03xifxA0CBikCBik0ifxACB0
125 36 a1i φk03V
126 85 adantlr φk03xifxACB00+∞
127 eqidd φk03xifxA0CBikCBik0=xifxA0CBikCBik0
128 eqidd φk03xifxACB0=xifxACB0
129 125 34 126 127 128 ofrfval2 φk03xifxA0CBikCBik0fxifxACB0xifxA0CBikCBik0ifxACB0
130 124 129 mpbird φk03xifxA0CBikCBik0fxifxACB0
131 itg2le xifxA0CBikCBik0:0+∞xifxACB0:0+∞xifxA0CBikCBik0fxifxACB02xifxA0CBikCBik02xifxACB0
132 35 87 130 131 syl3anc φk032xifxA0CBikCBik02xifxACB0
133 itg2lecl xifxA0CBikCBik0:0+∞2xifxACB02xifxA0CBikCBik02xifxACB02xifxA0CBikCBik0
134 35 77 132 133 syl3anc φk032xifxA0CBikCBik0
135 134 ralrimiva φk032xifxA0CBikCBik0
136 eqidd φxifxA0CBikCBik0=xifxA0CBikCBik0
137 eqidd φxACBik=CBik
138 136 137 10 isibl2 φxACB𝐿1xACBMblFnk032xifxA0CBikCBik0
139 6 135 138 mpbir2and φxACB𝐿1