:: The {C}atalan Numbers. {P}art {II}
:: by Karol P\c{a}k
::
:: Received October 31, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, ORDINAL1, FINSET_1,
RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1,
XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, FUNCOP_1, BINOP_2, FUNCT_2, SEQ_1,
SERIES_1, VALUED_1, SQUARE_1, COMPLEX1, PARTFUN3, ZFMISC_1, CARD_FIN,
REALSET1, CATALAN1, REAL_1, ORDINAL2, SEQ_2, NEWTON, PREPOWER, FUNCT_3,
CATALAN2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, XCMPLX_0, XREAL_0, ORDINAL1,
NUMBERS, RELAT_1, FUNCT_1, REAL_1, NAT_1, FINSET_1, XXREAL_0, NAT_D,
AFINSQ_1, SEQ_1, VALUED_1, RELSET_1, DOMAIN_1, FUNCT_2, FUNCOP_1,
BINOP_1, BINOP_2, RECDEF_1, SERIES_1, PARTFUN3, AFINSQ_2, ZFMISC_1,
SQUARE_1, NEWTON, STIRL2_1, CARD_FIN, CATALAN1, SEQ_2, PREPOWER,
COMPLEX1, QUIN_1;
constructors QUIN_1, PREPOWER, SERIES_1, PARTFUN3, BINOM, WELLORD2, DOMAIN_1,
SETWISEO, REAL_1, NAT_D, YELLOW20, RECDEF_1, BINOP_2, RELSET_1, SQUARE_1,
CATALAN1, STIRL2_1, CARD_FIN, AFINSQ_2, ABIAN, SEQ_2, COMSEQ_2, NUMBERS,
NEWTON;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FINSET_1, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
BINOP_2, CARD_1, AFINSQ_1, RELSET_1, VALUED_1, VALUED_0, MEMBERED,
NEWTON, AFINSQ_2, SERIES_1, SQUARE_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities QUIN_1, SQUARE_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems CATALAN1, AFINSQ_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1,
NAT_1, FUNCT_2, XCMPLX_1, CARD_2, INT_1, ORDINAL1, WELLORD2, CARD_1,
BINOP_2, NEWTON, XREAL_1, FUNCOP_1, STIRL2_1, FUNCT_1, CARD_FIN,
SERIES_1, SEQ_1, SEQ_2, COMPLEX1, SQUARE_1, ABSVALUE, RSSPACE2, POWER,
PREPOWER, WSIERP_1, FIB_NUM, TIETZE, XREAL_0, SERIES_2, XXREAL_0, NAT_D,
AFINSQ_2, XTUPLE_0, NUMBERS, FINSEQ_4;
schemes FUNCT_2, NAT_1, XBOOLE_0, STIRL2_1;
begin
reserve x, x1, x2, y, X, D for set,
i, j, k, l, m, n, N for Nat,
p, q for XFinSequence of NAT,
q9 for XFinSequence,
pd, qd for XFinSequence of D;
definition
let p,q;
redefine func p^q -> XFinSequence of NAT; :: redefines ^ (AFINSQ_1, redefinition) → ^ (ORDINAL4, definition)
coherence;
end;
theorem Th1:
ex qd st pd = (pd|n)^qd
proof
consider q9 such that
A1: pd = (pd|n)^q9 by AFINSQ_1:60;
rng q9 c= rng pd by A1,AFINSQ_1:25;
then rng q9 c= D by XBOOLE_1:1;
then q9 is XFinSequence of D by RELAT_1:def 19;
hence thesis by A1;
end;
definition
let p;
attr p is dominated_by_0 means
rng p c= {0,1} & for k st k <= dom p holds 2*Sum (p|k) <= k;
end;
theorem Th2:
p is dominated_by_0 implies 2*Sum (p|k) <= k
proof
assume
A1: p is dominated_by_0;
now
per cases;
suppose
k <= dom p;
hence thesis by A1;
end;
suppose
A2: k > dom p;
then Segm len p c= Segm k by NAT_1:39;
then
A3: p|k=p by RELAT_1:68;
2 * Sum (p|(len p)) <= dom p & p|(len p)=p by A1;
hence thesis by A2,A3,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th3:
p is dominated_by_0 implies p.0 = 0
proof
assume
A1: p is dominated_by_0;
now
per cases;
suppose
not 0 in dom p;
hence thesis by FUNCT_1:def 2;
end;
suppose
0 in dom p;
then len p >= 1 by NAT_1:14;
then
A2: Segm 1 c= Segm len p by NAT_1:39;
0 in Segm 1 by NAT_1:44;
then 0 in dom p /\ Segm 1 by A2,XBOOLE_0:def 4;
then
A3: (p|1).0=p.0 by FUNCT_1:48;
A4: Sum <%p.0%>= addnat"**"<%p.0%> by AFINSQ_2:51
.= p.0 by AFINSQ_2:37;
len (p|1)=1 by A2,RELAT_1:62;
then p|1=<%p.0%> by A3,AFINSQ_1:34;
then 2*(p.0)<=1+(0 qua Nat) by A1,A4,Th2;
then 2*(p.0)=1 or 2*(p.0)=0 by NAT_1:9;
hence thesis by NAT_1:15;
end;
end;
hence thesis;
end;
registration let x;let k be Nat;
cluster x-->k -> NAT-valued;
coherence;
end;
Lm1: n <= m implies (m-->k)|n = (n-->k)
proof
assume n <= m;
then Segm n c= Segm m by NAT_1:39;
then n/\m = n by XBOOLE_1:28;
hence thesis by FUNCOP_1:12;
end;
Lm2: (k-->0) is dominated_by_0
proof
rng (k-->0) c={0} & {0} c= {0,1} by FUNCOP_1:13,ZFMISC_1:7;
hence rng (k-->0) c={0,1};
let n;
assume n <= dom (k-->0);
then
A2: (k-->0)|n =(n-->0) by Lm1;
Sum (n-->0) =0*n by AFINSQ_2:58;
hence thesis by A2;
end;
registration
cluster empty dominated_by_0 for XFinSequence of NAT;
existence
proof
(0-->0) is dominated_by_0 by Lm2;
hence thesis;
end;
cluster non empty dominated_by_0 for XFinSequence of NAT;
existence
proof
(1-->0) is dominated_by_0 by Lm2;
hence thesis;
end;
end;
theorem
n-->0 is dominated_by_0 by Lm2;
theorem Th5:
n >= m implies (n-->0)^(m-->1) is dominated_by_0
proof
assume
A1: n>=m;
set p=(n-->0)^(m-->1);
rng (m-->1) c= {1} & {1} c= {0,1} by FUNCOP_1:13,ZFMISC_1:7;
then
A2: rng (m-->1) c= {0,1};
rng (n-->0) c={0} & {0} c= {0,1} by FUNCOP_1:13,ZFMISC_1:7;
then rng (n-->0) c= {0,1};
then rng (n-->0) \/ rng (m-->1) c= {0,1} by A2,XBOOLE_1:8;
hence rng p c= {0,1} by AFINSQ_1:26;
let k such that
A3: k <= dom p;
now
per cases;
suppose
A4: k <= dom (n-->0);
A5: (n-->0)|k = (k-->0) by A4,Lm1;
A6: Sum (k-->0)=0*k by AFINSQ_2:58;
p|k=(n-->0)|k by A4,AFINSQ_1:58;
hence thesis by A5,A6;
end;
suppose
k > dom (n-->0);
then reconsider kd=k-dom (n-->0) as Nat by NAT_1:21;
k<=len (n-->0)+len (m-->1) by A3,AFINSQ_1:17;
then k-len (n-->0)<=len (m-->1)+len (n-->0)-len (n-->0) by XREAL_1:9;
then kd <= m;
then
A8: (m-->1)|kd = (kd-->1) by Lm1;
reconsider m1 = m-->1 as XFinSequence of NAT;
k=kd+dom (n-->0);
then p|k = (n-->0)^(m1|kd) by AFINSQ_1:59;
then
A9: Sum(p|k)=Sum (n-->0) + Sum (kd-->1) by A8,AFINSQ_2:55;
dom p= len (n-->0) +len (m-->1) & dom (m-->1)=m by AFINSQ_1:def 3
;
then k-n <= m+n-n by A3,XREAL_1:9;
then k-n <= n by A1,XXREAL_0:2;
then
A10: k-n+(k-n)<=n+(k-n) by XREAL_1:6;
Sum (n-->0) =n*0 & Sum (kd-->1)=kd*1 by AFINSQ_2:58;
hence thesis by A9,A10;
end;
end;
hence thesis;
end;
theorem Th6:
p is dominated_by_0 implies p|n is dominated_by_0
proof
assume
A1: p is dominated_by_0;
A2: for k st k<=dom (p|n) holds 2*Sum((p|n)|k)<=k
proof
let k;
assume k <= dom (p|n);
then
A3: Segm k c= Segm len(p|n) by NAT_1:39;
dom (p|n) = dom p/\n by RELAT_1:61;
then (p|n)|k=p|k by A3,RELAT_1:74,XBOOLE_1:18;
hence thesis by A1,Th2;
end;
rng (p|n) c= rng p & rng p c= {0,1} by A1;
then rng(p|n)c={0,1};
hence thesis by A2;
end;
theorem Th7:
p is dominated_by_0 & q is dominated_by_0 implies p^q is dominated_by_0
proof
assume that
A1: p is dominated_by_0 and
A2: q is dominated_by_0;
rng p c= {0,1} & rng q c= {0,1} by A1,A2;
then rng p \/rng q c= {0,1} by XBOOLE_1:8;
hence rng (p^q) c= {0,1} by AFINSQ_1:26;
let k such that
k <= dom (p^q);
now
per cases;
suppose
A3: k <= dom p;
then (p^q)|k=p|k by AFINSQ_1:58;
hence thesis by A1,A3;
end;
suppose
k>dom p;
then reconsider kd=k-dom p as Nat by NAT_1:21;
k=kd+dom p;
then (p^q)|k=p^(q|kd) by AFINSQ_1:59;
then
A4: Sum((p^q)|k)=Sum p+Sum(q|kd) by AFINSQ_2:55;
2 * Sum (p|(len p)) <= len p & 2 * Sum (q|kd)<= kd by A1,A2,Th2;
then 2* Sum p + 2 * Sum (q|kd)<=dom p+kd by XREAL_1:7;
hence thesis by A4;
end;
end;
hence thesis;
end;
theorem Th8:
p is dominated_by_0 implies 2 * Sum (p|(2*n+1)) < 2*n+1
proof
assume p is dominated_by_0;
then
A1: 2 * Sum (p|(2*n+1)) <= 2 * n + 1 by Th2;
assume 2 * Sum (p|(2*n+1))>= 2 * n + 1;
then 2 * Sum (p|(2*n+1))= 2 * n + 1 by A1,XXREAL_0:1;
then 2 * (Sum (p|(2*n+1))-n)=1;
hence thesis by INT_1:9;
end;
theorem Th9:
p is dominated_by_0 & n <= len p-2*Sum p implies p^(n-->1) is dominated_by_0
proof
set q=(n-->1);
assume that
A1: p is dominated_by_0 and
A2: n <= len p- 2 * Sum p;
rng q c= {1} & {1} c= {0,1} by FUNCOP_1:13,ZFMISC_1:7;
then
A3: rng q c= {0,1};
rng p c= {0,1} by A1;
then rng p \/ rng q c= {0,1} by A3,XBOOLE_1:8;
hence rng (p^q) c= {0,1} by AFINSQ_1:26;
let m such that
A4: m <= dom (p^q);
now
per cases;
suppose
m <= dom p;
then (p^q)|m=p|m by AFINSQ_1:58;
hence thesis by A1,Th2;
end;
suppose
m > dom p;
then reconsider md=m-dom p as Nat by NAT_1:21;
A5: m=dom p+ md;
Sum (md-->1)=md*1 by AFINSQ_2:58;
then
A6: Sum (p^(md-->1))=Sum p+ md by AFINSQ_2:55;
dom q = n & len q = dom q;
then dom (p^q)= len p + n by AFINSQ_1:def 3;
then md+dom p<=n+dom p by A4;
then
A7: md <= n by XREAL_1:6;
then q|md = md-->1 by Lm1;
then (p^q)|m=p^(md-->1) by A5,AFINSQ_1:59;
then 2*Sum ((p^q)|m)= 2 * Sum p + m-dom p +md by A6;
then
A8: 2*Sum ((p^q)|m) <=2 * Sum p+m-dom p+n by A7,XREAL_1:6;
n-n<=len p- 2 * Sum p-n by A2,XREAL_1:9;
then m-(len p-2 * Sum p-n)<=m-0 by XREAL_1:10;
hence thesis by A8,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th10:
p is dominated_by_0 & n <= k+len p-2*Sum p implies (k-->0)^p^(n
-->1) is dominated_by_0
proof
assume that
A1: p is dominated_by_0 and
A2: n <= k + len p - 2 * Sum p;
set q=(k-->0);
dom q=k & len q =dom q;
then
A3: len (q^p)=k+len p by AFINSQ_1:17;
Sum q=k*0 by AFINSQ_2:58;
then
A4: Sum (q^p)=(0 qua Nat)+ Sum p by AFINSQ_2:55;
q is dominated_by_0 by Lm2;
then q^p is dominated_by_0 by A1,Th7;
hence thesis by A2,A3,A4,Th9;
end;
theorem Th11:
p is dominated_by_0 & 2*Sum (p|k)=k implies k <= len p & len (p| k) = k
proof
assume
A1: p is dominated_by_0 & 2 * Sum (p|k)=k;
A2: k <= len p
proof
A3: p|len p=p;
assume
A4: k > len p;
then Segm len p c= Segm k by NAT_1:39;
then p|k=p by RELAT_1:68;
hence thesis by A1,A4,A3;
end;
then Segm k c= Segm len p by NAT_1:39;
then dom p/\k=k by XBOOLE_1:28;
hence thesis by A2,RELAT_1:61;
end;
theorem Th12:
p is dominated_by_0 & 2*Sum (p|k) = k & p = (p|k)^q implies q is
dominated_by_0
proof
assume that
A1: p is dominated_by_0 and
A2: 2 * Sum (p|k)=k and
A3: p = (p|k)^q;
A4: len (p|k)=k by A1,A2,Th11;
rng q c= rng p & rng p c= {0,1} by A1,A3,AFINSQ_1:25;
hence rng q c= {0,1};
let n such that
n <= dom q;
p|(len (p|k)+n)=(p|k)^(q|n) by A3,AFINSQ_1:59;
then
A5: Sum (p|(len (p|k)+n))= Sum (p|k)+ Sum (q|n) by AFINSQ_2:55;
2* Sum (p|(len (p|k)+n))<= len (p|k)+n by A1,Th2;
then k+ 2 * Sum (q|n) <= len (p|k)+n by A2,A5;
hence thesis by A4,XREAL_1:6;
end;
theorem Th13:
p is dominated_by_0 & 2*Sum (p|k) = k & k = n+1 implies p|k = p| n^(1-->1)
proof
assume that
A1: p is dominated_by_0 and
A2: 2 * Sum (p|k) = k and
A3: k = n+1;
reconsider q=p|k as XFinSequence of NAT;
q.n=1
proof
Sum (p|k)<>0 by A2,A3;
then reconsider s=Sum (p|k)-1 as Nat by NAT_1:14,21;
A4: q is dominated_by_0 by A1,Th6;
then
A5: rng q c= {0,1};
2*s+1=n by A2,A3;
then
A6: Sum <%0%> = 0 & 2*Sum(q|n)<n by A4,Th8,AFINSQ_2:53;
A7: len q=n+1 by A1,A2,A3,Th11;
then
A8: q=(q|n)^<%q.n%> by AFINSQ_1:56;
n<n+1 by NAT_1:13;
then n in Segm(n+1) by NAT_1:44;
then
A9: q.n in rng q by A7,FUNCT_1:3;
assume q.n<>1;
then q.n=0 by A5,A9,TARSKI:def 2;
then Sum q= Sum(q|n) +Sum <%0%> by A8,AFINSQ_2:55;
hence thesis by A2,A3,A6,NAT_1:13;
end;
then
A10: dom <%q.n%>=1 & rng <%q.n%>={1} by AFINSQ_1:33;
n<=n+1 by NAT_1:11;
then Segm n c= Segm k by A3,NAT_1:39;
then
A11: q|n = p|n by RELAT_1:74;
len q=n+1 by A1,A2,A3,Th11;
then q=q|n^<%q.n%> by AFINSQ_1:56;
hence thesis by A11,A10,FUNCOP_1:9;
end;
theorem Th14:
for m,p st m = min*({N:2*Sum(p|N) = N & N > 0}) & m > 0 & p is
dominated_by_0 ex q st p|m = (1-->0)^q^(1-->1) & q is dominated_by_0
proof
A1: dom <%0%>=1 & rng <%0%>={0} by AFINSQ_1:33;
set q1=(1-->1);
set q0=(1-->0);
let m,p such that
A2: m = min*({N: 2*Sum(p|N)=N & N>0}) & m > 0 and
A3: p is dominated_by_0;
reconsider M={N: 2*Sum(p|N)=N & N>0} as non empty Subset of NAT by A2,
NAT_1:def 1;
min* M in M by NAT_1:def 1;
then consider n be Nat such that
A4: n=min*M and
A5: 2*Sum(p|n)=n and
A6: n>0;
reconsider n1=n-1 as Nat by A6,NAT_1:20;
Sum(p|n)<>0 by A5,A6;
then n>=2*1 by A5,NAT_1:14,XREAL_1:64;
then
A7: n1>=2-1 by XREAL_1:9;
then
A8: Segm 1 c= Segm n1 by NAT_1:39;
then
A9: (p|n1)|1=p|1 by RELAT_1:74;
A10: n1 < n1+1 by NAT_1:13;
n <= len p by A3,A5,Th11;
then
A11: n1 < len p by A10,XXREAL_0:2;
then 1 < len p by A7,XXREAL_0:2;
then len (p|1)=1 by AFINSQ_1:11;
then
A12: p|1 = <%(p|1).0%> by AFINSQ_1:34;
p|1 is dominated_by_0 by A3,Th6;then
(p|1).0=0 by Th3;
then
A13: p|1=1-->0 by A12,A1,FUNCOP_1:9;
consider q such that
A14: (p|n1) = (p|n1)|1 ^ q by Th1;
set qq=q0^q^q1;
take q;
A15: p|(n1+1)=p|n1^(1-->1) by A3,A5,Th13;
hence p|m =qq by A2,A4,A14,A8,A13,RELAT_1:74;
rng q c= rng (q0^q) & rng (q0^q) c= rng qq by AFINSQ_1:24,25;
then
A16: rng q c= rng qq;
p|m is dominated_by_0 by A3,Th6;
then rng qq c= {0,1} by A2,A4,A14,A13,A9,A15;
hence rng q c= {0,1} by A16;
A17: dom q0=1;
len (p|n1)=n1 by A11,AFINSQ_1:11;
then
A18: n1=len q0+ len q by A14,A13,A9,AFINSQ_1:17;
let k;
assume k <= dom q;
then
A19: len q0 + k <= n1 by A18,XREAL_1:6;
then Segm(len q0 +k) c= Segm n1 by NAT_1:39;
then
A20: (p|n1)|(1+k) =p|(1+k) by RELAT_1:74;
A21: 1+k <n by A15,A19,NAT_1:13;
A22: 2*Sum(p|(1+k)) < 1+k
proof
assume
A23: 2*Sum(p|(1+k)) >= 1+k;
2*Sum (p|(k+1))<=k+1 by A3,Th2;
then 2*Sum(p|(1+k))=1+k by A23,XXREAL_0:1;
then 1+k in M;
hence thesis by A4,A21,NAT_1:def 1;
end;
(p|n1)|(1+k)=q0^q|k by A14,A13,A9,A17,AFINSQ_1:59;
then
A24: Sum(p|(1+k))=Sum q0 + Sum (q|k) by A20,AFINSQ_2:55;
Sum (q0)=0*1 by AFINSQ_2:58;
hence thesis by A24,A22,NAT_1:13;
end;
theorem Th15:
for p st rng p c= {0,1} & p is not dominated_by_0 ex k st 2*k+1
= min*{N : 2*Sum(p|N) > N} & 2*k+1 <= dom p & k = Sum (p|(2*k)) & p.(2*k) = 1
proof
let p such that
A1: rng p c= {0,1} and
A2: p is not dominated_by_0;
set M={N : 2*Sum(p|N) > N};
M c= NAT
proof
let x be object;
assume x in M;
then ex N st x=N & 2*Sum(p|N) > N;
hence thesis by ORDINAL1:def 12;
end;
then reconsider M as Subset of NAT;
consider k be Nat such that
A3: k <= dom p and
A4: 2*Sum(p|k) > k by A1,A2;
reconsider k as Nat;
k in M by A4;
then reconsider M as non empty Subset of NAT;
min*M in M by NAT_1:def 1;
then consider n be Nat such that
A5: min*M=n and
A6: 2*Sum(p|n) > n;
A7: Sum(p|0) = 0;
Sum(p|n) > 0 by A6;
then n>0 by A7;
then reconsider n1=n-1 as Nat by NAT_1:20;
reconsider S=Sum(p|n1) as Nat;
take S;
k in M by A4;
then
A8: k >= n by A5,NAT_1:def 1;
then
A9: dom p >= n by A3,XXREAL_0:2;
A10: 2*Sum(p|n1) = n1
proof
A11: n1 < n1+1 by NAT_1:13;
then Segm n1 c= Segm(n1+1) by NAT_1:39;
then
A12: (p|n)|n1=p|n1 by RELAT_1:74;
n = len p & p|dom p = p or n <len p by A9,XXREAL_0:1;
then
A13: len(p|n) = n1+1 by AFINSQ_1:11;
then n1 in Segm(len (p|n)) by A11,NAT_1:44;
then
A14: (p|n).n1 in rng(p|n) by FUNCT_1:3;
(p|n)=((p|n)|n1)^<%(p|n).n1%> by A13,AFINSQ_1:56;
then Sum(p|n)=Sum(p|n1)+ Sum <%(p|n).n1%> by A12,AFINSQ_2:55;
then
A15: 2*Sum(p|n1)+ 2* Sum <%(p|n).n1%> >= n+1 by A6,NAT_1:13;
n1 < n1+1 by NAT_1:13;
then not n1 in M by A5,NAT_1:def 1;
then
A16: 2*Sum(p|n1) <= n1;
(p|n).n1 in {0,1} by A1,A14;
then
A17: (p|n).n1 =0 or (p|n).n1 = 1 by TARSKI:def 2;
assume 2*Sum(p|n1) <> n1;
then Sum <%(p|n).n1%> = (p|n).n1 & 2*Sum(p|n1)<n1 by A16,AFINSQ_2:53
,XXREAL_0:1;
then 2*Sum(p|n1) + 2*Sum <%(p|n).n1%> < n1+2 by A17,XREAL_1:8;
hence contradiction by A15;
end;
p.n1=1
proof
Segm n c= Segm len p by A9,NAT_1:39;
then
A18: dom(p|n)=n1+1 by RELAT_1:62;
A19: Sum <%0%>=0 & (p|n)=((p|n)|n1)^<%(p|n).n1%> by A18,AFINSQ_1:56,AFINSQ_2:53
;
assume
A20: p.n1<>1;
A21: n1 <n1+1 by NAT_1:13;
then n1 < len p by A9,XXREAL_0:2;
then
A22: n1 in dom p by AFINSQ_1:86;
Segm n1 c= Segm n by A21,NAT_1:39;
then
A23: (p|n)|n1=p|n1 by RELAT_1:74;
n1 in Segm n by A21,NAT_1:44;
then n1 in dom p/\n by A22,XBOOLE_0:def 4;
then
A24: (p|n).n1=p.n1 by FUNCT_1:48;
A25: n1 <n1+1 by NAT_1:13;
p.n1 in rng p by A22,FUNCT_1:3;
then p.n1=0 by A1,A20,TARSKI:def 2;
then Sum (p|n)=Sum (p|n1) +(0 qua Nat) by A19,A24,A23,AFINSQ_2:55;
hence thesis by A6,A10,A25;
end;
hence thesis by A3,A5,A8,A10,XXREAL_0:2;
end;
theorem Th16:
for p, q, k st p|(2*k+len q) = (k-->0)^q^(k-->1) & q is
dominated_by_0 & 2*Sum q = len q & k > 0 holds min*{N:2*Sum(p|N) = N & N > 0} =
2*k+len q
proof
let p,q,k such that
A1: p|(2*k+len q)=(k-->0)^q^(k-->1) and
A2: q is dominated_by_0 and
A3: 2*Sum q=len q and
A4: k>0;
set k0=k-->0;
A5: Sum k0=k*0 by AFINSQ_2:58;
then
A6: 2*k > 0 by A4,XREAL_1:68;
reconsider k1=k-->1 as XFinSequence of NAT;
set M={N:2*Sum(p|N)=N & N>0};
set kqk=k0^q^k1;
Sum kqk = Sum (k0^q) + Sum k1 by AFINSQ_2:55;
then
A7: Sum kqk = Sum k0+Sum q+Sum k1 by AFINSQ_2:55;
Sum k1=k*1 by AFINSQ_2:58;
then 2*Sum (p|(2*k+len q))=len q+2*k by A1,A3,A7,A5;
then
A8: 2*k+len q in M by A6;
M c= NAT
proof
let y be object;
assume y in M;
then ex i be Nat st i=y & 2*Sum(p|i)=i & i>0;
hence thesis by ORDINAL1:def 12;
end;
then reconsider M as non empty Subset of NAT by A8;
min*M=2*k+len q
proof
kqk = k0^(q^k1) by AFINSQ_1:27;
then
A9: len kqk = len k0+len (q^k1) by AFINSQ_1:17;
A10: len kqk = k+(len q+len k1) by A9,AFINSQ_1:17;
assume
A11: min*M<>2*k+len q;
min*M in M by NAT_1:def 1;
then
A12: ex i be Nat st i=min*M & 2*Sum(p|i)=i & i>0;
A14: 2*k+len q >= min*M by A8,NAT_1:def 1;
then
A15: Segm(min*M) c= Segm(2*k+len q) by NAT_1:39;
then
A16: p|min*M= kqk|min*M by A1,RELAT_1:74;
now
per cases;
suppose
A17: min*M <= k;
k=dom k0 & kqk=k0^(q^k1) by AFINSQ_1:27;
then
A18: kqk|min*M=k0|min*M by A17,AFINSQ_1:58;
A19: Sum (min*M-->0)=min*M * 0 by AFINSQ_2:58;
k0|min*M =min*M-->0 by A17,Lm1;
then Sum (p|min*M)=Sum (min*M-->0) by A1,A15,A18,RELAT_1:74;
hence contradiction by A12,A19;
end;
suppose
min*M > k;
then reconsider mk=min*M-k as Nat by NAT_1:21;
now
per cases;
suppose
A20: min*M <= k+len q;
A21: dom k0 = k;
min*M=mk + k;
then
A22: (k0^q)|min*M=k0^(q|mk) by A21,AFINSQ_1:59;
dom (k0^q)=len k0+len q by AFINSQ_1:def 3;
then kqk|min*M=(k0^q)|min*M by A20,AFINSQ_1:58;
then
A23: Sum(p|min*M)=Sum(k0)+Sum(q|mk) by A16,A22,AFINSQ_2:55;
A24: 1 <= k by A4,NAT_1:14;
Sum(k0)=k*0 by AFINSQ_2:58;
then mk+k <= mk by A2,A12,A23,Th2;
hence contradiction by A24,NAT_1:19;
end;
suppose
min*M > k+len q;
then reconsider mkL=min*M-(k+len q) as Nat by NAT_1:21;
A25: 2*Sum(p|min*M)=min*M by A12;
dom (k0^q)=len k0 + len q & dom k0=k by AFINSQ_1:def 3;
then min*M=dom(k0^q)+mkL;
then kqk|min*M=(k0^q)^(k1|mkL) by AFINSQ_1:59;
then
A26: Sum(p|min*M)=Sum(k0^q)+Sum (k1|mkL) by A16,AFINSQ_2:55;
min*M < len kqk by A11,A10,A14,XXREAL_0:1;
then mkL < 2*k+len q-(k+len q) by A10,XREAL_1:9;
then k1|mkL=mkL-->1 by Lm1;
then
A27: Sum(k1|mkL)=mkL*1 by AFINSQ_2:58;
Sum(k0^q)=Sum(k0)+Sum q & Sum k0=k*0 by AFINSQ_2:55,58;
hence contradiction by A3,A11,A26,A27,A25;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th17:
for p st p is dominated_by_0 & {N: 2*Sum(p|N) = N & N > 0} = {}
& len p > 0 ex q st p = <%0%>^q & q is dominated_by_0
proof
let p such that
A1: p is dominated_by_0 and
A2: {N: 2*Sum(p|N)=N & N>0}={} & len p > 0;
set M={N: 2*Sum(p|N)=N & N>0};
consider q such that
A3: p=p|1^q by Th1;
take q;
A4: rng p c= {0,1} by A1;
rng q c= rng p by A3,AFINSQ_1:25;
then
A5: rng q c= {0,1} by A4;
len p >= 1 by A2,NAT_1:14;
then Segm 1 c= Segm len p by NAT_1:39;
then
A6: dom (p|1)=1 by RELAT_1:62;
A7: p|1=<%(p|1).0%> by A6,AFINSQ_1:34;
0 in Segm 1 by NAT_1:44;
then
A8: (p|1).0=p.0 by A6,FUNCT_1:47;
hence p=<%0%>^q by A1,A3,A7,Th3;
assume q is not dominated_by_0;
then consider i such that
i <= dom q and
A9: 2*Sum(q|i) > i by A5;
reconsider i as Nat;
p|(1+i)=(p|1)^(q|i) by A3,A6,AFINSQ_1:59;
then
A10: Sum (p|(1+i))=Sum <%p.0%>+Sum (q|i) by A7,A8,AFINSQ_2:55;
A11: 2*Sum(q|i) >= i+1 by A9,NAT_1:13;
Sum <%p.0%>=p.0 by AFINSQ_2:53;
then
A12: Sum (p|(1+i))=(0 qua Nat)+Sum (q|i) by A1,A10,Th3;
then 1+i >=2*Sum (q|i) by A1,Th2;
then 1+i =2*Sum (q|i) by A11,XXREAL_0:1;
then 1+i in M by A12;
hence thesis by A2;
end;
theorem Th18:
p is dominated_by_0 implies <%0%>^p is dominated_by_0 &
{N: 2*Sum((<%0%>^p)|N) = N & N > 0} = {}
proof
reconsider q=1-->0 as XFinSequence of NAT;
assume
A1: p is dominated_by_0;
dom q = 1 & len q = dom q;
then
A2: q = <%q.0%> by AFINSQ_1:34;
q is dominated_by_0 by Lm2;
then q is dominated_by_0 & q.0 = 0;
hence <%0%>^p is dominated_by_0 by A1,A2,Th7;
set M={N: 2*Sum((<%0%>^p)|N)=N & N>0};
assume M<>{};
then consider x being object such that
A3: x in M by XBOOLE_0:def 1;
consider i be Nat such that
x=i and
A4: 2*Sum((<%0%>^p)|i)=i and
A5: i>0 by A3;
reconsider i1=i-1 as Nat by A5,NAT_1:20;
dom <%0%>=1 by AFINSQ_1:33;
then i=dom <%0%> +i1;
then (<%0%>^p)|i=<%0%>^(p|i1) by AFINSQ_1:59;
then
A6: Sum ((<%0%>^p)|i)=Sum <%0%>+ Sum (p|i1) by AFINSQ_2:55;
Sum <%0%>=0 & i1<i1+1 by AFINSQ_2:53,NAT_1:13;
hence thesis by A1,A4,A6,Th2;
end;
theorem
rng p c= {0,1} & 2*k+1 = min*{N:2*Sum(p|N) > N} implies p|(2*k) is
dominated_by_0
proof
set M={N : 2*Sum(p|N) > N};
set q=p|(2*k);
assume that
A1: rng p c= {0,1} and
A2: 2 * k + 1 = min*M;
thus rng q c= {0,1} by A1;
reconsider M as non empty Subset of NAT by A2,NAT_1:def 1;
let m;
assume
A3: m <= dom q;
then
A4: Segm m c= Segm len q by NAT_1:39;
len q <= 2*k by AFINSQ_1:55;
then Segm len q c= Segm(2*k) by NAT_1:39;
then Segm m c= Segm(2*k) by A4;
then m<=2*k by NAT_1:39;
then
A5: m < 2*k+1 by NAT_1:13;
assume
A6: 2*Sum(q|m) > m;
reconsider m as Element of NAT by ORDINAL1:def 12;
q|m=p|m & m in NAT by A4,RELAT_1:74,XBOOLE_1:1,A3;
then m in M by A6;
hence thesis by A2,A5,NAT_1:def 1;
end;
begin
definition
let n,m be Nat;
func Domin_0(n,m) -> Subset of {0,1}^omega means
:Def2:
x in it iff ex p be
XFinSequence of NAT st p = x & p is dominated_by_0 & dom p = n & Sum p = m;
existence
proof
defpred Q[object] means
ex p st p=$1 & p is dominated_by_0 & dom p = n & Sum
p=m;
consider X such that
A1: for x being object holds x in X iff x in bool [:NAT,NAT:] & Q[x]
from XBOOLE_0:sch 1;
X c= {0,1}^omega
proof
let x be object;
assume x in X;
then consider p such that
A2: p=x and
A3: p is dominated_by_0 and
dom p = n and
Sum p=m by A1;
rng p c= {0,1} by A3;
then p is XFinSequence of {0,1} by RELAT_1:def 19;
hence thesis by A2,AFINSQ_1:42;
end;
then reconsider X as Subset of {0,1}^omega;
take X;
let x;
thus x in X implies Q[x] by A1;
given p such that
A4: p=x & p is dominated_by_0 & dom p = n & Sum p=m;
p c= [:dom p,rng p:] & [:dom p,rng p:] c= [:NAT,NAT:] by RELAT_1:7
,ZFMISC_1:96;
then p c= [:NAT,NAT:];
hence thesis by A1,A4;
end;
uniqueness
proof
let X1,X2 be Subset of {0,1}^omega such that
A5: x in X1 iff ex p st p=x & p is dominated_by_0 & dom p = n &Sum p= m and
A6: x in X2 iff ex p st p=x & p is dominated_by_0 & dom p = n & Sum p =m;
for x being object holds x in X1 iff x in X2
proof let x be object;
x in X1 iff ex p st p=x & p is dominated_by_0&dom p=n&Sum p=m by A5;
hence thesis by A6;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th20:
p in Domin_0(n,m) iff p is dominated_by_0 & dom p = n & Sum p = m
proof
thus p in Domin_0(n,m) implies p is dominated_by_0 & dom p=n & Sum p=m
proof
assume p in Domin_0(n,m);
then ex q st q=p & q is dominated_by_0 & dom q = n & Sum q = m by Def2;
hence thesis;
end;
thus thesis by Def2;
end;
theorem Th21:
Domin_0(n,m) c= Choose(n,m,1,0)
proof
let x be object;
assume x in Domin_0(n,m);
then consider p such that
A1: p = x and
A2: p is dominated_by_0 and
A3: dom p = n & Sum p = m by Def2;
rng p c= {0,1} by A2;
hence thesis by A1,A3,CARD_FIN:40;
end;
registration
let n,m;
cluster Domin_0(n,m) -> finite;
coherence
proof
Domin_0(n,m) c= Choose(n,m,1,0) by Th21;
hence thesis;
end;
end;
theorem Th22:
Domin_0(n,m) is empty iff 2*m > n
proof
thus Domin_0(n,m) is empty implies 2 * m > n
proof
set q=m-->1;
assume
A1: Domin_0(n,m) is empty;
assume
A2: 2*m <= n;
m<=m+m by NAT_1:12;
then reconsider nm=n-m as Nat by A2,NAT_1:21,XXREAL_0:2;
set p=nm-->0;
2*m-m <= nm by A2,XREAL_1:9;
then
A3: p^q is dominated_by_0 by Th5;
dom (p^q)=len p+len q & dom p=nm by AFINSQ_1:def 3;
then
A4: dom (p^q)=nm+m;
A5: Sum (p^q)=Sum p+ Sum q by AFINSQ_2:55;
Sum p=0*nm & Sum q =1*m by AFINSQ_2:58;
hence thesis by A1,A5,A4,A3,Def2;
end;
assume
A6: 2 * m > n;
assume Domin_0(n,m) is non empty;
then consider x being object such that
A7: x in Domin_0(n,m);
consider p such that
p = x and
A8: p is dominated_by_0 and
A9: dom p = n and
A10: Sum p = m by A7,Def2;
p|n=p by A9;
hence thesis by A6,A8,A10,Th2;
end;
theorem Th23:
Domin_0(n,0) = {n-->0}
proof
set p=n-->0;
A1: Domin_0(n,0) c= {p}
proof
let x be object;
assume x in Domin_0(n,0);
then consider q such that
A2: x=q and
q is dominated_by_0 and
A3: dom q = n and
A4: Sum q =0 by Def2;
len q=n & q is nonnegative-yielding by A3;
then q = n --> 0 or (q={} & n=0) by A4,AFINSQ_2:62;
then q= n-->0;
hence thesis by A2,TARSKI:def 1;
end;
{p} c= Domin_0(n,0)
proof
A5: p is dominated_by_0 by Lm2;
dom p=n & Sum p=n*0 by AFINSQ_2:58;
then
A6: p in Domin_0(n,0) by A5,Def2;
let x be object;
assume x in {p};
hence thesis by A6,TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem Th24:
card Domin_0(n,0) = 1
proof
Domin_0(n,0)={n-->0} by Th23;
hence thesis by CARD_1:30;
end;
theorem Th25:
for p,n st rng p c= {0,n} ex q st len p = len q & rng q c= {0,n}
& (for k st k <= len p holds Sum (p|k)+Sum (q|k) = n*k) & for k st k in len p
holds q.k = n-p.k
proof
let p,n such that
A1: rng p c= {0,n};
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
defpred P[set,set] means for k st k=$1 holds $2=n-p.k;
A2: for k st k in Segm len p ex x be Element of {0,n} st P[k,x]
proof
let k;
assume k in Segm len p;
then p.k in rng p by FUNCT_1:3;
then p.k=0 or p.k=n by A1,TARSKI:def 2;
then
A3: n-p.k in {0,n} by TARSKI:def 2;
P[k,n-p.k];
hence thesis by A3;
end;
consider q be XFinSequence of {0,n} such that
A4: dom q= Segm len p& for k st k in Segm len p holds P[k,q.k]
from STIRL2_1:sch 5(A2);
reconsider q as XFinSequence of NAT;
defpred Q[Nat] means $1 <= len p implies Sum (p|$1)+ Sum (q|$1)=n*$1;
A5: for k st Q[k] holds Q[k+1]
proof
let k such that
A6: Q[k];
set k1=k+1;
A7: k<k+1 by NAT_1:13;
then
A8: Segm k c= Segm(k+1) by NAT_1:39;
then
A9: (p|k1)|k=p|k by RELAT_1:74;
A10: (q|k1)|k=q|k by A8,RELAT_1:74;
assume
A11: k+1 <= len p;
then
A12: Segm k1 c= Segm len p by NAT_1:39;
then
A13: len (q|k1)=k1 by A4,RELAT_1:62;
then
A14: (q|k1)=((q|k1)|k)^<%(q|k1).k%> by AFINSQ_1:56;
len (p|k1)=k1 by A12,RELAT_1:62;
then
A15: k in dom (p|k1) by A7,AFINSQ_1:86;
then
A16: (p|k1).k= p.k by FUNCT_1:47;
len (p|k1)=k1 by A12,RELAT_1:62;
then (p|k1)=((p|k1)|k)^<%(p|k1).k%> by AFINSQ_1:56;
then Sum (p|k1)=Sum (p|k)+Sum <%p.k%> by A16,A9,AFINSQ_2:55;
then
A17: Sum (p|k1)=Sum (p|k)+p.k by AFINSQ_2:53;
k< len p by A11,NAT_1:13;
then k in len p by AFINSQ_1:86;
then
A18: q.k=n-p.k by A4;
(q|k1).k= q.k by A13,A15,FUNCT_1:47;
then Sum (q|k1)=Sum (q|k)+Sum <%q.k%> by A14,A10,AFINSQ_2:55;
then Sum (q|k1)=Sum (q|k)+ (n-p.k) by A18,AFINSQ_2:53;
hence thesis by A6,A11,A17,NAT_1:13;
end;
take q;
thus len p=len q by A4;
thus rng q c= {0,n} by RELAT_1:def 19;
A19: Q[0];
for k holds Q[k] from NAT_1:sch 2(A19,A5);
hence thesis by A4;
end;
theorem Th26:
m <= n implies n choose m > 0
proof
assume
A1: m<=n;
then reconsider nm=n-m as Nat by NAT_1:21;
A2: (m!)*(nm!)>(m!)*0 by XREAL_1:68;
n!>0*((m!)*(nm!));
then (n!)/((m!)*(nm!))>0 by A2,XREAL_1:81;
hence thesis by A1,NEWTON:def 3;
end;
theorem Th27:
2*(m+1) <= n implies card (Choose(n,m+1,1,0) \ Domin_0(n,m+1)) =
card Choose(n,m,1,0)
proof
defpred P[object,object] means
for p,k st $1 = p & 2 * k + 1= min*{N:2*Sum (p|N)>N
} ex r1,r2 be XFinSequence of NAT st $2=r1^r2 & len r1=2*k+1 & len r1=len (p|(2
*k+1)) & p=(p|(2*k+1))^r2 & (for o be Nat st o < 2*k+1 holds r1.o=1-p.o);
assume
A1: 2 * (m+1) <= n;
A2: m <= m+m by XREAL_1:31;
m<=m+1 by NAT_1:13;
then 2*m <= 2*(m+1) by XREAL_1:64;
then 2*m <= n by A1,XXREAL_0:2;
then m<= n by A2,XXREAL_0:2;
then (card n) choose m>0 by Th26;
then reconsider W=Choose(n,m,1,0) as non empty finite set by CARD_1:27
,CARD_FIN:16;
set Z=Domin_0(n,m+1);
set CH=Choose(n,m+1,1,0);
A3: for x being object st x in CH\Z ex y being object st y in W & P[x,y]
proof
let x being object such that
A4: x in CH\Z;
x in CH by A4,XBOOLE_0:def 5;
then consider p be XFinSequence of NAT such that
A5: p = x and
A6: dom p = n and
A7: rng p c= {0,1} and
A8: Sum p=m+1 by CARD_FIN:40;
not p in Z by A4,A5,XBOOLE_0:def 5;
then p is not dominated_by_0 by A6,A8,Def2;
then consider o be Nat such that
A9: 2 * o + 1 = min*{N : 2*Sum(p|N) > N} & 2 * o + 1 <= dom p & o =
Sum (p|(2*o)) & p.(2*o) = 1 by A7,Th15;
set q=p|(2*o+1);
consider r2 be XFinSequence of NAT such that
A10: p=q^r2 by Th1;
rng q c= {0,1} by A7;
then consider r1 be XFinSequence of NAT such that
A11: len q=len r1 and
A12: rng r1 c= {0,1} and
A13: for i st i <=len q holds Sum (q|i)+ Sum (r1|i)= 1*i and
A14: for i st i in len q holds r1.i=1-q.i by Th25;
take R=r1^r2;
len p=len r1+len r2 by A11,A10,AFINSQ_1:17;
then
A15: dom R=n by A6,AFINSQ_1:def 3;
rng r2 c= rng p by A10,AFINSQ_1:25;
then rng r2 c= {0,1} by A7;
then rng r1 \/ rng r2 c= {0,1} by A12,XBOOLE_1:8;
then
A16: rng R c= {0,1} by AFINSQ_1:26;
q|dom q=q & r1|dom r1=r1;
then
A17: Sum q+Sum r1=1*len q by A11,A13;
A18: 2*o <2*o+1 by NAT_1:13;
then Segm(2*o) c= Segm(2*o+1) by NAT_1:39;
then
A19: q|(2*o)=p|(2*o) by RELAT_1:74;
A20: Segm(2*o+1) c= Segm len p by A9,NAT_1:39;
then
A21: dom q=2*o+1 by RELAT_1:62;
A22: len q=2*o+1 by A20,RELAT_1:62;
then
A23: q=(q|(2*o))^<%q.(2*o)%> by AFINSQ_1:56;
2*o in Segm(2*o+1) by A18,NAT_1:44;
then q.(2*o)=p.(2*o) by A22,FUNCT_1:47;
then Sum q=Sum (p|(2*o))+Sum <%p.(2*o)%> by A23,A19,AFINSQ_2:55;
then
A24: Sum q = o+1 by A9,AFINSQ_2:53;
m+1= Sum q + Sum r2 by A8,A10,AFINSQ_2:55;
then Sum r1+Sum r2=m+1-(2*o+1)+2*o by A17,A21,A24;
then Sum (r1^r2)=m by AFINSQ_2:55;
hence R in W by A15,A16,CARD_FIN:40;
thus P[x,R]
proof
let p9 be XFinSequence of NAT, k such that
A25: x=p9 & 2 * k + 1= min*{N:2*Sum (p9|N)>N};
set q9=p9|(2*k+1);
take r1,r2;
thus R=r1^r2 &len r1=2*k+1 & len r1=len q9 &p9=q9^r2 by A5,A9,A11,A10
,A20,A25,RELAT_1:62;
thus for i be Nat st i < 2*k+1 holds r1.i=1-p9.i
proof
let i be Nat;
assume i <2*k+1;
then
A26: i in len q by A5,A9,A21,A25,AFINSQ_1:86;
then r1.i=1-q.i by A14;
hence thesis by A5,A25,A26,FUNCT_1:47;
end;
end;
end;
consider F be Function of CH\Z,W such that
A27: for x being object st x in CH\Z holds P[x,F.x] from FUNCT_2:sch 1(A3);
W c= rng F
proof
let x be object;
assume x in W;
then consider p such that
A28: p = x and
A29: dom p = n and
A30: rng p c= {0,1} and
A31: Sum p=m by CARD_FIN:40;
set M={N:2*Sum (p|N)<N};
m<m+1 by NAT_1:13;
then 2*m < 2*(m+1) by XREAL_1:68;
then 2*m < n by A1,XXREAL_0:2;
then 2*Sum (p|n)<n & n in NAT by A29,A31,ORDINAL1:def 12;
then
A32: n in M;
M c= NAT
proof
let y be object;
assume y in M;
then ex i be Nat st i=y & 2*Sum(p|i)<i;
hence thesis by ORDINAL1:def 12;
end;
then reconsider M as non empty Subset of NAT by A32;
ex k st 2*k+1 = min*M & Sum (p|(2*k+1))=k & 2*k+1 <= dom p
proof
set mm=min*M;
mm in M by NAT_1:def 1;
then
A33: ex o be Nat st mm=o & 2*Sum(p|o)<o;
then reconsider m1=mm-1 as Nat by NAT_1:20;
A34: 2*Sum(p|mm)<m1+1 by A33;
A35: m1<m1+1 by NAT_1:13;
then Segm m1 c= Segm mm by NAT_1:39;
then
A36: (p|mm)|m1=p|m1 by RELAT_1:74;
mm <= dom p by A29,A32,NAT_1:def 1;
then
A37: Segm mm c= Segm len p by NAT_1:39;
then dom(p|mm)=mm by RELAT_1:62;
then m1 in Segm dom (p|mm) by A35,NAT_1:44;
then
A38: (p|mm).m1=p.m1 by FUNCT_1:47;
m1 < m1+1 by NAT_1:13;
then not m1 in M by NAT_1:def 1;
then 2*Sum(p|m1)>=m1;
then
A39: Sum<%p.m1%>=p.m1 & 2*Sum(p|m1)+2*p.m1 >=
m1+(0 qua Nat) by AFINSQ_2:53,XREAL_1:7;
reconsider S=Sum(p|mm) as Nat;
take S;
A40: mm <= dom p by A29,A32,NAT_1:def 1;
len(p|mm)=m1+1 by A37,RELAT_1:62;
then p|mm=(p|mm)|m1 ^ <%(p|mm).m1%> by AFINSQ_1:56;
then Sum(p|mm)=Sum(p|m1)+Sum<%p.m1%> by A38,A36,AFINSQ_2:55;
hence thesis by A40,A39,A34,NAT_1:9;
end;
then consider k such that
A41: 2 * k + 1 = min*M and
A42: Sum (p|(2*k+1))=k and
A43: 2 * k + 1 <= dom p;
set k1=2*k+1;
consider q such that
A44: p=p|k1^q by Th1;
rng (p|k1) c= {0,1} by A30;
then consider r be XFinSequence of NAT such that
A45: len r=len (p|k1) and
A46: rng r c= {0,1} and
A47: for i st i <= len (p|k1) holds Sum ((p|k1)|i)+Sum(r|i)=1*i and
A48: for i st i in len (p|k1) holds r.i=1-(p|k1).i by Th25;
set rq=r^q;
A49: dom rq=len(p|k1)+len q by A45,AFINSQ_1:def 3;
A50: m=k+Sum q by A31,A42,A44,AFINSQ_2:55;
dom rq=len (p|k1)+len q by A45,AFINSQ_1:def 3;
then
A51: dom rq=dom p by A44,AFINSQ_1:def 3;
(p|k1)|dom (p|k1)=(p|k1) & r|dom r=r;
then
A52: Sum (p|k1)+Sum r=1*len (p|k1) by A45,A47;
rng q c= rng p by A44,AFINSQ_1:25;
then rng q c= {0,1} by A30;
then rng r\/rng q c= {0,1} by A46,XBOOLE_1:8;
then
A53: rng rq c= {0,1} by AFINSQ_1:26;
A54: Segm k1 c= Segm len p by A43,NAT_1:39;
then
A55: len (p|k1)=k1 by RELAT_1:62;
then
A56: (r^q)|k1=r by A45,AFINSQ_1:57;
A57: k1+1> k1 by NAT_1:13;
then
A58: k1 < 2*Sum r by A42,A52,A55;
A59: 2* Sum r > k1 by A42,A52,A55,A57;
then consider j be Nat such that
A60: 2 * j + 1 = min*{N : 2*Sum(rq|N) > N} & 2*j+1<=dom rq & j = Sum
(rq|(2*j)) & rq.(2*j)=1 by A53,A56,Th2,Th15;
set j1=2*j+1;
A61: len (p|k1^q)=len (p|k1)+ len q by AFINSQ_1:def 3;
rq is not dominated_by_0 by A59,A56,Th2;
then
A62: not rq in Z by Th20;
set rqj=rq|(2*j+1);
Sum rq=Sum r+ Sum q by AFINSQ_2:55;
then rq in CH by A29,A42,A52,A55,A51,A53,A50,CARD_FIN:40;
then
A63: rq in CH\Z by A62,XBOOLE_0:def 5;
then consider r1,r2 be XFinSequence of NAT such that
A64: F.rq=r1^r2 and
A65: len r1=j1 and
A66: len r1=len rqj & rq=rqj^r2 and
A67: for i be Nat st i < j1 holds r1.i=1-rq.i by A27,A60;
A68: dom rq=len r1+len r2 by A66,AFINSQ_1:def 3;
then
A69: len (r1^r2)=len (p|k1^q) by A49,A61,AFINSQ_1:17;
reconsider K={N : 2*Sum(rq|N) > N} as non empty Subset of NAT by A60,
NAT_1:def 1;
rq|k1=r by A45,A55,AFINSQ_1:57;
then k1 in K by A58;
then
A70: k1>=j1 by A60,NAT_1:def 1;
then Segm j1 c= Segm k1 by NAT_1:39;
then
A71: (p|k1)|j1=p|j1 by RELAT_1:74;
j1 in K by A60,NAT_1:def 1;
then
A72: ex N st N=j1 & 2*Sum(rq|N) > N;
Sum ((p|k1)|j1)+Sum(r|j1)=j1*1 by A47,A55,A70;
then 2*Sum(r|j1)=2*j1-2*Sum (p|j1) by A71;
then j1+(j1-2*Sum (p|j1))>2*Sum (p|j1)+(j1-2*Sum (p|j1)) by A45,A55,A70,A72
,AFINSQ_1:58;
then j1>2*Sum (p|j1) by XREAL_1:6;
then j1 in M;
then j1 >= k1 by A41,NAT_1:def 1;
then
A73: j1=k1 by A70,XXREAL_0:1;
A74: len (p|k1^q)=len rq by A49,AFINSQ_1:def 3;
now
let i be Nat such that
A75: i < len (r1^r2);
now
per cases;
suppose
A76: i < len r1;
then
A77: i in dom r1 & r1.i=1-rq.i by A65,A67,AFINSQ_1:86;
A78: i in len r1 by A76,AFINSQ_1:86;
A79: len r1=len (p|k1) & i in NAT
by A54,A65,A73,ORDINAL1:def 12,RELAT_1:62;
then
A80: r.i=1-(p|k1).i by A48,A78;
(p|k1^q).i=(p|k1).i & rq.i=r.i by A45,A78,A79,AFINSQ_1:def 3;
hence (r1^r2).i=(p|k1^q).i by A80,A77,AFINSQ_1:def 3;
end;
suppose
A81: i>= len r1;
then
A82: (p|k1^q).i=q.(i-len r) by A45,A55,A65,A73,A69,A75,AFINSQ_1:19;
(r1^r2).i=r2.(i-len r1) & rq.i=q.(i-len r) by A45,A55,A65,A73,A69,A74
,A75,A81,AFINSQ_1:19;
hence (r1^r2).i=(p|k1^q).i by A66,A69,A74,A75,A81,A82,AFINSQ_1:19;
end;
end;
hence (r1^r2).i=(p|k1^q).i;
end;
then
A83: r1^r2=p|k1^q by A68,A49,A61,AFINSQ_1:9,17;
rq in dom F by A63,FUNCT_2:def 1;
hence thesis by A28,A44,A64,A83,FUNCT_1:3;
end;
then
A84: rng F = W;
A85: F is one-to-one
proof
let x,y being object such that
A86: x in dom F and
A87: y in dom F and
A88: F.x=F.y;
x in CH by A86,XBOOLE_0:def 5;
then consider p such that
A89: p = x and
A90: dom p = n and
A91: rng p c= {0,1} and
A92: Sum p=m+1 by CARD_FIN:40;
not p in Z by A86,A89,XBOOLE_0:def 5;
then p is not dominated_by_0 by A90,A92,Def2;
then consider k1 be Nat such that
A93: 2 * k1 + 1 = min*{N : 2*Sum(p|N) > N} & 2*k1+1<=dom p & k1 = Sum
(p|(2*k1)) & p.(2*k1)=1 by A91,Th15;
y in CH by A87,XBOOLE_0:def 5;
then consider q such that
A94: q = y and
A95: dom q = n and
A96: rng q c= {0,1} and
A97: Sum q=m+1 by CARD_FIN:40;
not q in Z by A87,A94,XBOOLE_0:def 5;
then q is not dominated_by_0 by A95,A97,Def2;
then consider k2 be Nat such that
A98: 2 * k2 + 1 = min*{N : 2*Sum(q|N) > N} & 2*k2+1<=dom q & k2 = Sum
(q|(2*k2)) & q.(2*k2)=1 by A96,Th15;
A99: len q=n by A95;
reconsider M={N : 2*Sum(q|N) > N} as non empty Subset of NAT by A98,
NAT_1:def 1;
set qk=q|(2*k2+1);
consider s1,s2 be XFinSequence of NAT such that
A100: F.y=s1^s2 and
A101: len s1=2*k2+1 and
A102: len s1=len qk and
A103: q=qk^s2 and
A104: for i be Nat st i < 2*k2+1 holds s1.i=1-q.i by A27,A87,A94,A98;
A105: len q= len qk + len s2 by A103,AFINSQ_1:17;
then
A106: len q=len (s1^s2) by A102,AFINSQ_1:17;
reconsider K={N : 2*Sum(p|N) > N} as non empty Subset of NAT by A93,
NAT_1:def 1;
set pk=p|(2*k1+1);
consider r1,r2 be XFinSequence of NAT such that
A107: F.x=r1^r2 and
A108: len r1=2*k1+1 and
A109: len r1=len (p|(2*k1+1)) and
A110: p=(p|(2*k1+1))^r2 and
A111: for i be Nat st i < 2*k1+1 holds r1.i=1-p.i by A27,A86,A89,A93;
assume x<>y;
then consider i be Nat such that
A112: i < len p and
A113: p.i<>q.i by A89,A90,A94,A95,AFINSQ_1:9;
A114: len p=len pk+ len r2 by A110,AFINSQ_1:17;
then
A115: len p=len (r1^r2) by A109,AFINSQ_1:17;
now
per cases by XXREAL_0:1;
suppose
A116: k1=k2;
now
per cases;
suppose
A117: i< len pk;
then i in len pk by AFINSQ_1:86;
then
A118: r1.i=(r1^r2).i & s1.i=(s1^s2).i by A108,A109,A101,A116,
AFINSQ_1:def 3;
r1.i=1-p.i & s1.i=1-q.i by A108,A109,A111,A104,A116,A117;
hence contradiction by A88,A107,A100,A113,A118;
end;
suppose
A119: i>=len pk;
then
A120: (s1^s2).i=s2.(i-len pk) by A90,A108,A109,A95,A101,A106,A112,A116,
AFINSQ_1:19;
p.i=r2.(i-len pk) & q.i=s2.(i-len pk) by A90,A108,A109,A110,A101
,A102,A103,A99,A112,A116,A119,AFINSQ_1:19;
hence contradiction by A88,A107,A109,A100,A115,A112,A113,A119,A120,
AFINSQ_1:19;
end;
end;
hence contradiction;
end;
suppose
A121: k1>k2;
len s1 <= len p by A90,A95,A102,A105,NAT_1:11;
then
A122: Segm len s1 c= Segm len p by NAT_1:39;
2*k2<2*k1 by A121,XREAL_1:68;
then
A123: len s1 < len r1 by A108,A101,XREAL_1:6;
then (s1^s2)|(len s1)=r1|(len s1) by A88,A107,A100,AFINSQ_1:58;
then
A124: s1=r1|(len s1) by AFINSQ_1:57;
A125: for k be Nat st k < len qk holds qk.k=(p|len qk).k
proof
let k be Nat such that
A126: k<len qk;
A127: k in len s1 by A102,A126,AFINSQ_1:86;
then
A128: k in dom q/\len s1 by A90,A95,A122,XBOOLE_0:def 4;
k in dom p/\ len s1 by A122,A127,XBOOLE_0:def 4;
then
A129: p.k=(p|len qk).k by A102,FUNCT_1:48;
A130: k<len r1 by A102,A123,A126,XXREAL_0:2;
then
A131: r1.k=1-p.k by A108,A111;
k in dom r1 by A130,AFINSQ_1:86;
then k in dom r1/\ len s1 by A127,XBOOLE_0:def 4;
then
A132: r1.k=(r1|len s1).k by FUNCT_1:48;
s1.k=1-q.k by A101,A102,A104,A126;
hence thesis by A101,A124,A131,A132,A128,A129,FUNCT_1:48;
end;
2*k2+1 in M by A98,NAT_1:def 1;
then
A133: ex N st 2*k2+1=N & 2* Sum(q|N)>N;
len qk= len (p|len qk) by A102,A122,RELAT_1:62;
then qk=p|len qk by A125,AFINSQ_1:9;
then len qk in K by A101,A102,A133;
hence contradiction by A93,A108,A102,A123,NAT_1:def 1;
end;
suppose
A134: k1<k2;
len r1 <= len q by A90,A109,A95,A114,NAT_1:11;
then
A135: Segm len r1 c= Segm len q by NAT_1:39;
2*k1<2*k2 by A134,XREAL_1:68;
then
A136: len r1 < len s1 by A108,A101,XREAL_1:6;
then (r1^r2)|(len r1)=s1|(len r1) by A88,A107,A100,AFINSQ_1:58;
then
A137: r1=s1|(len r1) by AFINSQ_1:57;
A138: for k be Nat st k < len pk holds pk.k=(q|len pk).k
proof
let k be Nat such that
A139: k<len pk;
A140: k in len r1 by A109,A139,AFINSQ_1:86;
then
A141: k in dom p/\len r1 by A90,A95,A135,XBOOLE_0:def 4;
k in dom q/\ len r1 by A135,A140,XBOOLE_0:def 4;
then
A142: q.k=(q|len pk).k by A109,FUNCT_1:48;
A143: k<len s1 by A109,A136,A139,XXREAL_0:2;
then
A144: s1.k=1-q.k by A101,A104;
k in dom s1 by A143,AFINSQ_1:86;
then k in dom s1/\ len r1 by A140,XBOOLE_0:def 4;
then
A145: s1.k=(s1|len r1).k by FUNCT_1:48;
r1.k=1-p.k by A108,A109,A111,A139;
hence thesis by A108,A137,A144,A145,A141,A142,FUNCT_1:48;
end;
2*k1+1 in K by A93,NAT_1:def 1;
then
A146: ex N st 2*k1+1=N & 2* Sum(p|N)>N;
len pk= len (q|len pk) by A109,A135,RELAT_1:62;
then pk=q|len pk by A138,AFINSQ_1:9;
then len pk in M by A108,A109,A146;
hence contradiction by A109,A98,A101,A136,NAT_1:def 1;
end;
end;
hence contradiction;
end;
dom F=CH\Z by FUNCT_2:def 1;
then (CH\Z),W are_equipotent by A85,A84,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem Th28:
2*(m+1) <= n implies card Domin_0(n,m+1) = (n choose (m+1)) - (n choose m)
proof
set CH=Choose(n,m+1,1,0);
set Z=Domin_0(n,m+1);
set W=Choose(n,m,1,0);
A1: card CH = (card n) choose (m+1) & card n=n by CARD_FIN:16;
card (CH \ Z) = card CH - card Z by Th21,CARD_2:44;
then
A2: card Z=card CH - card (CH \ Z);
assume 2 * (m+1) <= n;
then card Z=card CH-card W by A2,Th27;
hence thesis by A1,CARD_FIN:16;
end;
theorem Th29:
2*m <= n implies card Domin_0(n,m) = (n+1-2*m) / (n+1-m) * (n choose m)
proof
assume
A1: 2*m<=n;
now
per cases;
suppose
A2: m=0;
then (n choose m)=1 by NEWTON:19;
then (n+1-2*m)/(n+1-m)*(n choose m)=1 by A2,XCMPLX_1:60;
hence thesis by A2,Th24;
end;
suppose
A3: m>0;
A4: m<=m+m by NAT_1:11;
then reconsider nm=n-m as Nat by A1,NAT_1:21,XXREAL_0:2;
reconsider m1=m-1 as Nat by A3,NAT_1:20;
set n9=n!;
set m9=m!;
set nm19=(nm+1)!;
set nm9=nm!;
m<=n by A1,A4,XXREAL_0:2;
then
A5: n choose m=n9/(m9*nm9) by NEWTON:def 3;
A6: 2*(m1+1)<=n by A1;
set m19=m1!;
A7: 1/(m19*nm19)=((m1+1)*1)/((m19*nm19)*(m1+1)) by XCMPLX_1:91
.=m/(nm19*(m19*(m1+1)))
.=m/(nm19*((m1+1)!)) by NEWTON:15
.=-(-m)/(nm19*m9) by XCMPLX_1:190;
1/(m9*nm9)=((nm+1)*1)/((m9*nm9)*(nm+1)) by XCMPLX_1:91
.=(nm+1)/(m9*(nm9*(nm+1)))
.=(nm+1)/(m9*nm19) by NEWTON:15;
then
A8: 1/(m9*nm9)-1/(m19*nm19)=(nm+1)/(m9*nm19)+(-m)/(m9*nm19) by A7
.=((nm+1)+(-m))/(m9*nm19) by XCMPLX_1:62
.=(n+1-2*m)/(m9*(nm9*(nm+1))) by NEWTON:15
.=(1*(n+1-2*m))/((m9*nm9)*(nm+1))
.=(1/(m9*nm9))*((n+1-2*m)/(nm+1)) by XCMPLX_1:76;
m1<=m1+(1+m1+1) by NAT_1:11;
then
A9: m1 <= n by A1,XXREAL_0:2;
n-m1=nm+1;
then
A10: n choose m1=n9/(m19*nm19) by A9,NEWTON:def 3;
n9/(m9*nm9)-n9/(m19*nm19)=n9*(1/(m9*nm9))-n9/(m19*nm19) by XCMPLX_1:99
.=n9*(1/(m9*nm9))-n9*(1/(m19*nm19)) by XCMPLX_1:99
.=n9*(1/(m9*nm9)-1/(m19*nm19))
.=n9*((1/(m9*nm9))*((n+1-2*m)/(nm+1))) by A8
.=(n9*(1/(m9*nm9)))*((n+1-2*m)/(nm+1))
.=((n9*1)/(m9*nm9))*((n+1-2*m)/(nm+1)) by XCMPLX_1:74;
hence thesis by A5,A10,A6,Th28;
end;
end;
hence thesis;
end;
theorem Th30:
card Domin_0(2+k,1) = k+1
proof
card Domin_0(2+k,1)=(2+k+1-2*1)/(2+k+1-1)*((2+k) choose 1) by Th29,NAT_1:11
.=(k+1)/(2+k)*(2+k) by STIRL2_1:51
.=k+1 by XCMPLX_1:87;
hence thesis;
end;
theorem
card Domin_0(4+k,2) = (k+1)*(k+4)/2
proof
card Domin_0(4+k,2)=(4+k+1-2*2)/(4+k+1-2)*((4+k) choose 2) by Th29,NAT_1:11
.=(k+1)/(k+3)*((4+k)*(4+k-1)/2) by STIRL2_1:51
.=((k+1)/(k+3)*(3+k))*(4+k)/2
.=(k+1)*(4+k)/2 by XCMPLX_1:87;
hence thesis;
end;
theorem
card Domin_0(6+k,3) = (k+1)*(k+5)*(k+6)/6
proof
card Domin_0(6+k,3)=(6+k+1-2*3)/(6+k+1-3)*((6+k) choose 3) by Th29,NAT_1:11
.=(k+1)/(k+4)*((6+k)*(6+k-1)*(6+k-2)/6) by STIRL2_1:51
.=((k+1)/(k+4)*(4+k))*(5+k)*(6+k)/6
.=(k+1)*(5+k)*(6+k)/6 by XCMPLX_1:87;
hence thesis;
end;
theorem Th33:
card Domin_0(2*n,n) = ((2*n) choose n) / (n+1)
proof
card Domin_0(2*n,n) = (2*n+1-2*n)/(2*n+1-n)*((2*n) choose n) by Th29
.=(1*((2*n) choose n))/(n+1) by XCMPLX_1:74;
hence thesis;
end;
theorem Th34:
card Domin_0(2*n,n) = Catalan(n+1)
proof
A1: Catalan(n+1)=((2*(n+1) -' 2) choose ((n+1) -' 1))/(n+1) by CATALAN1:def 1;
2*n+2 -' 2=2*n+2-2 & n+1 -'1 =n+1-1 by XREAL_0:def 2;
hence thesis by A1,Th33;
end;
definition
let D;
mode OMEGA of D -> functional non empty set means
:Def3:
for x st x in it holds x is XFinSequence of D;
existence
proof
reconsider D9OMEGA=D^omega as functional non empty set;
take D9OMEGA;
thus thesis by AFINSQ_1:def 7;
end;
end;
definition
let D;
redefine func D^omega -> OMEGA of D; :: redefines ^omega (AFINSQ_1, definition)
coherence
proof
D^omega is functional & for x st x in D^omega holds x is XFinSequence
of D by AFINSQ_1:def 7;
hence thesis by Def3;
end;
end;
registration
let D;
let F be OMEGA of D;
cluster -> finite D-valued Sequence-like for Element of F;
coherence by Def3;
end;
reserve pN, qN for Element of NAT^omega;
theorem
card {pN:dom pN = 2*n & pN is dominated_by_0} = (2*n) choose n
proof
set D=bool ({0,1}^omega);
set 2n=2*n;
defpred P[set,set] means for i st i=$1 holds $2=Domin_0(2n,i);
set Z={pN:dom pN = 2* n & pN is dominated_by_0};
A1: for k st k in Segm(n+1) ex x be Element of D st P[k,x]
proof
let k such that
k in Segm(n+1);
reconsider Z=Domin_0(2n,k) as Element of D;
take Z;
thus thesis;
end;
consider r be XFinSequence of D such that
A2: dom r= Segm(n+1) & for k st k in Segm(n+1) holds P[k,r.k]
from STIRL2_1:sch 5(A1);
A3: Z c= union rng r
proof
let x be object;
assume x in Z;
then consider pN such that
A4: x=pN and
A5: dom pN = 2n & pN is dominated_by_0;
pN in Domin_0(2*n,Sum pN) by A5,Th20;
then 2*Sum pN <= 2n by Th22;
then 1/2*(2*Sum pN)<= 1/2*(2 * n) by XREAL_1:64;
then Sum pN < n+1 by NAT_1:13;
then
A6: Sum pN in Segm(n+1) by NAT_1:44;
then r.(Sum pN)=Domin_0(2n,Sum pN) by A2;
then
A7: pN in r.(Sum pN) by A5,Th20;
r.(Sum pN) in rng r by A2,A6,FUNCT_1:3;
hence thesis by A4,A7,TARSKI:def 4;
end;
A8: union rng r c= Z
proof
let x be object;
assume x in union rng r;
then consider y such that
A9: x in y and
A10: y in rng r by TARSKI:def 4;
consider i be object such that
A11: i in dom r and
A12: y = r.i by A10,FUNCT_1:def 3;
reconsider i as Nat by A11;
y=Domin_0(2n,i) by A2,A11,A12;
then consider p such that
A13: p=x & p is dominated_by_0 & dom p = 2n and
Sum p = i by A9,Def2;
p in NAT^omega by AFINSQ_1:def 7;
hence thesis by A13;
end;
A14: for i,j be Nat st i in dom r & j in dom r & i<>j holds r.i
misses r.j
proof
let i,j be Nat such that
A15: i in dom r and
A16: j in dom r and
A17: i<>j;
assume r.i meets r.j;
then r.i/\r.j<>{};
then consider x being object such that
A18: x in r.i/\r.j by XBOOLE_0:def 1;
A19: x in r.j by A18,XBOOLE_0:def 4;
r.j=Domin_0(2n,j) by A2,A16;
then
A20: ex q st q = x & q is dominated_by_0 & dom q = 2*n & Sum q = j by A19,Def2;
A21: x in r.i by A18,XBOOLE_0:def 4;
r.i=Domin_0(2n,i) by A2,A15;
then ex p st p = x & p is dominated_by_0 & dom p = 2n & Sum p = i by A21
,Def2;
hence thesis by A17,A20;
end;
A22: for i st i in dom r holds r.i is finite
proof
let i;
assume i in dom r;
then r.i=Domin_0(2n,i) by A2;
hence thesis;
end;
consider Cardr be XFinSequence of NAT such that
A23: dom Cardr = dom r and
A24: for i st i in dom Cardr holds Cardr.i=card (r.i) and
A25: card union rng r = Sum(Cardr) by A22,A14,STIRL2_1:66;
A26: n < dom Cardr & Cardr|(n+1)= Cardr by A2,A23,NAT_1:13;
defpred Q[Nat] means $1 <len Cardr implies Sum(Cardr|($1+1))=(2n choose $1);
A27: Q[0]
proof
0 in Segm(n+1) by NAT_1:44;
then r.0=Domin_0(2n,0) by A2;
then
A28: card (r.0)=1 by Th24;
A29: 0 in Segm 1 by NAT_1:44;
assume
A30: 0 <len Cardr;
then 1<=len Cardr by NAT_1:14;
then
A31: Segm 1 c= Segm len Cardr by NAT_1:39;
then
A32: len (Cardr|1)=1 by RELAT_1:62;
dom (Cardr|1)=1 by A31,RELAT_1:62;
then (Cardr|1).0=Cardr.0 by A29,FUNCT_1:47;
then
A33: Cardr|1=<%Cardr.0%> by A32,AFINSQ_1:34;
0 in len Cardr by A30,AFINSQ_1:86;
then Cardr.0 = card (r.0) by A24;
then Sum (Cardr|1)=1 by A33,A28,AFINSQ_2:53;
hence thesis by NEWTON:19;
end;
A34: for i st Q[i] holds Q[i+1]
proof
let i such that
A35: Q[i];
set i1=i+1;
assume
A36: i+1< len Cardr;
then
A37: i1 in dom Cardr by AFINSQ_1:86;
then
A38: Sum (Cardr|i1) + Cardr.i1 = Sum (Cardr|(i1+1)) & Cardr.i1=card(r.i1)
by A24,AFINSQ_2:65;
i1 <=n by A2,A23,A36,NAT_1:13;
then
A39: 2*i1<=2n by XREAL_1:64;
r.i1=Domin_0(2n,i1) by A2,A23,A37;
then
Sum(Cardr|(i1+1))=(2n choose i)+((2n choose i1)-(2n choose i)) by A35,A36
,A38,A39,Th28,NAT_1:13;
hence thesis;
end;
for i holds Q[i] from NAT_1:sch 2(A27,A34);
then Sum(Cardr)=(2n choose n) by A26;
hence thesis by A25,A3,A8,XBOOLE_0:def 10;
end;
theorem Th36:
for n,m,k,j,l st j = n-2*(k+1) & l = m-(k+1) holds card {pN : pN
in Domin_0(n,m) & 2*(k+1) = min*{N:2*Sum(pN|N) = N & N > 0}} = card Domin_0(2*k
,k) * card Domin_0(j,l)
proof
set q1=1-->1;
set q0=1-->0;
let n,m,k,j,l such that
A1: j=n-2*(k+1) & l=m-(k+1);
defpred P[object,object] means
ex r1,r2 be XFinSequence of NAT st $1 = q0^r1^q1^r2
& len (q0^r1^q1) = 2*(k+1) & $2 = [r1,r2];
set Z2=Domin_0(j,l);
set Z1=Domin_0(2*k,k);
set F={pN:pN in Domin_0(n,m) & 2 * (k + 1) = min*{N: 2*Sum(pN|N)=N&N>0}};
set 2k1=2*(k+1);
A2: for x being object st x in F ex y being object st y in [:Z1,Z2:] & P[x,y]
proof
A3: dom q0=1 & Sum q0=0*1 by AFINSQ_2:58;
let x be object;
assume x in F;
then consider pN such that
A4: pN=x & pN in Domin_0(n,m) & 2k1=min*{N: 2*Sum(pN|N)=N & N>0};
2k1>2*0 by XREAL_1:68;
then reconsider
M={N:2*Sum(pN|N)=N & N>0} as non empty Subset of NAT by A4,NAT_1:def 1;
consider r2 be XFinSequence of NAT such that
A5: pN = pN|2k1^r2 by Th1;
2k1>2*0 & pN is dominated_by_0 by A4,Th20,XREAL_1:68;
then consider r1 be XFinSequence of NAT such that
A6: pN|2k1 = q0^r1^q1 and
A7: r1 is dominated_by_0 by A4,Th14;
A8: Sum q1=1*1 by AFINSQ_2:58;
2k1 in M by A4,NAT_1:def 1;
then
A9: ex o be Nat st o=2k1 & 2*Sum(pN|o)=o & o>0;
then k+1=Sum (q0^r1) + Sum q1 by A6,AFINSQ_2:55;
then
A10: k=Sum q0+ Sum r1 by A8,AFINSQ_2:55;
pN is dominated_by_0 by A4,Th20;
then
A11: r2 is dominated_by_0 by A5,A9,Th12;
pN is dominated_by_0 by A4,Th20;
then
A12: len (pN|2k1)=2k1 by A9,Th11;
Sum pN=m by A4,Th20;
then
A13: m=k+1+Sum r2 by A5,A9,AFINSQ_2:55;
take [r1,r2];
dom pN=n by A4,Th20;
then n=2k1+len r2 by A5,A12,AFINSQ_1:def 3;
then
A15: r2 in Z2 by A1,A13,A11,Th20;
2k1=len(q0^r1)+len q1 by A6,A12,AFINSQ_1:17;
then 2*k+1=len q0+ len r1 by AFINSQ_1:17;
then r1 in Z1 by A7,A10,A3,Th20;
hence thesis by A4,A5,A6,A12,A15,ZFMISC_1:def 2;
end;
consider f being Function of F,[:Z1,Z2:] such that
A16: for x being object st x in F holds P[x,f.x] from FUNCT_2:sch 1(A2);
A17: [:Z1,Z2:]={} implies F={}
proof
assume [:Z1,Z2:]={};
then Z1={} or Z2={};
then 2*l > j by Th22;
then 2*m-2*(k+1) > n-2*(k+1) by A1;
then
A18: 2*m > n by XREAL_1:9;
assume F<>{};
then consider x being object such that
A19: x in F by XBOOLE_0:def 1;
ex pN st pN=x & pN in Domin_0(n,m) & 2k1=min*{N:2*Sum(pN|N)=N&N>0} by A19;
hence thesis by A18,Th22;
end;
then
A20: dom f=F by FUNCT_2:def 1;
A21: rng f=[:Z1,Z2:]
proof
A22: Sum q0=1*0 & Sum q1 = 1*1 by AFINSQ_2:58;
thus rng f c= [:Z1,Z2:];
let x be object;
assume x in [:Z1,Z2:];
then consider x1,x2 being object such that
A24: x1 in Z1 and
A25: x2 in Z2 and
A26: x=[x1,x2] by ZFMISC_1:def 2;
consider p such that
A27: p=x1 and
A28: p is dominated_by_0 and
A29: dom p = 2*k and
A30: Sum p = k by A24,Def2;
consider q such that
A31: q=x2 and
A32: q is dominated_by_0 and
A33: dom q = j and
A34: Sum q = l by A25,Def2;
set 0p1=q0^p^q1;
A35: dom (0p1^q)=len 0p1+len q by AFINSQ_1:def 3;
dom 0p1=len (q0^p)+ len q1 & dom q1=1 by AFINSQ_1:def 3;
then
A36: dom 0p1 = len q0+len p+1 by AFINSQ_1:17;
then (0p1^q)|(2*1+len p)=0p1 by AFINSQ_1:57;
then
A37: min*{N:2*Sum((0p1^q)|N)=N & N>0}=2*1+len p by A28,A29,A30,Th16;
1<= 1+len p - 2 * Sum p by A29,A30;
then 0p1 is dominated_by_0 by A28,Th10;
then
A38: 0p1^q is dominated_by_0 by A32,Th7;
A39: 0p1^q in NAT^omega by AFINSQ_1:def 7;
0p1=q0^(p^q1) by AFINSQ_1:27;
then Sum 0p1=Sum q0+ Sum (p^q1) by AFINSQ_2:55;
then Sum 0p1=(0 qua Nat)+ (Sum p+ 1) by A22,AFINSQ_2:55;
then Sum (0p1^q)=k+1+l by A30,A34,AFINSQ_2:55;
then 0p1^q in Domin_0(n,m) by A1,A29,A33,A38,A36,A35,Th20;
then
A40: 0p1^q in F by A29,A37,A39;
then consider r1,r2 be XFinSequence of NAT such that
A41: 0p1^q = q0^r1^q1^r2 and
A42: len (q0^r1^q1) = 2k1 and
A43: f.(0p1^q) = [r1,r2] by A16;
A44: (0p1^q)|2k1=0p1 by A29,A36,AFINSQ_1:57;
then q0^p=q0^r1 by A41,A42,AFINSQ_1:28,57;
then
A45: p=r1 by AFINSQ_1:28;
(q0^r1^q1^r2)|2k1=(q0^r1^q1) by A42,AFINSQ_1:57;
then q=r2 by A41,A44,AFINSQ_1:28;
hence thesis by A20,A26,A27,A31,A40,A43,A45,FUNCT_1:3;
end;
for x,y being object st x in F & y in F & f.x = f.y holds x = y
proof
let x,y being object such that
A46: x in F and
A47: y in F and
A48: f.x = f.y;
consider y1,y2 be XFinSequence of NAT such that
A49: y = q0^y1^q1^y2 and
len (q0^y1^q1) = 2k1 and
A50: f.y = [y1,y2] by A16,A47;
consider x1,x2 be XFinSequence of NAT such that
A51: x = q0^x1^q1^x2 and
len (q0^x1^q1) = 2k1 and
A52: f.x = [x1,x2] by A16,A46;
x1=y1 by A48,A52,A50,XTUPLE_0:1;
hence thesis by A48,A51,A52,A49,A50,XTUPLE_0:1;
end;
then f is one-to-one by A17,FUNCT_2:19;
then F,[:Z1,Z2:] are_equipotent by A20,A21,WELLORD2:def 4;
then card F=card [:Z1,Z2:] by CARD_1:5;
hence thesis by CARD_2:46;
end;
:: THE RECURRENCE RELATION FOR THE CATALAN NUMBERS
theorem Th37:
for n,m st 2*m <= n ex CardF be XFinSequence of NAT st card {pN:
pN in Domin_0(n,m) & {N:2*Sum(pN|N)=N & N > 0}<>{}} = Sum CardF & dom CardF = m
& for j st j < m holds CardF.j = card Domin_0(2*j,j) * card Domin_0(n-'2*(j+1),
m -'(j+1))
proof
let n,m such that
A1: 2*m <=n;
set Z=Domin_0(n,m);
defpred P[set,set] means for j st j=$1 holds $2={pN : pN in Domin_0(n,m) & 2
* (j + 1) = min*{N: 2*Sum(pN|N) = N&N>0}};
set W={pN: pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}<>{}};
A2: for k st k in Segm m ex x be Element of bool Z st P[k,x]
proof
let k such that
k in Segm m;
set NN={pN : pN in Domin_0(n,m) & 2*(k+1) = min*{N: 2*Sum(pN|N)=N & N>0}};
NN c= Z
proof
let x be object;
assume x in NN;
then ex pN st x=pN & pN in Z & 2*(k+1) = min*{N: 2*Sum(pN|N)=N&N>0};
hence thesis;
end;
then reconsider NN as Element of bool Z;
take NN;
thus thesis;
end;
consider C be XFinSequence of bool Z such that
A3: dom C= Segm m & for k st k in Segm m holds P[k,C.k]
from STIRL2_1:sch 5(A2);
A4: W c= union rng C
proof
let x be object;
assume x in W;
then consider pN such that
A5: x=pN & pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}<>{};
set I={N: 2*Sum(pN|N)=N & N>0};
I c= NAT
proof
let y be object;
assume y in I;
then ex i be Nat st i=y & 2*Sum(pN|i)=i & i>0;
hence thesis by ORDINAL1:def 12;
end;
then reconsider I as non empty Subset of NAT by A5;
min*I in I by NAT_1:def 1;
then consider M be Nat such that
A6: min*I=M and
A7: 2*Sum (pN|M)=M and
A8: M>0;
Sum (pN|M)>0 by A7,A8;
then reconsider Sum1=Sum (pN|M)-1 as Nat by NAT_1:20;
consider q such that
A9: pN=(pN|M)^q by Th1;
Sum pN =Sum (pN|M)+Sum q by A9,AFINSQ_2:55;
then m =Sum (pN|M)+Sum q by A5,Th20;
then
A10: m >= Sum (pN|M) by NAT_1:11;
Sum1+1 >Sum1 by NAT_1:13;
then m > Sum1 by A10,XXREAL_0:2;
then
A11: Sum1 in Segm m by NAT_1:44;
then
C.Sum1={qN:qN in Domin_0(n,m) & 2*(Sum1+1) = min*{N:2*Sum(qN|N)=N&N>0
}} by A3;
then
A12: pN in C.Sum1 by A5,A6,A7;
C.Sum1 in rng C by A3,A11,FUNCT_1:3;
hence thesis by A5,A12,TARSKI:def 4;
end;
A13: for i,j st i in dom C & j in dom C & i<>j holds C.i misses C.j
proof
let i,j such that
A14: i in dom C and
A15: j in dom C and
A16: i<>j;
assume C.i meets C.j;
then C.i/\C.j<>{};
then consider x being object such that
A17: x in C.i/\C.j by XBOOLE_0:def 1;
A18: x in C.j by A17,XBOOLE_0:def 4;
C.j={qN : qN in Domin_0(n,m) & 2 *(j+1) = min*{N: 2*Sum(qN|N) = N & N
>0 }} by A3,A15;
then
A19: ex qN st x=qN & qN in Domin_0(n,m) & 2*(j+1)=min*{N:2*Sum(qN|N)=N&N>0
} by A18;
A20: x in C.i by A17,XBOOLE_0:def 4;
C.i={pN : pN in Domin_0(n,m) & 2 *(i+1) = min*{N: 2*Sum(pN|N) = N & N
>0 }} by A3,A14;
then
ex pN st x=pN & pN in Domin_0(n,m) & 2 *(i+1) = min*{N: 2 *Sum(pN|N) =
N & N>0} by A20;
hence thesis by A16,A19;
end;
A21: for k st k in dom C holds C.k is finite
proof
let k;
assume k in dom C;
then
A22: C.k in rng C by FUNCT_1:3;
thus thesis by A22;
end;
consider CardC be XFinSequence of NAT such that
A23: dom CardC = dom C and
A24: for i st i in dom CardC holds CardC.i=card (C.i) and
A25: card union rng C = Sum(CardC) by A21,A13,STIRL2_1:66;
take CardC;
union rng C c= W
proof
let x be object;
assume x in union rng C;
then consider y such that
A26: x in y and
A27: y in rng C by TARSKI:def 4;
consider j be object such that
A28: j in dom C and
A29: C.j=y by A27,FUNCT_1:def 3;
reconsider j as Nat by A28;
y={pN : pN in Domin_0(n,m) & 2 *(j+1)=min*{N:2*Sum(pN|N)=N&N>0}} by A3,A28
,A29;
then consider pN such that
A30: x=pN & pN in Domin_0(n,m) & 2 *(j+1)=min*{N:2*Sum(pN|N)=N&N>0} by A26;
2*(j+1)<>0;
then {N : 2 * Sum(pN | N)=N & N>0} <>{} by A30,NAT_1:def 1;
hence thesis by A30;
end;
hence card W = Sum CardC & dom CardC = m by A3,A23,A25,A4,XBOOLE_0:def 10;
let j such that
A31: j < m;
A32: m >=j+1 by A31,NAT_1:13;
then
A33: m-'(j+1)=m-(j+1) by XREAL_1:233;
set P={pN : pN in Domin_0(n,m) & 2 *(j+1)=min*{N:2*Sum(pN|N)=N&N>0}};
j < len C by A3,A31;
then
A34: j in dom C by A3,NAT_1:44;
then
A35: C.j=P by A3;
2*(j+1)<= 2*m by A32,XREAL_1:64;
then
A36: n-'2*(j+1)=n-2*(j+1) by A1,XREAL_1:233,XXREAL_0:2;
CardC.j =card (C.j) by A23,A24,A34;
hence thesis by A36,A33,A35,Th36;
end;
theorem Th38:
for n st n > 0 holds Domin_0(2*n,n)={pN:pN in Domin_0(2*n,n) & {
N: 2*Sum(pN|N) = N & N > 0}<>{}}
proof
let n such that
A1: n>0;
set P={pN: pN in Domin_0(2*n,n) & {N: 2*Sum(pN|N)=N & N>0}<>{}};
thus Domin_0(2*n,n) c= P
proof
A2: n+n >(0 qua Nat)+(0 qua Nat) by A1;
let x be object such that
A3: x in Domin_0(2*n,n);
consider p such that
A4: x=p and
p is dominated_by_0 and
A5: dom p = 2*n & Sum p = n by A3,Def2;
A6: p in NAT^omega by AFINSQ_1:def 7;
2*Sum(p|(2*n))=2*n by A5;
then 2*n in {N: 2*Sum(p|N)=N & N>0} by A2;
hence thesis by A3,A4,A6;
end;
thus P c= Domin_0(2*n,n)
proof
let x be object;
assume x in P;
then ex pN st x=pN & pN in Domin_0(2*n,n) & {N: 2*Sum(pN|N)=N & N>0}<>{};
hence thesis;
end;
end;
theorem Th39:
for n st n > 0 ex Catal be XFinSequence of NAT st Sum Catal =
Catalan(n+1) & dom Catal = n & for j st j < n holds Catal.j = Catalan(j+1)*
Catalan(n-'j)
proof
let n such that
A1: n>0;
consider CardF be XFinSequence of NAT such that
A2: card {pN: pN in Domin_0(2*n,n) & {N:2*Sum(pN|N)=N&N>0}<>{}}=Sum CardF and
A3: dom CardF = n and
A4: for j st j < n holds CardF.j=card Domin_0(2*j,j)*card Domin_0(2*n-'2
*(j+1),n-'(j+1)) by Th37;
take CardF;
Sum CardF= card Domin_0(2*n,n) by A1,A2,Th38;
hence Sum CardF=Catalan(n+1) & dom CardF =n by A3,Th34;
let j such that
A5: j < n;
n-j > j-j by A5,XREAL_1:9;
then n-'j >0 by A5,XREAL_1:233;
then reconsider nj=(n-'j)-1 as Nat by NAT_1:20;
j+1<=n by A5,NAT_1:13;
then
A6: 2*n-'2*(j+1)=2*n-2*(j+1) & n-'(j+1)=n-(j+1) by XREAL_1:64,233;
A7: card Domin_0(2*j,j)=Catalan(j+1) by Th34;
n-j=n-'j by A5,XREAL_1:233;
then card Domin_0(2*n-'2*(j+1),n-'(j+1))=card Domin_0(2*nj,nj) by A6
.=Catalan(nj+1) by Th34;
hence thesis by A4,A5,A7;
end;
theorem Th40:
card {pN:pN in Domin_0(n+1,m) & {N: 2*Sum(pN|N) = N & N > 0} =
{}} = card Domin_0(n,m)
proof
defpred P[object,object]
means ex p st $1=<%0%>^p & $2=p;
set F={pN: pN in Domin_0(n+1,m) & {N: 2*Sum(pN|N)=N & N>0}={}};
set Z=Domin_0(n,m);
A1: for x being object st x in F ex y being object st y in Z & P[x,y]
proof
A2: len <%0%> =1 by AFINSQ_1:33;
let x be object;
A3: Sum <%0%>=0 by AFINSQ_2:53;
assume x in F;
then consider pN such that
A4: x=pN & pN in Domin_0(n+1,m) & {N: 2*Sum(pN|N)=N & N>0}={};
pN is dominated_by_0 & dom pN=n+1 by A4,Th20;
then consider q such that
A6: pN=<%0%>^q and
A7: q is dominated_by_0 by A4,Th17;
dom pN=len <%0%>+ len q by A6,AFINSQ_1:def 3;
then
A8: n+1=len q+1 by A4,A2,Th20;
take q;
Sum pN=Sum <%0%>+Sum q by A6,AFINSQ_2:55;
then Sum q=m by A4,A3,Th20;
hence thesis by A4,A6,A7,A8,Th20;
end;
consider f being Function of F,Z such that
A9: for x being object st x in F holds P[x,f.x] from FUNCT_2:sch 1(A1);
A10: Z={} implies F={}
proof
assume Z={};
then 2*m >n by Th22;
then
A11: 2*m >= n+1 by NAT_1:13;
assume F<>{};
then consider x being object such that
A12: x in F by XBOOLE_0:def 1;
consider pN such that
A13: x=pN & pN in Domin_0(n+1,m) & {N: 2*Sum(pN|N)=N & N>0}={} by A12;
dom pN=n+1 by A13,Th20;
then pN|(n+1)=pN;
then
A14: Sum(pN|(n+1))=m by A13,Th20;
pN is dominated_by_0 by A13,Th20;
then 2*m <= n +1 by A14,Th2;
then 2*Sum(pN|(n+1)) =n+1 by A14,A11,XXREAL_0:1;
then n+1 in {N:2*Sum(pN|N)=N&N>0};
hence thesis by A13;
end;
then
A15: dom f=F by FUNCT_2:def 1;
A16: rng f=Z
proof
thus rng f c= Z;
let x be object;
assume x in Z;
then consider p such that
A17: p = x and
A18: p is dominated_by_0 and
A19: dom p = n and
A20: Sum p = m by Def2;
set q=<%0%>^p;
A21: {N: 2*Sum(q|N)=N & N>0}={} by A18,Th18;
Sum q=Sum <%0%>+Sum p by AFINSQ_2:55;
then
A22: Sum q=(0 qua Nat)+m by A20,AFINSQ_2:53;
A23: q in NAT^omega by AFINSQ_1:def 7;
dom q=len <%0%>+len p by AFINSQ_1:def 3;
then
A24: dom q=1+n by A19,AFINSQ_1:33;
q is dominated_by_0 by A18,Th18;
then q in Domin_0(n+1,m) by A24,A22,Th20;
then
A25: q in F by A21,A23;
then consider r be XFinSequence of NAT such that
A26: q=<%0%>^r and
A27: f.q=r by A9;
r=p by A26,AFINSQ_1:28;
hence thesis by A15,A17,A25,A27,FUNCT_1:3;
end;
for x,y being object st x in F & y in F & f.x = f.y holds x = y
proof
let x,y being object such that
A28: x in F & y in F and
A29: f.x = f.y;
( ex p st x=<%0%>^p & f.x=p)& ex q st y=<%0%>^q & f.y=q by A9,A28;
hence thesis by A29;
end;
then f is one-to-one by A10,FUNCT_2:19;
then F,Z are_equipotent by A15,A16,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem
for n,m st 2*m <= n ex CardF be XFinSequence of NAT st card Domin_0(n,
m) = Sum CardF + card Domin_0(n-'1,m) & dom CardF = m & for j st j < m holds
CardF.j = card Domin_0(2*j,j) * card Domin_0(n-'2*(j+1),m-'(j+1))
proof
let n,m such that
A1: 2*m <=n;
set Z=Domin_0(n,m);
set Zne={pN: pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}<>{}};
A2: Zne c= Z
proof
let x be object;
assume x in Zne;
then ex pN st x=pN & pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}<>{};
hence thesis;
end;
set Ze={pN: pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}={}};
A3: Ze c= Z
proof
let x be object;
assume x in Ze;
then ex pN st x=pN & pN in Domin_0(n,m) & {N: 2*Sum(pN|N)=N & N>0}={};
hence thesis;
end;
reconsider Zne as finite set by A2;
consider C be XFinSequence of NAT such that
A4: card Zne = Sum C and
A5: dom C = m and
A6: for j st j < m holds C.j=card Domin_0(2*j,j)*card Domin_0(n-'2*(j+1
),m-'(j+1)) by A1,Th37;
reconsider Ze as finite set by A3;
take C;
A7: Ze misses Zne
proof
assume Ze meets Zne;
then consider x being object such that
A8: x in Ze and
A9: x in Zne by XBOOLE_0:3;
A10: ex qN st qN=x & qN in Z & {N: 2*Sum(qN|N)=N & N>0}={} by A8;
ex pN st pN=x & pN in Z & {N: 2*Sum(pN|N)=N & N>0}<>{} by A9;
hence thesis by A10;
end;
A11: Z c= Ze \/ Zne
proof
let x be object such that
A12: x in Z;
consider p be XFinSequence of NAT such that
A13: p = x and
p is dominated_by_0 and
dom p = n and
Sum p = m by A12,Def2;
reconsider p as Element of NAT^omega by AFINSQ_1:def 7;
set I={N: 2*Sum(p|N)=N & N>0};
now
per cases;
suppose
I={};
then p in Ze by A12,A13;
hence thesis by A13,XBOOLE_0:def 3;
end;
suppose
I<>{};
then p in Zne by A12,A13;
hence thesis by A13,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
Ze\/ Zne c= Z by A3,A2,XBOOLE_1:8;
then
A14: Ze\/Zne=Z by A11;
now
per cases;
suppose
A15: n=0;
then 2*m=0 by A1;
then C={} by A5;
then A16:Sum C= 0;
n-1<1-1 by A15;
hence card Z = Sum C + card Domin_0(n-'1,m) by A15,A16,XREAL_0:def 2;
end;
suppose
A17: n>0;
then reconsider n1=n-1 as Nat by NAT_1:20;
n=n1+1;
then
A18: card Ze = card Domin_0(n1,m) by Th40;
n1 = n-'1 by A17,NAT_1:14,XREAL_1:233;
hence card Z = Sum C+card Domin_0(n-'1,m) by A7,A14,A4,A18,CARD_2:40;
end;
end;
hence thesis by A5,A6;
end;
theorem
for n,k ex p st Sum p = card Domin_0(2*n+2+k,n+1) & dom p = k+1 & for
i st i <= k holds p.i = card Domin_0(2*n+1+i,n)
proof
let n,k;
defpred P[set,set] means for j st $1=j holds $2=card Domin_0(2*n+1+j,n);
A1: for i st i in Segm(k+1) ex x be Element of NAT st P[i,x]
proof
let i such that
i in Segm(k+1);
P[i,card Domin_0(2*n+1+i,n)];
hence thesis;
end;
consider p such that
A2: dom p=Segm(k+1) and
A3: for i be Nat st i in Segm(k+1) holds P[i,p.i] from STIRL2_1:sch 5(A1);
take p;
A4: for i st i <= k holds p.i = card Domin_0(2*n+1+i,n)
proof
let i;
assume i <= k;
then i<k+1 by NAT_1:13;
then i in Segm(k+1) by NAT_1:44;
hence thesis by A3;
end;
now
per cases;
suppose
A5: n=0;
for x being object st x in dom p holds p.x = 1
proof
let x be object such that
A6: x in dom p;
reconsider i=x as Nat by A6;
p.i=card Domin_0(2*n+1+i,n) by A2,A3,A6;
hence thesis by A5,Th24;
end;
then p=(k+1)-->1 by A2,FUNCOP_1:11;
then Sum p=(k+1)*1 by AFINSQ_2:58;
hence Sum p = card Domin_0(2*n+2+k,n+1) by A5,Th30;
end;
suppose
n>0;
then reconsider n1=n-1 as Nat by NAT_1:20;
defpred Q[Nat ] means for q st dom q = $1+1 & for i st i <= $1
holds q.i = card Domin_0(2*n+1+i,n) holds Sum q = card Domin_0(2*n+2+$1,n+1);
A7: for j st Q[j] holds Q[j+1]
proof
let j such that
A8: Q[j];
set CH2=(2*n+2+j) choose (n1+1);
set CH1=(2*n+2+j) choose (n+1);
set j1=j+1;
let q such that
A9: dom q=j1+1 and
A10: for i st i<=j1 holds q.i=card Domin_0(2*n+1+i,n);
A11: 2*(n+1)<=2*(n+1)+j1 by NAT_1:11;
j1 <=j1+1 by NAT_1:11;
then Segm j1 c= Segm(j1+1) by NAT_1:39;
then
A12: dom (q|j1)=j1 by A9,RELAT_1:62;
A13: for i st i<=j holds (q|j1).i = card Domin_0(2*n+1+i,n)
proof
let i;
assume i<=j;
then i<j1 by NAT_1:13;
then i < len(q|j1) by A12;
then i in dom (q|j1) & q.i= card Domin_0(2*n+1+i,n) by A10,A12,
AFINSQ_1:86;
hence thesis by FUNCT_1:47;
end;
set CH4=(2*n+1+j1) choose n1;
set CH3=(2*n+1+j1) choose n;
A14: 2*n<=2*n+(1+j1) & n1+1=n by NAT_1:11;
q.j1=card Domin_0(2*n+1+j1,n) by A10;
then
A15: q.j1=CH3-CH4 by A14,Th28;
j1 <j1+1 by NAT_1:13;
then j1 < len q by A9;
then j1 in dom q by AFINSQ_1:86;
then
A16: Sum (q|(j1+1))=Sum (q|j1) + q.j1 by AFINSQ_2:65;
2*(n+1)<=2*n+2+j by NAT_1:11;
then card Domin_0(2*n+2+j,n+1)=CH1-CH2 by Th28;
then Sum(q|j1)=CH1-CH2 by A8,A12,A13;
then Sum(q|j1)+q.j1=CH1+CH2-(CH3+CH4) by A15
.=((2*n+2+j+1) choose (n+1))-(CH3+CH4) by NEWTON:22
.=((2*n+2+j1) choose (n+1))-((2*n+2+j1) choose (n1+1)) by NEWTON:22
.=card Domin_0(2*n+2+j1,n+1) by A11,Th28;
hence thesis by A9,A16;
end;
A17: Q[0]
proof
reconsider 2n1=2*n+1 as Nat;
set 2CHn=(2*n+2) choose n;
set 2CHn91=(2*n+2) choose (n+1);
set CHn91=2n1 choose (n+1);
set CHn1=2n1 choose n1;
set CHn=2n1 choose n;
let q;
assume
dom q= (0 qua Nat)+1 &
for i st i <= 0 holds q.i = card Domin_0(2*n+1+i ,n);
then
A18: q.0=card Domin_0(2*n+1+(0 qua Nat),n) & len q = 1;
A19: 2*n+2=(2*n+1)+1;
then
A20: 2CHn91 = CHn91 + CHn by NEWTON:22;
n1+1=n;
then
A21: 2CHn = CHn + CHn1 by A19,NEWTON:22;
n<=n+(n+1) & (2*n+1)-n=n+1 by NAT_1:11;
then
A22: CHn = CHn91 by NEWTON:20;
2*(n+1)=2*n+2;
then
A23: card Domin_0(2*n+2,n+1)=2CHn91-2CHn by Th28;
card Domin_0(2n1,n1+1)=CHn-CHn1 & Sum <%q.0%>=q.0
by Th28,AFINSQ_2:53,NAT_1:11;
hence thesis by A20,A21,A22,A23,A18,AFINSQ_1:34;
end;
for j holds Q[j] from NAT_1:sch 2(A17,A7);
hence Sum p = card Domin_0(2*n+2+k,n+1) by A2,A4;
end;
end;
hence thesis by A2,A4;
end;
begin
reserve seq1,seq2,seq3,seq4 for Real_Sequence,
r,s,e for Real,
Fr,Fr1, Fr2 for XFinSequence of REAL;
Lm3: (dom Fr=1 or len Fr=1) implies Sum Fr=Fr.0
proof
assume dom Fr=1 or len Fr=1;
then len Fr=1;
then Fr=<%Fr.0%> by AFINSQ_1:34;
hence thesis by AFINSQ_2:53;
end;
Lm4: for Fr1,Fr2 st dom Fr1=dom Fr2 & for n st n in len Fr1 holds Fr1.n=Fr2.(
len Fr1-'(1+n)) holds Sum Fr1 = Sum Fr2
proof
let Fr1,Fr2 such that
A1: dom Fr1=dom Fr2 and
A2: for n st n in len Fr1 holds Fr1.n=Fr2.(len Fr1-'(1+n));
defpred P[object,object] means
for i st i=$1 holds $2=len Fr1-'(1+i);
A3: card len Fr1 =card len Fr1;
A4: for x being object st x in len Fr1
ex y being object st y in len Fr1 & P[x,y]
proof
let x being object such that
A5: x in len Fr1;
reconsider k=x as Nat by A5;
k< len Fr1 by A5,AFINSQ_1:86;
then k+1 <= len Fr1 by NAT_1:13;
then
A6: len Fr1-'(1+k)=len Fr1-(1+k) by XREAL_1:233;
take len Fr1-'(1+k);
len Fr1 +(0 qua Nat)< len Fr1 +(1+k) by XREAL_1:8;
then len Fr1-(1+k) < len Fr1+(1+k)-(1+k) by XREAL_1:9;
hence thesis by A6,AFINSQ_1:86;
end;
consider P be Function of len Fr1,len Fr1 such that
A7: for x being object st x in len Fr1 holds P[x,P.x] from FUNCT_2:sch 1(A4);
for x1,x2 being object st x1 in len Fr1 & x2 in len Fr1 & P.x1 = P.x2
holds x1 = x2
proof
let x1,x2 being object such that
A8: x1 in len Fr1 and
A9: x2 in len Fr1 and
A10: P.x1 = P.x2;
reconsider i=x1,j=x2 as Nat by A8,A9;
j < len Fr1 by A9,AFINSQ_1:86;
then j+1 <= len Fr1 by NAT_1:13;
then len Fr1-'(1+j)=len Fr1-(1+j) by XREAL_1:233;
then
A11: P.x2=len Fr1-(1+j) by A7,A9;
i< len Fr1 by A8,AFINSQ_1:86;
then i+1 <= len Fr1 by NAT_1:13;
then len Fr1-'(1+i)=len Fr1-(1+i) by XREAL_1:233;
then P.x1=len Fr1-(1+i) by A7,A8;
hence thesis by A10,A11;
end;
then
A12: P is one-to-one by FUNCT_2:56;
then P is onto by A3,FINSEQ_4:63;
then reconsider P as Permutation of dom Fr1 by A12;
A13: now
let x be object such that
A14: x in dom Fr1;
reconsider k=x as Nat by A14;
P.k=len Fr1-'(1+k) by A7,A14;
hence Fr1.x=Fr2.(P.x) by A2,A14;
end;
A15: for x being object st x in dom Fr1 holds x in dom P & P.x in dom Fr2
proof let x be object;
assume
x in dom Fr1;
hence
x in dom P by FUNCT_2:52;
then P.x in rng P by FUNCT_1:3;
then P.x in dom Fr1;
then P.x in dom P by FUNCT_2:52;
hence thesis by A1;
end;
for x being object st x in dom P & P.x in dom Fr2 holds x in dom Fr1;
then Fr1 = Fr2 * P by A15,A13,FUNCT_1:10;
then addreal "**" Fr1 = addreal "**" Fr2 by A1,AFINSQ_2:45
.= Sum Fr2 by AFINSQ_2:48;
hence thesis by AFINSQ_2:48;
end;
:: CAUCHY PRODUCT
definition
let seq1, seq2 be Real_Sequence;
func seq1 (##) seq2 -> Real_Sequence means
:Def4:
for k be Nat
ex Fr be XFinSequence of REAL
st dom Fr = k+1 &
(for n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) &
Sum Fr = it.k;
existence
proof
defpred P[object,object] means
for k be Nat st k=$1 ex Fr st dom Fr = k+1 & (for
n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) & Sum Fr = $2;
A1: for x being object st x in NAT ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
defpred Q[set,set] means for i st i=$1 holds $2=seq1.i * seq2.(k-'i);
A2: for i st i in Segm(k+1) ex z be Element of REAL st Q[i,z]
proof
let i such that
i in Segm(k+1);
reconsider ss = seq1.i * seq2.(k-'i) as Element of REAL;
take ss;
thus thesis;
end;
consider Fr such that
A3: dom Fr = Segm(k+1) and
A4: for i st i in Segm(k+1) holds Q[i,Fr.i] from STIRL2_1:sch 5(A2);
take Sum Fr;
for n be Nat st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n) by A4;
hence thesis by A3,XREAL_0:def 1;
end;
consider seq3 such that
A5: for x being object st x in NAT holds P[x,seq3.x] from FUNCT_2:sch 1(A1);
for k be Nat holds ex Fr st dom Fr = k+1 & (for n st n in k+1 holds Fr
.n = seq1.n * seq2.(k-'n)) & Sum Fr = seq3.k
by ORDINAL1:def 12,A5;
hence thesis;
end;
uniqueness
proof
let seq3,seq4 such that
A6: for k be Nat ex Fr be XFinSequence of REAL st dom Fr = k+1 & (for
n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) & Sum Fr = seq3.k and
A7: for k be Nat ex Fr be XFinSequence of REAL st dom Fr = k+1 & (for
n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) & Sum Fr = seq4.k;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
consider Fr1 be XFinSequence of REAL such that
A8: dom Fr1 = k+1 and
A9: for n st n in k+1 holds Fr1.n = seq1.n * seq2.(k-'n) and
A10: Sum Fr1 = seq3.k by A6;
consider Fr2 be XFinSequence of REAL such that
A11: dom Fr2 = k+1 and
A12: for n st n in k+1 holds Fr2.n = seq1.n * seq2.(k-'n) and
A13: Sum Fr2 = seq4.k by A7;
now
let n be Nat such that
A14: n in dom Fr1;
Fr1.n=seq1.n * seq2.(k-'n) by A8,A9,A14;
hence Fr1.n=Fr2.n by A8,A12,A14;
end;
hence seq3.x=seq4.x by A8,A10,A11,A13,AFINSQ_1:8;
end;
hence seq3=seq4 by FUNCT_2:12;
end;
commutativity
proof
let seq3,seq1,seq2;
assume
A15: for k be Nat ex Fr be XFinSequence of REAL st dom Fr = k+1 & (for
n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) & Sum Fr = seq3.k;
let k be Nat;
consider Fr1 be XFinSequence of REAL such that
A16: dom Fr1 = k+1 and
A17: for n st n in k+1 holds Fr1.n = seq1.n * seq2.(k-'n) and
A18: Sum Fr1 = seq3.k by A15;
defpred Q[set,set] means for i st i=$1 holds $2=seq2.i * seq1.(k-'i);
reconsider k9=k as Nat;
A19: for i st i in Segm(k9+1) ex z be Element of REAL st Q[i,z ]
proof
let i such that
i in Segm(k9+1);
reconsider ss = seq2.i * seq1.(k-'i) as Element of REAL;
take ss;
thus thesis;
end;
consider Fr2 such that
A20: dom Fr2 = Segm(k9+1) and
A21: for i st i in Segm(k9+1) holds Q[i,Fr2.i] from
STIRL2_1:sch 5(A19);
take Fr2;
thus dom Fr2 = k+1 & for n st n in k+1 holds Fr2.n = seq2.n * seq1.(k-'n)
by A20,A21;
now
let n such that
A22: n in len Fr1;
A23: n < k+1 by A16,A22,AFINSQ_1:86;
then n <= k by NAT_1:13;
then
A24: k-'n=k-n by XREAL_1:233;
k-'n <= k-'n + n by NAT_1:11;
then
A25: k-'(k-'n)=k-(k-'n) by A24,XREAL_1:233;
n+1 <= len Fr2 by A20,A23,NAT_1:13;
then
A26: len Fr2-'(n+1)=(k+1)-(n+1) by A20,XREAL_1:233;
k-n<=k & k<k+1 by NAT_1:13,XREAL_1:43;
then k-n < k+1 by XXREAL_0:2;
then len Fr2-'(n+1) in Segm(k+1) by A26,NAT_1:44;
then Fr2.(len Fr2-'(n+1))=seq2.(k-'n) * seq1.n by A21,A26,A24,A25;
hence Fr1.n=Fr2.(len Fr1-'(1+n)) by A16,A17,A20,A22;
end;
hence thesis by A16,A18,A20,Lm4;
end;
end;
theorem
for Fr1,Fr2 st dom Fr1=dom Fr2 & for n st n in len Fr1 holds Fr1.n=Fr2
.(len Fr1-'(1+n)) holds Sum Fr1 = Sum Fr2 by Lm4;
theorem Th44:
for Fr1,Fr2 st dom Fr1=dom Fr2 & for n st n in len Fr1 holds Fr1
.n=r*Fr2.n holds Sum Fr1 = r*Sum Fr2
proof
let Fr1,Fr2 such that
A1: dom Fr1=dom Fr2 and
A2: for n st n in len Fr1 holds Fr1.n=r*Fr2.n;
A3: Fr1|(dom Fr1)=Fr1 & Fr2|(dom Fr1)=Fr2 by A1;
defpred P[Nat] means $1 <= len Fr1 implies Sum(Fr1|$1)=r*Sum(Fr2|
$1);
A4: for i st P[i] holds P[i+1]
proof
let i such that
A5: P[i];
assume
A6: i+1 <= len Fr1;
then i< len Fr1 by NAT_1:13;
then
A7: i in len Fr1 by AFINSQ_1:86;
then
A8: Fr1.i=r*Fr2.i by A2;
Sum(Fr1|(i+1))=Fr1.i+Sum(Fr1|i) & Sum(Fr2|(i+1))=Fr2.i+Sum(Fr2|i) by A1,A7,
AFINSQ_2:65;
hence thesis by A5,A6,A8,NAT_1:13;
end;
A9: P[0];
for i holds P[i] from NAT_1:sch 2(A9,A4);
hence thesis by A3;
end;
theorem
seq1 (##) (r(#)seq2) = r(#)(seq1 (##) seq2)
proof
set RS=r(#)seq2;
set S=seq1 (##) seq2;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
consider Fr1 such that
A1: dom Fr1 = k+1 and
A2: for n st n in k+1 holds Fr1.n = seq1.n * RS.(k-'n) and
A3: Sum Fr1 = (seq1(##)RS).k by Def4;
consider Fr2 such that
A4: dom Fr2 = k+1 and
A5: for n st n in k+1 holds Fr2.n = seq1.n * seq2.(k-'n) and
A6: Sum Fr2 = S.k by Def4;
now
let n;
assume n in len Fr1;
then
A7: Fr1.n = seq1.n * RS.(k-'n) & Fr2.n = seq1.n * seq2.(k-'n) by A1,A2,A5;
RS.(k-'n)= r * seq2.(k-'n) by SEQ_1:9;
hence Fr1.n=r*Fr2.n by A7;
end;
then Sum Fr1 = r*Sum Fr2 by A1,A4,Th44;
hence (seq1(##)RS).x=(r(#)S).x by A3,A6,SEQ_1:9;
end;
hence thesis by FUNCT_2:12;
end;
theorem
seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3)
proof
set S=seq2 + seq3;
set S2=seq1 (##) seq2;
set S3=seq1 (##) seq3;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
consider Fr be XFinSequence of REAL such that
A1: dom Fr = k+1 and
A2: for n st n in k+1 holds Fr.n = seq1.n * S.(k-'n) and
A3: Sum Fr = (seq1(##)S).k by Def4;
consider Fr1 be XFinSequence of REAL such that
A4: dom Fr1 = k+1 and
A5: for n st n in k+1 holds Fr1.n = seq1.n * seq2.(k-'n) and
A6: Sum Fr1 = S2.k by Def4;
A7: len Fr1=len Fr by A1,A4;
consider Fr2 be XFinSequence of REAL such that
A8: dom Fr2 = k+1 and
A9: for n st n in k+1 holds Fr2.n = seq1.n * seq3.(k-'n) and
A10: Sum Fr2 = S3.k by Def4;
A11: for n be Nat st n in dom Fr holds Fr.n=addreal.(Fr1.n,Fr2.n)
proof
let n be Nat such that
A12: n in dom Fr;
A13: Fr.n = seq1.n * S.(k-'n) by A1,A2,A12;
A14: S.(k-'n)=seq2.(k-'n) + seq3.(k-'n) by SEQ_1:7;
Fr1.n = seq1.n * seq2.(k-'n) & Fr2.n = seq1.n * seq3.(k-'n) by A1,A5,A9
,A12;
then Fr.n=Fr1.n+Fr2.n by A13,A14;
hence thesis by BINOP_2:def 9;
end;
len Fr1=len Fr2 by A4,A8;
then addreal "**" Fr1^Fr2 = addreal "**" Fr by A11,A7,AFINSQ_2:46;
then Sum Fr=addreal "**" Fr1^Fr2 by AFINSQ_2:48;
then Sum Fr=Sum (Fr1^Fr2) by AFINSQ_2:48;
then Sum Fr=Sum (Fr1)+Sum(Fr2) by AFINSQ_2:55;
hence (seq1(##)S).x=(S2+S3).x by A3,A6,A10,SEQ_1:7;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th47:
(seq1 (##) seq2).0=seq1.0*seq2.0
proof
set S=seq1.0 * seq2.0;
consider Fr such that
A1: dom Fr = (0 qua Nat)+1 and
A2: for n st n in (0 qua Nat)+1 holds Fr.n = seq1.n * seq2.(0-'n) and
A3: Sum Fr = (seq1 (##) seq2).0 by Def4;
A4: 0-'0=0 & len Fr=1 by A1,XREAL_1:232;
0 in Segm 1 by NAT_1:44;
then Fr.0=seq1.0 * seq2.(0-'0) by A2;
then Fr=<%S%> by A4,AFINSQ_1:34;
hence thesis by A3,AFINSQ_2:53;
end;
reconsider zz = 0 as Nat;
theorem Th48:
for seq1, seq2, n ex Fr st Partial_Sums(seq1 (##) seq2).n = Sum
Fr & dom Fr=n+1 & for i st i in n+1 holds Fr.i=seq1.i * Partial_Sums(seq2).(n-'
i)
proof
let seq1,seq2,n;
set S=seq1 (##) seq2;
set P=Partial_Sums(seq2);
defpred P[Nat] means ex Fr st Partial_Sums(S).$1 = Sum Fr & dom Fr=$1+1 &
for i st i in $1+1 holds Fr.i=seq1.i * P.($1-'i);
A1: for n st P[n] holds P[n+1]
proof
set A=addreal;
let n;
set n1=n+1;
defpred Q[set,set] means for i st i=$1 holds $2=seq1.i * P.(n1-'i);
A2: n1-'n1=0 & P.0=seq2.0 by SERIES_1:def 1,XREAL_1:232;
A3: for i st i in Segm(n1+1) ex x be Element of REAL st Q[i,x]
proof
let i such that
i in Segm(n1+1);
reconsider ss = seq1.i * Partial_Sums(seq2).(n1-'i) as Element of REAL;
take ss;
thus thesis;
end;
consider Fr2 such that
A4: dom Fr2 = Segm(n1+1) and
A5: for i st i in Segm(n1+1) holds Q[i,Fr2.i] from STIRL2_1:sch 5(A3);
assume P[n];
then consider Fr such that
A6: Partial_Sums(S).n = Sum Fr and
A7: dom Fr=n1 and
A8: for i st i in n+1 holds Fr.i=seq1.i * P.(n-'i);
consider Fr1 such that
A9: dom Fr1 = n1+1 and
A10: for i st i in n1+1 holds Fr1.i = seq1.i * seq2.(n1-'i) and
A11: Sum Fr1 = S.n1 by Def4;
A12: Fr1|(n1+1)=Fr1 by A9;
A13: for i be Nat
st i in dom (Fr2|n1) holds (Fr2|n1).i=addreal.(Fr.i,(Fr1|n1).i)
proof
let i be Nat such that
A14: i in dom (Fr2|n1);
A15: i in dom Fr2 /\ n1 by A14,RELAT_1:61;
then i in dom(Fr1|n1) by A9,A4,RELAT_1:61;
then
A16: Fr1.i=(Fr1|n1).i by FUNCT_1:47;
A17: i in Segm n1 by A15,XBOOLE_0:def 4;
then
A18: i < n1 by NAT_1:44;
then i <=n by NAT_1:13;
then
A19: n-'i=n-i by XREAL_1:233;
i in n1+1 & i in NAT by A4,A15,XBOOLE_0:def 4;
then
A20: Fr1.i = seq1.i * seq2.(n1-'i) & Fr2.i=seq1.i * P.(n1-'i) by A10,A5;
A21: Fr2.i=(Fr2|n1).i by A14,FUNCT_1:47;
n1-'i=n1-i by A18,XREAL_1:233;
then (n-'i)+1=n1-'i by A19;
then
A22: P.(n1-'i)=P.(n-'i)+seq2.(n1-'i) by SERIES_1:def 1;
Fr.i=seq1.i * P.(n-'i) by A8,A17;
then Fr2.i=Fr.i+Fr1.i by A20,A22;
hence thesis by A16,A21,BINOP_2:def 9;
end;
n1<=n1+1 by NAT_1:11;
then
A23: Segm n1 c= Segm(n1+1) by NAT_1:39;
then
A24: len (Fr1|n1)=len Fr by A7,A9,RELAT_1:62;
n1 < n1+1 by NAT_1:13;
then
A25: n1 in Segm(n1+1) by NAT_1:44;
then
A26: Fr1.n1=seq1.n1 * seq2.(n1-'n1) & Sum(Fr1|(n1+1)) = Fr1.n1 + Sum(Fr1|
n1) by A9,A10,AFINSQ_2:65;
len (Fr2|n1)=len Fr by A7,A4,A23,RELAT_1:62;
then A"**"(Fr2|n1)=A"**"(Fr^(Fr1|n1)) by A13,A24,AFINSQ_2:46
.= Sum(Fr^(Fr1|n1)) by AFINSQ_2:48
.= Sum(Fr)+Sum(Fr1|n1) by AFINSQ_2:55;
then
A27: Sum(Fr2|n1)=Sum Fr+Sum(Fr1|n1) by AFINSQ_2:48;
take Fr2;
Fr2.n1=seq1.n1 * P.(n1-'n1) & Sum(Fr2|(n1+1)) = Fr2.n1 + Sum(Fr2|n1)
by A4,A5,A25,AFINSQ_2:65;
then Sum Fr2=Partial_Sums(S).n + S.n1 & n in NAT & n1 in NAT
by A6,A11,A4,A27,A2,A26,A12,ORDINAL1:def 12;
hence thesis by A4,A5,SERIES_1:def 1;
end;
A28: P[0]
proof
reconsider rr = seq1.0*seq2.0 as Element of REAL;
set Fr=1--> rr;
reconsider Fr as XFinSequence of REAL;
take Fr;
A29: dom Fr=1;
A30: Sum(Fr|zz) = 0;
A31: 0 in Segm 1 by NAT_1:44;
then
A32: Fr.zz=seq1.0*seq2.0 by FUNCOP_1:7;
A33: Sum(Fr|zz)+Fr.zz=Sum(Fr|(zz+1)) by A29,A31,AFINSQ_2:65;
Sum Fr = Sum(Fr|((0 qua Nat)+1))
.= Sum(Fr|zz)+Fr.zz by A33
.= Fr.zz by A30
.=S.0 by Th47,A32;
hence Partial_Sums(S).0 = Sum Fr & dom Fr=(0 qua Nat)+1
by SERIES_1:def 1;
let i such that
A34: i in (0 qua Nat)+1;
i in Segm 1 by A34;
then i<1 by NAT_1:44;
then
A35: i=0 by NAT_1:14;
then (0-'i)=0 by XREAL_1:232;
then P.(0-'i)= seq2.0 by SERIES_1:def 1;
hence thesis by A34,A35,FUNCOP_1:7;
end;
for i holds P[i] from NAT_1:sch 2(A28,A1);
hence thesis;
end;
theorem Th49:
for seq1, seq2, n st seq2 is summable ex Fr st Partial_Sums(seq1
(##) seq2).n= Sum seq2 * Partial_Sums(seq1).n- Sum Fr & dom Fr=n+1 & for i st i
in n+1 holds Fr.i=seq1.i * Sum (seq2^\(n-'i+1))
proof
let seq1, seq2, n such that
A1: seq2 is summable;
defpred Q[set,set] means for i st i=$1 holds $2=seq1.i * Sum (seq2^\(n-'i+1)
);
set P2=Partial_Sums(seq2);
set P1=Partial_Sums(seq1);
set S=seq1 (##) seq2;
A2: for i st i in Segm(n+1) ex x be Element of REAL st Q[i,x]
proof
let i such that
i in Segm(n+1);
reconsider ss = seq1.i * Sum (seq2^\(n-'i+1)) as Element of REAL
by XREAL_0:def 1;
take ss;
thus thesis;
end;
consider Fr such that
A3: dom Fr = Segm(n+1) and
A4: for i st i in Segm(n+1) holds Q[i,Fr.i] from STIRL2_1:sch 5(A2);
consider Fr1 such that
A5: Partial_Sums(S).n = Sum Fr1 and
A6: dom Fr1=n+1 and
A7: for i st i in n+1 holds Fr1.i=seq1.i * P2.(n-'i) by Th48;
A8: 0 in Segm(n+1) by NAT_1:44;
then
A9: Fr1.0=seq1.0 * P2.(n-'0) &
Sum (Fr1|(zz+1))=Fr1.0 + Sum (Fr1|zz) by A6,A7,AFINSQ_2:65;
defpred P[Nat] means $1+1 <= n+1 implies Sum (Fr1|($1+1)) + Sum (
Fr|($1+1))= Sum seq2 * P1.$1;
A10: for k st P[k] holds P[k+1]
proof
let k such that
A11: P[k];
reconsider k1=k+1 as Nat;
assume
A12: k+1+1<=n+1;
then k1<n+1 by NAT_1:13;
then
A13: k1 in Segm(n+1) by NAT_1:44;
then
A14: Fr.k1=seq1.k1*Sum(seq2^\(n-'k1+1)) & Sum(Fr1|(k1+1))=Fr1.k1+Sum (Fr1|
k1) by A4,A6,AFINSQ_2:65;
A15:Sum (Fr1|k1) + Sum (Fr|k1)= Sum seq2 * P1.k by A12,A11,NAT_1:13;
Sum(Fr|(k1+1))=Fr.k1 + Sum (Fr|k1) & Fr1.k1=seq1.k1 * P2.(n-'k1) by A3,A7
,A13,AFINSQ_2:65;
then Sum(Fr|(k1+1)) + Sum(Fr1|(k1+1))
=seq1.k1 * ( Sum(seq2^\(n-'k1+1)) + P2.(n-'k1) )
+ Sum seq2 * P1.k by A15,A14
.=seq1.k1*Sum seq2 +Sum seq2 * P1.k by A1,SERIES_1:15
.=Sum seq2*(P1.k+seq1.k1)
.=P1.k1*Sum seq2 by SERIES_1:def 1;
hence thesis;
end;
A16: Sum (Fr|zz) = 0;
A17: Sum (Fr1|zz) = 0;
A18: Sum (Fr|(zz+1))=Fr.0 + Sum (Fr|zz) &
Fr.0= seq1.0 * Sum (seq2^\(n-'0+1)) by A3,A4,A8,AFINSQ_2:65;
then Sum (Fr|(zz+1))+Sum (Fr1|(zz+1))
= Fr.0 + Sum (Fr|zz)+Sum (Fr1|(zz+1))
.= Fr.0 + Sum (Fr1|(zz+1)) by A16
.= seq1.0 * Sum (seq2^\(n-'0+1)) + Sum (Fr1|(zz+1)) by A18
.= seq1.0 * Sum (seq2^\(n-'0+1)) +
Fr1.0 + Sum (Fr1|zz) by A9
.= seq1.0 * Sum (seq2^\(n-'0+1)) +
seq1.0 * P2.(n-'0) + Sum (Fr1|zz) by A9
.= seq1.0*(Sum(seq2^\(n-'0+1))+P2.(n-'0)) by A17
.=seq1.0*Sum seq2 by A1,SERIES_1:15;
then
A19: P[0] by SERIES_1:def 1;
A20: for k holds P[k] from NAT_1:sch 2(A19,A10);
take Fr;
A21: Fr1|(n+1)=Fr1 by A6;
Fr|(n+1)=Fr by A3;
then Sum Fr1 + Sum Fr= Sum seq2 * P1.n by A20,A21;
hence thesis by A3,A4,A5;
end;
theorem Th50:
for Fr ex absFr be XFinSequence of REAL st dom absFr=dom Fr &
|.Sum Fr.| <= Sum absFr & for i st i in dom absFr holds absFr.i=|.Fr.i.|
proof
let Fr;
defpred P[object,object] means $2=|.Fr.$1.|;
A1: for i st i in Segm len Fr ex x be Element of REAL st P[i,x]
proof let i;
assume i in Segm len Fr;
consider x being Real such that
A2: P[i,x];
reconsider x as Element of REAL by XREAL_0:def 1;
P[i,x] by A2;
hence thesis;
end;
consider absFr be XFinSequence of REAL such that
A3: dom absFr = Segm len Fr and
A4: for i st i in Segm len Fr holds P[i,absFr.i] from STIRL2_1:sch 5(A1);
defpred Q[Nat] means $1 <= len Fr implies |.Sum (Fr|$1).| <= Sum
(absFr|$1);
A5: for i st Q[i] holds Q[i+1]
proof
let i such that
A6: Q[i];
set i1=i+1;
assume
A7: i1<=len Fr;
then i < len Fr by NAT_1:13;
then
A8: i in dom Fr by AFINSQ_1:86;
then Sum(Fr|i1)=Fr.i+Sum(Fr|i) & absFr.i=|.Fr.i.| by A4,AFINSQ_2:65;
then
A9: |.Sum(Fr|i1).|<=absFr.i +|.Sum (Fr|i).| by COMPLEX1:56;
Sum(absFr|i1)=absFr.i+Sum (absFr|i) by A3,A8,AFINSQ_2:65;
then absFr.i + |.Sum (Fr|i).| <= Sum(absFr|i1) by A6,A7,NAT_1:13,XREAL_1:7;
hence thesis by A9,XXREAL_0:2;
end;
take absFr;
A10: Q[0] by COMPLEX1:44;
for i holds Q[i] from NAT_1:sch 2(A10,A5);
then |.Sum (Fr|(len Fr)).| <= Sum (absFr|(len Fr));
hence thesis by A3,A4;
end;
theorem Th51:
for seq1 st seq1 is summable ex r st 0 < r & for k holds |.Sum
(seq1^\k).| < r
proof
let seq1 such that
A1: seq1 is summable;
defpred P[Nat] means ex r st r>=0 & for i st i <= $1 holds |.Sum (seq1^\i)
.|<=r;
A2: for k st P[k] holds P[k+1]
proof
let k;
assume P[k];
then consider r such that
A3: r>=0 and
A4: for i st i <= k holds |.Sum (seq1^\i) .|<=r;
take M=max(r,|.Sum (seq1^\(k+1)).|);
thus M >=0 by A3,XXREAL_0:25;
let i such that
A5: i <= k+1;
now
per cases by A5,NAT_1:8;
suppose
i=k+1;
hence thesis by XXREAL_0:25;
end;
suppose
A6: i<=k;
A7: r<=M by XXREAL_0:25;
|.Sum (seq1^\i) .|<=r by A4,A6;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
set P=Partial_Sums(seq1);
A8: lim P= Sum seq1 by SERIES_1:def 3;
P is convergent by A1,SERIES_1:def 2;
then consider n be Nat such that
A9: for m be Nat
st n<=m holds |.P.m-Sum seq1.|<1 by A8,SEQ_2:def 7;
A10: P[0]
proof
take |.Sum(seq1).|;
thus |.Sum(seq1).|>=0 by COMPLEX1:46;
let i;
assume i<=0;
then i=0;
hence thesis by NAT_1:47;
end;
for k holds P[k] from NAT_1:sch 2(A10,A2);
then consider r such that
A11: r>=0 and
A12: for i st i <= n holds |.Sum (seq1^\i) .|<=r;
take r1=r+1;
thus r1>0 by A11;
let k;
now
per cases;
suppose
A13: k <= n;
A14: 0 qua Nat+r< r1 by XREAL_1:8;
|.Sum (seq1^\k) .|<=r by A12,A13;
hence thesis by A14,XXREAL_0:2;
end;
suppose
A15: k > n;
then reconsider k1=k-1 as Nat by NAT_1:20;
k1+1>n by A15;
then k1>=n by NAT_1:13;
then
A16: |.P.k1-Sum seq1.|<1 by A9;
Sum seq1 = P.k1+Sum(seq1^\(k1+1)) by A1,SERIES_1:15;
then |.-Sum(seq1^\(k1+1)).|<1 by A16;
then
A17: |. Sum(seq1^\(k1+1)) .|<1 by COMPLEX1:52;
1+(0 qua Nat)<=r1 by A11,XREAL_1:6;
hence thesis by A17,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th52:
for seq1, n, m st n <= m & for i holds seq1.i>=0 holds (
Partial_Sums seq1).n <= (Partial_Sums seq1).m
proof
let seq1, n, m such that
A1: n <= m and
A2: for i holds seq1.i>=0;
set S=Partial_Sums seq1;
defpred P[Nat] means S.n <= S.(n+$1);
A3: for i st P[i] holds P[i+1]
proof
let i such that
A4: P[i];
set ni=n+i;
S.(ni+1)=S.ni+seq1.(ni+1) & seq1.(ni+1)>=0 by A2,SERIES_1:def 1;
then S.(ni+1) >= S.ni + (0 qua Nat) by XREAL_1:6;
hence thesis by A4,XXREAL_0:2;
end;
A5: P[0];
A6: for i holds P[i] from NAT_1:sch 2(A5,A3);
reconsider m9=m, n9=n as Nat;
A7: n9+(m9-n9)=m9;
m9-n9 is Nat by A1,NAT_1:21;
hence thesis by A6,A7;
end;
:: CAUCHY PRODUCT THEOREM
theorem Th53:
for seq1, seq2 st seq1 is absolutely_summable & seq2 is summable
holds seq1 (##) seq2 is summable & Sum(seq1 (##) seq2) = Sum seq1 * Sum seq2
proof
let seq1, seq2 such that
A1: seq1 is absolutely_summable and
A2: seq2 is summable;
set S2=Sum seq2;
set S1=Sum seq1;
set PA=Partial_Sums(|.seq1.|);
set P2=Partial_Sums(seq2);
set P1=Partial_Sums(seq1);
set S=seq1 (##) seq2;
set P=Partial_Sums(S);
A3: for e st 0<e ex n be Nat st
for m be Nat st n<=m holds |.P.m-S1*S2.|<e
proof
seq1 is summable by A1;
then
A4: P1 is convergent by SERIES_1:def 2;
let e such that
A5: 0<e;
set e1=e/(3*(|.S2.|+1));
(|.S2.|+1)> (0 qua Nat)+(0 qua Nat) by COMPLEX1:46,XREAL_1:8;
then
A6: 3*(|.S2.|+1)>3*0 by XREAL_1:68;
then lim P1= S1 & e1>0 by A5,SERIES_1:def 3,XREAL_1:139;
then consider n0 be Nat such that
A7: for n be Nat st n0 <= n holds |.P1.n-S1.| < e1
by A4,SEQ_2:def 7;
set e3=e/(3*(Sum abs(seq1)+1));
|.S2.|+1>(0 qua Nat)+(0 qua Nat) by COMPLEX1:46,XREAL_1:8;
then
A8: e1*(|.S2.|+1)=e/3 by XCMPLX_1:92;
A9: P2 is convergent & lim P2= S2 by A2,SERIES_1:def 2,def 3;
consider r such that
A10: 0 < r and
A11: for k holds |.Sum(seq2^\k).| < r by A2,Th51;
set e2=e/(3*r);
A12: |.S2.|+1 > |.S2.|+(0 qua Nat) by XREAL_1:8;
A13: now
let n;
|.seq1.n.|=abs(seq1).n by SEQ_1:12;
hence abs(seq1).n>=0 by COMPLEX1:46;
end;
then A14:for n be Nat holds |.seq1.|.n>=0;
A15: abs seq1 is summable by A1,SERIES_1:def 4;
then Sum abs(seq1)>=0 by A14,SERIES_1:18;
then
A16: (Sum abs(seq1)+1)*e3=e/3 by XCMPLX_1:92;
A17: Sum abs seq1>=0 by A15,A14,SERIES_1:18;
then 3*(Sum abs(seq1)+1)>0*3 by XREAL_1:68;
then e3>0 by A5,XREAL_1:139;
then consider n2 be Nat such that
A18: for n be Nat st n2<=n holds |.P2.n-S2.|<e3 by A9,SEQ_2:def 7;
3*r>0*3 by A10,XREAL_1:68;
then e2>0 by A5,XREAL_1:139;
then consider n1 be Nat such that
A19: for n be Nat
st n1 <= n holds |.PA.n-PA.n1.| < e2 by A15,SERIES_1:21;
reconsider M=max(max(1,n0),max(n1+1,n2)) as Nat by TARSKI:1;
A20: max(n1+1,n2)<=M by XXREAL_0:25;
take 2M=M*2;
let m be Nat such that
A21: 2M <= m;
A22: max(1,n0)<=M by XXREAL_0:25;
then 0<M by XXREAL_0:25;
then reconsider M1=M-1 as Nat by NAT_1:20;
A23: M=M1+1;
A24: n1+1 <= max(n1+1,n2) by XXREAL_0:25;
then M1+1>=n1+1 by A20,XXREAL_0:2;
then M1>= n1 by XREAL_1:8;
then PA.M1>=PA.n1 by A13,Th52;
then PA.m-PA.M1<=PA.m-PA.n1 by XREAL_1:10;
then
A25: r*(PA.m-PA.M1)<=r*(PA.m-PA.n1) by A10,XREAL_1:64;
consider Fr such that
A26: P.m= S2 * P1.m- Sum Fr and
A27: dom Fr=m+1 and
A28: for i st i in m+1 holds Fr.i=seq1.i*Sum(seq2^\(m-'i+1))by A2,Th49;
consider absFr be XFinSequence of REAL such that
A29: dom absFr=dom Fr and
A30: |.Sum Fr.| <= Sum absFr and
A31: for i st i in dom absFr holds absFr.i=|.Fr.i.| by Th50;
A32: M<=M+M by NAT_1:11;
then
A33: M<=m by A21,XXREAL_0:2;
then M < len absFr by A27,A29,NAT_1:13;
then
A34: len (absFr|M)=M by AFINSQ_1:11;
n1+1 <= M by A24,A20,XXREAL_0:2;
then n1+1<=m by A33,XXREAL_0:2;
then
A35: n1 <= m by NAT_1:13;
then PA.m>=PA.n1 by A13,Th52;
then PA.m-PA.n1>=PA.n1-PA.n1 by XREAL_1:9;
then
A36: |.PA.m-PA.n1.|=(PA.m-PA.n1) by ABSVALUE:def 1;
consider Fr1 such that
A37: absFr=absFr|M^Fr1 by Th1;
A38: m+1=len (absFr|M)+ len Fr1 by A27,A29,A37,AFINSQ_1:def 3;
then
A39: Fr1|((m-M)+1)=Fr1 by A34;
A40: n2 <= max(n1+1,n2) by XXREAL_0:25;
then n2 <= M by A20,XXREAL_0:2;
then n2 <=2M by A32,XXREAL_0:2;
then n2 <= m & m in NAT by A21,XXREAL_0:2, ORDINAL1:def 12;
then
A41: |.P2.m-S2.|<e3 by A18;
defpred S[Nat] means M+$1+1<=m+1 implies Sum(Fr1|($1+1))<=r*(PA
.(M+$1)-PA.M1);
A42: for k st S[k] holds S[k+1]
proof
let k such that
A43: S[k];
set k1=k+1;
set Mk1=M+k1;
reconsider Mk=M+k as Nat;
A44: |.seq1.Mk1.|=abs(seq1).Mk1 by SEQ_1:12;
assume
A45: Mk1+1<=m+1;
then
A46: Mk1 <m+1 by NAT_1:13;
then
A47: Mk1 in Segm(m+1) by NAT_1:44;
then Fr.Mk1=seq1.Mk1*Sum(seq2^\(m-'Mk1+1)) by A28;
then
A48: |.Fr.Mk1.|=|.seq1.Mk1.|*|.Sum(seq2^\(m-'Mk1+1)).| by COMPLEX1:65;
Mk1<m+1 by A45,NAT_1:13;
then k1 < len Fr1 by A38,A34,XREAL_1:7;
then k1 in len Fr1 by AFINSQ_1:86;
then
A49: Sum(Fr1|(k1+1))=Fr1.k1+Sum(Fr1|k1) by AFINSQ_2:65;
m+1=len absFr by A27,A29;
then absFr.Mk1=Fr1.(Mk1-M) by A37,A34,A46,AFINSQ_1:19,NAT_1:11;
then
A50: Fr1.k1=|.Fr.Mk1.| by A27,A29,A31,A47;
A51: (|.seq1.|.(Mk+1)+PA.(Mk)) = PA.(Mk+1) by SERIES_1:def 1;
|.seq1.Mk1.|>=0 & |.Sum(seq2^\(m-'Mk1+1)).|<r by A11,COMPLEX1:46;
then Fr1.k1<=r*|.seq1.Mk1.| by A50,A48,XREAL_1:64;
then Sum(Fr1|(k1+1))<=r*|.seq1.|.Mk1+r*(PA.(M+k)-PA.M1)by A43,A45,A49
,A44,NAT_1:13,XREAL_1:7;
then Sum(Fr1|(k1+1))<=r*((|.seq1.|.Mk1+PA.(M+k))-PA.M1);
then Sum(Fr1|(k1+1))<=r*(PA.(M+k+1)-PA.M1) by A51;
hence thesis;
end;
|.PA.m - PA.n1.| < e2 by A19,A35;
then r*(PA.m-PA.n1)<=r*e2 by A10,A36,XREAL_1:64;
then
A52: r*(PA.m-PA.M1)<=r*e2 by A25,XXREAL_0:2;
A53: m=M+(m-M) & m-M=m-'M by A21,A32,XREAL_1:233,XXREAL_0:2;
A54: S[0]
proof
assume
A55: M+(0 qua Nat)+1<=m+1;
then
A56: M <m+1 by NAT_1:13;
then
A57: M in Segm(m+1) by NAT_1:44;
then
A58: Fr.M=seq1.M*Sum(seq2^\(m-'M+1)) by A28;
M+1-M<=m+1-M by A55,XREAL_1:9;
then Segm 1 c= Segm len Fr1 by A38,A34,NAT_1:39;
then
A59: dom (Fr1|1)=1 by RELAT_1:62;
m+1=len absFr by A27,A29;
then absFr.M=Fr1.(M-M) by A37,A34,A56,AFINSQ_1:19;
then Fr1.0=|.Fr.M.| by A27,A29,A31,A57;
then
A60: Fr1.0=|.seq1.M.|*|.Sum(seq2^\(m-'M+1)).| by A58,COMPLEX1:65;
A61: |.seq1.M.|>=0 & r>|.Sum(seq2^\(m-'M+1)) .| by A11,COMPLEX1:46;
0 in Segm 1 by NAT_1:44;
then
A62: (Fr1|1).0=Fr1.0 by A59,FUNCT_1:47;
PA.M1+|.seq1.|.(M1+1)=PA.(M1+1) by SERIES_1:def 1;
then
A63: PA.M-PA.M1=|.seq1.M.| by SEQ_1:12;
Sum (Fr1|1)=(Fr1|1).0 by A59,Lm3;
hence thesis by A62,A60,A63,A61,XREAL_1:64;
end;
for k holds S[k] from NAT_1:sch 2(A54,A42);
then Sum(Fr1)<=r*(PA.m-PA.M1) by A39,A53;
then Sum(Fr1)<=r*e2 by A52,XXREAL_0:2;
then
A64: Sum(Fr1)<=e/3 by A10,XCMPLX_1:92;
|.seq1.|.0>=0 by A13;
then
A65: |.seq1.|.0*|.P2.m-S2.|<=e3*|.seq1.|.0 by A41,XREAL_1:64;
A66: 0 in Segm(m+1) by NAT_1:44;
then
A67: Fr.0=seq1.0*Sum(seq2^\(m-'0+1)) by A28;
PA.M1 <= Sum |.seq1.| by A14,A15,RSSPACE2:3;
then
A68: e3* PA.M1 <= e3* Sum |.seq1.| by A5,A17,XREAL_1:64;
S2=P2.(m-'0)+Sum(seq2^\(m-'0+1)) & m-'0=m by A2,NAT_D:40,SERIES_1:15;
then
A69: Sum(seq2^\(m-'0+1))=S2-P2.m;
n0<= max(1,n0) by XXREAL_0:25;
then n0 <= M by A22,XXREAL_0:2;
then n0 <= m & m in NAT by A33,XXREAL_0:2, ORDINAL1:def 12;
then
A70: |.P1.m-S1.|<e1 by A7;
|.S2*(P1.m-S1).|=|.S2.|*|.P1.m-S1.| & |.S2.|>=0 by COMPLEX1:46,65;
then
A71: |.S2*(P1.m-S1).|<=|.S2.|*e1 by A70,XREAL_1:64;
A72: Sum absFr=Sum(absFr|M)+Sum Fr1 by A37,AFINSQ_2:55;
defpred Q[Nat] means $1+1 <= M implies Sum(absFr|($1+1))<= e3 *
PA.$1;
A73: n2 <= M by A40,A20,XXREAL_0:2;
A74: for k st Q[k] holds Q[k+1]
proof
let k such that
A75: Q[k];
reconsider k1=k+1 as Nat;
A76: |.seq1.k1.|=abs(seq1).k1 by SEQ_1:12;
A77: m-M >= 2M-M by A21,XREAL_1:9;
assume
A78: k+1+1<=M;
then
A79: k1<M by NAT_1:13;
then m-k1 >= m-M by XREAL_1:10;
then m-k1 >= M by A77,XXREAL_0:2;
then
A80: m-k1 >= n2 by A73,XXREAL_0:2;
e3*|.seq1.k1.|+Sum(absFr|k1) <= e3*|.seq1.k1.| + e3 * PA.k by A75,A78,
NAT_1:13,XREAL_1:6;
then e3*|.seq1.k1.|+Sum(absFr|k1)<=e3*(abs(seq1).k1+PA.k) & k in NAT
by A76,ORDINAL1:def 12;
then
A81: e3*|.seq1.k1.|+Sum(absFr|k1)<= e3* PA.k1 by SERIES_1:def 1;
k1<m by A33,A79,XXREAL_0:2;
then k1 < m+1 by NAT_1:13;
then
A82: k1 in Segm(m+1) by NAT_1:44;
then
A83: Sum(absFr|(k1+1))=absFr.k1 + Sum(absFr|k1) by A27,A29,AFINSQ_2:65;
m-k1=m-'k1 by A33,A79,XREAL_1:233,XXREAL_0:2;
then |.P2.(m-'k1)-S2.|<e3 by A18,A80;
then
A84: |.S2-P2.(m-'k1).|<e3 by COMPLEX1:60;
A85: S2=P2.(m-'k1)+Sum(seq2^\(m-'k1+1)) by A2,SERIES_1:15;
|.seq1.k1.|>=0 by COMPLEX1:46;
then |.S2-P2.(m-'k1).|*|.seq1.k1.| <= e3*|.seq1.k1.| by A84,XREAL_1:64;
then
A86:
|.seq1.k1 * Sum(seq2^\(m-'k1+1)).| <= e3 * |.seq1.k1.| by A85,COMPLEX1:65;
Fr.k1=seq1.k1*Sum(seq2^\(m-'k1+1)) & |.Fr.k1.|=absFr.k1 by A27,A28,A29
,A31,A82;
then Sum(absFr|(k1+1))<=e3*|.seq1.k1.|+Sum(absFr|k1) by A83,A86,
XREAL_1:6;
hence thesis by A81,XXREAL_0:2;
end;
A87: Sum(absFr|zz) = 0;
Sum(absFr|(zz+1))=absFr.0 + Sum(absFr|zz) & absFr.0=|.Fr.0.|
by A27,A29,A31,A66,AFINSQ_2:65;
then Sum(absFr|(zz+1))=|.seq1.0 .|*|.Sum(seq2^\(m-'0+1)).| by A67,A87,
COMPLEX1:65
.=abs(seq1).0*|.Sum(seq2^\(m-'0+1)).| by SEQ_1:12
.=abs(seq1).0*|.P2.m-S2.| by A69,COMPLEX1:60;
then
A88: Q[0] by A65,SERIES_1:def 1;
for k holds Q[k] from NAT_1:sch 2(A88,A74);
then
A89: Sum(absFr|M)<= e3 * PA.M1 by A23;
Sum abs(seq1)+1>Sum abs(seq1)+(0 qua Nat) by XREAL_1:8;
then e3*(Sum abs(seq1)+1) >= e3*Sum abs(seq1) by A5,A17,XREAL_1:64;
then e3* PA.M1 <=e/3 by A68,A16,XXREAL_0:2;
then Sum(absFr|M)<=e/3 by A89,XXREAL_0:2;
then Sum(absFr|M)+Sum Fr1 <=e/3+e/3 by A64,XREAL_1:7;
then
A90: |.Sum Fr.|<= e/3+e/3 by A30,A72,XXREAL_0:2;
P.m-S1*S2=S2*(P1.m-S1)-Sum Fr by A26;
then
A91: |.P.m-S1*S2.|<=|.S2*(P1.m-S1).|+|.Sum Fr.| by COMPLEX1:57;
e1>0 by A5,A6,XREAL_1:139;
then e1*(|.S2.|+1) > e1*|.S2.| by A12,XREAL_1:68;
then |.S2*(P1.m-S1).|<e/3 by A8,A71,XXREAL_0:2;
then |.S2*(P1.m-S1).|+|.Sum Fr.| <e/3+(e/3+e/3) by A90,XREAL_1:8;
hence thesis by A91,XXREAL_0:2;
end;
then
A92: P is convergent by SEQ_2:def 6;
hence S is summable by SERIES_1:def 2;
lim P = S1*S2 by A3,A92,SEQ_2:def 7;
hence thesis by SERIES_1:def 3;
end;
begin :: THE GENERATING FUNCTION FOR THE CATALAN NUMBERS
theorem
for r ex Catal be Real_Sequence st (for n holds Catal.n = Catalan(n+1)
* r|^n) & (|.r.| < 1/4 implies Catal is absolutely_summable & Sum Catal = 1 + r
* (Sum Catal) |^ 2 & Sum Catal = 2 / (1 + sqrt(1-4*r)) & (r<>0 implies Sum
Catal = (1 - sqrt(1-4*r)) / (2*r)) )
proof
defpred E[object,object] means
for r st $1=r ex Catal be Real_Sequence st (for n
holds Catal.n = Catalan(n+1) * r|^n) & (|.r.| < 1/4 implies Catal is
absolutely_summable & Sum Catal = 1 + r * (Sum Catal) |^ 2 & $2=Sum Catal);
A1: for x being object st x in REAL ex y being object st y in REAL & E[x,y]
proof
let x be object;
A2: |.1 .|=1 by ABSVALUE:def 1;
assume x in REAL;
then reconsider r=x as Real;
set a=4*|.r.|;
deffunc C(Nat)= In(Catalan($1+1) * r|^$1,REAL);
consider Cat be Real_Sequence such that
A3: for n be Element of NAT holds Cat.n = C(n) from FUNCT_2:sch 4;
set G=a GeoSeq;
defpred P[Nat] means abs(Cat).$1 <= G.$1;
A4: for n st P[n] holds P[n+1]
proof
A5: |.r.|>=0 by COMPLEX1:46;
let n;
assume P[n];
then
A6: a*abs(Cat).n <= a*G.n by A5,XREAL_1:64;
set n1=n+1;
A7: |.r|^n1.| >=0 & r|^n1= r*r|^n by COMPLEX1:46,NEWTON:6;
Catalan(n1+1)>=0 by CATALAN1:17;
then
A8: |.Catalan(n1+1).|=Catalan(n1+1) by ABSVALUE:def 1;
Catalan(n1)>=0 by CATALAN1:17;
then |.Catalan(n1).|=Catalan(n1) by ABSVALUE:def 1;
then |.Catalan(n1+1).| < 4*|.Catalan(n1).| by A8,CATALAN1:21;
then
A9: |.r|^n1.|*|.Catalan(n1+1).|<=(4*|.Catalan(n1).|)*|.r*r|^n.| by A7,
XREAL_1:64;
|.r*r|^n.| =|.r.|*|.r|^n.| by COMPLEX1:65;
then
|.C(n1).| <=a*(|.Catalan(n1).|*|.r|^n.|) by A9,COMPLEX1:65;
then |.Cat.n1.|<=a*(|.Catalan(n1).|*|.r|^n.|) by A3;
then |.Cat.n1.|<=a*|.C(n).| & n in NAT
by COMPLEX1:65,ORDINAL1:def 12;
then
A10: |.Cat.n1.|<=a*|.Cat.n.| by A3;
|.Cat.n.|=abs(Cat).n by SEQ_1:12;
then abs(Cat).n1<=a*abs(Cat).n by A10,SEQ_1:12;
then abs(Cat).n1<=a*G.n by A6,XXREAL_0:2;
hence thesis by PREPOWER:3;
end;
Cat.0=C(0) by A3;
then
A11: abs(Cat).0=|.r|^0.| by CATALAN1:11,SEQ_1:12;
r|^0=1 & a|^0= 1 by NEWTON:4;
then
A12: P[0] by A11,A2,PREPOWER:def 1;
for n holds P[n] from NAT_1:sch 2(A12,A4);
then A13: for n be Nat holds P[n];
A14: now
let n be Nat;
abs(Cat).n=|.Cat.n.| by SEQ_1:12;
hence abs(Cat).n>=0 by COMPLEX1:46;
end;
take Sum Cat;
thus Sum Cat in REAL by XREAL_0:def 1;
let s such that
A15: x=s;
for y being object st y in NAT holds (Cat^\1).y=(Cat (##) (r(#)Cat)).y
proof
let y be object;
assume y in NAT;
then reconsider n=y as Nat;
set n1=n+1;
consider Fr1 such that
A16: dom Fr1 = n1 and
A17: for i st i in n+1 holds Fr1.i = Cat.i * (r(#)Cat).(n-'i) and
A18: Sum Fr1 = (Cat (##) (r(#)Cat)).n by Def4;
consider Catal be XFinSequence of NAT such that
A19: Sum Catal = Catalan (n1+1) and
A20: dom Catal = n1 and
A21: for j st j<n1 holds Catal.j=Catalan(j+1)*Catalan(n1-'j) by Th39;
reconsider CatalR=Catal as XFinSequence of REAL;
defpred Q[set,set] means for k st k=$1 holds $2 = r |^ n1 * Catal.k;
A22: for k st k in Segm n1 ex x be Element of REAL st Q[k,x]
proof
let k such that
k in Segm n1;
reconsider rr = r |^ n1 * Catal.k as Element of REAL
by XREAL_0:def 1;
take rr;
thus thesis;
end;
consider Fr2 such that
A23: dom Fr2 = Segm n1 and
A24: for k be Nat st k in Segm n1 holds Q[k,Fr2.k] from STIRL2_1:sch 5(A22);
A25: now
let k be Nat such that
A26: k in dom Fr2;
k < len Fr2 by A26,AFINSQ_1:86;
then
A27: k<n+1 by A23;
then
A28: n1-'k=n1-k by XREAL_1:233;
A29: n=k+(n-k);
k<=n by A27,NAT_1:13;
then
A30: n-'k=n-k by XREAL_1:233;
then Fr1.k = Cat.k * (r(#)Cat).(n-k) by A17,A23,A26
.= C(k) * (r(#)Cat).(n-k) by A26,A3
.=Catalan(k+1) * r|^k * (r(#)Cat).(n-k)
.=Catalan(k+1) * r|^k * (r * Cat.(n-k)) by A30,SEQ_1:9
.=Catalan(k+1) * r|^k*(r*C(n-'k)) by A3,A30
.=Catalan(k+1) * Catalan(n1-'k) * r *(r|^k*r|^(n-'k)) by A30,A28
.=Catalan(k+1) * Catalan(n1-'k) * r *(r|^n) by A30,A29,NEWTON:8
.=Catal.k * r * r|^n by A21,A27
.=Catal.k * (r * r|^n)
.=Catal.k * r|^n1 by NEWTON:6
.=Fr2.k by A23,A24,A26;
hence Fr1.k=Fr2.k;
end;
for k st k in len Fr2 holds Fr2.k= r|^n1 * CatalR.k by A23,A24;
then Sum Fr2 = r|^n1 * (Sum CatalR) by A20,A23,Th44
.=C(n1) by A19
.=Cat.n1 by A3
.=(Cat^\1).n by NAT_1:def 3;
hence thesis by A16,A18,A23,A25,AFINSQ_1:8;
end;
then
A31: Cat^\1= Cat(##)(r(#)Cat) by FUNCT_2:12;
|.r.|>=0 by COMPLEX1:46;
then
A32: |.a.|=a by ABSVALUE:def 1;
take Cat;
hereby let n;
n in NAT by ORDINAL1:def 12;
hence Cat.n = C(n) by A3
.= Catalan(n+1) * s|^n by A15;
end;
A33: r|^0=1 by NEWTON:4;
Cat.0 = C(0) by A3
.=Catalan((0 qua Nat)+1)*r|^0;
then
A34: Partial_Sums(Cat).0=1 by A33,CATALAN1:11,SERIES_1:def 1;
assume |.s.| <1/4;
then a<4*(1/4) by A15,XREAL_1:68;
then G is summable by A32,SERIES_1:24;
then abs(Cat) is summable by A14,A13,SERIES_1:20;
hence
A35: Cat is absolutely_summable by SERIES_1:def 4;
then Cat is summable;
then r(#)Cat is summable & Sum(r(#)Cat)=r*Sum Cat by SERIES_1:10;
then Sum(Cat^\((0 qua Nat)+1))=Sum Cat *(r*Sum Cat) by A35,A31,Th53;
then Sum Cat= 1 + r*(Sum Cat*Sum Cat) by A35,A34,SERIES_1:15;
hence thesis by A15,WSIERP_1:1;
end;
consider SumC be Function of REAL,REAL such that
A36: for x being object st x in REAL holds E[x,SumC.x] from FUNCT_2:sch 1(A1);
A37: for r,s st 0<s & s <= r & r < 1/4 holds SumC.s <= SumC.r
proof
let r,s such that
A38: 0<s and
A39: s <= r and
A40: r < 1/4;
r in REAL by XREAL_0:def 1;
then consider Cr be Real_Sequence such that
A41: for n holds Cr.n = Catalan(n+1) * r|^n and
A42: |.r.| < 1/4 implies Cr is absolutely_summable & Sum Cr = 1 + r *
(Sum Cr) |^ 2 & SumC.r=Sum Cr by A36;
s in REAL by XREAL_0:def 1;
then consider Cs be Real_Sequence such that
A43: for n holds Cs.n = Catalan(n+1) * s|^n and
A44: |.s.| < 1/4 implies Cs is absolutely_summable & Sum Cs = 1 + s *
(Sum Cs) |^ 2 & SumC.s=Sum Cs by A36;
A45: now
let n be Nat;
s|^n <= r|^n & Catalan(n+1)>=0 by A38,A39,CATALAN1:17,PREPOWER:9;
then
A46: Catalan(n+1) * s|^n <= Catalan(n+1)*r|^n by XREAL_1:64;
Catalan(n+1)*r|^n=Cr.n by A41;
hence Cs.n <= Cr.n by A43,A46;
end;
A47: s < 1/4 by A39,A40,XXREAL_0:2;
thus thesis by A38,A39,A40,A47,A44,A42,A45,ABSVALUE:def 1,TIETZE:5;
end;
set R={r where r is Real:0<r & r<1/4 &
SumC.r=(1+sqrt(1-4*r))/(2*r)};
A48: for r st r<>0 & |.r.| < 1/4 holds SumC.r=(1-sqrt(1-4*r))/(2*r) or SumC.
r=(1+sqrt(1-4*r))/(2*r)
proof
let r such that
A49: r<>0 and
A50: |.r.| < 1/4;
r<=1/4 by A50,ABSVALUE:5;
then 4*r <= (1/4)*4 by XREAL_1:64;
then
A51: 4*r-4*r<=1-4*r by XREAL_1:9;
r in REAL by XREAL_0:def 1;
then consider Catal be Real_Sequence such that
for n holds Catal.n = Catalan(n+1) * r|^n and
A52: |.r.| < 1/4 implies Catal is absolutely_summable & Sum Catal = 1
+ r * (Sum Catal) |^ 2 & SumC.r=Sum Catal by A36;
set S=Sum Catal;
S=1+r*S^2 by A50,A52,WSIERP_1:1;
then
A53: r*S^2+(-1)*S+1=0;
delta(r,-1,1)= 1-4*r & -(-1)=1;
hence thesis by A49,A50,A52,A53,A51,FIB_NUM:6;
end;
A54: for r,s st 0<r & r<s & s<1/4 holds (1+sqrt(1-4*r))/(2*r) > (1+sqrt(1-4*
s))/(2*s)
proof
let r,s such that
A55: 0<r and
A56: r<s and
A57: s<1/4;
4*s<4*(1/4) by A57,XREAL_1:68;
then
A58: 4*s-4*s < 1-4*s by XREAL_1:9;
then
A59: sqrt(1-4*s)>0 by SQUARE_1:25;
4*r < 4*s by A56,XREAL_1:68;
then 1-4*r >= 1-4*s by XREAL_1:10;
then sqrt(1-4*r)>= sqrt(1-4*s) by A58,SQUARE_1:26;
then 1+sqrt(1-4*r)>=1+sqrt(1-4*s) by XREAL_1:7;
then
A60: (1+sqrt(1-4*r))/(2*r)>=(1+sqrt(1-4*s))/(2*r) by A55,XREAL_1:72;
2*r>2*0 & 2*r<2*s by A55,A56,XREAL_1:68;
then (1+sqrt(1-4*s))/(2*r)>(1+sqrt(1-4*s))/(2*s) by A59,XREAL_1:76;
hence thesis by A60,XXREAL_0:2;
end;
A61: R={}
proof
assume R<>{};
then consider x being object such that
A62: x in R by XBOOLE_0:def 1;
consider r be Real such that
x=r and
A63: 0<r and
A64: r<1/4 and
A65: SumC.r=(1+sqrt(1-4*r))/(2*r) by A62;
consider s be Real such that
A66: r<s and
A67: s< 1/4 by A64,XREAL_1:5;
A68: |.s.|=s by A63,A66,ABSVALUE:def 1;
4*s<4*(1/4) by A67,XREAL_1:68;
then 4*s-4*s < 1-4*s by XREAL_1:9;
then sqrt(1-4*s)>0 by SQUARE_1:25;
then 1-sqrt(1-4*s) <= 1-0 by XREAL_1:10;
then
A69: (1-sqrt(1-4*s))/(2*s)<=1/(2*s) by A63,A66,XREAL_1:72;
A70: 2*r>2*0 by A63,XREAL_1:68;
R c= {r}
proof
assume not R c= {r};
then R\{r}<>{} by XBOOLE_1:37;
then consider y being object such that
A71: y in R\{r} by XBOOLE_0:def 1;
y in R by A71;
then consider s be Real such that
A72: y=s and
A73: 0<s and
A74: s<1/4 and
A75: SumC.s=(1+sqrt(1-4*s))/(2*s);
A76: r<>s by A71,A72,ZFMISC_1:56;
now
per cases by A76,XXREAL_0:1;
suppose
A77: r>s;
then SumC.s > SumC.r by A54,A64,A65,A73,A75;
hence contradiction by A37,A64,A73,A77;
end;
suppose
A78: r<s;
then SumC.r > SumC.s by A54,A63,A65,A74,A75;
hence contradiction by A37,A63,A74,A78;
end;
end;
hence contradiction;
end;
then not s in R by A66,TARSKI:def 1;
then SumC.s<>(1+sqrt(1-4*s))/(2*s) by A63,A66,A67;
then
A79: SumC.s=(1-sqrt(1-4*s))/(2*s) by A48,A63,A66,A67,A68;
4*r<4*(1/4) by A64,XREAL_1:68;
then 4*r-4*r < 1-4*r by XREAL_1:9;
then sqrt(1-4*r)>0 by SQUARE_1:25;
then 1+(0 qua Nat)<1+sqrt(1-4*r) by XREAL_1:8;
then
A80: 1/(2*r) < SumC.r by A65,A70,XREAL_1:74;
2*r<2* s by A66,XREAL_1:68;
then 1/(2*s)<1/(2*r) by A70,XREAL_1:76;
then SumC.s<1/(2*r) by A79,A69,XXREAL_0:2;
then SumC.s<SumC.r by A80,XXREAL_0:2;
hence thesis by A37,A63,A66,A67;
end;
A81: for r st 0<r & |.r.| <1/4 holds SumC.r=(1-sqrt(1-4*r))/(2*r)
proof
let r such that
A82: 0<r and
A83: |.r.|<1/4;
assume SumC.r<>(1-sqrt(1-4*r))/(2*r);
then
A84: SumC.r=(1+sqrt(1-4*r))/(2*r) by A48,A82,A83;
|.r.|=r by A82,ABSVALUE:def 1;
then r in R by A82,A83,A84;
hence thesis by A61;
end;
A85: for r st r<0 & |.r.|<1/4 holds SumC.r=(1-sqrt(1-4*r))/(2*r)
proof
let r such that
A86: r<0 and
A87: |.r.|<1/4;
2*r<2*0 by A86,XREAL_1:68;
then
A88: |.2*r.|=-(2*r) & 0 qua Nat-2*r > 0 qua Nat-0 by ABSVALUE:def 1;
A89: |.-r.|<1/4 by A87,COMPLEX1:52;
then 1/4>= -r by ABSVALUE:5;
then 4*(1/4)>=4*(-r) by XREAL_1:64;
then 1-4*(-r)>=4*(-r)-4*(-r) by XREAL_1:9;
then sqrt(1-4*(-r))>=0 by SQUARE_1:def 2;
then
A90: 1-sqrt(1-4*(-r))<=1-0 by XREAL_1:10;
A91: sqrt(1-4*r)>0 by A86,SQUARE_1:25;
then 1+sqrt(1-4*r)> 1+(0 qua Nat) by XREAL_1:8;
then
A92: 1-sqrt(1-4*(-r)) < 1+sqrt(1-4*r) by A90,XXREAL_0:2;
1+sqrt(1-4*r)=|.1+sqrt(1-4*r).| by A91,ABSVALUE:def 1;
then
A93: (1-sqrt(1-4*(-r)))/(2*(-r))<|.1+sqrt(1-4*r).|/|.2*r.| by A92,A88,
XREAL_1:74;
-r in REAL by XREAL_0:def 1;
then E[-r,SumC.-r] by A36;
then
for s st -r=s ex Catal be Real_Sequence st (for n
holds Catal.n = Catalan(n+1) * s|^n) & (|.s.| < 1/4 implies Catal is
absolutely_summable & Sum Catal = 1 + s * (Sum Catal) |^ 2
& SumC.-r=Sum Catal);
then consider CR be Real_Sequence such that
A94: for n holds CR.n = Catalan(n+1) * (-r)|^n and
A95: |.-r.| < 1/4 implies CR is absolutely_summable & Sum CR = 1 +
(-r) * (Sum CR) |^ 2 & SumC.(-r)=Sum CR;
assume
A96: SumC.r<>(1-sqrt(1-4*r))/(2*r);
r in REAL by XREAL_0:def 1;
then consider Cr be Real_Sequence such that
A97: for n holds Cr.n = Catalan(n+1) * (r|^n) and
A98: |.r.| < 1/4 implies Cr is absolutely_summable & Sum Cr = 1 + r *
(Sum Cr) |^ 2 & SumC.r=Sum Cr by A36;
now
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
(-r)|^n=((-1) *r)|^n .=(-1)|^n* r|^n by NEWTON:7;
then
A99: |.(-r)|^n.|=|.(-1)|^n.|*|.r|^n.| by COMPLEX1:65
.=1*|.r|^n.| by SERIES_2:1;
Catalan(n+1)>=0 by CATALAN1:17;
then
A100: |.Catalan(n+1).|=Catalan(n+1) by ABSVALUE:def 1;
(-r)|^ n>=0 by A86,POWER:3;
then |.(-r)|^ n.|=(-r)|^ n by ABSVALUE:def 1;
then CR.n=|.r|^n.|*|.Catalan(n+1).| by A94,A99,A100
.=|.r|^n*Catalan(n+1).| by COMPLEX1:65
.=|.Cr.n.| by A97
.=abs(Cr).n by SEQ_1:12;
hence abs(Cr).x=CR.x;
end;
then
A101: abs(Cr)=CR by FUNCT_2:12;
0 qua Nat-r > 0 qua Nat-0 by A86;
then
A102: Sum CR=(1-sqrt(1-4*(-r)))/(2*(-r)) by A81,A95,A89;
|.Sum Cr.|<=Sum abs Cr by A87,A98,TIETZE:6;
then |.(1+sqrt(1-4*r))/(2*r).|<= Sum CR by A48,A86,A87,A98,A101,A96;
hence thesis by A102,A93,COMPLEX1:67;
end;
let r;
r in REAL by XREAL_0:def 1;
then consider Cat be Real_Sequence such that
A103: for n holds Cat.n = Catalan(n+1) * r|^n and
A104: |.r.| < 1/4 implies Cat is absolutely_summable & Sum Cat = 1 + r *
(Sum Cat) |^ 2 & SumC.r=Sum Cat by A36;
set s=sqrt(1-4*r);
take Cat;
thus for n holds Cat.n = Catalan(n+1) * r|^n by A103;
assume
A105: |.r.|<1/4;
hence Cat is absolutely_summable & Sum Cat = 1 + r*(Sum Cat)|^ 2 by A104;
A106: r<>0 implies Sum Cat = (1 - sqrt(1-4*r)) / (2*r)
proof
assume r<>0;
then r>0 or r<0;
hence thesis by A81,A85,A104,A105;
end;
now
per cases;
suppose
r=0;
hence 2 / (1 + s)=Sum Cat by A104,A105;
end;
suppose r<>0;
then
A108: 2*r<>0;
r<=1/4 by A105,ABSVALUE:5;
then 4*r <=4*(1/4) by XREAL_1:64;
then
A109: 1-4*r >= 4*r-4*r by XREAL_1:9;
then s >=0 by SQUARE_1:def 2;
then (1+s)/(1+s)=1 by XCMPLX_1:60;
then (1-s) / (2*r)=((1-s) / (2*r)) * ((1+s)/(1+s))
.=((1-s)*(1+s)) / ((2*r)*(1+s)) by XCMPLX_1:76
.=(1^2-s^2)/ ((2*r)*(1+s))
.=(1-(1-4*r))/ ((2*r)*(1+s)) by A109,SQUARE_1:def 2
.=((2*r)*2)/((2*r)*(1+s))
.=((2*r)/(2*r))*(2/(1+s)) by XCMPLX_1:76
.=(1)*(2/(1+s)) by A108,XCMPLX_1:60;
hence Sum Cat=2/(1+s) by A106;
end;
end;
hence thesis by A106;
end;