Metamath Proof Explorer

Theorem itgaddnclem2

Description: Lemma for itgaddnc ; cf. itgaddlem2 . (Contributed by Brendan Leahy, 10-Nov-2017) (Revised by Brendan Leahy, 3-Apr-2018)

Ref Expression
Hypotheses ibladdnc.1 
|- ( ( ph /\ x e. A ) -> B e. V )
ibladdnc.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
ibladdnc.3 
|- ( ( ph /\ x e. A ) -> C e. V )
ibladdnc.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
ibladdnc.m 
|- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
itgaddnclem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgaddnclem.2 
|- ( ( ph /\ x e. A ) -> C e. RR )
Assertion itgaddnclem2 
|- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )

Proof

Step Hyp Ref Expression
1 ibladdnc.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 ibladdnc.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 ibladdnc.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 ibladdnc.4 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 ibladdnc.m 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
6 itgaddnclem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
7 itgaddnclem.2 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
8 max0sub 
 |-  ( B e. RR -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
9 6 8 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
10 max0sub 
 |-  ( C e. RR -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
11 7 10 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
12 9 11 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) + ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) ) = ( B + C ) )
13 0re 
 |-  0 e. RR
14 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
15 6 13 14 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
16 15 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
17 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
18 7 13 17 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
19 18 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. CC )
20 6 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
21 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
22 20 13 21 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
23 22 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. CC )
24 7 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. RR )
25 ifcl 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
26 24 13 25 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
27 26 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
28 16 19 23 27 addsub4d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) = ( ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) + ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) ) )
29 6 7 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
30 max0sub 
 |-  ( ( B + C ) e. RR -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( B + C ) )
31 29 30 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( B + C ) )
32 12 28 31 3eqtr4rd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
33 29 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( B + C ) e. RR )
34 ifcl 
 |-  ( ( -u ( B + C ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. RR )
35 33 13 34 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. RR )
36 35 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. CC )
37 15 18 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
38 37 recnd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. CC )
39 ifcl 
 |-  ( ( ( B + C ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. RR )
40 29 13 39 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. RR )
41 40 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. CC )
42 22 26 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) e. RR )
43 42 recnd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) e. CC )
44 36 38 41 43 addsubeq4d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) <-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) )
45 32 44 mpbird 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
46 45 itgeq2dv 
 |-  ( ph -> S. A ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) _d x = S. A ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) _d x )
47 6 2 7 4 5 ibladdnc 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
48 29 iblre 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 ) ) )
49 47 48 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 ) )
50 49 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 )
51 6 iblre 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )
52 2 51 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) )
53 52 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
54 7 iblre 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 ) ) )
55 4 54 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 ) )
56 55 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 )
57 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
58 2 57 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
59 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
60 4 59 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
61 58 6 60 7 5 mbfposadd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. MblFn )
62 15 53 18 56 61 ibladdnc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. L^1 )
63 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
64 13 6 63 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
65 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
66 13 7 65 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
67 15 18 64 66 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
68 67 iftrued 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
69 68 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) = ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
70 69 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) )
71 29 5 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( B + C ) ) e. MblFn )
72 6 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
73 7 recnd 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
74 72 73 negdid 
 |-  ( ( ph /\ x e. A ) -> -u ( B + C ) = ( -u B + -u C ) )
