Metamath Proof Explorer

Theorem hoidmv1lelem2

Description: This is the contradiction proven in step (c) in the proof of Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem2.a 
|- ( ph -> A e. RR )
hoidmv1lelem2.b 
|- ( ph -> B e. RR )
hoidmv1lelem2.c 
|- ( ph -> C : NN --> RR )
hoidmv1lelem2.d 
|- ( ph -> D : NN --> RR )
hoidmv1lelem2.r 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )
hoidmv1lelem2.u 
|- U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }
hoidmv1lelem2.e 
|- ( ph -> S e. U )
hoidmv1lelem2.g 
|- ( ph -> A <_ S )
hoidmv1lelem2.l 
|- ( ph -> S < B )
hoidmv1lelem2.k 
|- ( ph -> K e. NN )
hoidmv1lelem2.s 
|- ( ph -> S e. ( ( C ` K ) [,) ( D ` K ) ) )
hoidmv1lelem2.m 
|- M = if ( ( D ` K ) <_ B , ( D ` K ) , B )
Assertion hoidmv1lelem2 
|- ( ph -> E. u e. U S < u )

Proof

Step Hyp Ref Expression
1 hoidmv1lelem2.a 
 |-  ( ph -> A e. RR )
2 hoidmv1lelem2.b 
 |-  ( ph -> B e. RR )
3 hoidmv1lelem2.c 
 |-  ( ph -> C : NN --> RR )
4 hoidmv1lelem2.d 
 |-  ( ph -> D : NN --> RR )
5 hoidmv1lelem2.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )
6 hoidmv1lelem2.u 
 |-  U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }
7 hoidmv1lelem2.e 
 |-  ( ph -> S e. U )
8 hoidmv1lelem2.g 
 |-  ( ph -> A <_ S )
9 hoidmv1lelem2.l 
 |-  ( ph -> S < B )
10 hoidmv1lelem2.k 
 |-  ( ph -> K e. NN )
11 hoidmv1lelem2.s 
 |-  ( ph -> S e. ( ( C ` K ) [,) ( D ` K ) ) )
12 hoidmv1lelem2.m 
 |-  M = if ( ( D ` K ) <_ B , ( D ` K ) , B )
13 12 a1i 
 |-  ( ph -> M = if ( ( D ` K ) <_ B , ( D ` K ) , B ) )
14 4 10 ffvelcdmd 
 |-  ( ph -> ( D ` K ) e. RR )
15 14 2 ifcld 
 |-  ( ph -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) e. RR )
16 13 15 eqeltrd 
 |-  ( ph -> M e. RR )
17 3 10 ffvelcdmd 
 |-  ( ph -> ( C ` K ) e. RR )
18 14 rexrd 
 |-  ( ph -> ( D ` K ) e. RR* )
19 icossre 
 |-  ( ( ( C ` K ) e. RR /\ ( D ` K ) e. RR* ) -> ( ( C ` K ) [,) ( D ` K ) ) C_ RR )
20 17 18 19 syl2anc 
 |-  ( ph -> ( ( C ` K ) [,) ( D ` K ) ) C_ RR )
21 20 11 sseldd 
 |-  ( ph -> S e. RR )
22 17 rexrd 
 |-  ( ph -> ( C ` K ) e. RR* )
23 icoltub 
 |-  ( ( ( C ` K ) e. RR* /\ ( D ` K ) e. RR* /\ S e. ( ( C ` K ) [,) ( D ` K ) ) ) -> S < ( D ` K ) )
24 22 18 11 23 syl3anc 
 |-  ( ph -> S < ( D ` K ) )
25 21 14 24 ltled 
 |-  ( ph -> S <_ ( D ` K ) )
26 21 2 9 ltled 
 |-  ( ph -> S <_ B )
27 25 26 jca 
 |-  ( ph -> ( S <_ ( D ` K ) /\ S <_ B ) )
28 lemin 
 |-  ( ( S e. RR /\ ( D ` K ) e. RR /\ B e. RR ) -> ( S <_ if ( ( D ` K ) <_ B , ( D ` K ) , B ) <-> ( S <_ ( D ` K ) /\ S <_ B ) ) )
