Theorem sqrlem20 6630

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 groups:   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 5315	. . . . 5 |- (B x. B) e. RR
4	2, 3	resubcl 5419	. . . 4 |- (A - (B x. B)) e. RR
5		1re 5415	. . . . . . 7 |- 1 e. RR
6	5, 5	readdcl 5314	. . . . . 6 |- (1 + 1) e. RR
7	6, 5	readdcl 5314	. . . . 5 |- ((1 + 1) + 1) e. RR
8	7, 1	remulcl 5315	. . . 4 |- (((1 + 1) + 1) x. B) e. RR
9	7	recn 5294	. . . . 5 |- ((1 + 1) + 1) e. CC
10	1	recn 5294	. . . . 5 |- B e. CC
11		lt01 5661	. . . . . . . 8 |- 0 < 1
12	5, 5, 11, 11	addgt0i 5583	. . . . . . 7 |- 0 < (1 + 1)
13	6, 5, 12, 11	addgt0i 5583	. . . . . 6 |- 0 < ((1 + 1) + 1)
14	7, 13	gt0ne0i 5599	. . . . 5 |- ((1 + 1) + 1) =/= 0
15		sqrlem15.4	. . . . . 6 |- 0 < B
16	1, 15	gt0ne0i 5599	. . . . 5 |- B =/= 0
17	9, 10, 14, 16	muln0 5676	. . . 4 |- (((1 + 1) + 1) x. B) =/= 0
18	4, 8, 17	redivcl 5762	. . 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 6629	. . 3 |- 0 < ((A - (B x. B)) / (((1 + 1) + 1) x. B))
22	1, 18, 15, 21	posex 5864	. 2 |- E.w e. RR (0 < w /\ (w < B /\ w < ((A - (B x. B)) / (((1 + 1) + 1) x. B))))
23		breq1 2617	. . . . . . 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 612	. . . . . 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 1531	. . . . . . . . . 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 2618	. . . . . . . . . 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 2617	. . . . . . . . . 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	3anbi123d 891	. . . . . . . . 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 1531	. . . . . . . . . 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 2618	. . . . . . . . . 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 2617	. . . . . . . . . 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	3anbi123d 891	. . . . . . . . 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 5599	. . . . . . . . . . 11 |- (1 + 1) =/= 0
34	1, 6, 33	redivcl 5762	. . . . . . . . . 10 |- (B / (1 + 1)) e. RR
35	1, 6, 15, 12	divgt0i 5822	. . . . . . . . . 10 |- 0 < (B / (1 + 1))
36	1	halfpos 5860	. . . . . . . . . . 11 |- (0 < B <-> (B / (1 + 1)) < B)
37	15, 36	mpbi 189	. . . . . . . . . 10 |- (B / (1 + 1)) < B
38	34, 35, 37	3pm3.2i 817	. . . . . . . . 9 |- ((B / (1 + 1)) e. RR /\ 0 < (B / (1 + 1)) /\ (B / (1 + 1)) < B)
39	28, 32, 38	elimhyp 2386	. . . . . . . 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	39	3simp1i 790	. . . . . . 7 |- if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR
41	39	3simp2i 791	. . . . . . 7 |- 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1)))
42	39	3simp3i 792	. . . . . . 7 |- if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) < B
43		sqrlem20.6	. . . . . . 7 |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}
44	2, 19, 1, 15, 40, 41, 42, 43	sqrlem18 6628	. . . . . 6 |- (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, < ))
45	24, 44	dedth 2379	. . . . 5 |- ((w e. RR /\ 0 < w /\ w < B) -> (w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> -. B = sup(S, RR, < )))
46	45	3exp 831	. . . 4 |- (w e. RR -> (0 < w -> (w < B -> (w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)) -> -. B = sup(S, RR, < )))))
47	46	imp4d 367	. . 3 |- (w e. RR -> ((0 < w /\ (w < B /\ w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)))) -> -. B = sup(S, RR, < )))
48	47	r19.23aiv 1740	. 2 |- (E.w e. RR (0 < w /\ (w < B /\ w < ((A - (B x. B)) / (((1 + 1) + 1) x. B)))) -> -. B = sup(S, RR, < ))
49	22, 48	ax-mp 7	1 |- -. B = sup(S, RR, < )

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   /\ w3a 774   = wceq 954   e. wcel 956  E.wrex 1643  {crab 1645  ifcif 2357   class class class wbr 2614  (class class class)co 3954  supcsup 4553  RRcr 5213  0cc0 5214  1c1 5215   + caddc 5217   x. cmul 5219   - cmin 5272   / cdiv 5274   <_ cle 5275   < clt 5466

This theorem is referenced by:  sqrlem22 6632

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967