let n be natural number ; :: 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: (n -' 1) + 1 = n by XREAL_1:237;
A4: 1 * 2 <= 2 * n by A2, XREAL_1:66;
then A5: 1 < 2 * n by XXREAL_0:2;
A6: (2 * n) -' 1 = (2 * n) - 1 by A4, XREAL_1:235, XXREAL_0:2;
A7: ((2 * n) -' 2) + 1 = (2 * n) -' 1 by A5, Th4;
A8: ((2 * n) -' 1) + 1 = 2 * n by A4, XREAL_1:237, XXREAL_0:2;
A9: 2 * (n -' 1) = 2 * (n - 1) by A2, XREAL_1:235
.= (2 * n) - (2 * 1)
.= (2 * n) -' 2 by A2, XREAL_1:66, XREAL_1:235 ;
A10: Catalan n = Catalan ((n -' 1) + 1) by A2, XREAL_1:237
.= ((2 * (n -' 1)) ! ) / (((n -' 1) ! ) * (((n -' 1) + 1) ! )) by Th14
.= (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )) by A2, A9, XREAL_1:237 ;
A11: 2 * (2 - (3 / (n + 1))) = 2 * (((2 * (n + 1)) / (n + 1)) - (3 / (n + 1))) by XCMPLX_1:90
.= 2 * (((2 * (n + 1)) - 3) / (n + 1)) by XCMPLX_1:121
.= (2 * ((2 * n) - 1)) / (n + 1) by XCMPLX_1:75
.= ((((2 * n) -' 1) * 2) * n) / (n * (n + 1)) by A1, A6, XCMPLX_1:92
.= (((2 * n) -' 1) * (2 * n)) / (n * (n + 1)) ;
Catalan (n + 1) = ((2 * n) ! ) / ((n ! ) * ((n + 1) ! )) by Th14
.= ((((2 * n) -' 1) ! ) * (2 * n)) / ((n ! ) * ((n + 1) ! )) by A8, NEWTON:21
.= (((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((n + 1) ! )) by A7, NEWTON:21
.= (((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((n ! ) * (n + 1))) by NEWTON:21
.= (((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((((n -' 1) ! ) * n) * (n + 1))) by A3, NEWTON:21
.= ((((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 A10, XCMPLX_1:77 ;
hence Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) by A11; :: thesis: verum