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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
23 22 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : 𝑋 ⟶ ℝ )
25 24 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
38 difrp ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ+ ) )
39 37 21 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ+ ) )
40 5 39 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ+ )
41 36 40 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ∈ ℝ )
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 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
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 ⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )