let n be natural number ; :: 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: 1 + 1 <= n by A1, NAT_1:13;
then A4: 2 * 2 <= 2 * n by XREAL_1:66;
((2 * n) -' 3) - (n -' 1) = ((2 * n) -' 3) - (n - 1) by A1, XREAL_1:235
.= ((2 * n) - 3) - (n - 1) by A4, XREAL_1:235, XXREAL_0:2
.= n - 2
.= n -' 2 by A3, XREAL_1:235 ;
then ((2 * n) -' 3) choose (n -' 1) = (((2 * n) -' 3) ! ) / (((n -' 1) ! ) * ((n -' 2) ! )) by A2, NEWTON:def 3;
then A5: 4 * (((2 * n) -' 3) choose (n -' 1)) = (4 * (((2 * n) -' 3) ! )) / (((n -' 1) ! ) * ((n -' 2) ! )) by XCMPLX_1:75;
A6: 1 * n < 2 * n by A1, XREAL_1:70;
then 1 < 2 * n by A1, XXREAL_0:2;
then A7: n -' 1 < (2 * n) -' 1 by A6, NAT_D:57;
((2 * n) -' 1) - (n -' 1) = ((2 * n) -' 1) - (n - 1) by A1, XREAL_1:235
.= (((2 * n) -' 1) - n) + 1
.= (((2 * n) - 1) - n) + 1 by A1, A6, XREAL_1:235, XXREAL_0:2
.= n ;
then A8: ((2 * n) -' 1) choose (n -' 1) = (((2 * n) -' 1) ! ) / (((n -' 1) ! ) * (n ! )) by A7, NEWTON:def 3;
A9: n - 1 > 0 by A1, XREAL_1:52;
A10: n -' 1 = n - 1 by A1, XREAL_1:235;
A11: 2 * 1 <= 2 * n by A1, XREAL_1:66;
then A12: (2 * n) -' 2 = (2 * n) - 2 by XREAL_1:235;
A13: (n -' 1) + 1 = n by A10;
A14: 1 < 2 * n by A1, A6, XXREAL_0:2;
A15: (2 * n) -' 1 = (2 * n) - 1 by A1, A6, XREAL_1:235, XXREAL_0:2;
A16: (n -' 2) + 1 = n -' 1 by A1, Th4;
(2 * n) -' 3 = (2 * n) - 3 by A4, XREAL_1:235, XXREAL_0:2;
then A17: ((2 * n) -' 3) + 1 = (2 * n) - 2
.= (2 * n) -' 2 by A11, XREAL_1:235 ;
A18: ((2 * n) -' 2) + 1 = (2 * n) -' 1 by A14, Th4;
A19: 4 * (((2 * n) -' 3) choose (n -' 1)) = ((n * (n - 1)) * (4 * (((2 * n) -' 3) ! ))) / ((n * (n - 1)) * (((n -' 1) ! ) * ((n -' 2) ! ))) by A1, A5, A9, XCMPLX_1:6, XCMPLX_1:92
.= (((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 A13, NEWTON:21
.= (((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 A12, A16, NEWTON:21
.= ((2 * n) * (((2 * n) -' 2) ! )) / ((n ! ) * ((n -' 1) ! )) by A17, NEWTON:21 ;
((2 * n) -' 1) choose (n -' 1) = ((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) / (((n -' 1) ! ) * (n ! )) by A8, A18, NEWTON:21;
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 A19, XCMPLX_1:121
.= Catalan n by A1, A15, Th8 ;
hence Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) ; :: thesis: verum