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