Metamath Proof Explorer

Theorem vonioolem1

Description: The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonioolem1.x 
|- ( ph -> X e. Fin )
vonioolem1.a 
|- ( ph -> A : X --> RR )
vonioolem1.b 
|- ( ph -> B : X --> RR )
vonioolem1.u 
|- ( ph -> X =/= (/) )
vonioolem1.t 
|- ( ( ph /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
vonioolem1.c 
|- C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
vonioolem1.d 
|- D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
vonioolem1.s 
|- S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
vonioolem1.r 
|- T = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
vonioolem1.e 
|- E = inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < )
vonioolem1.n 
|- N = ( ( |_ ` ( 1 / E ) ) + 1 )
vonioolem1.z 
|- Z = ( ZZ>= ` N )
Assertion vonioolem1 
|- ( ph -> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )

Proof

Step Hyp Ref Expression
1 vonioolem1.x 
 |-  ( ph -> X e. Fin )
2 vonioolem1.a 
 |-  ( ph -> A : X --> RR )
3 vonioolem1.b 
 |-  ( ph -> B : X --> RR )
4 vonioolem1.u 
 |-  ( ph -> X =/= (/) )
5 vonioolem1.t 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
6 vonioolem1.c 
 |-  C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
7 vonioolem1.d 
 |-  D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
8 vonioolem1.s 
 |-  S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
9 vonioolem1.r 
 |-  T = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
10 vonioolem1.e 
 |-  E = inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < )
11 vonioolem1.n 
 |-  N = ( ( |_ ` ( 1 / E ) ) + 1 )
12 vonioolem1.z 
 |-  Z = ( ZZ>= ` N )
13 9 a1i 
 |-  ( ph -> T = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) )
14 6 a1i 
 |-  ( ph -> C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) )
15 1 mptexd 
 |-  ( ph -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V )
16 15 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V )
17 14 16 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
18 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. _V )
19 17 18 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( A ` k ) + ( 1 / n ) ) )
20 19 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) - ( ( C ` n ) ` k ) ) = ( ( B ` k ) - ( ( A ` k ) + ( 1 / n ) ) ) )
21 3 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
22 21 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR )
23 22 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. CC )
24 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : X --> RR )
25 24 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR )
26 25 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. CC )
27 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
28 27 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
29 28 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. CC )
30 23 26 29 subsub4d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) = ( ( B ` k ) - ( ( A ` k ) + ( 1 / n ) ) ) )
31 20 30 eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) - ( ( C ` n ) ` k ) ) = ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) )
32 31 prodeq2dv 
 |-  ( ( ph /\ n e. NN ) -> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) = prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) )
33 32 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) )
34 13 33 eqtrd 
 |-  ( ph -> T = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) )
35 nfv 
 |-  F/ k ph
36 rpssre 
 |-  RR+ C_ RR
37 2 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
38 difrp 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
39 37 21 38 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
40 5 39 mpbid 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR+ )
41 36 40 sselid 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR )
42 41 recnd 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. CC )
43 eqid 
 |-  ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) )
44 35 1 42 43 fprodsubrecnncnv 
 |-  ( ph -> ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
45 34 44 eqbrtrd 
 |-  ( ph -> T ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
46 nnex 
 |-  NN e. _V
47 46 mptex 
 |-  ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) e. _V
48 47 a1i 
 |-  ( ph -> ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) e. _V )
49 9 48 eqeltrid 
 |-  ( ph -> T e. _V )
50 46 mptex 
 |-  ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) e. _V
51 50 a1i 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) e. _V )
52 8 51 eqeltrid 
 |-  ( ph -> S e. _V )
53 1rp 
 |-  1 e. RR+
54 53 a1i 
 |-  ( ph -> 1 e. RR+ )
55 eqid 
 |-  ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) = ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) )
56 35 55 40 rnmptssd 
 |-  ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR+ )
57 ltso 
 |-  < Or RR
58 57 a1i 
 |-  ( ph -> < Or RR )
59 55 rnmptfi 
 |-  ( X e. Fin -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin )
60 1 59 syl 
 |-  ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin )
61 35 40 55 4 rnmptn0 
 |-  ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) =/= (/) )
62 36 a1i 
 |-  ( ph -> RR+ C_ RR )
63 56 62 sstrd 
 |-  ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR )
64 fiinfcl 
 |-  ( ( < Or RR /\ ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) =/= (/) /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR ) ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
65 58 60 61 63 64 syl13anc 
 |-  ( ph -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
66 10 65 eqeltrid 
 |-  ( ph -> E e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
67 56 66 sseldd 
 |-  ( ph -> E e. RR+ )
68 54 67 rpdivcld 
 |-  ( ph -> ( 1 / E ) e. RR+ )
69 68 rpred 
 |-  ( ph -> ( 1 / E ) e. RR )
70 68 rpge0d 
 |-  ( ph -> 0 <_ ( 1 / E ) )
71 flge0nn0 
 |-  ( ( ( 1 / E ) e. RR /\ 0 <_ ( 1 / E ) ) -> ( |_ ` ( 1 / E ) ) e. NN0 )