75 74 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( -u ( B + C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( ( -u B + -u C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
76 20 recnd 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
77 24 recnd 
 |-  ( ( ph /\ x e. A ) -> -u C e. CC )
78 76 77 16 19 add4d 
 |-  ( ( ph /\ x e. A ) -> ( ( -u B + -u C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( ( -u B + if ( 0 <_ B , B , 0 ) ) + ( -u C + if ( 0 <_ C , C , 0 ) ) ) )
79 negeq 
 |-  ( B = 0 -> -u B = -u 0 )
80 neg0 
 |-  -u 0 = 0
81 79 80 eqtrdi 
 |-  ( B = 0 -> -u B = 0 )
82 0le0 
 |-  0 <_ 0
83 82 81 breqtrrid 
 |-  ( B = 0 -> 0 <_ -u B )
84 83 iftrued 
 |-  ( B = 0 -> if ( 0 <_ -u B , -u B , 0 ) = -u B )
85 id 
 |-  ( B = 0 -> B = 0 )
86 82 85 breqtrrid 
 |-  ( B = 0 -> 0 <_ B )
87 86 iftrued 
 |-  ( B = 0 -> if ( 0 <_ B , B , 0 ) = B )
88 87 85 eqtrd 
 |-  ( B = 0 -> if ( 0 <_ B , B , 0 ) = 0 )
89 81 88 oveq12d 
 |-  ( B = 0 -> ( -u B + if ( 0 <_ B , B , 0 ) ) = ( 0 + 0 ) )
90 00id 
 |-  ( 0 + 0 ) = 0
91 89 90 eqtrdi 
 |-  ( B = 0 -> ( -u B + if ( 0 <_ B , B , 0 ) ) = 0 )
92 81 84 91 3eqtr4rd 
 |-  ( B = 0 -> ( -u B + if ( 0 <_ B , B , 0 ) ) = if ( 0 <_ -u B , -u B , 0 ) )
93 92 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ B = 0 ) -> ( -u B + if ( 0 <_ B , B , 0 ) ) = if ( 0 <_ -u B , -u B , 0 ) )
94 ovif2 
 |-  ( -u B + if ( 0 <_ B , B , 0 ) ) = if ( 0 <_ B , ( -u B + B ) , ( -u B + 0 ) )
95 72 negne0bd 
 |-  ( ( ph /\ x e. A ) -> ( B =/= 0 <-> -u B =/= 0 ) )
96 95 biimpa 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> -u B =/= 0 )
97 6 le0neg2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ B <-> -u B <_ 0 ) )
98 leloe 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> ( -u B <_ 0 <-> ( -u B < 0 \/ -u B = 0 ) ) )
99 20 13 98 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( -u B <_ 0 <-> ( -u B < 0 \/ -u B = 0 ) ) )
100 97 99 bitrd 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( -u B < 0 \/ -u B = 0 ) ) )
101 df-ne 
 |-  ( -u B =/= 0 <-> -. -u B = 0 )
102 biorf 
 |-  ( -. -u B = 0 -> ( -u B < 0 <-> ( -u B = 0 \/ -u B < 0 ) ) )
103 101 102 sylbi 
 |-  ( -u B =/= 0 -> ( -u B < 0 <-> ( -u B = 0 \/ -u B < 0 ) ) )
104 orcom 
 |-  ( ( -u B = 0 \/ -u B < 0 ) <-> ( -u B < 0 \/ -u B = 0 ) )
105 103 104 bitr2di 
 |-  ( -u B =/= 0 -> ( ( -u B < 0 \/ -u B = 0 ) <-> -u B < 0 ) )
106 100 105 sylan9bb 
 |-  ( ( ( ph /\ x e. A ) /\ -u B =/= 0 ) -> ( 0 <_ B <-> -u B < 0 ) )
107 96 106 syldan 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( 0 <_ B <-> -u B < 0 ) )
108 ltnle 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> ( -u B < 0 <-> -. 0 <_ -u B ) )
109 20 13 108 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( -u B < 0 <-> -. 0 <_ -u B ) )
110 109 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( -u B < 0 <-> -. 0 <_ -u B ) )
111 107 110 bitrd 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( 0 <_ B <-> -. 0 <_ -u B ) )
112 76 72 addcomd 
 |-  ( ( ph /\ x e. A ) -> ( -u B + B ) = ( B + -u B ) )
113 72 negidd 
 |-  ( ( ph /\ x e. A ) -> ( B + -u B ) = 0 )
114 112 113 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( -u B + B ) = 0 )
115 114 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( -u B + B ) = 0 )
116 76 addid1d 
 |-  ( ( ph /\ x e. A ) -> ( -u B + 0 ) = -u B )
117 116 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( -u B + 0 ) = -u B )
118 111 115 117 ifbieq12d 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> if ( 0 <_ B , ( -u B + B ) , ( -u B + 0 ) ) = if ( -. 0 <_ -u B , 0 , -u B ) )
119 ifnot 
 |-  if ( -. 0 <_ -u B , 0 , -u B ) = if ( 0 <_ -u B , -u B , 0 )
