Metamath Proof Explorer

Theorem ovoliun2

Description: The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun .) (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t 
|- T = seq 1 ( + , G )
ovoliun.g 
|- G = ( n e. NN |-> ( vol* ` A ) )
ovoliun.a 
|- ( ( ph /\ n e. NN ) -> A C_ RR )
ovoliun.v 
|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
ovoliun2.t 
|- ( ph -> T e. dom ~~> )
Assertion ovoliun2 
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sum_ n e. NN ( vol* ` A ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t 
 |-  T = seq 1 ( + , G )
2 ovoliun.g 
 |-  G = ( n e. NN |-> ( vol* ` A ) )
3 ovoliun.a 
 |-  ( ( ph /\ n e. NN ) -> A C_ RR )
4 ovoliun.v 
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
5 ovoliun2.t 
 |-  ( ph -> T e. dom ~~> )
6 1 2 3 4 ovoliun 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 fvex 
 |-  ( vol* ` [_ m / n ]_ A ) e. _V
10 nfcv 
 |-  F/_ m ( vol* ` A )
11 nfcv 
 |-  F/_ n vol*
12 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
13 11 12 nffv 
 |-  F/_ n ( vol* ` [_ m / n ]_ A )
14 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
15 14 fveq2d 
 |-  ( n = m -> ( vol* ` A ) = ( vol* ` [_ m / n ]_ A ) )
16 10 13 15 cbvmpt 
 |-  ( n e. NN |-> ( vol* ` A ) ) = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
17 2 16 eqtri 
 |-  G = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
18 17 fvmpt2 
 |-  ( ( m e. NN /\ ( vol* ` [_ m / n ]_ A ) e. _V ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) )
19 9 18 mpan2 
 |-  ( m e. NN -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) )
20 19 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) )
21 4 ralrimiva 
 |-  ( ph -> A. n e. NN ( vol* ` A ) e. RR )
22 10 nfel1 
 |-  F/ m ( vol* ` A ) e. RR
23 13 nfel1 
 |-  F/ n ( vol* ` [_ m / n ]_ A ) e. RR
24 15 eleq1d 
 |-  ( n = m -> ( ( vol* ` A ) e. RR <-> ( vol* ` [_ m / n ]_ A ) e. RR ) )
25 22 23 24 cbvralw 
 |-  ( A. n e. NN ( vol* ` A ) e. RR <-> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
26 21 25 sylib 
 |-  ( ph -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
27 26 r19.21bi 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
28 20 27 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. RR )
29 7 8 28 serfre 
 |-  ( ph -> seq 1 ( + , G ) : NN --> RR )
30 1 feq1i 
 |-  ( T : NN --> RR <-> seq 1 ( + , G ) : NN --> RR )
31 29 30 sylibr 
 |-  ( ph -> T : NN --> RR )
32 31 frnd 
 |-  ( ph -> ran T C_ RR )
33 1nn 
 |-  1 e. NN
34 31 fdmd 
 |-  ( ph -> dom T = NN )
35 33 34 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
36 35 ne0d 
 |-  ( ph -> dom T =/= (/) )
37 dm0rn0 
 |-  ( dom T = (/) <-> ran T = (/) )
38 37 necon3bii 
 |-  ( dom T =/= (/) <-> ran T =/= (/) )
39 36 38 sylib 
 |-  ( ph -> ran T =/= (/) )
40 1 5 eqeltrrid 
 |-  ( ph -> seq 1 ( + , G ) e. dom ~~> )
41 7 8 20 27 40 isumrecl 
 |-  ( ph -> sum_ m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
42 elfznn 
 |-  ( m e. ( 1 ... k ) -> m e. NN )
43 42 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> m e. NN )
44 43 19 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) )
45 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
46 45 7 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
47 simpl 
 |-  ( ( ph /\ k e. NN ) -> ph )
48 47 42 27 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
49 48 recnd 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( vol* ` [_ m / n ]_ A ) e. CC )
50 44 46 49 fsumser 
 |-  ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) = ( seq 1 ( + , G ) ` k ) )
51 1 fveq1i 
 |-  ( T ` k ) = ( seq 1 ( + , G ) ` k )
52 50 51 eqtr4di 
 |-  ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) = ( T ` k ) )
53 fzfid 
 |-  ( ph -> ( 1 ... k ) e. Fin )
54 fz1ssnn 
 |-  ( 1 ... k ) C_ NN
55 54 a1i 
 |-  ( ph -> ( 1 ... k ) C_ NN )
56 3 ralrimiva 
 |-  ( ph -> A. n e. NN A C_ RR )
57 nfv 
 |-  F/ m A C_ RR
58 nfcv 
 |-  F/_ n RR
59 12 58 nfss 
 |-  F/ n [_ m / n ]_ A C_ RR
60 14 sseq1d 
 |-  ( n = m -> ( A C_ RR <-> [_ m / n ]_ A C_ RR ) )
61 57 59 60 cbvralw 
 |-  ( A. n e. NN A C_ RR <-> A. m e. NN [_ m / n ]_ A C_ RR )
62 56 61 sylib 
 |-  ( ph -> A. m e. NN [_ m / n ]_ A C_ RR )
63 62 r19.21bi 
 |-  ( ( ph /\ m e. NN ) -> [_ m / n ]_ A C_ RR )
64 ovolge0 
 |-  ( [_ m / n ]_ A C_ RR -> 0 <_ ( vol* ` [_ m / n ]_ A ) )
65 63 64 syl 
 |-  ( ( ph /\ m e. NN ) -> 0 <_ ( vol* ` [_ m / n ]_ A ) )
66 7 8 53 55 20 27 65 40 isumless 
 |-  ( ph -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) )
67 66 adantr 
 |-  ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) )
68 52 67 eqbrtrrd 
 |-  ( ( ph /\ k e. NN ) -> ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) )
69 68 ralrimiva 
 |-  ( ph -> A. k e. NN ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) )
70 brralrspcev 
 |-  ( ( sum_ m e. NN ( vol* ` [_ m / n ]_ A ) e. RR /\ A. k e. NN ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) -> E. x e. RR A. k e. NN ( T ` k ) <_ x )
71 41 69 70 syl2anc 
 |-  ( ph -> E. x e. RR A. k e. NN ( T ` k ) <_ x )
72 31 ffnd 
 |-  ( ph -> T Fn NN )
73 breq1 
 |-  ( z = ( T ` k ) -> ( z <_ x <-> ( T ` k ) <_ x ) )
74 73 ralrn 
 |-  ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. k e. NN ( T ` k ) <_ x ) )
75 72 74 syl 
 |-  ( ph -> ( A. z e. ran T z <_ x <-> A. k e. NN ( T ` k ) <_ x ) )
76 75 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. k e. NN ( T ` k ) <_ x ) )
77 71 76 mpbird 
 |-  ( ph -> E. x e. RR A. z e. ran T z <_ x )
78 supxrre 
 |-  ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
79 32 39 77 78 syl3anc 
 |-  ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
80 7 1 8 20 27 65 71 isumsup 
 |-  ( ph -> sum_ m e. NN ( vol* ` [_ m / n ]_ A ) = sup ( ran T , RR , < ) )
81 79 80 eqtr4d 
 |-  ( ph -> sup ( ran T , RR* , < ) = sum_ m e. NN ( vol* ` [_ m / n ]_ A ) )
82 10 13 15 cbvsumi 
 |-  sum_ n e. NN ( vol* ` A ) = sum_ m e. NN ( vol* ` [_ m / n ]_ A )
83 81 82 eqtr4di 
 |-  ( ph -> sup ( ran T , RR* , < ) = sum_ n e. NN ( vol* ` A ) )
84 6 83 breqtrd 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ sum_ n e. NN ( vol* ` A ) )