Metamath Proof Explorer

Theorem 01sqrexlem3

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

Ref Expression
Hypotheses 01sqrexlem1.1 
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
01sqrexlem1.2 
|- B = sup ( S , RR , < )
Assertion 01sqrexlem3 
|- ( ( 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 01sqrexlem1.1 
 |-  S = { x e. RR+ | ( x ^ 2 ) <_ A }
2 01sqrexlem1.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 01sqrexlem2 
 |-  ( ( 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 01sqrexlem1 
 |-  ( ( 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 ) )