:: Catalan Numbers
:: by Dorota Cz\c{e}stochowska and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: CATALAN1:1
for n being Nat st n > 1 holds
n -' 1 <= (2 * n) -' 3
proofend;

theorem Th2: :: CATALAN1:2
for n being Nat st n >= 1 holds
n -' 1 <= (2 * n) -' 2
proofend;

theorem Th3: :: CATALAN1:3
for n being Nat st n > 1 holds
n < (2 * n) -' 1
proofend;

theorem Th4: :: CATALAN1:4
for n being Nat st n > 1 holds
(n -' 2) + 1 = n -' 1
proofend;

theorem :: CATALAN1:5
for n being Nat st n > 1 holds
(((4 * n) * n) - (2 * n)) / (n + 1) > 1
proofend;

theorem Th6: :: CATALAN1:6
for n being Nat st n > 1 holds
((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !
proofend;

theorem Th7: :: CATALAN1:7
for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4
proofend;

begin

definition
let n be Nat;
func Catalan n ->  Real equals :: CATALAN1:def 1
(((2 * n) -' 2) choose (n -' 1)) / n;
coherence
 (((2 * n) -' 2) choose (n -' 1)) / n is Real ;
end;

:: deftheorem  defines Catalan CATALAN1:def_1_:_
 for n being Nat holds Catalan n = (((2 * n) -' 2) choose (n -' 1)) / n;

theorem Th8: :: CATALAN1:8
for n being Nat st n > 1 holds
Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !))
proofend;

theorem Th9: :: CATALAN1:9
for n being Nat st n > 1 holds
Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))
proofend;

theorem :: CATALAN1:10
Catalan 0 = 0 ;

theorem Th11: :: CATALAN1:11
Catalan 1 = 1
proofend;

theorem Th12: :: CATALAN1:12
Catalan 2 = 1
proofend;

theorem Th13: :: CATALAN1:13
for n being Nat holds Catalan n is Integer
proofend;

theorem Th14: :: CATALAN1:14
for k being Nat holds Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !))
proofend;

theorem Th15: :: CATALAN1:15
for n being Nat st n > 1 holds
Catalan n < Catalan (n + 1)
proofend;

theorem Th16: :: CATALAN1:16
for n being Nat holds Catalan n <= Catalan (n + 1)
proofend;

theorem :: CATALAN1:17
for n being Nat holds Catalan n >= 0 ;

theorem Th18: :: CATALAN1:18
for n being Nat holds Catalan n is Element of NAT
proofend;

theorem Th19: :: CATALAN1:19
for n being Nat st n > 0 holds
Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n)
proofend;

registration
let n be Nat;
cluster Catalan n ->  natural ;
coherence
 Catalan n is natural by Th18;
end;

theorem Th20: :: CATALAN1:20
for n being Nat st n > 0 holds
Catalan n > 0
proofend;

registration
let n be non empty Nat;
cluster Catalan n ->  non empty ;
coherence
 not Catalan n is empty by Th20;
end;

theorem :: CATALAN1:21
for n being Nat st n > 0 holds
Catalan (n + 1) < 4 * (Catalan n)
proofend;