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 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
vonioolem2.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
vonioolem2.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
vonioolem2.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
vonioolem2.t ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
vonioolem2.i ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) (,) ( 𝐵 ‘ 𝑘 ) )
vonioolem2.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
vonioolem2.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
Assertion vonioolem2 ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )

Proof

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