Theorem projlem26 5218

Description: Part of Lemma 3.6 of [Beran] p. 101. The real sequence G (Beran's "{||yn-x0||}") converges to the infimum of norms. Used by projlem31 5223.

Hypotheses

Ref	Expression
projlem26.1	|- A e. H~
projlem26.2	|- H e. CH
projlem26.3	|- S = {u e. RR | E.v e. H u = -u(norm` (v -v A))}
projlem26.4	|- R = -usup(S, RR, < )
projlem26.5	|- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (norm` ((F` w) -v A)) /\ (norm` ((F` w) -v A)) < (R + (1 / w)))))
projlem26.6	|- G = {<.x, y>. | (x e. NN /\ y = (norm` ((F` x) -v A)))}

Assertion

Ref	Expression
projlem26	|- (ph -> G ~~> R)

Distinct variable group(s):   w,u,v,x,y,A   w,F,x,y   w,R   ph,x   u,H,v

Proof of Theorem projlem26

Step	Hyp	Ref	Expression
1		projlem26.5	. . . . . 6 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (norm` ((F` w) -v A)) /\ (norm` ((F` w) -v A)) < (R + (1 / w)))))
2	1	pm3.26bd 259	. . . . 5 |- (ph -> F:NN-->H)
3		projlem26.2	. . . . . . 7 |- H e. CH
4	3	chssi 5136	. . . . . 6 |- H (_ H~
5		fss 2759	. . . . . 6 |- ((F:NN-->H /\ H (_ H~) -> F:NN-->H~)
6	4, 5	mpan2 519	. . . . 5 |- (F:NN-->H -> F:NN-->H~)
7		projlem26.6	. . . . . 6 |- G = {<.x, y>. | (x e. NN /\ y = (norm` ((F` x) -v A)))}
8		projlem26.1	. . . . . 6 |- A e. H~
9	7, 8	projlem24 5216	. . . . 5 |- (F:NN-->H~ -> G:NN-->CC)
10	2, 6, 9	3syl 21	. . . 4 |- (ph -> G:NN-->CC)
11		projlem26.3	. . . . . 6 |- S = {u e. RR | E.v e. H u = -u(norm` (v -v A))}
12		projlem26.4	. . . . . 6 |- R = -usup(S, RR, < )
13	8, 3, 11, 12	projlem11 5203	. . . . 5 |- R e. RR
14	13	recn 4098	. . . 4 |- R e. CC
15	10, 14	jctir 241	. . 3 |- (ph -> (G:NN-->CC /\ R e. CC))
16		redivclt 4276	. . . . . . . . . 10 |- (((1 e. RR /\ z e. RR) /\ z =/= 0) -> (1 / z) e. RR)
17		pm3.26 256	. . . . . . . . . . 11 |- ((z e. RR /\ 0 < z) -> z e. RR)
18		ax1re 4064	. . . . . . . . . . 11 |- 1 e. RR
19	17, 18	jctil 240	. . . . . . . . . 10 |- ((z e. RR /\ 0 < z) -> (1 e. RR /\ z e. RR))
20		gt0ne0t 4346	. . . . . . . . . . 11 |- (z e. RR -> (0 < z -> z =/= 0))
21	20	imp 277	. . . . . . . . . 10 |- ((z e. RR /\ 0 < z) -> z =/= 0)
22	16, 19, 21	sylanc 361	. . . . . . . . 9 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
23		arch 4521	. . . . . . . . 9 |- ((1 / z) e. RR -> E.f e. NN (1 / z) < f)
24	22, 23	syl 12	. . . . . . . 8 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / z) < f)
25		ltdiv23t 4419	. . . . . . . . . . 11 |- ((1 e. RR /\ z e. RR /\ f e. RR) -> ((0 < z /\ 0 < f) -> ((1 / z) < f <-> (1 / f) < z)))
26	18, 25	mp3an1 639	. . . . . . . . . 10 |- ((z e. RR /\ f e. RR) -> ((0 < z /\ 0 < f) -> ((1 / z) < f <-> (1 / f) < z)))
27		nnret 4427	. . . . . . . . . . 11 |- (f e. NN -> f e. RR)
28	17, 27	anim12i 268	. . . . . . . . . 10 |- (((z e. RR /\ 0 < z) /\ f e. NN) -> (z e. RR /\ f e. RR))
29		pm3.27 260	. . . . . . . . . . 11 |- ((z e. RR /\ 0 < z) -> 0 < z)
30		nngt0t 4441	. . . . . . . . . . 11 |- (f e. NN -> 0 < f)
31	29, 30	anim12i 268	. . . . . . . . . 10 |- (((z e. RR /\ 0 < z) /\ f e. NN) -> (0 < z /\ 0 < f))
32	26, 28, 31	sylc 62	. . . . . . . . 9 |- (((z e. RR /\ 0 < z) /\ f e. NN) -> ((1 / z) < f <-> (1 / f) < z))
33	32	birexdva 1216	. . . . . . . 8 |- ((z e. RR /\ 0 < z) -> (E.f e. NN (1 / z) < f <-> E.f e. NN (1 / f) < z))
34	24, 33	mpbid 170	. . . . . . 7 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / f) < z)
35	34	adantl 305	. . . . . 6 |- ((ph /\ (z e. RR /\ 0 < z)) -> E.f e. NN (1 / f) < z)
36		lerect 4418	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f e. RR /\ g e. RR) -> ((0 < f /\ 0 < g) -> (f <_ g <-> (1 / g) <_ (1 / f))))
37		nnret 4427	. . . . . . . . . . . . . . . . . . . . . . 23 |- (g e. NN -> g e. RR)
38	27, 37	anim12i 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f e. NN /\ g e. NN) -> (f e. RR /\ g e. RR))
39		nngt0t 4441	. . . . . . . . . . . . . . . . . . . . . . 23 |- (g e. NN -> 0 < g)
40	30, 39	anim12i 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f e. NN /\ g e. NN) -> (0 < f /\ 0 < g))
41	36, 38, 40	sylc 62	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. NN /\ g e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
42	41	ancoms 334	. . . . . . . . . . . . . . . . . . . 20 |- ((g e. NN /\ f e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
43	42	3adant3 599	. . . . . . . . . . . . . . . . . . 19 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g <-> (1 / g) <_ (1 / f)))
44		lelttrt 4289	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> (((1 / g) <_ (1 / f) /\ (1 / f) < z) -> (1 / g) < z))
45	44	exp3a 292	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
46		redivclt 4276	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1 e. RR /\ f e. RR) /\ f =/= 0) -> (1 / f) e. RR)
47	27, 18	jctil 240	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. NN -> (1 e. RR /\ f e. RR))
48		nnne0t 4444	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. NN -> f =/= 0)
49	46, 47, 48	sylanc 361	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. NN -> (1 / f) e. RR)
50	45, 49	syl3an2 620	. . . . . . . . . . . . . . . . . . . 20 |- (((1 / g) e. RR /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
51		redivclt 4276	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 e. RR /\ g e. RR) /\ g =/= 0) -> (1 / g) e. RR)
52	37, 18	jctil 240	. . . . . . . . . . . . . . . . . . . . 21 |- (g e. NN -> (1 e. RR /\ g e. RR))
53		nnne0t 4444	. . . . . . . . . . . . . . . . . . . . 21 |- (g e. NN -> g =/= 0)
54	51, 52, 53	sylanc 361	. . . . . . . . . . . . . . . . . . . 20 |- (g e. NN -> (1 / g) e. RR)
55	50, 54	syl3an1 619	. . . . . . . . . . . . . . . . . . 19 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
56	43, 55	sylbid 178	. . . . . . . . . . . . . . . . . 18 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g -> ((1 / f) < z -> (1 / g) < z)))
57	56	com23 32	. . . . . . . . . . . . . . . . 17 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / f) < z -> (f <_ g -> (1 / g) < z)))
58	57	imp3a 279	. . . . . . . . . . . . . . . 16 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
59	58	3exp 611	. . . . . . . . . . . . . . 15 |- (g e. NN -> (f e. NN -> (z e. RR -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
60	59	com13 33	. . . . . . . . . . . . . 14 |- (z e. RR -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
61	60	ad2antrl 322	. . . . . . . . . . . . 13 |- ((ph /\ (z e. RR /\ 0 < z)) -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
62	61	imp31 280	. . . . . . . . . . . 12 |- ((((ph /\ (z e. RR /\ 0 < z)) /\ f e. NN) /\ g e. NN) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
63		axlttrn 4084	. . . . . . . . . . . . . . . . 17 |- (((abs` ((norm` ((F` g) -v A)) - R)) e. RR /\ (1 / g) e. RR /\ z e. RR) -> (((abs` ((norm` ((F` g) -v A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((norm` ((F` g) -v A)) - R)) < z))
64	63	3expa 612	. . . . . . . . . . . . . . . 16 |- ((((abs` ((norm` ((F` g) -v A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> (((abs` ((norm` ((F` g) -v A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((norm` ((F` g) -v A)) - R)) < z))
65	64	exp3a 292	. . . . . . . . . . . . . . 15 |- ((((abs` ((norm` ((F` g) -v A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> ((abs` ((norm` ((F` g) -v A)) - R)) < (1 / g) -> ((1 / g) < z -> (abs` ((norm` ((F` g) -v A)) -