let s be Real_Sequence; :: thesis: for a being real number st a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
let a be real number ; :: thesis: ( a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )
assume A1:
a >= 1
; :: thesis: ( ex n being Element of NAT st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )
assume A2:
for n being Element of NAT st n >= 1 holds
s . n = n -Root a
; :: thesis: ( s is convergent & lim s = 1 )
deffunc H1( Element of NAT ) -> Element of REAL = (a - 1) / ($1 + 1);
consider s1 being Real_Sequence such that
A3:
for n being Element of NAT holds s1 . n = H1(n)
from SEQ_1:sch 1();
A4:
( s1 is convergent & lim s1 = 0 )
by A3, SEQ_4:46;
reconsider s2 = NAT --> 1 as Real_Sequence by FUNCOP_1:57;
set s3 = s2 + s1;
A6:
s2 + s1 is convergent
by A4, SEQ_2:19;
A7: lim (s2 + s1) =
(s2 . 0 ) + 0
by A4, SEQ_4:59
.=
1
by FUNCOP_1:13
;
A8: lim s2 =
s2 . 0
by SEQ_4:41
.=
1
by FUNCOP_1:13
;
A9:
now let n be
Element of
NAT ;
:: thesis: ( s2 . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (s2 + s1) . n )A10:
n + 1
>= 0 + 1
by XREAL_1:8;
A11:
(s ^\ 1) . n =
s . (n + 1)
by NAT_1:def 3
.=
(n + 1) -Root a
by A2, A10
;
then A12:
(s ^\ 1) . n >= 1
by A1, A10, Th38;
then A13:
((s ^\ 1) . n) - 1
>= 0
by XREAL_1:50;
set b =
((s ^\ 1) . n) - 1;
A14:
- 1
< ((s ^\ 1) . n) - 1
by A13, XXREAL_0:2;
a = (1 + (((s ^\ 1) . n) - 1)) |^ (n + 1)
by A1, A10, A11, Lm2;
then
a >= 1
+ ((n + 1) * (((s ^\ 1) . n) - 1))
by A14, Th24;
then
a - 1
>= (1 + ((n + 1) * (((s ^\ 1) . n) - 1))) - 1
by XREAL_1:11;
then
(a - 1) * ((n + 1) " ) >= ((n + 1) " ) * ((n + 1) * (((s ^\ 1) . n) - 1))
by XREAL_1:66;
then
(a - 1) * ((n + 1) " ) >= (((n + 1) " ) * (n + 1)) * (((s ^\ 1) . n) - 1)
;
then
(a - 1) * ((n + 1) " ) >= 1
* (((s ^\ 1) . n) - 1)
by XCMPLX_0:def 7;
then
(a - 1) / (n + 1) >= ((s ^\ 1) . n) - 1
;
then
((a - 1) / (n + 1)) + 1
>= (((s ^\ 1) . n) - 1) + 1
by XREAL_1:8;
then
(s2 . n) + ((a - 1) / (n + 1)) >= (s ^\ 1) . n
by FUNCOP_1:13;
then
(s2 . n) + (s1 . n) >= (s ^\ 1) . n
by A3;
hence
(
s2 . n <= (s ^\ 1) . n &
(s ^\ 1) . n <= (s2 + s1) . n )
by A12, FUNCOP_1:13, SEQ_1:11;
:: thesis: verum end;
then A15:
s ^\ 1 is convergent
by A6, A7, A8, SEQ_2:33;
A16:
lim (s ^\ 1) = 1
by A6, A7, A8, A9, SEQ_2:34;
thus
s is convergent
by A15, SEQ_4:35; :: thesis: lim s = 1
thus
lim s = 1
by A15, A16, SEQ_4:36; :: thesis: verum