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 
|- ( ph -> X e. Fin )
vonicclem1.a 
|- ( ph -> A : X --> RR )
vonicclem1.b 
|- ( ph -> B : X --> RR )
vonicclem1.u 
|- ( ph -> X =/= (/) )
vonicclem1.t 
|- ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( B ` k ) )
vonicclem1.c 
|- C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
vonicclem1.d 
|- D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
vonicclem1.s 
|- S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
Assertion vonicclem1 
|- ( ph -> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )

Proof

Step Hyp Ref Expression
1 vonicclem1.x 
 |-  ( ph -> X e. Fin )
2 vonicclem1.a 
 |-  ( ph -> A : X --> RR )
3 vonicclem1.b 
 |-  ( ph -> B : X --> RR )
4 vonicclem1.u 
 |-  ( ph -> X =/= (/) )
5 vonicclem1.t 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( B ` k ) )
6 vonicclem1.c 
 |-  C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
7 vonicclem1.d 
 |-  D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
8 vonicclem1.s 
 |-  S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) )
9 8 a1i 
 |-  ( ph -> S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) )
10 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
11 7 a1i 
 |-  ( ph -> D = ( n e. NN |-> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) )
12 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
13 eqid 
 |-  dom ( voln ` X ) = dom ( voln ` X )
14 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : X --> RR )
15 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
16 15 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR )
17 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
18 17 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
19 16 18 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / n ) ) e. RR )
20 19 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) : X --> RR )
21 6 a1i 
 |-  ( ph -> C = ( n e. NN |-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) ) )
22 1 mptexd 
 |-  ( ph -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) e. _V )
23 22 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) e. _V )
24 21 23 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) = ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) )
25 24 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR <-> ( k e. X |-> ( ( B ` k ) + ( 1 / n ) ) ) : X --> RR ) )
26 20 25 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR )
27 12 13 14 26 hoimbl 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) e. dom ( voln ` X ) )
28 27 elexd 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) e. _V )
29 11 28 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
30 10 29 syldan 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) )
31 30 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln ` X ) ` ( D ` n ) ) = ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) )
32 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> X =/= (/) )
33 10 26 syldan 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR )
34 eqid 
 |-  X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) )
35 12 32 14 33 34 vonn0hoi 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) )
36 14 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR )
37 10 36 syldanl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR )
38 33 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR )
39 volico 
 |-  ( ( ( A ` k ) e. RR /\ ( ( C ` n ) ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = if ( ( A ` k ) < ( ( C ` n ) ` k ) , ( ( ( C ` n ) ` k ) - ( A ` k ) ) , 0 ) )
40 37 38 39 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = if ( ( A ` k ) < ( ( C ` n ) ` k ) , ( ( ( C ` n ) ` k ) - ( A ` k ) ) , 0 ) )
41 10 16 syldanl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR )
42 5 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) <_ ( B ` k ) )
43 nnrp 
 |-  ( n e. NN -> n e. RR+ )
44 43 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
45 44 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR+ )
46 41 45 ltaddrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) < ( ( B ` k ) + ( 1 / n ) ) )
47 19 elexd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) + ( 1 / n ) ) e. _V )
48 24 47 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( B ` k ) + ( 1 / n ) ) )
49 10 48 syldanl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( B ` k ) + ( 1 / n ) ) )
50 46 49 breqtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) < ( ( C ` n ) ` k ) )
51 37 41 38 42 50 lelttrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) < ( ( C ` n ) ` k ) )
52 51 iftrued 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> if ( ( A ` k ) < ( ( C ` n ) ` k ) , ( ( ( C ` n ) ` k ) - ( A ` k ) ) , 0 ) = ( ( ( C ` n ) ` k ) - ( A ` k ) ) )
53 40 52 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = ( ( ( C ` n ) ` k ) - ( A ` k ) ) )
54 53 prodeq2dv 
 |-  ( ( ph /\ n e. NN ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( ( C ` n ) ` k ) ) ) = prod_ k e. X ( ( ( C ` n ) ` k ) - ( A ` k ) ) )
55 31 35 54 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln ` X ) ` ( D ` n ) ) = prod_ k e. X ( ( ( C ` n ) ` k ) - ( A ` k ) ) )
56 48 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` n ) ` k ) - ( A ` k ) ) = ( ( ( B ` k ) + ( 1 / n ) ) - ( A ` k ) ) )
57 16 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. CC )
58 18 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. CC )
59 36 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. CC )
60 57 58 59 addsubd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( B ` k ) + ( 1 / n ) ) - ( A ` k ) ) = ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) )
61 56 60 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( C ` n ) ` k ) - ( A ` k ) ) = ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) )
62 61 prodeq2dv 
 |-  ( ( ph /\ n e. NN ) -> prod_ k e. X ( ( ( C ` n ) ` k ) - ( A ` k ) ) = prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) )
63 55 62 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln ` X ) ` ( D ` n ) ) = prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) )
64 63 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) ) )
65 9 64 eqtrd 
 |-  ( ph -> S = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) ) )
66 nfv 
 |-  F/ k ph
67 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
68 15 67 resubcld 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR )
69 68 recnd 
 |-  ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. CC )
70 eqid 
 |-  ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) )
71 66 1 69 70 fprodaddrecnncnv 
 |-  ( ph -> ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) + ( 1 / n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
72 65 71 eqbrtrd 
 |-  ( ph -> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )