Theorem sqrlem6 4736

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 group(s):   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		ssrab 1556	. . 3 |- {x e. RR | (0 <_ x /\ (x x. x) <_ A)} (_ RR
3	1, 2	eqsstr 1530	. 2 |- S (_ RR
4		ax0re 4063	. . . . . 6 |- 0 e. RR
5	4	leid 4339	. . . . . . 7 |- 0 <_ 0
6		0cn 4100	. . . . . . . . 9 |- 0 e. CC
7	6	mulzer1 4185	. . . . . . . 8 |- (0 x. 0) = 0
8		sqrlem1.1	. . . . . . . . 9 |- A e. RR
9		sqrlem1.2	. . . . . . . . 9 |- 0 < A
10	4, 8, 9	ltlei 4303	. . . . . . . 8 |- 0 <_ A
11	7, 10	eqbrtr 2076	. . . . . . 7 |- (0 x. 0) <_ A
12	5, 11	pm3.2i 234	. . . . . 6 |- (0 <_ 0 /\ (0 x. 0) <_ A)
13	4, 12	pm3.2i 234	. . . . 5 |- (0 e. RR /\ (0 <_ 0 /\ (0 x. 0) <_ A))
14	8, 9, 1	sqrlem4 4734	. . . . 5 |- (0 e. S <-> (0 e. RR /\ (0 <_ 0 /\ (0 x. 0) <_ A)))
15	13, 14	mpbir 165	. . . 4 |- 0 e. S
16		n0i 1712	. . . 4 |- (0 e. S -> -. S = (/))
17	15, 16	ax-mp 6	. . 3 |- -. S = (/)
18		df-ne 1192	. . 3 |- (S =/= (/) <-> -. S = (/))
19	17, 18	mpbir 165	. 2 |- S =/= (/)
20		ax1re 4064	. . . 4 |- 1 e. RR
21	20, 8	readdcl 4118	. . 3 |- (1 + A) e. RR
22	8, 9, 1	sqrlem4 4734	. . . . 5 |- (y e. S <-> (y e. RR /\ (0 <_ y /\ (y x. y) <_ A)))
23		leloet 4284	. . . . . . . . 9 |- ((0 e. RR /\ y e. RR) -> (0 <_ y <-> (0 < y \/ 0 = y)))
24	4, 23	mpan 518	. . . . . . . 8 |- (y e. RR -> (0 <_ y <-> (0 < y \/ 0 = y)))
25		breq2 2066	. . . . . . . . . . 11 |- (y = if(y e. RR, y, 1) -> (0 < y <-> 0 < if(y e. RR, y, 1)))
26		opreq12 3008	. . . . . . . . . . . . . 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)))
27	26	anidms 332	. . . . . . . . . . . . 13 |- (y = if(y e. RR, y, 1) -> (y x. y) = (if(y e. RR, y, 1) x. if(y e. RR, y, 1)))
28	27	breq1d 2071	. . . . . . . . . . . 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))))
29		breq1 2065	. . . . . . . . . . . 12 |- (y = if(y e. RR, y, 1) -> (y < (1 + A) <-> if(y e. RR, y, 1) < (1 + A)))
30	28, 29	imbi12d 474	. . . . . . . . . . 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))))
31	25, 30	imbi12d 474	. . . . . . . . . 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)))))
32		lt01 4377	. . . . . . . . . . . . 13 |- 0 < 1
33	20, 8, 32, 9	addgt0i 4326	. . . . . . . . . . . 12 |- 0 < (1 + A)
34	20	elimel 1793	. . . . . . . . . . . . . 14 |- if(y e. RR, y, 1) e. RR
35	34, 21	lt2sq 4414	. . . . . . . . . . . . 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))))
36	4, 34	ltle 4302	. . . . . . . . . . . . 13 |- (0 < if(y e. RR, y, 1) -> 0 <_ if(y e. RR, y, 1))
37	4, 21	ltle 4302	. . . . . . . . . . . . 13 |- (0 < (1 + A) -> 0 <_ (1 + A))
38	35, 36, 37	syl2an 349	. . . . . . . . . . . 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))))
39	33, 38	mpan2 519	. . . . . . . . . . 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))))
40	39	biimprd 136	. . . . . . . . . 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)))
41	31, 40	dedth 1784	. . . . . . . . 9 |- (y e. RR -> (0 < y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
42		breq1 2065	. . . . . . . . . . . 12 |- (0 = y -> (0 < (1 + A) <-> y < (1 + A)))
43	33, 42	mpbii 168	. . . . . . . . . . 11 |- (0 = y -> y < (1 + A))
44	43	a1d 14	. . . . . . . . . 10 |- (0 = y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A)))
45	44	a1i 7	. . . . . . . . 9 |- (y e. RR -> (0 = y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
46	41, 45	jaod 329	. . . . . . . 8 |- (y e. RR -> ((0 < y \/ 0 = y) -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
47	24, 46	sylbid 178	. . . . . . 7 |- (y e. RR -> (0 <_ y -> ((y x. y) < ((1 + A) x. (1 + A)) -> y < (1 + A))))
48		axmulrcl 4069	. . . . . . . . 9 |- ((y e. RR /\ y e. RR) -> (y x. y) e. RR)
49	48	anidms 332	. . . . . . . 8 |- (y e. RR -> (y x. y) e. RR)
50		leloet 4284	. . . . . . . . . 10 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) <_ A <-> ((y x. y) < A \/ (y x. y) = A)))
51	8, 9	sqrlem1 4731	. . . . . . . . . . . 12 |- A < ((1 + A) x. (1 + A))
52	21, 21	remulcl 4119	. . . . . . . . . . . . 13 |- ((1 + A) x. (1 + A)) e. RR
53		axlttrn 4084	. . . . . . . . . . . . 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))))
54	52, 53	mp3an3 641	. . . . . . . . . . . 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))))
55	51, 54	mpan2i 522	. . . . . . . . . . 11 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) < A -> (y x. y) < ((1 + A) x. (1 + A))))
56		breq1 2065	. . . . . . . . . . . . 13 |- ((y x. y) = A -> ((y x. y) < ((1 + A) x. (1 + A)) <-> A < ((1 + A) x. (1 + A))))
57	51, 56	mpbiri 169	. . . . . . . . . . . 12 |- ((y x. y) = A -> (y x. y) < ((1 + A) x. (1 + A)))
58	57	a1i 7	. . . . . . . . . . 11 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) = A -> (y x. y) < ((1 + A) x. (1 + A))))
59	55, 58	jaod 329	. . . . . . . . . 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))))
60	50, 59	sylbid 178	. . . . . . . . 9 |- (((y x. y) e. RR /\ A e. RR) -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))))
61	8, 60	mpan2 519	. . . . . . . 8 |- ((y x. y) e. RR -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))))
62	49, 61	syl 12	. . . . . . 7 |- (y e. RR -> ((y x. y) <_ A -> (y x. y) < ((1 + A) x. (1 + A))))
63	47, 62	syl5d 53	. . . . . 6 |- (y e. RR -> (0 <_ y -> ((y x. y) <_ A -> y < (1 + A))))
64	63	imp32 281	. . . . 5 |- (