Theorem sqrlem20 4750

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
sqrlem19.5	|- (B x. B) < A
sqrlem20.6	|- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}

Assertion

Ref	Expression
sqrlem20	|- -. B = sup(S, RR, < )

Distinct variable group(s):   x,A   x,B   x,S

Proof of Theorem sqrlem20

Step	Hyp	Ref	Expression
1		sqrlem15.3	. . 3 |- B e. RR
2		sqrlem1.1	. . . . 5 |- A e. RR
3	1, 1	remulcl 4119	. . . . 5 |- (B x. B) e. RR
4	2, 3	resubcl 4174	. . . 4 |- (A - (B x. B)) e. RR
5		ax1re 4064	. . . . . . 7 |- 1 e. RR
6	5, 5	readdcl 4118	. . . . . 6 |- (1 + 1) e. RR
7	6, 5	readdcl 4118	. . . . 5 |- ((1 + 1) + 1) e. RR
8	7, 1	remulcl 4119	. . . 4 |- (((1 + 1) + 1) x. B) e. RR
9	7	recn 4098	. . . . 5 |- ((1 + 1) + 1) e. CC
10	1	recn 4098	. . . . 5 |- B e. CC
11		lt01 4377	. . . . . . . 8 |- 0 < 1
12	5, 5, 11, 11	addgt0i 4326	. . . . . . 7 |- 0 < (1 + 1)
13	6, 5, 12, 11	addgt0i 4326	. . . . . 6 |- 0 < ((1 + 1) + 1)
14	7, 13	gt0ne0i 4345	. . . . 5 |- ((1 + 1) + 1) =/= 0
15		sqrlem15.4	. . . . . 6 |- 0 < B
16	1, 15	gt0ne0i 4345	. . . . 5 |- B =/= 0
17	9, 10, 14, 16	muln0 4214	. . . 4 |- (((1 + 1) + 1) x. B) =/= 0
18	4, 8, 17	redivcl 4274	. . 3 |- ((A - (B x. B)) / (((1 + 1) + 1) x. B)) e. RR
19		sqrlem1.2	. . . 4 |- 0 < A
20		sqrlem19.5	. . . 4 |- (B x. B) < A
21	2, 19, 1, 15, 20	sqrlem19 4749	. . 3 |- 0 < ((A - (B x. B)) / (((1 + 1) + 1) x. B))
22	1, 18, 15, 21	posex 4422	. 2 |- E.w e. RR (0 < w /\ (w < B /\ w < ((A - (B x. B)) / (((1 + 1) + 1) x. B))))
23		breq1 2065	. . . . . . 7 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) <-> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < ((A - (B x. B)) / (((1 + 1) + 1) x. B))))
24	23	imbi1d 465	. . . . . 6 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> ((w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> -. B = sup(S, RR, < )) <-> (if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> -. B = sup(S, RR, < ))))
25		eleq1 1149	. . . . . . . . . 10 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (w e. RR <-> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR))
26		breq2 2066	. . . . . . . . . 10 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (0 < w <-> 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1)))))
27		breq1 2065	. . . . . . . . . 10 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (w < B <-> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B))
28	25, 26, 27	bi3and 636	. . . . . . . . 9 |- (w = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> ((w e. RR /\ 0 < w /\ w < B) <-> (if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B)))
29		eleq1 1149	. . . . . . . . . 10 |- ((B / (1 + 1)) = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> ((B / (1 + 1)) e. RR <-> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR))
30		breq2 2066	. . . . . . . . . 10 |- ((B / (1 + 1)) = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (0 < (B / (1 + 1)) <-> 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1)))))
31		breq1 2065	. . . . . . . . . 10 |- ((B / (1 + 1)) = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> ((B / (1 + 1)) < B <-> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B))
32	29, 30, 31	bi3and 636	. . . . . . . . 9 |- ((B / (1 + 1)) = if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) -> (((B / (1 + 1)) e. RR /\ 0 < (B / (1 + 1)) /\ (B / (1 + 1)) < B) <-> (if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B)))
33	6, 12	gt0ne0i 4345	. . . . . . . . . . 11 |- (1 + 1) =/= 0
34	1, 6, 33	redivcl 4274	. . . . . . . . . 10 |- (B / (1 + 1)) e. RR
35	1, 6, 15, 12	divgt0i 4391	. . . . . . . . . 10 |- 0 < (B / (1 + 1))
36	1	halfpos 4421	. . . . . . . . . . 11 |- (0 < B <-> (B / (1 + 1)) < B)
37	15, 36	mpbi 164	. . . . . . . . . 10 |- (B / (1 + 1)) < B
38	34, 35, 37	3pm3.2i 603	. . . . . . . . 9 |- ((B / (1 + 1)) e. RR /\ 0 < (B / (1 + 1)) /\ (B / (1 + 1)) < B)
39	28, 32, 38	elimhyp 1790	. . . . . . . 8 |- (if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B)
40		3simp1 594	. . . . . . . 8 |- ((if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B) -> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR)
41	39, 40	ax-mp 6	. . . . . . 7 |- if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR
42		3simp2 595	. . . . . . . 8 |- ((if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B) -> 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))))
43	39, 42	ax-mp 6	. . . . . . 7 |- 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1)))
44		3simp3 596	. . . . . . . 8 |- ((if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR /\ 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) /\ if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B) -> if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B)
45	39, 44	ax-mp 6	. . . . . . 7 |- if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B
46		sqrlem20.6	. . . . . . 7 |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}
47	2, 19, 1, 15, 41, 43, 45, 46	sqrlem18 4748	. . . . . 6 |- (if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> -. B = sup