Metamath Proof Explorer

Theorem vitalilem4

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 
|- .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
vitali.2 
|- S = ( ( 0 [,] 1 ) /. .~ )
vitali.3 
|- ( ph -> F Fn S )
vitali.4 
|- ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
vitali.5 
|- ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
vitali.6 
|- T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
vitali.7 
|- ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
Assertion vitalilem4 
|- ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) = 0 )

Proof

Step Hyp Ref Expression
1 vitali.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
2 vitali.2 
 |-  S = ( ( 0 [,] 1 ) /. .~ )
3 vitali.3 
 |-  ( ph -> F Fn S )
4 vitali.4 
 |-  ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
5 vitali.5 
 |-  ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
6 vitali.6 
 |-  T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
7 vitali.7 
 |-  ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
8 fveq2 
 |-  ( n = m -> ( G ` n ) = ( G ` m ) )
9 8 oveq2d 
 |-  ( n = m -> ( s - ( G ` n ) ) = ( s - ( G ` m ) ) )
10 9 eleq1d 
 |-  ( n = m -> ( ( s - ( G ` n ) ) e. ran F <-> ( s - ( G ` m ) ) e. ran F ) )
11 10 rabbidv 
 |-  ( n = m -> { s e. RR | ( s - ( G ` n ) ) e. ran F } = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
12 reex 
 |-  RR e. _V
13 12 rabex 
 |-  { s e. RR | ( s - ( G ` m ) ) e. ran F } e. _V
14 11 6 13 fvmpt 
 |-  ( m e. NN -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
15 14 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
16 15 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) = ( vol* ` { s e. RR | ( s - ( G ` m ) ) e. ran F } ) )
17 1 2 3 4 5 6 7 vitalilem2 
 |-  ( ph -> ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) ) )
18 17 simp1d 
 |-  ( ph -> ran F C_ ( 0 [,] 1 ) )
19 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
20 18 19 sstrdi 
 |-  ( ph -> ran F C_ RR )
21 20 adantr 
 |-  ( ( ph /\ m e. NN ) -> ran F C_ RR )
22 neg1rr 
 |-  -u 1 e. RR
23 1re 
 |-  1 e. RR
24 iccssre 
 |-  ( ( -u 1 e. RR /\ 1 e. RR ) -> ( -u 1 [,] 1 ) C_ RR )
25 22 23 24 mp2an 
 |-  ( -u 1 [,] 1 ) C_ RR
26 f1of 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
27 5 26 syl 
 |-  ( ph -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
28 27 ffvelrnda 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. ( QQ i^i ( -u 1 [,] 1 ) ) )
29 28 elin2d 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. ( -u 1 [,] 1 ) )
30 25 29 sseldi 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. RR )
31 eqidd 
 |-  ( ( ph /\ m e. NN ) -> { s e. RR | ( s - ( G ` m ) ) e. ran F } = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
32 21 30 31 ovolshft 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ran F ) = ( vol* ` { s e. RR | ( s - ( G ` m ) ) e. ran F } ) )
33 16 32 eqtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) = ( vol* ` ran F ) )
34 3re 
 |-  3 e. RR
35 34 rexri 
 |-  3 e. RR*
36 35 a1i 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 3 e. RR* )
37 3rp 
 |-  3 e. RR+
38 0re 
 |-  0 e. RR
39 0le1 
 |-  0 <_ 1
40 ovolicc 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 0 <_ 1 ) -> ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 ) )
41 38 23 39 40 mp3an 
 |-  ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 )
42 1m0e1 
 |-  ( 1 - 0 ) = 1
43 41 42 eqtri 
 |-  ( vol* ` ( 0 [,] 1 ) ) = 1
44 43 23 eqeltri 
 |-  ( vol* ` ( 0 [,] 1 ) ) e. RR
45 ovolsscl 
 |-  ( ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ RR /\ ( vol* ` ( 0 [,] 1 ) ) e. RR ) -> ( vol* ` ran F ) e. RR )
46 19 44 45 mp3an23 
 |-  ( ran F C_ ( 0 [,] 1 ) -> ( vol* ` ran F ) e. RR )
47 18 46 syl 
 |-  ( ph -> ( vol* ` ran F ) e. RR )
48 47 adantr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` ran F ) e. RR )
49 simpr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 0 < ( vol* ` ran F ) )
50 48 49 elrpd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` ran F ) e. RR+ )
51 rpdivcl 
 |-  ( ( 3 e. RR+ /\ ( vol* ` ran F ) e. RR+ ) -> ( 3 / ( vol* ` ran F ) ) e. RR+ )
52 37 50 51 sylancr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( 3 / ( vol* ` ran F ) ) e. RR+ )
53 52 rpred 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( 3 / ( vol* ` ran F ) ) e. RR )
54 52 rpge0d 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 0 <_ ( 3 / ( vol* ` ran F ) ) )
55 flge0nn0 
 |-  ( ( ( 3 / ( vol* ` ran F ) ) e. RR /\ 0 <_ ( 3 / ( vol* ` ran F ) ) ) -> ( |_ ` ( 3 / ( vol* ` ran F ) ) ) e. NN0 )
56 53 54 55 syl2anc 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( |_ ` ( 3 / ( vol* ` ran F ) ) ) e. NN0 )
57 nn0p1nn 
 |-  ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) e. NN0 -> ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) e. NN )
58 56 57 syl 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) e. NN )
59 58 nnred 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) e. RR )
60 59 48 remulcld 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) e. RR )
61 60 rexrd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) e. RR* )
62 12 elpw2 
 |-  ( ran F e. ~P RR <-> ran F C_ RR )
63 20 62 sylibr 
 |-  ( ph -> ran F e. ~P RR )
64 63 anim1i 
 |-  ( ( ph /\ -. ran F e. dom vol ) -> ( ran F e. ~P RR /\ -. ran F e. dom vol ) )
65 eldif 
 |-  ( ran F e. ( ~P RR \ dom vol ) <-> ( ran F e. ~P RR /\ -. ran F e. dom vol ) )
66 64 65 sylibr 
 |-  ( ( ph /\ -. ran F e. dom vol ) -> ran F e. ( ~P RR \ dom vol ) )
67 66 ex 
 |-  ( ph -> ( -. ran F e. dom vol -> ran F e. ( ~P RR \ dom vol ) ) )
68 7 67 mt3d 
 |-  ( ph -> ran F e. dom vol )
69 inss1 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ
70 qssre 
 |-  QQ C_ RR
71 69 70 sstri 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ RR
72 fss 
 |-  ( ( G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( QQ i^i ( -u 1 [,] 1 ) ) C_ RR ) -> G : NN --> RR )
73 27 71 72 sylancl 
 |-  ( ph -> G : NN --> RR )
74 73 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. RR )
75 shftmbl 
 |-  ( ( ran F e. dom vol /\ ( G ` n ) e. RR ) -> { s e. RR | ( s - ( G ` n ) ) e. ran F } e. dom vol )
76 68 74 75 syl2an2r 
 |-  ( ( ph /\ n e. NN ) -> { s e. RR | ( s - ( G ` n ) ) e. ran F } e. dom vol )
77 76 6 fmptd 
 |-  ( ph -> T : NN --> dom vol )
78 77 ffvelrnda 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) e. dom vol )
79 78 ralrimiva 
 |-  ( ph -> A. m e. NN ( T ` m ) e. dom vol )
80 iunmbl 
 |-  ( A. m e. NN ( T ` m ) e. dom vol -> U_ m e. NN ( T ` m ) e. dom vol )
81 79 80 syl 
 |-  ( ph -> U_ m e. NN ( T ` m ) e. dom vol )
82 mblss 
 |-  ( U_ m e. NN ( T ` m ) e. dom vol -> U_ m e. NN ( T ` m ) C_ RR )
83 ovolcl 
 |-  ( U_ m e. NN ( T ` m ) C_ RR -> ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* )
84 81 82 83 3syl 
 |-  ( ph -> ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* )
85 84 adantr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* )
86 flltp1 
 |-  ( ( 3 / ( vol* ` ran F ) ) e. RR -> ( 3 / ( vol* ` ran F ) ) < ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) )
87 53 86 syl 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( 3 / ( vol* ` ran F ) ) < ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) )
88 34 a1i 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 3 e. RR )
89 88 59 50 ltdivmul2d 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( 3 / ( vol* ` ran F ) ) < ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) <-> 3 < ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) ) )
90 87 89 mpbid 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 3 < ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) )
91 nnuz 
 |-  NN = ( ZZ>= ` 1 )
92 1zzd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 1 e. ZZ )
93 mblvol 
 |-  ( ( T ` m ) e. dom vol -> ( vol ` ( T ` m ) ) = ( vol* ` ( T ` m ) ) )
94 78 93 syl 
 |-  ( ( ph /\ m e. NN ) -> ( vol ` ( T ` m ) ) = ( vol* ` ( T ` m ) ) )
95 94 33 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( vol ` ( T ` m ) ) = ( vol* ` ran F ) )
96 47 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ran F ) e. RR )
97 95 96 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( vol ` ( T ` m ) ) e. RR )
98 97 adantlr 
 |-  ( ( ( ph /\ 0 < ( vol* ` ran F ) ) /\ m e. NN ) -> ( vol ` ( T ` m ) ) e. RR )
