Metamath Proof Explorer

Theorem voliunlem2

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 
|- ( ph -> F : NN --> dom vol )
voliunlem.5 
|- ( ph -> Disj_ i e. NN ( F ` i ) )
voliunlem.6 
|- H = ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) )
Assertion voliunlem2 
|- ( ph -> U. ran F e. dom vol )

Proof

Step Hyp Ref Expression
1 voliunlem.3 
 |-  ( ph -> F : NN --> dom vol )
2 voliunlem.5 
 |-  ( ph -> Disj_ i e. NN ( F ` i ) )
3 voliunlem.6 
 |-  H = ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) )
4 1 frnd 
 |-  ( ph -> ran F C_ dom vol )
5 mblss 
 |-  ( x e. dom vol -> x C_ RR )
6 velpw 
 |-  ( x e. ~P RR <-> x C_ RR )
7 5 6 sylibr 
 |-  ( x e. dom vol -> x e. ~P RR )
8 7 ssriv 
 |-  dom vol C_ ~P RR
9 4 8 sstrdi 
 |-  ( ph -> ran F C_ ~P RR )
10 sspwuni 
 |-  ( ran F C_ ~P RR <-> U. ran F C_ RR )
11 9 10 sylib 
 |-  ( ph -> U. ran F C_ RR )
12 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
13 inundif 
 |-  ( ( x i^i U. ran F ) u. ( x \ U. ran F ) ) = x
14 13 fveq2i 
 |-  ( vol* ` ( ( x i^i U. ran F ) u. ( x \ U. ran F ) ) ) = ( vol* ` x )
15 inss1 
 |-  ( x i^i U. ran F ) C_ x
16 simp2 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> x C_ RR )
17 15 16 sstrid 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x i^i U. ran F ) C_ RR )
18 ovolsscl 
 |-  ( ( ( x i^i U. ran F ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) e. RR )
19 15 18 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) e. RR )
20 19 3adant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) e. RR )
21 difss 
 |-  ( x \ U. ran F ) C_ x
22 21 16 sstrid 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ U. ran F ) C_ RR )
23 ovolsscl 
 |-  ( ( ( x \ U. ran F ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ U. ran F ) ) e. RR )
24 21 23 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ U. ran F ) ) e. RR )
25 24 3adant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ U. ran F ) ) e. RR )
26 ovolun 
 |-  ( ( ( ( x i^i U. ran F ) C_ RR /\ ( vol* ` ( x i^i U. ran F ) ) e. RR ) /\ ( ( x \ U. ran F ) C_ RR /\ ( vol* ` ( x \ U. ran F ) ) e. RR ) ) -> ( vol* ` ( ( x i^i U. ran F ) u. ( x \ U. ran F ) ) ) <_ ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) )
27 17 20 22 25 26 syl22anc 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( ( x i^i U. ran F ) u. ( x \ U. ran F ) ) ) <_ ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) )
28 14 27 eqbrtrrid 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) <_ ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) )
29 20 rexrd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) e. RR* )
30 nnuz 
 |-  NN = ( ZZ>= ` 1 )
31 1zzd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> 1 e. ZZ )
32 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
33 32 ineq2d 
 |-  ( n = k -> ( x i^i ( F ` n ) ) = ( x i^i ( F ` k ) ) )
34 33 fveq2d 
 |-  ( n = k -> ( vol* ` ( x i^i ( F ` n ) ) ) = ( vol* ` ( x i^i ( F ` k ) ) ) )
35 fvex 
 |-  ( vol* ` ( x i^i ( F ` k ) ) ) e. _V
36 34 3 35 fvmpt 
 |-  ( k e. NN -> ( H ` k ) = ( vol* ` ( x i^i ( F ` k ) ) ) )
37 36 adantl 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( H ` k ) = ( vol* ` ( x i^i ( F ` k ) ) ) )
38 inss1 
 |-  ( x i^i ( F ` k ) ) C_ x
39 ovolsscl 
 |-  ( ( ( x i^i ( F ` k ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` k ) ) ) e. RR )
40 38 39 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` k ) ) ) e. RR )
41 40 3adant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` k ) ) ) e. RR )
42 41 adantr 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( vol* ` ( x i^i ( F ` k ) ) ) e. RR )
43 37 42 eqeltrd 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( H ` k ) e. RR )
44 30 31 43 serfre 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> seq 1 ( + , H ) : NN --> RR )
45 44 frnd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ran seq 1 ( + , H ) C_ RR )
46 ressxr 
 |-  RR C_ RR*
47 45 46 sstrdi 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ran seq 1 ( + , H ) C_ RR* )
48 supxrcl 
 |-  ( ran seq 1 ( + , H ) C_ RR* -> sup ( ran seq 1 ( + , H ) , RR* , < ) e. RR* )
49 47 48 syl 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> sup ( ran seq 1 ( + , H ) , RR* , < ) e. RR* )
50 simp3 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) e. RR )
51 50 25 resubcld 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) e. RR )
52 51 rexrd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) e. RR* )
53 iunin2 
 |-  U_ n e. NN ( x i^i ( F ` n ) ) = ( x i^i U_ n e. NN ( F ` n ) )
