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