99 eqid 
 |-  ( m e. NN |-> ( vol ` ( T ` m ) ) ) = ( m e. NN |-> ( vol ` ( T ` m ) ) )
100 98 99 fmptd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( m e. NN |-> ( vol ` ( T ` m ) ) ) : NN --> RR )
101 100 ffvelrnda 
 |-  ( ( ( ph /\ 0 < ( vol* ` ran F ) ) /\ k e. NN ) -> ( ( m e. NN |-> ( vol ` ( T ` m ) ) ) ` k ) e. RR )
102 91 92 101 serfre 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) : NN --> RR )
103 102 frnd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) C_ RR )
104 ressxr 
 |-  RR C_ RR*
105 103 104 sstrdi 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) C_ RR* )
106 95 adantlr 
 |-  ( ( ( ph /\ 0 < ( vol* ` ran F ) ) /\ m e. NN ) -> ( vol ` ( T ` m ) ) = ( vol* ` ran F ) )
107 106 mpteq2dva 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( m e. NN |-> ( vol ` ( T ` m ) ) ) = ( m e. NN |-> ( vol* ` ran F ) ) )
108 fconstmpt 
 |-  ( NN X. { ( vol* ` ran F ) } ) = ( m e. NN |-> ( vol* ` ran F ) )
109 107 108 eqtr4di 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( m e. NN |-> ( vol ` ( T ` m ) ) ) = ( NN X. { ( vol* ` ran F ) } ) )
110 109 seqeq3d 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) = seq 1 ( + , ( NN X. { ( vol* ` ran F ) } ) ) )
111 110 fveq1d 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) = ( seq 1 ( + , ( NN X. { ( vol* ` ran F ) } ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) )
112 48 recnd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` ran F ) e. CC )
113 ser1const 
 |-  ( ( ( vol* ` ran F ) e. CC /\ ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) e. NN ) -> ( seq 1 ( + , ( NN X. { ( vol* ` ran F ) } ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) = ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) )
114 112 58 113 syl2anc 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( seq 1 ( + , ( NN X. { ( vol* ` ran F ) } ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) = ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) )
115 111 114 eqtrd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) = ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) )
116 102 ffnd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) Fn NN )
117 fnfvelrn 
 |-  ( ( seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) Fn NN /\ ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) e. NN ) -> ( seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) e. ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) )
118 116 58 117 syl2anc 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) ` ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) ) e. ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) )
119 115 118 eqeltrrd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) e. ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) )
120 supxrub 
 |-  ( ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) C_ RR* /\ ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) e. ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) , RR* , < ) )
121 105 119 120 syl2anc 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) , RR* , < ) )
122 81 adantr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> U_ m e. NN ( T ` m ) e. dom vol )
123 mblvol 
 |-  ( U_ m e. NN ( T ` m ) e. dom vol -> ( vol ` U_ m e. NN ( T ` m ) ) = ( vol* ` U_ m e. NN ( T ` m ) ) )
124 122 123 syl 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol ` U_ m e. NN ( T ` m ) ) = ( vol* ` U_ m e. NN ( T ` m ) ) )
125 78 97 jca 
 |-  ( ( ph /\ m e. NN ) -> ( ( T ` m ) e. dom vol /\ ( vol ` ( T ` m ) ) e. RR ) )
126 125 ralrimiva 
 |-  ( ph -> A. m e. NN ( ( T ` m ) e. dom vol /\ ( vol ` ( T ` m ) ) e. RR ) )
127 1 2 3 4 5 6 7 vitalilem3 
 |-  ( ph -> Disj_ m e. NN ( T ` m ) )
128 127 adantr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> Disj_ m e. NN ( T ` m ) )
129 eqid 
 |-  seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) = seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) )
130 129 99 voliun 
 |-  ( ( A. m e. NN ( ( T ` m ) e. dom vol /\ ( vol ` ( T ` m ) ) e. RR ) /\ Disj_ m e. NN ( T ` m ) ) -> ( vol ` U_ m e. NN ( T ` m ) ) = sup ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) , RR* , < ) )
131 126 128 130 syl2an2r 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol ` U_ m e. NN ( T ` m ) ) = sup ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) , RR* , < ) )
132 124 131 eqtr3d 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` U_ m e. NN ( T ` m ) ) = sup ( ran seq 1 ( + , ( m e. NN |-> ( vol ` ( T ` m ) ) ) ) , RR* , < ) )
133 121 132 breqtrrd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( ( |_ ` ( 3 / ( vol* ` ran F ) ) ) + 1 ) x. ( vol* ` ran F ) ) <_ ( vol* ` U_ m e. NN ( T ` m ) ) )
134 36 61 85 90 133 xrltletrd 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> 3 < ( vol* ` U_ m e. NN ( T ` m ) ) )
135 17 simp3d 
 |-  ( ph -> U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) )
136 135 adantr 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) )
137 2re 
 |-  2 e. RR