72 69 70 71 syl2anc 
 |-  ( ph -> ( |_ ` ( 1 / E ) ) e. NN0 )
73 nn0p1nn 
 |-  ( ( |_ ` ( 1 / E ) ) e. NN0 -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. NN )
74 72 73 syl 
 |-  ( ph -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. NN )
75 74 nnzd 
 |-  ( ph -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. ZZ )
76 11 75 eqeltrid 
 |-  ( ph -> N e. ZZ )
77 11 recnnltrp 
 |-  ( E e. RR+ -> ( N e. NN /\ ( 1 / N ) < E ) )
78 67 77 syl 
 |-  ( ph -> ( N e. NN /\ ( 1 / N ) < E ) )
79 78 simpld 
 |-  ( ph -> N e. NN )
80 uznnssnn 
 |-  ( N e. NN -> ( ZZ>= ` N ) C_ NN )
81 79 80 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ NN )
82 12 81 eqsstrid 
 |-  ( ph -> Z C_ NN )
83 82 adantr 
 |-  ( ( ph /\ n e. Z ) -> Z C_ NN )
84 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
85 83 84 sseldd 
 |-  ( ( ph /\ n e. Z ) -> n e. NN )
86 7 a1i 
 |-  ( ph -> D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) )
87 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
88 eqid 
 |-  dom ( voln ` X ) = dom ( voln ` X )
89 25 28 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. RR )
90 89 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR )
91 17 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR <-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR ) )
92 90 91 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR )
93 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> B : X --> RR )
94 87 88 92 93 hoimbl 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. dom ( voln ` X ) )
95 94 elexd 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. _V )
96 86 95 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
97 85 96 syldan 
 |-  ( ( ph /\ n e. Z ) -> ( D ` n ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
98 97 fveq2d 
 |-  ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) = ( ( voln ` X ) ` X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) )
99 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> X e. Fin )
100 4 adantr 
 |-  ( ( ph /\ n e. Z ) -> X =/= (/) )
101 85 92 syldan 
 |-  ( ( ph /\ n e. Z ) -> ( C ` n ) : X --> RR )
102 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> B : X --> RR )
103 eqid 
 |-  X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) )
104 99 100 101 102 103 vonn0hoi 
 |-  ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) )
105 101 ffvelcdmda 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR )
106 85 22 syldanl 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( B ` k ) e. RR )
107 volico 
 |-  ( ( ( ( C ` n ) ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) )
108 105 106 107 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) )
109 85 19 syldanl 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( A ` k ) + ( 1 / n ) ) )
110 85 28 syldanl 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) e. RR )
111 79 nnrecred 
 |-  ( ph -> ( 1 / N ) e. RR )
112 111 ad2antrr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / N ) e. RR )
113 41 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR )
114 12 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` N ) )
115 114 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` N ) )
116 eluzle 
 |-  ( n e. ( ZZ>= ` N ) -> N <_ n )
117 115 116 syl 
 |-  ( n e. Z -> N <_ n )
118 117 adantl 
 |-  ( ( ph /\ n e. Z ) -> N <_ n )
119 79 nnrpd 
 |-  ( ph -> N e. RR+ )
