This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 01sqrexlem1

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

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

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 
 |-  S = { x e. RR+ | ( x ^ 2 ) <_ A }
2 01sqrexlem1.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 biimtrid 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( y e. S -> y <_ 1 ) )
29 28 ralrimiv 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> A. y e. S y <_ 1 )