138 iccssre 
 |-  ( ( -u 1 e. RR /\ 2 e. RR ) -> ( -u 1 [,] 2 ) C_ RR )
139 22 137 138 mp2an 
 |-  ( -u 1 [,] 2 ) C_ RR
140 ovolss 
 |-  ( ( U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) /\ ( -u 1 [,] 2 ) C_ RR ) -> ( vol* ` U_ m e. NN ( T ` m ) ) <_ ( vol* ` ( -u 1 [,] 2 ) ) )
141 136 139 140 sylancl 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` U_ m e. NN ( T ` m ) ) <_ ( vol* ` ( -u 1 [,] 2 ) ) )
142 2cn 
 |-  2 e. CC
143 ax-1cn 
 |-  1 e. CC
144 142 143 subnegi 
 |-  ( 2 - -u 1 ) = ( 2 + 1 )
145 neg1lt0 
 |-  -u 1 < 0
146 2pos 
 |-  0 < 2
147 22 38 137 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < 2 ) -> -u 1 < 2 )
148 145 146 147 mp2an 
 |-  -u 1 < 2
149 22 137 148 ltleii 
 |-  -u 1 <_ 2
150 ovolicc 
 |-  ( ( -u 1 e. RR /\ 2 e. RR /\ -u 1 <_ 2 ) -> ( vol* ` ( -u 1 [,] 2 ) ) = ( 2 - -u 1 ) )
151 22 137 149 150 mp3an 
 |-  ( vol* ` ( -u 1 [,] 2 ) ) = ( 2 - -u 1 )
152 df-3 
 |-  3 = ( 2 + 1 )
153 144 151 152 3eqtr4i 
 |-  ( vol* ` ( -u 1 [,] 2 ) ) = 3
154 141 153 breqtrdi 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( vol* ` U_ m e. NN ( T ` m ) ) <_ 3 )
155 xrlenlt 
 |-  ( ( ( vol* ` U_ m e. NN ( T ` m ) ) e. RR* /\ 3 e. RR* ) -> ( ( vol* ` U_ m e. NN ( T ` m ) ) <_ 3 <-> -. 3 < ( vol* ` U_ m e. NN ( T ` m ) ) ) )
156 85 35 155 sylancl 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> ( ( vol* ` U_ m e. NN ( T ` m ) ) <_ 3 <-> -. 3 < ( vol* ` U_ m e. NN ( T ` m ) ) ) )
157 154 156 mpbid 
 |-  ( ( ph /\ 0 < ( vol* ` ran F ) ) -> -. 3 < ( vol* ` U_ m e. NN ( T ` m ) ) )
158 134 157 pm2.65da 
 |-  ( ph -> -. 0 < ( vol* ` ran F ) )
159 ovolge0 
 |-  ( ran F C_ RR -> 0 <_ ( vol* ` ran F ) )
160 20 159 syl 
 |-  ( ph -> 0 <_ ( vol* ` ran F ) )
161 0xr 
 |-  0 e. RR*
162 ovolcl 
 |-  ( ran F C_ RR -> ( vol* ` ran F ) e. RR* )
163 20 162 syl 
 |-  ( ph -> ( vol* ` ran F ) e. RR* )
164 xrleloe 
 |-  ( ( 0 e. RR* /\ ( vol* ` ran F ) e. RR* ) -> ( 0 <_ ( vol* ` ran F ) <-> ( 0 < ( vol* ` ran F ) \/ 0 = ( vol* ` ran F ) ) ) )
165 161 163 164 sylancr 
 |-  ( ph -> ( 0 <_ ( vol* ` ran F ) <-> ( 0 < ( vol* ` ran F ) \/ 0 = ( vol* ` ran F ) ) ) )
166 160 165 mpbid 
 |-  ( ph -> ( 0 < ( vol* ` ran F ) \/ 0 = ( vol* ` ran F ) ) )
167 166 ord 
 |-  ( ph -> ( -. 0 < ( vol* ` ran F ) -> 0 = ( vol* ` ran F ) ) )
168 158 167 mpd 
 |-  ( ph -> 0 = ( vol* ` ran F ) )
169 168 adantr 
 |-  ( ( ph /\ m e. NN ) -> 0 = ( vol* ` ran F ) )
170 33 169 eqtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` ( T ` m ) ) = 0 )