120 119 adantr 
 |-  ( ( ph /\ n e. Z ) -> N e. RR+ )
121 nnrp 
 |-  ( n e. NN -> n e. RR+ )
122 85 121 syl 
 |-  ( ( ph /\ n e. Z ) -> n e. RR+ )
123 120 122 lerecd 
 |-  ( ( ph /\ n e. Z ) -> ( N <_ n <-> ( 1 / n ) <_ ( 1 / N ) ) )
124 118 123 mpbid 
 |-  ( ( ph /\ n e. Z ) -> ( 1 / n ) <_ ( 1 / N ) )
125 124 adantr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) <_ ( 1 / N ) )
126 111 adantr 
 |-  ( ( ph /\ k e. X ) -> ( 1 / N ) e. RR )
127 36 67 sselid 
 |-  ( ph -> E e. RR )
128 127 adantr 
 |-  ( ( ph /\ k e. X ) -> E e. RR )
129 78 simprd 
 |-  ( ph -> ( 1 / N ) < E )
130 129 adantr 
 |-  ( ( ph /\ k e. X ) -> ( 1 / N ) < E )
131 63 adantr 
 |-  ( ( ph /\ k e. X ) -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR )
132 60 adantr 
 |-  ( ( ph /\ k e. X ) -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin )
133 id 
 |-  ( k e. X -> k e. X )
134 ovexd 
 |-  ( k e. X -> ( ( B ` k ) - ( A ` k ) ) e. _V )
135 55 elrnmpt1 
 |-  ( ( k e. X /\ ( ( B ` k ) - ( A ` k ) ) e. _V ) -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
136 133 134 135 syl2anc 
 |-  ( k e. X -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
137 136 adantl 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) )
138 infrefilb 
 |-  ( ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin /\ ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) <_ ( ( B ` k ) - ( A ` k ) ) )
139 131 132 137 138 syl3anc 
 |-  ( ( ph /\ k e. X ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) <_ ( ( B ` k ) - ( A ` k ) ) )
140 10 139 eqbrtrid 
 |-  ( ( ph /\ k e. X ) -> E <_ ( ( B ` k ) - ( A ` k ) ) )
141 126 128 41 130 140 ltletrd 
 |-  ( ( ph /\ k e. X ) -> ( 1 / N ) < ( ( B ` k ) - ( A ` k ) ) )
142 141 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / N ) < ( ( B ` k ) - ( A ` k ) ) )
143 110 112 113 125 142 lelttrd 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) < ( ( B ` k ) - ( A ` k ) ) )
144 85 25 syldanl 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( A ` k ) e. RR )
145 144 110 106 ltaddsub2d 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( ( A ` k ) + ( 1 / n ) ) < ( B ` k ) <-> ( 1 / n ) < ( ( B ` k ) - ( A ` k ) ) ) )
146 143 145 mpbird 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) < ( B ` k ) )
147 109 146 eqbrtrd 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) < ( B ` k ) )
148 147 iftrued 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) = ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
149 108 148 eqtrd 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
150 149 prodeq2dv 
 |-  ( ( ph /\ n e. Z ) -> prod_ k e. X ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
151 98 104 150 3eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
152 fvexd 
 |-  ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) e. _V )
153 8 fvmpt2 
 |-  ( ( n e. NN /\ ( ( voln ` X ) ` ( D ` n ) ) e. _V ) -> ( S ` n ) = ( ( voln ` X ) ` ( D ` n ) ) )
154 85 152 153 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( S ` n ) = ( ( voln ` X ) ` ( D ` n ) ) )
155 prodex 
 |-  prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V
156 155 a1i 
 |-  ( ( ph /\ n e. Z ) -> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V )
157 9 fvmpt2 
 |-  ( ( n e. NN /\ prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V ) -> ( T ` n ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
158 85 156 157 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( T ` n ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
159 151 154 158 3eqtr4rd 
 |-  ( ( ph /\ n e. Z ) -> ( T ` n ) = ( S ` n ) )
160 12 49 52 76 159 climeq 
 |-  ( ph -> ( T ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) <-> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) )
161 45 160 mpbid 
 |-  ( ph -> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )