let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies ( 1 < n + i & n + i <= 2 * n & n + i < ((n * n) + (3 * n)) + 1 ) )
assume that
A1: 1 <= i and
A2: i <= n ; :: thesis: ( 1 < n + i & n + i <= 2 * n & n + i < ((n * n) + (3 * n)) + 1 )
set ni = n + i;
1 <= n by A1, A2, XXREAL_0:2;
then 1 + 1 <= n + i by A1, XREAL_1:7;
hence 1 < n + i by NAT_1:13; :: thesis: ( n + i <= 2 * n & n + i < ((n * n) + (3 * n)) + 1 )
A3: n + i <= n + n by A2, XREAL_1:7;
hence n + i <= 2 * n ; :: thesis: n + i < ((n * n) + (3 * n)) + 1
2 * n < ((n * n) + (3 * n)) + 1 by Lm7;
hence n + i < ((n * n) + (3 * n)) + 1 by A3, XXREAL_0:2; :: thesis: verum