Metamath Proof Explorer

Theorem vonicclem2

Description: The n-dimensional Lebesgue measure of closed intervals. This is the second statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonicclem2.x 
|- ( ph -> X e. Fin )
vonicclem2.a 
|- ( ph -> A : X --> RR )
vonicclem2.b 
|- ( ph -> B : X --> RR )
vonicclem2.n 
|- ( ph -> X =/= (/) )
vonicclem2.t 
|- ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( B ` k ) )
vonicclem2.i 
|- I = X_ k e. X ( ( A ` k ) [,] ( B ` k ) )
vonicclem2.c 
|- C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
vonicclem2.d 
|- D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
Assertion vonicclem2 
|- ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )

Proof

Step Hyp Ref Expression
1 vonicclem2.x 
 |-  ( ph -> X e. Fin )
2 vonicclem2.a 
 |-  ( ph -> A : X --> RR )
3 vonicclem2.b 
 |-  ( ph -> B : X --> RR )
4 vonicclem2.n 
 |-  ( ph -> X =/= (/) )
5 vonicclem2.t 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( B ` k ) )
6 vonicclem2.i 
 |-  I = X_ k e. X ( ( A ` k ) [,] ( B ` k ) )
7 vonicclem2.c 
 |-  C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
8 vonicclem2.d 
 |-  D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
9 nfv 
 |-  F/ n ph
10 1 vonmea 
 |-  ( ph -> ( voln ` X ) e. Meas )
11 1zzd 
 |-  ( ph -> 1 e. ZZ )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
14 eqid 
 |-  dom ( voln ` X ) = dom ( voln ` X )
15 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : X --> RR )
16 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
17 16 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR )
18 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
19 18 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
20 17 19 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / n ) ) e. RR )
21 20 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) : X --> RR )
22 7 a1i 
 |-  ( ph -> C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) ) )
23 1 mptexd 
 |-  ( ph -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) e. _V )
24 23 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) e. _V )
25 22 24 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) = ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
26 25 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR <-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) : X --> RR ) )
27 21 26 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR )
28 13 14 15 27 hoimbl 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) e. dom ( voln ` X ) )
29 28 8 fmptd 
 |-  ( ph -> D : NN --> dom ( voln ` X ) )
30 nfv 
 |-  F/ k ( ph /\ n e. NN )
31 ressxr 
 |-  RR C_ RR*
32 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
33 31 32 sselid 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
34 33 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR* )
35 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / n ) ) e. _V )
36 25 35 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( B ` k ) + ( 1 / n ) ) )
37 36 20 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR )
38 37 rexrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR* )
39 15 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR )
40 39 leidd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) <_ ( A ` k ) )
41 1red 
 |-  ( n e. NN -> 1 e. RR )
42 nnre 
 |-  ( n e. NN -> n e. RR )
43 42 41 readdcld 
 |-  ( n e. NN -> ( n + 1 ) e. RR )
44 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
45 nnne0 
 |-  ( ( n + 1 ) e. NN -> ( n + 1 ) =/= 0 )
46 44 45 syl 
 |-  ( n e. NN -> ( n + 1 ) =/= 0 )
47 41 43 46 redivcld 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) e. RR )
48 47 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / ( n + 1 ) ) e. RR )
49 42 ltp1d 
 |-  ( n e. NN -> n < ( n + 1 ) )
50 nnrp 
 |-  ( n e. NN -> n e. RR+ )
51 44 nnrpd 
 |-  ( n e. NN -> ( n + 1 ) e. RR+ )
52 50 51 ltrecd 
 |-  ( n e. NN -> ( n < ( n + 1 ) <-> ( 1 / ( n + 1 ) ) < ( 1 / n ) ) )
53 49 52 mpbid 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) < ( 1 / n ) )
54 47 18 53 ltled 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) <_ ( 1 / n ) )
55 54 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / ( n + 1 ) ) <_ ( 1 / n ) )
56 48 19 17 55 leadd2dd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) <_ ( ( B ` k ) + ( 1 / n ) ) )
57 oveq2 
 |-  ( n = m -> ( 1 / n ) = ( 1 / m ) )
58 57 oveq2d 
 |-  ( n = m -> ( ( B ` k ) + ( 1 / n ) ) = ( ( B ` k ) + ( 1 / m ) ) )
