Theorem sqrlem16 4746

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		1cn 4101	. . . . . . 7 |- 1 e. CC
2	1, 1	addcl 4104	. . . . . 6 |- (1 + 1) e. CC
3	2, 1	addcl 4104	. . . . 5 |- ((1 + 1) + 1) e. CC
4		sqrlem15.3	. . . . . 6 |- B e. RR
5	4	recn 4098	. . . . 5 |- B e. CC
6		sqrlem15.5	. . . . . 6 |- C e. RR
7	6	recn 4098	. . . . 5 |- C e. CC
8	3, 5, 7	mulass 4109	. . . 4 |- ((((1 + 1) + 1) x. B) x. C) = (((1 + 1) + 1) x. (B x. C))
9	3, 5	mulcl 4105	. . . . 5 |- (((1 + 1) + 1) x. B) e. CC
10		sqrlem1.1	. . . . . . 7 |- A e. RR
11	4, 4	remulcl 4119	. . . . . . 7 |- (B x. B) e. RR
12	10, 11	resubcl 4174	. . . . . 6 |- (A - (B x. B)) e. RR
13	12	recn 4098	. . . . 5 |- (A - (B x. B)) e. CC
14		ax1re 4064	. . . . . . . . 9 |- 1 e. RR
15	14, 14	readdcl 4118	. . . . . . . 8 |- (1 + 1) e. RR
16	15, 14	readdcl 4118	. . . . . . 7 |- ((1 + 1) + 1) e. RR
17	16	recn 4098	. . . . . 6 |- ((1 + 1) + 1) e. CC
18		lt01 4377	. . . . . . . . 9 |- 0 < 1
19	14, 14, 18, 18	addgt0i 4326	. . . . . . . 8 |- 0 < (1 + 1)
20	15, 14, 19, 18	addgt0i 4326	. . . . . . 7 |- 0 < ((1 + 1) + 1)
21	16, 20	gt0ne0i 4345	. . . . . 6 |- ((1 + 1) + 1) =/= 0
22		sqrlem15.4	. . . . . . 7 |- 0 < B
23	4, 22	gt0ne0i 4345	. . . . . 6 |- B =/= 0
24	17, 5, 21, 23	muln0 4214	. . . . 5 |- (((1 + 1) + 1) x. B) =/= 0
25	9, 13, 24	divcan2 4224	. . . 4 |- ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B))) = (A - (B x. B))
26	8, 25	breq12i 2070	. . 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)))
27	16, 4, 20, 22	mulgt0i 4336	. . . 4 |- 0 < (((1 + 1) + 1) x. B)
28	16, 4	remulcl 4119	. . . . . 6 |- (((1 + 1) + 1) x. B) e. RR
29	12, 28, 24	redivcl 4274	. . . . 5 |- ((A - (B x. B)) / (((1 + 1) + 1) x. B)) e. RR
30	6, 29, 28	ltmul2 4395	. . . 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)))))
31	27, 30	ax-mp 6	. . 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))))
32	4, 6	remulcl 4119	. . . . 5 |- (B x. C) e. RR
33	16, 32	remulcl 4119	. . . 4 |- (((1 + 1) + 1) x. (B x. C)) e. RR
34	33, 11, 10	ltaddsub 4320	. . 3 |- (((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A <-> (((1 + 1) + 1) x. (B x. C)) < (A - (B x. B)))
35	26, 31, 34	3bitr4 158	. 2 |- (C < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) <-> ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A)
36		sqrlem16.7	. . . . . . 7 |- C < B
37		sqrlem15.6	. . . . . . . 8 |- 0 < C
38	6, 4, 6	ltmul2 4395	. . . . . . . 8 |- (0 < C -> (C < B <-> (C x. C) < (C x. B)))
39	37, 38	ax-mp 6	. . . . . . 7 |- (C < B <-> (C x. C) < (C x. B))
40	36, 39	mpbi 164	. . . . . 6 |- (C x. C) < (C x. B)
41	6, 6	remulcl 4119	. . . . . . 7 |- (C x. C) e. RR
42	6, 4	remulcl 4119	. . . . . . 7 |- (C x. B) e. RR
43	41, 42, 11	ltadd2 4312	. . . . . 6 |- ((C x. C) < (C x. B) <-> ((B x. B) + (C x. C)) < ((B x. B) + (C x. B)))
44	40, 43	mpbi 164	. . . . 5 |- ((B x. B) + (C x. C)) < ((B x. B) + (C x. B))
45	11, 41	readdcl 4118	. . . . . 6 |- ((B x. B) + (C x. C)) e. RR
46	11, 42	readdcl 4118	. . . . . 6 |- ((B x. B) + (C x. B)) e. RR
47	32, 32	readdcl 4118	. . . . . 6 |- ((B x. C) + (B x. C)) e. RR
48	45, 46, 47	ltadd1 4313	. . . . 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))))
49	44, 48	mpbi 164	. . . 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)))
50	5, 7, 5, 7	muladd 4181	. . . 4 |- ((B + C) x. (B + C)) = (((B x. B) + (C x. C)) + ((B x. C) + (B x. C)))
51	42, 47	readdcl 4118	. . . . . . 7 |- ((C x. B) + ((B x. C) + (B x. C))) e. RR
52	51	recn 4098	. . . . . 6 |- ((C x. B) + ((B x. C) + (B x. C))) e. CC
53	11	recn 4098	. . . . . 6 |- (B x. B) e. CC
54	52, 53	addcom 4106	. . . . 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))))
55	32	recn 4098	. . . . . . . 8 |- (B x. C) e. CC
56	2, 1, 55	adddir 4111	. . . . . . 7 |- (((1 + 1) + 1) x. (B x. C)) = (((1 + 1) x. (B x. C)) + (1 x. (B x. C)))
57	55	1p1times 4187	. . . . . . . 8 |- ((1 + 1) x. (B x. C)) = ((B x. C) + (B x. C))
58	55	mulid2 4115	. . . . . . . . 9 |- (1 x. (B x. C)) = (B x. C)
59	5, 7	mulcom 4107	. . . . . . . . 9 |- (B x. C) = (C x. B)
60	58, 59	eqtr 1119	. . . . . . . 8 |- (1 x. (B x. C)) = (C x. B)
61	57, 60	opreq12i 3011	. . . . . . 7 |- (((1 + 1) x. (B x. C)) + (1 x. (B x. C))) = (((B x. C) + (B x. C)) + (C x. B))
62	47	recn 4098	. . . . . . . 8 |- ((B x. C) + (B x. C)) e. CC
63	42	recn 4098	. . . . . . . 8 |- (C x. B) e. CC
64	62, 63	addcom 4106	. . . . . . 7 |- (((B x. C) + (B x. C)) + (C x. B)) = ((C x. B) + ((B x. C) + (B x. C)))
65	56, 61, 64	3eqtr 1123	. . . . . 6 |- (((1 + 1) + 1) x. (B x. C)) = ((C x. B) + ((B x. C) + (B x. C)))
66	65	opreq1i 3009	. . . . 5 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) = (((C x. B) + ((B x. C) + (B x. C))) + (B x. B))
67	53, 63, 62	addass 4108	. . . . 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))))
68	54, 66, 67	3eqtr4 1126	. . . 4 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) = (((B x. B) + (C x. B)) + ((B x. C) + (B x. C)))
69	49, 50, 68	3brtr4 2085	. . 3 |- ((B + C) x. (B + C)) < ((((1 + 1) + 1) x. (B x. C)) + (B x. B))
70	4, 6	readdcl 4118	. . . . 5 |- (B + C) e. RR
71	70, 70	remulcl 4119	. . . 4 |- ((B + C) x. (B + C)) e. RR
72	33, 11	readdcl 4118	. . . 4 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) e. RR
73	71, 72, 10	lttr 4307	. . 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)
74	69, 73	mpan 518	. 2 |- (((((1 + 1) + 1) x. (B x. C)) + (B x. B)) < A -> ((B + C) x. (B + C)) < A)
75	35, 74	sylbi 174	1 |- (C < ((A - (B x. B)) / (((1 + 1) + 1) x.