Metamath Proof Explorer

Theorem ibladdnclem

Description: Lemma for ibladdnc ; cf ibladdlem , whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc . (Contributed by Brendan Leahy, 31-Oct-2017)

Ref Expression
Hypotheses ibladdnclem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
ibladdnclem.2 
|- ( ( ph /\ x e. A ) -> C e. RR )
ibladdnclem.3 
|- ( ( ph /\ x e. A ) -> D = ( B + C ) )
ibladdnclem.4 
|- ( ph -> ( x e. A |-> B ) e. MblFn )
ibladdnclem.6 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
ibladdnclem.7 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
Assertion ibladdnclem 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 ibladdnclem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 ibladdnclem.2 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
3 ibladdnclem.3 
 |-  ( ( ph /\ x e. A ) -> D = ( B + C ) )
4 ibladdnclem.4 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
5 ibladdnclem.6 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
6 ibladdnclem.7 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )
7 ifan 
 |-  if ( ( x e. A /\ 0 <_ D ) , D , 0 ) = if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 )
8 1 2 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
9 3 8 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> D e. RR )
10 0re 
 |-  0 e. RR
11 ifcl 
 |-  ( ( D e. RR /\ 0 e. RR ) -> if ( 0 <_ D , D , 0 ) e. RR )
12 9 10 11 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR )
13 12 rexrd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. RR* )
14 max1 
 |-  ( ( 0 e. RR /\ D e. RR ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
15 10 9 14 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ D , D , 0 ) )
16 elxrge0 
 |-  ( if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ D , D , 0 ) e. RR* /\ 0 <_ if ( 0 <_ D , D , 0 ) ) )
17 13 15 16 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) e. ( 0 [,] +oo ) )
18 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
19 18 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
20 17 19 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
21 20 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) e. ( 0 [,] +oo ) )
22 7 21 eqeltrid 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) e. ( 0 [,] +oo ) )
23 22 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) )
24 reex 
 |-  RR e. _V
25 24 a1i 
 |-  ( ph -> RR e. _V )
26 ifan 
 |-  if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
27 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
28 1 10 27 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
29 10 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. RR )
30 28 29 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. RR )
31 26 30 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
32 31 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
33 ifan 
 |-  if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 )
34 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
35 2 10 34 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
36 35 29 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. RR )
37 33 36 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
38 37 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. RR )
39 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) )
40 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
41 25 32 38 39 40 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) )
42 iftrue 
 |-  ( x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
43 ibar 
 |-  ( x e. A -> ( 0 <_ B <-> ( x e. A /\ 0 <_ B ) ) )
44 43 ifbid 
 |-  ( x e. A -> if ( 0 <_ B , B , 0 ) = if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
45 ibar 
 |-  ( x e. A -> ( 0 <_ C <-> ( x e. A /\ 0 <_ C ) ) )
46 45 ifbid 
 |-  ( x e. A -> if ( 0 <_ C , C , 0 ) = if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
47 44 46 oveq12d 
 |-  ( x e. A -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) )
48 42 47 eqtr2d 
 |-  ( x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
49 00id 
 |-  ( 0 + 0 ) = 0
50 simpl 
 |-  ( ( x e. A /\ 0 <_ B ) -> x e. A )
51 50 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ B ) )
52 51 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
53 simpl 
 |-  ( ( x e. A /\ 0 <_ C ) -> x e. A )
54 53 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ C ) )
55 54 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) = 0 )
56 52 55 oveq12d 
 |-  ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = ( 0 + 0 ) )
57 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = 0 )
58 49 56 57 3eqtr4a 
 |-  ( -. x e. A -> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
59 48 58 pm2.61i 
 |-  ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) = if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 )
60 59 mpteq2i 
 |-  ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ B ) , B , 0 ) + if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
61 41 60 eqtrdi 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
62 61 fveq2d 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
63 4 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
64 mblss 
 |-  ( A e. dom vol -> A C_ RR )
