Metamath Proof Explorer

Theorem 01sqrexlem6

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Hypotheses 01sqrexlem1.1 
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }
01sqrexlem1.2 
|- B = sup ( S , RR , < )
01sqrexlem5.3 
|- T = { y | E. a e. S E. b e. S y = ( a x. b ) }
Assertion 01sqrexlem6 
|- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) <_ A )

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 
 |-  S = { x e. RR+ | ( x ^ 2 ) <_ A }
2 01sqrexlem1.2 
 |-  B = sup ( S , RR , < )
3 01sqrexlem5.3 
 |-  T = { y | E. a e. S E. b e. S y = ( a x. b ) }
4 1 2 3 01sqrexlem5 
 |-  ( ( 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 01sqrexlem3 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 )