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
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( 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
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR ) |
51 |
4
|
ffvelrnda |
|- ( ( 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
|
ffvelrnd |
|- ( ( 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
|
ffvelrnd |
|- ( ( 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
|
ffvelrnd |
|- ( ( 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
|
ffvelrnd |
|- ( ( 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
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( 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 ) |