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