Metamath Proof Explorer

Theorem sqrlem5

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 , < )
sqrlem5.3 
|- T = { y | E. a e. S E. b e. S y = ( a x. b ) }
Assertion sqrlem5 
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) /\ ( B ^ 2 ) = sup ( T , RR , < ) ) )

Proof

Step Hyp Ref Expression
1 sqrlem1.1 
 |-  S = { x e. RR+ | ( x ^ 2 ) <_ A }
2 sqrlem1.2 
 |-  B = sup ( S , RR , < )
3 sqrlem5.3 
 |-  T = { y | E. a e. S E. b e. S y = ( a x. b ) }
4 1 ssrab3 
 |-  S C_ RR+
5 4 sseli 
 |-  ( v e. S -> v e. RR+ )
6 5 rpge0d 
 |-  ( v e. S -> 0 <_ v )
7 6 rgen 
 |-  A. v e. S 0 <_ v
8 1 2 sqrlem3 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) )
9 pm4.24 
 |-  ( A. v e. S 0 <_ v <-> ( A. v e. S 0 <_ v /\ A. v e. S 0 <_ v ) )
10 9 3anbi1i 
 |-  ( ( A. v e. S 0 <_ v /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) ) <-> ( ( A. v e. S 0 <_ v /\ A. v e. S 0 <_ v ) /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) ) )
11 3 10 supmullem2 
 |-  ( ( A. v e. S 0 <_ v /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) ) -> ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) )
12 7 8 8 11 mp3an2i 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) )
13 1 2 sqrlem4 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) )
14 rpre 
 |-  ( B e. RR+ -> B e. RR )
15 14 adantr 
 |-  ( ( B e. RR+ /\ B <_ 1 ) -> B e. RR )
16 13 15 syl 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> B e. RR )
17 16 recnd 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> B e. CC )
18 17 sqvald 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = ( B x. B ) )
19 2 2 oveq12i 
 |-  ( B x. B ) = ( sup ( S , RR , < ) x. sup ( S , RR , < ) )
20 3 10 supmul 
 |-  ( ( A. v e. S 0 <_ v /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) /\ ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. z e. S z <_ v ) ) -> ( sup ( S , RR , < ) x. sup ( S , RR , < ) ) = sup ( T , RR , < ) )
21 7 8 8 20 mp3an2i 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( S , RR , < ) x. sup ( S , RR , < ) ) = sup ( T , RR , < ) )
22 19 21 syl5eq 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B x. B ) = sup ( T , RR , < ) )
23 18 22 eqtrd 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = sup ( T , RR , < ) )
24 12 23 jca 
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) /\ ( B ^ 2 ) = sup ( T , RR , < ) ) )