120 118 119 eqtrdi 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> if ( 0 <_ B , ( -u B + B ) , ( -u B + 0 ) ) = if ( 0 <_ -u B , -u B , 0 ) )
121 94 120 syl5eq 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( -u B + if ( 0 <_ B , B , 0 ) ) = if ( 0 <_ -u B , -u B , 0 ) )
122 93 121 pm2.61dane 
 |-  ( ( ph /\ x e. A ) -> ( -u B + if ( 0 <_ B , B , 0 ) ) = if ( 0 <_ -u B , -u B , 0 ) )
123 negeq 
 |-  ( C = 0 -> -u C = -u 0 )
124 123 80 eqtrdi 
 |-  ( C = 0 -> -u C = 0 )
125 82 124 breqtrrid 
 |-  ( C = 0 -> 0 <_ -u C )
126 125 iftrued 
 |-  ( C = 0 -> if ( 0 <_ -u C , -u C , 0 ) = -u C )
127 id 
 |-  ( C = 0 -> C = 0 )
128 82 127 breqtrrid 
 |-  ( C = 0 -> 0 <_ C )
129 128 iftrued 
 |-  ( C = 0 -> if ( 0 <_ C , C , 0 ) = C )
130 129 127 eqtrd 
 |-  ( C = 0 -> if ( 0 <_ C , C , 0 ) = 0 )
131 124 130 oveq12d 
 |-  ( C = 0 -> ( -u C + if ( 0 <_ C , C , 0 ) ) = ( 0 + 0 ) )
132 131 90 eqtrdi 
 |-  ( C = 0 -> ( -u C + if ( 0 <_ C , C , 0 ) ) = 0 )
133 124 126 132 3eqtr4rd 
 |-  ( C = 0 -> ( -u C + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ -u C , -u C , 0 ) )
134 133 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ C = 0 ) -> ( -u C + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ -u C , -u C , 0 ) )
135 ovif2 
 |-  ( -u C + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ C , ( -u C + C ) , ( -u C + 0 ) )
136 73 negne0bd 
 |-  ( ( ph /\ x e. A ) -> ( C =/= 0 <-> -u C =/= 0 ) )
137 136 biimpa 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> -u C =/= 0 )
138 7 le0neg2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ C <-> -u C <_ 0 ) )
139 leloe 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> ( -u C <_ 0 <-> ( -u C < 0 \/ -u C = 0 ) ) )
140 24 13 139 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( -u C <_ 0 <-> ( -u C < 0 \/ -u C = 0 ) ) )
141 138 140 bitrd 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( -u C < 0 \/ -u C = 0 ) ) )
142 df-ne 
 |-  ( -u C =/= 0 <-> -. -u C = 0 )
143 biorf 
 |-  ( -. -u C = 0 -> ( -u C < 0 <-> ( -u C = 0 \/ -u C < 0 ) ) )
144 142 143 sylbi 
 |-  ( -u C =/= 0 -> ( -u C < 0 <-> ( -u C = 0 \/ -u C < 0 ) ) )
145 orcom 
 |-  ( ( -u C = 0 \/ -u C < 0 ) <-> ( -u C < 0 \/ -u C = 0 ) )
146 144 145 bitr2di 
 |-  ( -u C =/= 0 -> ( ( -u C < 0 \/ -u C = 0 ) <-> -u C < 0 ) )
147 141 146 sylan9bb 
 |-  ( ( ( ph /\ x e. A ) /\ -u C =/= 0 ) -> ( 0 <_ C <-> -u C < 0 ) )
148 137 147 syldan 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( 0 <_ C <-> -u C < 0 ) )
149 ltnle 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> ( -u C < 0 <-> -. 0 <_ -u C ) )
150 24 13 149 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( -u C < 0 <-> -. 0 <_ -u C ) )
151 150 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( -u C < 0 <-> -. 0 <_ -u C ) )
152 148 151 bitrd 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( 0 <_ C <-> -. 0 <_ -u C ) )
153 77 73 addcomd 
 |-  ( ( ph /\ x e. A ) -> ( -u C + C ) = ( C + -u C ) )
