Metamath Proof Explorer


Theorem imasdsf1olem

Description: Lemma for imasdsf1o . (Contributed by Mario Carneiro, 21-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasdsf1o.u φ U = F 𝑠 R
imasdsf1o.v φ V = Base R
imasdsf1o.f φ F : V 1-1 onto B
imasdsf1o.r φ R Z
imasdsf1o.e E = dist R V × V
imasdsf1o.d D = dist U
imasdsf1o.m φ E ∞Met V
imasdsf1o.x φ X V
imasdsf1o.y φ Y V
imasdsf1o.w W = 𝑠 * 𝑠 * −∞
imasdsf1o.s S = h V × V 1 n | F 1 st h 1 = F X F 2 nd h n = F Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
imasdsf1o.t T = n ran g S 𝑠 * E g
Assertion imasdsf1olem φ F X D F Y = X E Y

Proof

Step Hyp Ref Expression
1 imasdsf1o.u φ U = F 𝑠 R
2 imasdsf1o.v φ V = Base R
3 imasdsf1o.f φ F : V 1-1 onto B
4 imasdsf1o.r φ R Z
5 imasdsf1o.e E = dist R V × V
6 imasdsf1o.d D = dist U
7 imasdsf1o.m φ E ∞Met V
8 imasdsf1o.x φ X V
9 imasdsf1o.y φ Y V
10 imasdsf1o.w W = 𝑠 * 𝑠 * −∞
11 imasdsf1o.s S = h V × V 1 n | F 1 st h 1 = F X F 2 nd h n = F Y i 1 n 1 F 2 nd h i = F 1 st h i + 1
12 imasdsf1o.t T = n ran g S 𝑠 * E g
13 f1ofo F : V 1-1 onto B F : V onto B
14 3 13 syl φ F : V onto B
15 eqid dist R = dist R
16 f1of F : V 1-1 onto B F : V B
17 3 16 syl φ F : V B
18 17 8 ffvelrnd φ F X B
19 17 9 ffvelrnd φ F Y B
20 1 2 14 4 15 6 18 19 11 5 imasdsval2 φ F X D F Y = sup n ran g S 𝑠 * E g * <
21 12 infeq1i sup T * < = sup n ran g S 𝑠 * E g * <
22 20 21 eqtr4di φ F X D F Y = sup T * <
23 xrsbas * = Base 𝑠 *
24 xrsadd + 𝑒 = + 𝑠 *
25 xrsex 𝑠 * V
26 25 a1i φ n g S 𝑠 * V
27 fzfid φ n g S 1 n Fin
28 difss * −∞ *
29 28 a1i φ n g S * −∞ *
30 xmetf E ∞Met V E : V × V *
31 ffn E : V × V * E Fn V × V
32 7 30 31 3syl φ E Fn V × V
33 xmetcl E ∞Met V f V g V f E g *
34 xmetge0 E ∞Met V f V g V 0 f E g
35 ge0nemnf f E g * 0 f E g f E g −∞
36 33 34 35 syl2anc E ∞Met V f V g V f E g −∞
37 eldifsn f E g * −∞ f E g * f E g −∞
38 33 36 37 sylanbrc E ∞Met V f V g V f E g * −∞
39 38 3expb E ∞Met V f V g V f E g * −∞
40 7 39 sylan φ f V g V f E g * −∞
41 40 ralrimivva φ f V g V f E g * −∞
42 ffnov E : V × V * −∞ E Fn V × V f V g V f E g * −∞
43 32 41 42 sylanbrc φ E : V × V * −∞
44 43 ad2antrr φ n g S E : V × V * −∞
45 11 ssrab3 S V × V 1 n
46 45 a1i φ n S V × V 1 n
47 46 sselda φ n g S g V × V 1 n
48 elmapi g V × V 1 n g : 1 n V × V
49 47 48 syl φ n g S g : 1 n V × V
50 fco E : V × V * −∞ g : 1 n V × V E g : 1 n * −∞
51 44 49 50 syl2anc φ n g S E g : 1 n * −∞
52 0re 0
53 rexr 0 0 *
54 renemnf 0 0 −∞
55 eldifsn 0 * −∞ 0 * 0 −∞
56 53 54 55 sylanbrc 0 0 * −∞
57 52 56 mp1i φ n g S 0 * −∞
58 xaddid2 x * 0 + 𝑒 x = x
59 xaddid1 x * x + 𝑒 0 = x
60 58 59 jca x * 0 + 𝑒 x = x x + 𝑒 0 = x
61 60 adantl φ n g S x * 0 + 𝑒 x = x x + 𝑒 0 = x
62 23 24 10 26 27 29 51 57 61 gsumress φ n g S 𝑠 * E g = W E g
63 10 23 ressbas2 * −∞ * * −∞ = Base W
64 28 63 ax-mp * −∞ = Base W
65 10 xrs10 0 = 0 W
66 10 xrs1cmn W CMnd
67 66 a1i φ n g S W CMnd
68 c0ex 0 V
69 68 a1i φ n g S 0 V
70 51 27 69 fdmfifsupp φ n g S finSupp 0 E g
71 64 65 67 27 51 70 gsumcl φ n g S W E g * −∞
72 62 71 eqeltrd φ n g S 𝑠 * E g * −∞
73 72 eldifad φ n g S 𝑠 * E g *
74 73 fmpttd φ n g S 𝑠 * E g : S *
75 74 frnd φ n ran g S 𝑠 * E g *
76 75 ralrimiva φ n ran g S 𝑠 * E g *
77 iunss n ran g S 𝑠 * E g * n ran g S 𝑠 * E g *
78 76 77 sylibr φ n ran g S 𝑠 * E g *
79 12 78 eqsstrid φ T *
80 infxrcl T * sup T * < *
81 79 80 syl φ sup T * < *
82 xmetcl E ∞Met V X V Y V X E Y *
83 7 8 9 82 syl3anc φ X E Y *
84 1nn 1
85 1ex 1 V
86 opex X Y V
87 85 86 f1osn 1 X Y : 1 1-1 onto X Y
88 f1of 1 X Y : 1 1-1 onto X Y 1 X Y : 1 X Y
89 87 88 ax-mp 1 X Y : 1 X Y
90 8 9 opelxpd φ X Y V × V
91 90 snssd φ X Y V × V
92 fss 1 X Y : 1 X Y X Y V × V 1 X Y : 1 V × V
93 89 91 92 sylancr φ 1 X Y : 1 V × V
94 7 elfvexd φ V V
95 94 94 xpexd φ V × V V
96 snex 1 V
97 elmapg V × V V 1 V 1 X Y V × V 1 1 X Y : 1 V × V
98 95 96 97 sylancl φ 1 X Y V × V 1 1 X Y : 1 V × V
99 93 98 mpbird φ 1 X Y V × V 1
100 op1stg X V Y V 1 st X Y = X
101 8 9 100 syl2anc φ 1 st X Y = X
102 101 fveq2d φ F 1 st X Y = F X
103 op2ndg X V Y V 2 nd X Y = Y
104 8 9 103 syl2anc φ 2 nd X Y = Y
105 104 fveq2d φ F 2 nd X Y = F Y
106 102 105 jca φ F 1 st X Y = F X F 2 nd X Y = F Y
107 25 a1i φ 𝑠 * V
108 snfi 1 Fin
109 108 a1i φ 1 Fin
110 28 a1i φ * −∞ *
111 xmetge0 E ∞Met V X V Y V 0 X E Y
112 7 8 9 111 syl3anc φ 0 X E Y
113 ge0nemnf X E Y * 0 X E Y X E Y −∞
114 83 112 113 syl2anc φ X E Y −∞
115 eldifsn X E Y * −∞ X E Y * X E Y −∞
116 83 114 115 sylanbrc φ X E Y * −∞
117 fconst6g X E Y * −∞ 1 × X E Y : 1 * −∞
118 116 117 syl φ 1 × X E Y : 1 * −∞
119 fcoconst E Fn V × V X Y V × V E 1 × X Y = 1 × E X Y
120 32 90 119 syl2anc φ E 1 × X Y = 1 × E X Y
121 85 86 xpsn 1 × X Y = 1 X Y
122 121 coeq2i E 1 × X Y = E 1 X Y
123 df-ov X E Y = E X Y
124 123 eqcomi E X Y = X E Y
125 124 sneqi E X Y = X E Y
126 125 xpeq2i 1 × E X Y = 1 × X E Y
127 120 122 126 3eqtr3g φ E 1 X Y = 1 × X E Y
128 127 feq1d φ E 1 X Y : 1 * −∞ 1 × X E Y : 1 * −∞
129 118 128 mpbird φ E 1 X Y : 1 * −∞
130 52 56 mp1i φ 0 * −∞
131 60 adantl φ x * 0 + 𝑒 x = x x + 𝑒 0 = x
132 23 24 10 107 109 110 129 130 131 gsumress φ 𝑠 * E 1 X Y = W E 1 X Y
133 fconstmpt 1 × X E Y = j 1 X E Y
134 127 133 eqtrdi φ E 1 X Y = j 1 X E Y
135 134 oveq2d φ W E 1 X Y = W j 1 X E Y
136 cmnmnd W CMnd W Mnd
137 66 136 mp1i φ W Mnd
138 84 a1i φ 1
139 eqidd j = 1 X E Y = X E Y
140 64 139 gsumsn W Mnd 1 X E Y * −∞ W j 1 X E Y = X E Y
141 137 138 116 140 syl3anc φ W j 1 X E Y = X E Y
142 132 135 141 3eqtrrd φ X E Y = 𝑠 * E 1 X Y
143 fveq1 g = 1 X Y g 1 = 1 X Y 1
144 85 86 fvsn 1 X Y 1 = X Y
145 143 144 eqtrdi g = 1 X Y g 1 = X Y
146 145 fveq2d g = 1 X Y 1 st g 1 = 1 st X Y
147 146 fveqeq2d g = 1 X Y F 1 st g 1 = F X F 1 st X Y = F X
148 145 fveq2d g = 1 X Y 2 nd g 1 = 2 nd X Y
149 148 fveqeq2d g = 1 X Y F 2 nd g 1 = F Y F 2 nd X Y = F Y
150 147 149 anbi12d g = 1 X Y F 1 st g 1 = F X F 2 nd g 1 = F Y F 1 st X Y = F X F 2 nd X Y = F Y
151 coeq2 g = 1 X Y E g = E 1 X Y
152 151 oveq2d g = 1 X Y 𝑠 * E g = 𝑠 * E 1 X Y
153 152 eqeq2d g = 1 X Y X E Y = 𝑠 * E g X E Y = 𝑠 * E 1 X Y
154 150 153 anbi12d g = 1 X Y F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g F 1 st X Y = F X F 2 nd X Y = F Y X E Y = 𝑠 * E 1 X Y
155 154 rspcev 1 X Y V × V 1 F 1 st X Y = F X F 2 nd X Y = F Y X E Y = 𝑠 * E 1 X Y g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
156 99 106 142 155 syl12anc φ g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
157 ovex X E Y V
158 eqid g S 𝑠 * E g = g S 𝑠 * E g
159 158 elrnmpt X E Y V X E Y ran g S 𝑠 * E g g S X E Y = 𝑠 * E g
160 157 159 ax-mp X E Y ran g S 𝑠 * E g g S X E Y = 𝑠 * E g
161 11 rexeqi g S X E Y = 𝑠 * E g g h V × V 1 n | F 1 st h 1 = F X F 2 nd h n = F Y i 1 n 1 F 2 nd h i = F 1 st h i + 1 X E Y = 𝑠 * E g
162 fveq1 h = g h 1 = g 1
163 162 fveq2d h = g 1 st h 1 = 1 st g 1
164 163 fveqeq2d h = g F 1 st h 1 = F X F 1 st g 1 = F X
165 fveq1 h = g h n = g n
166 165 fveq2d h = g 2 nd h n = 2 nd g n
167 166 fveqeq2d h = g F 2 nd h n = F Y F 2 nd g n = F Y
168 fveq1 h = g h i = g i
169 168 fveq2d h = g 2 nd h i = 2 nd g i
170 169 fveq2d h = g F 2 nd h i = F 2 nd g i
171 fveq1 h = g h i + 1 = g i + 1
172 171 fveq2d h = g 1 st h i + 1 = 1 st g i + 1
173 172 fveq2d h = g F 1 st h i + 1 = F 1 st g i + 1
174 170 173 eqeq12d h = g F 2 nd h i = F 1 st h i + 1 F 2 nd g i = F 1 st g i + 1
175 174 ralbidv h = g i 1 n 1 F 2 nd h i = F 1 st h i + 1 i 1 n 1 F 2 nd g i = F 1 st g i + 1
176 164 167 175 3anbi123d h = g F 1 st h 1 = F X F 2 nd h n = F Y i 1 n 1 F 2 nd h i = F 1 st h i + 1 F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
177 176 rexrab g h V × V 1 n | F 1 st h 1 = F X F 2 nd h n = F Y i 1 n 1 F 2 nd h i = F 1 st h i + 1 X E Y = 𝑠 * E g g V × V 1 n F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 X E Y = 𝑠 * E g
178 161 177 bitri g S X E Y = 𝑠 * E g g V × V 1 n F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 X E Y = 𝑠 * E g
179 oveq2 n = 1 1 n = 1 1
180 1z 1
181 fzsn 1 1 1 = 1
182 180 181 ax-mp 1 1 = 1
183 179 182 eqtrdi n = 1 1 n = 1
184 183 oveq2d n = 1 V × V 1 n = V × V 1
185 df-3an F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
186 ral0 i F 2 nd g i = F 1 st g i + 1
187 oveq1 n = 1 n 1 = 1 1
188 1m1e0 1 1 = 0
189 187 188 eqtrdi n = 1 n 1 = 0
190 189 oveq2d n = 1 1 n 1 = 1 0
191 fz10 1 0 =
192 190 191 eqtrdi n = 1 1 n 1 =
193 192 raleqdv n = 1 i 1 n 1 F 2 nd g i = F 1 st g i + 1 i F 2 nd g i = F 1 st g i + 1
194 186 193 mpbiri n = 1 i 1 n 1 F 2 nd g i = F 1 st g i + 1
195 194 biantrud n = 1 F 1 st g 1 = F X F 2 nd g n = F Y F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
196 2fveq3 n = 1 2 nd g n = 2 nd g 1
197 196 fveqeq2d n = 1 F 2 nd g n = F Y F 2 nd g 1 = F Y
198 197 anbi2d n = 1 F 1 st g 1 = F X F 2 nd g n = F Y F 1 st g 1 = F X F 2 nd g 1 = F Y
199 195 198 bitr3d n = 1 F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 F 1 st g 1 = F X F 2 nd g 1 = F Y
200 185 199 syl5bb n = 1 F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 F 1 st g 1 = F X F 2 nd g 1 = F Y
201 200 anbi1d n = 1 F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 X E Y = 𝑠 * E g F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
202 184 201 rexeqbidv n = 1 g V × V 1 n F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1 X E Y = 𝑠 * E g g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
203 178 202 syl5bb n = 1 g S X E Y = 𝑠 * E g g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
204 160 203 syl5bb n = 1 X E Y ran g S 𝑠 * E g g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g
205 204 rspcev 1 g V × V 1 F 1 st g 1 = F X F 2 nd g 1 = F Y X E Y = 𝑠 * E g n X E Y ran g S 𝑠 * E g
206 84 156 205 sylancr φ n X E Y ran g S 𝑠 * E g
207 eliun X E Y n ran g S 𝑠 * E g n X E Y ran g S 𝑠 * E g
208 206 207 sylibr φ X E Y n ran g S 𝑠 * E g
209 208 12 eleqtrrdi φ X E Y T
210 infxrlb T * X E Y T sup T * < X E Y
211 79 209 210 syl2anc φ sup T * < X E Y
212 12 eleq2i p T p n ran g S 𝑠 * E g
213 eliun p n ran g S 𝑠 * E g n p ran g S 𝑠 * E g
214 212 213 bitri p T n p ran g S 𝑠 * E g
215 158 elrnmpt p V p ran g S 𝑠 * E g g S p = 𝑠 * E g
216 215 elv p ran g S 𝑠 * E g g S p = 𝑠 * E g
217 176 11 elrab2 g S g V × V 1 n F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
218 217 simprbi g S F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
219 218 adantl φ n g S F 1 st g 1 = F X F 2 nd g n = F Y i 1 n 1 F 2 nd g i = F 1 st g i + 1
220 219 simp2d φ n g S F 2 nd g n = F Y
221 3 ad2antrr φ n g S F : V 1-1 onto B
222 f1of1 F : V 1-1 onto B F : V 1-1 B
223 221 222 syl φ n g S F : V 1-1 B
224 simplr φ n g S n
225 elfz1end n n 1 n
226 224 225 sylib φ n g S n 1 n
227 49 226 ffvelrnd φ n g S g n V × V
228 xp2nd g n V × V 2 nd g n V
229 227 228 syl φ n g S 2 nd g n V
230 9 ad2antrr φ n g S Y V
231 f1fveq F : V 1-1 B 2 nd g n V Y V F 2 nd g n = F Y 2 nd g n = Y
232 223 229 230 231 syl12anc φ n g S F 2 nd g n = F Y 2 nd g n = Y
233 220 232 mpbid φ n g S 2 nd g n = Y
234 233 oveq2d φ n g S X E 2 nd g n = X E Y
235 eleq1 m = 1 m 1 n 1 1 n
236 2fveq3 m = 1 2 nd g m = 2 nd g 1
237 236 oveq2d m = 1 X E 2 nd g m = X E 2 nd g 1
238 oveq2 m = 1 1 m = 1 1
239 238 182 eqtrdi m = 1 1 m = 1
240 239 reseq2d m = 1 E g 1 m = E g 1
241 240 oveq2d m = 1 W E g 1 m = W E g 1
242 237 241 breq12d m = 1 X E 2 nd g m W E g 1 m X E 2 nd g 1 W E g 1
243 235 242 imbi12d m = 1 m 1 n X E 2 nd g m W E g 1 m 1 1 n X E 2 nd g 1 W E g 1
244 243 imbi2d m = 1 φ n g S m 1 n X E 2 nd g m W E g 1 m φ n g S 1 1 n X E 2 nd g 1 W E g 1
245 eleq1 m = x m 1 n x 1 n
246 2fveq3 m = x 2 nd g m = 2 nd g x
247 246 oveq2d m = x X E 2 nd g m = X E 2 nd g x
248 oveq2 m = x 1 m = 1 x
249 248 reseq2d m = x E g 1 m = E g 1 x
250 249 oveq2d m = x W E g 1 m = W E g 1 x
251 247 250 breq12d m = x X E 2 nd g m W E g 1 m X E 2 nd g x W E g 1 x
252 245 251 imbi12d m = x m 1 n X E 2 nd g m W E g 1 m x 1 n X E 2 nd g x W E g 1 x
253 252 imbi2d m = x φ n g S m 1 n X E 2 nd g m W E g 1 m φ n g S x 1 n X E 2 nd g x W E g 1 x
254 eleq1 m = x + 1 m 1 n x + 1 1 n
255 2fveq3 m = x + 1 2 nd g m = 2 nd g x + 1
256 255 oveq2d m = x + 1 X E 2 nd g m = X E 2 nd g x + 1
257 oveq2 m = x + 1 1 m = 1 x + 1
258 257 reseq2d m = x + 1 E g 1 m = E g 1 x + 1
259 258 oveq2d m = x + 1 W E g 1 m = W E g 1 x + 1
260 256 259 breq12d m = x + 1 X E 2 nd g m W E g 1 m X E 2 nd g x + 1 W E g 1 x + 1
261 254 260 imbi12d m = x + 1 m 1 n X E 2 nd g m W E g 1 m x + 1 1 n X E 2 nd g x + 1 W E g 1 x + 1
262 261 imbi2d m = x + 1 φ n g S m 1 n X E 2 nd g m W E g 1 m φ n g S x + 1 1 n X E 2 nd g x + 1 W E g 1 x + 1
263 eleq1 m = n m 1 n n 1 n
264 2fveq3 m = n 2 nd g m = 2 nd g n
265 264 oveq2d m = n X E 2 nd g m = X E 2 nd g n
266 oveq2 m = n 1 m = 1 n
267 266 reseq2d m = n E g 1 m = E g 1 n
268 267 oveq2d m = n W E g 1 m = W E g 1 n
269 265 268 breq12d m = n X E 2 nd g m W E g 1 m X E 2 nd g n W E g 1 n
270 263 269 imbi12d m = n m 1 n X E 2 nd g m W E g 1 m n 1 n X E 2 nd g n W E g 1 n
271 270 imbi2d m = n φ n g S m 1 n X E 2 nd g m W E g 1 m φ n g S n 1 n X E 2 nd g n W E g 1 n
272 7 ad2antrr φ n g S E ∞Met V
273 8 ad2antrr φ n g S X V
274 nnuz = 1
275 224 274 eleqtrdi φ n g S n 1
276 eluzfz1 n 1 1 1 n
277 275 276 syl φ n g S 1 1 n
278 49 277 ffvelrnd φ n g S g 1 V × V
279 xp2nd g 1 V × V 2 nd g 1 V
280 278 279 syl φ n g S 2 nd g 1 V
281 xmetcl E ∞Met V X V 2 nd g 1 V X E 2 nd g 1 *
282 272 273 280 281 syl3anc φ n g S X E 2 nd g 1 *
283 282 xrleidd φ n g S X E 2 nd g 1 X E 2 nd g 1
284 137 ad2antrr φ n g S W Mnd
285 84 a1i φ n g S 1
286 44 278 ffvelrnd φ n g S E g 1 * −∞
287 2fveq3 j = 1 E g j = E g 1
288 64 287 gsumsn W Mnd 1 E g 1 * −∞ W j 1 E g j = E g 1
289 284 285 286 288 syl3anc φ n g S W j 1 E g j = E g 1
290 272 30 syl φ n g S E : V × V *
291 fcompt E : V × V * g : 1 n V × V E g = j 1 n E g j
292 290 49 291 syl2anc φ n g S E g = j 1 n E g j
293 292 reseq1d φ n g S E g 1 = j 1 n E g j 1
294 277 snssd φ n g S 1 1 n
295 294 resmptd φ n g S j 1 n E g j 1 = j 1 E g j
296 293 295 eqtrd φ n g S E g 1 = j 1 E g j
297 296 oveq2d φ n g S W E g 1 = W j 1 E g j
298 df-ov X E 2 nd g 1 = E X 2 nd g 1
299 1st2nd2 g 1 V × V g 1 = 1 st g 1 2 nd g 1
300 278 299 syl φ n g S g 1 = 1 st g 1 2 nd g 1
301 219 simp1d φ n g S F 1 st g 1 = F X
302 xp1st g 1 V × V 1 st g 1 V
303 278 302 syl φ n g S 1 st g 1 V
304 f1fveq F : V 1-1 B 1 st g 1 V X V F 1 st g 1 = F X 1 st g 1 = X
305 223 303 273 304 syl12anc φ n g S F 1 st g 1 = F X 1 st g 1 = X
306 301 305 mpbid φ n g S 1 st g 1 = X
307 306 opeq1d φ n g S 1 st g 1 2 nd g 1 = X 2 nd g 1
308 300 307 eqtr2d φ n g S X 2 nd g 1 = g 1
309 308 fveq2d φ n g S E X 2 nd g 1 = E g 1
310 298 309 syl5eq φ n g S X E 2 nd g 1 = E g 1
311 289 297 310 3eqtr4d φ n g S W E g 1 = X E 2 nd g 1
312 283 311 breqtrrd φ n g S X E 2 nd g 1 W E g 1
313 312 a1d φ n g S 1 1 n X E 2 nd g 1 W E g 1
314 simprl φ n g S x x + 1 1 n x
315 314 274 eleqtrdi φ n g S x x + 1 1 n x 1
316 simprr φ n g S x x + 1 1 n x + 1 1 n
317 peano2fzr x 1 x + 1 1 n x 1 n
318 315 316 317 syl2anc φ n g S x x + 1 1 n x 1 n
319 318 expr φ n g S x x + 1 1 n x 1 n
320 319 imim1d φ n g S x x 1 n X E 2 nd g x W E g 1 x x + 1 1 n X E 2 nd g x W E g 1 x
321 272 adantr φ n g S x x + 1 1 n E ∞Met V
322 273 adantr φ n g S x x + 1 1 n X V
323 49 adantr φ n g S x x + 1 1 n g : 1 n V × V
324 323 318 ffvelrnd φ n g S x x + 1 1 n g x V × V
325 xp2nd g x V × V 2 nd g x V
326 324 325 syl φ n g S x x + 1 1 n 2 nd g x V
327 xmetcl E ∞Met V X V 2 nd g x V X E 2 nd g x *
328 321 322 326 327 syl3anc φ n g S x x + 1 1 n X E 2 nd g x *
329 66 a1i φ n g S x x + 1 1 n W CMnd
330 fzfid φ n g S x x + 1 1 n 1 x Fin
331 51 adantr φ n g S x x + 1 1 n E g : 1 n * −∞
332 fzsuc x 1 1 x + 1 = 1 x x + 1
333 315 332 syl φ n g S x x + 1 1 n 1 x + 1 = 1 x x + 1
334 elfzuz3 x + 1 1 n n x + 1
335 334 ad2antll φ n g S x x + 1 1 n n x + 1
336 fzss2 n x + 1 1 x + 1 1 n
337 335 336 syl φ n g S x x + 1 1 n 1 x + 1 1 n
338 333 337 eqsstrrd φ n g S x x + 1 1 n 1 x x + 1 1 n
339 338 unssad φ n g S x x + 1 1 n 1 x 1 n
340 331 339 fssresd φ n g S x x + 1 1 n E g 1 x : 1 x * −∞
341 68 a1i φ n g S x x + 1 1 n 0 V
342 340 330 341 fdmfifsupp φ n g S x x + 1 1 n finSupp 0 E g 1 x
343 64 65 329 330 340 342 gsumcl φ n g S x x + 1 1 n W E g 1 x * −∞
344 343 eldifad φ n g S x x + 1 1 n W E g 1 x *
345 321 30 syl φ n g S x x + 1 1 n E : V × V *
346 323 316 ffvelrnd φ n g S x x + 1 1 n g x + 1 V × V
347 345 346 ffvelrnd φ n g S x x + 1 1 n E g x + 1 *
348 xleadd1a X E 2 nd g x * W E g 1 x * E g x + 1 * X E 2 nd g x W E g 1 x X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1
349 348 ex X E 2 nd g x * W E g 1 x * E g x + 1 * X E 2 nd g x W E g 1 x X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1
350 328 344 347 349 syl3anc φ n g S x x + 1 1 n X E 2 nd g x W E g 1 x X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1
351 xp2nd g x + 1 V × V 2 nd g x + 1 V
352 346 351 syl φ n g S x x + 1 1 n 2 nd g x + 1 V
353 xmettri E ∞Met V X V 2 nd g x + 1 V 2 nd g x V X E 2 nd g x + 1 X E 2 nd g x + 𝑒 2 nd g x E 2 nd g x + 1
354 321 322 352 326 353 syl13anc φ n g S x x + 1 1 n X E 2 nd g x + 1 X E 2 nd g x + 𝑒 2 nd g x E 2 nd g x + 1
355 1st2nd2 g x + 1 V × V g x + 1 = 1 st g x + 1 2 nd g x + 1
356 346 355 syl φ n g S x x + 1 1 n g x + 1 = 1 st g x + 1 2 nd g x + 1
357 2fveq3 i = x 2 nd g i = 2 nd g x
358 357 fveq2d i = x F 2 nd g i = F 2 nd g x
359 fvoveq1 i = x g i + 1 = g x + 1
360 359 fveq2d i = x 1 st g i + 1 = 1 st g x + 1
361 360 fveq2d i = x F 1 st g i + 1 = F 1 st g x + 1
362 358 361 eqeq12d i = x F 2 nd g i = F 1 st g i + 1 F 2 nd g x = F 1 st g x + 1
363 219 simp3d φ n g S i 1 n 1 F 2 nd g i = F 1 st g i + 1
364 363 adantr φ n g S x x + 1 1 n i 1 n 1 F 2 nd g i = F 1 st g i + 1
365 nnz x x
366 365 ad2antrl φ n g S x x + 1 1 n x
367 eluzp1m1 x n x + 1 n 1 x
368 366 335 367 syl2anc φ n g S x x + 1 1 n n 1 x
369 elfzuzb x 1 n 1 x 1 n 1 x
370 315 368 369 sylanbrc φ n g S x x + 1 1 n x 1 n 1
371 362 364 370 rspcdva φ n g S x x + 1 1 n F 2 nd g x = F 1 st g x + 1
372 223 adantr φ n g S x x + 1 1 n F : V 1-1 B
373 xp1st g x + 1 V × V 1 st g x + 1 V
374 346 373 syl φ n g S x x + 1 1 n 1 st g x + 1 V
375 f1fveq F : V 1-1 B 2 nd g x V 1 st g x + 1 V F 2 nd g x = F 1 st g x + 1 2 nd g x = 1 st g x + 1
376 372 326 374 375 syl12anc φ n g S x x + 1 1 n F 2 nd g x = F 1 st g x + 1 2 nd g x = 1 st g x + 1
377 371 376 mpbid φ n g S x x + 1 1 n 2 nd g x = 1 st g x + 1
378 377 opeq1d φ n g S x x + 1 1 n 2 nd g x 2 nd g x + 1 = 1 st g x + 1 2 nd g x + 1
379 356 378 eqtr4d φ n g S x x + 1 1 n g x + 1 = 2 nd g x 2 nd g x + 1
380 379 fveq2d φ n g S x x + 1 1 n E g x + 1 = E 2 nd g x 2 nd g x + 1
381 df-ov 2 nd g x E 2 nd g x + 1 = E 2 nd g x 2 nd g x + 1
382 380 381 eqtr4di φ n g S x x + 1 1 n E g x + 1 = 2 nd g x E 2 nd g x + 1
383 382 oveq2d φ n g S x x + 1 1 n X E 2 nd g x + 𝑒 E g x + 1 = X E 2 nd g x + 𝑒 2 nd g x E 2 nd g x + 1
384 354 383 breqtrrd φ n g S x x + 1 1 n X E 2 nd g x + 1 X E 2 nd g x + 𝑒 E g x + 1
385 xmetcl E ∞Met V X V 2 nd g x + 1 V X E 2 nd g x + 1 *
386 321 322 352 385 syl3anc φ n g S x x + 1 1 n X E 2 nd g x + 1 *
387 328 347 xaddcld φ n g S x x + 1 1 n X E 2 nd g x + 𝑒 E g x + 1 *
388 344 347 xaddcld φ n g S x x + 1 1 n W E g 1 x + 𝑒 E g x + 1 *
389 xrletr X E 2 nd g x + 1 * X E 2 nd g x + 𝑒 E g x + 1 * W E g 1 x + 𝑒 E g x + 1 * X E 2 nd g x + 1 X E 2 nd g x + 𝑒 E g x + 1 X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1 X E 2 nd g x + 1 W E g 1 x + 𝑒 E g x + 1
390 386 387 388 389 syl3anc φ n g S x x + 1 1 n X E 2 nd g x + 1 X E 2 nd g x + 𝑒 E g x + 1 X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1 X E 2 nd g x + 1 W E g 1 x + 𝑒 E g x + 1
391 384 390 mpand φ n g S x x + 1 1 n X E 2 nd g x + 𝑒 E g x + 1 W E g 1 x + 𝑒 E g x + 1 X E 2 nd g x + 1 W E g 1 x + 𝑒 E g x + 1
392 350 391 syld φ n g S x x + 1 1 n X E 2 nd g x W E g 1 x X E 2 nd g x + 1 W E g 1 x + 𝑒 E g x + 1
393 xrex * V
394 393 difexi * −∞ V
395 10 24 ressplusg * −∞ V + 𝑒 = + W
396 394 395 ax-mp + 𝑒 = + W
397 44 ad2antrr φ n g S x x + 1 1 n j 1 x E : V × V * −∞
398 fzelp1 j 1 x j 1 x + 1
399 49 ad2antrr φ n g S x x + 1 1 n j 1 x + 1 g : 1 n V × V
400 337 sselda φ n g S x x + 1 1 n j 1 x + 1 j 1 n
401 399 400 ffvelrnd φ n g S x x + 1 1 n j 1 x + 1 g j V × V
402 398 401 sylan2 φ n g S x x + 1 1 n j 1 x g j V × V
403 397 402 ffvelrnd φ n g S x x + 1 1 n j 1 x E g j * −∞
404 fzp1disj 1 x x + 1 =
405 404 a1i φ n g S x x + 1 1 n 1 x x + 1 =
406 disjsn 1 x x + 1 = ¬ x + 1 1 x
407 405 406 sylib φ n g S x x + 1 1 n ¬ x + 1 1 x
408 44 adantr φ n g S x x + 1 1 n E : V × V * −∞
409 408 346 ffvelrnd φ n g S x x + 1 1 n E g x + 1 * −∞
410 2fveq3 j = x + 1 E g j = E g x + 1
411 64 396 329 330 403 316 407 409 410 gsumunsn φ n g S x x + 1 1 n W j 1 x x + 1 E g j = W j = 1 x E g j + 𝑒 E g x + 1
412 292 adantr φ n g S x x + 1 1 n E g = j 1 n E g j
413 412 333 reseq12d φ n g S x x + 1 1 n E g 1 x + 1 = j 1 n E g j 1 x x + 1
414 338 resmptd φ n g S x x + 1 1 n j 1 n E g j 1 x x + 1 = j 1 x x + 1 E g j
415 413 414 eqtrd φ n g S x x + 1 1 n E g 1 x + 1 = j 1 x x + 1 E g j
416 415 oveq2d φ n g S x x + 1 1 n W E g 1 x + 1 = W j 1 x x + 1 E g j
417 412 reseq1d φ n g S x x + 1 1 n E g 1 x = j 1 n E g j 1 x
418 339 resmptd φ n g S x x + 1 1 n j 1 n E g j 1 x = j 1 x E g j
419 417 418 eqtrd φ n g S x x + 1 1 n E g 1 x = j 1 x E g j
420 419 oveq2d φ n g S x x + 1 1 n W E g 1 x = W j = 1 x E g j
421 420 oveq1d φ n g S x x + 1 1 n W E g 1 x + 𝑒 E g x + 1 = W j = 1 x E g j + 𝑒 E g x + 1
422 411 416 421 3eqtr4d φ n g S x x + 1 1 n W E g 1 x + 1 = W E g 1 x + 𝑒 E g x + 1
423 422 breq2d φ n g S x x + 1 1 n X E 2 nd g x + 1 W E g 1 x + 1 X E 2 nd g x + 1 W E g 1 x + 𝑒 E g x + 1
424 392 423 sylibrd φ n g S x x + 1 1 n X E 2 nd g x W E g 1 x X E 2 nd g x + 1 W E g 1 x + 1
425 320 424 animpimp2impd x φ n g S x 1 n X E 2 nd g x W E g 1 x φ n g S x + 1 1 n X E 2 nd g x + 1 W E g 1 x + 1
426 244 253 262 271 313 425 nnind n φ n g S n 1 n X E 2 nd g n W E g 1 n
427 224 426 mpcom φ n g S n 1 n X E 2 nd g n W E g 1 n
428 226 427 mpd φ n g S X E 2 nd g n W E g 1 n
429 234 428 eqbrtrrd φ n g S X E Y W E g 1 n
430 ffn E g : 1 n * −∞ E g Fn 1 n
431 fnresdm E g Fn 1 n E g 1 n = E g
432 51 430 431 3syl φ n g S E g 1 n = E g
433 432 oveq2d φ n g S W E g 1 n = W E g
434 62 433 eqtr4d φ n g S 𝑠 * E g = W E g 1 n
435 429 434 breqtrrd φ n g S X E Y 𝑠 * E g
436 breq2 p = 𝑠 * E g X E Y p X E Y 𝑠 * E g
437 435 436 syl5ibrcom φ n g S p = 𝑠 * E g X E Y p
438 437 rexlimdva φ n g S p = 𝑠 * E g X E Y p
439 216 438 syl5bi φ n p ran g S 𝑠 * E g X E Y p
440 439 rexlimdva φ n p ran g S 𝑠 * E g X E Y p
441 214 440 syl5bi φ p T X E Y p
442 441 ralrimiv φ p T X E Y p
443 infxrgelb T * X E Y * X E Y sup T * < p T X E Y p
444 79 83 443 syl2anc φ X E Y sup T * < p T X E Y p
445 442 444 mpbird φ X E Y sup T * <
446 81 83 211 445 xrletrid φ sup T * < = X E Y
447 22 446 eqtrd φ F X D F Y = X E Y