let i, j, n be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies ( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) ) )
assume that
A1: 1 <= i and
A2: i <= n and
A3: 1 <= j and
A4: j <= n ; :: thesis: ( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) )
set m3 = ((2 * n) + (n * i)) + j;
A5: ( ((2 * n) + (n * i)) + j = ((2 * n) + j) + (n * i) & n * i <= n * n ) by A2, XREAL_1:64;
n * 1 <= n * i by A1, XREAL_1:64;
then (2 * n) + n <= (2 * n) + (n * i) by XREAL_1:7;
hence (3 * n) + 1 <= ((2 * n) + (n * i)) + j by A3, XREAL_1:7; :: thesis: ((2 * n) + (n * i)) + j <= (n * n) + (3 * n)
(2 * n) + n = (2 + 1) * n ;
then (2 * n) + j <= 3 * n by A4, XREAL_1:7;
hence ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) by A5, XREAL_1:7; :: thesis: verum