29 21 14 2 28 syl3anc 
 |-  ( ph -> ( S <_ if ( ( D ` K ) <_ B , ( D ` K ) , B ) <-> ( S <_ ( D ` K ) /\ S <_ B ) ) )
30 27 29 mpbird 
 |-  ( ph -> S <_ if ( ( D ` K ) <_ B , ( D ` K ) , B ) )
31 1 21 15 8 30 letrd 
 |-  ( ph -> A <_ if ( ( D ` K ) <_ B , ( D ` K ) , B ) )
32 13 eqcomd 
 |-  ( ph -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) = M )
33 31 32 breqtrd 
 |-  ( ph -> A <_ M )
34 min2 
 |-  ( ( ( D ` K ) e. RR /\ B e. RR ) -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) <_ B )
35 14 2 34 syl2anc 
 |-  ( ph -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) <_ B )
36 13 35 eqbrtrd 
 |-  ( ph -> M <_ B )
37 1 2 16 33 36 eliccd 
 |-  ( ph -> M e. ( A [,] B ) )
38 16 recnd 
 |-  ( ph -> M e. CC )
39 21 recnd 
 |-  ( ph -> S e. CC )
40 1 recnd 
 |-  ( ph -> A e. CC )
41 38 39 40 npncand 
 |-  ( ph -> ( ( M - S ) + ( S - A ) ) = ( M - A ) )
42 41 eqcomd 
 |-  ( ph -> ( M - A ) = ( ( M - S ) + ( S - A ) ) )
43 16 21 resubcld 
 |-  ( ph -> ( M - S ) e. RR )
44 21 1 resubcld 
 |-  ( ph -> ( S - A ) e. RR )
45 43 44 readdcld 
 |-  ( ph -> ( ( M - S ) + ( S - A ) ) e. RR )
46 nnex 
 |-  NN e. _V
47 46 a1i 
 |-  ( ph -> NN e. _V )
48 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
49 48 a1i 
 |-  ( ( ph /\ j e. NN ) -> vol : dom vol --> ( 0 [,] +oo ) )
50 3 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR )
51 4 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR )
52 21 adantr 
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
53 51 52 ifcld 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR )
54 53 rexrd 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* )
55 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
56 50 54 55 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
57 49 56 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) e. ( 0 [,] +oo ) )
58 eqid 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
59 57 58 fmptd 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) : NN --> ( 0 [,] +oo ) )
60 47 59 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR* )
61 pnfxr 
 |-  +oo e. RR*
62 61 a1i 
 |-  ( ph -> +oo e. RR* )
63 5 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR* )
64 nfv 
 |-  F/ j ph
65 51 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR* )
66 icombl 
 |-  ( ( ( C ` j ) e. RR /\ ( D ` j ) e. RR* ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
67 50 65 66 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
68 49 67 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) e. ( 0 [,] +oo ) )
69 50 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR* )
70 50 leidd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) <_ ( C ` j ) )
71 min1 
 |-  ( ( ( D ` j ) e. RR /\ S e. RR ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) )
