Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- { y e. RR+ | ( y ^ 2 ) <_ A } = { y e. RR+ | ( y ^ 2 ) <_ A } |
2 |
|
eqid |
|- sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) = sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) |
3 |
1 2
|
sqrlem4 |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) e. RR+ /\ sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) <_ 1 ) ) |
4 |
|
eqid |
|- { z | E. w e. { y e. RR+ | ( y ^ 2 ) <_ A } E. x e. { y e. RR+ | ( y ^ 2 ) <_ A } z = ( w x. x ) } = { z | E. w e. { y e. RR+ | ( y ^ 2 ) <_ A } E. x e. { y e. RR+ | ( y ^ 2 ) <_ A } z = ( w x. x ) } |
5 |
1 2 4
|
sqrlem7 |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) = A ) |
6 |
|
breq1 |
|- ( x = sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) -> ( x <_ 1 <-> sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) <_ 1 ) ) |
7 |
|
oveq1 |
|- ( x = sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) -> ( x ^ 2 ) = ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) ) |
8 |
7
|
eqeq1d |
|- ( x = sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) -> ( ( x ^ 2 ) = A <-> ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) = A ) ) |
9 |
6 8
|
anbi12d |
|- ( x = sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) -> ( ( x <_ 1 /\ ( x ^ 2 ) = A ) <-> ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) <_ 1 /\ ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) = A ) ) ) |
10 |
9
|
rspcev |
|- ( ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) e. RR+ /\ ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) <_ 1 /\ ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) = A ) ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) ) |
11 |
10
|
anassrs |
|- ( ( ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) e. RR+ /\ sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) <_ 1 ) /\ ( sup ( { y e. RR+ | ( y ^ 2 ) <_ A } , RR , < ) ^ 2 ) = A ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) ) |
12 |
3 5 11
|
syl2anc |
|- ( ( A e. RR+ /\ A <_ 1 ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) ) |