let n be Nat; :: thesis: ( n > 1 implies ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! )
assume A1: n > 1 ; :: thesis: ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !
then A2: 2 * 1 < 2 * n by XREAL_1:68;
then A3: ((2 * n) -' 1) + 1 = 2 * n by XREAL_1:235, XXREAL_0:2;
2 - 1 < (2 * n) - 1 by A2, XREAL_1:9;
then A4: 1 < (2 * n) -' 1 by A2, XREAL_1:233, XXREAL_0:2;
((2 * n) -' 2) + 1 = (((2 * n) -' 1) -' 1) + 1 by NAT_D:45
.= (2 * n) -' 1 by A4, XREAL_1:235 ;
then A5: ((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n) = (((2 * n) -' 1) !) * (2 * n) by NEWTON:15
.= (2 * n) ! by A3, NEWTON:15 ;
((2 * n) -' 2) ! > 0 by NEWTON:17;
then A6: ( (((2 * n) -' 2) !) * n > 0 * n & (((2 * n) -' 2) !) * n < (((2 * n) -' 2) !) * ((2 * n) -' 1) ) by A1, Th3, XREAL_1:68;
n + 1 < n + n by A1, XREAL_1:6;
hence ((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) ! by A5, A6, XREAL_1:98; :: thesis: verum