Theorem sqrlem11 4741

Description: Lemma for square root theorem.

Hypotheses

Ref	Expression
sqrlem1.1	|- A e. RR
sqrlem1.2	|- 0 < A
sqrlem9.3	|- B e. RR
sqrlem9.4	|- C e. RR
sqrlem9.5	|- 0 < B
sqrlem9.6	|- A < (B x. B)
sqrlem9.7	|- C = ((B + (A / B)) / (1 + 1))

Assertion

Ref	Expression
sqrlem11	|- A < (C x. C)

Proof of Theorem sqrlem11

Step	Hyp	Ref	Expression
1		sqrlem9.3	. . . . . . . . . . . 12 |- B e. RR
2	1, 1	remulcl 4119	. . . . . . . . . . 11 |- (B x. B) e. RR
3	2	recn 4098	. . . . . . . . . 10 |- (B x. B) e. CC
4		1cn 4101	. . . . . . . . . . . 12 |- 1 e. CC
5	4, 4	addcl 4104	. . . . . . . . . . 11 |- (1 + 1) e. CC
6	5	negcl 4142	. . . . . . . . . 10 |- -u(1 + 1) e. CC
7		sqrlem1.1	. . . . . . . . . . . 12 |- A e. RR
8	7	renegcl 4171	. . . . . . . . . . 11 |- -uA e. RR
9	8	recn 4098	. . . . . . . . . 10 |- -uA e. CC
10	3, 6, 9	mul12 4178	. . . . . . . . 9 |- ((B x. B) x. (-u(1 + 1) x. -uA)) = (-u(1 + 1) x. ((B x. B) x. -uA))
11	2, 8	remulcl 4119	. . . . . . . . . . 11 |- ((B x. B) x. -uA) e. RR
12	11	recn 4098	. . . . . . . . . 10 |- ((B x. B) x. -uA) e. CC
13	5, 12	mulneg1 4190	. . . . . . . . 9 |- (-u(1 + 1) x. ((B x. B) x. -uA)) = -u((1 + 1) x. ((B x. B) x. -uA))
14	12	1p1times 4187	. . . . . . . . . . 11 |- ((1 + 1) x. ((B x. B) x. -uA)) = (((B x. B) x. -uA) + ((B x. B) x. -uA))
15	14	negeqi 4137	. . . . . . . . . 10 |- -u((1 + 1) x. ((B x. B) x. -uA)) = -u(((B x. B) x. -uA) + ((B x. B) x. -uA))
16		df-neg 4135	. . . . . . . . . 10 |- -u(((B x. B) x. -uA) + ((B x. B) x. -uA)) = (0 - (((B x. B) x. -uA) + ((B x. B) x. -uA)))
17	15, 16	eqtr 1119	. . . . . . . . 9 |- -u((1 + 1) x. ((B x. B) x. -uA)) = (0 - (((B x. B) x. -uA) + ((B x. B) x. -uA)))
18	10, 13, 17	3eqtr 1123	. . . . . . . 8 |- ((B x. B) x. (-u(1 + 1) x. -uA)) = (0 - (((B x. B) x. -uA) + ((B x. B) x. -uA)))
19	2, 8	readdcl 4118	. . . . . . . . . . 11 |- ((B x. B) + -uA) e. RR
20	7	recn 4098	. . . . . . . . . . . . 13 |- A e. CC
21	20	negid 4147	. . . . . . . . . . . 12 |- (A + -uA) = 0
22		sqrlem9.6	. . . . . . . . . . . . 13 |- A < (B x. B)
23	7, 2, 8	ltadd1 4313	. . . . . . . . . . . . 13 |- (A < (B x. B) <-> (A + -uA) < ((B x. B) + -uA))
24	22, 23	mpbi 164	. . . . . . . . . . . 12 |- (A + -uA) < ((B x. B) + -uA)
25	21, 24	eqbrtrr 2078	. . . . . . . . . . 11 |- 0 < ((B x. B) + -uA)
26	19, 19, 25, 25	mulgt0i 4336	. . . . . . . . . 10 |- 0 < (((B x. B) + -uA) x. ((B x. B) + -uA))
27	3, 9, 3, 9	muladd 4181	. . . . . . . . . 10 |- (((B x. B) + -uA) x. ((B x. B) + -uA)) = ((((B x. B) x. (B x. B)) + (-uA x. -uA)) + (((B x. B) x. -uA) + ((B x. B) x. -uA)))
28	26, 27	breqtr 2080	. . . . . . . . 9 |- 0 < ((((B x. B) x. (B x. B)) + (-uA x. -uA)) + (((B x. B) x. -uA) + ((B x. B) x. -uA)))
29		ax0re 4063	. . . . . . . . . 10 |- 0 e. RR
30	11, 11	readdcl 4118	. . . . . . . . . 10 |- (((B x. B) x. -uA) + ((B x. B) x. -uA)) e. RR
31	2, 2	remulcl 4119	. . . . . . . . . . 11 |- ((B x. B) x. (B x. B)) e. RR
32	8, 8	remulcl 4119	. . . . . . . . . . 11 |- (-uA x. -uA) e. RR
33	31, 32	readdcl 4118	. . . . . . . . . 10 |- (((B x. B) x. (B x. B)) + (-uA x. -uA)) e. RR
34	29, 30, 33	ltsubadd 4316	. . . . . . . . 9 |- ((0 - (((B x. B) x. -uA) + ((B x. B) x. -uA))) < (((B x. B) x. (B x. B)) + (-uA x. -uA)) <-> 0 < ((((B x. B) x. (B x. B)) + (-uA x. -uA)) + (((B x. B) x. -uA) + ((B x. B) x. -uA))))
35	28, 34	mpbir 165	. . . . . . . 8 |- (0 - (((B x. B) x. -uA) + ((B x. B) x. -uA))) < (((B x. B) x. (B x. B)) + (-uA x. -uA))
36	18, 35	eqbrtr 2076	. . . . . . 7 |- ((B x. B) x. (-u(1 + 1) x. -uA)) < (((B x. B) x. (B x. B)) + (-uA x. -uA))
37		ax1re 4064	. . . . . . . . . . . 12 |- 1 e. RR
38	37, 37	readdcl 4118	. . . . . . . . . . 11 |- (1 + 1) e. RR
39	38	renegcl 4171	. . . . . . . . . 10 |- -u(1 + 1) e. RR
40	39, 8	remulcl 4119	. . . . . . . . 9 |- (-u(1 + 1) x. -uA) e. RR
41	2, 40	remulcl 4119	. . . . . . . 8 |- ((B x. B) x. (-u(1 + 1) x. -uA)) e. RR
42		sqrlem9.5	. . . . . . . . 9 |- 0 < B
43	1, 1, 42, 42	mulgt0i 4336	. . . . . . . 8 |- 0 < (B x. B)
44	41, 33, 2, 43	ltdivi 4398	. . . . . . 7 |- (((B x. B) x. (-u(1 + 1) x. -uA)) < (((B x. B) x. (B x. B)) + (-uA x. -uA)) <-> (((B x. B) x. (-u(1 + 1) x. -uA)) / (B x. B)) < ((((B x. B) x. (B x. B)) + (-uA x. -uA)) / (B x. B)))
45	36, 44	mpbi 164	. . . . . 6 |- (((B x. B) x. (-u(1 + 1) x. -uA)) / (B x. B)) < ((((B x. B) x. (B x. B)) + (-uA x. -uA)) / (B x. B))
46	6, 9	mulcl 4105	. . . . . . . 8 |- (-u(1 + 1) x. -uA) e. CC
47	1	recn 4098	. . . . . . . . 9 |- B e. CC
48	1, 42	gt0ne0i 4345	. . . . . . . . 9 |- B =/= 0
49	47, 47, 48, 48	muln0 4214	. . . . . . . 8 |- (B x. B) =/= 0
50	3, 46, 49	divcan3 4247	. . . . . . 7 |- (((B x. B) x. (-u(1 + 1) x. -uA)) / (B x. B)) = (-u(1 + 1) x. -uA)
51	5, 20	mul2neg 4192	. . . . . . 7 |- (-u(1 + 1) x. -uA) = ((1 + 1) x. A)
52	50, 51	eqtr 1119	. . . . . 6 |- (((B x. B) x. (-u(1 + 1) x. -uA)) / (B x. B)) = ((1 + 1) x. A)
53	31	recn 4098	. . . . . . 7 |- ((B x. B) x. (B x. B)) e. CC
54	32	recn 4098	. . . . . . 7 |- (-uA x. -uA) e. CC
55	2, 43	gt0ne0i 4345	. . . . . . 7 |- (B x. B) =/= 0
56	53, 54, 3, 55	divdistr 4243	. . . . . 6 |- ((((B x. B) x. (B x. B)) + (-uA x. -uA)) / (B x. B)) = ((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B)))
57	45, 52, 56	3brtr3 2084	. . . . 5 |- ((1 + 1) x. A) < ((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B)))
58	38, 7	remulcl 4119	. . . . . 6 |- ((1 + 1) x. A) e. RR
59	31, 2, 55	redivcl 4274	. . . . . . 7 |- (((B x. B) x. (B x. B)) / (B x. B)) e. RR
60	32, 2, 55	redivcl 4274	. . . . . . 7 |- ((-uA x. -uA) / (B x. B)) e. RR
61	59, 60	readdcl 4118	. . . . . 6 |- ((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B))) e. RR
62	58, 61, 58	ltadd1 4313	. . . . 5 |- (((1 + 1) x. A) < ((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B))) <-> (((1 + 1) x. A) + ((1 + 1) x. A)) < (((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B))) + ((1 + 1) x. A)))
63	57, 62	mpbi 164	. . . 4 |- (((1 + 1) x. A) + ((1 + 1) x. A)) < (((((B x. B) x. (B x. B)) / (B x. B)) + ((-uA x. -uA) / (B x. B))) + ((1 + 1) x. A))
64	5, 5	mulcl 4105	. . . . . 6 |- ((1 + 1) x. (1 + 1)) e. CC
65	20, 64	mulcom 4107	. . . . 5 |- (A x. ((1 + 1) x. (1 + 1))) = (((1 + 1) x. (1 + 1)) x. A)
66	5, 5, 20	mulass 4109	. . . . 5 |- (((1 + 1) x. (1 + 1)) x. A) = ((1 + 1) x. ((1 + 1) x. A))
67	5, 20	mulcl 4105	. . . . . 6 |- ((1 + 1) x. A) e. CC
68	67	1p1times 4187	. . . . 5 |- ((1 + 1) x. ((1 + 1) x. A)) = (((1 + 1) x. A) + ((1 + 1) x. A))
69	65, 66, 68	3eqtr 1123	. . . 4 |- (A x. ((1 + 1) x. (1 + 1))) = (((1 + 1) x. A) + ((1 + 1) x. A))
70	20, 47, 48	divcl 4221	. . . . . 6 |- (A / B) e. CC
71	47, 70, 47, 70	muladd 4181	. . . . 5 |- ((B + (A / B)) x. (B + (A / B))) = (((B x. B) + ((A / B) x. (A / B))) + ((B x. (A