Theorem projlem6 5198

Description: Part of Lemma 3.6 of [Beran] p. 101. Used by projlem7 5199.

Hypotheses

Ref	Expression
projlem5.1	|- A e. H~
projlem5.2	|- B e. H~
projlem5.3	|- C e. H~
projlem5.4	|- R e. RR
projlem5.5	|- 0 <_ R
projlem5.6	|- (4 x. (R^2)) <_ ((norm` ((B +v C) -v (2 .s A)))^2)
projlem5.7	|- D e. NN
projlem5.8	|- G e. NN
projlem5.9	|- N e. NN
projlem5.10	|- (norm` (B -v A)) < (R + (1 / D))
projlem5.11	|- (norm` (C -v A)) < (R + (1 / G))

Assertion

Ref	Expression
projlem6	|- ((N <_ D /\ N <_ G) -> (norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))

Proof of Theorem projlem6

Step	Hyp	Ref	Expression
1		projlem5.4	. . . . 5 |- R e. RR
2		projlem5.5	. . . . 5 |- 0 <_ R
3		projlem5.7	. . . . 5 |- D e. NN
4		projlem5.8	. . . . 5 |- G e. NN
5		projlem5.9	. . . . 5 |- N e. NN
6	1, 2, 3, 4, 5	projlem4 5196	. . . 4 |- ((N <_ D /\ N <_ G) -> (((4 x. R) + 2) x. ((1 / D) + (1 / G))) <_ ((4 x. ((2 x. R) + 1)) / N))
7		projlem5.1	. . . . . . 7 |- A e. H~
8		projlem5.2	. . . . . . 7 |- B e. H~
9		projlem5.3	. . . . . . 7 |- C e. H~
10		projlem5.6	. . . . . . 7 |- (4 x. (R^2)) <_ ((norm` ((B +v C) -v (2 .s A)))^2)
11		projlem5.10	. . . . . . 7 |- (norm` (B -v A)) < (R + (1 / D))
12		projlem5.11	. . . . . . 7 |- (norm` (C -v A)) < (R + (1 / G))
13	7, 8, 9, 1, 2, 10, 3, 4, 3, 11, 12	projlem5 5197	. . . . . 6 |- ((norm` (B -v C))^2) < (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2)))
14	1, 3, 4	projlem3 5195	. . . . . 6 |- (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) <_ (((4 x. R) + 2) x. ((1 / D) + (1 / G)))
15	8, 9	hvsubcl 5002	. . . . . . . . 9 |- (B -v C) e. H~
16	15	normcl 5081	. . . . . . . 8 |- (norm` (B -v C)) e. RR
17	16	sqrecl 4699	. . . . . . 7 |- ((norm` (B -v C))^2) e. RR
18		2re 4470	. . . . . . . . . 10 |- 2 e. RR
19		ax1re 4064	. . . . . . . . . . . . 13 |- 1 e. RR
20	3	nnre 4429	. . . . . . . . . . . . 13 |- D e. RR
21	3	nnne0 4446	. . . . . . . . . . . . 13 |- D =/= 0
22	19, 20, 21	redivcl 4274	. . . . . . . . . . . 12 |- (1 / D) e. RR
23	1, 22	readdcl 4118	. . . . . . . . . . 11 |- (R + (1 / D)) e. RR
24	23	sqrecl 4699	. . . . . . . . . 10 |- ((R + (1 / D))^2) e. RR
25	18, 24	remulcl 4119	. . . . . . . . 9 |- (2 x. ((R + (1 / D))^2)) e. RR
26	4	nnre 4429	. . . . . . . . . . . . 13 |- G e. RR
27	4	nnne0 4446	. . . . . . . . . . . . 13 |- G =/= 0
28	19, 26, 27	redivcl 4274	. . . . . . . . . . . 12 |- (1 / G) e. RR
29	1, 28	readdcl 4118	. . . . . . . . . . 11 |- (R + (1 / G)) e. RR
30	29	sqrecl 4699	. . . . . . . . . 10 |- ((R + (1 / G))^2) e. RR
31	18, 30	remulcl 4119	. . . . . . . . 9 |- (2 x. ((R + (1 / G))^2)) e. RR
32	25, 31	readdcl 4118	. . . . . . . 8 |- ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) e. RR
33		4re 4473	. . . . . . . . 9 |- 4 e. RR
34	1	sqrecl 4699	. . . . . . . . 9 |- (R^2) e. RR
35	33, 34	remulcl 4119	. . . . . . . 8 |- (4 x. (R^2)) e. RR
36	32, 35	resubcl 4174	. . . . . . 7 |- (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) e. RR
37	33, 1	remulcl 4119	. . . . . . . . 9 |- (4 x. R) e. RR
38	37, 18	readdcl 4118	. . . . . . . 8 |- ((4 x. R) + 2) e. RR
39	22, 28	readdcl 4118	. . . . . . . 8 |- ((1 / D) + (1 / G)) e. RR
40	38, 39	remulcl 4119	. . . . . . 7 |- (((4 x. R) + 2) x. ((1 / D) + (1 / G))) e. RR
41	17, 36, 40	ltletr 4309	. . . . . 6 |- ((((norm` (B -v C))^2) < (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) /\ (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) <_ (((4 x. R) + 2) x. ((1 / D) + (1 / G)))) -> ((norm` (B -v C))^2) < (((4 x. R) + 2) x. ((1 / D) + (1 / G))))
42	13, 14, 41	mp2an 520	. . . . 5 |- ((norm` (B -v C))^2) < (((4 x. R) + 2) x. ((1 / D) + (1 / G)))
43	18, 1	remulcl 4119	. . . . . . . . 9 |- (2 x. R) e. RR
44	43, 19	readdcl 4118	. . . . . . . 8 |- ((2 x. R) + 1) e. RR
45	33, 44	remulcl 4119	. . . . . . 7 |- (4 x. ((2 x. R) + 1)) e. RR
46	5	nnre 4429	. . . . . . 7 |- N e. RR
47	5	nnne0 4446	. . . . . . 7 |- N =/= 0
48	45, 46, 47	redivcl 4274	. . . . . 6 |- ((4 x. ((2 x. R) + 1)) / N) e. RR
49	17, 40, 48	ltletr 4309	. . . . 5 |- ((((norm` (B -v C))^2) < (((4 x. R) + 2) x. ((1 / D) + (1 / G))) /\ (((4 x. R) + 2) x. ((1 / D) + (1 / G))) <_ ((4 x. ((2 x. R) + 1)) / N)) -> ((norm` (B -v C))^2) < ((4 x. ((2 x. R) + 1)) / N))
50	42, 49	mpan 518	. . . 4 |- ((((4 x. R) + 2) x. ((1 / D) + (1 / G))) <_ ((4 x. ((2 x. R) + 1)) / N) -> ((norm` (B -v C))^2) < ((4 x. ((2 x. R) + 1)) / N))
51	6, 50	syl 12	. . 3 |- ((N <_ D /\ N <_ G) -> ((norm` (B -v C))^2) < ((4 x. ((2 x. R) + 1)) / N))
52		ax0re 4063	. . . . . 6 |- 0 e. RR
53		4pos 4481	. . . . . . . 8 |- 0 < 4
54		2pos 4479	. . . . . . . . . . 11 |- 0 < 2
55	52, 18, 54	ltlei 4303	. . . . . . . . . 10 |- 0 <_ 2
56	18, 1	mulge0 4335	. . . . . . . . . 10 |- ((0 <_ 2 /\ 0 <_ R) -> 0 <_ (2 x. R))
57	55, 2, 56	mp2an 520	. . . . . . . . 9 |- 0 <_ (2 x. R)
58		lt01 4377	. . . . . . . . 9 |- 0 < 1
59	43, 19	addgegt0 4325	. . . . . . . . 9 |- ((0 <_ (2 x. R) /\ 0 < 1) -> 0 < ((2 x. R) + 1))
60	57, 58, 59	mp2an 520	. . . . . . . 8 |- 0 < ((2 x. R) + 1)
61	33, 44, 53, 60	mulgt0i 4336	. . . . . . 7 |- 0 < (4 x. ((2 x. R) + 1))
62	5	nngt0 4445	. . . . . . 7 |- 0 < N
63	45, 46, 61, 62	divgt0i 4391	. . . . . 6 |- 0 < ((4 x. ((2 x. R) + 1)) / N)
64	52, 48, 63	ltlei 4303	. . . . 5 |- 0 <_ ((4 x. ((2 x. R) + 1)) / N)
65	48	sqsqr 4775	. . . . 5 |- (0 <_ ((4 x. ((2 x. R) + 1)) / N) -> ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2) = ((4 x. ((2 x. R) + 1)) / N))
66	64, 65	ax-mp 6	. . . 4 |- ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2) = ((4 x. ((2 x. R) + 1)) / N)
67	66	breq2i 2069	. . 3 |- (((norm` (B -v C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2) <-> ((norm` (B -v C))^2) < ((4 x. ((2 x. R) + 1)) / N))
68	51, 67	sylibr 175	. 2 |- ((N <_ D /\ N <_ G) -> ((norm` (B -v C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2))
69		normge0t 5077	. . . 4 |- ((B -v C) e. H~ -> 0 <_ (norm` (B -v C)))
70	15, 69	ax-mp 6	. . 3 |- 0 <_ (norm` (B -v C))
71	48	sqrge0 4760	. . . 4 |- (0 <_ ((4 x. ((2 x. R) + 1)) / N) -> 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N)))
72	64, 71	ax-mp 6	. . 3 |- 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N))
73	48, 63	sqrlem24 4754	. . . 4 |- (sqr` ((4 x. ((2 x. R) + 1)) / N)) e. RR
74	16, 73	lt2sqe 4700	. . 3 |- ((0 <_ (norm` (B -v C)) /\ 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N))) -> ((norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> ((norm` (B -v C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2)))
75	70, 72, 74	mp2an 520	. 2 |- ((norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> ((norm` (B -v C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2))
76	68, 75	sylibr 175	1 |- ((N <_ D /\ N <_ G) ->