let k be Nat; ( 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 )
; 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 A14:
n <> 0
;
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
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 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
t <> 0
;
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
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;
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 )
;
verum end; end;