Theorem projlem3 5195

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

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 4471	. . . . . 6 |- 2 e. CC
2		projlem3.1	. . . . . . . . 9 |- R e. RR
3		ax1re 4064	. . . . . . . . . 10 |- 1 e. RR
4		projlem3.2	. . . . . . . . . . 11 |- D e. NN
5	4	nnre 4429	. . . . . . . . . 10 |- D e. RR
6	4	nnne0 4446	. . . . . . . . . 10 |- D =/= 0
7	3, 5, 6	redivcl 4274	. . . . . . . . 9 |- (1 / D) e. RR
8	2, 7	readdcl 4118	. . . . . . . 8 |- (R + (1 / D)) e. RR
9	8	sqrecl 4699	. . . . . . 7 |- ((R + (1 / D))^2) e. RR
10	9	recn 4098	. . . . . 6 |- ((R + (1 / D))^2) e. CC
11		projlem3.3	. . . . . . . . . . 11 |- G e. NN
12	11	nnre 4429	. . . . . . . . . 10 |- G e. RR
13	11	nnne0 4446	. . . . . . . . . 10 |- G =/= 0
14	3, 12, 13	redivcl 4274	. . . . . . . . 9 |- (1 / G) e. RR
15	2, 14	readdcl 4118	. . . . . . . 8 |- (R + (1 / G)) e. RR
16	15	sqrecl 4699	. . . . . . 7 |- ((R + (1 / G))^2) e. RR
17	16	recn 4098	. . . . . 6 |- ((R + (1 / G))^2) e. CC
18	1, 10, 17	adddi 4110	. . . . 5 |- (2 x. (((R + (1 / D))^2) + ((R + (1 / G))^2))) = ((2 x. ((R + (1 / D))^2)) + (2 x. ((R + (1 / G))^2)))
19	2	recn 4098	. . . . . . . . . 10 |- R e. CC
20	7	recn 4098	. . . . . . . . . 10 |- (1 / D) e. CC
21	19, 20	binom 4712	. . . . . . . . 9 |- ((R + (1 / D))^2) = (((R^2) + (2 x. (R x. (1 / D)))) + ((1 / D)^2))
22	19	sqcl 4686	. . . . . . . . . 10 |- (R^2) e. CC
23	19, 20	mulcl 4105	. . . . . . . . . . 11 |- (R x. (1 / D)) e. CC
24	1, 23	mulcl 4105	. . . . . . . . . 10 |- (2 x. (R x. (1 / D))) e. CC
25	20	sqcl 4686	. . . . . . . . . 10 |- ((1 / D)^2) e. CC
26	22, 24, 25	addass 4108	. . . . . . . . 9 |- (((R^2) + (2 x. (R x. (1 / D)))) + ((1 / D)^2)) = ((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2)))
27	21, 26	eqtr 1119	. . . . . . . 8 |- ((R + (1 / D))^2) = ((R^2) + ((2 x. (R x. (1 / D))) + ((1 / D)^2)))
28	14	recn 4098	. . . . . . . . . 10 |- (1 / G) e. CC
29	19, 28	binom 4712	. . . . . . . . 9 |- ((R + (1 / G))^2) = (((R^2) + (2 x. (R x. (1 / G)))) + ((1 / G)^2))
30	19, 28	mulcl 4105	. . . . . . . . . . 11 |- (R x. (1 / G)) e. CC
31	1, 30	mulcl 4105	. . . . . . . . . 10 |- (2 x. (R x. (1 / G))) e. CC
32	28	sqcl 4686	. . . . . . . . . 10 |- ((1 / G)^2) e. CC
33	22, 31, 32	addass 4108	. . . . . . . . 9 |- (((R^2) + (2 x. (R x. (1 / G)))) + ((1 / G)^2)) = ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))
34	29, 33	eqtr 1119	. . . . . . . 8 |- ((R + (1 / G))^2) = ((R^2) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))
35	27, 34	opreq12i 3011	. . . . . . 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))))
36	24, 25	addcl 4104	. . . . . . . 8 |- ((2 x. (R x. (1 / D))) + ((1 / D)^2)) e. CC
37	31, 32	addcl 4104	. . . . . . . 8 |- ((2 x. (R x. (1 / G))) + ((1 / G)^2)) e. CC
38	22, 36, 22, 37	add4 4130	. . . . . . 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))))
39	35, 38	eqtr 1119	. . . . . 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))))
40	39	opreq2i 3010	. . . . 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)))))
41	18, 40	eqtr3 1121	. . . 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)))))
42	1, 1, 22	mulass 4109	. . . . 5 |- ((2 x. 2) x. (R^2)) = (2 x. (2 x. (R^2)))
43		2t2e4 4503	. . . . . 6 |- (2 x. 2) = 4
44	43	opreq1i 3009	. . . . 5 |- ((2 x. 2) x. (R^2)) = (4 x. (R^2))
45	22	2times 4489	. . . . . 6 |- (2 x. (R^2)) = ((R^2) + (R^2))
46	45	opreq2i 3010	. . . . 5 |- (2 x. (2 x. (R^2))) = (2 x. ((R^2) + (R^2)))
47	42, 44, 46	3eqtr3 1124	. . . 4 |- (4 x. (R^2)) = (2 x. ((R^2) + (R^2)))
48	41, 47	opreq12i 3011	. . 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))))
49	22, 22	addcl 4104	. . . . . 6 |- ((R^2) + (R^2)) e. CC
50	36, 37	addcl 4104	. . . . . 6 |- (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2))) e. CC
51	49, 50	addcl 4104	. . . . 5 |- (((R^2) + (R^2)) + (((2 x. (R x. (1 / D))) + ((1 / D)^2)) + ((2 x. (R x. (1 / G))) + ((1 / G)^2)))) e. CC
52	1, 51, 49	subdi 4182	. . . 4 |- (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))))
53	49, 50, 49	addsubass 4152	. . . . . 6 |- ((((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 x. (1 / G))) + ((1 / G)^2))) - ((R^2) +