let i, j, n be Nat; for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
let G be Go-board; ( [i,j] in Indices G & [i,(j + n)] in Indices G implies dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) )
assume that
A1:
[i,j] in Indices G
and
A2:
[i,(j + n)] in Indices G
; dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
set x = G * (i,j);
set y = G * (i,(j + n));
per cases
( n = 0 or n <> 0 )
;
suppose A3:
n <> 0
;
dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)A4:
j + n <= width G
by A2, MATRIX_0:32;
A5:
( 1
<= i &
i <= len G )
by A1, MATRIX_0:32;
A6:
1
<= j + n
by A2, MATRIX_0:32;
A7:
1
<= j
by A1, MATRIX_0:32;
1
<= n
by A3, NAT_1:14;
then
j < j + n
by NAT_1:19;
then
(G * (i,j)) `2 < (G * (i,(j + n))) `2
by A4, A7, A5, GOBOARD5:4;
then A8:
((G * (i,j)) `2) - ((G * (i,j)) `2) < ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
by XREAL_1:14;
j <= width G
by A1, MATRIX_0:32;
then A9:
(G * (i,j)) `1 =
(G * (i,1)) `1
by A7, A5, GOBOARD5:2
.=
(G * (i,(j + n))) `1
by A6, A4, A5, GOBOARD5:2
;
thus dist (
(G * (i,j)),
(G * (i,(j + n)))) =
sqrt (((((G * (i,j)) `1) - ((G * (i,(j + n))) `1)) ^2) + ((((G * (i,j)) `2) - ((G * (i,(j + n))) `2)) ^2))
by TOPREAL6:92
.=
|.(((G * (i,j)) `2) - ((G * (i,(j + n))) `2)).|
by A9, COMPLEX1:72
.=
|.(- (((G * (i,j)) `2) - ((G * (i,(j + n))) `2))).|
by COMPLEX1:52
.=
((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
by A8, ABSVALUE:def 1
;
verum end;