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

theorem Th1: :: CATALAN1:1

for n being Nat st n > 1 holds
n -' 1 <= (2 * n) -' 3

proof end;

theorem Th2: :: CATALAN1:2

for n being Nat st n >= 1 holds
n -' 1 <= (2 * n) -' 2

proof end;

theorem Th3: :: CATALAN1:3

for n being Nat st n > 1 holds
n < (2 * n) -' 1

proof end;

theorem Th4: :: CATALAN1:4

for n being Nat st n > 1 holds
(n -' 2) + 1 = n -' 1

proof end;

theorem :: CATALAN1:5

for n being Nat st n > 1 holds
(((4 * n) * n) - (2 * n)) / (n + 1) > 1

proof end;

theorem Th6: :: CATALAN1:6

for n being Nat st n > 1 holds
((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !

proof end;

theorem Th7: :: CATALAN1:7

for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4

proof end;

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 !))

proof end;

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))

proof end;

theorem :: CATALAN1:10

Catalan 0 = 0 ;

theorem Th11: :: CATALAN1:11

Catalan 1 = 1

proof end;

theorem Th12: :: CATALAN1:12

Catalan 2 = 1

proof end;

theorem Th13: :: CATALAN1:13

for n being Nat holds Catalan n is Integer

proof end;

theorem Th14: :: CATALAN1:14

for k being Nat holds Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !))

proof end;

theorem Th15: :: CATALAN1:15

for n being Nat st n > 1 holds
Catalan n < Catalan (n + 1)

proof end;

theorem Th16: :: CATALAN1:16

for n being Nat holds Catalan n <= Catalan (n + 1)

proof end;

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

proof end;

theorem Th19: :: CATALAN1:19

for n being Nat st n > 0 holds
Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n)

proof end;

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

proof end;

registration

let n be non zero Nat;

cluster Catalan n -> non zero ;

coherence
not Catalan n is zero by Th20;

end;

theorem :: CATALAN1:21

for n being Nat st n > 0 holds
Catalan (n + 1) < 4 * (Catalan n)

proof end;