Metamath Proof Explorer


Theorem vitalilem4

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

Ref Expression
Hypotheses vitali.1 ˙ = x y | x 0 1 y 0 1 x y
vitali.2 S = 0 1 / ˙
vitali.3 φ F Fn S
vitali.4 φ z S z F z z
vitali.5 φ G : 1-1 onto 1 1
vitali.6 T = n s | s G n ran F
vitali.7 φ ¬ ran F 𝒫 dom vol
Assertion vitalilem4 φ m vol * T m = 0

Proof

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