Theorem sqrlem16 6626

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 5415	. . . . . . . 8 |- 1 e. RR
2	1, 1	readdcl 5314	. . . . . . 7 |- (1 + 1) e. RR
3	2, 1	readdcl 5314	. . . . . 6 |- ((1 + 1) + 1) e. RR
4	3	recn 5294	. . . . 5 |- ((1 + 1) + 1) e. CC
5		sqrlem15.3	. . . . . 6 |- B e. RR
6	5	recn 5294	. . . . 5 |- B e. CC
7		sqrlem15.5	. . . . . 6 |- C e. RR
8	7	recn 5294	. . . . 5 |- C e. CC
9	4, 6, 8	mulass 5305	. . . 4 |- ((((1 + 1) + 1) x. B) x. C) = (((1 + 1) + 1) x. (B x. C))
10	3, 5	remulcl 5315	. . . . . 6 |- (((1 + 1) + 1) x. B) e. RR
11	10	recn 5294	. . . . 5 |- (((1 + 1) + 1) x. B) e. CC
12		sqrlem1.1	. . . . . . 7 |- A e. RR
13	5, 5	remulcl 5315	. . . . . . 7 |- (B x. B) e. RR
14	12, 13	resubcl 5419	. . . . . 6 |- (A - (B x. B)) e. RR
15	14	recn 5294	. . . . 5 |- (A - (B x. B)) e. CC
16		lt01 5661	. . . . . . . . 9 |- 0 < 1
17	1, 1, 16, 16	addgt0i 5583	. . . . . . . 8 |- 0 < (1 + 1)
18	2, 1, 17, 16	addgt0i 5583	. . . . . . 7 |- 0 < ((1 + 1) + 1)
19	3, 18	gt0ne0i 5599	. . . . . 6 |- ((1 + 1) + 1) =/= 0
20		sqrlem15.4	. . . . . . 7 |- 0 < B
21	5, 20	gt0ne0i 5599	. . . . . 6 |- B =/= 0
22	4, 6, 19, 21	muln0 5676	. . . . 5 |- (((1 + 1) + 1) x. B) =/= 0
23	11, 15, 22	divcan2 5693	. . . 4 |- ((((1 + 1) + 1) x. B) x. ((A - (B x. B)) / (((1 + 1) + 1) x. B))) = (A - (B x. B))
24	9, 23	breq12i 2623	. . 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 5590	. . . 4 |- 0 < (((1 + 1) + 1) x. B)
26	14, 10, 22	redivcl 5762	. . . . 5 |- ((A - (B x. B)) / (((1 + 1) + 1) x. B)) e. RR
27	7, 26, 10	ltmul2 5798	. . . 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 5315	. . . . 5 |- (B x. C) e. RR
30	3, 29	remulcl 5315	. . . 4 |- (((1 + 1) + 1) x. (B x. C)) e. RR
31	30, 13, 12	ltaddsub 5621	. . 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 5798	. . . . . . . 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 5315	. . . . . . 7 |- (C x. C) e. RR
39	7, 5	remulcl 5315	. . . . . . 7 |- (C x. B) e. RR
40	38, 39, 13	ltadd2 5572	. . . . . 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	13, 38	readdcl 5314	. . . . . 6 |- ((B x. B) + (C x. C)) e. RR
43	13, 39	readdcl 5314	. . . . . 6 |- ((B x. B) + (C x. B)) e. RR
44	29, 29	readdcl 5314	. . . . . 6 |- ((B x. C) + (B x. C)) e. RR
45	42, 43, 44	ltadd1 5573	. . . . 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 5406	. . . 4 |- ((B + C) x. (B + C)) = (((B x. B) + (C x. C)) + ((B x. C) + (B x. C)))
48	39, 44	readdcl 5314	. . . . . . 7 |- ((C x. B) + ((B x. C) + (B x. C))) e. RR
49	48	recn 5294	. . . . . 6 |- ((C x. B) + ((B x. C) + (B x. C))) e. CC
50	13	recn 5294	. . . . . 6 |- (B x. B) e. CC
51	49, 50	addcom 5302	. . . . 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 5294	. . . . . . . 8 |- (1 + 1) e. CC
53		ax1cn 5249	. . . . . . . 8 |- 1 e. CC
54	29	recn 5294	. . . . . . . 8 |- (B x. C) e. CC
55	52, 53, 54	adddir 5307	. . . . . . 7 |- (((1 + 1) + 1) x. (B x. C)) = (((1 + 1) x. (B x. C)) + (1 x. (B x. C)))
56	54	1p1times 5413	. . . . . . . 8 |- ((1 + 1) x. (B x. C)) = ((B x. C) + (B x. C))
57	54	mulid2 5313	. . . . . . . . 9 |- (1 x. (B x. C)) = (B x. C)
58	6, 8	mulcom 5303	. . . . . . . . 9 |- (B x. C) = (C x. B)
59	57, 58	eqtr 1492	. . . . . . . 8 |- (1 x. (B x. C)) = (C x. B)
60	56, 59	opreq12i 3964	. . . . . . 7 |- (((1 + 1) x. (B x. C)) + (1 x. (B x. C))) = (((B x. C) + (B x. C)) + (C x. B))
61	44	recn 5294	. . . . . . . 8 |- ((B x. C) + (B x. C)) e. CC
62	39	recn 5294	. . . . . . . 8 |- (C x. B) e. CC
63	61, 62	addcom 5302	. . . . . . 7 |- (((B x. C) + (B x. C)) + (C x. B)) = ((C x. B) + ((B x. C) + (B x. C)))
64	55, 60, 63	3eqtr 1496	. . . . . 6 |- (((1 + 1) + 1) x. (B x. C)) = ((C x. B) + ((B x. C) + (B x. C)))
65	64	opreq1i 3962	. . . . 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 5304	. . . . 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 1502	. . . 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 2638	. . 3 |- ((B + C) x. (B + C)) < ((((1 + 1) + 1) x. (B x. C)) + (B x. B))
69	5, 7	readdcl 5314	. . . . 5 |- (B + C) e. RR
70	69, 69	remulcl 5315	. . . 4 |- ((B + C) x. (B + C)) e. RR
71	30, 13	readdcl 5314	. . . 4 |- ((((1 + 1) + 1) x. (B x. C)) + (B x. B)) e. RR
72	70, 71, 12	lttr 5567	. . 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 694	. 2 |- (((((1 + 1) + 1) x. (B x. C)) + (B x. B))