let seq1, seq2 be Real_Sequence; :: thesis: for k being positive Real st ( for n being Nat holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds
( seq1 is convergent iff seq2 is convergent )
let k be positive Real; :: thesis: ( ( for n being Nat holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) implies ( seq1 is convergent iff seq2 is convergent ) )
assume A1: for n being Nat holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ; :: thesis: ( seq1 is convergent iff seq2 is convergent )
A2: for n being Nat holds seq1 . n >= 0
proof
let n be Nat; :: thesis: seq1 . n >= 0
(seq2 . n) to_power k >= 0 by A1, Th4;
hence seq1 . n >= 0 by A1; :: thesis: verum
end;
thus ( seq1 is convergent implies seq2 is convergent ) :: thesis: ( seq2 is convergent implies seq1 is convergent )
proof
assume A3: seq1 is convergent ; :: thesis: seq2 is convergent
for n being Nat holds seq2 . n = (seq1 . n) to_power (1 / k)
proof
let n be Nat; :: thesis: seq2 . n = (seq1 . n) to_power (1 / k)
(seq1 . n) to_power (1 / k) = ((seq2 . n) to_power k) to_power (1 / k) by A1
.= (seq2 . n) to_power (k * (1 / k)) by A1, HOLDER_1:2
.= (seq2 . n) to_power 1 by XCMPLX_1:106 ;
hence seq2 . n = (seq1 . n) to_power (1 / k) by POWER:25; :: thesis: verum
end;
hence seq2 is convergent by A2, A3, HOLDER_1:10; :: thesis: verum
end;
assume seq2 is convergent ; :: thesis: seq1 is convergent
hence seq1 is convergent by A1, HOLDER_1:10; :: thesis: verum