let i be Nat; for G being Go-board st 1 <= i & i + 1 <= len G holds
((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| in Int (cell (G,i,0))
let G be Go-board; ( 1 <= i & i + 1 <= len G implies ((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| in Int (cell (G,i,0)) )
assume that
A1:
1 <= i
and
A2:
i + 1 <= len G
; ((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| in Int (cell (G,i,0))
set r1 = (G * (i,1)) `1 ;
set s1 = (G * (i,1)) `2 ;
set r2 = (G * ((i + 1),1)) `1 ;
width G <> 0
by MATRIX_0:def 10;
then A3:
1 <= width G
by NAT_1:14;
width G <> 0
by MATRIX_0:def 10;
then A4:
1 <= width G
by NAT_1:14;
i < i + 1
by XREAL_1:29;
then A5:
(G * (i,1)) `1 < (G * ((i + 1),1)) `1
by A1, A2, A4, GOBOARD5:3;
then
((G * (i,1)) `1) + ((G * (i,1)) `1) < ((G * (i,1)) `1) + ((G * ((i + 1),1)) `1)
by XREAL_1:6;
then A6:
(1 / 2) * (((G * (i,1)) `1) + ((G * (i,1)) `1)) < (1 / 2) * (((G * (i,1)) `1) + ((G * ((i + 1),1)) `1))
by XREAL_1:68;
i < len G
by A2, NAT_1:13;
then A7:
(G * (1,1)) `2 = (G * (i,1)) `2
by A1, A3, GOBOARD5:1;
then
(G * (i,1)) `2 < ((G * (1,1)) `2) + 1
by XREAL_1:29;
then A8:
((G * (i,1)) `2) - 1 < (G * (1,1)) `2
by XREAL_1:19;
1 <= i + 1
by NAT_1:11;
then
(G * (1,1)) `2 = (G * ((i + 1),1)) `2
by A2, A3, GOBOARD5:1;
then
( G * (i,1) = |[((G * (i,1)) `1),((G * (i,1)) `2)]| & G * ((i + 1),1) = |[((G * ((i + 1),1)) `1),((G * (i,1)) `2)]| )
by A7, EUCLID:53;
then
( (1 / 2) * (((G * (i,1)) `2) + ((G * (i,1)) `2)) = (G * (i,1)) `2 & (G * (i,1)) + (G * ((i + 1),1)) = |[(((G * (i,1)) `1) + ((G * ((i + 1),1)) `1)),(((G * (i,1)) `2) + ((G * (i,1)) `2))]| )
by EUCLID:56;
then
(1 / 2) * ((G * (i,1)) + (G * ((i + 1),1))) = |[((1 / 2) * (((G * (i,1)) `1) + ((G * ((i + 1),1)) `1))),((G * (i,1)) `2)]|
by EUCLID:58;
then A9: ((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| =
|[(((1 / 2) * (((G * (i,1)) `1) + ((G * ((i + 1),1)) `1))) - 0),(((G * (i,1)) `2) - 1)]|
by EUCLID:62
.=
|[((1 / 2) * (((G * (i,1)) `1) + ((G * ((i + 1),1)) `1))),(((G * (i,1)) `2) - 1)]|
;
((G * (i,1)) `1) + ((G * ((i + 1),1)) `1) < ((G * ((i + 1),1)) `1) + ((G * ((i + 1),1)) `1)
by A5, XREAL_1:6;
then A10:
(1 / 2) * (((G * (i,1)) `1) + ((G * ((i + 1),1)) `1)) < (1 / 2) * (((G * ((i + 1),1)) `1) + ((G * ((i + 1),1)) `1))
by XREAL_1:68;
i < len G
by A2, NAT_1:13;
then
Int (cell (G,i,0)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & s < (G * (1,1)) `2 ) }
by A1, Th24;
hence
((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| in Int (cell (G,i,0))
by A9, A6, A10, A8; verum