Metamath Proof Explorer

Theorem itgle

Description: Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgle.1 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgle.2 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
itgle.3 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgle.4 
|- ( ( ph /\ x e. A ) -> C e. RR )
itgle.5 
|- ( ( ph /\ x e. A ) -> B <_ C )
Assertion itgle 
|- ( ph -> S. A B _d x <_ S. A C _d x )

Proof

Step Hyp Ref Expression
1 itgle.1 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
2 itgle.2 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
3 itgle.3 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 itgle.4 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
5 itgle.5 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
6 3 iblrelem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) ) )
7 1 6 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) )
8 7 simp2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
9 4 iblrelem 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) e. RR ) ) )
10 2 9 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) e. RR ) )
11 10 simp3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) e. RR )
12 10 simp2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
13 7 simp3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR )
14 3 ad2ant2r 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ B ) ) -> B e. RR )
15 14 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ B ) ) -> B e. RR* )
16 simprr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ B ) ) -> 0 <_ B )
17 elxrge0 
 |-  ( B e. ( 0 [,] +oo ) <-> ( B e. RR* /\ 0 <_ B ) )
18 15 16 17 sylanbrc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ B ) ) -> B e. ( 0 [,] +oo ) )
19 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
20 19 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( x e. A /\ 0 <_ B ) ) -> 0 e. ( 0 [,] +oo ) )
21 18 20 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,] +oo ) )
22 21 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) : RR --> ( 0 [,] +oo ) )
23 4 ad2ant2r 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ C ) ) -> C e. RR )
24 23 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ C ) ) -> C e. RR* )
25 simprr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ C ) ) -> 0 <_ C )
26 elxrge0 
 |-  ( C e. ( 0 [,] +oo ) <-> ( C e. RR* /\ 0 <_ C ) )
27 24 25 26 sylanbrc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ C ) ) -> C e. ( 0 [,] +oo ) )
28 19 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( x e. A /\ 0 <_ C ) ) -> 0 e. ( 0 [,] +oo ) )
29 27 28 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,] +oo ) )
30 29 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) : RR --> ( 0 [,] +oo ) )
31 0re 
 |-  0 e. RR
32 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
33 31 4 32 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
34 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
35 4 31 34 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
36 max2 
 |-  ( ( 0 e. RR /\ C e. RR ) -> C <_ if ( 0 <_ C , C , 0 ) )
37 31 4 36 sylancr 
 |-  ( ( ph /\ x e. A ) -> C <_ if ( 0 <_ C , C , 0 ) )
38 3 4 35 5 37 letrd 
 |-  ( ( ph /\ x e. A ) -> B <_ if ( 0 <_ C , C , 0 ) )
39 maxle 
 |-  ( ( 0 e. RR /\ B e. RR /\ if ( 0 <_ C , C , 0 ) e. RR ) -> ( if ( 0 <_ B , B , 0 ) <_ if ( 0 <_ C , C , 0 ) <-> ( 0 <_ if ( 0 <_ C , C , 0 ) /\ B <_ if ( 0 <_ C , C , 0 ) ) ) )
40 31 3 35 39 mp3an2i 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) <_ if ( 0 <_ C , C , 0 ) <-> ( 0 <_ if ( 0 <_ C , C , 0 ) /\ B <_ if ( 0 <_ C , C , 0 ) ) ) )
41 33 38 40 mpbir2and 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) <_ if ( 0 <_ C , C , 0 ) )
42 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) = if ( 0 <_ B , B , 0 ) )
43 42 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) = if ( 0 <_ B , B , 0 ) )
44 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) = if ( 0 <_ C , C , 0 ) )
45 44 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) = if ( 0 <_ C , C , 0 ) )
46 41 43 45 3brtr4d 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) )
47 46 ex 
 |-  ( ph -> ( x e. A -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) ) )
48 0le0 
 |-  0 <_ 0
49 48 a1i 
 |-  ( -. x e. A -> 0 <_ 0 )
50 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) = 0 )
51 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) = 0 )
52 49 50 51 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) )
53 47 52 pm2.61d1 
 |-  ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) )
54 ifan 
 |-  if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
55 ifan 
 |-  if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 )
