Theorem sqrlem20 6622

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 5307	. . . . 5 |- (B x. B) e. RR
4	2, 3	resubcl 5411	. . . 4 |- (A - (B x. B)) e. RR
5		1re 5407	. . . . . . 7 |- 1 e. RR
6	5, 5	readdcl 5306	. . . . . 6 |- (1 + 1) e. RR
7	6, 5	readdcl 5306	. . . . 5 |- ((1 + 1) + 1) e. RR
8	7, 1	remulcl 5307	. . . 4 |- (((1 + 1) + 1) x. B) e. RR
9	7	recn 5286	. . . . 5 |- ((1 + 1) + 1) e. CC
10	1	recn 5286	. . . . 5 |- B e. CC
11		lt01 5653	. . . . . . . 8 |- 0 < 1
12	5, 5, 11, 11	addgt0i 5575	. . . . . . 7 |- 0 < (1 + 1)
13	6, 5, 12, 11	addgt0i 5575	. . . . . 6 |- 0 < ((1 + 1) + 1)
14	7, 13	gt0ne0i 5591	. . . . 5 |- ((1 + 1) + 1) =/= 0
15		sqrlem15.4	. . . . . 6 |- 0 < B
16	1, 15	gt0ne0i 5591	. . . . 5 |- B =/= 0
17	9, 10, 14, 16	muln0 5668	. . . 4 |- (((1 + 1) + 1) x. B) =/= 0
18	4, 8, 17	redivcl 5754	. . 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 6621	. . 3 |- 0 < ((A - (B x. B)) / (((1 + 1) + 1) x. B))
22	1, 18, 15, 21	posex 5856	. 2 |- E.w e. RR (0 < w /\ (w < B /\ w < ((A - (B x. B)) / (((1 + 1) + 1) x. B))))
23		breq1 2612	. . . . . . 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 611	. . . . . 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 1526	. . . . . . . . . 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 2613	. . . . . . . . . 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 2612	. . . . . . . . . 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 890	. . . . . . . . 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 1526	. . . . . . . . . 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 2613	. . . . . . . . . 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 2612	. . . . . . . . . 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 890	. . . . . . . . 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 5591	. . . . . . . . . . 11 |- (1 + 1) =/= 0
34	1, 6, 33	redivcl 5754	. . . . . . . . . 10 |- (B / (1 + 1)) e. RR
35	1, 6, 15, 12	divgt0i 5814	. . . . . . . . . 10 |- 0 < (B / (1 + 1))
36	1	halfpos 5852	. . . . . . . . . . 11 |- (0 < B <-> (B / (1 + 1)) < B)
37	15, 36	mpbi 189	. . . . . . . . . 10 |- (B / (1 + 1)) < B
38	34, 35, 37	3pm3.2i 816	. . . . . . . . 9 |- ((B / (1 + 1)) e. RR /\ 0 < (B / (1 + 1)) /\ (B / (1 + 1)) < B)
39	28, 32, 38	elimhyp 2380	. . . . . . . 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 789	. . . . . . 7 |- if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1))) e. RR
41	39	3simp2i 790	. . . . . . 7 |- 0 < if((w e. RR /\ 0 < w /\ w < B), w, (B / (1 + 1)))
42	39	3simp3i 791	. . . . . . 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 6620	. . . . . 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 2373	. . . . 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 830	. . . 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 1735	. 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 773   = wceq 953   e. wcel 955  E.wrex 1638  {crab 1640  ifcif 2351   class class class wbr 2609  (class class class)co 3948  supcsup 4547  RRcr 5205  0cc0 5206  1c1 5207   + caddc 5209   x. cmul 5211   - cmin 5264   / cdiv 5266   <_ cle 5267   < clt 5458

This theorem is referenced by:  sqrlem22 6624

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