let i, n, j be Element of NAT ; :: thesis: ( 1 <= i & i <= n & j <= n implies ( 1 < ((2 * n) + (n * i)) + j & i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 ) )
assume A1: ( 1 <= i & i <= n & j <= n ) ; :: thesis: ( 1 < ((2 * n) + (n * i)) + j & i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )
set m3 = ((2 * n) + (n * i)) + j;
A2: ((2 * n) + (n * i)) + j = (2 * n) + ((n * i) + j) ;
A3: 1 <= n by A1, XXREAL_0:2;
then 2 * 1 <= 2 * n by XREAL_1:66;
then A4: 1 < 2 * n by XXREAL_0:2;
2 * n <= ((2 * n) + (n * i)) + j by A2, NAT_1:12;
hence 1 < ((2 * n) + (n * i)) + j by A4, XXREAL_0:2; :: thesis: ( i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )
1 * i <= n * i by A3, XREAL_1:66;
then A5: 1 + i < (2 * n) + (n * i) by A4, XREAL_1:10;
(2 * n) + (n * i) <= ((2 * n) + (n * i)) + j by NAT_1:12;
then 1 + i < ((2 * n) + (n * i)) + j by A5, XXREAL_0:2;
hence i < ((2 * n) + (n * i)) + j by NAT_1:13; :: thesis: ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1
(2 * n) + n = (2 + 1) * n ;
then A6: (2 * n) + j <= 3 * n by A1, XREAL_1:9;
A7: ((2 * n) + (n * i)) + j = ((2 * n) + j) + (n * i) ;
n * i <= n * n by A1, XREAL_1:66;
then ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) by A6, A7, XREAL_1:9;
hence ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 by NAT_1:13; :: thesis: verum