Theorem projlem3 9104

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

Hypotheses

Ref	Expression
projlem3.1	|- R e. RR
projlem3.2	|- D e. NN
projlem3.3	|- G e. NN

Assertion

Ref	Expression
projlem3	|- (((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)))

Proof of Theorem projlem3

Step	Hyp	Ref	Expression
1		2cn 5927	. . . . . 6 |- 2 e. CC
2		projlem3.1	. . . . . . . . 9 |- R e. RR
3		projlem3.2	. . . . . . . . . . 11 |- D e. NN
4	3	nnre 5879	. . . . . . . . . 10 |- D e. RR
5	3	nnne0 5899	. . . . . . . . . 10 |- D =/= 0
6	4, 5	rereccl 5757	. . . . . . . . 9 |- (1 / D) e. RR
7	2, 6	readdcl 5306	. . . . . . . 8 |- (R + (1 / D)) e. RR
8	7	resqcl 6554	. . . . . . 7 |- ((R + (1 / D))^2) e. RR
9	8	recn 5286	. . . . . 6 |- ((R + (1 / D))^2) e. CC
10		projlem3.3	. . . . . . . . . . 11 |- G e. NN
11	10	nnre 5879	. . . . . . . . . 10 |- G e. RR
12	10	nnne0 5899	. . . . . . . . . 10 |- G =/= 0
13	11, 12	rereccl 5757	. . . . . . . . 9 |- (1 / G) e. RR
14	2, 13	readdcl 5306	. . . . . . . 8 |- (R + (1 / G)) e. RR
15	14	resqcl 6554	. . . . . . 7 |- ((R + (1 / G))^2) e. RR
16	15	recn 5286	. . . . . 6 |- ((R + (1 / G))^2) e. CC
17	1, 9, 16	adddi 5298	. . . . 5 |- (2 x. (((R + (1 / D))^2) + ((R + (1 / G))^2))) = ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2)))
18	2	recn 5286	. . . . . . . . . 10 |- R e. CC
19	6	recn 5286	. . . . . . . . . 10 |- (1 / D) e. CC
20	18, 19	binom2 6575	. . . . . . . . 9 |- ((R + (1 / D))^2) = (((R^2) + (2 x. (R x. (1 / D)))) + ((1 / D)^2))
21	18	sqcl 6545	. . . . . . . . . 10 |- (R^2) e. CC
22	18, 19	mulcl 5293	. . . . . . . . . . 11 |- (R x. (1 / D)) e. CC
23	1, 22	mulcl 5293	. . . . . . . . . 10 |- (2 x. (R x. (1 / D))) e. CC
24	19	sqcl 6545	. . . . . . . . . 10 |- ((1 / D)^2) e. CC
25	21, 23, 24	addass 5296	. . . . . . . . 9 |- (((R^2) + (2 x. (R x. (1 / D)))) + ((1 / D)^2)) = ((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2)))
26	20, 25	eqtr 1487	. . . . . . . 8 |- ((R + (1 / D))^2) = ((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2)))
27	13	recn 5286	. . . . . . . . . 10 |- (1 / G) e. CC
28	18, 27	binom2 6575	. . . . . . . . 9 |- ((R + (1 / G))^2) = (((R^2) + (2 x. (R x. (1 / G)))) + ((1 / G)^2))
29	18, 27	mulcl 5293	. . . . . . . . . . 11 |- (R x. (1 / G)) e. CC
30	1, 29	mulcl 5293	. . . . . . . . . 10 |- (2 x. (R x. (1 / G))) e. CC
31	27	sqcl 6545	. . . . . . . . . 10 |- ((1 / G)^2) e. CC
32	21, 30, 31	addass 5296	. . . . . . . . 9 |- (((R^2) + (2 x. (R x. (1 / G)))) + ((1 / G)^2)) = ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))
33	28, 32	eqtr 1487	. . . . . . . 8 |- ((R + (1 / G))^2) = ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))
34	26, 33	opreq12i 3958	. . . . . . 7 |- (((R + (1 / D))^2) + ((R + (1 / G))^2)) = (((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2))) + ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))))
35	23, 24	addcl 5292	. . . . . . . 8 |- ((2 x. (R x. (1 / D))) + ((1 / D)^2)) e. CC
36	30, 31	addcl 5292	. . . . . . . 8 |- ((2 x. (R x. (1 / G))) + ((1 / G)^2)) e. CC
37	21, 35, 21, 36	add4 5314	. . . . . . 7 |- (((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2))) + ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))) = (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))))
38	34, 37	eqtr 1487	. . . . . 6 |- (((R + (1 / D))^2) + ((R + (1 / G))^2)) = (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))))
39	38	opreq2i 3957	. . . . 5 |- (2 x. (((R + (1 / D))^2) + ((R + (1 / G))^2))) = (2 x. (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))))
40	17, 39	eqtr3 1489	. . . 4 |- ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) = (2 x. (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))))
41	1, 1, 21	mulass 5297	. . . . 5 |- ((2 x. 2) x. (R^2)) = (2 x. (2 x. (R^2)))
42		2t2e4 5969	. . . . . 6 |- (2 x. 2) = 4
43	42	opreq1i 3956	. . . . 5 |- ((2 x. 2) x. (R^2)) = (4 x. (R^2))
44	21	2times 5950	. . . . . 6 |- (2 x. (R^2)) = ((R^2) + (R^2))
45	44	opreq2i 3957	. . . . 5 |- (2 x. (2 x. (R^2))) = (2 x. ((R^2) + (R^2)))
46	41, 43, 45	3eqtr3 1495	. . . 4 |- (4 x. (R^2)) = (2 x. ((R^2) + (R^2)))
47	40, 46	opreq12i 3958	. . 3 |- (((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2))) - (4 x. (R^2))) = ((2 x. (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))))) - (2 x. ((R^2) + (R^2))))
48	21, 21	addcl 5292	. . . . 5 |- ((R^2) + (R^2)) e. CC
49	35, 36	addcl 5292	. . . . 5 |- (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))) e. CC
50	48, 49	addcl 5292	. . . 4 |- (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))) e. CC
51	1, 50, 48	subdi 5401	. . 3 |- (2 x. ((((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))) - ((R^2) + (R^2)))) = ((2 x. (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))))) - (2 x. ((R^2) + (R^2))))
52	48, 49, 48	addsubass 5359	. . . . 5 |- ((((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))) - ((R^2) + (R^2))) = (((R^2) + (R^2)) + ((((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R <