let f be non constant standard special_circular_sequence; :: thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f
let j be Element of NAT ; :: thesis: ( 1 <= j & j + 2 <= width (GoB f) implies LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f )
assume A1:
( 1 <= j & j + 2 <= width (GoB f) )
; :: thesis: LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f
A2:
1 <= len (GoB f)
by GOBOARD7:34;
now let p be
Point of
(TOP-REAL 2);
:: thesis: ( p in LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) implies p `1 < ((GoB f) * 1,1) `1 )assume A3:
p in LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),
(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|)
;
:: thesis: p `1 < ((GoB f) * 1,1) `1 A4:
j <= j + 2
by NAT_1:11;
then
j <= width (GoB f)
by A1, XXREAL_0:2;
then A5:
((GoB f) * 1,j) `1 = ((GoB f) * 1,1) `1
by A1, A2, GOBOARD5:3;
j + 1
<= j + 2
by XREAL_1:8;
then
( 1
<= j + 1 &
j + 1
<= width (GoB f) )
by A1, NAT_1:11, XXREAL_0:2;
then A6:
((GoB f) * 1,(j + 1)) `1 = ((GoB f) * 1,1) `1
by A2, GOBOARD5:3;
1
<= j + 2
by A1, A4, XXREAL_0:2;
then A7:
((GoB f) * 1,(j + 2)) `1 = ((GoB f) * 1,1) `1
by A1, A2, GOBOARD5:3;
(((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|) `1 =
(((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) `1 ) - (|[1,0 ]| `1 )
by TOPREAL3:8
.=
((1 / 2) * ((((GoB f) * 1,j) + ((GoB f) * 1,(j + 1))) `1 )) - (|[1,0 ]| `1 )
by TOPREAL3:9
.=
((1 / 2) * ((((GoB f) * 1,1) `1 ) + (((GoB f) * 1,1) `1 ))) - (|[1,0 ]| `1 )
by A5, A6, TOPREAL3:7
.=
(1 * (((GoB f) * 1,1) `1 )) - 1
by EUCLID:56
;
then A8:
((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]| = |[((((GoB f) * 1,1) `1 ) - 1),((((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|) `2 )]|
by EUCLID:57;
(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) `1 =
(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) `1 ) - (|[1,0 ]| `1 )
by TOPREAL3:8
.=
((1 / 2) * ((((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2))) `1 )) - (|[1,0 ]| `1 )
by TOPREAL3:9
.=
((1 / 2) * ((((GoB f) * 1,1) `1 ) + (((GoB f) * 1,1) `1 ))) - (|[1,0 ]| `1 )
by A6, A7, TOPREAL3:7
.=
(1 * (((GoB f) * 1,1) `1 )) - 1
by EUCLID:56
;
then
((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]| = |[((((GoB f) * 1,1) `1 ) - 1),((((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) `2 )]|
by EUCLID:57;
then
p `1 = (((GoB f) * 1,1) `1 ) - 1
by A3, A8, TOPREAL3:17;
hence
p `1 < ((GoB f) * 1,1) `1
by XREAL_1:46;
:: thesis: verum end;
hence
LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f
by Th21; :: thesis: verum