Презентация на тему Системы компьютерной алгебры. Maple, mathematica, derive

интеллектуальных систем, проф. Подколзин А.С., http://intsys.msu.ru)

seq' is convergent implies seq + seq' is convergent

by A1,Def6;
consider g2 such that
A4: for p st 0

by A2,Def6;
take g=g1+g2;
let p; assume
0

Mizar
Библиотека: около 1000 статей, десятки тысяч теорем, около 150 авторов
http://mizar.org

n1 such that
A6: for m st n1

take k=n1+n2;
let m such that
A8: k<=m;
n1<=n1+n2 by NAT_1:37;
then n1<=m by A8,XREAL_1:2;
then A9: abs(seq.m-g1)

n2<=k by NAT_1:37;
then n2<=m by A8,XREAL_1:2;
then abs(seq'.m-g2)

then A10: abs(seq.m-g1)+abs(seq'.m-g2)

A11: abs((seq+seq').m-g)=abs(seq.m+seq'.m-(g1+g2)) by SEQ_1:11
.=abs(seq.m-g1+(seq'.m-g2));
abs(seq.m-g1+(seq'.m-g2))<=abs(seq.m-g1)+abs(seq'.m-g2) by COMPLEX1:142;
hence abs((seq+seq').m-g)

end;