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

Proof

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