Theorem projlem5 9129

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

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)) <_ ((normh` ((B +h C) -h (2 .h A)))^2)
projlem5.7	|- D e. NN
projlem5.8	|- G e. NN
projlem5.9	|- N e. NN
projlem5.10	|- (normh` (B -h A)) < (R + (1 / D))
projlem5.11	|- (normh` (C -h A)) < (R + (1 / G))

Assertion

Ref	Expression
projlem5	|- ((normh` (B -h 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 8962	. 2 |- ((normh` (B -h C))^2) = (((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) - ((normh` ((B +h C) -h (2 .h A)))^2))
5		projlem5.10	. . . . . . . 8 |- (normh` (B -h A)) < (R + (1 / D))
6	1, 3	hvsubcl 8830	. . . . . . . . . 10 |- (B -h A) e. H~
7		normge0t 8931	. . . . . . . . . 10 |- ((B -h A) e. H~ -> 0 <_ (normh` (B -h A)))
8	6, 7	ax-mp 7	. . . . . . . . 9 |- 0 <_ (normh` (B -h A))
9		projlem5.5	. . . . . . . . . 10 |- 0 <_ R
10		0re 5420	. . . . . . . . . . 11 |- 0 e. RR
11		projlem5.7	. . . . . . . . . . . . 13 |- D e. NN
12	11	nnre 5887	. . . . . . . . . . . 12 |- D e. RR
13	11	nnne0 5907	. . . . . . . . . . . 12 |- D =/= 0
14	12, 13	rereccl 5765	. . . . . . . . . . 11 |- (1 / D) e. RR
15		nnrecgt0t 5908	. . . . . . . . . . . 12 |- (D e. NN -> 0 < (1 / D))
16	11, 15	ax-mp 7	. . . . . . . . . . 11 |- 0 < (1 / D)
17	10, 14, 16	ltlei 5562	. . . . . . . . . 10 |- 0 <_ (1 / D)
18		projlem5.4	. . . . . . . . . . 11 |- R e. RR
19	18, 14	addge0 5581	. . . . . . . . . 10 |- ((0 <_ R /\ 0 <_ (1 / D)) -> 0 <_ (R + (1 / D)))
20	9, 17, 19	mp2an 696	. . . . . . . . 9 |- 0 <_ (R + (1 / D))
21	6	normcl 8937	. . . . . . . . . 10 |- (normh` (B -h A)) e. RR
22	18, 14	readdcl 5314	. . . . . . . . . 10 |- (R + (1 / D)) e. RR
23	21, 22	lt2sq 6563	. . . . . . . . 9 |- ((0 <_ (normh` (B -h A)) /\ 0 <_ (R + (1 / D))) -> ((normh` (B -h A)) < (R + (1 / D)) <-> ((normh` (B -h A))^2) < ((R + (1 / D))^2)))
24	8, 20, 23	mp2an 696	. . . . . . . 8 |- ((normh` (B -h A)) < (R + (1 / D)) <-> ((normh` (B -h A))^2) < ((R + (1 / D))^2))
25	5, 24	mpbi 189	. . . . . . 7 |- ((normh` (B -h A))^2) < ((R + (1 / D))^2)
26		2pos 5944	. . . . . . . 8 |- 0 < 2
27	21	resqcl 6562	. . . . . . . . 9 |- ((normh` (B -h A))^2) e. RR
28	22	resqcl 6562	. . . . . . . . 9 |- ((R + (1 / D))^2) e. RR
29		2re 5934	. . . . . . . . 9 |- 2 e. RR
30	27, 28, 29	ltmul2 5798	. . . . . . . 8 |- (0 < 2 -> (((normh` (B -h A))^2) < ((R + (1 / D))^2) <-> (2 x. ((normh` (B -h A))^2)) < (2 x. ((R + (1 / D))^2))))
31	26, 30	ax-mp 7	. . . . . . 7 |- (((normh` (B -h A))^2) < ((R + (1 / D))^2) <-> (2 x. ((normh` (B -h A))^2)) < (2 x. ((R + (1 / D))^2)))
32	25, 31	mpbi 189	. . . . . 6 |- (2 x. ((normh` (B -h A))^2)) < (2 x. ((R + (1 / D))^2))
33		projlem5.11	. . . . . . . 8 |- (normh` (C -h A)) < (R + (1 / G))
34	2, 3	hvsubcl 8830	. . . . . . . . . 10 |- (C -h A) e. H~
35		normge0t 8931	. . . . . . . . . 10 |- ((C -h A) e. H~ -> 0 <_ (normh` (C -h A)))
36	34, 35	ax-mp 7	. . . . . . . . 9 |- 0 <_ (normh` (C -h A))
37		projlem5.8	. . . . . . . . . . . . 13 |- G e. NN
38	37	nnre 5887	. . . . . . . . . . . 12 |- G e. RR
39	37	nnne0 5907	. . . . . . . . . . . 12 |- G =/= 0
40	38, 39	rereccl 5765	. . . . . . . . . . 11 |- (1 / G) e. RR
41		nnrecgt0t 5908	. . . . . . . . . . . 12 |- (G e. NN -> 0 < (1 / G))
42	37, 41	ax-mp 7	. . . . . . . . . . 11 |- 0 < (1 / G)
43	10, 40, 42	ltlei 5562	. . . . . . . . . 10 |- 0 <_ (1 / G)
44	18, 40	addge0 5581	. . . . . . . . . 10 |- ((0 <_ R /\ 0 <_ (1 / G)) -> 0 <_ (R + (1 / G)))
45	9, 43, 44	mp2an 696	. . . . . . . . 9 |- 0 <_ (R + (1 / G))
46	34	normcl 8937	. . . . . . . . . 10 |- (normh` (C -h A)) e. RR
47	18, 40	readdcl 5314	. . . . . . . . . 10 |- (R + (1 / G)) e. RR
48	46, 47	lt2sq 6563	. . . . . . . . 9 |- ((0 <_ (normh` (C -h A)) /\ 0 <_ (R + (1 / G))) -> ((normh` (C -h A)) < (R + (1 / G)) <-> ((normh` (C -h A))^2) < ((R + (1 / G))^2)))
49	36, 45, 48	mp2an 696	. . . . . . . 8 |- ((normh` (C -h A)) < (R + (1 / G)) <-> ((normh` (C -h A))^2) < ((R + (1 / G))^2))
50	33, 49	mpbi 189	. . . . . . 7 |- ((normh` (C -h A))^2) < ((R + (1 / G))^2)
51	46	resqcl 6562	. . . . . . . . 9 |- ((normh` (C -h A))^2) e. RR
52	47	resqcl 6562	. . . . . . . . 9 |- ((R + (1 / G))^2) e. RR
53	51, 52, 29	ltmul2 5798	. . . . . . . 8 |- (0 < 2 -> (((normh` (C -h A))^2) < ((R + (1 / G))^2) <-> (2 x. ((normh` (C -h A))^2)) < (2 x. ((R + (1 / G))^2))))
54	26, 53	ax-mp 7	. . . . . . 7 |- (((normh` (C -h A))^2) < ((R + (1 / G))^2) <-> (2 x. ((normh` (C -h A))^2)) < (2 x. ((R + (1 / G))^2)))
55	50, 54	mpbi 189	. . . . . 6 |- (2 x. ((normh` (C -h A))^2)) < (2 x. ((R + (1 / G))^2))
56	29, 27	remulcl 5315	. . . . . . 7 |- (2 x. ((normh` (B -h A))^2)) e. RR
57	29, 51	remulcl 5315	. . . . . . 7 |- (2 x. ((normh` (C -h A))^2)) e. RR
58	29, 28	remulcl 5315	. . . . . . 7 |- (2 x. ((R + (1 / D))^2)) e. RR
59	29, 52	remulcl 5315	. . . . . . 7 |- (2 x. ((R + (1 / G))^2)) e. RR
60	56, 57, 58, 59	lt2add 5578	. . . . . 6 |- (((2 x. ((normh` (B -h A))^2)) < (2 x. ((R + (1 / D))^2)) /\ (2 x. ((normh` (C -h A))^2)) < (2 x. ((R + (1 / G))^2))) -> ((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))))
61	32, 55, 60	mp2an 696	. . . . 5 |- ((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2)))
62	56, 57	readdcl 5314	. . . . . 6 |- ((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) e. RR
63	58, 59	readdcl 5314	. . . . . 6 |- ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) e. RR
64	1, 2	hvaddcl 8827	. . . . . . . . . 10 |- (B +h C) e. H~
65		2cn 5935	. . . . . . . . . . 11 |- 2 e. CC
66	65, 3	hvmulcl 8823	. . . . . . . . . 10 |- (2 .h A) e. H~
67	64, 66	hvsubcl 8830	. . . . . . . . 9 |- ((B +h C) -h (2 .h A)) e. H~
68	67	normcl 8937	. . . . . . . 8 |- (normh` ((B +h C) -h (2 .h A))) e. RR
69	68	resqcl 6562	. . . . . . 7 |- ((normh` ((B +h C) -h (2 .h A)))^2) e. RR
70	69	renegcl 5396	. . . . . 6 |- -u((normh` ((B +h C) -h (2 .h A)))^2) e. RR
71	62, 63, 70	ltadd1 5573	. . . . 5 |- (((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) < ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) <-> (((2 x. ((normh` (B -h A))^2)) + (2 x. ((normh` (C -h A))^2))) + -u((normh` ((B +h C) -h (2 .h A)))