72 51 52 71 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) )
73 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ ( D ` j ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
74 69 65 70 72 73 syl22anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
75 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol /\ ( ( C ` j ) [,) ( D ` j ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
76 56 67 74 75 syl3anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
77 64 47 57 68 76 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
78 5 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) < +oo )
79 60 63 62 77 78 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) < +oo )
80 60 62 79 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) =/= +oo )
81 80 neneqd 
 |-  ( ph -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = +oo )
82 47 59 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = +oo ) )
83 81 82 mpbird 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR )
84 43 83 readdcld 
 |-  ( ph -> ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) e. RR )
85 16 adantr 
 |-  ( ( ph /\ j e. NN ) -> M e. RR )
86 51 85 ifcld 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR )
87 86 rexrd 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR* )
88 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) e. dom vol )
89 50 87 88 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) e. dom vol )
90 49 89 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) e. ( 0 [,] +oo ) )
91 eqid 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) )
92 90 91 fmptd 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) : NN --> ( 0 [,] +oo ) )
93 47 92 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR* )
94 min1 
 |-  ( ( ( D ` j ) e. RR /\ M e. RR ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) <_ ( D ` j ) )
95 51 85 94 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) <_ ( D ` j ) )
96 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ ( D ` j ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ M , ( D ` j ) , M ) <_ ( D ` j ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
97 69 65 70 95 96 syl22anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
98 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) e. dom vol /\ ( ( C ` j ) [,) ( D ` j ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
99 89 67 97 98 syl3anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
100 64 47 90 68 99 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
101 93 63 62 100 78 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) < +oo )
102 93 62 101 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) =/= +oo )
103 102 neneqd 
 |-  ( ph -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = +oo )
104 47 92 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = +oo ) )
105 103 104 mpbird 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR )
106 7 6 eleqtrdi 
 |-  ( ph -> S e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
107 oveq1 
 |-  ( z = S -> ( z - A ) = ( S - A ) )
108 simpl 
 |-  ( ( z = S /\ j e. NN ) -> z = S )
109 108 breq2d 
 |-  ( ( z = S /\ j e. NN ) -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ S ) )
110 109 108 ifbieq2d 
 |-  ( ( z = S /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
111 110 oveq2d 
 |-  ( ( z = S /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) )
112 111 fveq2d 
 |-  ( ( z = S /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
113 112 mpteq2dva 
 |-  ( z = S -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) )
114 113 fveq2d 
 |-  ( z = S -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
115 107 114 breq12d 
 |-  ( z = S -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
116 115 elrab 
 |-  ( S e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } <-> ( S e. ( A [,] B ) /\ ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
117 106 116 sylib 
 |-  ( ph -> ( S e. ( A [,] B ) /\ ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
118 117 simprd 
 |-  ( ph -> ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
119 44 83 43 118 leadd2dd 
 |-  ( ph -> ( ( M - S ) + ( S - A ) ) <_ ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
120 difssd 
 |-  ( ph -> ( NN \ { K } ) C_ NN )
121 64 47 57 83 120 sge0ssrempt 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR )
122 difexg 
 |-  ( NN e. _V -> ( NN \ { K } ) e. _V )
123 46 122 ax-mp 
 |-  ( NN \ { K } ) e. _V
124 123 a1i 
 |-  ( ph -> ( NN \ { K } ) e. _V )
125 48 a1i 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> vol : dom vol --> ( 0 [,] +oo ) )
126 simpl 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ph )
127 eldifi 
 |-  ( j e. ( NN \ { K } ) -> j e. NN )
128 127 adantl 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> j e. NN )
129 126 128 50 syl2anc 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( C ` j ) e. RR )
130 128 87 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR* )
131 129 130 88 syl2anc 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) e. dom vol )
132 125 131 ffvelcdmd 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) e. ( 0 [,] +oo ) )
133 64 124 132 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR* )
134 47 90 120 sge0lessmpt 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
135 133 93 62 134 101 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) < +oo )
136 133 62 135 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) =/= +oo )
137 136 neneqd 
 |-  ( ph -> -. ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = +oo )
138 64 124 132 sge0repnfmpt 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = +oo ) )
139 137 138 mpbird 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR )
140 16 17 resubcld 
 |-  ( ph -> ( M - ( C ` K ) ) e. RR )
141 128 57 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) e. ( 0 [,] +oo ) )
142 128 56 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
143 128 69 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( C ` j ) e. RR* )
144 128 70 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( C ` j ) <_ ( C ` j ) )
145 iftrue 
 |-  ( ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
146 145 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
147 51 leidd 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) <_ ( D ` j ) )
148 147 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) <_ ( D ` j ) )
149 51 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) e. RR )
150 85 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> M e. RR )
151 52 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> S e. RR )
152 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) <_ S )
153 24 9 jca 
 |-  ( ph -> ( S < ( D ` K ) /\ S < B ) )
154 ltmin 
 |-  ( ( S e. RR /\ ( D ` K ) e. RR /\ B e. RR ) -> ( S < if ( ( D ` K ) <_ B , ( D ` K ) , B ) <-> ( S < ( D ` K ) /\ S < B ) ) )
155 21 14 2 154 syl3anc 
 |-  ( ph -> ( S < if ( ( D ` K ) <_ B , ( D ` K ) , B ) <-> ( S < ( D ` K ) /\ S < B ) ) )
156 153 155 mpbird 
 |-  ( ph -> S < if ( ( D ` K ) <_ B , ( D ` K ) , B ) )
157 156 32 breqtrd 
 |-  ( ph -> S < M )
