Theorem projlem28 5220

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

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(norm` (v -v A))}
projlem27.4	|- R = -usup(S, RR, < )
projlem27.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)))))
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) -> (norm` ((F` x) -v (F` y))) < D)))

Distinct variable group(s):   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 2065	. . . . . . . . . . . . . . . 16 |- (z = if(z e. NN, z, 1) -> (z <_ x <-> if(z e. NN, z, 1) <_ x))
2		breq1 2065	. . . . . . . . . . . . . . . 16 |- (z = if(z e. NN, z, 1) -> (z <_ y <-> if(z e. NN, z, 1) <_ y))
3	1, 2	anbi12d 476	. . . . . . . . . . . . . . 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 3007	. . . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . . 15 |- (z = if(z e. NN, z, 1) -> ((norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) <-> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))))
7	3, 6	imbi12d 474	. . . . . . . . . . . . . 14 |- (z = if(z e. NN, z, 1) -> (((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))) <-> ((if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1))))))
8	7	imbi2d 464	. . . . . . . . . . . . 13 |- (z = if(z e. NN, z, 1) -> (((ph /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (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) -> (norm` ((F` x) -v (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(norm` (v -v A))}
12		projlem27.4	. . . . . . . . . . . . . 14 |- R = -usup(S, RR, < )
13		projlem27.5	. . . . . . . . . . . . . 14 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (norm` ((F` w) -v A)) /\ (norm` ((F` w) -v A)) < (R + (1 / w)))))
14		1nn 4432	. . . . . . . . . . . . . . 15 |- 1 e. NN
15	14	elimel 1793	. . . . . . . . . . . . . 14 |- if(z e. NN, z, 1) e. NN
16	9, 10, 11, 12, 13, 15	projlem27 5219	. . . . . . . . . . . . 13 |- ((ph /\ (x e. NN /\ y e. NN)) -> ((if(z e. NN, z, 1) <_ x /\ if(z e. NN, z, 1) <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / if(z e. NN, z, 1)))))
17	8, 16	dedth 1784	. . . . . . . . . . . 12 |- (z e. NN -> ((ph /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)))))
18	17	exp3a 292	. . . . . . . . . . 11 |- (z e. NN -> (ph -> ((x e. NN /\ y e. NN) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))))
19	18	com12 13	. . . . . . . . . 10 |- (ph -> (z e. NN -> ((x e. NN /\ y e. NN) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))))
20	19	imp31 280	. . . . . . . . 9 |- (((ph /\ z e. NN) /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))
21	20	adantlr 310	. . . . . . . 8 |- ((((ph /\ z e. NN) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) /\ (x e. NN /\ y e. NN)) -> ((z <_ x /\ z <_ y) -> (norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z))))
22		projlem28.6	. . . . . . . . . . . . . . . 16 |- D e. RR
23		axlttrn 4084	. . . . . . . . . . . . . . . 16 |- (((norm` ((F` x) -v (F` y))) e. RR /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) e. RR /\ D e. RR) -> (((norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) -> (norm` ((F` x) -v (F` y))) < D))
24	22, 23	mp3an3 641	. . . . . . . . . . . . . . 15 |- (((norm` ((F` x) -v (F` y))) e. RR /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) e. RR) -> (((norm` ((F` x) -v (F` y))) < (sqr` ((4 x. ((2 x. R) + 1)) / z)) /\ (sqr` ((4 x. ((2 x. R) + 1)) / z)) < D) -> (norm` ((F` x) -v (F` y))) < D))
25		hvsubclt 4998	. . . . . . . . . . . . . . . . . 18 |- (((F` x) e. H~ /\ (F` y) e. H~) -> ((F` x) -v (F` y)) e. H~)
26	13	projlem21 5213	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> (x e. NN -> (F` x) e. H))
27	26	imp 277	. . . . . . . . . . . . . . . . . . 19 |- ((ph /\ x e. NN) -> (F` x) e. H)
28	10	chel 5137	. . . . . . . . . . . . . . . . . . 19 |- ((F` x) e. H -> (F` x) e. H~)
29	27, 28	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ x e. NN) -> (F` x) e. H~)
30	13	projlem21 5213	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> (y e. NN -> (F` y) e. H))
31	30	imp 277	. . . . . . . . . . . . . . . . . . 19 |- ((ph /\ y e. NN) -> (F` y) e. H)
32	10	chel 5137	. . . . . . . . . . . . . . . . . . 19 |- ((F` y) e. H -> (F` y) e. H~)
33	31, 32	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ y e. NN) -> (F` y) e. H~)
34	25, 29, 33	syl2an 349	. . . . . . . . . . . . . . . . 17 |- (((ph /\ x e. NN) /\ (ph /\ y e. NN)) -> ((F` x) -v (F` y)) e. H~)
35	34	anandis 394	. . . . . . . . . . . . . . . 16 |- ((ph /\ (x e. NN /\ y e. NN)) -> ((F` x) -v (F` y)) e. H~)
36		normclt 5076	. . . . . . . . . . . . . . . 16 |- (((F` x) -v (F` y)) e. H~ -> (norm` ((F` x) -v (F` y))) e. RR)
37	35, 36	syl 12	. . . . . . . . . . . . . . 15 |- ((ph /\ (x e. NN /\ y e. NN)) -> (norm` ((F` x) -v (F` y))) e. RR)
38		sqrclt 4767	. . . . . . . . . . . . . . . 16 |- ((((4 x. ((2 x. R) + 1)) / z) e. RR /\ 0 <_ ((4 x. ((2 x. R)