let s be Real; ( 1 < s & s + (1 / s) < sqrt 5 implies ( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 ) )
assume that
A1:
1 < s
and
A2:
s + (1 / s) < sqrt 5
; ( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )
A4: (- (1 * (sqrt 5))) ^2 =
((- 1) ^2) * ((sqrt 5) ^2)
.=
5
by SQUARE_1:def 2
;
s * (s + (1 / s)) < s * (sqrt 5)
by A1, A2, XREAL_1:68;
then
(s * s) + ((s * 1) / s) < s * (sqrt 5)
;
then
(s * s) + 1 < s * (sqrt 5)
by A1, XCMPLX_0:def 7;
then A5:
((s * s) + 1) - (s * (sqrt 5)) < (s * (sqrt 5)) - (s * (sqrt 5))
by XREAL_1:14;
set a = 1;
set b = - (sqrt 5);
set c = 1;
A7:
((1 * (s ^2)) + ((- (sqrt 5)) * s)) + 1 < 0
by A5;
A6: delta (1,(- (sqrt 5)),1) =
((- (sqrt 5)) ^2) - ((4 * 1) * 1)
by QUIN_1:def 1
.=
1
by A4
;
then
((- (- (sqrt 5))) + (sqrt (delta (1,(- (sqrt 5)),1)))) / (2 * 1) = ((sqrt 5) + 1) / 2
by SQUARE_1:18;
then A8:
s < ((sqrt 5) + 1) / 2
by A7, A6, QUIN_1:26;
(sqrt 5) - 1 <> 0
by SQRT2;
then A9:
((sqrt 5) - 1) / ((sqrt 5) - 1) = 1
by XCMPLX_1:60;
1 / (((sqrt 5) + 1) / 2) =
(2 / ((sqrt 5) + 1)) * (((sqrt 5) - 1) / ((sqrt 5) - 1))
by A9, XCMPLX_1:57
.=
(2 * ((sqrt 5) - 1)) / (((sqrt 5) + 1) * ((sqrt 5) - 1))
by XCMPLX_1:76
.=
(2 * ((sqrt 5) - 1)) / (((sqrt 5) ^2) - 1)
.=
(2 * ((sqrt 5) - 1)) / (5 - 1)
by SQUARE_1:def 2
.=
((sqrt 5) - 1) / 2
;
hence
( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )
by A1, A8, XREAL_1:88; verum