158 157 ad2antrr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> S < M )
159 149 151 150 152 158 lelttrd 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) < M )
160 149 150 159 ltled 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) <_ M )
161 148 160 jca 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( ( D ` j ) <_ ( D ` j ) /\ ( D ` j ) <_ M ) )
162 lemin 
 |-  ( ( ( D ` j ) e. RR /\ ( D ` j ) e. RR /\ M e. RR ) -> ( ( D ` j ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) <-> ( ( D ` j ) <_ ( D ` j ) /\ ( D ` j ) <_ M ) ) )
163 149 149 150 162 syl3anc 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( ( D ` j ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) <-> ( ( D ` j ) <_ ( D ` j ) /\ ( D ` j ) <_ M ) ) )
164 161 163 mpbird 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> ( D ` j ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
165 146 164 eqbrtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
166 iffalse 
 |-  ( -. ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
167 166 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
168 52 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> S e. RR )
169 86 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR )
170 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> -. ( D ` j ) <_ S )
171 51 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> ( D ` j ) e. RR )
172 168 171 ltnled 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> ( S < ( D ` j ) <-> -. ( D ` j ) <_ S ) )
173 170 172 mpbird 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> S < ( D ` j ) )
174 157 ad2antrr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> S < M )
175 173 174 jca 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> ( S < ( D ` j ) /\ S < M ) )
176 85 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> M e. RR )
177 ltmin 
 |-  ( ( S e. RR /\ ( D ` j ) e. RR /\ M e. RR ) -> ( S < if ( ( D ` j ) <_ M , ( D ` j ) , M ) <-> ( S < ( D ` j ) /\ S < M ) ) )
178 168 171 176 177 syl3anc 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> ( S < if ( ( D ` j ) <_ M , ( D ` j ) , M ) <-> ( S < ( D ` j ) /\ S < M ) ) )
179 175 178 mpbird 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> S < if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
180 168 169 179 ltled 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> S <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
181 167 180 eqbrtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
182 165 181 pm2.61dan 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
183 128 182 syldan 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
184 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ if ( ( D ` j ) <_ M , ( D ` j ) , M ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) )
185 143 130 144 183 184 syl22anc 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) )
186 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) )
187 142 131 185 186 syl3anc 
 |-  ( ( ph /\ j e. ( NN \ { K } ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) )
188 64 124 141 132 187 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) <_ ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
189 121 139 140 188 leadd2dd 
 |-  ( ph -> ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) <_ ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
190 difsnid 
 |-  ( K e. NN -> ( ( NN \ { K } ) u. { K } ) = NN )
191 10 190 syl 
 |-  ( ph -> ( ( NN \ { K } ) u. { K } ) = NN )
192 191 eqcomd 
 |-  ( ph -> NN = ( ( NN \ { K } ) u. { K } ) )
193 192 mpteq1d 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) = ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) )
194 193 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = ( sum^ ` ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
195 neldifsnd 
 |-  ( ph -> -. K e. ( NN \ { K } ) )
196 fveq2 
 |-  ( j = K -> ( C ` j ) = ( C ` K ) )
197 fveq2 
 |-  ( j = K -> ( D ` j ) = ( D ` K ) )
198 197 breq1d 
 |-  ( j = K -> ( ( D ` j ) <_ S <-> ( D ` K ) <_ S ) )
199 198 197 ifbieq1d 
 |-  ( j = K -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = if ( ( D ` K ) <_ S , ( D ` K ) , S ) )
200 196 199 oveq12d 
 |-  ( j = K -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) = ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) )
201 200 fveq2d 
 |-  ( j = K -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) = ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) )
202 48 a1i 
 |-  ( ph -> vol : dom vol --> ( 0 [,] +oo ) )
203 14 21 ifcld 
 |-  ( ph -> if ( ( D ` K ) <_ S , ( D ` K ) , S ) e. RR )
204 203 rexrd 
 |-  ( ph -> if ( ( D ` K ) <_ S , ( D ` K ) , S ) e. RR* )
205 icombl 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ S , ( D ` K ) , S ) e. RR* ) -> ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) e. dom vol )
206 17 204 205 syl2anc 
 |-  ( ph -> ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) e. dom vol )
207 202 206 ffvelcdmd 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) e. ( 0 [,] +oo ) )
208 64 124 10 195 141 201 207 sge0splitsn 
 |-  ( ph -> ( sum^ ` ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) )
