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

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