| Step |
Hyp |
Ref |
Expression |
| 1 |
|
01sqrexlem1.1 |
|- S = { x e. RR+ | ( x ^ 2 ) <_ A } |
| 2 |
|
01sqrexlem1.2 |
|- B = sup ( S , RR , < ) |
| 3 |
1 2
|
01sqrexlem3 |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) ) |
| 4 |
|
suprcl |
|- ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) -> sup ( S , RR , < ) e. RR ) |
| 5 |
3 4
|
syl |
|- ( ( A e. RR+ /\ A <_ 1 ) -> sup ( S , RR , < ) e. RR ) |
| 6 |
2 5
|
eqeltrid |
|- ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR ) |
| 7 |
|
rpgt0 |
|- ( A e. RR+ -> 0 < A ) |
| 8 |
7
|
adantr |
|- ( ( A e. RR+ /\ A <_ 1 ) -> 0 < A ) |
| 9 |
1 2
|
01sqrexlem2 |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S ) |
| 10 |
|
suprub |
|- ( ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) /\ A e. S ) -> A <_ sup ( S , RR , < ) ) |
| 11 |
3 9 10
|
syl2anc |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A <_ sup ( S , RR , < ) ) |
| 12 |
11 2
|
breqtrrdi |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A <_ B ) |
| 13 |
|
0re |
|- 0 e. RR |
| 14 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
| 15 |
|
ltletr |
|- ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) ) |
| 16 |
13 14 6 15
|
mp3an2ani |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) ) |
| 17 |
8 12 16
|
mp2and |
|- ( ( A e. RR+ /\ A <_ 1 ) -> 0 < B ) |
| 18 |
6 17
|
elrpd |
|- ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR+ ) |
| 19 |
1 2
|
01sqrexlem1 |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A. z e. S z <_ 1 ) |
| 20 |
|
1re |
|- 1 e. RR |
| 21 |
|
suprleub |
|- ( ( ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. z e. S z <_ y ) /\ 1 e. RR ) -> ( sup ( S , RR , < ) <_ 1 <-> A. z e. S z <_ 1 ) ) |
| 22 |
3 20 21
|
sylancl |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( S , RR , < ) <_ 1 <-> A. z e. S z <_ 1 ) ) |
| 23 |
19 22
|
mpbird |
|- ( ( A e. RR+ /\ A <_ 1 ) -> sup ( S , RR , < ) <_ 1 ) |
| 24 |
2 23
|
eqbrtrid |
|- ( ( A e. RR+ /\ A <_ 1 ) -> B <_ 1 ) |
| 25 |
18 24
|
jca |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) ) |