Metamath Proof Explorer


Theorem sqrlem1

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Hypotheses sqrlem1.1
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
sqrlem1.2
|- B = sup ( S , RR , < )
Assertion sqrlem1
|- ( ( A e. RR+ /\ A <_ 1 ) -> A. y e. S y <_ 1 )

Proof

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 )