Metamath Proof Explorer

Theorem sqrlem2

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 sqrlem2 
|- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S )

Proof

Step Hyp Ref Expression
1 sqrlem1.1 
 |-  S = { x e. RR+ | ( x ^ 2 ) <_ A }
2 sqrlem1.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 mulid2d 
 |-  ( 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 )