Theorem sqrlem16 6688

Description: Lemma for square root theorem.

Hypotheses

Ref	Expression
sqrlem1.1	|- A e. RR
sqrlem1.2	|- 0 < A
sqrlem15.3	|- B e. RR
sqrlem15.4	|- 0 < B
sqrlem15.5	|- C e. RR
sqrlem15.6	|- 0 < C
sqrlem16.7	|- C < B

Assertion

Ref	Expression
sqrlem16	|- (C < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> ((B + C) x. (B + C)) < A)

Proof of Theorem sqrlem16

Step	Hyp	Ref	Expression
1		1re 5435	. . . . . . . 8 |- 1 e. RR
2	1, 1	readdcl 5334	. . . . . . 7 |- (1 + 1) e. RR
3	2, 1	readdcl 5334	. . . . . 6 |- ((1 + 1) + 1) e. RR
4	3	recn 5314	. . . . 5 |- ((1 + 1) + 1) e. CC
5		sqrlem15.3	. . . . . 6 |- B e. RR
6	5	recn 5314	. . . . 5 |- B e. CC
7		sqrlem15.5	. . . . . 6 |- C e. RR
8	7	recn 5314	. . . . 5 |- C e. CC
9	4, 6, 8	mulass 5325	. . . 4 |- ((((1 + 1) + 1) x. B) x. C) = (((1 + 1) + 1) x. (B x. C))
10		sqrlem1.1	. . . . . . 7 |- A e. RR
11	5, 5	remulcl 5335	. . . . . . 7 |- (B x. B) e. RR
12	10, 11	resubcl 5439	. . . . . 6 |- (A - (B x. B)) e. RR
13	12	recn 5314	. . . . 5 |- (A - (B x. B)) e. CC
14	3, 5	remulcl 5335	. . . . . 6 |- (((1 + 1) + 1) x. B) e. RR
15	14	recn 5314	. . . . 5 |- (((1 + 1) + 1) x. B) e. CC
16		lt01 5680	. . . . . . . . 9 |- 0 < 1
17	1, 1, 16, 16	addgt0i 5601	. . . . . . . 8 |- 0 < (1 + 1)
18	2, 1, 17, 16	addgt0i 5601	. . . . . . 7 |- 0 < ((1 + 1) + 1)
19	3, 18	gt0ne0i 5617	. . . . . 6 |- ((1 + 1) + 1) =/= 0
20		sqrlem15.4	. . . . . . 7 |- 0 < B
21	5, 20	gt0ne0i 5617	. . . . . 6 |- B =/= 0
22	4, 6, 19, 21	muln0 5699	. . . . 5 |- (((1 + 1) + 1) x. B) =/= 0
23	13, 15, 22	divcan2 5716	. . . 4 |- ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B))) = (A - (B x. B))
24	9, 23	breq12i 2628	. . 3 |- (((((1 + 1) + 1) x. B) x. C) < ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B))) <-> (((1 + 1) + 1) x. (B x. C)) < (A - (B x. B)))
25	3, 5, 18, 20	mulgt0i 5608	. . . 4 |- 0 < (((1 + 1) + 1) x. B)
26	12, 14, 22	redivcl 5798	. . . . 5 |- ((A - (B x. B)) / (((1 + 1) + 1) x. B)) e. RR
27	7, 26, 14	ltmul2 5834	. . . 4 |- (0 < (((1 + 1) + 1) x. B) -> (C < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) <-> ((((1 + 1) + 1) x. B) x. C) < ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B)))))
28	25, 27	ax-mp 7	. . 3 |- (C < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) <-> ((((1 + 1) + 1) x. B) x. C) < ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B))))
29	5, 7	remulcl 5335	. . . . 5 |- (B x. C) e. RR
30	3, 29	remulcl 5335	. . . 4 |- (((1 + 1) + 1) x. (B x. C)) e. RR
31	30, 11, 10	ltaddsub 5639	. . 3 |- (((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A <-> (((1 + 1) + 1) x. (B x. C)) < (A - (B x. B)))
32	24, 28, 31	3bitr4 183	. 2 |- (C < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) <-> ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A)
33		sqrlem16.7	. . . . . . 7 |- C < B
34		sqrlem15.6	. . . . . . . 8 |- 0 < C
35	7, 5, 7	ltmul2 5834	. . . . . . . 8 |- (0 < C -> (C < B <-> (C x. C) < (C x. B)))
36	34, 35	ax-mp 7	. . . . . . 7 |- (C < B <-> (C x. C) < (C x. B))
37	33, 36	mpbi 189	. . . . . 6 |- (C x. C) < (C x. B)
38	7, 7	remulcl 5335	. . . . . . 7 |- (C x. C) e. RR
39	7, 5	remulcl 5335	. . . . . . 7 |- (C x. B) e. RR
40	38, 39, 11	ltadd2 5590	. . . . . 6 |- ((C x. C) < (C x. B) <-> ((B x. B) + (C x. C)) < ((B x. B) + (C x. B)))
41	37, 40	mpbi 189	. . . . 5 |- ((B x. B) + (C x. C)) < ((B x. B) + (C x. B))
42	11, 38	readdcl 5334	. . . . . 6 |- ((B x. B) + (C x. C)) e. RR
43	11, 39	readdcl 5334	. . . . . 6 |- ((B x. B) + (C x. B)) e. RR
44	29, 29	readdcl 5334	. . . . . 6 |- ((B x. C) + (B x. C)) e. RR
45	42, 43, 44	ltadd1 5591	. . . . 5 |- (((B x. B) + (C x. C)) < ((B x. B) + (C x. B)) <-> (((B x. B) + (C x. C)) + ((B x. C) + (B x. C))) < (((B x. B) + (C x. B)) + ((B x. C) + (B x. C))))
46	41, 45	mpbi 189	. . . 4 |- (((B x. B) + (C x. C)) + ((B x. C) + (B x. C))) < (((B x. B) + (C x. B)) + ((B x. C) + (B x. C)))
47	6, 8, 6, 8	muladd 5426	. . . 4 |- ((B + C) x. (B + C)) = (((B x. B) + (C x. C)) + ((B x. C) + (B x. C)))
48	39, 44	readdcl 5334	. . . . . . 7 |- ((C x. B) + ((B x. C) + (B x. C))) e. RR
49	48	recn 5314	. . . . . 6 |- ((C x. B) + ((B x. C) + (B x. C))) e. CC
50	11	recn 5314	. . . . . 6 |- (B x. B) e. CC
51	49, 50	addcom 5322	. . . . 5 |- (((C x. B) + ((B x. C) + (B x. C))) + (B x. B)) = ((B x. B) + ((C x. B) + ((B x. C) + (B x. C))))
52	2	recn 5314	. . . . . . . 8 |- (1 + 1) e. CC
53		ax1cn 5269	. . . . . . . 8 |- 1 e. CC
54	29	recn 5314	. . . . . . . 8 |- (B x. C) e. CC
55	52, 53, 54	adddir 5327	. . . . . . 7 |- (((1 + 1) + 1) x. (B x. C)) = (((1 + 1) x. (B x. C)) + (1 x. (B x. C)))
56	54	1p1times 5433	. . . . . . . 8 |- ((1 + 1) x. (B x. C)) = ((B x. C) + (B x. C))
57	54	mulid2 5333	. . . . . . . . 9 |- (1 x. (B x. C)) = (B x. C)
58	6, 8	mulcom 5323	. . . . . . . . 9 |- (B x. C) = (C x. B)
59	57, 58	eqtr 1495	. . . . . . . 8 |- (1 x. (B x. C)) = (C x. B)
60	56, 59	opreq12i 3973	. . . . . . 7 |- (((1 + 1) x. (B x. C)) + (1 x. (B x. C))) = (((B x. C) + (B x. C)) + (C x. B))
61	44	recn 5314	. . . . . . . 8 |- ((B x. C) + (B x. C)) e. CC
62	39	recn 5314	. . . . . . . 8 |- (C x. B) e. CC
63	61, 62	addcom 5322	. . . . . . 7 |- (((B x. C) + (B x. C)) + (C x. B)) = ((C x. B) + ((B x. C) + (B x. C)))
64	55, 60, 63	3eqtr 1499	. . . . . 6 |- (((1 + 1) + 1) x. (B x. C)) = ((C x. B) + ((B x. C) + (B x. C)))
65	64	opreq1i 3971	. . . . 5 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) = (((C x. B) + ((B x. C) + (B x. C))) + (B x. B))
66	50, 62, 61	addass 5324	. . . . 5 |- (((B x. B) + (C x. B)) + ((B x. C) + (B x. C))) = ((B x. B) + ((C x. B) + ((B x. C) + (B x. C))))
67	51, 65, 66	3eqtr4 1505	. . . 4 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) = (((B x. B) + (C x. B)) + ((B x. C) + (B x. C)))
68	46, 47, 67	3brtr4 2643	. . 3 |- ((B + C) x. (B + C)) < ((((1 + 1) + 1) x. (B x. C)) + (B x. B))
69	5, 7	readdcl 5334	. . . . 5 |- (B + C) e. RR
70	69, 69	remulcl 5335	. . . 4 |- ((B + C) x. (B + C)) e. RR
71	30, 11	readdcl 5334	. . . 4 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) e. RR
72	70, 71, 10	lttr 5585	. . 3 |- ((((B + C) x. (B + C)) < ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) /\ ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A) -> ((B + C) x. (B + C)) < A)
73	68, 72	mpan 695	. 2 |- (((((1 + 1) + 1) x. (B x. C)) + (B x. B)