:: CATALAN1 semantic presentation begin theorem Th1: :: CATALAN1:1 for n being Nat st n > 1 holds n -' 1 <= (2 * n) -' 3 proof let n be Nat; ::_thesis: ( n > 1 implies n -' 1 <= (2 * n) -' 3 ) assume A1: n > 1 ; ::_thesis: n -' 1 <= (2 * n) -' 3 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 n -' 1 <= (2 * n) -' 3 by A1, A3, XREAL_1:233; ::_thesis: verum end; theorem Th2: :: CATALAN1:2 for n being Nat st n >= 1 holds n -' 1 <= (2 * n) -' 2 proof let n be Nat; ::_thesis: ( n >= 1 implies n -' 1 <= (2 * n) -' 2 ) assume A1: n >= 1 ; ::_thesis: n -' 1 <= (2 * n) -' 2 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, XREAL_1:233; n -' 1 = n - 1 by A1, XREAL_1:233; hence n -' 1 <= (2 * n) -' 2 by A2; ::_thesis: verum end; theorem Th3: :: CATALAN1:3 for n being Nat st n > 1 holds n < (2 * n) -' 1 proof let n be Nat; ::_thesis: ( n > 1 implies n < (2 * n) -' 1 ) assume A1: n > 1 ; ::_thesis: n < (2 * 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 n < (2 * n) -' 1 by A2, XREAL_1:233, XXREAL_0:2; ::_thesis: verum end; theorem Th4: :: CATALAN1:4 for n being Nat st n > 1 holds (n -' 2) + 1 = n -' 1 proof let n be Nat; ::_thesis: ( n > 1 implies (n -' 2) + 1 = n -' 1 ) assume n > 1 ; ::_thesis: (n -' 2) + 1 = 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 (n -' 2) + 1 = n -' 1 ; ::_thesis: verum end; theorem :: CATALAN1:5 for n being Nat st n > 1 holds (((4 * n) * n) - (2 * n)) / (n + 1) > 1 proof defpred S1[ Nat] means (((4 * $1) * $1) - (2 * $1)) / ($1 + 1) > 1; let n be Nat; ::_thesis: ( n > 1 implies (((4 * n) * n) - (2 * n)) / (n + 1) > 1 ) A1: for k being non trivial Nat st S1[k] holds S1[k + 1] proof let k be non trivial Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] 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 * (k + 1)) * (k + 1)) - (2 * (k + 1))) - ((k + 1) + 1)) + ((k + 1) + 1) > 0 + ((k + 1) + 1) by XREAL_1:8; then (((4 * (k + 1)) * (k + 1)) - (2 * (k + 1))) / ((k + 1) + 1) > ((k + 1) + 1) / ((k + 1) + 1) by XREAL_1:74; hence S1[k + 1] by XCMPLX_1:60; ::_thesis: verum end; assume n > 1 ; ::_thesis: (((4 * n) * n) - (2 * n)) / (n + 1) > 1 then A3: not n is trivial by NAT_2:28; A4: S1[2] ; for k being non trivial Nat holds S1[k] from NAT_2:sch_2(A4, A1); hence (((4 * n) * n) - (2 * n)) / (n + 1) > 1 by A3; ::_thesis: verum end; theorem Th6: :: CATALAN1:6 for n being Nat st n > 1 holds ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! proof let n be Nat; ::_thesis: ( n > 1 implies ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! ) assume A1: n > 1 ; ::_thesis: ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! 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 ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! by A5, A6, XREAL_1:98; ::_thesis: verum end; theorem Th7: :: CATALAN1:7 for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4 proof let n be Nat; ::_thesis: 2 * (2 - (3 / (n + 1))) < 4 assume 2 * (2 - (3 / (n + 1))) >= 4 ; ::_thesis: contradiction 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 contradiction by XREAL_1:139; ::_thesis: verum end; begin definition let n be Nat; func Catalan n -> Real equals :: CATALAN1:def 1 (((2 * n) -' 2) choose (n -' 1)) / n; coherence (((2 * n) -' 2) choose (n -' 1)) / n is Real ; end; :: deftheorem defines Catalan CATALAN1:def_1_:_ for n being Nat holds Catalan n = (((2 * n) -' 2) choose (n -' 1)) / n; theorem Th8: :: CATALAN1:8 for n being Nat st n > 1 holds Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) proof let n be Nat; ::_thesis: ( n > 1 implies Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) ) assume A1: n > 1 ; ::_thesis: Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) 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 Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) ; ::_thesis: verum end; theorem Th9: :: 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)) proof let n be Nat; ::_thesis: ( n > 1 implies Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) ) assume A1: n > 1 ; ::_thesis: Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (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, XCMPLX_1: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 Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) ; ::_thesis: verum end; theorem :: CATALAN1:10 Catalan 0 = 0 ; theorem Th11: :: CATALAN1:11 Catalan 1 = 1 proof Catalan 1 = ((2 * 1) -' 2) choose 0 by XREAL_1:232 .= 1 by NEWTON:19 ; hence Catalan 1 = 1 ; ::_thesis: verum end; theorem Th12: :: CATALAN1:12 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 Catalan 2 = 1 ; ::_thesis: verum end; theorem Th13: :: CATALAN1:13 for n being Nat holds Catalan n is Integer proof let n be Nat; ::_thesis: Catalan n is Integer percases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25; suppose n = 0 ; ::_thesis: Catalan n is Integer hence Catalan n is Integer ; ::_thesis: verum end; suppose n = 1 ; ::_thesis: Catalan n is Integer hence Catalan n is Integer ; ::_thesis: verum end; suppose n > 1 ; ::_thesis: Catalan n is Integer then Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) by Th9; hence Catalan n is Integer ; ::_thesis: verum end; end; end; theorem Th14: :: CATALAN1:14 for k being Nat holds Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !)) proof let k be Nat; ::_thesis: Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !)) 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 Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !)) ; ::_thesis: verum end; theorem Th15: :: CATALAN1:15 for n being Nat st n > 1 holds Catalan n < Catalan (n + 1) proof let n be Nat; ::_thesis: ( n > 1 implies Catalan n < Catalan (n + 1) ) set a = ((2 * n) -' 2) ! ; set b = (2 * n) ! ; A1: Catalan (n + 1) = ((2 * n) !) / ((n !) * ((n + 1) !)) by Th14; assume A2: n > 1 ; ::_thesis: Catalan n < Catalan (n + 1) then (n -' 1) + 1 = n by XREAL_1:235; then A3: (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n !) * ((n + 1) !)) = (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n * ((n -' 1) !)) * ((n + 1) !)) by NEWTON:15 .= (n * ((((2 * n) -' 2) !) * (n + 1))) / (n * (((n -' 1) !) * ((n + 1) !))) .= ((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) !)) by A2, XCMPLX_1:91 .= ((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) * (n !))) by NEWTON:15 .= ((((2 * n) -' 2) !) * (n + 1)) / ((((n -' 1) !) * (n !)) * (n + 1)) .= (((2 * n) -' 2) !) / (((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 (((((2 * n) -' 2) !) * n) * (n + 1)) / ((n !) * ((n + 1) !)) < ((2 * n) !) / ((n !) * ((n + 1) !)) by A2, Th6, XREAL_1:74; hence Catalan n < Catalan (n + 1) by A2, A1, A3, Th8; ::_thesis: verum end; theorem Th16: :: CATALAN1:16 for n being Nat holds Catalan n <= Catalan (n + 1) proof let n be Nat; ::_thesis: Catalan n <= Catalan (n + 1) percases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25; suppose n = 0 ; ::_thesis: Catalan n <= Catalan (n + 1) hence Catalan n <= Catalan (n + 1) ; ::_thesis: verum end; suppose n = 1 ; ::_thesis: Catalan n <= Catalan (n + 1) hence Catalan n <= Catalan (n + 1) by Th11, Th12; ::_thesis: verum end; suppose n > 1 ; ::_thesis: Catalan n <= Catalan (n + 1) hence Catalan n <= Catalan (n + 1) by Th15; ::_thesis: verum end; end; end; theorem :: CATALAN1:17 for n being Nat holds Catalan n >= 0 ; theorem Th18: :: CATALAN1:18 for n being Nat holds Catalan n is Element of NAT proof let n be Nat; ::_thesis: Catalan n is Element of NAT Catalan n is Integer by Th13; hence Catalan n is Element of NAT by INT_1:3; ::_thesis: verum end; theorem Th19: :: CATALAN1:19 for n being Nat st n > 0 holds Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) proof let n be Nat; ::_thesis: ( n > 0 implies Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) ) assume A1: n > 0 ; ::_thesis: Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) 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, XREAL_1: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 Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) by A8; ::_thesis: verum end; registration let n be Nat; cluster Catalan n -> natural ; coherence Catalan n is natural by Th18; end; theorem Th20: :: CATALAN1:20 for n being Nat st n > 0 holds Catalan n > 0 proof defpred S1[ Nat] means Catalan $1 > 0 ; let n be Nat; ::_thesis: ( n > 0 implies Catalan n > 0 ) assume A1: n > 0 ; ::_thesis: Catalan n > 0 A2: for n being non empty Nat st S1[n] holds S1[n + 1] by Th16; A3: S1[1] by Th11; for n being non empty Nat holds S1[n] from NAT_1:sch_10(A3, A2); hence Catalan n > 0 by A1; ::_thesis: verum end; registration let n be non empty Nat; cluster Catalan n -> non empty ; coherence not Catalan n is empty by Th20; end; theorem :: CATALAN1:21 for n being Nat st n > 0 holds Catalan (n + 1) < 4 * (Catalan n) proof let n be Nat; ::_thesis: ( n > 0 implies Catalan (n + 1) < 4 * (Catalan n) ) assume A1: n > 0 ; ::_thesis: Catalan (n + 1) < 4 * (Catalan n) then Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) by Th19; hence Catalan (n + 1) < 4 * (Catalan n) by A1, Th7, XREAL_1:68; ::_thesis: verum end;