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 ) |