let n be natural number ; :: thesis: ( n > 1 implies Catalan n < Catalan (n + 1) )
assume A1: n > 1 ; :: thesis: Catalan n < Catalan (n + 1)
A2: Catalan (n + 1) = ((2 * n) ! ) / ((n ! ) * ((n + 1) ! )) by Th14;
A3: n ! > 0 by NEWTON:23;
(n + 1) ! > 0 by NEWTON:23;
then A4: (n ! ) * ((n + 1) ! ) > 0 * (n ! ) by A3, XREAL_1:70;
set a = ((2 * n) -' 2) ! ;
set b = (2 * n) ! ;
((((2 * n) -' 2) ! ) * n) * (n + 1) < (2 * n) ! by A1, Th6;
then A5: (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n ! ) * ((n + 1) ! )) < ((2 * n) ! ) / ((n ! ) * ((n + 1) ! )) by A4, XREAL_1:76;
(n -' 1) + 1 = n by A1, XREAL_1:237;
then (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n ! ) * ((n + 1) ! )) = (((((2 * n) -' 2) ! ) * n) * (n + 1)) / ((n * ((n -' 1) ! )) * ((n + 1) ! )) by NEWTON:21
.= (n * ((((2 * n) -' 2) ! ) * (n + 1))) / (n * (((n -' 1) ! ) * ((n + 1) ! )))
.= ((((2 * n) -' 2) ! ) * (n + 1)) / (((n -' 1) ! ) * ((n + 1) ! )) by A1, XCMPLX_1:92
.= ((((2 * n) -' 2) ! ) * (n + 1)) / (((n -' 1) ! ) * ((n + 1) * (n ! ))) by NEWTON:21
.= ((((2 * n) -' 2) ! ) * (n + 1)) / ((((n -' 1) ! ) * (n ! )) * (n + 1))
.= (((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )) by XCMPLX_1:92 ;
hence Catalan n < Catalan (n + 1) by A1, A2, A5, Th8; :: thesis: verum