Metamath Proof Explorer


Theorem iblmulc2nc

Description: Choice-free analogue of iblmulc2 . (Contributed by Brendan Leahy, 17-Nov-2017)

Ref Expression
Hypotheses itgmulc2nc.1 φC
itgmulc2nc.2 φxABV
itgmulc2nc.3 φxAB𝐿1
itgmulc2nc.m φxACBMblFn
Assertion iblmulc2nc φxACB𝐿1

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 φC
2 itgmulc2nc.2 φxABV
3 itgmulc2nc.3 φxAB𝐿1
4 itgmulc2nc.m φxACBMblFn
5 ifan ifxA0CBikCBik0=ifxAif0CBikCBik00
6 1 adantr φxAC
7 iblmbf xAB𝐿1xABMblFn
8 3 7 syl φxABMblFn
9 8 2 mbfmptcl φxAB
10 6 9 mulcld φxACB
11 10 adantlr φk03xACB
12 elfzelz k03k
13 12 ad2antlr φk03xAk
14 ax-icn i
15 ine0 i0
16 expclz ii0kik
17 14 15 16 mp3an12 kik
18 13 17 syl φk03xAik
19 expne0i ii0kik0
20 14 15 19 mp3an12 kik0
21 13 20 syl φk03xAik0
22 11 18 21 divcld φk03xACBik
23 22 recld φk03xACBik
24 0re 0
25 ifcl CBik0if0CBikCBik0
26 23 24 25 sylancl φk03xAif0CBikCBik0
27 26 rexrd φk03xAif0CBikCBik0*
28 max1 0CBik0if0CBikCBik0
29 24 23 28 sylancr φk03xA0if0CBikCBik0
30 elxrge0 if0CBikCBik00+∞if0CBikCBik0*0if0CBikCBik0
31 27 29 30 sylanbrc φk03xAif0CBikCBik00+∞
32 0e0iccpnf 00+∞
33 32 a1i φk03¬xA00+∞
34 31 33 ifclda φk03ifxAif0CBikCBik000+∞
35 34 adantr φk03xifxAif0CBikCBik000+∞
36 5 35 eqeltrid φk03xifxA0CBikCBik00+∞
37 36 fmpttd φk03xifxA0CBikCBik0:0+∞
38 9 recld φxAB
39 38 recnd φxAB
40 39 abscld φxAB
41 9 imcld φxAB
42 41 recnd φxAB
43 42 abscld φxAB
44 40 43 readdcld φxAB+B
45 39 absge0d φxA0B
46 42 absge0d φxA0B
47 40 43 45 46 addge0d φxA0B+B
48 elrege0 B+B0+∞B+B0B+B
49 44 47 48 sylanbrc φxAB+B0+∞
50 0e0icopnf 00+∞
51 50 a1i φ¬xA00+∞
52 49 51 ifclda φifxAB+B00+∞
53 52 adantr φxifxAB+B00+∞
54 53 fmpttd φxifxAB+B0:0+∞
55 reex V
56 55 a1i φV
57 elrege0 B0+∞B0B
58 40 45 57 sylanbrc φxAB0+∞
59 58 51 ifclda φifxAB00+∞
60 59 adantr φxifxAB00+∞
61 elrege0 B0+∞B0B
62 43 46 61 sylanbrc φxAB0+∞
63 62 51 ifclda φifxAB00+∞
64 63 adantr φxifxAB00+∞
65 eqidd φxifxAB0=xifxAB0
66 eqidd φxifxAB0=xifxAB0
67 56 60 64 65 66 offval2 φxifxAB0+fxifxAB0=xifxAB0+ifxAB0
68 iftrue xAifxAB0=B
69 iftrue xAifxAB0=B
70 68 69 oveq12d xAifxAB0+ifxAB0=B+B
71 iftrue xAifxAB+B0=B+B
72 70 71 eqtr4d xAifxAB0+ifxAB0=ifxAB+B0
73 00id 0+0=0
74 iffalse ¬xAifxAB0=0
75 iffalse ¬xAifxAB0=0
76 74 75 oveq12d ¬xAifxAB0+ifxAB0=0+0
77 iffalse ¬xAifxAB+B0=0
78 73 76 77 3eqtr4a ¬xAifxAB0+ifxAB0=ifxAB+B0
79 72 78 pm2.61i ifxAB0+ifxAB0=ifxAB+B0
80 79 mpteq2i xifxAB0+ifxAB0=xifxAB+B0
81 67 80 eqtr2di φxifxAB+B0=xifxAB0+fxifxAB0
82 81 fveq2d φ2xifxAB+B0=2xifxAB0+fxifxAB0
83 eqid xifxAB0=xifxAB0
84 9 iblcn φxAB𝐿1xAB𝐿1xAB𝐿1
85 3 84 mpbid φxAB𝐿1xAB𝐿1
86 85 simpld φxAB𝐿1
87 2 3 83 86 38 iblabsnclem φxifxAB0MblFn2xifxAB0
88 87 simpld φxifxAB0MblFn
89 60 fmpttd φxifxAB0:0+∞
90 87 simprd φ2xifxAB0
91 64 fmpttd φxifxAB0:0+∞
92 eqid xifxAB0=xifxAB0
93 85 simprd φxAB𝐿1
94 2 3 92 93 41 iblabsnclem φxifxAB0MblFn2xifxAB0
95 94 simprd φ2xifxAB0
96 88 89 90 91 95 itg2addnc φ2xifxAB0+fxifxAB0=2xifxAB0+2xifxAB0
97 82 96 eqtrd φ2xifxAB+B0=2xifxAB0+2xifxAB0
98 90 95 readdcld φ2xifxAB0+2xifxAB0
99 97 98 eqeltrd φ2xifxAB+B0
100 1 abscld φC
101 1 absge0d φ0C
102 elrege0 C0+∞C0C
103 100 101 102 sylanbrc φC0+∞
104 54 99 103 itg2mulc φ2×C×fxifxAB+B0=C2xifxAB+B0
105 100 adantr φxC
106 fconstmpt ×C=xC
107 106 a1i φ×C=xC
108 eqidd φxifxAB+B0=xifxAB+B0
109 56 105 53 107 108 offval2 φ×C×fxifxAB+B0=xCifxAB+B0
110 71 oveq2d xACifxAB+B0=CB+B
111 iftrue xAifxACB+B0=CB+B
112 110 111 eqtr4d xACifxAB+B0=ifxACB+B0
113 112 adantl φxACifxAB+B0=ifxACB+B0
114 100 recnd φC
115 114 mul01d φC0=0
116 115 adantr φ¬xAC0=0
117 77 adantl φ¬xAifxAB+B0=0
118 117 oveq2d φ¬xACifxAB+B0=C0
119 iffalse ¬xAifxACB+B0=0
120 119 adantl φ¬xAifxACB+B0=0
121 116 118 120 3eqtr4d φ¬xACifxAB+B0=ifxACB+B0
122 113 121 pm2.61dan φCifxAB+B0=ifxACB+B0
123 122 mpteq2dv φxCifxAB+B0=xifxACB+B0
124 109 123 eqtrd φ×C×fxifxAB+B0=xifxACB+B0
125 124 fveq2d φ2×C×fxifxAB+B0=2xifxACB+B0
126 97 oveq2d φC2xifxAB+B0=C2xifxAB0+2xifxAB0
127 104 125 126 3eqtr3d φ2xifxACB+B0=C2xifxAB0+2xifxAB0
128 100 98 remulcld φC2xifxAB0+2xifxAB0
129 127 128 eqeltrd φ2xifxACB+B0
130 129 adantr φk032xifxACB+B0
131 100 adantr φxAC
132 131 44 remulcld φxACB+B
133 132 rexrd φxACB+B*
134 101 adantr φxA0C
135 131 44 134 47 mulge0d φxA0CB+B
136 elxrge0 CB+B0+∞CB+B*0CB+B
137 133 135 136 sylanbrc φxACB+B0+∞
138 32 a1i φ¬xA00+∞
139 137 138 ifclda φifxACB+B00+∞
140 139 ad2antrr φk03xifxACB+B00+∞
141 140 fmpttd φk03xifxACB+B0:0+∞
142 9 abscld φxAB
143 131 142 remulcld φxACB
144 143 adantlr φk03xACB
145 132 adantlr φk03xACB+B
146 22 releabsd φk03xACBikCBik
147 11 18 21 absdivd φk03xACBik=CBik
148 elfznn0 k03k0
149 absexp ik0ik=ik
150 14 148 149 sylancr k03ik=ik
151 absi i=1
152 151 oveq1i ik=1k
153 1exp k1k=1
154 12 153 syl k031k=1
155 152 154 eqtrid k03ik=1
156 150 155 eqtrd k03ik=1
157 156 oveq2d k03CBik=CB1
158 157 ad2antlr φk03xACBik=CB1
159 10 abscld φxACB
160 159 recnd φxACB
161 160 adantlr φk03xACB
162 161 div1d φk03xACB1=CB
163 147 158 162 3eqtrd φk03xACBik=CB
164 6 9 absmuld φxACB=CB
165 164 adantlr φk03xACB=CB
166 163 165 eqtrd φk03xACBik=CB
167 146 166 breqtrd φk03xACBikCB
168 mulcl iBiB
169 14 42 168 sylancr φxAiB
170 39 169 abstrid φxAB+iBB+iB
171 9 replimd φxAB=B+iB
172 171 fveq2d φxAB=B+iB
173 absmul iBiB=iB
174 14 42 173 sylancr φxAiB=iB
175 151 oveq1i iB=1B
176 174 175 eqtrdi φxAiB=1B
177 43 recnd φxAB
178 177 mulid2d φxA1B=B
179 176 178 eqtr2d φxAB=iB
180 179 oveq2d φxAB+B=B+iB
181 170 172 180 3brtr4d φxABB+B
182 142 44 131 134 181 lemul2ad φxACBCB+B
183 182 adantlr φk03xACBCB+B
184 23 144 145 167 183 letrd φk03xACBikCB+B
185 135 adantlr φk03xA0CB+B
186 breq1 CBik=if0CBikCBik0CBikCB+Bif0CBikCBik0CB+B
187 breq1 0=if0CBikCBik00CB+Bif0CBikCBik0CB+B
188 186 187 ifboth CBikCB+B0CB+Bif0CBikCBik0CB+B
189 184 185 188 syl2anc φk03xAif0CBikCBik0CB+B
190 iftrue xAifxAif0CBikCBik00=if0CBikCBik0
191 190 adantl φk03xAifxAif0CBikCBik00=if0CBikCBik0
192 111 adantl φk03xAifxACB+B0=CB+B
193 189 191 192 3brtr4d φk03xAifxAif0CBikCBik00ifxACB+B0
194 193 ex φk03xAifxAif0CBikCBik00ifxACB+B0
195 0le0 00
196 195 a1i ¬xA00
197 iffalse ¬xAifxAif0CBikCBik00=0
198 196 197 119 3brtr4d ¬xAifxAif0CBikCBik00ifxACB+B0
199 194 198 pm2.61d1 φk03ifxAif0CBikCBik00ifxACB+B0
200 5 199 eqbrtrid φk03ifxA0CBikCBik0ifxACB+B0
201 200 ralrimivw φk03xifxA0CBikCBik0ifxACB+B0
202 55 a1i φk03V
203 eqidd φk03xifxA0CBikCBik0=xifxA0CBikCBik0
204 eqidd φk03xifxACB+B0=xifxACB+B0
205 202 36 140 203 204 ofrfval2 φk03xifxA0CBikCBik0fxifxACB+B0xifxA0CBikCBik0ifxACB+B0
206 201 205 mpbird φk03xifxA0CBikCBik0fxifxACB+B0
207 itg2le xifxA0CBikCBik0:0+∞xifxACB+B0:0+∞xifxA0CBikCBik0fxifxACB+B02xifxA0CBikCBik02xifxACB+B0
208 37 141 206 207 syl3anc φk032xifxA0CBikCBik02xifxACB+B0
209 itg2lecl xifxA0CBikCBik0:0+∞2xifxACB+B02xifxA0CBikCBik02xifxACB+B02xifxA0CBikCBik0
210 37 130 208 209 syl3anc φk032xifxA0CBikCBik0
211 210 ralrimiva φk032xifxA0CBikCBik0
212 eqidd φxifxA0CBikCBik0=xifxA0CBikCBik0
213 eqidd φxACBik=CBik
214 212 213 10 isibl2 φxACB𝐿1xACBMblFnk032xifxA0CBikCBik0
215 4 211 214 mpbir2and φxACB𝐿1