| Step |
Hyp |
Ref |
Expression |
| 1 |
|
01sqrexlem1.1 |
|- S = { x e. RR+ | ( x ^ 2 ) <_ A } |
| 2 |
|
01sqrexlem1.2 |
|- B = sup ( S , RR , < ) |
| 3 |
|
simpl |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. RR+ ) |
| 4 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
| 5 |
|
rpgt0 |
|- ( A e. RR+ -> 0 < A ) |
| 6 |
|
1re |
|- 1 e. RR |
| 7 |
|
lemul1 |
|- ( ( A e. RR /\ 1 e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( A <_ 1 <-> ( A x. A ) <_ ( 1 x. A ) ) ) |
| 8 |
6 7
|
mp3an2 |
|- ( ( A e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( A <_ 1 <-> ( A x. A ) <_ ( 1 x. A ) ) ) |
| 9 |
4 4 5 8
|
syl12anc |
|- ( A e. RR+ -> ( A <_ 1 <-> ( A x. A ) <_ ( 1 x. A ) ) ) |
| 10 |
9
|
biimpa |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( A x. A ) <_ ( 1 x. A ) ) |
| 11 |
|
rpcn |
|- ( A e. RR+ -> A e. CC ) |
| 12 |
11
|
adantr |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. CC ) |
| 13 |
|
sqval |
|- ( A e. CC -> ( A ^ 2 ) = ( A x. A ) ) |
| 14 |
13
|
eqcomd |
|- ( A e. CC -> ( A x. A ) = ( A ^ 2 ) ) |
| 15 |
12 14
|
syl |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( A x. A ) = ( A ^ 2 ) ) |
| 16 |
11
|
mullidd |
|- ( A e. RR+ -> ( 1 x. A ) = A ) |
| 17 |
16
|
adantr |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( 1 x. A ) = A ) |
| 18 |
10 15 17
|
3brtr3d |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( A ^ 2 ) <_ A ) |
| 19 |
|
oveq1 |
|- ( x = A -> ( x ^ 2 ) = ( A ^ 2 ) ) |
| 20 |
19
|
breq1d |
|- ( x = A -> ( ( x ^ 2 ) <_ A <-> ( A ^ 2 ) <_ A ) ) |
| 21 |
20 1
|
elrab2 |
|- ( A e. S <-> ( A e. RR+ /\ ( A ^ 2 ) <_ A ) ) |
| 22 |
3 18 21
|
sylanbrc |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S ) |