Theorem sqrlem6 6678

Description: Lemma for square root theorem.

Hypotheses

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

Assertion

Ref	Expression
sqrlem6	|- (S (_ RR /\ S =/= (/) /\ E.x e. RR A.y e. S y < x)

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

Proof of Theorem sqrlem6

Step	Hyp	Ref	Expression
1		sqrlem4.3	. . 3 |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}
2		ssrab2 2131	. . 3 |- {x e. RR | (0 <_ x /\ (x x. x) <_ A)} (_ RR
3	1, 2	eqsstr 2091	. 2 |- S (_ RR
4		sqrlem1.1	. . . . . 6 |- A e. RR
5		sqrlem1.2	. . . . . 6 |- 0 < A
6	4, 5, 1	sqrlem4 6676	. . . . 5 |- (0 e. S <-> (0 e. RR /\ (0 <_ 0 /\ (0 x. 0) <_ A)))
7		0re 5440	. . . . 5 |- 0 e. RR
8	7	leid 5610	. . . . . 6 |- 0 <_ 0
9		0cn 5328	. . . . . . . 8 |- 0 e. CC
10	9	mul01 5431	. . . . . . 7 |- (0 x. 0) = 0
11	7, 4, 5	ltlei 5581	. . . . . . 7 |- 0 <_ A
12	10, 11	eqbrtr 2634	. . . . . 6 |- (0 x. 0) <_ A
13	8, 12	pm3.2i 285	. . . . 5 |- (0 <_ 0 /\ (0 x. 0) <_ A)
14	6, 7, 13	mpbir2an 730	. . . 4 |- 0 e. S
15		n0i 2285	. . . 4 |- (0 e. S -> -. S = (/))
16	14, 15	ax-mp 7	. . 3 |- -. S = (/)
17		df-ne 1587	. . 3 |- (S =/= (/) <-> -. S = (/))
18	16, 17	mpbir 190	. 2 |- S =/= (/)
19		1re 5435	. . . 4 |- 1 e. RR
20	19, 4	readdcl 5334	. . 3 |- (1 + A) e. RR
21	4, 5, 1	sqrlem4 6676	. . . . 5 |- (y e. S <-> (y e. RR /\ (0 <_ y /\ (y x. y) <_ A)))
22		leloet 5518	. . . . . . . . 9 |- ((0 e. RR /\ y e. RR) -> (0 <_ y <-> (0 < y \/ 0 = y)))
23	7, 22	mpan 695	. . . . . . . 8 |- (y e. RR -> (0 <_ y <-> (0 < y \/ 0 = y)))
24		breq2 2623	. . . . . . . . . . 11 |- (y = if(y e. RR, y, 1) -> (0 < y <-> 0 < if(y e. RR, y, 1)))
25		opreq12 3970	. . . . . . . . . . . . . 14 |- ((y = if(y e. RR, y, 1) /\ y = if(y e. RR, y, 1)) -> (y x. y) = (if(y e. RR, y, 1) x. if(y e. RR, y, 1)))
26	25	anidms 434	. . . . . . . . . . . . 13 |- (y = if(y e. RR, y, 1) -> (y x. y) = (if(y e. RR, y, 1) x. if(y e. RR, y, 1)))
27	26	breq1d 2629	. . . . . . . . . . . 12 |- (y = if(y e. RR, y, 1) -> ((y x. y) < ((1 + A) x. (1 + A)) <-> (if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A))))
28		breq1 2622	. . . . . . . . . . . 12 |- (y = if(y e. RR, y, 1) -> (y < (1 + A) <-> if(y e. RR, y, 1) < (1 + A)))
29	27, 28	imbi12d 626	. . . . . . . . . . 11 |- (y = if(y e. RR, y, 1) -> (((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A)) <-> ((if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A)) -> if(y e. RR, y, 1) < (1 + A))))
30	24, 29	imbi12d 626	. . . . . . . . . 10 |- (y = if(y e. RR, y, 1) -> ((0 < y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))) <-> (0 < if(y e. RR, y, 1) -> ((if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A)) -> if(y e. RR, y, 1) < (1 + A)))))
31		lt01 5680	. . . . . . . . . . . . 13 |- 0 < 1
32	19, 4, 31, 5	addgt0i 5601	. . . . . . . . . . . 12 |- 0 < (1 + A)
33	19	elimel 2394	. . . . . . . . . . . . . 14 |- if(y e. RR, y, 1) e. RR
34	33, 20	lt2msq 5881	. . . . . . . . . . . . 13 |- ((0 <_ if(y e. RR, y, 1) /\ 0 <_ (1 + A)) -> (if(y e. RR, y, 1) < (1 + A) <-> (if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A))))
35	7, 33	ltle 5580	. . . . . . . . . . . . 13 |- (0 < if(y e. RR, y, 1) -> 0 <_ if(y e. RR, y, 1))
36	7, 20	ltle 5580	. . . . . . . . . . . . 13 |- (0 < (1 + A) -> 0 <_ (1 + A))
37	34, 35, 36	syl2an 454	. . . . . . . . . . . 12 |- ((0 < if(y e. RR, y, 1) /\ 0 < (1 + A)) -> (if(y e. RR, y, 1) < (1 + A) <-> (if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A))))
38	32, 37	mpan2 696	. . . . . . . . . . 11 |- (0 < if(y e. RR, y, 1) -> (if(y e. RR, y, 1) < (1 + A) <-> (if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A))))
39	38	biimprd 154	. . . . . . . . . 10 |- (0 < if(y e. RR, y, 1) -> ((if(y e. RR, y, 1) x. if(y e. RR, y, 1)) < ((1 + A) x. (1 + A)) -> if(y e. RR, y, 1) < (1 + A)))
40	30, 39	dedth 2383	. . . . . . . . 9 |- (y e. RR -> (0 < y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
41		breq1 2622	. . . . . . . . . . . 12 |- (0 = y -> (0 < (1 + A) <-> y < (1 + A)))
42	32, 41	mpbii 193	. . . . . . . . . . 11 |- (0 = y -> y < (1 + A))
43	42	a1d 12	. . . . . . . . . 10 |- (0 = y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A)))
44	43	a1i 8	. . . . . . . . 9 |- (y e. RR -> (0 = y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
45	40, 44	jaod 424	. . . . . . . 8 |- (y e. RR -> ((0 < y \/ 0 = y) -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
46	23, 45	sylbid 203	. . . . . . 7 |- (y e. RR -> (0 <_ y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
47		axmulrcl 5274	. . . . . . . . 9 |- ((y e. RR /\ y e. RR) -> (y x. y) e. RR)
48	47	anidms 434	. . . . . . . 8 |- (y e. RR -> (y x. y) e. RR)
49		leloet 5518	. . . . . . . . . 10 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) <_ A <-> ((y x. y) < A \/ (y x. y) = A)))
50	4, 5	sqrlem1 6673	. . . . . . . . . . . 12 |- A < ((1 + A) x. (1 + A))
51	20, 20	remulcl 5335	. . . . . . . . . . . . 13 |- ((1 + A) x. (1 + A)) e. RR
52		axlttrn 5504	. . . . . . . . . . . . 13 |- (((y x. y) e. RR /\ A e. RR /\ ((1 + A) x. (1 + A)) e. RR) -> (((y x. y) < A /\ A < ((1 + A) x. (1 + A))) -> (y x. y) < ((1 + A) x. (1 + A))))
53	51, 52	mp3an3 905	. . . . . . . . . . . 12 |- (((y x. y) e. RR /\ A e. RR) -> (((y x. y) < A /\ A < ((1 + A) x. (1 + A))) -> (y x. y) < ((1 + A) x. (1 + A))))
54	50, 53	mpan2i 699	. . . . . . . . . . 11 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) < A -> (y x. y) < ((1 + A) x. (1 + A))))
55		breq1 2622	. . . . . . . . . . . . 13 |- ((y x. y) = A -> ((y x. y) < ((1 + A) x. (1 + A)) <-> A < ((1 + A) x. (1 + A))))
56	50, 55	mpbiri 194	. . . . . . . . . . . 12 |- ((y x. y) = A -> (y x. y) < ((1 + A) x. (1 + A)))
57	56	a1i 8	. . . . . . . . . . 11 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) = A -> (y x. y) < ((1 + A) x. (1 + A))))
58	54, 57	jaod 424	. . . . . . . . . 10 |- (((y x. y) e. RR /\ A e. RR) -> (((y x. y) < A \/ (y x. y) = A) -> (y x. y) < ((1 + A) x. (1 + A))))
59	49, 58	sylbid 203	. . . . . . . . 9 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))))
60	4, 59	mpan2 696	. . . . . . . 8 |- ((y x. y) e. RR -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))))
61	48, 60	syl 10	. . . . . . 7 |- (y e. RR -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))