Metamath Proof Explorer

Theorem vonioolem2

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

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

Proof

Step Hyp Ref Expression
1 vonioolem2.x 
 |-  ( ph -> X e. Fin )
2 vonioolem2.a 
 |-  ( ph -> A : X --> RR )
3 vonioolem2.b 
 |-  ( ph -> B : X --> RR )
4 vonioolem2.n 
 |-  ( ph -> X =/= (/) )
5 vonioolem2.t 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
6 vonioolem2.i 
 |-  I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) )
7 vonioolem2.c 
 |-  C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
8 vonioolem2.d 
 |-  D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
9 1 vonmea 
 |-  ( ph -> ( voln ` X ) e. Meas )
10 1zzd 
 |-  ( ph -> 1 e. ZZ )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
13 eqid 
 |-  dom ( voln ` X ) = dom ( voln ` X )
14 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : X --> RR )
15 14 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR )
16 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
17 16 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
18 15 17 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. RR )
19 18 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR )
20 7 a1i 
 |-  ( ph -> C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) )
21 1 mptexd 
 |-  ( ph -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V )
22 21 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V )
23 20 22 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
24 23 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR <-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR ) )
25 19 24 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR )
26 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> B : X --> RR )
27 12 13 25 26 hoimbl 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. dom ( voln ` X ) )
28 27 8 fmptd 
 |-  ( ph -> D : NN --> dom ( voln ` X ) )
29 nfv 
 |-  F/ k ( ph /\ n e. NN )
30 oveq2 
 |-  ( n = m -> ( 1 / n ) = ( 1 / m ) )
31 30 oveq2d 
 |-  ( n = m -> ( ( A ` k ) + ( 1 / n ) ) = ( ( A ` k ) + ( 1 / m ) ) )
32 31 mpteq2dv 
 |-  ( n = m -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) )
33 32 cbvmptv 
 |-  ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) = ( m e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) )
34 7 33 eqtri 
 |-  C = ( m e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) )
35 oveq2 
 |-  ( m = ( n + 1 ) -> ( 1 / m ) = ( 1 / ( n + 1 ) ) )
36 35 oveq2d 
 |-  ( m = ( n + 1 ) -> ( ( A ` k ) + ( 1 / m ) ) = ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) )
37 36 mpteq2dv 
 |-  ( m = ( n + 1 ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) ) )
38 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
39 38 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
40 12 mptexd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) ) e. _V )
41 34 37 39 40 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( C ` ( n + 1 ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) ) )
42 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) e. _V )
43 41 42 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) = ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) )
44 1red 
 |-  ( n e. NN -> 1 e. RR )
45 nnre 
 |-  ( n e. NN -> n e. RR )
46 45 44 readdcld 
 |-  ( n e. NN -> ( n + 1 ) e. RR )
47 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
48 nnne0 
 |-  ( ( n + 1 ) e. NN -> ( n + 1 ) =/= 0 )
49 47 48 syl 
 |-  ( n e. NN -> ( n + 1 ) =/= 0 )
50 44 46 49 redivcld 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) e. RR )
51 50 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / ( n + 1 ) ) e. RR )
52 15 51 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) e. RR )
53 43 52 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) e. RR )
54 53 rexrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) e. RR* )
55 ressxr 
 |-  RR C_ RR*
56 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
57 55 56 sseldi 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
58 57 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR* )
59 45 ltp1d 
 |-  ( n e. NN -> n < ( n + 1 ) )
60 nnrp 
 |-  ( n e. NN -> n e. RR+ )
61 47 nnrpd 
 |-  ( n e. NN -> ( n + 1 ) e. RR+ )
62 60 61 ltrecd 
 |-  ( n e. NN -> ( n < ( n + 1 ) <-> ( 1 / ( n + 1 ) ) < ( 1 / n ) ) )
63 59 62 mpbid 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) < ( 1 / n ) )
64 50 16 63 ltled 
 |-  ( n e. NN -> ( 1 / ( n + 1 ) ) <_ ( 1 / n ) )
65 64 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / ( n + 1 ) ) <_ ( 1 / n ) )
66 51 17 15 65 leadd2dd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) <_ ( ( A ` k ) + ( 1 / n ) ) )
67 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. _V )
68 23 67 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( A ` k ) + ( 1 / n ) ) )
69 43 68 breq12d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) <-> ( ( A ` k ) + ( 1 / ( n + 1 ) ) ) <_ ( ( A ` k ) + ( 1 / n ) ) ) )
70 66 69 mpbird 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) )
71 56 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR )
72 eqidd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) = ( B ` k ) )
73 71 72 eqled 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) <_ ( B ` k ) )
74 icossico 
 |-  ( ( ( ( ( C ` ( n + 1 ) ) ` k ) e. RR* /\ ( B ` k ) e. RR* ) /\ ( ( ( C ` ( n + 1 ) ) ` k ) <_ ( ( C ` n ) ` k ) /\ ( B ` k ) <_ ( B ` k ) ) ) -> ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) C_ ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
