:: Catalan Numbers :: by Dorota Cz\c{e}stochowska and Adam Grabowski :: :: Received May 31, 2004 :: Copyright (c) 2004-2017 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, BOOLE, SUBSET, ARITHM; theorems NAT_1, XCMPLX_1, NAT_2, NEWTON, INT_1, XREAL_1, XXREAL_0, NAT_D; schemes NAT_2, NAT_1; begin :: Preliminaries theorem Th1: for n being Nat st n > 1 holds n -' 1 <= 2 * n -' 3 proof let n be Nat; assume A1: n > 1; then n -' 1 > 1 -' 1 by NAT_D:57; then A2: n -' 1 + n > 0 + n by XREAL_1:6; 2 * 1 < 2 * n by A1,XREAL_1:68; then 2 + 1 <= 2 * n by NAT_1:13; then A3: 2 * n -' 3 = 2 * n - 3 by XREAL_1:233; n -' 1 = n - 1 by A1,XREAL_1:233; then 2 * n - 1 - 1 > n - 1 by A2,XREAL_1:9; then 2 * n - 2 - 1 >= n - 1 by INT_1:52; hence thesis by A1,A3,XREAL_1:233; end; theorem Th2: for n being Nat st n >= 1 holds n -' 1 <= 2 * n -' 2 proof let n be Nat; assume A1: n >= 1; then 2 * 1 <= 2 * n by XREAL_1:64; then A2: 1 * (n -' 1) <= 2 * (n -' 1) & 2 * n -' 2 = 2 * n - 2 by XREAL_1:64,233; n -' 1 = n - 1 by A1,XREAL_1:233; hence thesis by A2; end; theorem Th3: for n being Nat st n > 1 holds n < 2 * n -' 1 proof let n be Nat; assume A1: n > 1; then n + n > n + 1 by XREAL_1:6; then A2: n + n - 1 > n + 1 - 1 by XREAL_1:9; 1 * 2 < 2 * n by A1,XREAL_1:68; hence thesis by A2,XREAL_1:233,XXREAL_0:2; end; theorem Th4: for n being Nat st n > 1 holds n -' 2 + 1 = n -' 1 proof let n be Nat; assume n > 1; then A1: n -' 1 >= 1 by NAT_D:49; n -' 2 + 1 = n -' 1 -' 1 + 1 by NAT_D:45 .= n -' 1 by A1,XREAL_1:235; hence thesis; end; theorem for n being Nat st n > 1 holds (4 * n * n - 2*n) / (n + 1) > 1 proof defpred P[Nat] means (4 * \$1 * \$1 - 2*\$1)/(\$1 + 1) > 1; let n be Nat; A1: for k be non trivial Nat st P[k] holds P[k + 1] proof let k be non trivial Nat such that A2: P[k]; set k1 = k+1; (4 * k * k - 2*k) / (k + 1) = (4 * k * k - 2*k) * ( 1/ (k + 1)) by XCMPLX_1:99; then (4 * k * k - 2*k) * (1 / (k + 1)) * (k + 1) > 1 * (k + 1) by A2, XREAL_1:68; then (4 * k * k - 2*k) > 1 * (k + 1) by XCMPLX_1:109; then (4 * k * k - 2*k)-(k + 1) > 0 by XREAL_1:50; then (4 * k * k - 3*k - 1) + (8 * k + 1) > 0 + 0; then (4 * k1 * k1 - 2*k1 - (k1 + 1)) + (k1 + 1) > 0 + (k1 + 1) by XREAL_1:8 ; then (4 * k1 * k1 - 2 * k1) / (k1 + 1) > (k1 + 1) / (k1 + 1) by XREAL_1:74; hence thesis by XCMPLX_1:60; end; assume n > 1; then A3: n is non trivial by NAT_2:28; A4: P[2]; for k be non trivial Nat holds P[k] from NAT_2:sch 2 (A4, A1); hence thesis by A3; end; theorem Th6: for n being Nat st n > 1 holds (2 * n -' 2)! * n * (n + 1) < (2 * n)! proof let n be Nat; assume A1: n > 1; then A2: 2 * 1 < 2 * n by XREAL_1:68; then A3: 2 * n -' 1 + 1 = 2 * n by XREAL_1:235,XXREAL_0:2; 2 - 1 < 2 * n - 1 by A2,XREAL_1:9; then A4: 1 < 2 * n -' 1 by A2,XREAL_1:233,XXREAL_0:2; 2 * n -' 2 + 1 = 2 * n -' 1 -' 1 + 1 by NAT_D:45 .= 2 * n -' 1 by A4,XREAL_1:235; then A5: (2 * n -' 2)! * (2 * n -' 1) * (2 * n) = (2 * n -' 1)! * (2 * n) by NEWTON:15 .= (2 * n)! by A3,NEWTON:15; (2 * n -' 2)! > 0 by NEWTON:17; then A6: (2 * n -' 2)! * n > 0 * n & (2 * n -' 2)! * n < (2 * n -' 2)! * (2 * n -' 1) by A1,Th3,XREAL_1:68; n + 1 < n + n by A1,XREAL_1:6; hence thesis by A5,A6,XREAL_1:98; end; theorem Th7: for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4 proof let n be Nat; assume 2 * (2 - (3 / (n + 1))) >= 4; then 2 * (2 - (3 / (n + 1))) / 2 >= 4 / 2 by XREAL_1:72; then 2 - (3 / (n + 1)) - 2 >= 2 - 2 by XREAL_1:9; then --- (3 / (n + 1)) >= 0; hence thesis by XREAL_1:139; end; begin :: Catalan Numbers definition let n be Nat; func Catalan (n) -> Real equals ((2*n -' 2) choose (n -' 1)) / n; coherence; end; theorem Th8: for n being Nat st n > 1 holds Catalan (n) = (2 * n -' 2)! / ((n -' 1)! * (n!)) proof let n be Nat; assume A1: n > 1; then A2: 2 * 1 <= 2 * n by XREAL_1:64; A3: n -' 1 + 1 = n by A1,XREAL_1:235; A4: n -' 1 <= 2 * n -' 2 by A1,Th2; (2*n -' 2) - (n -' 1) = (2*n -' 2) - (n - 1) by A1,XREAL_1:233 .= (2*n - 2) - (n - 1) by A2,XREAL_1:233 .= n -' 1 by A1,XREAL_1:233; then ((2*n -' 2) choose (n -' 1)) = ((2*n -' 2)!) / ((n -' 1)! * ((n -' 1)!)) by A4,NEWTON:def 3; then Catalan (n) = ((2*n -' 2)!) / ((n -' 1)! * ((n -' 1)!) * n) by XCMPLX_1:78 .= ((2*n -' 2)!) / ((n -' 1)! * (((n -' 1)!) * n)) .= ((2*n -' 2)!) / ((n -' 1)! * (n!)) by A3,NEWTON:15; hence thesis; end; theorem Th9: for n being Nat st n > 1 holds Catalan n = 4 * ((2*n -' 3) choose (n -' 1)) - ((2*n -' 1) choose (n -' 1)) proof let n be Nat; assume A1: n > 1; then A2: n -' 1 <= 2 * n -' 3 by Th1; A3: 2 * 1 <= 2 * n by A1,XREAL_1:64; then A4: 2 * n -' 2 = 2 * n - 2 by XREAL_1:233; A5: 1 + 1 <= n by A1,NAT_1:13; then A6: 2 * 2 <= 2 * n by XREAL_1:64; then 2 * n -' 3 = 2 * n - 3 by XREAL_1:233,XXREAL_0:2; then A7: 2 * n -' 3 + 1 = 2 * n - 2 .= 2 * n -' 2 by A3,XREAL_1:233; (2*n -' 3) - (n -' 1) = (2*n -' 3) - (n - 1) by A1,XREAL_1:233 .= (2*n - 3) - (n - 1) by A6,XREAL_1:233,XXREAL_0:2 .= n - 2 .= n -' 2 by A5,XREAL_1:233; then ((2*n -' 3) choose (n -' 1)) = ((2*n -' 3)!) / ((n -' 1)! * ((n -' 2)!)) by A2,NEWTON:def 3; then A8: 4 * ((2*n -' 3) choose (n -' 1)) = (4 * ((2*n -' 3)!)) / ((n -' 1)! * (( n -' 2)!)) by XCMPLX_1:74; A9: n -' 2 + 1 = n -' 1 by A1,Th4; A10: n -' 1 = n - 1 by A1,XREAL_1:233; then A11: n -' 1 + 1 = n; A12: 1 * n < 2 * n by A1,XREAL_1:68; then A13: 2 * n -' 1 = 2 * n - 1 by A1,XREAL_1:233,XXREAL_0:2; 1 < 2 * n by A1,A12,XXREAL_0:2; then A14: 2 * n -' 2 + 1 = 2 * n -' 1 by Th4; 1 < 2 * n by A1,A12,XXREAL_0:2; then A15: n -' 1 < 2 * n -' 1 by A12,NAT_D:57; 2 * n -' 1 - (n -' 1) = 2 * n -' 1 - (n - 1) by A1,XREAL_1:233 .= 2 * n -' 1 - n + 1 .= 2 * n - 1 - n + 1 by A1,A12,XREAL_1:233,XXREAL_0:2 .= n; then (2*n -' 1) choose (n -' 1) = ((2*n -' 1)!) / ((n -' 1)! * (n!)) by A15, NEWTON:def 3; then A16: (2*n -' 1) choose (n -' 1) = ((2*n -' 2)! * (2*n -' 1)) / ((n -' 1)! * (n!)) by A14,NEWTON:15; n - 1 > 0 by A1,XREAL_1:50; then 4 * ((2*n -' 3) choose (n -' 1)) = ((n * (n - 1)) * (4 * ((2*n -' 3)!)) ) / (((n * (n - 1)) * ((n -' 1)! * ((n -' 2)!)))) by A1,A8,XCMPLX_1:6,91 .= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n - 1) * (n * ((n -' 1)!)) * ((n -' 2)!))) .= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n - 1) * (n!) * ((n -' 2)! ))) by A11,NEWTON:15 .= (((n - 1) * n) * (4 * ((2*n -' 3)!))) / (((n!) * ((n -' 1) * ((n -' 2 )!)))) by A10 .= (2 * n * ((2 * n -' 2) * ((2*n -' 3)!))) / (((n!) * ((n -' 1)!))) by A4 ,A9,NEWTON:15 .= (2 * n * ((2*n -' 2)!)) / (((n!) * ((n -' 1)!))) by A7,NEWTON:15; then 4 * ((2*n -' 3) choose (n -' 1)) - ((2*n -' 1) choose (n -' 1)) = ((2 * n * ((2*n -' 2)!)) - ((2*n -' 2)! * (2*n -' 1))) / (((n!) * ((n -' 1)!))) by A16,XCMPLX_1:120 .= Catalan n by A1,A13,Th8; hence thesis; end; theorem Catalan 0 = 0; theorem Th11: Catalan 1 = 1 proof Catalan 1 = (2*1 -' 2) choose 0 by XREAL_1:232 .= 1 by NEWTON:19; hence thesis; end; theorem Th12: Catalan 2 = 1 proof A1: 4 -' 2 = 4 - 2 by XREAL_1:233 .= 2; 2 -' 1 = 2 - 1 by XREAL_1:233 .= 1; then Catalan 2 = 2 / 2 by A1,NEWTON:23 .= 1; hence thesis; end; theorem Th13: for n being Nat holds Catalan (n) is Integer proof let n be Nat; per cases by NAT_1:25; suppose n = 0; hence thesis; end; suppose n = 1; hence thesis; end; suppose n > 1; then Catalan n = 4 * ((2*n -' 3) choose (n -' 1)) - ((2*n -' 1) choose (n -' 1)) by Th9; hence thesis; end; end; theorem Th14: for k being Nat holds Catalan (k + 1) = (2*k)! / (k! * ((k+1)!)) proof let k be Nat; reconsider l = 2*k - k as Nat; l = k & 1*k <= 2*k by XREAL_1:64; then A1: (2*k) choose k = (2*k!)/((k!) * (k!)) by NEWTON:def 3; 2*k + 2 -' 2 = 2*k & k + 1 -' 1 = k by NAT_D:34; then Catalan (k+1) = (2*k!) / ((k!) * (k!) * (k+1)) by A1,XCMPLX_1:78 .= (2*k!) / ((k!) * ((k!) * (k+1))) .= (2*k!) / ((k!) * ((k+1)!)) by NEWTON:15; hence thesis; end; theorem Th15: for n being Nat st n > 1 holds Catalan (n) < Catalan (n + 1) proof let n be Nat; set a = (2 * n -' 2)!; set b = (2 * n)!; A1: Catalan (n + 1) = (2*n)! / (n! * ((n+1)!)) by Th14; assume A2: n > 1; then n -' 1 + 1 = n by XREAL_1:235; then A3: (a * n * (n + 1)) / (n! * ((n + 1)!)) = (a * n * (n + 1)) / (n * ((n -' 1)!)* ((n + 1)!)) by NEWTON:15 .= (n * (a * (n + 1))) / (n * (((n -' 1)!)* ((n + 1)!))) .= (a * (n + 1)) /(((n -' 1)!) * ((n + 1)!)) by A2,XCMPLX_1:91 .= (a * (n + 1)) / (((n -' 1)!) * ((n + 1) * (n!))) by NEWTON:15 .= (a * (n + 1)) / (((n -' 1)!) * (n!) * (n + 1)) .= a / ((n -' 1)! * (n!)) by XCMPLX_1:91; n! > 0 & (n + 1)! > 0 by NEWTON:17; then n! * ((n + 1)!) > 0 * (n!) by XREAL_1:68; then (a * n * (n + 1)) / (n! * ((n + 1)!)) < b / (n! * ((n + 1)!)) by A2,Th6, XREAL_1:74; hence thesis by A2,A1,A3,Th8; end; theorem Th16: for n being Nat holds Catalan (n) <= Catalan (n + 1) proof let n be Nat; per cases by NAT_1:25; suppose n = 0; hence thesis; end; suppose n = 1; hence thesis by Th11,Th12; end; suppose n > 1; hence thesis by Th15; end; end; theorem for n being Nat holds Catalan (n) >= 0; theorem Th18: for n being Nat holds Catalan (n) is Element of NAT proof let n be Nat; Catalan (n) is Integer by Th13; hence thesis by INT_1:3; end; theorem Th19: for n being Nat st n > 0 holds Catalan (n+1) = 2 * (2 - (3 / (n + 1))) * Catalan (n) proof let n be Nat; assume A1: n > 0; then A2: n >= 1 + 0 by NAT_1:13; then A3: 2 * (n -' 1) = 2 * (n - 1) by XREAL_1:233 .= 2 * n - 2 * 1 .= 2 * n -' 2 by A2,XREAL_1:64,233; A4: Catalan n = Catalan (n -' 1 + 1) by A2,XREAL_1:235 .= (2 * (n -' 1))! / ((n -' 1)! * ((n -' 1 + 1)!)) by Th14 .= (2 * n -' 2)! / ((n -' 1)! * (n!)) by A2,A3,XREAL_1:235; A5: n -' 1 + 1 = n by A2,XREAL_1:235; A6: 1 * 2 <= 2 * n by A2,XREAL_1:64; then A7: 2 * n -' 1 = 2 * n - 1 by XREAL_1:233,XXREAL_0:2; A8: 2 * (2 - (3 / (n + 1))) = 2 * ((2 * (n + 1) / (n + 1) - (3 / (n + 1)))) by XCMPLX_1:89 .= 2 * ((2 * (n + 1) - 3) / (n + 1)) by XCMPLX_1:120 .= (2 * (2 * n - 1)) / (n + 1) by XCMPLX_1:74 .= ((2 * n -' 1) * 2 * n) / (n * (n + 1)) by A1,A7,XCMPLX_1:91 .= ((2 * n -' 1) * (2 * n)) / (n * (n + 1)); A9: 2 * n -' 1 + 1 = 2 * n by A6,XREAL_1:235,XXREAL_0:2; 1 < 2 * n by A6,XXREAL_0:2; then A10: 2 * n -' 2 + 1 = 2 * n -' 1 by Th4; Catalan (n + 1) = (2*n)! / (n! * ((n+1)!)) by Th14 .= ((2*n -' 1)! * (2*n)) / (n! * ((n+1)!)) by A9,NEWTON:15 .= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * ((n+1)!)) by A10,NEWTON:15 .= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * (n! * (n+1))) by NEWTON:15 .= ((2*n -' 2)! * (2 * n -' 1) * (2*n)) / (n! * ((n -' 1)! * n * (n+1))) by A5,NEWTON:15 .= ((2*n -' 2)! * ((2 * n -' 1) * (2*n))) / (n! * ((n -' 1)!) * (n * (n+ 1))) .= (Catalan n) * (((2 * n -' 1) * (2*n)) / (n * (n+1))) by A4,XCMPLX_1:76; hence thesis by A8; end; registration let n be Nat; cluster Catalan n -> natural; coherence by Th18; end; theorem Th20: for n being Nat st n > 0 holds Catalan n > 0 proof defpred P[Nat] means Catalan \$1 > 0; let n be Nat; assume A1: n > 0; A2: for n being non zero Nat st P[n] holds P[n+1] by Th16; A3: P[1] by Th11; for n being non zero Nat holds P[n] from NAT_1:sch 10(A3,A2); hence thesis by A1; end; registration let n be non zero Nat; cluster Catalan n -> non zero; coherence by Th20; end; theorem for n being Nat st n > 0 holds Catalan (n+1) < 4 * Catalan (n) proof let n be Nat; assume A1: n > 0; then Catalan (n + 1) = 2 * (2 - (3 / (n + 1))) * Catalan (n) by Th19; hence thesis by A1,Th7,XREAL_1:68; end;