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

end;

:: deftheorem Def1 defines Catalan CATALAN1:def 1 :

theorem Th8: :: CATALAN1:8

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

proof end;

theorem Th9: :: CATALAN1:9

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

proof end;

theorem Th10: :: CATALAN1:10

Catalan 0 = 0 ;

theorem Th11: :: CATALAN1:11

proof end;

theorem Th12: :: CATALAN1:12

proof end;

theorem Th13: :: CATALAN1:13

for b₁ being natural number holds Catalan b₁ is Integer

proof end;

theorem Th14: :: CATALAN1:14

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

proof end;

theorem Th15: :: CATALAN1:15

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

proof end;

theorem Th16: :: CATALAN1:16

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

proof end;

theorem Th17: :: CATALAN1:17

for b₁ being natural number holds Catalan b₁ >= 0 ;

theorem Th18: :: CATALAN1:18

for b₁ being natural number holds Catalan b₁ is Nat

proof end;

theorem Th19: :: CATALAN1:19

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

proof end;

registration

let c₁ be natural number ;
cluster Catalan a₁ -> natural ;
coherence by Th18;

end;

theorem Th20: :: CATALAN1:20

for b₁ being natural number st b₁ > 0 holds
Catalan b₁ > 0

proof end;

registration

let c₁ be non empty natural number ;
cluster Catalan a₁ -> non empty natural ;
coherence by Th20;

end;

theorem Th21: :: CATALAN1:21

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

proof end;