let p be Real; :: thesis: ( 1 <= p implies for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being Nat holds rseq . n = 0 )
assume A1: 1 <= p ; :: thesis: for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being Nat holds rseq . n = 0
A2: 1 / p > 0 by A1, XREAL_1:139;
let rseq be Real_Sequence; :: thesis: ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 implies for n being Nat holds rseq . n = 0 )
assume that
A3: rseq rto_power p is summable and
A4: (Sum (rseq rto_power p)) to_power (1 / p) = 0 ; :: thesis: for n being Nat holds rseq . n = 0
A5: for i being Nat holds (rseq rto_power p) . i >= 0
proof
let i be Nat; :: thesis: (rseq rto_power p) . i >= 0
(rseq rto_power p) . i = |.(rseq . i).| to_power p by Def1;
hence (rseq rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; :: thesis: verum
end;
then ((Sum (rseq rto_power p)) to_power (1 / p)) to_power p = (Sum (rseq rto_power p)) to_power ((1 / p) * p) by A1, A2, A3, HOLDER_1:2, SERIES_1:18
.= (Sum (rseq rto_power p)) to_power 1 by A1, XCMPLX_1:106
.= Sum (rseq rto_power p) by POWER:25 ;
then A6: Sum (rseq rto_power p) = 0 by A1, A4, POWER:def 2;
now :: thesis: for n being Nat holds rseq . n = 0
let n be Nat; :: thesis: rseq . n = 0
reconsider n9 = n as Nat ;
A7: 0 to_power (1 / p) = 0 by A2, POWER:def 2;
(rseq rto_power p) . n9 = |.(rseq . n9).| to_power p by Def1;
then A8: |.(rseq . n).| to_power p = 0 by A3, A5, A6, RSSPACE:17;
(|.(rseq . n).| to_power p) to_power (1 / p) = |.(rseq . n).| to_power (p * (1 / p)) by A1, A2, COMPLEX1:46, HOLDER_1:2
.= |.(rseq . n).| to_power 1 by A1, XCMPLX_1:106
.= |.(rseq . n).| by POWER:25 ;
hence rseq . n = 0 by A8, A7, ABSVALUE:2; :: thesis: verum
end;
hence for n being Nat holds rseq . n = 0 ; :: thesis: verum