Metamath Proof Explorer

Theorem 01sqrex

Description: Existence of a square root for reals in the interval ( 0 , 1 ] . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Assertion 01sqrex 
|- ( ( A e. RR+ /\ A <_ 1 ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) )

Proof

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 01sqrexlem4 
 |-  ( ( 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 01sqrexlem7 
 |-  ( ( 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 ) )