59 58 mpteq2dv 
 |-  ( n = m -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) = ( k e. X |-> ( ( B ` k ) + ( 1 / m ) ) ) )
60 59 cbvmptv 
 |-  ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) ) = ( m e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / m ) ) ) )
61 7 60 eqtri 
 |-  C = ( m e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / m ) ) ) )
62 oveq2 
 |-  ( m = ( n + 1 ) -> ( 1 / m ) = ( 1 / ( n + 1 ) ) )
63 62 oveq2d 
 |-  ( m = ( n + 1 ) -> ( ( B ` k ) + ( 1 / m ) ) = ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) )
64 63 mpteq2dv 
 |-  ( m = ( n + 1 ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) ) )
65 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
66 65 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
67 13 mptexd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) ) e. _V )
68 61 64 66 67 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( C ` ( n + 1 ) ) = ( k e. X |-> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) ) )
69 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) e. _V )
70 68 69 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) = ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) )
71 70 36 breq12d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) <-> ( ( B ` k ) + ( 1 / ( n + 1 ) ) ) <_ ( ( B ` k ) + ( 1 / n ) ) ) )
72 56 71 mpbird 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) )
73 icossico 
 |-  ( ( ( ( A ` k ) e. RR* /\ ( ( C ` n ) ` k ) e. RR* ) /\ ( ( A ` k ) <_ ( A ` k ) /\ ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) ) ) -> ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) C_ ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
74 34 38 40 72 73 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) C_ ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
75 30 74 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) C_ X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
76 fveq2 
 |-  ( n = m -> ( C ` n ) = ( C ` m ) )
77 76 fveq1d 
 |-  ( n = m -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) )
78 77 oveq2d 
 |-  ( n = m -> ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) )
79 78 ixpeq2dv 
 |-  ( n = m -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) )
80 79 cbvmptv 
 |-  ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = ( m e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) )
81 8 80 eqtri 
 |-  D = ( m e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) )
82 fveq2 
 |-  ( m = ( n + 1 ) -> ( C ` m ) = ( C ` ( n + 1 ) ) )
83 82 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( C ` m ) ` k ) = ( ( C ` ( n + 1 ) ) ` k ) )
84 83 oveq2d 
 |-  ( m = ( n + 1 ) -> ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) = ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) )
85 84 ixpeq2dv 
 |-  ( m = ( n + 1 ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` m ) ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) )
86 ovex 
 |-  ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V
87 86 rgenw 
 |-  A. k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V
88 ixpexg 
 |-  ( A. k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V -> X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V )
89 87 88 ax-mp 
 |-  X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V
90 89 a1i 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) e. _V )
91 81 85 66 90 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( D ` ( n + 1 ) ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) )
92 8 a1i 
 |-  ( ph -> D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) )
93 28 elexd 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) e. _V )
94 92 93 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
95 91 94 sseq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` ( n + 1 ) ) C_ ( D ` n ) <-> X_ k e. X ( ( A ` k ) [,) ( ( C ` ( n + 1 ) ) ` k ) ) C_ X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) )
96 75 95 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( D ` ( n + 1 ) ) C_ ( D ` n ) )
97 1nn 
 |-  1 e. NN
98 97 12 eleqtri 
 |-  1 e. ( ZZ>= ` 1 )
99 98 a1i 
 |-  ( ph -> 1 e. ( ZZ>= ` 1 ) )
100 fveq2 
 |-  ( n = 1 -> ( C ` n ) = ( C ` 1 ) )
101 100 fveq1d 
 |-  ( n = 1 -> ( ( C ` n ) ` k ) = ( ( C ` 1 ) ` k ) )
102 101 oveq2d 
 |-  ( n = 1 -> ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) )
103 102 ixpeq2dv 
 |-  ( n = 1 -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) )
104 97 a1i 
 |-  ( ph -> 1 e. NN )
105 ovex 
 |-  ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V
106 105 rgenw 
 |-  A. k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V
107 ixpexg 
 |-  ( A. k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V -> X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V )
108 106 107 ax-mp 
 |-  X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V
109 108 a1i 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) e. _V )
110 8 103 104 109 fvmptd3 
 |-  ( ph -> ( D ` 1 ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) )
