let a be Real; :: thesis: for s being Real_Sequence st a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
let s be Real_Sequence; :: thesis: ( a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )
assume A1: a > 0 ; :: thesis: ( ex n being Nat st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )
assume A2: for n being Nat st n >= 1 holds
s . n = n -Root a ; :: thesis: ( s is convergent & lim s = 1 )
per cases ( a >= 1 or a < 1 ) ;
suppose a >= 1 ; :: thesis: ( s is convergent & lim s = 1 )
hence ( s is convergent & lim s = 1 ) by A2, Lm3; :: thesis: verum
end;
suppose A3: a < 1 ; :: thesis: ( s is convergent & lim s = 1 )
then a / a < 1 / a by A1, XREAL_1:74;
then A4: 1 <= 1 / a by A1, XCMPLX_1:60;
deffunc H1( Nat) -> Real = $1 -Root (1 / a);
consider s1 being Real_Sequence such that
A5: for n being Nat holds s1 . n = H1(n) from SEQ_1:sch 1();
A6: for n being Nat st n >= 1 holds
s1 . n = n -Root (1 / a) by A5;
then A7: lim s1 = 1 by A4, Lm3;
A8: s1 is convergent by A4, A6, Lm3;
A9: now :: thesis: for b being Real st b > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - 1).| < b
let b be Real; :: thesis: ( b > 0 implies ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - 1).| < b )
assume b > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - 1).| < b
then consider m1 being Nat such that
A10: for m being Nat st m1 <= m holds
|.((s1 . m) - 1).| < b by A8, A7, SEQ_2:def 7;
reconsider n = m1 + 1 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s . m) - 1).| < b
let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 1).| < b )
assume A11: n <= m ; :: thesis: |.((s . m) - 1).| < b
A12: n >= 0 + 1 by XREAL_1:6;
then A13: 1 <= m by A11, XXREAL_0:2;
then A14: m -Root a < 1 by A1, A3, Th30;
A15: m -Root a <> 0 by A1, A13, Def2;
then A16: |.((1 / (m -Root a)) - 1).| = |.((1 / (m -Root a)) - ((m -Root a) / (m -Root a))).| by XCMPLX_1:60
.= |.((1 - (m -Root a)) / (m -Root a)).|
.= |.((1 - (m -Root a)) * ((m -Root a) ")).|
.= |.(1 - (m -Root a)).| * |.((m -Root a) ").| by COMPLEX1:65 ;
0 < m -Root a by A1, A3, A13, Th30;
then (m -Root a) * ((m -Root a) ") < 1 * ((m -Root a) ") by A14, XREAL_1:68;
then 1 < (m -Root a) " by A15, XCMPLX_0:def 7;
then A17: 1 < |.((m -Root a) ").| by ABSVALUE:def 1;
0 <> 1 - (m -Root a) by A1, A3, A13, Th30;
then |.(1 - (m -Root a)).| > 0 by COMPLEX1:47;
then A18: 1 * |.(1 - (m -Root a)).| < |.(1 - (m -Root a)).| * |.((m -Root a) ").| by A17, XREAL_1:68;
m1 <= n by XREAL_1:29;
then m1 <= m by A11, XXREAL_0:2;
then |.((s1 . m) - 1).| < b by A10;
then |.((m -Root (1 / a)) - 1).| < b by A5;
then |.((1 / (m -Root a)) - 1).| < b by A1, A13, Th23;
then |.(- ((m -Root a) - 1)).| < b by A16, A18, XXREAL_0:2;
then |.((m -Root a) - 1).| < b by COMPLEX1:52;
hence |.((s . m) - 1).| < b by A2, A12, A11, XXREAL_0:2; :: thesis: verum
end;
hence s is convergent by SEQ_2:def 6; :: thesis: lim s = 1
hence lim s = 1 by A9, SEQ_2:def 7; :: thesis: verum
end;
end;