let i, j, n be 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 that
A1: 1 <= i and
A2: i <= n and
A3: 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 )
A4: 1 <= n by A1, A2, XXREAL_0:2;
then 2 * 1 <= 2 * n by XREAL_1:64;
then A5: 1 < 2 * n by XXREAL_0:2;
set m3 = ((2 * n) + (n * i)) + j;
A6: ( ((2 * n) + (n * i)) + j = ((2 * n) + j) + (n * i) & n * i <= n * n ) by A2, XREAL_1:64;
((2 * n) + (n * i)) + j = (2 * n) + ((n * i) + j) ;
then 2 * n <= ((2 * n) + (n * i)) + j by NAT_1:12;
hence 1 < ((2 * n) + (n * i)) + j by A5, XXREAL_0:2; :: thesis: ( i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )
A7: (2 * n) + (n * i) <= ((2 * n) + (n * i)) + j by NAT_1:12;
1 * i <= n * i by A4, XREAL_1:64;
then 1 + i < (2 * n) + (n * i) by A5, XREAL_1:8;
then 1 + i < ((2 * n) + (n * i)) + j by A7, 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 (2 * n) + j <= 3 * n by A3, XREAL_1:7;
then ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) by A6, XREAL_1:7;
hence ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 by NAT_1:13; :: thesis: verum