209 volicore 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ S , ( D ` K ) , S ) e. RR ) -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) e. RR )
210 17 203 209 syl2anc 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) e. RR )
211 rexadd 
 |-  ( ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR /\ ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) e. RR ) -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) )
212 121 210 211 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) )
213 volico 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ S , ( D ` K ) , S ) e. RR ) -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) = if ( ( C ` K ) < if ( ( D ` K ) <_ S , ( D ` K ) , S ) , ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) , 0 ) )
214 17 203 213 syl2anc 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) = if ( ( C ` K ) < if ( ( D ` K ) <_ S , ( D ` K ) , S ) , ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) , 0 ) )
215 21 14 ltnled 
 |-  ( ph -> ( S < ( D ` K ) <-> -. ( D ` K ) <_ S ) )
216 24 215 mpbid 
 |-  ( ph -> -. ( D ` K ) <_ S )
217 216 iffalsed 
 |-  ( ph -> if ( ( D ` K ) <_ S , ( D ` K ) , S ) = S )
218 217 breq2d 
 |-  ( ph -> ( ( C ` K ) < if ( ( D ` K ) <_ S , ( D ` K ) , S ) <-> ( C ` K ) < S ) )
219 218 ifbid 
 |-  ( ph -> if ( ( C ` K ) < if ( ( D ` K ) <_ S , ( D ` K ) , S ) , ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) , 0 ) = if ( ( C ` K ) < S , ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) , 0 ) )
220 217 oveq1d 
 |-  ( ph -> ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) = ( S - ( C ` K ) ) )
221 220 adantr 
 |-  ( ( ph /\ ( C ` K ) < S ) -> ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) = ( S - ( C ` K ) ) )
222 217 204 eqeltrrd 
 |-  ( ph -> S e. RR* )
223 222 adantr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> S e. RR* )
224 22 adantr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( C ` K ) e. RR* )
225 simpr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> -. ( C ` K ) < S )
226 21 adantr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> S e. RR )
227 17 adantr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( C ` K ) e. RR )
228 226 227 lenltd 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( S <_ ( C ` K ) <-> -. ( C ` K ) < S ) )
229 225 228 mpbird 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> S <_ ( C ` K ) )
230 icogelb 
 |-  ( ( ( C ` K ) e. RR* /\ ( D ` K ) e. RR* /\ S e. ( ( C ` K ) [,) ( D ` K ) ) ) -> ( C ` K ) <_ S )
231 22 18 11 230 syl3anc 
 |-  ( ph -> ( C ` K ) <_ S )
232 231 adantr 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( C ` K ) <_ S )
233 223 224 229 232 xrletrid 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> S = ( C ` K ) )
234 233 oveq1d 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( S - ( C ` K ) ) = ( ( C ` K ) - ( C ` K ) ) )
235 227 recnd 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( C ` K ) e. CC )
236 235 subidd 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> ( ( C ` K ) - ( C ` K ) ) = 0 )
237 234 236 eqtr2d 
 |-  ( ( ph /\ -. ( C ` K ) < S ) -> 0 = ( S - ( C ` K ) ) )
238 221 237 ifeqda 
 |-  ( ph -> if ( ( C ` K ) < S , ( if ( ( D ` K ) <_ S , ( D ` K ) , S ) - ( C ` K ) ) , 0 ) = ( S - ( C ` K ) ) )
239 214 219 238 3eqtrd 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) = ( S - ( C ` K ) ) )
240 239 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + ( S - ( C ` K ) ) ) )
241 121 recnd 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. CC )
242 17 recnd 
 |-  ( ph -> ( C ` K ) e. CC )
243 39 242 subcld 
 |-  ( ph -> ( S - ( C ` K ) ) e. CC )
244 241 243 addcomd 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + ( S - ( C ` K ) ) ) = ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
245 212 240 244 3eqtrd 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ S , ( D ` K ) , S ) ) ) ) = ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
246 194 208 245 3eqtrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
247 246 oveq2d 
 |-  ( ph -> ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) = ( ( M - S ) + ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) ) )
248 43 recnd 
 |-  ( ph -> ( M - S ) e. CC )
249 248 243 241 addassd 
 |-  ( ph -> ( ( ( M - S ) + ( S - ( C ` K ) ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) = ( ( M - S ) + ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) ) )
