Metamath Proof Explorer


Theorem uniioombllem6

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
uniioombl.a A = ran . F
uniioombl.e φ vol * E
uniioombl.c φ C +
uniioombl.g φ G : 2
uniioombl.s φ E ran . G
uniioombl.t T = seq 1 + abs G
uniioombl.v φ sup ran T * < vol * E + C
Assertion uniioombllem6 φ vol * E A + vol * E A vol * E + 4 C

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 uniioombl.a A = ran . F
5 uniioombl.e φ vol * E
6 uniioombl.c φ C +
7 uniioombl.g φ G : 2
8 uniioombl.s φ E ran . G
9 uniioombl.t T = seq 1 + abs G
10 uniioombl.v φ sup ran T * < vol * E + C
11 nnuz = 1
12 1zzd φ 1
13 eqidd φ m T m = T m
14 eqidd φ a abs G a = abs G a
15 eqid abs G = abs G
16 15 ovolfsf G : 2 abs G : 0 +∞
17 7 16 syl φ abs G : 0 +∞
18 17 ffvelrnda φ a abs G a 0 +∞
19 elrege0 abs G a 0 +∞ abs G a 0 abs G a
20 18 19 sylib φ a abs G a 0 abs G a
21 20 simpld φ a abs G a
22 20 simprd φ a 0 abs G a
23 1 2 3 4 5 6 7 8 9 10 uniioombllem1 φ sup ran T * <
24 15 9 ovolsf G : 2 T : 0 +∞
25 7 24 syl φ T : 0 +∞
26 25 frnd φ ran T 0 +∞
27 icossxr 0 +∞ *
28 26 27 sstrdi φ ran T *
29 supxrub ran T * x ran T x sup ran T * <
30 28 29 sylan φ x ran T x sup ran T * <
31 30 ralrimiva φ x ran T x sup ran T * <
32 25 ffnd φ T Fn
33 breq1 x = T m x sup ran T * < T m sup ran T * <
34 33 ralrn T Fn x ran T x sup ran T * < m T m sup ran T * <
35 32 34 syl φ x ran T x sup ran T * < m T m sup ran T * <
36 31 35 mpbid φ m T m sup ran T * <
37 brralrspcev sup ran T * < m T m sup ran T * < x m T m x
38 23 36 37 syl2anc φ x m T m x
39 11 9 12 14 21 22 38 isumsup2 φ T sup ran T <
40 rge0ssre 0 +∞
41 26 40 sstrdi φ ran T
42 1nn 1
43 25 fdmd φ dom T =
44 42 43 eleqtrrid φ 1 dom T
45 44 ne0d φ dom T
46 dm0rn0 dom T = ran T =
47 46 necon3bii dom T ran T
48 45 47 sylib φ ran T
49 brralrspcev sup ran T * < x ran T x sup ran T * < y x ran T x y
50 23 31 49 syl2anc φ y x ran T x y
51 supxrre ran T ran T y x ran T x y sup ran T * < = sup ran T <
52 41 48 50 51 syl3anc φ sup ran T * < = sup ran T <
53 39 52 breqtrrd φ T sup ran T * <
54 11 12 6 13 53 climi2 φ j m j T m sup ran T * < < C
55 11 r19.2uz j m j T m sup ran T * < < C m T m sup ran T * < < C
56 54 55 syl φ m T m sup ran T * < < C
57 1zzd φ m T m sup ran T * < < C j 1 m 1
58 6 ad2antrr φ m T m sup ran T * < < C j 1 m C +
59 simplrl φ m T m sup ran T * < < C j 1 m m
60 59 nnrpd φ m T m sup ran T * < < C j 1 m m +
61 58 60 rpdivcld φ m T m sup ran T * < < C j 1 m C m +
62 fvex . F z V
63 62 inex1 . F z . G j V
64 63 rgenw z . F z . G j V
65 eqid z . F z . G j = z . F z . G j
66 65 fnmpt z . F z . G j V z . F z . G j Fn
67 64 66 mp1i φ m T m sup ran T * < < C j 1 m n z . F z . G j Fn
68 elfznn i 1 n i
69 fvco2 z . F z . G j Fn i vol * z . F z . G j i = vol * z . F z . G j i
70 67 68 69 syl2an φ m T m sup ran T * < < C j 1 m n i 1 n vol * z . F z . G j i = vol * z . F z . G j i
71 68 adantl φ m T m sup ran T * < < C j 1 m n i 1 n i
72 2fveq3 z = i . F z = . F i
73 72 ineq1d z = i . F z . G j = . F i . G j
74 fvex . F i V
75 74 inex1 . F i . G j V
76 73 65 75 fvmpt i z . F z . G j i = . F i . G j
77 71 76 syl φ m T m sup ran T * < < C j 1 m n i 1 n z . F z . G j i = . F i . G j
78 77 fveq2d φ m T m sup ran T * < < C j 1 m n i 1 n vol * z . F z . G j i = vol * . F i . G j
79 70 78 eqtrd φ m T m sup ran T * < < C j 1 m n i 1 n vol * z . F z . G j i = vol * . F i . G j
80 simpr φ m T m sup ran T * < < C j 1 m n n
81 80 11 eleqtrdi φ m T m sup ran T * < < C j 1 m n n 1
82 inss2 . F i . G j . G j
83 7 adantr φ m T m sup ran T * < < C G : 2
84 elfznn j 1 m j
85 ffvelrn G : 2 j G j 2
86 83 84 85 syl2an φ m T m sup ran T * < < C j 1 m G j 2
87 86 elin2d φ m T m sup ran T * < < C j 1 m G j 2
88 1st2nd2 G j 2 G j = 1 st G j 2 nd G j
89 87 88 syl φ m T m sup ran T * < < C j 1 m G j = 1 st G j 2 nd G j
90 89 fveq2d φ m T m sup ran T * < < C j 1 m . G j = . 1 st G j 2 nd G j
91 df-ov 1 st G j 2 nd G j = . 1 st G j 2 nd G j
92 90 91 syl6eqr φ m T m sup ran T * < < C j 1 m . G j = 1 st G j 2 nd G j
93 ioossre 1 st G j 2 nd G j
94 92 93 eqsstrdi φ m T m sup ran T * < < C j 1 m . G j
95 94 ad2antrr φ m T m sup ran T * < < C j 1 m n i 1 n . G j
96 92 fveq2d φ m T m sup ran T * < < C j 1 m vol * . G j = vol * 1 st G j 2 nd G j
97 ovolfcl G : 2 j 1 st G j 2 nd G j 1 st G j 2 nd G j
98 83 84 97 syl2an φ m T m sup ran T * < < C j 1 m 1 st G j 2 nd G j 1 st G j 2 nd G j
99 ovolioo 1 st G j 2 nd G j 1 st G j 2 nd G j vol * 1 st G j 2 nd G j = 2 nd G j 1 st G j
100 98 99 syl φ m T m sup ran T * < < C j 1 m vol * 1 st G j 2 nd G j = 2 nd G j 1 st G j
101 96 100 eqtrd φ m T m sup ran T * < < C j 1 m vol * . G j = 2 nd G j 1 st G j
102 98 simp2d φ m T m sup ran T * < < C j 1 m 2 nd G j
103 98 simp1d φ m T m sup ran T * < < C j 1 m 1 st G j
104 102 103 resubcld φ m T m sup ran T * < < C j 1 m 2 nd G j 1 st G j
105 101 104 eqeltrd φ m T m sup ran T * < < C j 1 m vol * . G j
106 105 ad2antrr φ m T m sup ran T * < < C j 1 m n i 1 n vol * . G j
107 ovolsscl . F i . G j . G j . G j vol * . G j vol * . F i . G j
108 82 95 106 107 mp3an2i φ m T m sup ran T * < < C j 1 m n i 1 n vol * . F i . G j
109 108 recnd φ m T m sup ran T * < < C j 1 m n i 1 n vol * . F i . G j
110 79 81 109 fsumser φ m T m sup ran T * < < C j 1 m n i = 1 n vol * . F i . G j = seq 1 + vol * z . F z . G j n
111 110 eqcomd φ m T m sup ran T * < < C j 1 m n seq 1 + vol * z . F z . G j n = i = 1 n vol * . F i . G j
112 2fveq3 z = k . F z = . F k
113 112 ineq1d z = k . F z . G j = . F k . G j
114 113 cbvmptv z . F z . G j = k . F k . G j
115 eqeq1 z = x z = x =
116 infeq1 z = x sup z * < = sup x * <
117 supeq1 z = x sup z * < = sup x * <
118 116 117 opeq12d z = x sup z * < sup z * < = sup x * < sup x * <
119 115 118 ifbieq2d z = x if z = 0 0 sup z * < sup z * < = if x = 0 0 sup x * < sup x * <
120 119 cbvmptv z ran . if z = 0 0 sup z * < sup z * < = x ran . if x = 0 0 sup x * < sup x * <
121 1 2 3 4 5 6 7 8 9 10 114 120 uniioombllem2 φ j seq 1 + vol * z . F z . G j vol * . G j A
122 84 121 sylan2 φ j 1 m seq 1 + vol * z . F z . G j vol * . G j A
123 122 adantlr φ m T m sup ran T * < < C j 1 m seq 1 + vol * z . F z . G j vol * . G j A
124 11 57 61 111 123 climi2 φ m T m sup ran T * < < C j 1 m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
125 1z 1
126 11 rexuz3 1 a n a i = 1 n vol * . F i . G j vol * . G j A < C m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
127 125 126 ax-mp a n a i = 1 n vol * . F i . G j vol * . G j A < C m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
128 124 127 sylib φ m T m sup ran T * < < C j 1 m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
129 128 ralrimiva φ m T m sup ran T * < < C j 1 m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
130 fzfi 1 m Fin
131 rexfiuz 1 m Fin a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m j 1 m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
132 130 131 ax-mp a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m j 1 m a n a i = 1 n vol * . F i . G j vol * . G j A < C m
133 129 132 sylibr φ m T m sup ran T * < < C a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
134 11 rexuz3 1 a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
135 125 134 ax-mp a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
136 133 135 sylibr φ m T m sup ran T * < < C a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
137 11 r19.2uz a n a j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
138 136 137 syl φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
139 1 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m F : 2
140 2 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m Disj x . F x
141 5 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m vol * E
142 6 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m C +
143 7 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m G : 2
144 8 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m E ran . G
145 10 adantr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m sup ran T * < vol * E + C
146 simprll φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m m
147 simprlr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m T m sup ran T * < < C
148 eqid . G 1 m = . G 1 m
149 simprrl φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m n
150 simprrr φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m
151 2fveq3 i = z . F i = . F z
152 151 ineq1d i = z . F i . G j = . F z . G j
153 152 fveq2d i = z vol * . F i . G j = vol * . F z . G j
154 153 cbvsumv i = 1 n vol * . F i . G j = z = 1 n vol * . F z . G j
155 2fveq3 j = k . G j = . G k
156 155 ineq2d j = k . F z . G j = . F z . G k
157 156 fveq2d j = k vol * . F z . G j = vol * . F z . G k
158 157 sumeq2sdv j = k z = 1 n vol * . F z . G j = z = 1 n vol * . F z . G k
159 154 158 syl5eq j = k i = 1 n vol * . F i . G j = z = 1 n vol * . F z . G k
160 155 ineq1d j = k . G j A = . G k A
161 160 fveq2d j = k vol * . G j A = vol * . G k A
162 159 161 oveq12d j = k i = 1 n vol * . F i . G j vol * . G j A = z = 1 n vol * . F z . G k vol * . G k A
163 162 fveq2d j = k i = 1 n vol * . F i . G j vol * . G j A = z = 1 n vol * . F z . G k vol * . G k A
164 163 breq1d j = k i = 1 n vol * . F i . G j vol * . G j A < C m z = 1 n vol * . F z . G k vol * . G k A < C m
165 164 cbvralvw j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m k 1 m z = 1 n vol * . F z . G k vol * . G k A < C m
166 150 165 sylib φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m k 1 m z = 1 n vol * . F z . G k vol * . G k A < C m
167 eqid . F 1 n = . F 1 n
168 139 140 3 4 141 142 143 144 9 145 146 147 148 149 166 167 uniioombllem5 φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m vol * E A + vol * E A vol * E + 4 C
169 168 anassrs φ m T m sup ran T * < < C n j 1 m i = 1 n vol * . F i . G j vol * . G j A < C m vol * E A + vol * E A vol * E + 4 C
170 138 169 rexlimddv φ m T m sup ran T * < < C vol * E A + vol * E A vol * E + 4 C
171 56 170 rexlimddv φ vol * E A + vol * E A vol * E + 4 C