Theorem projlem5 5197

Description: Part of Lemma 3.6 of [Beran] p. 100, bottom. Used by projlem6 5198.

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
projlem5	|- ((norm` (B -v C))^2) < (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2)))

Proof of Theorem projlem5

Step	Hyp	Ref	Expression
1		projlem5.2	. . 3 |- B e. H~
2		projlem5.3	. . 3 |- C e. H~
3		projlem5.1	. . 3 |- A e. H~
4	1, 2, 3	normpar2 5100	. 2 |- ((norm` (B -v C))^2) = (((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) - ((norm` ((B +v C) -v (2 .s A)))^2))
5		projlem5.10	. . . . . . . 8 |- (norm` (B -v A)) < (R + (1 / D))
6	1, 3	hvsubcl 5002	. . . . . . . . . 10 |- (B -v A) e. H~
7		normge0t 5077	. . . . . . . . . 10 |- ((B -v A) e. H~ -> 0 <_ (norm` (B -v A)))
8	6, 7	ax-mp 6	. . . . . . . . 9 |- 0 <_ (norm` (B -v A))
9		projlem5.5	. . . . . . . . . 10 |- 0 <_ R
10		ax0re 4063	. . . . . . . . . . 11 |- 0 e. RR
11		ax1re 4064	. . . . . . . . . . . 12 |- 1 e. RR
12		projlem5.7	. . . . . . . . . . . . 13 |- D e. NN
13	12	nnre 4429	. . . . . . . . . . . 12 |- D e. RR
14	12	nnne0 4446	. . . . . . . . . . . 12 |- D =/= 0
15	11, 13, 14	redivcl 4274	. . . . . . . . . . 11 |- (1 / D) e. RR
16		nnrecgt0t 4447	. . . . . . . . . . . 12 |- (D e. NN -> 0 < (1 / D))
17	12, 16	ax-mp 6	. . . . . . . . . . 11 |- 0 < (1 / D)
18	10, 15, 17	ltlei 4303	. . . . . . . . . 10 |- 0 <_ (1 / D)
19		projlem5.4	. . . . . . . . . . 11 |- R e. RR
20	19, 15	addge0 4324	. . . . . . . . . 10 |- ((0 <_ R /\ 0 <_ (1 / D)) -> 0 <_ (R + (1 / D)))
21	9, 18, 20	mp2an 520	. . . . . . . . 9 |- 0 <_ (R + (1 / D))
22	6	normcl 5081	. . . . . . . . . 10 |- (norm` (B -v A)) e. RR
23	19, 15	readdcl 4118	. . . . . . . . . 10 |- (R + (1 / D)) e. RR
24	22, 23	lt2sqe 4700	. . . . . . . . 9 |- ((0 <_ (norm` (B -v A)) /\ 0 <_ (R + (1 / D))) -> ((norm` (B -v A)) < (R + (1 / D)) <-> ((norm` (B -v A))^2) < ((R + (1 / D))^2)))
25	8, 21, 24	mp2an 520	. . . . . . . 8 |- ((norm` (B -v A)) < (R + (1 / D)) <-> ((norm` (B -v A))^2) < ((R + (1 / D))^2))
26	5, 25	mpbi 164	. . . . . . 7 |- ((norm` (B -v A))^2) < ((R + (1 / D))^2)
27		2pos 4479	. . . . . . . 8 |- 0 < 2
28	22	sqrecl 4699	. . . . . . . . 9 |- ((norm` (B -v A))^2) e. RR
29	23	sqrecl 4699	. . . . . . . . 9 |- ((R + (1 / D))^2) e. RR
30		2re 4470	. . . . . . . . 9 |- 2 e. RR
31	28, 29, 30	ltmul2 4395	. . . . . . . 8 |- (0 < 2 -> (((norm` (B -v A))^2) < ((R + (1 / D))^2) <-> (2 x. ((norm` (B -v A))^2)) < (2 x. ((R + (1 / D))^2))))
32	27, 31	ax-mp 6	. . . . . . 7 |- (((norm` (B -v A))^2) < ((R + (1 / D))^2) <-> (2 x. ((norm` (B -v A))^2)) < (2 x. ((R + (1 / D))^2)))
33	26, 32	mpbi 164	. . . . . 6 |- (2 x. ((norm` (B -v A))^2)) < (2 x. ((R + (1 / D))^2))
34		projlem5.11	. . . . . . . 8 |- (norm` (C -v A)) < (R + (1 / G))
35	2, 3	hvsubcl 5002	. . . . . . . . . 10 |- (C -v A) e. H~
36		normge0t 5077	. . . . . . . . . 10 |- ((C -v A) e. H~ -> 0 <_ (norm` (C -v A)))
37	35, 36	ax-mp 6	. . . . . . . . 9 |- 0 <_ (norm` (C -v A))
38		projlem5.8	. . . . . . . . . . . . 13 |- G e. NN
39	38	nnre 4429	. . . . . . . . . . . 12 |- G e. RR
40	38	nnne0 4446	. . . . . . . . . . . 12 |- G =/= 0
41	11, 39, 40	redivcl 4274	. . . . . . . . . . 11 |- (1 / G) e. RR
42		nnrecgt0t 4447	. . . . . . . . . . . 12 |- (G e. NN -> 0 < (1 / G))
43	38, 42	ax-mp 6	. . . . . . . . . . 11 |- 0 < (1 / G)
44	10, 41, 43	ltlei 4303	. . . . . . . . . 10 |- 0 <_ (1 / G)
45	19, 41	addge0 4324	. . . . . . . . . 10 |- ((0 <_ R /\ 0 <_ (1 / G)) -> 0 <_ (R + (1 / G)))
46	9, 44, 45	mp2an 520	. . . . . . . . 9 |- 0 <_ (R + (1 / G))
47	35	normcl 5081	. . . . . . . . . 10 |- (norm` (C -v A)) e. RR
48	19, 41	readdcl 4118	. . . . . . . . . 10 |- (R + (1 / G)) e. RR
49	47, 48	lt2sqe 4700	. . . . . . . . 9 |- ((0 <_ (norm` (C -v A)) /\ 0 <_ (R + (1 / G))) -> ((norm` (C -v A)) < (R + (1 / G)) <-> ((norm` (C -v A))^2) < ((R + (1 / G))^2)))
50	37, 46, 49	mp2an 520	. . . . . . . 8 |- ((norm` (C -v A)) < (R + (1 / G)) <-> ((norm` (C -v A))^2) < ((R + (1 / G))^2))
51	34, 50	mpbi 164	. . . . . . 7 |- ((norm` (C -v A))^2) < ((R + (1 / G))^2)
52	47	sqrecl 4699	. . . . . . . . 9 |- ((norm` (C -v A))^2) e. RR
53	48	sqrecl 4699	. . . . . . . . 9 |- ((R + (1 / G))^2) e. RR
54	52, 53, 30	ltmul2 4395	. . . . . . . 8 |- (0 < 2 -> (((norm` (C -v A))^2) < ((R + (1 / G))^2) <-> (2 x. ((norm` (C -v A))^2)) < (2 x. ((R + (1 / G))^2))))
55	27, 54	ax-mp 6	. . . . . . 7 |- (((norm` (C -v A))^2) < ((R + (1 / G))^2) <-> (2 x. ((norm` (C -v A))^2)) < (2 x. ((R + (1 / G))^2)))
56	51, 55	mpbi 164	. . . . . 6 |- (2 x. ((norm` (C -v A))^2)) < (2 x. ((R + (1 / G))^2))
57	30, 28	remulcl 4119	. . . . . . 7 |- (2 x. ((norm` (B -v A))^2)) e. RR
58	30, 52	remulcl 4119	. . . . . . 7 |- (2 x. ((norm` (C -v A))^2)) e. RR
59	30, 29	remulcl 4119	. . . . . . 7 |- (2 x. ((R + (1 / D))^2)) e. RR
60	30, 53	remulcl 4119	. . . . . . 7 |- (2 x. ((R + (1 / G))^2)) e. RR
61	57, 58, 59, 60	lt2add 4321	. . . . . 6 |- (((2 x. ((norm` (B -v A))^2)) < (2 x. ((R + (1 / D))^2)) /\ (2 x. ((norm` (C -v A))^2)) < (2 x. ((R + (1 / G))^2))) -> ((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))))
62	33, 56, 61	mp2an 520	. . . . 5 |- ((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2)))
63	57, 58	readdcl 4118	. . . . . 6 |- ((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) e. RR
64	59, 60	readdcl 4118	. . . . . 6 |- ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) e. RR
65	1, 2	hvaddcl 4999	. . . . . . . . . 10 |- (B +v C) e. H~
66		2cn 4471	. . . . . . . . . . 11 |- 2 e. CC
67	66, 3	hvmulcl 4990	. . . . . . . . . 10 |- (2 .s A) e. H~
68	65, 67	hvsubcl 5002	. . . . . . . . 9 |- ((B +v C) -v (2 .s A)) e. H~
69	68	normcl 5081	. . . . . . . 8 |- (norm` ((B +v C) -v (2 .s A))) e. RR
70	69	sqrecl 4699	. . . . . . 7 |- ((norm` ((B +v C) -v (2 .s A)))^2) e. RR
71	70	renegcl 4171	. . . . . 6 |- -u((norm` ((B +v C) -v (2 .s A)))^2) e. RR
72	63, 64, 71	ltadd1 4313	. . . . 5 |- (((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) <-> (((2 x. ((norm` (B -v A))^2)) + (2 x. ((norm` (C -v A))^2))) + -u((norm` ((B +v C) -v (2 .s A)))^2)) < (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) + -u((norm` ((B +v C) -v (2