65 63 64 syl 
 |-  ( ph -> A C_ RR )
66 rembl 
 |-  RR e. dom vol
67 66 a1i 
 |-  ( ph -> RR e. dom vol )
68 31 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. RR )
69 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
70 69 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
71 70 intnanrd 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. ( x e. A /\ 0 <_ B ) )
72 71 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
73 44 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
74 1 4 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
75 73 74 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
76 65 67 68 72 75 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) e. MblFn )
77 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
78 10 1 77 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
79 elrege0 
 |-  ( if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ 0 <_ if ( 0 <_ B , B , 0 ) ) )
80 28 78 79 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. ( 0 [,) +oo ) )
81 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
82 81 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
83 80 82 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) e. ( 0 [,) +oo ) )
84 26 83 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
85 84 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) e. ( 0 [,) +oo ) )
86 85 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
87 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
88 10 2 87 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
89 elrege0 
 |-  ( if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ C , C , 0 ) e. RR /\ 0 <_ if ( 0 <_ C , C , 0 ) ) )
90 35 88 89 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. ( 0 [,) +oo ) )
91 90 82 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ C , C , 0 ) , 0 ) e. ( 0 [,) +oo ) )
92 33 91 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
93 92 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) e. ( 0 [,) +oo ) )
94 93 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) : RR --> ( 0 [,) +oo ) )
95 76 86 5 94 6 itg2addnc 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) oF + ( 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 ) ) ) ) )
96 62 95 eqtr3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 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 ) ) ) ) )
97 5 6 readdcld 
 |-  ( 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 ) ) ) ) e. RR )
98 96 97 eqeltrd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR )
99 28 35 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
100 99 rexrd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* )
101 28 35 78 88 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
102 elxrge0 
 |-  ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) <-> ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR* /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
103 100 101 102 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. ( 0 [,] +oo ) )
104 103 19 ifclda 
 |-  ( ph -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
105 104 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) e. ( 0 [,] +oo ) )
106 105 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
107 max2 
 |-  ( ( 0 e. RR /\ B e. RR ) -> B <_ if ( 0 <_ B , B , 0 ) )
108 10 1 107 sylancr 
 |-  ( ( ph /\ x e. A ) -> B <_ if ( 0 <_ B , B , 0 ) )
109 max2 
 |-  ( ( 0 e. RR /\ C e. RR ) -> C <_ if ( 0 <_ C , C , 0 ) )
110 10 2 109 sylancr 
 |-  ( ( ph /\ x e. A ) -> C <_ if ( 0 <_ C , C , 0 ) )
111 1 2 28 35 108 110 le2addd 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
112 3 111 eqbrtrd 
 |-  ( ( ph /\ x e. A ) -> D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
113 breq1 
 |-  ( D = if ( 0 <_ D , D , 0 ) -> ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
114 breq1 
 |-  ( 0 = if ( 0 <_ D , D , 0 ) -> ( 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
115 113 114 ifboth 
 |-  ( ( D <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) /\ 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
116 112 101 115 syl2anc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ D , D , 0 ) <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
117 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
118 117 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = if ( 0 <_ D , D , 0 ) )
119 42 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
120 116 118 119 3brtr4d 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
121 120 ex 
 |-  ( ph -> ( x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
122 0le0 
 |-  0 <_ 0
123 122 a1i 
 |-  ( -. x e. A -> 0 <_ 0 )
124 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) = 0 )
125 123 124 57 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
126 121 125 pm2.61d1 
 |-  ( ph -> if ( x e. A , if ( 0 <_ D , D , 0 ) , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
127 7 126 eqbrtrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
128 127 ralrimivw 
 |-  ( ph -> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) )
129 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) )
130 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
131 25 22 105 129 130 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ D ) , D , 0 ) <_ if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
132 128 131 mpbird 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) )
133 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
134 23 106 132 133 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) )
135 itg2lecl 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )
136 23 98 134 135 syl3anc 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )