:: CATALAN1 semantic presentation

theorem Th1: :: CATALAN1:1

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

proof end;

theorem Th2: :: CATALAN1:2

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

proof end;

theorem Th3: :: CATALAN1:3

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

proof end;

theorem Th4: :: CATALAN1:4

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

proof end;

Lm1: for a, b being natural number st a < b & 1 < b holds
a -' 1 < b -' 1

proof end;

theorem :: CATALAN1:5

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

proof end;

theorem Th6: :: CATALAN1:6

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

proof end;

theorem Th7: :: CATALAN1:7

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

proof end;

definition

let n be natural number ;
func Catalan n -> Real equals :: CATALAN1:def 1
(((2 * n) -' 2) choose (n -' 1)) / n;
coherence by XREAL_0:def 1;

end;

:: deftheorem defines Catalan CATALAN1:def 1 :

theorem Th8: :: CATALAN1:8

for n being natural number st n > 1 holds
Catalan n = (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! ))

proof end;

theorem Th9: :: CATALAN1:9

for n being natural number st n > 1 holds
Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))

proof end;

theorem Th10: :: 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 natural number holds Catalan n is Integer

proof end;

theorem Th14: :: CATALAN1:14

for k being natural number st k >= 1 holds
Catalan (k + 1) = ((2 * k) ! ) / ((k ! ) * ((k + 1) ! ))

proof end;

theorem Th15: :: CATALAN1:15

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

proof end;

theorem Th16: :: CATALAN1:16

for n being natural number holds Catalan n <= Catalan (n + 1)

proof end;

theorem :: CATALAN1:17

for n being natural number holds Catalan n >= 0 ;

theorem Th18: :: CATALAN1:18

for n being natural number holds Catalan n is Nat

proof end;

theorem Th19: :: CATALAN1:19

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

proof end;

registration

let n be natural number ;
cluster Catalan n -> natural ;
coherence by Th18;

end;

theorem Th20: :: CATALAN1:20

for n being natural number st n > 0 holds
Catalan n > 0

proof end;

registration

let n be non empty natural number ;
cluster Catalan n -> non empty natural ;
coherence by Th20;

end;

theorem :: CATALAN1:21

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

proof end;