250 249 eqcomd 
 |-  ( ph -> ( ( M - S ) + ( ( S - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) ) = ( ( ( M - S ) + ( S - ( C ` K ) ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
251 38 39 242 npncand 
 |-  ( ph -> ( ( M - S ) + ( S - ( C ` K ) ) ) = ( M - ( C ` K ) ) )
252 251 oveq1d 
 |-  ( ph -> ( ( ( M - S ) + ( S - ( C ` K ) ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) = ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
253 247 250 252 3eqtrd 
 |-  ( ph -> ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) = ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
254 192 mpteq1d 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) = ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) )
255 254 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = ( sum^ ` ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
256 197 breq1d 
 |-  ( j = K -> ( ( D ` j ) <_ M <-> ( D ` K ) <_ M ) )
257 256 197 ifbieq1d 
 |-  ( j = K -> if ( ( D ` j ) <_ M , ( D ` j ) , M ) = if ( ( D ` K ) <_ M , ( D ` K ) , M ) )
258 196 257 oveq12d 
 |-  ( j = K -> ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) = ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) )
259 258 fveq2d 
 |-  ( j = K -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) = ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) )
260 14 16 ifcld 
 |-  ( ph -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) e. RR )
261 260 rexrd 
 |-  ( ph -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) e. RR* )
262 icombl 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ M , ( D ` K ) , M ) e. RR* ) -> ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) e. dom vol )
263 17 261 262 syl2anc 
 |-  ( ph -> ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) e. dom vol )
264 202 263 ffvelcdmd 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) e. ( 0 [,] +oo ) )
265 64 124 10 195 132 259 264 sge0splitsn 
 |-  ( ph -> ( sum^ ` ( j e. ( ( NN \ { K } ) u. { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) )
266 volicore 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ M , ( D ` K ) , M ) e. RR ) -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) e. RR )
267 17 260 266 syl2anc 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) e. RR )
268 rexadd 
 |-  ( ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. RR /\ ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) e. RR ) -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) )
269 139 267 268 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) )
270 volico 
 |-  ( ( ( C ` K ) e. RR /\ if ( ( D ` K ) <_ M , ( D ` K ) , M ) e. RR ) -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) = if ( ( C ` K ) < if ( ( D ` K ) <_ M , ( D ` K ) , M ) , ( if ( ( D ` K ) <_ M , ( D ` K ) , M ) - ( C ` K ) ) , 0 ) )
271 17 260 270 syl2anc 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) = if ( ( C ` K ) < if ( ( D ` K ) <_ M , ( D ` K ) , M ) , ( if ( ( D ` K ) <_ M , ( D ` K ) , M ) - ( C ` K ) ) , 0 ) )
272 24 157 jca 
 |-  ( ph -> ( S < ( D ` K ) /\ S < M ) )
273 ltmin 
 |-  ( ( S e. RR /\ ( D ` K ) e. RR /\ M e. RR ) -> ( S < if ( ( D ` K ) <_ M , ( D ` K ) , M ) <-> ( S < ( D ` K ) /\ S < M ) ) )
274 21 14 16 273 syl3anc 
 |-  ( ph -> ( S < if ( ( D ` K ) <_ M , ( D ` K ) , M ) <-> ( S < ( D ` K ) /\ S < M ) ) )
275 272 274 mpbird 
 |-  ( ph -> S < if ( ( D ` K ) <_ M , ( D ` K ) , M ) )
276 17 21 260 231 275 lelttrd 
 |-  ( ph -> ( C ` K ) < if ( ( D ` K ) <_ M , ( D ` K ) , M ) )
277 276 iftrued 
 |-  ( ph -> if ( ( C ` K ) < if ( ( D ` K ) <_ M , ( D ` K ) , M ) , ( if ( ( D ` K ) <_ M , ( D ` K ) , M ) - ( C ` K ) ) , 0 ) = ( if ( ( D ` K ) <_ M , ( D ` K ) , M ) - ( C ` K ) ) )
278 iftrue 
 |-  ( ( D ` K ) <_ M -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) = ( D ` K ) )
279 278 adantl 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) = ( D ` K ) )
280 18 adantr 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> ( D ` K ) e. RR* )
281 16 rexrd 
 |-  ( ph -> M e. RR* )
282 281 adantr 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> M e. RR* )
283 simpr 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> ( D ` K ) <_ M )
284 min1 
 |-  ( ( ( D ` K ) e. RR /\ B e. RR ) -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) <_ ( D ` K ) )
285 14 2 284 syl2anc 
 |-  ( ph -> if ( ( D ` K ) <_ B , ( D ` K ) , B ) <_ ( D ` K ) )
286 13 285 eqbrtrd 
 |-  ( ph -> M <_ ( D ` K ) )
287 286 adantr 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> M <_ ( D ` K ) )
288 280 282 283 287 xrletrid 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> ( D ` K ) = M )
289 279 288 eqtrd 
 |-  ( ( ph /\ ( D ` K ) <_ M ) -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) = M )
290 simpr 
 |-  ( ( ph /\ -. ( D ` K ) <_ M ) -> -. ( D ` K ) <_ M )
291 290 iffalsed 
 |-  ( ( ph /\ -. ( D ` K ) <_ M ) -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) = M )
