Theorem projlem6 9107

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

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
projlem6	|- ((N <_ D /\ N <_ G) -> (normh` (B -h 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 9105	. . . 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)) <_ ((normh` ((B +h C) -h (2 .h A)))^2)
11		projlem5.10	. . . . . . 7 |- (normh` (B -h A)) < (R + (1 / D))
12		projlem5.11	. . . . . . 7 |- (normh` (C -h A)) < (R + (1 / G))
13	7, 8, 9, 1, 2, 10, 3, 4, 3, 11, 12	projlem5 9106	. . . . . 6 |- ((normh` (B -h C))^2) < (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2)))
14	1, 3, 4	projlem3 9104	. . . . . 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 8812	. . . . . . . . 9 |- (B -h C) e. H~
16	15	normcl 8919	. . . . . . . 8 |- (normh` (B -h C)) e. RR
17	16	resqcl 6554	. . . . . . 7 |- ((normh` (B -h C))^2) e. RR
18		2re 5926	. . . . . . . . . 10 |- 2 e. RR
19	3	nnre 5879	. . . . . . . . . . . . 13 |- D e. RR
20	3	nnne0 5899	. . . . . . . . . . . . 13 |- D =/= 0
21	19, 20	rereccl 5757	. . . . . . . . . . . 12 |- (1 / D) e. RR
22	1, 21	readdcl 5306	. . . . . . . . . . 11 |- (R + (1 / D)) e. RR
23	22	resqcl 6554	. . . . . . . . . 10 |- ((R + (1 / D))^2) e. RR
24	18, 23	remulcl 5307	. . . . . . . . 9 |- (2 x. ((R + (1 / D))^2)) e. RR
25	4	nnre 5879	. . . . . . . . . . . . 13 |- G e. RR
26	4	nnne0 5899	. . . . . . . . . . . . 13 |- G =/= 0
27	25, 26	rereccl 5757	. . . . . . . . . . . 12 |- (1 / G) e. RR
28	1, 27	readdcl 5306	. . . . . . . . . . 11 |- (R + (1 / G)) e. RR
29	28	resqcl 6554	. . . . . . . . . 10 |- ((R + (1 / G))^2) e. RR
30	18, 29	remulcl 5307	. . . . . . . . 9 |- (2 x. ((R + (1 / G))^2)) e. RR
31	24, 30	readdcl 5306	. . . . . . . 8 |- ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) e. RR
32		4re 5929	. . . . . . . . 9 |- 4 e. RR
33	1	resqcl 6554	. . . . . . . . 9 |- (R^2) e. RR
34	32, 33	remulcl 5307	. . . . . . . 8 |- (4 x. (R^2)) e. RR
35	31, 34	resubcl 5411	. . . . . . 7 |- (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) e. RR
36	32, 1	remulcl 5307	. . . . . . . . 9 |- (4 x. R) e. RR
37	36, 18	readdcl 5306	. . . . . . . 8 |- ((4 x. R) + 2) e. RR
38	21, 27	readdcl 5306	. . . . . . . 8 |- ((1 / D) + (1 / G)) e. RR
39	37, 38	remulcl 5307	. . . . . . 7 |- (((4 x. R) + 2) x. ((1 / D) + (1 / G))) e. RR
40	17, 35, 39	ltletr 5561	. . . . . 6 |- ((((normh` (B -h 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)))) -> ((normh` (B -h C))^2) < (((4 x. R) + 2) x. ((1 / D) + (1 / G))))
41	13, 14, 40	mp2an 695	. . . . 5 |- ((normh` (B -h C))^2) < (((4 x. R) + 2) x. ((1 / D) + (1 / G)))
42	18, 1	remulcl 5307	. . . . . . . . 9 |- (2 x. R) e. RR
43		1re 5407	. . . . . . . . 9 |- 1 e. RR
44	42, 43	readdcl 5306	. . . . . . . 8 |- ((2 x. R) + 1) e. RR
45	32, 44	remulcl 5307	. . . . . . 7 |- (4 x. ((2 x. R) + 1)) e. RR
46	5	nnre 5879	. . . . . . 7 |- N e. RR
47	5	nnne0 5899	. . . . . . 7 |- N =/= 0
48	45, 46, 47	redivcl 5754	. . . . . 6 |- ((4 x. ((2 x. R) + 1)) / N) e. RR
49	17, 39, 48	ltletr 5561	. . . . 5 |- ((((normh` (B -h 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)) -> ((normh` (B -h C))^2) < ((4 x. ((2 x. R) + 1)) / N))
50	41, 49	mpan 693	. . . 4 |- ((((4 x. R) + 2) x. ((1 / D) + (1 / G))) <_ ((4 x. ((2 x. R) + 1)) / N) -> ((normh` (B -h C))^2) < ((4 x. ((2 x. R) + 1)) / N))
51	6, 50	syl 10	. . 3 |- ((N <_ D /\ N <_ G) -> ((normh` (B -h C))^2) < ((4 x. ((2 x. R) + 1)) / N))
52		0re 5412	. . . . 5 |- 0 e. RR
53		4pos 5939	. . . . . . 7 |- 0 < 4
54		2pos 5936	. . . . . . . . . 10 |- 0 < 2
55	52, 18, 54	ltlei 5554	. . . . . . . . 9 |- 0 <_ 2
56	18, 1	mulge0 5581	. . . . . . . . 9 |- ((0 <_ 2 /\ 0 <_ R) -> 0 <_ (2 x. R))
57	55, 2, 56	mp2an 695	. . . . . . . 8 |- 0 <_ (2 x. R)
58		lt01 5653	. . . . . . . 8 |- 0 < 1
59	42, 43	addgegt0 5574	. . . . . . . 8 |- ((0 <_ (2 x. R) /\ 0 < 1) -> 0 < ((2 x. R) + 1))
60	57, 58, 59	mp2an 695	. . . . . . 7 |- 0 < ((2 x. R) + 1)
61	32, 44, 53, 60	mulgt0i 5582	. . . . . 6 |- 0 < (4 x. ((2 x. R) + 1))
62	5	nngt0 5898	. . . . . 6 |- 0 < N
63	45, 46, 61, 62	divgt0i 5814	. . . . 5 |- 0 < ((4 x. ((2 x. R) + 1)) / N)
64	52, 48, 63	ltlei 5554	. . . 4 |- 0 <_ ((4 x. ((2 x. R) + 1)) / N)
65	48	sqsqr 6651	. . . 4 |- (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 7	. . 3 |- ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2) = ((4 x. ((2 x. R) + 1)) / N)
67	51, 66	syl6breqr 2645	. 2 |- ((N <_ D /\ N <_ G) -> ((normh` (B -h C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2))
68		normge0t 8913	. . . 4 |- ((B -h C) e. H~ -> 0 <_ (normh` (B -h C)))
69	15, 68	ax-mp 7	. . 3 |- 0 <_ (normh` (B -h C))
70	48	sqrge0 6632	. . . 4 |- (0 <_ ((4 x. ((2 x. R) + 1)) / N) -> 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N)))
71	64, 70	ax-mp 7	. . 3 |- 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N))
72	48, 63	sqrlem24 6626	. . . 4 |- (sqr` ((4 x. ((2 x. R) + 1)) / N)) e. RR
73	16, 72	lt2sq 6555	. . 3 |- ((0 <_ (normh` (B -h C)) /\ 0 <_ (sqr` ((4 x. ((2 x. R) + 1)) / N))) -> ((normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> ((normh` (B -h C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2)))
74	69, 71, 73	mp2an 695	. 2 |- ((normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> ((normh` (B -h C))^2) < ((sqr` ((4 x. ((2 x. R) + 1)) / N))^2))
75	67, 74	sylibr 200	1 |- ((N <_ D /\ N <_ G) -> (normh` (B -h C)) < (sqr` ((