Metamath Proof Explorer


Theorem sqrlem6

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 sqrlem6
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) <_ A )

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 2 3 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 , < ) ) )
5 4 simprd
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = sup ( T , RR , < ) )
6 vex
 |-  v e. _V
7 eqeq1
 |-  ( y = v -> ( y = ( a x. b ) <-> v = ( a x. b ) ) )
8 7 2rexbidv
 |-  ( y = v -> ( E. a e. S E. b e. S y = ( a x. b ) <-> E. a e. S E. b e. S v = ( a x. b ) ) )
9 6 8 3 elab2
 |-  ( v e. T <-> E. a e. S E. b e. S v = ( a x. b ) )
10 oveq1
 |-  ( x = a -> ( x ^ 2 ) = ( a ^ 2 ) )
11 10 breq1d
 |-  ( x = a -> ( ( x ^ 2 ) <_ A <-> ( a ^ 2 ) <_ A ) )
12 11 1 elrab2
 |-  ( a e. S <-> ( a e. RR+ /\ ( a ^ 2 ) <_ A ) )
13 12 simplbi
 |-  ( a e. S -> a e. RR+ )
14 oveq1
 |-  ( x = b -> ( x ^ 2 ) = ( b ^ 2 ) )
15 14 breq1d
 |-  ( x = b -> ( ( x ^ 2 ) <_ A <-> ( b ^ 2 ) <_ A ) )
16 15 1 elrab2
 |-  ( b e. S <-> ( b e. RR+ /\ ( b ^ 2 ) <_ A ) )
17 16 simplbi
 |-  ( b e. S -> b e. RR+ )
18 rpre
 |-  ( a e. RR+ -> a e. RR )
19 18 adantr
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> a e. RR )
20 rpre
 |-  ( b e. RR+ -> b e. RR )
21 20 adantl
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> b e. RR )
22 rpgt0
 |-  ( b e. RR+ -> 0 < b )
23 22 adantl
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> 0 < b )
24 lemul1
 |-  ( ( a e. RR /\ b e. RR /\ ( b e. RR /\ 0 < b ) ) -> ( a <_ b <-> ( a x. b ) <_ ( b x. b ) ) )
25 19 21 21 23 24 syl112anc
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> ( a <_ b <-> ( a x. b ) <_ ( b x. b ) ) )
26 13 17 25 syl2an
 |-  ( ( a e. S /\ b e. S ) -> ( a <_ b <-> ( a x. b ) <_ ( b x. b ) ) )
27 17 rpcnd
 |-  ( b e. S -> b e. CC )
28 27 sqvald
 |-  ( b e. S -> ( b ^ 2 ) = ( b x. b ) )
29 28 breq2d
 |-  ( b e. S -> ( ( a x. b ) <_ ( b ^ 2 ) <-> ( a x. b ) <_ ( b x. b ) ) )
30 29 adantl
 |-  ( ( a e. S /\ b e. S ) -> ( ( a x. b ) <_ ( b ^ 2 ) <-> ( a x. b ) <_ ( b x. b ) ) )
31 26 30 bitr4d
 |-  ( ( a e. S /\ b e. S ) -> ( a <_ b <-> ( a x. b ) <_ ( b ^ 2 ) ) )
32 31 adantl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a <_ b <-> ( a x. b ) <_ ( b ^ 2 ) ) )
33 16 simprbi
 |-  ( b e. S -> ( b ^ 2 ) <_ A )
34 33 ad2antll
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( b ^ 2 ) <_ A )
35 13 rpred
 |-  ( a e. S -> a e. RR )
36 17 rpred
 |-  ( b e. S -> b e. RR )
37 remulcl
 |-  ( ( a e. RR /\ b e. RR ) -> ( a x. b ) e. RR )
38 35 36 37 syl2an
 |-  ( ( a e. S /\ b e. S ) -> ( a x. b ) e. RR )
39 38 adantl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a x. b ) e. RR )
40 36 resqcld
 |-  ( b e. S -> ( b ^ 2 ) e. RR )
41 40 ad2antll
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( b ^ 2 ) e. RR )
42 rpre
 |-  ( A e. RR+ -> A e. RR )
43 42 ad2antrr
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> A e. RR )
44 letr
 |-  ( ( ( a x. b ) e. RR /\ ( b ^ 2 ) e. RR /\ A e. RR ) -> ( ( ( a x. b ) <_ ( b ^ 2 ) /\ ( b ^ 2 ) <_ A ) -> ( a x. b ) <_ A ) )
45 39 41 43 44 syl3anc
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( ( ( a x. b ) <_ ( b ^ 2 ) /\ ( b ^ 2 ) <_ A ) -> ( a x. b ) <_ A ) )
46 34 45 mpan2d
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( ( a x. b ) <_ ( b ^ 2 ) -> ( a x. b ) <_ A ) )
47 32 46 sylbid
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a <_ b -> ( a x. b ) <_ A ) )
48 rpgt0
 |-  ( a e. RR+ -> 0 < a )