154 73 negidd 
 |-  ( ( ph /\ x e. A ) -> ( C + -u C ) = 0 )
155 153 154 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( -u C + C ) = 0 )
156 155 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( -u C + C ) = 0 )
157 77 addid1d 
 |-  ( ( ph /\ x e. A ) -> ( -u C + 0 ) = -u C )
158 157 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( -u C + 0 ) = -u C )
159 152 156 158 ifbieq12d 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> if ( 0 <_ C , ( -u C + C ) , ( -u C + 0 ) ) = if ( -. 0 <_ -u C , 0 , -u C ) )
160 ifnot 
 |-  if ( -. 0 <_ -u C , 0 , -u C ) = if ( 0 <_ -u C , -u C , 0 )
161 159 160 eqtrdi 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> if ( 0 <_ C , ( -u C + C ) , ( -u C + 0 ) ) = if ( 0 <_ -u C , -u C , 0 ) )
162 135 161 syl5eq 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( -u C + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ -u C , -u C , 0 ) )
163 134 162 pm2.61dane 
 |-  ( ( ph /\ x e. A ) -> ( -u C + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ -u C , -u C , 0 ) )
164 122 163 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( -u B + if ( 0 <_ B , B , 0 ) ) + ( -u C + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) )
165 75 78 164 3eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( -u ( B + C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) )
166 165 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( -u ( B + C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) = ( x e. A |-> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
167 6 58 mbfneg 
 |-  ( ph -> ( x e. A |-> -u B ) e. MblFn )
168 7 60 mbfneg 
 |-  ( ph -> ( x e. A |-> -u C ) e. MblFn )
169 74 mpteq2dva 
 |-  ( ph -> ( x e. A |-> -u ( B + C ) ) = ( x e. A |-> ( -u B + -u C ) ) )
170 169 71 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( -u B + -u C ) ) e. MblFn )
171 167 20 168 24 170 mbfposadd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) e. MblFn )
172 166 171 eqeltrd 
 |-  ( ph -> ( x e. A |-> ( -u ( B + C ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) e. MblFn )
173 71 33 61 37 172 mbfposadd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. MblFn )
174 70 173 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) e. MblFn )
175 max1 
 |-  ( ( 0 e. RR /\ -u ( B + C ) e. RR ) -> 0 <_ if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) )
176 13 33 175 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) )
177 35 50 37 62 174 35 37 176 67 itgaddnclem1 
 |-  ( ph -> S. A ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) _d x = ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) )
178 49 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 )
179 52 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
180 55 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 )
181 22 179 26 180 171 ibladdnc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) e. L^1 )
182 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
183 13 20 182 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
184 max1 
 |-  ( ( 0 e. RR /\ -u C e. RR ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
185 13 24 184 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
186 22 26 183 185 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) )
187 186 iftrued 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , 0 ) = ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) )
188 187 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , 0 ) ) = ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
189 188 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) )
190 72 73 23 27 add4d 
 |-  ( ( ph /\ x e. A ) -> ( ( B + C ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) = ( ( B + if ( 0 <_ -u B , -u B , 0 ) ) + ( C + if ( 0 <_ -u C , -u C , 0 ) ) ) )
191 84 81 eqtrd 
 |-  ( B = 0 -> if ( 0 <_ -u B , -u B , 0 ) = 0 )
192 85 191 oveq12d 
 |-  ( B = 0 -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = ( 0 + 0 ) )
193 192 90 eqtrdi 
 |-  ( B = 0 -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = 0 )
194 85 87 193 3eqtr4rd 
 |-  ( B = 0 -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = if ( 0 <_ B , B , 0 ) )
195 194 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ B = 0 ) -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = if ( 0 <_ B , B , 0 ) )
196 ovif2 
 |-  ( B + if ( 0 <_ -u B , -u B , 0 ) ) = if ( 0 <_ -u B , ( B + -u B ) , ( B + 0 ) )
197 6 le0neg1d 
 |-  ( ( ph /\ x e. A ) -> ( B <_ 0 <-> 0 <_ -u B ) )