75 54 58 70 73 74 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) C_ ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
76 29 75 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) C_ X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
77 8 a1i 
 |-  ( ph -> D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) )
78 27 elexd 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. _V )
79 77 78 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) )
80 fveq2 
 |-  ( n = m -> ( C ` n ) = ( C ` m ) )
81 80 fveq1d 
 |-  ( n = m -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) )
82 81 oveq1d 
 |-  ( n = m -> ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) )
83 82 ixpeq2dv 
 |-  ( n = m -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) )
84 83 cbvmptv 
 |-  ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = ( m e. NN |-> X_ k e. X ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) )
85 8 84 eqtri 
 |-  D = ( m e. NN |-> X_ k e. X ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) )
86 fveq2 
 |-  ( m = ( n + 1 ) -> ( C ` m ) = ( C ` ( n + 1 ) ) )
87 86 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( C ` m ) ` k ) = ( ( C ` ( n + 1 ) ) ` k ) )
88 87 oveq1d 
 |-  ( m = ( n + 1 ) -> ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) = ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
89 88 ixpeq2dv 
 |-  ( m = ( n + 1 ) -> X_ k e. X ( ( ( C ` m ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
90 ovex 
 |-  ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V
91 90 rgenw 
 |-  A. k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V
92 ixpexg 
 |-  ( A. k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V -> X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V )
93 91 92 ax-mp 
 |-  X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V
94 93 a1i 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) e. _V )
95 85 89 39 94 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( D ` ( n + 1 ) ) = X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) )
96 79 95 sseq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) C_ ( D ` ( n + 1 ) ) <-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) C_ X_ k e. X ( ( ( C ` ( n + 1 ) ) ` k ) [,) ( B ` k ) ) ) )
97 76 96 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) C_ ( D ` ( n + 1 ) ) )
98 1 13 2 3 hoimbl 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) e. dom ( voln ` X ) )
99 nfv 
 |-  F/ k ph
100 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
101 99 1 100 56 vonhoire 
 |-  ( ph -> ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
102 6 a1i 
 |-  ( ph -> I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
103 nftru 
 |-  F/ k T.
104 ioossico 
 |-  ( ( A ` k ) (,) ( B ` k ) ) C_ ( ( A ` k ) [,) ( B ` k ) )
105 104 a1i 
 |-  ( ( T. /\ k e. X ) -> ( ( A ` k ) (,) ( B ` k ) ) C_ ( ( A ` k ) [,) ( B ` k ) ) )
106 103 105 ixpssixp 
 |-  ( T. -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) C_ X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
107 106 mptru 
 |-  X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) C_ X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
108 107 a1i 
 |-  ( ph -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) C_ X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
109 102 108 eqsstrd 
 |-  ( ph -> I C_ X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
110 55 a1i 
 |-  ( ph -> RR C_ RR* )
111 2 110 fssd 
 |-  ( ph -> A : X --> RR* )
112 3 110 fssd 
 |-  ( ph -> B : X --> RR* )
113 1 13 111 112 ioovonmbl 
 |-  ( ph -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) e. dom ( voln ` X ) )
114 6 113 eqeltrid 
 |-  ( ph -> I e. dom ( voln ` X ) )
115 9 98 101 109 114 meassre 
 |-  ( ph -> ( ( voln ` X ) ` I ) e. RR )
116 9 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( voln ` X ) e. Meas )
117 79 27 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) e. dom ( voln ` X ) )
118 114 adantr 
 |-  ( ( ph /\ n e. NN ) -> I e. dom ( voln ` X ) )
119 55 100 sseldi 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
120 119 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR* )
121 60 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
122 121 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR+ )
123 15 122 ltaddrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) < ( ( A ` k ) + ( 1 / n ) ) )
124 icossioo 
 |-  ( ( ( ( A ` k ) e. RR* /\ ( B ` k ) e. RR* ) /\ ( ( A ` k ) < ( ( A ` k ) + ( 1 / n ) ) /\ ( B ` k ) <_ ( B ` k ) ) ) -> ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) C_ ( ( A ` k ) (,) ( B ` k ) ) )
