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