Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ibladdnc Structured version   Unicode version

 Description: Choice-free analogue of itgadd 22104. A measurability hypothesis is necessitated by the loss of mbfadd 21941; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

StepHypRef Expression
2 ibladdnc.2 . . . . . . 7
3 iblmbf 22047 . . . . . . 7 MblFn
42, 3syl 16 . . . . . 6 MblFn
5 ibladdnc.1 . . . . . 6
64, 5mbfmptcl 21917 . . . . 5
76recld 13006 . . . 4
8 ibladdnc.4 . . . . . . 7
9 iblmbf 22047 . . . . . . 7 MblFn
108, 9syl 16 . . . . . 6 MblFn
11 ibladdnc.3 . . . . . 6
1210, 11mbfmptcl 21917 . . . . 5
1312recld 13006 . . . 4
146, 12readdd 13026 . . . 4
156ismbfcn2 21919 . . . . . 6 MblFn MblFn MblFn
164, 15mpbid 210 . . . . 5 MblFn MblFn
1716simpld 459 . . . 4 MblFn
18 eqid 2443 . . . . . . . 8
19 eqid 2443 . . . . . . . 8
20 eqid 2443 . . . . . . . 8
21 eqid 2443 . . . . . . . 8
2218, 19, 20, 21, 5iblcnlem 22068 . . . . . . 7 MblFn
232, 22mpbid 210 . . . . . 6 MblFn
2423simp2d 1010 . . . . 5
2524simpld 459 . . . 4
26 eqid 2443 . . . . . . . 8
27 eqid 2443 . . . . . . . 8
28 eqid 2443 . . . . . . . 8
29 eqid 2443 . . . . . . . 8
3026, 27, 28, 29, 11iblcnlem 22068 . . . . . . 7 MblFn
318, 30mpbid 210 . . . . . 6 MblFn
3231simp2d 1010 . . . . 5
3332simpld 459 . . . 4
347, 13, 14, 17, 25, 33ibladdnclem 30046 . . 3
357renegcld 9992 . . . 4
3613renegcld 9992 . . . 4
3714negeqd 9819 . . . . 5
387recnd 9625 . . . . . 6
3913recnd 9625 . . . . . 6
4038, 39negdid 9949 . . . . 5
4137, 40eqtrd 2484 . . . 4
427, 17mbfneg 21930 . . . 4 MblFn
4324simprd 463 . . . 4
4432simprd 463 . . . 4
4535, 36, 41, 42, 43, 44ibladdnclem 30046 . . 3
4634, 45jca 532 . 2
476imcld 13007 . . . 4
4812imcld 13007 . . . 4
496, 12imaddd 13027 . . . 4
5016simprd 463 . . . 4 MblFn
5123simp3d 1011 . . . . 5
5251simpld 459 . . . 4
5331simp3d 1011 . . . . 5
5453simpld 459 . . . 4
5547, 48, 49, 50, 52, 54ibladdnclem 30046 . . 3
5647renegcld 9992 . . . 4
5748renegcld 9992 . . . 4
5849negeqd 9819 . . . . 5
5947recnd 9625 . . . . . 6
6048recnd 9625 . . . . . 6
6159, 60negdid 9949 . . . . 5
6258, 61eqtrd 2484 . . . 4
6347, 50mbfneg 21930 . . . 4 MblFn
6451simprd 463 . . . 4
6553simprd 463 . . . 4
6656, 57, 62, 63, 64, 65ibladdnclem 30046 . . 3
6755, 66jca 532 . 2
68 eqid 2443 . . 3
69 eqid 2443 . . 3
70 eqid 2443 . . 3
71 eqid 2443 . . 3
72 ovex 6309 . . . 4
7372a1i 11 . . 3
7468, 69, 70, 71, 73iblcnlem 22068 . 2 MblFn
751, 46, 67, 74mpbir3and 1180 1