111 110 fveq2d 
 |-  ( ph -> ( ( voln ` X ) ` ( D ` 1 ) ) = ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) ) )
112 nfv 
 |-  F/ k ph
113 simpl 
 |-  ( ( ph /\ k e. X ) -> ph )
114 97 a1i 
 |-  ( ( ph /\ k e. X ) -> 1 e. NN )
115 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
116 97 elexi 
 |-  1 e. _V
117 eleq1 
 |-  ( n = 1 -> ( n e. NN <-> 1 e. NN ) )
118 117 anbi2d 
 |-  ( n = 1 -> ( ( ph /\ n e. NN ) <-> ( ph /\ 1 e. NN ) ) )
119 118 anbi1d 
 |-  ( n = 1 -> ( ( ( ph /\ n e. NN ) /\ k e. X ) <-> ( ( ph /\ 1 e. NN ) /\ k e. X ) ) )
120 101 eleq1d 
 |-  ( n = 1 -> ( ( ( C ` n ) ` k ) e. RR <-> ( ( C ` 1 ) ` k ) e. RR ) )
121 119 120 imbi12d 
 |-  ( n = 1 -> ( ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR ) <-> ( ( ( ph /\ 1 e. NN ) /\ k e. X ) -> ( ( C ` 1 ) ` k ) e. RR ) ) )
122 116 121 37 vtocl 
 |-  ( ( ( ph /\ 1 e. NN ) /\ k e. X ) -> ( ( C ` 1 ) ` k ) e. RR )
123 113 114 115 122 syl21anc 
 |-  ( ( ph /\ k e. X ) -> ( ( C ` 1 ) ` k ) e. RR )
124 112 1 32 123 vonhoire 
 |-  ( ph -> ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,) ( ( C ` 1 ) ` k ) ) ) e. RR )
125 111 124 eqeltrd 
 |-  ( ph -> ( ( voln ` X ) ` ( D ` 1 ) ) e. RR )
126 eqid 
 |-  ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
127 9 10 11 12 29 96 99 125 126 meaiininc 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> ( ( voln ` X ) ` |^|_ n e. NN ( D ` n ) ) )
128 112 32 16 iinhoiicc 
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( ( A ` k ) [,) ( ( B ` k ) + ( 1 / n ) ) ) = X_ k e. X ( ( A ` k ) [,] ( B ` k ) ) )
129 36 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = ( ( A ` k ) [,) ( ( B ` k ) + ( 1 / n ) ) ) )
130 129 ixpeq2dva 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( ( B ` k ) + ( 1 / n ) ) ) )
131 94 130 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( A ` k ) [,) ( ( B ` k ) + ( 1 / n ) ) ) )
132 131 iineq2dv 
 |-  ( ph -> |^|_ n e. NN ( D ` n ) = |^|_ n e. NN X_ k e. X ( ( A ` k ) [,) ( ( B ` k ) + ( 1 / n ) ) ) )
133 6 a1i 
 |-  ( ph -> I = X_ k e. X ( ( A ` k ) [,] ( B ` k ) ) )
134 128 132 133 3eqtr4d 
 |-  ( ph -> |^|_ n e. NN ( D ` n ) = I )
135 134 eqcomd 
 |-  ( ph -> I = |^|_ n e. NN ( D ` n ) )
136 135 fveq2d 
 |-  ( ph -> ( ( voln ` X ) ` I ) = ( ( voln ` X ) ` |^|_ n e. NN ( D ` n ) ) )
137 136 eqcomd 
 |-  ( ph -> ( ( voln ` X ) ` |^|_ n e. NN ( D ` n ) ) = ( ( voln ` X ) ` I ) )
138 127 137 breqtrd 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> ( ( voln ` X ) ` I ) )
139 2fveq3 
 |-  ( n = m -> ( ( voln ` X ) ` ( D ` n ) ) = ( ( voln ` X ) ` ( D ` m ) ) )
140 139 cbvmptv 
 |-  ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) )
141 140 a1i 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) )
142 140 eqcomi 
 |-  ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
143 1 2 3 4 5 7 8 142 vonicclem1 
 |-  ( ph -> ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
144 141 143 eqbrtrd 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
145 climuni 
 |-  ( ( ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> ( ( voln ` X ) ` I ) /\ ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
146 138 144 145 syl2anc 
 |-  ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )