Metamath Proof Explorer

Theorem vonicclem1

Description: The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonicclem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
vonicclem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
vonicclem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
vonicclem1.u ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
vonicclem1.t ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ≤ ( 𝐵 ‘ 𝑘 ) )
vonicclem1.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
vonicclem1.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) )
vonicclem1.s ⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) )
Assertion vonicclem1 ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 vonicclem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 vonicclem1.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 vonicclem1.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 vonicclem1.u ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
5 vonicclem1.t ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ≤ ( 𝐵 ‘ 𝑘 ) )
6 vonicclem1.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
7 vonicclem1.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) )
8 vonicclem1.s ⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) )
9 8 a1i ⊢ ( 𝜑 → 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
11 7 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑛 ∈ ℕ ↦ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
13 eqid ⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : 𝑋 ⟶ ℝ )
15 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
16 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
17 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
18 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
19 16 18 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
20 19 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ )
21 6 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) ) )
22 1 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) ∈ V )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) ∈ V )
24 21 23 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) )
25 24 feq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑛 ) : 𝑋 ⟶ ℝ ↔ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ ) )
26 20 25 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) : 𝑋 ⟶ ℝ )
27 12 13 14 26 hoimbl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ dom ( voln ‘ 𝑋 ) )
28 27 elexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ V )
29 11 28 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) )
30 10 29 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) )
31 30 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
32 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ )
33 10 26 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) : 𝑋 ⟶ ℝ )
34 eqid ⊢ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) )
35 12 32 14 33 34 vonn0hoi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln ‘ 𝑋 ) ‘ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) )
36 14 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
37 10 36 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
38 33 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ∈ ℝ )
39 volico ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) , ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
40 37 38 39 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) , ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
41 10 16 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
42 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ≤ ( 𝐵 ‘ 𝑘 ) )
43 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
44 43 rpreccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
45 44 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ+ )
46 41 45 ltaddrpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) < ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) )
47 19 elexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) ∈ V )
48 24 47 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) )
49 10 48 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) )
50 46 49 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) < ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) )
51 37 41 38 42 50 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) < ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) )
52 51 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) , ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) = ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
53 40 52 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) = ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
54 53 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
55 31 35 54 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) = ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
56 48 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ( ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) − ( 𝐴 ‘ 𝑘 ) ) )
57 16 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
58 18 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℂ )
59 36 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
60 57 58 59 addsubd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐵 ‘ 𝑘 ) + ( 1 / 𝑛 ) ) − ( 𝐴 ‘ 𝑘 ) ) = ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) )
61 56 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) )
62 61 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) )
63 55 62 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) = ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) )
64 63 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( voln ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) ) )
65 9 64 eqtrd ⊢ ( 𝜑 → 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) ) )
66 nfv ⊢ Ⅎ 𝑘 𝜑
67 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
68 15 67 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
69 68 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
70 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) )
71 66 1 69 70 fprodaddrecnncnv ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) + ( 1 / 𝑛 ) ) ) ⇝ ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
72 65 71 eqbrtrd ⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )