Metamath Proof Explorer


Theorem iblabsnc

Description: Choice-free analogue of iblabs . As with ibladdnc , a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses iblabsnc.1 φxABV
iblabsnc.2 φxAB𝐿1
iblabsnc.m φxABMblFn
Assertion iblabsnc φxAB𝐿1

Proof

Step Hyp Ref Expression
1 iblabsnc.1 φxABV
2 iblabsnc.2 φxAB𝐿1
3 iblabsnc.m φxABMblFn
4 iblmbf xAB𝐿1xABMblFn
5 2 4 syl φxABMblFn
6 5 1 mbfmptcl φxAB
7 6 abscld φxAB
8 7 rexrd φxAB*
9 6 absge0d φxA0B
10 elxrge0 B0+∞B*0B
11 8 9 10 sylanbrc φxAB0+∞
12 0e0iccpnf 00+∞
13 12 a1i φ¬xA00+∞
14 11 13 ifclda φifxAB00+∞
15 14 adantr φxifxAB00+∞
16 15 fmpttd φxifxAB0:0+∞
17 reex V
18 17 a1i φV
19 6 recld φxAB
20 19 recnd φxAB
21 20 abscld φxAB
22 20 absge0d φxA0B
23 elrege0 B0+∞B0B
24 21 22 23 sylanbrc φxAB0+∞
25 0e0icopnf 00+∞
26 25 a1i φ¬xA00+∞
27 24 26 ifclda φifxAB00+∞
28 27 adantr φxifxAB00+∞
29 6 imcld φxAB
30 29 recnd φxAB
31 30 abscld φxAB
32 30 absge0d φxA0B
33 elrege0 B0+∞B0B
34 31 32 33 sylanbrc φxAB0+∞
35 34 26 ifclda φifxAB00+∞
36 35 adantr φxifxAB00+∞
37 eqidd φxifxAB0=xifxAB0
38 eqidd φxifxAB0=xifxAB0
39 18 28 36 37 38 offval2 φxifxAB0+fxifxAB0=xifxAB0+ifxAB0
40 iftrue xAifxAB0=B
41 iftrue xAifxAB0=B
42 40 41 oveq12d xAifxAB0+ifxAB0=B+B
43 iftrue xAifxAB+B0=B+B
44 42 43 eqtr4d xAifxAB0+ifxAB0=ifxAB+B0
45 00id 0+0=0
46 iffalse ¬xAifxAB0=0
47 iffalse ¬xAifxAB0=0
48 46 47 oveq12d ¬xAifxAB0+ifxAB0=0+0
49 iffalse ¬xAifxAB+B0=0
50 45 48 49 3eqtr4a ¬xAifxAB0+ifxAB0=ifxAB+B0
51 44 50 pm2.61i ifxAB0+ifxAB0=ifxAB+B0
52 51 mpteq2i xifxAB0+ifxAB0=xifxAB+B0
53 39 52 eqtr2di φxifxAB+B0=xifxAB0+fxifxAB0
54 53 fveq2d φ2xifxAB+B0=2xifxAB0+fxifxAB0
55 eqid xifxAB0=xifxAB0
56 6 iblcn φxAB𝐿1xAB𝐿1xAB𝐿1
57 2 56 mpbid φxAB𝐿1xAB𝐿1
58 57 simpld φxAB𝐿1
59 1 2 55 58 19 iblabsnclem φxifxAB0MblFn2xifxAB0
60 59 simpld φxifxAB0MblFn
61 28 fmpttd φxifxAB0:0+∞
62 59 simprd φ2xifxAB0
63 36 fmpttd φxifxAB0:0+∞
64 eqid xifxAB0=xifxAB0
65 57 simprd φxAB𝐿1
66 1 2 64 65 29 iblabsnclem φxifxAB0MblFn2xifxAB0
67 66 simprd φ2xifxAB0
68 60 61 62 63 67 itg2addnc φ2xifxAB0+fxifxAB0=2xifxAB0+2xifxAB0
69 54 68 eqtrd φ2xifxAB+B0=2xifxAB0+2xifxAB0
70 62 67 readdcld φ2xifxAB0+2xifxAB0
71 69 70 eqeltrd φ2xifxAB+B0
72 21 31 readdcld φxAB+B
73 72 rexrd φxAB+B*
74 21 31 22 32 addge0d φxA0B+B
75 elxrge0 B+B0+∞B+B*0B+B
76 73 74 75 sylanbrc φxAB+B0+∞
77 76 13 ifclda φifxAB+B00+∞
78 77 adantr φxifxAB+B00+∞
79 78 fmpttd φxifxAB+B0:0+∞
80 ax-icn i
81 mulcl iBiB
82 80 30 81 sylancr φxAiB
83 20 82 abstrid φxAB+iBB+iB
84 iftrue xAifxAB0=B
85 84 adantl φxAifxAB0=B
86 6 replimd φxAB=B+iB
87 86 fveq2d φxAB=B+iB
88 85 87 eqtrd φxAifxAB0=B+iB
89 43 adantl φxAifxAB+B0=B+B
90 absmul iBiB=iB
91 80 30 90 sylancr φxAiB=iB
92 absi i=1
93 92 oveq1i iB=1B
94 31 recnd φxAB
95 94 mulid2d φxA1B=B
96 93 95 eqtrid φxAiB=B
97 91 96 eqtr2d φxAB=iB
98 97 oveq2d φxAB+B=B+iB
99 89 98 eqtrd φxAifxAB+B0=B+iB
100 83 88 99 3brtr4d φxAifxAB0ifxAB+B0
101 100 ex φxAifxAB0ifxAB+B0
102 0le0 00
103 102 a1i ¬xA00
104 iffalse ¬xAifxAB0=0
105 103 104 49 3brtr4d ¬xAifxAB0ifxAB+B0
106 101 105 pm2.61d1 φifxAB0ifxAB+B0
107 106 ralrimivw φxifxAB0ifxAB+B0
108 eqidd φxifxAB0=xifxAB0
109 eqidd φxifxAB+B0=xifxAB+B0
110 18 15 78 108 109 ofrfval2 φxifxAB0fxifxAB+B0xifxAB0ifxAB+B0
111 107 110 mpbird φxifxAB0fxifxAB+B0
112 itg2le xifxAB0:0+∞xifxAB+B0:0+∞xifxAB0fxifxAB+B02xifxAB02xifxAB+B0
113 16 79 111 112 syl3anc φ2xifxAB02xifxAB+B0
114 itg2lecl xifxAB0:0+∞2xifxAB+B02xifxAB02xifxAB+B02xifxAB0
115 16 71 113 114 syl3anc φ2xifxAB0
116 7 9 iblpos φxAB𝐿1xABMblFn2xifxAB0
117 3 115 116 mpbir2and φxAB𝐿1