198 leloe 
 |-  ( ( B e. RR /\ 0 e. RR ) -> ( B <_ 0 <-> ( B < 0 \/ B = 0 ) ) )
199 6 13 198 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( B <_ 0 <-> ( B < 0 \/ B = 0 ) ) )
200 197 199 bitr3d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u B <-> ( B < 0 \/ B = 0 ) ) )
201 df-ne 
 |-  ( B =/= 0 <-> -. B = 0 )
202 biorf 
 |-  ( -. B = 0 -> ( B < 0 <-> ( B = 0 \/ B < 0 ) ) )
203 201 202 sylbi 
 |-  ( B =/= 0 -> ( B < 0 <-> ( B = 0 \/ B < 0 ) ) )
204 orcom 
 |-  ( ( B = 0 \/ B < 0 ) <-> ( B < 0 \/ B = 0 ) )
205 203 204 bitr2di 
 |-  ( B =/= 0 -> ( ( B < 0 \/ B = 0 ) <-> B < 0 ) )
206 200 205 sylan9bb 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( 0 <_ -u B <-> B < 0 ) )
207 ltnle 
 |-  ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
208 6 13 207 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( B < 0 <-> -. 0 <_ B ) )
209 208 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( B < 0 <-> -. 0 <_ B ) )
210 206 209 bitrd 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( 0 <_ -u B <-> -. 0 <_ B ) )
211 113 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( B + -u B ) = 0 )
212 72 addid1d 
 |-  ( ( ph /\ x e. A ) -> ( B + 0 ) = B )
213 212 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( B + 0 ) = B )
214 210 211 213 ifbieq12d 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> if ( 0 <_ -u B , ( B + -u B ) , ( B + 0 ) ) = if ( -. 0 <_ B , 0 , B ) )
215 ifnot 
 |-  if ( -. 0 <_ B , 0 , B ) = if ( 0 <_ B , B , 0 )
216 214 215 eqtrdi 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> if ( 0 <_ -u B , ( B + -u B ) , ( B + 0 ) ) = if ( 0 <_ B , B , 0 ) )
217 196 216 syl5eq 
 |-  ( ( ( ph /\ x e. A ) /\ B =/= 0 ) -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = if ( 0 <_ B , B , 0 ) )
218 195 217 pm2.61dane 
 |-  ( ( ph /\ x e. A ) -> ( B + if ( 0 <_ -u B , -u B , 0 ) ) = if ( 0 <_ B , B , 0 ) )
219 126 124 eqtrd 
 |-  ( C = 0 -> if ( 0 <_ -u C , -u C , 0 ) = 0 )
220 127 219 oveq12d 
 |-  ( C = 0 -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = ( 0 + 0 ) )
221 220 90 eqtrdi 
 |-  ( C = 0 -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = 0 )
222 127 129 221 3eqtr4rd 
 |-  ( C = 0 -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = if ( 0 <_ C , C , 0 ) )
223 222 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ C = 0 ) -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = if ( 0 <_ C , C , 0 ) )
224 ovif2 
 |-  ( C + if ( 0 <_ -u C , -u C , 0 ) ) = if ( 0 <_ -u C , ( C + -u C ) , ( C + 0 ) )
225 7 le0neg1d 
 |-  ( ( ph /\ x e. A ) -> ( C <_ 0 <-> 0 <_ -u C ) )
226 leloe 
 |-  ( ( C e. RR /\ 0 e. RR ) -> ( C <_ 0 <-> ( C < 0 \/ C = 0 ) ) )
227 7 13 226 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( C <_ 0 <-> ( C < 0 \/ C = 0 ) ) )
228 225 227 bitr3d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u C <-> ( C < 0 \/ C = 0 ) ) )
229 df-ne 
 |-  ( C =/= 0 <-> -. C = 0 )
230 biorf 
 |-  ( -. C = 0 -> ( C < 0 <-> ( C = 0 \/ C < 0 ) ) )
231 229 230 sylbi 
 |-  ( C =/= 0 -> ( C < 0 <-> ( C = 0 \/ C < 0 ) ) )
232 orcom 
 |-  ( ( C = 0 \/ C < 0 ) <-> ( C < 0 \/ C = 0 ) )
