let n, i be Nat; :: thesis: ( n >= 2 & i >= 1 implies (n + i) ! > (n !) + i )
assume ( n >= 2 & i >= 1 ) ; :: thesis: (n + i) ! > (n !) + i

per cases then ( ( n >= 2 & i > 1 ) or ( n >= 2 & i = 1 ) ) by XXREAL_0:1;

suppose ( n >= 2 & i > 1 ) ; :: thesis: (n + i) ! > (n !) + i

per cases then ( ( n > 2 & i > 1 ) or ( n = 2 & i > 1 ) ) by XXREAL_0:1;

suppose A1: ( n > 2 & i > 1 ) ; :: thesis: (n + i) ! > (n !) + i

then A2: i >= 1 + 1 by NAT_1:13;
A3: (n + i) ! >= (n !) * (i !) by NEWTON04:70;
( n ! > 1 & i ! > 1 ) by A2, A1, ASYMPT_1:55;
then A5: (n !) * (i !) >= (n !) + (i !) by Th1;

per cases ( i = 2 or i > 2 ) by A2, XXREAL_0:1;

suppose A6: i = 2 ; :: thesis: (n + i) ! > (n !) + i

n > 1 by A1, XXREAL_0:2;
hence (n + i) ! > (n !) + i by A6, Th6; :: thesis: verum

end;

suppose i > 2 ; :: thesis: (n + i) ! > (n !) + i

then A7: i >= 2 + 1 by NAT_1:13;
i ! > i by ASYMPT_1:59, A7;
then (n !) + (i !) > (n !) + i by XREAL_1:6;
then (n !) * (i !) > (n !) + i by A5, XXREAL_0:2;
hence (n + i) ! > (n !) + i by A3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose A8: ( n = 2 & i > 1 ) ; :: thesis: (n + i) ! > (n !) + i

then 2 + i >= 2 + 1 by XREAL_1:7;
hence (n + i) ! > (n !) + i by A8, NEWTON:14, ASYMPT_1:59; :: thesis: verum

end;

end;

end;

suppose ( n >= 2 & i = 1 ) ; :: thesis: (n + i) ! > (n !) + i

hence (n + i) ! > (n !) + i by Th5; :: thesis: verum

end;

end;