Theorem projlem26 9206

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 9211.

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(normh` (v -h A))}
projlem26.4	|- R = -usup(S, RR, < )
projlem26.5	|- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (normh` ((F` w) -h A)) /\ (normh` ((F` w) -h A)) < (R + (1 / w)))))
projlem26.6	|- G = {<.x, y>. | (x e. NN /\ y = (normh` ((F` x) -h A)))}

Assertion

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

Distinct variable groups:   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		gt0ne0t 5630	. . . . . . . . 9 |- ((z e. RR /\ 0 < z) -> z =/= 0)
2		rerecclt 5805	. . . . . . . . 9 |- ((z e. RR /\ z =/= 0) -> (1 / z) e. RR)
3	1, 2	syldan 469	. . . . . . . 8 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
4		arch 6073	. . . . . . . 8 |- ((1 / z) e. RR -> E.f e. NN (1 / z) < f)
5	3, 4	syl 10	. . . . . . 7 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / z) < f)
6		ltrec1t 5890	. . . . . . . . 9 |- (((z e. RR /\ 0 < z) /\ (f e. RR /\ 0 < f)) -> ((1 / z) < f <-> (1 / f) < z))
7		nnret 5931	. . . . . . . . . 10 |- (f e. NN -> f e. RR)
8		nngt0t 5948	. . . . . . . . . 10 |- (f e. NN -> 0 < f)
9	7, 8	jca 288	. . . . . . . . 9 |- (f e. NN -> (f e. RR /\ 0 < f))
10	6, 9	sylan2 453	. . . . . . . 8 |- (((z e. RR /\ 0 < z) /\ f e. NN) -> ((1 / z) < f <-> (1 / f) < z))
11	10	rexbidva 1663	. . . . . . 7 |- ((z e. RR /\ 0 < z) -> (E.f e. NN (1 / z) < f <-> E.f e. NN (1 / f) < z))
12	5, 11	mpbid 195	. . . . . 6 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / f) < z)
13	12	adantl 390	. . . . 5 |- ((ph /\ (z e. RR /\ 0 < z)) -> E.f e. NN (1 / f) < z)
14		lerect 5887	. . . . . . . . . . . . . . . . . . . . 21 |- (((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g)) -> (f <_ g <-> (1 / g) <_ (1 / f)))
15		nnret 5931	. . . . . . . . . . . . . . . . . . . . . 22 |- (g e. NN -> g e. RR)
16		nngt0t 5948	. . . . . . . . . . . . . . . . . . . . . 22 |- (g e. NN -> 0 < g)
17	15, 16	jca 288	. . . . . . . . . . . . . . . . . . . . 21 |- (g e. NN -> (g e. RR /\ 0 < g))
18	14, 9, 17	syl2an 456	. . . . . . . . . . . . . . . . . . . 20 |- ((f e. NN /\ g e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
19	18	ancoms 438	. . . . . . . . . . . . . . . . . . 19 |- ((g e. NN /\ f e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
20	19	3adant3 801	. . . . . . . . . . . . . . . . . 18 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g <-> (1 / g) <_ (1 / f)))
21		lelttrt 5535	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> (((1 / g) <_ (1 / f) /\ (1 / f) < z) -> (1 / g) < z))
22	21	exp3a 376	. . . . . . . . . . . . . . . . . . . 20 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
23		rerecclt 5805	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. RR /\ f =/= 0) -> (1 / f) e. RR)
24		nnne0t 5951	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. NN -> f =/= 0)
25	23, 7, 24	sylanc 473	. . . . . . . . . . . . . . . . . . . 20 |- (f e. NN -> (1 / f) e. RR)
26	22, 25	syl3an2 862	. . . . . . . . . . . . . . . . . . 19 |- (((1 / g) e. RR /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
27		rerecclt 5805	. . . . . . . . . . . . . . . . . . . 20 |- ((g e. RR /\ g =/= 0) -> (1 / g) e. RR)
28		nnne0t 5951	. . . . . . . . . . . . . . . . . . . 20 |- (g e. NN -> g =/= 0)
29	27, 15, 28	sylanc 473	. . . . . . . . . . . . . . . . . . 19 |- (g e. NN -> (1 / g) e. RR)
30	26, 29	syl3an1 861	. . . . . . . . . . . . . . . . . 18 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
31	20, 30	sylbid 203	. . . . . . . . . . . . . . . . 17 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g -> ((1 / f) < z -> (1 / g) < z)))
32	31	com23 32	. . . . . . . . . . . . . . . 16 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / f) < z -> (f <_ g -> (1 / g) < z)))
33	32	imp3a 361	. . . . . . . . . . . . . . 15 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
34	33	3exp 834	. . . . . . . . . . . . . 14 |- (g e. NN -> (f e. NN -> (z e. RR -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
35	34	com13 33	. . . . . . . . . . . . 13 |- (z e. RR -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
36	35	ad2antrl 408	. . . . . . . . . . . 12 |- ((ph /\ (z e. RR /\ 0 < z)) -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
37	36	imp31 362	. . . . . . . . . . 11 |- ((((ph /\ (z e. RR /\ 0 < z)) /\ f e. NN) /\ g e. NN) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
38		axlttrn 5516	. . . . . . . . . . . . . . . 16 |- (((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR /\ z e. RR) -> (((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((normh` ((F` g) -h A)) - R)) < z))
39	38	3expa 835	. . . . . . . . . . . . . . 15 |- ((((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> (((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((normh` ((F` g) -h A)) - R)) < z))
40	39	exp3a 376	. . . . . . . . . . . . . 14 |- ((((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> ((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) -> ((1 / g) < z -> (abs` ((normh` ((F` g) -h A)) - R)) < z)))
41		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H /\ g e. NN) -> (F` g) e. H)
42		projlem26.5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (normh` ((F` w) -h A)) /\ (normh` ((F` w) -h A)) < (R + (1 / w)))))
43	42	pm3.26bi 322	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (ph -> F:NN-->H)
44	41, 43	sylan 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((ph /\ g e. NN) -> (F` g) e. H)
45		projlem26.2	. . . . . . . . . . . . . . . . . . . . . . . 24 |- H e. CH
46	45	chel 9097	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` g) e. H -> (F` g) e. H~)
47	44, 46	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((ph /\ g e. NN) -> (F` g) e. H~)
48		projlem26.1	. . . . . . . . . . . . . . . . . . . . . 22 |- A e. H~
49	47, 48	jctir 293	. . . . . . . . . . . . . . . . . . . . 21 |- ((ph /\ g e. NN) -> ((F` g) e. H~ /\ A e. H~))
50		hvsubclt 8882	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` g) e. H~ /\ A e. H~) -> ((F` g) -h A) e. H~)
51		normclt 8986	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` g) -h A) e. H~ -> (normh` ((F` g) -h A)) e. RR)
52	49, 50, 51	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- ((ph /\ g e. NN) -> (normh` ((F` g) -h A)) e. RR)
53		projlem26.3	. . . . . . . . . . . . . . . . . . . . 21 |- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
54		projlem26.4	. . . . . . . . . . . . . . . . . . . . 21 |- R = -usup(S, RR, < )
55	48, 45, 53, 54	projlem11 9191	. . . . . . . . . . . . . . . . . . . 20 |- R e. RR
56	52, 55	jctir 293	. . . . . . . . . . . . . . . . . . 19 |- ((ph /\ g e. NN) -> ((normh` ((F` g) -h A)) e. RR /\ R e. RR))
57		resubclt 5450	. . . . . . . . . . . . . . . . . . 19 |- (((normh` ((F` g) -h A)) e. RR /\ R e. RR) -> ((normh` ((F` g) -h A)) - R) e. RR)
58	56, 57	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ g e. NN) -> ((normh` ((F` g) -h A)) - R) e. RR)
59	58	recnd 5327	. . . . . . . . . . . . . . . . 17 |- ((ph /\ g e. NN) -> ((normh`