Theorem sqrlem21 6623

Description: Lemma for square root theorem.

Hypotheses

Ref	Expression
sqrlem1.1	|- A e. RR
sqrlem1.2	|- 0 < A
sqrlem21.3	|- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}
sqrlem21.4	|- B = sup(S, RR, < )

Assertion

Ref	Expression
sqrlem21	|- -. A < (B x. B)

Distinct variable groups:   x,A   x,B   x,S

Proof of Theorem sqrlem21

Step	Hyp	Ref	Expression
1		sqrlem21.4	. 2 |- B = sup(S, RR, < )
2		eqeq1 1473	. . . 4 |- (B = if(A < (B x. B), B, (1 + A)) -> (B = sup(S, RR, < ) <-> if(A < (B x. B), B, (1 + A)) = sup(S, RR, < )))
3	2	negbid 609	. . 3 |- (B = if(A < (B x. B), B, (1 + A)) -> (-. B = sup(S, RR, < ) <-> -. if(A < (B x. B), B, (1 + A)) = sup(S, RR, < )))
4		sqrlem1.1	. . . 4 |- A e. RR
5		sqrlem1.2	. . . 4 |- 0 < A
6		sqrlem21.3	. . . . . 6 |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}
7	4, 5, 6, 1	sqrlem7 6609	. . . . 5 |- B e. RR
8		1re 5407	. . . . . 6 |- 1 e. RR
9	8, 4	readdcl 5306	. . . . 5 |- (1 + A) e. RR
10	7, 9	keepel 2389	. . . 4 |- if(A < (B x. B), B, (1 + A)) e. RR
11		id 59	. . . . . . . 8 |- (B = if(A < (B x. B), B, (1 + A)) -> B = if(A < (B x. B), B, (1 + A)))
12		opreq2 3954	. . . . . . . 8 |- (B = if(A < (B x. B), B, (1 + A)) -> (A / B) = (A / if(A < (B x. B), B, (1 + A))))
13	11, 12	opreq12d 3963	. . . . . . 7 |- (B = if(A < (B x. B), B, (1 + A)) -> (B + (A / B)) = (if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))))
14	13	opreq1d 3960	. . . . . 6 |- (B = if(A < (B x. B), B, (1 + A)) -> ((B + (A / B)) / (1 + 1)) = ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)))
15	14	eleq1d 1532	. . . . 5 |- (B = if(A < (B x. B), B, (1 + A)) -> (((B + (A / B)) / (1 + 1)) e. RR <-> ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)) e. RR))
16		id 59	. . . . . . . 8 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> (1 + A) = if(A < (B x. B), B, (1 + A)))
17		opreq2 3954	. . . . . . . 8 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> (A / (1 + A)) = (A / if(A < (B x. B), B, (1 + A))))
18	16, 17	opreq12d 3963	. . . . . . 7 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> ((1 + A) + (A / (1 + A))) = (if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))))
19	18	opreq1d 3960	. . . . . 6 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> (((1 + A) + (A / (1 + A))) / (1 + 1)) = ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)))
20	19	eleq1d 1532	. . . . 5 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> ((((1 + A) + (A / (1 + A))) / (1 + 1)) e. RR <-> ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)) e. RR))
21	4, 5, 6, 1	sqrlem8 6610	. . . . . . . . 9 |- 0 < B
22	7, 21	gt0ne0i 5591	. . . . . . . 8 |- B =/= 0
23	4, 7, 22	redivcl 5754	. . . . . . 7 |- (A / B) e. RR
24	7, 23	readdcl 5306	. . . . . 6 |- (B + (A / B)) e. RR
25	8, 8	readdcl 5306	. . . . . 6 |- (1 + 1) e. RR
26		lt01 5653	. . . . . . . 8 |- 0 < 1
27	8, 8, 26, 26	addgt0i 5575	. . . . . . 7 |- 0 < (1 + 1)
28	25, 27	gt0ne0i 5591	. . . . . 6 |- (1 + 1) =/= 0
29	24, 25, 28	redivcl 5754	. . . . 5 |- ((B + (A / B)) / (1 + 1)) e. RR
30	8, 4, 26, 5	addgt0i 5575	. . . . . . . . 9 |- 0 < (1 + A)
31	9, 30	gt0ne0i 5591	. . . . . . . 8 |- (1 + A) =/= 0
32	4, 9, 31	redivcl 5754	. . . . . . 7 |- (A / (1 + A)) e. RR
33	9, 32	readdcl 5306	. . . . . 6 |- ((1 + A) + (A / (1 + A))) e. RR
34	33, 25, 28	redivcl 5754	. . . . 5 |- (((1 + A) + (A / (1 + A))) / (1 + 1)) e. RR
35	15, 20, 29, 34	keephyp 2386	. . . 4 |- ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)) e. RR
36		breq2 2613	. . . . 5 |- (B = if(A < (B x. B), B, (1 + A)) -> (0 < B <-> 0 < if(A < (B x. B), B, (1 + A))))
37		breq2 2613	. . . . 5 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> (0 < (1 + A) <-> 0 < if(A < (B x. B), B, (1 + A))))
38	36, 37, 21, 30	keephyp 2386	. . . 4 |- 0 < if(A < (B x. B), B, (1 + A))
39		opreq12 3955	. . . . . . 7 |- ((B = if(A < (B x. B), B, (1 + A)) /\ B = if(A < (B x. B), B, (1 + A))) -> (B x. B) = (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A))))
40	39	anidms 434	. . . . . 6 |- (B = if(A < (B x. B), B, (1 + A)) -> (B x. B) = (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A))))
41	40	breq2d 2620	. . . . 5 |- (B = if(A < (B x. B), B, (1 + A)) -> (A < (B x. B) <-> A < (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A)))))
42		opreq12 3955	. . . . . . 7 |- (((1 + A) = if(A < (B x. B), B, (1 + A)) /\ (1 + A) = if(A < (B x. B), B, (1 + A))) -> ((1 + A) x. (1 + A)) = (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A))))
43	42	anidms 434	. . . . . 6 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> ((1 + A) x. (1 + A)) = (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A))))
44	43	breq2d 2620	. . . . 5 |- ((1 + A) = if(A < (B x. B), B, (1 + A)) -> (A < ((1 + A) x. (1 + A)) <-> A < (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A)))))
45	4, 5	sqrlem1 6603	. . . . 5 |- A < ((1 + A) x. (1 + A))
46	41, 44, 45	elimhyp 2380	. . . 4 |- A < (if(A < (B x. B), B, (1 + A)) x. if(A < (B x. B), B, (1 + A)))
47		eqid 1468	. . . 4 |- ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1)) = ((if(A < (B x. B), B, (1 + A)) + (A / if(A < (B x. B), B, (1 + A)))) / (1 + 1))
48	4, 5, 10, 35, 38, 46, 47, 6	sqrlem14 6616	. . 3 |- -. if(A < (B x. B), B, (1 + A)) = sup(S, RR, < )
49	3, 48	dedth 2373