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 ( 𝜑𝑋 ∈ Fin )
vonioolem1.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
vonioolem1.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
vonioolem1.u ( 𝜑𝑋 ≠ ∅ )
vonioolem1.t ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) < ( 𝐵𝑘 ) )
vonioolem1.c 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) )
vonioolem1.d 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) )
vonioolem1.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) )
vonioolem1.r 𝑇 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
vonioolem1.e 𝐸 = inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < )
vonioolem1.n 𝑁 = ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 )
vonioolem1.z 𝑍 = ( ℤ𝑁 )
Assertion vonioolem1 ( 𝜑𝑆 ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 vonioolem1.x ( 𝜑𝑋 ∈ Fin )
2 vonioolem1.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
3 vonioolem1.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
4 vonioolem1.u ( 𝜑𝑋 ≠ ∅ )
5 vonioolem1.t ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) < ( 𝐵𝑘 ) )
6 vonioolem1.c 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) )
7 vonioolem1.d 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) )
8 vonioolem1.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) )
9 vonioolem1.r 𝑇 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
10 vonioolem1.e 𝐸 = inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < )
11 vonioolem1.n 𝑁 = ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 )
12 vonioolem1.z 𝑍 = ( ℤ𝑁 )
13 9 a1i ( 𝜑𝑇 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ) )
14 6 a1i ( 𝜑𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) ) )
15 1 mptexd ( 𝜑 → ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) ∈ V )
16 15 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) ∈ V )
17 14 16 fvmpt2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐶𝑛 ) = ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) )
18 ovexd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ∈ V )
19 17 18 fvmpt2d ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐶𝑛 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) )
20 19 oveq2d ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) = ( ( 𝐵𝑘 ) − ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) )
21 3 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℝ )
22 21 adantlr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℝ )
23 22 recnd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℂ )
24 2 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐴 : 𝑋 ⟶ ℝ )
25 24 ffvelrnda ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℝ )
26 25 recnd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℂ )
27 nnrecre ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
28 27 ad2antlr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
29 28 recnd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( 1 / 𝑛 ) ∈ ℂ )
30 23 26 29 subsub4d ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) = ( ( 𝐵𝑘 ) − ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) )
31 20 30 eqtr4d ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) = ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) )
32 31 prodeq2dv ( ( 𝜑𝑛 ∈ ℕ ) → ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) = ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) )
33 32 mpteq2dva ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) ) )
34 13 33 eqtrd ( 𝜑𝑇 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) ) )
35 nfv 𝑘 𝜑
36 rpssre + ⊆ ℝ
37 2 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℝ )
38 difrp ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ ( 𝐵𝑘 ) ∈ ℝ ) → ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) ↔ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ ) )
39 37 21 38 syl2anc ( ( 𝜑𝑘𝑋 ) → ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) ↔ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ ) )
40 5 39 mpbid ( ( 𝜑𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ )
41 36 40 sseldi ( ( 𝜑𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ )
42 41 recnd ( ( 𝜑𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℂ )
43 eqid ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) )
44 35 1 42 43 fprodsubrecnncnv ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) − ( 1 / 𝑛 ) ) ) ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
45 34 44 eqbrtrd ( 𝜑𝑇 ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
46 nnex ℕ ∈ V
47 46 mptex ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ) ∈ V
48 47 a1i ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ) ∈ V )
49 9 48 eqeltrid ( 𝜑𝑇 ∈ V )
50 46 mptex ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) ) ∈ V
51 50 a1i ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) ) ∈ V )
52 8 51 eqeltrid ( 𝜑𝑆 ∈ V )
53 1rp 1 ∈ ℝ+
54 53 a1i ( 𝜑 → 1 ∈ ℝ+ )
55 eqid ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) = ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
56 35 55 40 rnmptssd ( 𝜑 → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ⊆ ℝ+ )
57 ltso < Or ℝ
58 57 a1i ( 𝜑 → < Or ℝ )
59 55 rnmptfi ( 𝑋 ∈ Fin → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ∈ Fin )
60 1 59 syl ( 𝜑 → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ∈ Fin )
61 35 40 55 4 rnmptn0 ( 𝜑 → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ≠ ∅ )
62 36 a1i ( 𝜑 → ℝ+ ⊆ ℝ )
63 56 62 sstrd ( 𝜑 → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ⊆ ℝ )
64 fiinfcl ( ( < Or ℝ ∧ ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ∈ Fin ∧ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ≠ ∅ ∧ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ⊆ ℝ ) ) → inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
65 58 60 61 63 64 syl13anc ( 𝜑 → inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
66 10 65 eqeltrid ( 𝜑𝐸 ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
67 56 66 sseldd ( 𝜑𝐸 ∈ ℝ+ )
68 54 67 rpdivcld ( 𝜑 → ( 1 / 𝐸 ) ∈ ℝ+ )
69 68 rpred ( 𝜑 → ( 1 / 𝐸 ) ∈ ℝ )
70 68 rpge0d ( 𝜑 → 0 ≤ ( 1 / 𝐸 ) )
71 flge0nn0 ( ( ( 1 / 𝐸 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐸 ) ) → ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ0 )
72 69 70 71 syl2anc ( 𝜑 → ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ0 )
73 nn0p1nn ( ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) ∈ ℕ )
74 72 73 syl ( 𝜑 → ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) ∈ ℕ )
75 74 nnzd ( 𝜑 → ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) ∈ ℤ )
76 11 75 eqeltrid ( 𝜑𝑁 ∈ ℤ )
77 11 recnnltrp ( 𝐸 ∈ ℝ+ → ( 𝑁 ∈ ℕ ∧ ( 1 / 𝑁 ) < 𝐸 ) )
78 67 77 syl ( 𝜑 → ( 𝑁 ∈ ℕ ∧ ( 1 / 𝑁 ) < 𝐸 ) )
79 78 simpld ( 𝜑𝑁 ∈ ℕ )
80 uznnssnn ( 𝑁 ∈ ℕ → ( ℤ𝑁 ) ⊆ ℕ )
81 79 80 syl ( 𝜑 → ( ℤ𝑁 ) ⊆ ℕ )
82 12 81 eqsstrid ( 𝜑𝑍 ⊆ ℕ )
83 82 adantr ( ( 𝜑𝑛𝑍 ) → 𝑍 ⊆ ℕ )
84 simpr ( ( 𝜑𝑛𝑍 ) → 𝑛𝑍 )
85 83 84 sseldd ( ( 𝜑𝑛𝑍 ) → 𝑛 ∈ ℕ )
86 7 a1i ( 𝜑𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
87 1 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
88 eqid dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
89 25 28 readdcld ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘𝑋 ) → ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
90 89 fmpttd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ )
91 17 feq1d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐶𝑛 ) : 𝑋 ⟶ ℝ ↔ ( 𝑘𝑋 ↦ ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ ) )
92 90 91 mpbird ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐶𝑛 ) : 𝑋 ⟶ ℝ )
93 3 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐵 : 𝑋 ⟶ ℝ )
94 87 88 92 93 hoimbl ( ( 𝜑𝑛 ∈ ℕ ) → X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ∈ dom ( voln ‘ 𝑋 ) )
95 94 elexd ( ( 𝜑𝑛 ∈ ℕ ) → X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ∈ V )
96 86 95 fvmpt2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐷𝑛 ) = X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) )
97 85 96 syldan ( ( 𝜑𝑛𝑍 ) → ( 𝐷𝑛 ) = X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) )
98 97 fveq2d ( ( 𝜑𝑛𝑍 ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
99 1 adantr ( ( 𝜑𝑛𝑍 ) → 𝑋 ∈ Fin )
100 4 adantr ( ( 𝜑𝑛𝑍 ) → 𝑋 ≠ ∅ )
101 85 92 syldan ( ( 𝜑𝑛𝑍 ) → ( 𝐶𝑛 ) : 𝑋 ⟶ ℝ )
102 3 adantr ( ( 𝜑𝑛𝑍 ) → 𝐵 : 𝑋 ⟶ ℝ )
103 eqid X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) = X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) )
104 99 100 101 102 103 vonn0hoi ( ( 𝜑𝑛𝑍 ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘𝑋 ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
105 101 ffvelrnda ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( 𝐶𝑛 ) ‘ 𝑘 ) ∈ ℝ )
106 85 22 syldanl ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 𝐵𝑘 ) ∈ ℝ )
107 volico ( ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) = if ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) , 0 ) )
108 105 106 107 syl2anc ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( vol ‘ ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) = if ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) , 0 ) )
109 85 19 syldanl ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( 𝐶𝑛 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) )
110 85 28 syldanl ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
111 79 nnrecred ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
112 111 ad2antrr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 1 / 𝑁 ) ∈ ℝ )
113 41 adantlr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ )
114 12 eleq2i ( 𝑛𝑍𝑛 ∈ ( ℤ𝑁 ) )
115 114 biimpi ( 𝑛𝑍𝑛 ∈ ( ℤ𝑁 ) )
116 eluzle ( 𝑛 ∈ ( ℤ𝑁 ) → 𝑁𝑛 )
117 115 116 syl ( 𝑛𝑍𝑁𝑛 )
118 117 adantl ( ( 𝜑𝑛𝑍 ) → 𝑁𝑛 )
119 79 nnrpd ( 𝜑𝑁 ∈ ℝ+ )
120 119 adantr ( ( 𝜑𝑛𝑍 ) → 𝑁 ∈ ℝ+ )
121 nnrp ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
122 85 121 syl ( ( 𝜑𝑛𝑍 ) → 𝑛 ∈ ℝ+ )
123 120 122 lerecd ( ( 𝜑𝑛𝑍 ) → ( 𝑁𝑛 ↔ ( 1 / 𝑛 ) ≤ ( 1 / 𝑁 ) ) )
124 118 123 mpbid ( ( 𝜑𝑛𝑍 ) → ( 1 / 𝑛 ) ≤ ( 1 / 𝑁 ) )
125 124 adantr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 1 / 𝑛 ) ≤ ( 1 / 𝑁 ) )
126 111 adantr ( ( 𝜑𝑘𝑋 ) → ( 1 / 𝑁 ) ∈ ℝ )
127 36 67 sseldi ( 𝜑𝐸 ∈ ℝ )
128 127 adantr ( ( 𝜑𝑘𝑋 ) → 𝐸 ∈ ℝ )
129 78 simprd ( 𝜑 → ( 1 / 𝑁 ) < 𝐸 )
130 129 adantr ( ( 𝜑𝑘𝑋 ) → ( 1 / 𝑁 ) < 𝐸 )
131 63 adantr ( ( 𝜑𝑘𝑋 ) → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ⊆ ℝ )
132 60 adantr ( ( 𝜑𝑘𝑋 ) → ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ∈ Fin )
133 id ( 𝑘𝑋𝑘𝑋 )
134 ovexd ( 𝑘𝑋 → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ V )
135 55 elrnmpt1 ( ( 𝑘𝑋 ∧ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ V ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
136 133 134 135 syl2anc ( 𝑘𝑋 → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
137 136 adantl ( ( 𝜑𝑘𝑋 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
138 infrefilb ( ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ⊆ ℝ ∧ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ∈ Fin ∧ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) ) → inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < ) ≤ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
139 131 132 137 138 syl3anc ( ( 𝜑𝑘𝑋 ) → inf ( ran ( 𝑘𝑋 ↦ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) , ℝ , < ) ≤ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
140 10 139 eqbrtrid ( ( 𝜑𝑘𝑋 ) → 𝐸 ≤ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
141 126 128 41 130 140 ltletrd ( ( 𝜑𝑘𝑋 ) → ( 1 / 𝑁 ) < ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
142 141 adantlr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 1 / 𝑁 ) < ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
143 110 112 113 125 142 lelttrd ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 1 / 𝑛 ) < ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
144 85 25 syldanl ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( 𝐴𝑘 ) ∈ ℝ )
145 144 110 106 ltaddsub2d ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) < ( 𝐵𝑘 ) ↔ ( 1 / 𝑛 ) < ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
146 143 145 mpbird ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( 𝐴𝑘 ) + ( 1 / 𝑛 ) ) < ( 𝐵𝑘 ) )
147 109 146 eqbrtrd ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( ( 𝐶𝑛 ) ‘ 𝑘 ) < ( 𝐵𝑘 ) )
148 147 iftrued ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → if ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) , 0 ) = ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
149 108 148 eqtrd ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝑋 ) → ( vol ‘ ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
150 149 prodeq2dv ( ( 𝜑𝑛𝑍 ) → ∏ 𝑘𝑋 ( vol ‘ ( ( ( 𝐶𝑛 ) ‘ 𝑘 ) [,) ( 𝐵𝑘 ) ) ) = ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
151 98 104 150 3eqtrd ( ( 𝜑𝑛𝑍 ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) = ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
152 fvexd ( ( 𝜑𝑛𝑍 ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) ∈ V )
153 8 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) ∈ V ) → ( 𝑆𝑛 ) = ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) )
154 85 152 153 syl2anc ( ( 𝜑𝑛𝑍 ) → ( 𝑆𝑛 ) = ( ( voln ‘ 𝑋 ) ‘ ( 𝐷𝑛 ) ) )
155 prodex 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ∈ V
156 155 a1i ( ( 𝜑𝑛𝑍 ) → ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ∈ V )
157 9 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) ∈ V ) → ( 𝑇𝑛 ) = ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
158 85 156 157 syl2anc ( ( 𝜑𝑛𝑍 ) → ( 𝑇𝑛 ) = ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( ( 𝐶𝑛 ) ‘ 𝑘 ) ) )
159 151 154 158 3eqtr4rd ( ( 𝜑𝑛𝑍 ) → ( 𝑇𝑛 ) = ( 𝑆𝑛 ) )
160 12 49 52 76 159 climeq ( 𝜑 → ( 𝑇 ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ↔ 𝑆 ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ) )
161 45 160 mpbid ( 𝜑𝑆 ⇝ ∏ 𝑘𝑋 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )