:: Catalan Numbers
:: by Dorota Cz\c{e}stochowska and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-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, ORDINAL1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, CARD_1,
NAT_1, ZFMISC_1, REALSET1, REAL_1, SUBSET_1, INT_1, CATALAN1, XCMPLX_0;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
REAL_1, NAT_1, NEWTON, INT_1, NAT_D, ZFMISC_1;
constructors XXREAL_0, REAL_1, NAT_1, NEWTON, ZFMISC_1, NAT_D, VALUED_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, NAT_2, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems NAT_1, XCMPLX_1, NAT_2, NEWTON, INT_1, XREAL_1, XXREAL_0, NAT_D;
schemes NAT_2, NAT_1;
begin :: Preliminaries
theorem Th1:
for n being Nat st n > 1 holds n -' 1 <= 2 * n -' 3
proof
let n be Nat;
assume
A1: n > 1;
then n -' 1 > 1 -' 1 by NAT_D:57;
then
A2: n -' 1 + n > 0 + n by XREAL_1:6;
2 * 1 < 2 * n by A1,XREAL_1:68;
then 2 + 1 <= 2 * n by NAT_1:13;
then
A3: 2 * n -' 3 = 2 * n - 3 by XREAL_1:233;
n -' 1 = n - 1 by A1,XREAL_1:233;
then 2 * n - 1 - 1 > n - 1 by A2,XREAL_1:9;
then 2 * n - 2 - 1 >= n - 1 by INT_1:52;
hence thesis by A1,A3,XREAL_1:233;
end;
theorem Th2:
for n being Nat st n >= 1 holds n -' 1 <= 2 * n -' 2
proof
let n be Nat;
assume
A1: n >= 1;
then 2 * 1 <= 2 * n by XREAL_1:64;
then
A2: 1 * (n -' 1) <= 2 * (n -' 1) & 2 * n -' 2 = 2 * n - 2 by XREAL_1:64,233;
n -' 1 = n - 1 by A1,XREAL_1:233;
hence thesis by A2;
end;
theorem Th3:
for n being Nat st n > 1 holds n < 2 * n -' 1
proof
let n be Nat;
assume
A1: n > 1;
then n + n > n + 1 by XREAL_1:6;
then
A2: n + n - 1 > n + 1 - 1 by XREAL_1:9;
1 * 2 < 2 * n by A1,XREAL_1:68;
hence thesis by A2,XREAL_1:233,XXREAL_0:2;
end;
theorem Th4:
for n being Nat st n > 1 holds n -' 2 + 1 = n -' 1
proof
let n be Nat;
assume n > 1;
then
A1: n -' 1 >= 1 by NAT_D:49;
n -' 2 + 1 = n -' 1 -' 1 + 1 by NAT_D:45
.= n -' 1 by A1,XREAL_1:235;
hence thesis;
end;
theorem
for n being Nat st n > 1 holds (4 * n * n - 2*n) / (n + 1) > 1
proof
defpred P[Nat] means (4 * $1 * $1 - 2*$1)/($1 + 1) > 1;
let n be Nat;
A1: for k be non trivial Nat st P[k] holds P[k + 1]
proof
let k be non trivial Nat such that
A2: P[k];
set k1 = k+1;
(4 * k * k - 2*k) / (k + 1) = (4 * k * k - 2*k) * ( 1/ (k + 1)) by
XCMPLX_1:99;
then (4 * k * k - 2*k) * (1 / (k + 1)) * (k + 1) > 1 * (k + 1) by A2,
XREAL_1:68;
then (4 * k * k - 2*k) > 1 * (k + 1) by XCMPLX_1:109;
then (4 * k * k - 2*k)-(k + 1) > 0 by XREAL_1:50;
then (4 * k * k - 3*k - 1) + (8 * k + 1) > 0 + 0;
then (4 * k1 * k1 - 2*k1 - (k1 + 1)) + (k1 + 1) > 0 + (k1 + 1) by XREAL_1:8
;
then (4 * k1 * k1 - 2 * k1) / (k1 + 1) > (k1 + 1) / (k1 + 1) by XREAL_1:74;
hence thesis by XCMPLX_1:60;
end;
assume n > 1;
then
A3: n is non trivial by NAT_2:28;
A4: P[2];
for k be non trivial Nat holds P[k] from NAT_2:sch 2 (A4, A1);
hence thesis by A3;
end;
theorem Th6:
for n being Nat st n > 1 holds (2 * n -' 2)! * n * (n
+ 1) < (2 * n)!
proof
let n be Nat;
assume
A1: n > 1;
then
A2: 2 * 1 < 2 * n by XREAL_1:68;
then
A3: 2 * n -' 1 + 1 = 2 * n by XREAL_1:235,XXREAL_0:2;
2 - 1 < 2 * n - 1 by A2,XREAL_1:9;
then
A4: 1 < 2 * n -' 1 by A2,XREAL_1:233,XXREAL_0:2;
2 * n -' 2 + 1 = 2 * n -' 1 -' 1 + 1 by NAT_D:45
.= 2 * n -' 1 by A4,XREAL_1:235;
then
A5: (2 * n -' 2)! * (2 * n -' 1) * (2 * n) = (2 * n -' 1)! * (2 * n) by
NEWTON:15
.= (2 * n)! by A3,NEWTON:15;
(2 * n -' 2)! > 0 by NEWTON:17;
then
A6: (2 * n -' 2)! * n > 0 * n & (2 * n -' 2)! * n < (2 * n -' 2)! * (2 * n
-' 1) by A1,Th3,XREAL_1:68;
n + 1 < n + n by A1,XREAL_1:6;
hence thesis by A5,A6,XREAL_1:98;
end;
theorem Th7:
for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4
proof
let n be Nat;
assume 2 * (2 - (3 / (n + 1))) >= 4;
then 2 * (2 - (3 / (n + 1))) / 2 >= 4 / 2 by XREAL_1:72;
then 2 - (3 / (n + 1)) - 2 >= 2 - 2 by XREAL_1:9;
then --- (3 / (n + 1)) >= 0;
hence thesis by XREAL_1:139;
end;
begin :: Catalan Numbers
definition
let n be Nat;
func Catalan (n) -> Real equals
((2*n -' 2) choose (n -' 1)) / n;
coherence;
end;
theorem Th8:
for n being Nat st n > 1 holds Catalan (n) = (2 * n -'
2)! / ((n -' 1)! * (n!))
proof
let n be Nat;
assume
A1: n > 1;
then
A2: 2 * 1 <= 2 * n by XREAL_1:64;
A3: n -' 1 + 1 = n by A1,XREAL_1:235;
A4: n -' 1 <= 2 * n -' 2 by A1,Th2;
(2*n -' 2) - (n -' 1) = (2*n -' 2) - (n - 1) by A1,XREAL_1:233
.= (2*n - 2) - (n - 1) by A2,XREAL_1:233
.= n -' 1 by A1,XREAL_1:233;
then
((2*n -' 2) choose (n -' 1)) = ((2*n -' 2)!) / ((n -' 1)! * ((n -' 1)!))
by A4,NEWTON:def 3;
then Catalan (n) = ((2*n -' 2)!) / ((n -' 1)! * ((n -' 1)!) * n) by
XCMPLX_1:78
.= ((2*n -' 2)!) / ((n -' 1)! * (((n -' 1)!) * n))
.= ((2*n -' 2)!) / ((n -' 1)! * (n!)) by A3,NEWTON:15;
hence thesis;
end;
theorem Th9:
for n being Nat st n > 1 holds Catalan n = 4 * ((2*n
-' 3) choose (n -' 1)) - ((2*n -' 1) choose (n -' 1))
proof
let n be Nat;
assume
A1: n > 1;
then
A2: n -' 1 <= 2 * n -' 3 by Th1;
A3: 2 * 1 <= 2 * n by A1,XREAL_1:64;
then
A4: 2 * n -' 2 = 2 * n - 2 by XREAL_1:233;
A5: 1 + 1 <= n by A1,NAT_1:13;
then
A6: 2 * 2 <= 2 * n by XREAL_1:64;
then 2 * n -' 3 = 2 * n - 3 by XREAL_1:233,XXREAL_0:2;
then
A7: 2 * n -' 3 + 1 = 2 * n - 2 .= 2 * n -' 2 by A3,XREAL_1:233;
(2*n -' 3) - (n -' 1) = (2*n -' 3) - (n - 1) by A1,XREAL_1:233
.= (2*n - 3) - (n - 1) by A6,XREAL_1:233,XXREAL_0:2
.= n - 2
.= n -' 2 by A5,XREAL_1:233;
then
((2*n -' 3) choose (n -' 1)) = ((2*n -' 3)!) / ((n -' 1)! * ((n -' 2)!))
by A2,NEWTON:def 3;
then
A8: 4 * ((2*n -' 3) choose (n -' 1)) = (4 * ((2*n -' 3)!)) / ((n -' 1)! * ((
n -' 2)!)) by XCMPLX_1:74;
A9: n -' 2 + 1 = n -' 1 by A1,Th4;
A10: n -' 1 = n - 1 by A1,XREAL_1:233;
then
A11: n -' 1 + 1 = n;
A12: 1 * n < 2 * n by A1,XREAL_1:68;
then
A13: 2 * n -' 1 = 2 * n - 1 by A1,XREAL_1:233,XXREAL_0:2;
1 < 2 * n by A1,A12,XXREAL_0:2;
then
A14: 2 * n -' 2 + 1 = 2 * n -' 1 by Th4;
1 < 2 * n by A1,A12,XXREAL_0:2;
then
A15: n -' 1 < 2 * n -' 1 by A12,NAT_D:57;
2 * n -' 1 - (n -' 1) = 2 * n -' 1 - (n - 1) by A1,XREAL_1:233
.= 2 * n -' 1 - n + 1
.= 2 * n - 1 - n + 1 by A1,A12,XREAL_1:233,XXREAL_0:2
.= n;
then
(2*n -' 1) choose (n -' 1) = ((2*n -' 1)!) / ((n -' 1)! * (n!)) by A15,
NEWTON:def 3;
then
A16: (2*n -' 1) choose (n -' 1) = ((2*n -' 2)! * (2*n -' 1)) / ((n -' 1)! *
(n!)) by A14,NEWTON:15;
n - 1 > 0 by A1,XREAL_1:50;
then
4 * ((2*n -' 3) choose (n -' 1)) = ((n * (n - 1)) * (4 * ((2*n -' 3)!))
) / (((n * (n - 1)) * ((n -' 1)! * ((n -' 2)!)))) by A1,A8,XCMPLX_1:6,91
.= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n - 1) * (n * ((n -' 1)!))
* ((n -' 2)!)))
.= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n - 1) * (n!) * ((n -' 2)!
))) by A11,NEWTON:15
.= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n!) * ((n -' 1) * ((n -' 2
)!)))) by A10
.= (2 * n * ((2 * n -' 2) * ((2*n -' 3)!))) / (((n!) * ((n -' 1)!))) by A4
,A9,NEWTON:15
.= (2 * n * ((2*n -' 2)!)) / (((n!) * ((n -' 1)!))) by A7,NEWTON:15;
then
4 * ((2*n -' 3) choose (n -' 1)) - ((2*n -' 1) choose (n -' 1)) = ((2 *
n * ((2*n -' 2)!)) - ((2*n -' 2)! * (2*n -' 1))) / (((n!) * ((n -' 1)!))) by
A16,XCMPLX_1:120
.= Catalan n by A1,A13,Th8;
hence thesis;
end;
theorem
Catalan 0 = 0;
theorem Th11:
Catalan 1 = 1
proof
Catalan 1 = (2*1 -' 2) choose 0 by XREAL_1:232
.= 1 by NEWTON:19;
hence thesis;
end;
theorem Th12:
Catalan 2 = 1
proof
A1: 4 -' 2 = 4 - 2 by XREAL_1:233
.= 2;
2 -' 1 = 2 - 1 by XREAL_1:233
.= 1;
then Catalan 2 = 2 / 2 by A1,NEWTON:23
.= 1;
hence thesis;
end;
theorem Th13:
for n being Nat holds Catalan (n) is Integer
proof
let n be Nat;
per cases by NAT_1:25;
suppose
n = 0;
hence thesis;
end;
suppose
n = 1;
hence thesis;
end;
suppose
n > 1;
then Catalan n = 4 * ((2*n -' 3) choose (n -' 1)) - ((2*n -' 1) choose (n
-' 1)) by Th9;
hence thesis;
end;
end;
theorem Th14:
for k being Nat holds Catalan (k + 1) = (2*k)! / (k! * ((k+1)!))
proof
let k be Nat;
reconsider l = 2*k - k as Nat;
l = k & 1*k <= 2*k by XREAL_1:64;
then
A1: (2*k) choose k = (2*k!)/((k!) * (k!)) by NEWTON:def 3;
2*k + 2 -' 2 = 2*k & k + 1 -' 1 = k by NAT_D:34;
then Catalan (k+1) = (2*k!) / ((k!) * (k!) * (k+1)) by A1,XCMPLX_1:78
.= (2*k!) / ((k!) * ((k!) * (k+1)))
.= (2*k!) / ((k!) * ((k+1)!)) by NEWTON:15;
hence thesis;
end;
theorem Th15:
for n being Nat st n > 1 holds Catalan (n) < Catalan (n + 1)
proof
let n be Nat;
set a = (2 * n -' 2)!;
set b = (2 * n)!;
A1: Catalan (n + 1) = (2*n)! / (n! * ((n+1)!)) by Th14;
assume
A2: n > 1;
then n -' 1 + 1 = n by XREAL_1:235;
then
A3: (a * n * (n + 1)) / (n! * ((n + 1)!)) = (a * n * (n + 1)) / (n * ((n -'
1)!)* ((n + 1)!)) by NEWTON:15
.= (n * (a * (n + 1))) / (n * (((n -' 1)!)* ((n + 1)!)))
.= (a * (n + 1)) /(((n -' 1)!) * ((n + 1)!)) by A2,XCMPLX_1:91
.= (a * (n + 1)) / (((n -' 1)!) * ((n + 1) * (n!))) by NEWTON:15
.= (a * (n + 1)) / (((n -' 1)!) * (n!) * (n + 1))
.= a / ((n -' 1)! * (n!)) by XCMPLX_1:91;
n! > 0 & (n + 1)! > 0 by NEWTON:17;
then n! * ((n + 1)!) > 0 * (n!) by XREAL_1:68;
then (a * n * (n + 1)) / (n! * ((n + 1)!)) < b / (n! * ((n + 1)!)) by A2,Th6,
XREAL_1:74;
hence thesis by A2,A1,A3,Th8;
end;
theorem Th16:
for n being Nat holds Catalan (n) <= Catalan (n + 1)
proof
let n be Nat;
per cases by NAT_1:25;
suppose
n = 0;
hence thesis;
end;
suppose
n = 1;
hence thesis by Th11,Th12;
end;
suppose
n > 1;
hence thesis by Th15;
end;
end;
theorem
for n being Nat holds Catalan (n) >= 0;
theorem Th18:
for n being Nat holds Catalan (n) is Element of NAT
proof
let n be Nat;
Catalan (n) is Integer by Th13;
hence thesis by INT_1:3;
end;
theorem Th19:
for n being Nat st n > 0 holds Catalan (n+1) = 2 * (2
- (3 / (n + 1))) * Catalan (n)
proof
let n be Nat;
assume
A1: n > 0;
then
A2: n >= 1 + 0 by NAT_1:13;
then
A3: 2 * (n -' 1) = 2 * (n - 1) by XREAL_1:233
.= 2 * n - 2 * 1
.= 2 * n -' 2 by A2,XREAL_1:64,233;
A4: Catalan n = Catalan (n -' 1 + 1) by A2,XREAL_1:235
.= (2 * (n -' 1))! / ((n -' 1)! * ((n -' 1 + 1)!)) by Th14
.= (2 * n -' 2)! / ((n -' 1)! * (n!)) by A2,A3,XREAL_1:235;
A5: n -' 1 + 1 = n by A2,XREAL_1:235;
A6: 1 * 2 <= 2 * n by A2,XREAL_1:64;
then
A7: 2 * n -' 1 = 2 * n - 1 by XREAL_1:233,XXREAL_0:2;
A8: 2 * (2 - (3 / (n + 1))) = 2 * ((2 * (n + 1) / (n + 1) - (3 / (n + 1))))
by XCMPLX_1:89
.= 2 * ((2 * (n + 1) - 3) / (n + 1)) by XCMPLX_1:120
.= (2 * (2 * n - 1)) / (n + 1) by XCMPLX_1:74
.= ((2 * n -' 1) * 2 * n) / (n * (n + 1)) by A1,A7,XCMPLX_1:91
.= ((2 * n -' 1) * (2 * n)) / (n * (n + 1));
A9: 2 * n -' 1 + 1 = 2 * n by A6,XREAL_1:235,XXREAL_0:2;
1 < 2 * n by A6,XXREAL_0:2;
then
A10: 2 * n -' 2 + 1 = 2 * n -' 1 by Th4;
Catalan (n + 1) = (2*n)! / (n! * ((n+1)!)) by Th14
.= ((2*n -' 1)! * (2*n)) / (n! * ((n+1)!)) by A9,NEWTON:15
.= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * ((n+1)!)) by A10,NEWTON:15
.= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * (n! * (n+1))) by NEWTON:15
.= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * ((n -' 1)! * n * (n+1)))
by A5,NEWTON:15
.= ((2*n -' 2)! * ((2 * n -' 1) * (2*n))) / (n! * ((n -' 1)!) * (n * (n+
1)))
.= (Catalan n) * (((2 * n -' 1) * (2*n)) / (n * (n+1))) by A4,XCMPLX_1:76;
hence thesis by A8;
end;
registration
let n be Nat;
cluster Catalan n -> natural;
coherence by Th18;
end;
theorem Th20:
for n being Nat st n > 0 holds Catalan n > 0
proof
defpred P[Nat] means Catalan $1 > 0;
let n be Nat;
assume
A1: n > 0;
A2: for n being non zero Nat st P[n] holds P[n+1] by Th16;
A3: P[1] by Th11;
for n being non zero Nat holds P[n] from NAT_1:sch 10(A3,A2);
hence thesis by A1;
end;
registration
let n be non zero Nat;
cluster Catalan n -> non zero;
coherence by Th20;
end;
theorem
for n being Nat st n > 0 holds Catalan (n+1) < 4 * Catalan (n)
proof
let n be Nat;
assume
A1: n > 0;
then Catalan (n + 1) = 2 * (2 - (3 / (n + 1))) * Catalan (n) by Th19;
hence thesis by A1,Th7,XREAL_1:68;
end;