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;