let n be natural number ; :: 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:70;
then 2 - 1 < (2 * n) - 1 by XREAL_1:11;
then A3: 1 < (2 * n) -' 1 by A2, XREAL_1:235, XXREAL_0:2;
A4: ((2 * n) -' 2) + 1 = (((2 * n) -' 1) -' 1) + 1 by NAT_D:45
.= (2 * n) -' 1 by A3, XREAL_1:237 ;
A5: ((2 * n) -' 1) + 1 = 2 * n by A2, XREAL_1:237, XXREAL_0:2;
A6: ((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n) = (((2 * n) -' 1) ! ) * (2 * n) by A4, NEWTON:21
.= (2 * n) ! by A5, NEWTON:21 ;
A7: n + 1 < n + n by A1, XREAL_1:8;
A8: ((2 * n) -' 2) ! > 0 by NEWTON:23;
then A9: (((2 * n) -' 2) ! ) * n > 0 * n by A1, XREAL_1:70;
(((2 * n) -' 2) ! ) * n < (((2 * n) -' 2) ! ) * ((2 * n) -' 1) by A1, A8, Th3, XREAL_1:70;
hence ((((2 * n) -' 2) ! ) * n) * (n + 1) < (2 * n) ! by A6, A7, A9, XREAL_1:100; :: thesis: verum