let f be non constant standard special_circular_sequence; :: thesis: LSeg (((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|),(((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|) misses L~ f
A1:
1 <= width (GoB f)
by GOBOARD7:35;
now let p be
Point of
(TOP-REAL 2);
:: thesis: ( p in LSeg (((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|),(((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|) implies p `2 < ((GoB f) * 1,1) `2 )assume A2:
p in LSeg (((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|),
(((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|)
;
:: thesis: p `2 < ((GoB f) * 1,1) `2 A3:
1
< len (GoB f)
by GOBOARD7:34;
then A4:
((len (GoB f)) -' 1) + 1
= len (GoB f)
by XREAL_1:237;
then A5:
1
<= (len (GoB f)) -' 1
by A3, NAT_1:13;
(len (GoB f)) -' 1
<= len (GoB f)
by A4, NAT_1:11;
then A6:
((GoB f) * ((len (GoB f)) -' 1),1) `2 = ((GoB f) * 1,1) `2
by A1, A5, GOBOARD5:2;
A7:
((GoB f) * (len (GoB f)),1) `2 = ((GoB f) * 1,1) `2
by A1, A3, GOBOARD5:2;
(((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|) `2 =
(((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) `2 ) - (|[0 ,1]| `2 )
by TOPREAL3:8
.=
((1 / 2) * ((((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1)) `2 )) - (|[0 ,1]| `2 )
by TOPREAL3:9
.=
((1 / 2) * ((((GoB f) * 1,1) `2 ) + (((GoB f) * 1,1) `2 ))) - (|[0 ,1]| `2 )
by A6, A7, TOPREAL3:7
.=
(1 * (((GoB f) * 1,1) `2 )) - 1
by EUCLID:56
;
then A8:
((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]| = |[((((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|) `1 ),((((GoB f) * 1,1) `2 ) - 1)]|
by EUCLID:57;
(((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|) `2 =
(((GoB f) * 1,1) `2 ) + (|[1,(- 1)]| `2 )
by A7, TOPREAL3:7
.=
(((GoB f) * 1,1) `2 ) + (- 1)
by EUCLID:56
.=
(((GoB f) * 1,1) `2 ) - 1
;
then
((GoB f) * (len (GoB f)),1) + |[1,(- 1)]| = |[((((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|) `1 ),((((GoB f) * 1,1) `2 ) - 1)]|
by EUCLID:57;
then
p `2 = (((GoB f) * 1,1) `2 ) - 1
by A2, A8, TOPREAL3:18;
hence
p `2 < ((GoB f) * 1,1) `2
by XREAL_1:46;
:: thesis: verum end;
hence
LSeg (((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),1) + ((GoB f) * (len (GoB f)),1))) - |[0 ,1]|),(((GoB f) * (len (GoB f)),1) + |[1,(- 1)]|) misses L~ f
by Th23; :: thesis: verum