let rseq1, rseq2 be convergent Real_Sequence; :: thesis: ( multreal * (rseq1,rseq2) is convergent_in_cod1 & multreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
set Rseq = multreal * (rseq1,rseq2);
a2: for n, m being Nat holds (multreal * (rseq1,rseq2)) . (n,m) = (rseq1 . n) * (rseq2 . m)
proof
let n, m be Nat; :: thesis: (multreal * (rseq1,rseq2)) . (n,m) = (rseq1 . n) * (rseq2 . m)
a1: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
dom (multreal * (rseq1,rseq2)) = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m] in dom (multreal * (rseq1,rseq2)) by a1, ZFMISC_1:def 2;
then (multreal * (rseq1,rseq2)) . (n,m) = multreal . ((rseq1 . n),(rseq2 . m)) by FINSEQOP:77;
hence (multreal * (rseq1,rseq2)) . (n,m) = (rseq1 . n) * (rseq2 . m) by BINOP_2:def 11; :: thesis: verum
end;
x1: for m being Element of NAT
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
proof
let m be Element of NAT ; :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e )
assume a3: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
per cases ( rseq2 . m <> 0 or rseq2 . m = 0 ) ;
suppose rseq2 . m <> 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
then a4: |.(rseq2 . m).| > 0 by COMPLEX1:47;
then consider N being Nat such that
a5: for n being Nat st n >= N holds
|.((rseq1 . n) - (lim rseq1)).| < e / |.(rseq2 . m).| by a3, SEQ_2:def 7;
take N ; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e )
assume n >= N ; :: thesis: |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
then a6: |.((rseq1 . n) - (lim rseq1)).| < e / |.(rseq2 . m).| by a5;
n is Element of NAT by ORDINAL1:def 12;
then |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| = |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (rseq2 . m))).| by MESFUNC9:def 7
.= |.(((rseq1 . n) * (rseq2 . m)) - ((lim rseq1) * (rseq2 . m))).| by a2
.= |.(((rseq1 . n) - (lim rseq1)) * (rseq2 . m)).|
.= |.((rseq1 . n) - (lim rseq1)).| * |.(rseq2 . m).| by COMPLEX1:65 ;
then |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < (e / |.(rseq2 . m).|) * |.(rseq2 . m).| by a4, a6, XREAL_1:68;
hence |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e by a4, XCMPLX_1:87; :: thesis: verum
end;
end;
suppose a7: rseq2 . m = 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
take 0 ; :: thesis: for n being Nat st n >= 0 holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= 0 implies |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e )
assume n >= 0 ; :: thesis: |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e
n is Element of NAT by ORDINAL1:def 12;
then |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| = |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (rseq2 . m))).| by MESFUNC9:def 7
.= |.(((rseq1 . n) * (rseq2 . m)) - ((lim rseq1) * (rseq2 . m))).| by a2
.= 0 by a7, COMPLEX1:44 ;
hence |.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e by a3; :: thesis: verum
end;
end;
end;
end;
p1: for m being Element of NAT holds ProjMap2 ((multreal * (rseq1,rseq2)),m) is convergent
proof
let m be Element of NAT ; :: thesis: ProjMap2 ((multreal * (rseq1,rseq2)),m) is convergent
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) * (rseq2 . m))).| < e by x1;
hence ProjMap2 ((multreal * (rseq1,rseq2)),m) is convergent by SEQ_2:def 6; :: thesis: verum
end;
hence multreal * (rseq1,rseq2) is convergent_in_cod1 ; :: thesis: ( multreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
x2: for m being Element of NAT
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
proof
let m be Element of NAT ; :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e )
assume a3: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
per cases ( rseq1 . m <> 0 or rseq1 . m = 0 ) ;
suppose rseq1 . m <> 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
then a4: |.(rseq1 . m).| > 0 by COMPLEX1:47;
then consider N being Nat such that
a5: for n being Nat st n >= N holds
|.((rseq2 . n) - (lim rseq2)).| < e / |.(rseq1 . m).| by a3, SEQ_2:def 7;
take N ; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e )
assume n >= N ; :: thesis: |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
then a6: |.((rseq2 . n) - (lim rseq2)).| < e / |.(rseq1 . m).| by a5;
n is Element of NAT by ORDINAL1:def 12;
then |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq2) * (rseq1 . m))).| = |.(((multreal * (rseq1,rseq2)) . (m,n)) - ((lim rseq2) * (rseq1 . m))).| by MESFUNC9:def 6
.= |.(((rseq2 . n) * (rseq1 . m)) - ((lim rseq2) * (rseq1 . m))).| by a2
.= |.(((rseq2 . n) - (lim rseq2)) * (rseq1 . m)).|
.= |.((rseq2 . n) - (lim rseq2)).| * |.(rseq1 . m).| by COMPLEX1:65 ;
then |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq2) * (rseq1 . m))).| < (e / |.(rseq1 . m).|) * |.(rseq1 . m).| by a4, a6, XREAL_1:68;
hence |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e by a4, XCMPLX_1:87; :: thesis: verum
end;
end;
suppose a7: rseq1 . m = 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
take 0 ; :: thesis: for n being Nat st n >= 0 holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= 0 implies |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e )
assume n >= 0 ; :: thesis: |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e
n is Element of NAT by ORDINAL1:def 12;
then |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((lim rseq2) * (rseq1 . m))).| = |.(((multreal * (rseq1,rseq2)) . (m,n)) - ((lim rseq2) * (rseq1 . m))).| by MESFUNC9:def 6
.= |.(((rseq2 . n) * (rseq1 . m)) - ((lim rseq2) * (rseq1 . m))).| by a2
.= 0 by a7, COMPLEX1:44 ;
hence |.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e by a3; :: thesis: verum
end;
end;
end;
end;
p2: for m being Element of NAT holds ProjMap1 ((multreal * (rseq1,rseq2)),m) is convergent
proof
let m be Element of NAT ; :: thesis: ProjMap1 ((multreal * (rseq1,rseq2)),m) is convergent
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) * (lim rseq2))).| < e by x2;
hence ProjMap1 ((multreal * (rseq1,rseq2)),m) is convergent by SEQ_2:def 6; :: thesis: verum
end;
hence multreal * (rseq1,rseq2) is convergent_in_cod2 ; :: thesis: ( lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
x3: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
proof
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume a3: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
a6: for n being Nat holds (lim_in_cod1 (multreal * (rseq1,rseq2))) . n = (lim rseq1) * (rseq2 . n)
proof
let n be Nat; :: thesis: (lim_in_cod1 (multreal * (rseq1,rseq2))) . n = (lim rseq1) * (rseq2 . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
a4: ProjMap2 ((multreal * (rseq1,rseq2)),n1) is convergent by p1;
a5: (lim_in_cod1 (multreal * (rseq1,rseq2))) . n = lim (ProjMap2 ((multreal * (rseq1,rseq2)),n1)) by def32;
for e being Real st 0 < e holds
ex N being Nat st
for m being Nat st m >= N holds
|.(((ProjMap2 ((multreal * (rseq1,rseq2)),n1)) . m) - ((lim rseq1) * (rseq2 . n))).| < e by x1;
hence (lim_in_cod1 (multreal * (rseq1,rseq2))) . n = (lim rseq1) * (rseq2 . n) by a5, a4, SEQ_2:def 7; :: thesis: verum
end;
per cases ( |.(lim rseq1).| > 0 or |.(lim rseq1).| = 0 ) by COMPLEX1:46;
suppose b1: |.(lim rseq1).| > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
then consider N being Nat such that
a7: for n being Nat st n >= N holds
|.((rseq2 . n) - (lim rseq2)).| < e / |.(lim rseq1).| by a3, SEQ_2:def 7;
take N ; :: thesis: for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= N implies |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume n >= N ; :: thesis: |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
then a8: |.((rseq2 . n) - (lim rseq2)).| < e / |.(lim rseq1).| by a7;
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| = |.(((lim rseq1) * (rseq2 . n)) - ((lim rseq1) * (lim rseq2))).| by a6
.= |.((lim rseq1) * ((rseq2 . n) - (lim rseq2))).|
.= |.(lim rseq1).| * |.((rseq2 . n) - (lim rseq2)).| by COMPLEX1:65 ;
hence |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e by a8, b1, XREAL_1:79; :: thesis: verum
end;
end;
suppose a9: |.(lim rseq1).| = 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
take 0 ; :: thesis: for n being Nat st n >= 0 holds
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= 0 implies |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume n >= 0 ; :: thesis: |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
|.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| = |.(((lim rseq1) * (rseq2 . n)) - ((lim rseq1) * (lim rseq2))).| by a6
.= |.((lim rseq1) * ((rseq2 . n) - (lim rseq2))).|
.= |.(lim rseq1).| * |.((rseq2 . n) - (lim rseq2)).| by COMPLEX1:65
.= 0 by a9 ;
hence |.(((lim_in_cod1 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e by a3; :: thesis: verum
end;
end;
end;
end;
hence lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent by SEQ_2:def 6; :: thesis: ( cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
hence cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) by x3, def34; :: thesis: ( lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
x4: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
proof
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume a3: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
a6: for n being Nat holds (lim_in_cod2 (multreal * (rseq1,rseq2))) . n = (rseq1 . n) * (lim rseq2)
proof
let n be Nat; :: thesis: (lim_in_cod2 (multreal * (rseq1,rseq2))) . n = (rseq1 . n) * (lim rseq2)
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
a4: ProjMap1 ((multreal * (rseq1,rseq2)),n1) is convergent by p2;
a5: (lim_in_cod2 (multreal * (rseq1,rseq2))) . n = lim (ProjMap1 ((multreal * (rseq1,rseq2)),n1)) by def33;
for e being Real st 0 < e holds
ex N being Nat st
for m being Nat st m >= N holds
|.(((ProjMap1 ((multreal * (rseq1,rseq2)),n1)) . m) - ((rseq1 . n) * (lim rseq2))).| < e by x2;
hence (lim_in_cod2 (multreal * (rseq1,rseq2))) . n = (rseq1 . n) * (lim rseq2) by a5, a4, SEQ_2:def 7; :: thesis: verum
end;
per cases ( |.(lim rseq2).| > 0 or |.(lim rseq2).| = 0 ) by COMPLEX1:46;
suppose b1: |.(lim rseq2).| > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
then consider N being Nat such that
a7: for n being Nat st n >= N holds
|.((rseq1 . n) - (lim rseq1)).| < e / |.(lim rseq2).| by a3, SEQ_2:def 7;
take N ; :: thesis: for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= N implies |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume n >= N ; :: thesis: |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
then a8: |.((rseq1 . n) - (lim rseq1)).| < e / |.(lim rseq2).| by a7;
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| = |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| by a6
.= |.(((rseq1 . n) - (lim rseq1)) * (lim rseq2)).|
.= |.(lim rseq2).| * |.((rseq1 . n) - (lim rseq1)).| by COMPLEX1:65 ;
hence |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e by a8, b1, XREAL_1:79; :: thesis: verum
end;
end;
suppose a9: |.(lim rseq2).| = 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
take 0 ; :: thesis: for n being Nat st n >= 0 holds
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= 0 implies |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e )
assume n >= 0 ; :: thesis: |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e
|.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| = |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| by a6
.= |.((lim rseq2) * ((rseq1 . n) - (lim rseq1))).|
.= |.(lim rseq2).| * |.((rseq1 . n) - (lim rseq1)).| by COMPLEX1:65
.= 0 by a9 ;
hence |.(((lim_in_cod2 (multreal * (rseq1,rseq2))) . n) - ((lim rseq1) * (lim rseq2))).| < e by a3; :: thesis: verum
end;
end;
end;
end;
hence lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent by SEQ_2:def 6; :: thesis: ( cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
hence cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) by x4, def35; :: thesis: ( multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )
x5: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e
proof
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e )
assume c1: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e
consider K being Real such that
c2: ( 0 < K & ( for n being Nat holds |.(rseq1 . n).| < K ) ) by SEQ_2:3;
set b = max (K,|.(lim rseq2).|);
c10: ( max (K,|.(lim rseq2).|) >= K & max (K,|.(lim rseq2).|) >= |.(lim rseq2).| ) by XXREAL_0:25;
then consider N1 being Nat such that
c4: for n being Nat st n >= N1 holds
|.((rseq1 . n) - (lim rseq1)).| < e / (2 * (max (K,|.(lim rseq2).|))) by c1, c2, SEQ_2:def 7;
consider N2 being Nat such that
c5: for n being Nat st n >= N2 holds
|.((rseq2 . n) - (lim rseq2)).| < e / (2 * (max (K,|.(lim rseq2).|))) by c1, c2, c10, SEQ_2:def 7;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N ; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e
thus for n, m being Nat st n >= N & m >= N holds
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e :: thesis: verum
proof
let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e )
assume c13: ( n >= N & m >= N ) ; :: thesis: |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e
( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;
then c6: ( n >= N1 & m >= N2 ) by c13, XXREAL_0:2;
c7: |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| <= |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| + |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| by COMPLEX1:63;
c11: ( |.((rseq1 . n) - (lim rseq1)).| >= 0 & |.((rseq2 . m) - (lim rseq2)).| >= 0 ) by COMPLEX1:46;
c12: ( |.(rseq1 . n).| < max (K,|.(lim rseq2).|) & |.(lim rseq2).| <= max (K,|.(lim rseq2).|) ) by c2, c10, XXREAL_0:2;
|.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| = |.(((rseq1 . n) * (rseq2 . m)) - ((rseq1 . n) * (lim rseq2))).| by a2
.= |.((rseq1 . n) * ((rseq2 . m) - (lim rseq2))).|
.= |.(rseq1 . n).| * |.((rseq2 . m) - (lim rseq2)).| by COMPLEX1:65 ;
then c8: |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| <= (max (K,|.(lim rseq2).|)) * |.((rseq2 . m) - (lim rseq2)).| by c11, c12, XREAL_1:64;
|.((rseq2 . m) - (lim rseq2)).| < e / (2 * (max (K,|.(lim rseq2).|))) by c5, c6;
then (max (K,|.(lim rseq2).|)) * |.((rseq2 . m) - (lim rseq2)).| < (max (K,|.(lim rseq2).|)) * (e / (2 * (max (K,|.(lim rseq2).|)))) by c2, c10, XREAL_1:68;
then |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| < (max (K,|.(lim rseq2).|)) * (e / (2 * (max (K,|.(lim rseq2).|)))) by c8, XXREAL_0:2;
then |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| < e / ((2 * (max (K,|.(lim rseq2).|))) / (max (K,|.(lim rseq2).|))) by XCMPLX_1:81;
then c15: |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| < e / 2 by c2, c10, XCMPLX_1:89;
|.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| = |.((lim rseq2) * ((rseq1 . n) - (lim rseq1))).|
.= |.(lim rseq2).| * |.((rseq1 . n) - (lim rseq1)).| by COMPLEX1:65 ;
then c9: |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| <= (max (K,|.(lim rseq2).|)) * |.((rseq1 . n) - (lim rseq1)).| by c11, XXREAL_0:25, XREAL_1:64;
|.((rseq1 . n) - (lim rseq1)).| < e / (2 * (max (K,|.(lim rseq2).|))) by c4, c6;
then (max (K,|.(lim rseq2).|)) * |.((rseq1 . n) - (lim rseq1)).| < (max (K,|.(lim rseq2).|)) * (e / (2 * (max (K,|.(lim rseq2).|)))) by c2, c10, XREAL_1:68;
then |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| < (max (K,|.(lim rseq2).|)) * (e / (2 * (max (K,|.(lim rseq2).|)))) by c9, XXREAL_0:2;
then |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| < e / ((2 * (max (K,|.(lim rseq2).|))) / (max (K,|.(lim rseq2).|))) by XCMPLX_1:81;
then |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| < e / 2 by c2, c10, XCMPLX_1:89;
then |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((rseq1 . n) * (lim rseq2))).| + |.(((rseq1 . n) * (lim rseq2)) - ((lim rseq1) * (lim rseq2))).| < (e / 2) + (e / 2) by c15, XREAL_1:8;
hence |.(((multreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) * (lim rseq2))).| < e by c7, XXREAL_0:2; :: thesis: verum
end;
end;
hence multreal * (rseq1,rseq2) is P-convergent ; :: thesis: P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2)
hence P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) by x5, def6; :: thesis: verum