Theorem projlem28 9152

Description: Part of Lemma 3.6 of [Beran] p. 101. Boundedness to show F is a Cauchy sequence. Used by projlem29 9153.

Hypotheses

Ref	Expression
projlem27.1	|- A e. H~
projlem27.2	|- H e. CH
projlem27.3	|- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
projlem27.4	|- R = -usup(S, RR, < )
projlem27.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)))))
projlem28.6	|- D e. RR

Assertion

Ref	Expression
projlem28	|- (ph -> (0 < D -> E.z e. NN A.x e. NN A.y e. NN ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < D)))

Distinct variable groups:   v,u,x,y,z,w,A   u,H,v,x,z   x,D,y,z,w   x,F,y,w,z   x,R,y,z,w   ph,x,y,z

Proof of Theorem projlem28

Step	Hyp	Ref	Expression
1		breq1 2617	. . . . . . . . . . . . . . . 16 |- (z = if(z e. NN, z, 1) -> (z <_ x <-> if(z e. NN, z, 1) <_ x))
2		breq1 2617	. . . . . . . . . . . . . . . 16 |- (z = if(z e. NN, z, 1) -> (z <_ y <-> if(z e. NN, z, 1) <_ y))
3	1, 2	anbi12d 627	. . . . . . . . . . . . . . 15 |- (z = if(z e. NN, z, 1) -> ((z <_ x /\ z <_ y) <-> (if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y)))
4		opreq2 3960	. . . . . . . . . . . . . . . . 17 |- (z = if(z e. NN, z, 1) -> ((4 x. ((2 x. R) + 1)) / z) = ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))
5	4	fveq2d 3719	. . . . . . . . . . . . . . . 16 |- (z = if(z e. NN, z, 1) -> (sqr` ((4 x. ((2 x. R) + 1)) / z)) = (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1))))
6	5	breq2d 2625	. . . . . . . . . . . . . . 15 |- (z = if(z e. NN, z, 1) -> ((normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) <-> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))))
7	3, 6	imbi12d 625	. . . . . . . . . . . . . 14 |- (z = if(z e. NN, z, 1) -> (((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))) <-> ((if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1))))))
8	7	imbi2d 611	. . . . . . . . . . . . 13 |- (z = if(z e. NN, z, 1) -> (((ph /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)))) <-> ((ph /\ (x e. NN /\ y e. NN)) -> ((if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))))))
9		projlem27.1	. . . . . . . . . . . . . 14 |- A e. H~
10		projlem27.2	. . . . . . . . . . . . . 14 |- H e. CH
11		projlem27.3	. . . . . . . . . . . . . 14 |- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
12		projlem27.4	. . . . . . . . . . . . . 14 |- R = -usup(S, RR, < )
13		projlem27.5	. . . . . . . . . . . . . 14 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (normh` ((F` w) -h A)) /\ (normh` ((F` w) -h A)) < (R + (1 / w)))))
14		1nn 5890	. . . . . . . . . . . . . . 15 |- 1 e. NN
15	14	elimel 2390	. . . . . . . . . . . . . 14 |- if(z e. NN, z, 1) e. NN
16	9, 10, 11, 12, 13, 15	projlem27 9151	. . . . . . . . . . . . 13 |- ((ph /\ (x e. NN /\ y e. NN)) -> ((if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))))
17	8, 16	dedth 2379	. . . . . . . . . . . 12 |- (z e. NN -> ((ph /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)))))
18	17	exp3a 375	. . . . . . . . . . 11 |- (z e. NN -> (ph -> ((x e. NN /\ y e. NN) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))))
19	18	com12 11	. . . . . . . . . 10 |- (ph -> (z e. NN -> ((x e. NN /\ y e. NN) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))))
20	19	imp31 362	. . . . . . . . 9 |- (((ph /\ z e. NN) /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))
21	20	adantlr 393	. . . . . . . 8 |- ((((ph /\ z e. NN) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))
22		projlem28.6	. . . . . . . . . . . . . . . 16 |- D e. RR
23		axlttrn 5484	. . . . . . . . . . . . . . . 16 |- (((normh` ((F` x) -h (F` y))) e. RR /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) e. RR /\ D e. RR) -> (((normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) -> (normh` ((F` x) -h (F` y))) < D))
24	22, 23	mp3an3 903	. . . . . . . . . . . . . . 15 |- (((normh` ((F` x) -h (F` y))) e. RR /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) e. RR) -> (((normh` ((F` x) -h (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) -> (normh` ((F` x) -h (F` y))) < D))
25		hvsubclt 8826	. . . . . . . . . . . . . . . . . 18 |- (((F` x) e. H~ /\ (F` y) e. H~) -> ((F` x) -h (F` y)) e. H~)
26	13	projlem21 9145	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> (x e. NN -> (F` x) e. H))
27	26	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((ph /\ x e. NN) -> (F` x) e. H)
28	10	chel 9041	. . . . . . . . . . . . . . . . . . 19 |- ((F` x) e. H -> (F` x) e. H~)
29	27, 28	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ x e. NN) -> (F` x) e. H~)
30	13	projlem21 9145	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> (y e. NN -> (F` y) e. H))
31	30	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((ph /\ y e. NN) -> (F` y) e. H)
32	10	chel 9041	. . . . . . . . . . . . . . . . . . 19 |- ((F` y) e. H -> (F` y) e. H~)
33	31, 32	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ y e. NN) -> (F` y) e. H~)
34	25, 29, 33	syl2an 454	. . . . . . . . . . . . . . . . 17 |- (((ph /\ x e. NN) /\ (ph /\ y e. NN)) -> ((F` x) -h (F` y)) e. H~)
35	34	anandis 512	. . . . . . . . . . . . . . . 16 |- ((ph /\ (x e. NN /\ y e. NN)) -> ((F` x) -h (F` y)) e. H~)
36		normclt 8930	. . . . . . . . . . . . . . . 16 |- (((F` x) -h (F` y)) e. H~ -> (normh` ((F` x) -h (F` y))) e. RR)
37	35, 36	syl 10	. . . . . . . . . . . . . . 15 |- ((ph /\ (x e. NN /\ y e. NN)) -> (normh` ((F` x) -h (F` y))) e. RR