Theorem sqrlem3

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Hypotheses	sqrlem1.1	|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
	sqrlem1.2	|- B = sup ( S , RR , < )
Assertion	sqrlem3	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. z e. RR A. y e. S y <_ z ) )

Proof

Step	Hyp	Ref	Expression
1		sqrlem1.1	|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
2		sqrlem1.2	|- B = sup ( S , RR , < )
3		ssrab2	|- { x e. RR+ | ( x ^ 2 ) <_ A } C_ RR+
4		rpssre	|- RR+ C_ RR
5	3 4	sstri	|- { x e. RR+ | ( x ^ 2 ) <_ A } C_ RR
6	1 5	eqsstri	|- S C_ RR
7	6	a1i	|- ( ( A e. RR+ /\ A <_ 1 ) -> S C_ RR )
8	1 2	sqrlem2	|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S )
9	8	ne0d	|- ( ( A e. RR+ /\ A <_ 1 ) -> S =/= (/) )
10		1re	|- 1 e. RR
11	1 2	sqrlem1	|- ( ( A e. RR+ /\ A <_ 1 ) -> A. y e. S y <_ 1 )
12		brralrspcev	|- ( ( 1 e. RR /\ A. y e. S y <_ 1 ) -> E. z e. RR A. y e. S y <_ z )
13	10 11 12	sylancr	|- ( ( A e. RR+ /\ A <_ 1 ) -> E. z e. RR A. y e. S y <_ z )
14	7 9 13	3jca	|- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. z e. RR A. y e. S y <_ z ) )