let n be natural number ; :: 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:66;
A3: (n -' 1) + 1 = n by A1, XREAL_1:237;
A4: n -' 1 <= (2 * n) -' 2 by A1, Th2;
((2 * n) -' 2) - (n -' 1) = ((2 * n) -' 2) - (n - 1) by A1, XREAL_1:235
.= ((2 * n) - 2) - (n - 1) by A2, XREAL_1:235
.= n -' 1 by A1, XREAL_1:235 ;
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:79
.= (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (((n -' 1) ! ) * n))
.= (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )) by A3, NEWTON:21 ;
hence Catalan n = (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )) ; :: thesis: verum