:: Catalan Numbers
:: by Dorota Cz\c{e}stochowska and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2021 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;
begin :: Preliminaries
theorem :: CATALAN1:1
for n being Nat st n > 1 holds n -' 1 <= 2 * n -' 3;
theorem :: CATALAN1:2
for n being Nat st n >= 1 holds n -' 1 <= 2 * n -' 2;
theorem :: CATALAN1:3
for n being Nat st n > 1 holds n < 2 * n -' 1;
theorem :: CATALAN1:4
for n being Nat st n > 1 holds n -' 2 + 1 = n -' 1;
theorem :: CATALAN1:5
for n being Nat st n > 1 holds (4 * n * n - 2*n) / (n + 1) > 1;
theorem :: CATALAN1:6
for n being Nat st n > 1 holds (2 * n -' 2)! * n * (n
+ 1) < (2 * n)!;
theorem :: CATALAN1:7
for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4;
begin :: Catalan Numbers
definition
let n be Nat;
func Catalan (n) -> Real equals
:: CATALAN1:def 1
((2*n -' 2) choose (n -' 1)) / n;
end;
theorem :: CATALAN1:8
for n being Nat st n > 1 holds Catalan (n) = (2 * n -'
2)! / ((n -' 1)! * (n!));
theorem :: 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));
theorem :: CATALAN1:10
Catalan 0 = 0;
theorem :: CATALAN1:11
Catalan 1 = 1;
theorem :: CATALAN1:12
Catalan 2 = 1;
theorem :: CATALAN1:13
for n being Nat holds Catalan (n) is Integer;
theorem :: CATALAN1:14
for k being Nat holds Catalan (k + 1) = (2*k)! / (k! * ((k+1)!));
theorem :: CATALAN1:15
for n being Nat st n > 1 holds Catalan (n) < Catalan (n + 1);
theorem :: CATALAN1:16
for n being Nat holds Catalan (n) <= Catalan (n + 1);
theorem :: CATALAN1:17
for n being Nat holds Catalan (n) >= 0;
theorem :: CATALAN1:18
for n being Nat holds Catalan (n) is Element of NAT;
theorem :: CATALAN1:19
for n being Nat st n > 0 holds Catalan (n+1) = 2 * (2
- (3 / (n + 1))) * Catalan (n);
registration
let n be Nat;
cluster Catalan n -> natural;
end;
theorem :: CATALAN1:20
for n being Nat st n > 0 holds Catalan n > 0;
registration
let n be non zero Nat;
cluster Catalan n -> non zero;
end;
theorem :: CATALAN1:21
for n being Nat st n > 0 holds Catalan (n+1) < 4 * Catalan (n);