56 53 54 55 3brtr4g 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) <_ if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
57 56 ralrimivw 
 |-  ( ph -> A. x e. RR if ( ( x e. A /\ 0 <_ B ) , B , 0 ) <_ if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
58 reex 
 |-  RR e. _V
59 58 a1i 
 |-  ( ph -> RR e. _V )
60 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) )
61 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
62 59 21 29 60 61 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ B ) , B , 0 ) <_ if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
63 57 62 mpbird 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
64 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) )
65 22 30 63 64 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) )
66 4 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. RR )
67 66 ad2ant2r 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u C ) ) -> -u C e. RR )
68 67 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u C ) ) -> -u C e. RR* )
69 simprr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u C ) ) -> 0 <_ -u C )
70 elxrge0 
 |-  ( -u C e. ( 0 [,] +oo ) <-> ( -u C e. RR* /\ 0 <_ -u C ) )
71 68 69 70 sylanbrc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u C ) ) -> -u C e. ( 0 [,] +oo ) )
72 19 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( x e. A /\ 0 <_ -u C ) ) -> 0 e. ( 0 [,] +oo ) )
73 71 72 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) e. ( 0 [,] +oo ) )
74 73 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) : RR --> ( 0 [,] +oo ) )
75 3 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
76 75 ad2ant2r 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B e. RR )
77 76 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B e. RR* )
78 simprr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u B ) ) -> 0 <_ -u B )
79 elxrge0 
 |-  ( -u B e. ( 0 [,] +oo ) <-> ( -u B e. RR* /\ 0 <_ -u B ) )
80 77 78 79 sylanbrc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B e. ( 0 [,] +oo ) )
81 19 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. ( x e. A /\ 0 <_ -u B ) ) -> 0 e. ( 0 [,] +oo ) )
82 80 81 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) e. ( 0 [,] +oo ) )
83 82 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) : RR --> ( 0 [,] +oo ) )
84 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
85 31 75 84 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
86 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
87 75 31 86 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
88 3 4 lenegd 
 |-  ( ( ph /\ x e. A ) -> ( B <_ C <-> -u C <_ -u B ) )
89 5 88 mpbid 
 |-  ( ( ph /\ x e. A ) -> -u C <_ -u B )
90 max2 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> -u B <_ if ( 0 <_ -u B , -u B , 0 ) )
91 31 75 90 sylancr 
 |-  ( ( ph /\ x e. A ) -> -u B <_ if ( 0 <_ -u B , -u B , 0 ) )
92 66 75 87 89 91 letrd 
 |-  ( ( ph /\ x e. A ) -> -u C <_ if ( 0 <_ -u B , -u B , 0 ) )
93 maxle 
 |-  ( ( 0 e. RR /\ -u C e. RR /\ if ( 0 <_ -u B , -u B , 0 ) e. RR ) -> ( if ( 0 <_ -u C , -u C , 0 ) <_ if ( 0 <_ -u B , -u B , 0 ) <-> ( 0 <_ if ( 0 <_ -u B , -u B , 0 ) /\ -u C <_ if ( 0 <_ -u B , -u B , 0 ) ) ) )
94 31 66 87 93 mp3an2i 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) <_ if ( 0 <_ -u B , -u B , 0 ) <-> ( 0 <_ if ( 0 <_ -u B , -u B , 0 ) /\ -u C <_ if ( 0 <_ -u B , -u B , 0 ) ) ) )
95 85 92 94 mpbir2and 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) <_ if ( 0 <_ -u B , -u B , 0 ) )
96 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) = if ( 0 <_ -u C , -u C , 0 ) )
97 96 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) = if ( 0 <_ -u C , -u C , 0 ) )
98 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) = if ( 0 <_ -u B , -u B , 0 ) )
99 98 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) = if ( 0 <_ -u B , -u B , 0 ) )
100 95 97 99 3brtr4d 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) )
101 100 ex 
 |-  ( ph -> ( x e. A -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) )
102 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) = 0 )
103 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) = 0 )
104 49 102 103 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) )
105 101 104 pm2.61d1 
 |-  ( ph -> if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 ) <_ if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) )
106 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) = if ( x e. A , if ( 0 <_ -u C , -u C , 0 ) , 0 )
107 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 )
108 105 106 107 3brtr4g 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) <_ if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) )
109 108 ralrimivw 
 |-  ( ph -> A. x e. RR if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) <_ if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) )
110 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) )
111 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) )
112 59 73 82 110 111 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) <_ if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) )
113 109 112 mpbird 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) )
114 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) )
115 74 83 113 114 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) )
116 8 11 12 13 65 115 le2subd 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) ) <_ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) ) )
117 3 1 itgrevallem1 
 |-  ( ph -> S. A B _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) ) )
118 4 2 itgrevallem1 
 |-  ( ph -> S. A C _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u C ) , -u C , 0 ) ) ) ) )
119 116 117 118 3brtr4d 
 |-  ( ph -> S. A B _d x <_ S. A C _d x )