292 289 291 pm2.61dan 
 |-  ( ph -> if ( ( D ` K ) <_ M , ( D ` K ) , M ) = M )
293 292 oveq1d 
 |-  ( ph -> ( if ( ( D ` K ) <_ M , ( D ` K ) , M ) - ( C ` K ) ) = ( M - ( C ` K ) ) )
294 271 277 293 3eqtrd 
 |-  ( ph -> ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) = ( M - ( C ` K ) ) )
295 294 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) + ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) = ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) + ( M - ( C ` K ) ) ) )
296 139 recnd 
 |-  ( ph -> ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) e. CC )
297 38 242 subcld 
 |-  ( ph -> ( M - ( C ` K ) ) e. CC )
298 296 297 addcomd 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) + ( M - ( C ` K ) ) ) = ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
299 269 295 298 3eqtrd 
 |-  ( ph -> ( ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) +e ( vol ` ( ( C ` K ) [,) if ( ( D ` K ) <_ M , ( D ` K ) , M ) ) ) ) = ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
300 255 265 299 3eqtrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) = ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
301 253 300 breq12d 
 |-  ( ph -> ( ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) <-> ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) <_ ( ( M - ( C ` K ) ) + ( sum^ ` ( j e. ( NN \ { K } ) |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) ) )
302 189 301 mpbird 
 |-  ( ph -> ( ( M - S ) + ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
303 45 84 105 119 302 letrd 
 |-  ( ph -> ( ( M - S ) + ( S - A ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
304 42 303 eqbrtrd 
 |-  ( ph -> ( M - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
305 37 304 jca 
 |-  ( ph -> ( M e. ( A [,] B ) /\ ( M - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
306 oveq1 
 |-  ( z = M -> ( z - A ) = ( M - A ) )
307 breq2 
 |-  ( z = M -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ M ) )
308 id 
 |-  ( z = M -> z = M )
309 307 308 ifbieq2d 
 |-  ( z = M -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ M , ( D ` j ) , M ) )
310 309 oveq2d 
 |-  ( z = M -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) )
311 310 fveq2d 
 |-  ( z = M -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) )
312 311 mpteq2dv 
 |-  ( z = M -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) )
313 312 fveq2d 
 |-  ( z = M -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) )
314 306 313 breq12d 
 |-  ( z = M -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( M - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
315 314 elrab 
 |-  ( M e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } <-> ( M e. ( A [,] B ) /\ ( M - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ M , ( D ` j ) , M ) ) ) ) ) ) )
316 305 315 sylibr 
 |-  ( ph -> M e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
317 316 6 eleqtrrdi 
 |-  ( ph -> M e. U )
318 272 simprd 
 |-  ( ph -> S < M )
319 breq2 
 |-  ( u = M -> ( S < u <-> S < M ) )
320 319 rspcev 
 |-  ( ( M e. U /\ S < M ) -> E. u e. U S < u )
321 317 318 320 syl2anc 
 |-  ( ph -> E. u e. U S < u )