Step |
Hyp |
Ref |
Expression |
1 |
|
sqrlem1.1 |
|- S = { x e. RR+ | ( x ^ 2 ) <_ A } |
2 |
|
sqrlem1.2 |
|- B = sup ( S , RR , < ) |
3 |
|
oveq1 |
|- ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) ) |
4 |
3
|
breq1d |
|- ( x = y -> ( ( x ^ 2 ) <_ A <-> ( y ^ 2 ) <_ A ) ) |
5 |
4 1
|
elrab2 |
|- ( y e. S <-> ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) |
6 |
|
simprr |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( y ^ 2 ) <_ A ) |
7 |
|
simplr |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> A <_ 1 ) |
8 |
|
rpre |
|- ( y e. RR+ -> y e. RR ) |
9 |
8
|
ad2antrl |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> y e. RR ) |
10 |
9
|
resqcld |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( y ^ 2 ) e. RR ) |
11 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
12 |
11
|
ad2antrr |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> A e. RR ) |
13 |
|
1re |
|- 1 e. RR |
14 |
|
letr |
|- ( ( ( y ^ 2 ) e. RR /\ A e. RR /\ 1 e. RR ) -> ( ( ( y ^ 2 ) <_ A /\ A <_ 1 ) -> ( y ^ 2 ) <_ 1 ) ) |
15 |
13 14
|
mp3an3 |
|- ( ( ( y ^ 2 ) e. RR /\ A e. RR ) -> ( ( ( y ^ 2 ) <_ A /\ A <_ 1 ) -> ( y ^ 2 ) <_ 1 ) ) |
16 |
10 12 15
|
syl2anc |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( ( ( y ^ 2 ) <_ A /\ A <_ 1 ) -> ( y ^ 2 ) <_ 1 ) ) |
17 |
6 7 16
|
mp2and |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( y ^ 2 ) <_ 1 ) |
18 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
19 |
17 18
|
breqtrrdi |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( y ^ 2 ) <_ ( 1 ^ 2 ) ) |
20 |
|
rpge0 |
|- ( y e. RR+ -> 0 <_ y ) |
21 |
20
|
ad2antrl |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> 0 <_ y ) |
22 |
|
0le1 |
|- 0 <_ 1 |
23 |
|
le2sq |
|- ( ( ( y e. RR /\ 0 <_ y ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( y <_ 1 <-> ( y ^ 2 ) <_ ( 1 ^ 2 ) ) ) |
24 |
13 22 23
|
mpanr12 |
|- ( ( y e. RR /\ 0 <_ y ) -> ( y <_ 1 <-> ( y ^ 2 ) <_ ( 1 ^ 2 ) ) ) |
25 |
9 21 24
|
syl2anc |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> ( y <_ 1 <-> ( y ^ 2 ) <_ ( 1 ^ 2 ) ) ) |
26 |
19 25
|
mpbird |
|- ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( y e. RR+ /\ ( y ^ 2 ) <_ A ) ) -> y <_ 1 ) |
27 |
26
|
ex |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( y e. RR+ /\ ( y ^ 2 ) <_ A ) -> y <_ 1 ) ) |
28 |
5 27
|
syl5bi |
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( y e. S -> y <_ 1 ) ) |
29 |
28
|
ralrimiv |
|- ( ( A e. RR+ /\ A <_ 1 ) -> A. y e. S y <_ 1 ) |