49 48 adantr
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> 0 < a )
50 lemul2
 |-  ( ( b e. RR /\ a e. RR /\ ( a e. RR /\ 0 < a ) ) -> ( b <_ a <-> ( a x. b ) <_ ( a x. a ) ) )
51 21 19 19 49 50 syl112anc
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> ( b <_ a <-> ( a x. b ) <_ ( a x. a ) ) )
52 13 17 51 syl2an
 |-  ( ( a e. S /\ b e. S ) -> ( b <_ a <-> ( a x. b ) <_ ( a x. a ) ) )
53 13 rpcnd
 |-  ( a e. S -> a e. CC )
54 53 sqvald
 |-  ( a e. S -> ( a ^ 2 ) = ( a x. a ) )
55 54 breq2d
 |-  ( a e. S -> ( ( a x. b ) <_ ( a ^ 2 ) <-> ( a x. b ) <_ ( a x. a ) ) )
56 55 adantr
 |-  ( ( a e. S /\ b e. S ) -> ( ( a x. b ) <_ ( a ^ 2 ) <-> ( a x. b ) <_ ( a x. a ) ) )
57 52 56 bitr4d
 |-  ( ( a e. S /\ b e. S ) -> ( b <_ a <-> ( a x. b ) <_ ( a ^ 2 ) ) )
58 57 adantl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( b <_ a <-> ( a x. b ) <_ ( a ^ 2 ) ) )
59 12 simprbi
 |-  ( a e. S -> ( a ^ 2 ) <_ A )
60 59 ad2antrl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a ^ 2 ) <_ A )
61 35 resqcld
 |-  ( a e. S -> ( a ^ 2 ) e. RR )
62 61 ad2antrl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a ^ 2 ) e. RR )
63 letr
 |-  ( ( ( a x. b ) e. RR /\ ( a ^ 2 ) e. RR /\ A e. RR ) -> ( ( ( a x. b ) <_ ( a ^ 2 ) /\ ( a ^ 2 ) <_ A ) -> ( a x. b ) <_ A ) )
64 39 62 43 63 syl3anc
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( ( ( a x. b ) <_ ( a ^ 2 ) /\ ( a ^ 2 ) <_ A ) -> ( a x. b ) <_ A ) )
65 60 64 mpan2d
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( ( a x. b ) <_ ( a ^ 2 ) -> ( a x. b ) <_ A ) )
66 58 65 sylbid
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( b <_ a -> ( a x. b ) <_ A ) )
67 1 2 sqrlem3
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. y e. RR A. v e. S v <_ y ) )
68 67 simp1d
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> S C_ RR )
69 68 sseld
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( a e. S -> a e. RR ) )
70 68 sseld
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( b e. S -> b e. RR ) )
71 69 70 anim12d
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( ( a e. S /\ b e. S ) -> ( a e. RR /\ b e. RR ) ) )
72 71 imp
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a e. RR /\ b e. RR ) )
73 letric
 |-  ( ( a e. RR /\ b e. RR ) -> ( a <_ b \/ b <_ a ) )
74 72 73 syl
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a <_ b \/ b <_ a ) )
75 47 66 74 mpjaod
 |-  ( ( ( A e. RR+ /\ A <_ 1 ) /\ ( a e. S /\ b e. S ) ) -> ( a x. b ) <_ A )
76 75 ex
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( ( a e. S /\ b e. S ) -> ( a x. b ) <_ A ) )
77 breq1
 |-  ( v = ( a x. b ) -> ( v <_ A <-> ( a x. b ) <_ A ) )
78 77 biimprcd
 |-  ( ( a x. b ) <_ A -> ( v = ( a x. b ) -> v <_ A ) )
79 76 78 syl6
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( ( a e. S /\ b e. S ) -> ( v = ( a x. b ) -> v <_ A ) ) )
80 79 rexlimdvv
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( E. a e. S E. b e. S v = ( a x. b ) -> v <_ A ) )
81 9 80 syl5bi
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( v e. T -> v <_ A ) )
82 81 ralrimiv
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> A. v e. T v <_ A )
83 4 simpld
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) )
84 42 adantr
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> A e. RR )
85 suprleub
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) /\ A e. RR ) -> ( sup ( T , RR , < ) <_ A <-> A. v e. T v <_ A ) )
86 83 84 85 syl2anc
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( sup ( T , RR , < ) <_ A <-> A. v e. T v <_ A ) )
87 82 86 mpbird
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> sup ( T , RR , < ) <_ A )
88 5 87 eqbrtrd
 |-  ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) <_ A )