125 120 58 123 73 124 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) C_ ( ( A ` k ) (,) ( B ` k ) ) )
126 29 125 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) C_ X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
127 68 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) )
128 127 ixpeq2dva 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) )
129 79 128 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) )
130 6 a1i 
 |-  ( ( ph /\ n e. NN ) -> I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
131 129 130 sseq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) C_ I <-> X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) C_ X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) ) )
132 126 131 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) C_ I )
133 116 13 117 118 132 meassle 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln ` X ) ` ( D ` n ) ) <_ ( ( voln ` X ) ` I ) )
134 eqid 
 |-  ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
135 9 10 11 28 97 115 133 134 meaiuninc2 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> ( ( voln ` X ) ` U_ n e. NN ( D ` n ) ) )
136 99 1 100 57 iunhoiioo 
 |-  ( ph -> U_ n e. NN X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
137 129 iuneq2dv 
 |-  ( ph -> U_ n e. NN ( D ` n ) = U_ n e. NN X_ k e. X ( ( ( A ` k ) + ( 1 / n ) ) [,) ( B ` k ) ) )
138 136 137 102 3eqtr4d 
 |-  ( ph -> U_ n e. NN ( D ` n ) = I )
139 138 eqcomd 
 |-  ( ph -> I = U_ n e. NN ( D ` n ) )
140 139 fveq2d 
 |-  ( ph -> ( ( voln ` X ) ` I ) = ( ( voln ` X ) ` U_ n e. NN ( D ` n ) ) )
141 140 eqcomd 
 |-  ( ph -> ( ( voln ` X ) ` U_ n e. NN ( D ` n ) ) = ( ( voln ` X ) ` I ) )
142 135 141 breqtrd 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> ( ( voln ` X ) ` I ) )
143 2fveq3 
 |-  ( n = m -> ( ( voln ` X ) ` ( D ` n ) ) = ( ( voln ` X ) ` ( D ` m ) ) )
144 143 cbvmptv 
 |-  ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) )
145 144 a1i 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) )
146 144 eqcomi 
 |-  ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
147 eqcom 
 |-  ( n = m <-> m = n )
148 147 imbi1i 
 |-  ( ( n = m -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) ) <-> ( m = n -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) ) )
149 eqcom 
 |-  ( ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) <-> ( ( C ` m ) ` k ) = ( ( C ` n ) ` k ) )
150 149 imbi2i 
 |-  ( ( m = n -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) ) <-> ( m = n -> ( ( C ` m ) ` k ) = ( ( C ` n ) ` k ) ) )
151 148 150 bitri 
 |-  ( ( n = m -> ( ( C ` n ) ` k ) = ( ( C ` m ) ` k ) ) <-> ( m = n -> ( ( C ` m ) ` k ) = ( ( C ` n ) ` k ) ) )
152 81 151 mpbi 
 |-  ( m = n -> ( ( C ` m ) ` k ) = ( ( C ` n ) ` k ) )
153 152 oveq2d 
 |-  ( m = n -> ( ( B ` k ) - ( ( C ` m ) ` k ) ) = ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
154 153 prodeq2ad 
 |-  ( m = n -> prod_ k e. X ( ( B ` k ) - ( ( C ` m ) ` k ) ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
155 154 cbvmptv 
 |-  ( m e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` m ) ` k ) ) ) = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) )
156 eqid 
 |-  inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) = inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < )
157 eqid 
 |-  ( ( |_ ` ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) ) ) + 1 ) = ( ( |_ ` ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) ) ) + 1 )
158 fveq2 
 |-  ( j = k -> ( B ` j ) = ( B ` k ) )
159 fveq2 
 |-  ( j = k -> ( A ` j ) = ( A ` k ) )
160 158 159 oveq12d 
 |-  ( j = k -> ( ( B ` j ) - ( A ` j ) ) = ( ( B ` k ) - ( A ` k ) ) )
161 160 cbvmptv 
 |-  ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) = ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) )
162 161 rneqi 
 |-  ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) = ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) )
163 162 infeq1i 
 |-  inf ( ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) , RR , < ) = inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < )
164 163 oveq2i 
 |-  ( 1 / inf ( ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) , RR , < ) ) = ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) )
165 164 fveq2i 
 |-  ( |_ ` ( 1 / inf ( ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) , RR , < ) ) ) = ( |_ ` ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) ) )
166 165 oveq1i 
 |-  ( ( |_ ` ( 1 / inf ( ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) , RR , < ) ) ) + 1 ) = ( ( |_ ` ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) ) ) + 1 )
167 166 fveq2i 
 |-  ( ZZ>= ` ( ( |_ ` ( 1 / inf ( ran ( j e. X |-> ( ( B ` j ) - ( A ` j ) ) ) , RR , < ) ) ) + 1 ) ) = ( ZZ>= ` ( ( |_ ` ( 1 / inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) ) ) + 1 ) )
168 1 2 3 4 5 7 8 146 155 156 157 167 vonioolem1 
 |-  ( ph -> ( m e. NN |-> ( ( voln ` X ) ` ( D ` m ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
169 145 168 eqbrtrd 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
170 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 ) ) )
171 142 169 170 syl2anc 
 |-  ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )