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 ) )