| 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 ) ) |