let k be Nat; :: thesis: ( 1 <= k & k <= 128 implies ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) )
assume A1: ( 1 <= k & k <= 128 ) ; :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
A3: k = (32 * (k div 32)) + (k mod 32) by NAT_D:2;
reconsider m = k div 32 as Nat ;
reconsider n = k mod 32 as Nat ;
k div 32 <= (32 * 4) div 32 by A1, NAT_2:24;
then M1: m <= 4 by NAT_D:18;
per cases ( n = 0 or n <> 0 ) ;
suppose A4: n = 0 ; :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
A5: 1 <= m
proof
assume not 1 <= m ; :: thesis: contradiction
then m = 0 by NAT_1:14;
hence contradiction by A1, A3, A4; :: thesis: verum
end;
set j = m;
A8: m in Seg 4 by M1, A5;
set i = 4;
A10: 4 in Seg 4 ;
A11: m -' 1 = m - 1 by XREAL_1:233, A5;
A13: k = (32 * (k div 32)) + (k mod 32) by NAT_D:2
.= (32 * (m -' 1)) + (8 * ((4 - 1) + 1)) by A4, A11
.= (32 * (m -' 1)) + (8 * ((4 -' 1) + 1)) by XREAL_1:233
.= ((1 + ((4 -' 1) * 8)) + ((m -' 1) * 32)) + 7 ;
((1 + ((4 -' 1) * 8)) + ((m -' 1) * 32)) + 0 <= ((1 + ((4 -' 1) * 8)) + ((m -' 1) * 32)) + 7 by XREAL_1:7;
hence ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by A8, A10, A13; :: thesis: verum
end;
suppose A14: n <> 0 ; :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
then XX0: 1 <= n by NAT_1:14;
XX1: n <= 32 by NAT_D:1;
m <> 4
proof
assume U1: m = 4 ; :: thesis: contradiction
U2: k = (32 * 4) + n by NAT_D:2, U1
.= 128 + n ;
128 + 1 <= 128 + n by XX0, XREAL_1:7;
hence contradiction by U2, XXREAL_0:2, A1; :: thesis: verum
end;
then m < 4 by XXREAL_0:1, M1;
then A15: m + 1 <= 4 by NAT_1:13;
A16: 1 <= m + 1 by NAT_1:11;
set j = m + 1;
A18: m + 1 in Seg 4 by A15, A16;
A19: (m + 1) -' 1 = (m + 1) - 1 by XREAL_1:233, NAT_1:11
.= m ;
A20: k = (32 * ((m + 1) -' 1)) + n by NAT_D:2, A19;
A22: n = (8 * (n div 8)) + (n mod 8) by NAT_D:2;
reconsider s = n div 8 as Nat ;
reconsider t = n mod 8 as Nat ;
n div 8 <= (8 * 4) div 8 by XX1, NAT_2:24;
then M2: n div 8 <= 4 by NAT_D:18;
now :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
per cases ( t = 0 or t <> 0 ) ;
suppose A23: t = 0 ; :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
A24: 1 <= s
proof
assume not 1 <= s ; :: thesis: contradiction
then n = (8 * 0) + 0 by NAT_1:14, A22, A23;
hence contradiction by A14; :: thesis: verum
end;
set i = s;
A28: s in Seg 4 by M2, A24;
A29: s -' 1 = s - 1 by XREAL_1:233, A24;
A30: n = (8 * s) + 0 by NAT_D:2, A23
.= (8 * (s -' 1)) + (8 * 1) by A29 ;
((1 + ((s -' 1) * 8)) + (((m + 1) -' 1) * 32)) + 0 <= ((1 + ((s -' 1) * 8)) + (((m + 1) -' 1) * 32)) + 7 by XREAL_1:7;
hence ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by A28, A18, A20, A30; :: thesis: verum
end;
suppose t <> 0 ; :: thesis: ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 )
then XX0: 1 <= t by NAT_1:14;
XXX1: t <= 8 by NAT_D:1;
s <> 4
proof
assume U1: s = 4 ; :: thesis: contradiction
U2: n = (8 * 4) + t by NAT_D:2, U1
.= 32 + t ;
32 + 1 <= 32 + t by XX0, XREAL_1:7;
hence contradiction by U2, XXREAL_0:2, XX1; :: thesis: verum
end;
then s < 4 by XXREAL_0:1, M2;
then B15: s + 1 <= 4 by NAT_1:13;
B16: 1 <= s + 1 by NAT_1:11;
set i = s + 1;
B18: s + 1 in Seg 4 by B15, B16;
B19: (s + 1) -' 1 = (s + 1) - 1 by XREAL_1:233, NAT_1:11
.= s ;
B20: n = (8 * ((s + 1) -' 1)) + t by NAT_D:2, B19;
B220: ((32 * ((m + 1) -' 1)) + (8 * ((s + 1) -' 1))) + 1 <= ((32 * ((m + 1) -' 1)) + (8 * ((s + 1) -' 1))) + t by XX0, XREAL_1:7;
((32 * ((m + 1) -' 1)) + (8 * ((s + 1) -' 1))) + t <= ((32 * ((m + 1) -' 1)) + (8 * ((s + 1) -' 1))) + 8 by XXX1, XREAL_1:7;
then k <= ((1 + (8 * ((s + 1) -' 1))) + (32 * ((m + 1) -' 1))) + 7 by A20, B20;
hence ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by B220, A20, B20, B18, A18; :: thesis: verum
end;
end;
end;
hence ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) ; :: thesis: verum
end;
end;