233 231 232 bitr2di 
 |-  ( C =/= 0 -> ( ( C < 0 \/ C = 0 ) <-> C < 0 ) )
234 228 233 sylan9bb 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( 0 <_ -u C <-> C < 0 ) )
235 ltnle 
 |-  ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
236 7 13 235 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( C < 0 <-> -. 0 <_ C ) )
237 236 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( C < 0 <-> -. 0 <_ C ) )
238 234 237 bitrd 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( 0 <_ -u C <-> -. 0 <_ C ) )
239 154 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( C + -u C ) = 0 )
240 73 addid1d 
 |-  ( ( ph /\ x e. A ) -> ( C + 0 ) = C )
241 240 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( C + 0 ) = C )
242 238 239 241 ifbieq12d 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> if ( 0 <_ -u C , ( C + -u C ) , ( C + 0 ) ) = if ( -. 0 <_ C , 0 , C ) )
243 ifnot 
 |-  if ( -. 0 <_ C , 0 , C ) = if ( 0 <_ C , C , 0 )
244 242 243 eqtrdi 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> if ( 0 <_ -u C , ( C + -u C ) , ( C + 0 ) ) = if ( 0 <_ C , C , 0 ) )
245 224 244 syl5eq 
 |-  ( ( ( ph /\ x e. A ) /\ C =/= 0 ) -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = if ( 0 <_ C , C , 0 ) )
246 223 245 pm2.61dane 
 |-  ( ( ph /\ x e. A ) -> ( C + if ( 0 <_ -u C , -u C , 0 ) ) = if ( 0 <_ C , C , 0 ) )
247 218 246 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( B + if ( 0 <_ -u B , -u B , 0 ) ) + ( C + if ( 0 <_ -u C , -u C , 0 ) ) ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
248 190 247 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( B + C ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
249 248 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( B + C ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) = ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
250 249 61 eqeltrd 
 |-  ( ph -> ( x e. A |-> ( ( B + C ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) e. MblFn )
251 5 29 171 42 250 mbfposadd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + if ( 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) , 0 ) ) ) e. MblFn )
252 189 251 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) e. MblFn )
253 max1 
 |-  ( ( 0 e. RR /\ ( B + C ) e. RR ) -> 0 <_ if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) )
254 13 29 253 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) )
255 40 178 42 181 252 40 42 254 186 itgaddnclem1 
 |-  ( ph -> S. A ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) _d x = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
256 46 177 255 3eqtr3d 
 |-  ( ph -> ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
257 35 50 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x e. CC )
258 15 53 18 56 61 15 18 64 66 itgaddnclem1 
 |-  ( ph -> S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) )
259 15 53 itgcl 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x e. CC )
260 18 56 itgcl 
 |-  ( ph -> S. A if ( 0 <_ C , C , 0 ) _d x e. CC )
261 259 260 addcld 
 |-  ( ph -> ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) e. CC )
262 258 261 eqeltrd 
 |-  ( ph -> S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x e. CC )
263 40 178 itgcl 
 |-  ( ph -> S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x e. CC )
264 22 179 26 180 171 22 26 183 185 itgaddnclem1 
 |-  ( ph -> S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x = ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) )
265 22 179 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x e. CC )
266 26 180 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u C , -u C , 0 ) _d x e. CC )
267 265 266 addcld 
 |-  ( ph -> ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) e. CC )
268 264 267 eqeltrd 
 |-  ( ph -> S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x e. CC )
269 257 262 263 268 addsubeq4d 
 |-  ( ph -> ( ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) <-> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) ) )
270 256 269 mpbid 
 |-  ( ph -> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
271 258 264 oveq12d 
 |-  ( ph -> ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) - ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
272 259 260 265 266 addsub4d 
 |-  ( ph -> ( ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) - ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
273 270 271 272 3eqtrd 
 |-  ( ph -> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
274 29 47 itgreval 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) )
275 6 2 itgreval 
 |-  ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )
276 7 4 itgreval 
 |-  ( ph -> S. A C _d x = ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) )
277 275 276 oveq12d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
278 273 274 277 3eqtr4d 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )