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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( ( 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 ffvelrnda
 |-  ( ( 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 sseldi
 |-  ( ( 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 ffvelrnda
 |-  ( ( ( 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 sseldi
 |-  ( 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 ) ) )