54 ffn 
 |-  ( F : NN --> dom vol -> F Fn NN )
55 fniunfv 
 |-  ( F Fn NN -> U_ n e. NN ( F ` n ) = U. ran F )
56 1 54 55 3syl 
 |-  ( ph -> U_ n e. NN ( F ` n ) = U. ran F )
57 56 3ad2ant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> U_ n e. NN ( F ` n ) = U. ran F )
58 57 ineq2d 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x i^i U_ n e. NN ( F ` n ) ) = ( x i^i U. ran F ) )
59 53 58 eqtrid 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> U_ n e. NN ( x i^i ( F ` n ) ) = ( x i^i U. ran F ) )
60 59 fveq2d 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` U_ n e. NN ( x i^i ( F ` n ) ) ) = ( vol* ` ( x i^i U. ran F ) ) )
61 eqid 
 |-  seq 1 ( + , H ) = seq 1 ( + , H )
62 inss1 
 |-  ( x i^i ( F ` n ) ) C_ x
63 62 16 sstrid 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x i^i ( F ` n ) ) C_ RR )
64 63 adantr 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ n e. NN ) -> ( x i^i ( F ` n ) ) C_ RR )
65 ovolsscl 
 |-  ( ( ( x i^i ( F ` n ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` n ) ) ) e. RR )
66 62 65 mp3an1 
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` n ) ) ) e. RR )
67 66 3adant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( F ` n ) ) ) e. RR )
68 67 adantr 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ n e. NN ) -> ( vol* ` ( x i^i ( F ` n ) ) ) e. RR )
69 61 3 64 68 ovoliun 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` U_ n e. NN ( x i^i ( F ` n ) ) ) <_ sup ( ran seq 1 ( + , H ) , RR* , < ) )
70 60 69 eqbrtrrd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) <_ sup ( ran seq 1 ( + , H ) , RR* , < ) )
71 1 3ad2ant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> F : NN --> dom vol )
72 2 3ad2ant1 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> Disj_ i e. NN ( F ` i ) )
73 71 72 3 16 50 voliunlem1 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) )
74 44 ffvelcdmda 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( seq 1 ( + , H ) ` k ) e. RR )
75 25 adantr 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( vol* ` ( x \ U. ran F ) ) e. RR )
76 simpl3 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( vol* ` x ) e. RR )
77 leaddsub 
 |-  ( ( ( seq 1 ( + , H ) ` k ) e. RR /\ ( vol* ` ( x \ U. ran F ) ) e. RR /\ ( vol* ` x ) e. RR ) -> ( ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
78 74 75 76 77 syl3anc 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
79 73 78 mpbid 
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) )
80 79 ralrimiva 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> A. k e. NN ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) )
81 ffn 
 |-  ( seq 1 ( + , H ) : NN --> RR -> seq 1 ( + , H ) Fn NN )
82 breq1 
 |-  ( z = ( seq 1 ( + , H ) ` k ) -> ( z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) <-> ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
83 82 ralrn 
 |-  ( seq 1 ( + , H ) Fn NN -> ( A. z e. ran seq 1 ( + , H ) z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) <-> A. k e. NN ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
84 44 81 83 3syl 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( A. z e. ran seq 1 ( + , H ) z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) <-> A. k e. NN ( seq 1 ( + , H ) ` k ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
85 80 84 mpbird 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> A. z e. ran seq 1 ( + , H ) z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) )
86 supxrleub 
 |-  ( ( ran seq 1 ( + , H ) C_ RR* /\ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) e. RR* ) -> ( sup ( ran seq 1 ( + , H ) , RR* , < ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) <-> A. z e. ran seq 1 ( + , H ) z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
87 47 52 86 syl2anc 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( sup ( ran seq 1 ( + , H ) , RR* , < ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) <-> A. z e. ran seq 1 ( + , H ) z <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
88 85 87 mpbird 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> sup ( ran seq 1 ( + , H ) , RR* , < ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) )
89 29 49 52 70 88 xrletrd 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i U. ran F ) ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) )
90 leaddsub 
 |-  ( ( ( vol* ` ( x i^i U. ran F ) ) e. RR /\ ( vol* ` ( x \ U. ran F ) ) e. RR /\ ( vol* ` x ) e. RR ) -> ( ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( vol* ` ( x i^i U. ran F ) ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
91 20 25 50 90 syl3anc 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( vol* ` ( x i^i U. ran F ) ) <_ ( ( vol* ` x ) - ( vol* ` ( x \ U. ran F ) ) ) ) )
92 89 91 mpbird 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) )
93 20 25 readdcld 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) e. RR )
94 50 93 letri3d 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) <-> ( ( vol* ` x ) <_ ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) /\ ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) ) )
95 28 92 94 mpbir2and 
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) )
96 95 3expia 
 |-  ( ( ph /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) ) )
97 12 96 sylan2 
 |-  ( ( ph /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) ) )
98 97 ralrimiva 
 |-  ( ph -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) ) )
99 ismbl 
 |-  ( U. ran F e. dom vol <-> ( U. ran F C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i U. ran F ) ) + ( vol* ` ( x \ U. ran F ) ) ) ) ) )
100 11 98 99 sylanbrc 
 |-  ( ph -> U. ran F e. dom vol )