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 eqtrid
 |-  ( ( 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 , < ) ) )