let n, i be Nat; :: thesis: ( n >= 1 & i >= 1 implies (n + i) ! >= (n !) + i )
assume ( n >= 1 & i >= 1 ) ; :: thesis: (n + i) ! >= (n !) + i
per cases then ( ( n >= 1 & i > 1 ) or ( n >= 1 & i = 1 ) ) by XXREAL_0:1;
suppose ( n >= 1 & i > 1 ) ; :: thesis: (n + i) ! >= (n !) + i
per cases then ( ( n > 1 & i > 1 ) or ( n = 1 & i > 1 ) ) by XXREAL_0:1;
suppose ( n > 1 & i > 1 ) ; :: thesis: (n + i) ! >= (n !) + i
hence (n + i) ! >= (n !) + i by Th7; :: thesis: verum
end;
suppose ( n = 1 & i > 1 ) ; :: thesis: (n + i) ! >= (n !) + i
hence (n + i) ! >= (n !) + i by NEWTON:13, NEWTON:38; :: thesis: verum
end;
end;
end;
suppose ( n >= 1 & i = 1 ) ; :: thesis: (n + i) ! >= (n !) + i
hence (n + i) ! >= (n !) + i by Th4; :: thesis: verum
end;
end;