let f be non constant standard special_circular_sequence; (S-min (L~ f)) `1 < (S-max (L~ f)) `1
set p = S-min (L~ f);
set i = (S-min (L~ f)) .. f;
A1:
len f > 3 + 1
by GOBOARD7:36;
A2:
len f >= 1 + 1
by GOBOARD7:36, XXREAL_0:2;
A3:
S-min (L~ f) in rng f
by Th45;
then A4:
(S-min (L~ f)) .. f in dom f
by FINSEQ_4:30;
then A5:
( 1 <= (S-min (L~ f)) .. f & (S-min (L~ f)) .. f <= len f )
by FINSEQ_3:27;
A6: S-min (L~ f) =
f . ((S-min (L~ f)) .. f)
by A3, FINSEQ_4:29
.=
f /. ((S-min (L~ f)) .. f)
by A4, PARTFUN1:def 8
;
A7:
(S-min (L~ f)) `2 = S-bound (L~ f)
by EUCLID:56;
per cases
( (S-min (L~ f)) .. f = 1 or (S-min (L~ f)) .. f = len f or ( 1 < (S-min (L~ f)) .. f & (S-min (L~ f)) .. f < len f ) )
by A5, XXREAL_0:1;
suppose A8:
(
(S-min (L~ f)) .. f = 1 or
(S-min (L~ f)) .. f = len f )
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 then
S-min (L~ f) = f /. 1
by A6, FINSEQ_6:def 1;
then A9:
S-min (L~ f) in LSeg f,1
by A2, TOPREAL1:27;
A10:
1
+ 1
in dom f
by A2, FINSEQ_3:27;
then A11:
f /. (1 + 1) in L~ f
by A1, GOBOARD1:16, XXREAL_0:2;
A12:
f /. (1 + 1) in LSeg f,1
by A2, TOPREAL1:27;
A13:
((len f) -' 1) + 1
= len f
by A1, XREAL_1:237, XXREAL_0:2;
then
(len f) -' 1
> 3
by A1, XREAL_1:8;
then A14:
(len f) -' 1
> 1
by XXREAL_0:2;
then A15:
f /. ((len f) -' 1) in LSeg f,
((len f) -' 1)
by A13, TOPREAL1:27;
(len f) -' 1
<= len f
by A13, NAT_1:11;
then A16:
(len f) -' 1
in dom f
by A14, FINSEQ_3:27;
then A17:
f /. ((len f) -' 1) in L~ f
by A1, GOBOARD1:16, XXREAL_0:2;
A18:
f /. 1
= f /. (len f)
by FINSEQ_6:def 1;
then A19:
S-min (L~ f) in LSeg f,
((len f) -' 1)
by A6, A8, A13, A14, TOPREAL1:27;
A20:
1
in dom f
by FINSEQ_5:6;
then A21:
S-min (L~ f) <> f /. (1 + 1)
by A6, A8, A18, A10, GOBOARD7:31;
A22:
len f in dom f
by FINSEQ_5:6;
then A23:
S-min (L~ f) <> f /. ((len f) -' 1)
by A6, A8, A18, A13, A16, GOBOARD7:31;
A24:
( not
LSeg f,
((len f) -' 1) is
vertical or not
LSeg f,1 is
vertical )
proof
assume
(
LSeg f,
((len f) -' 1) is
vertical &
LSeg f,1 is
vertical )
;
contradiction
then A25:
(
(S-min (L~ f)) `1 = (f /. (1 + 1)) `1 &
(S-min (L~ f)) `1 = (f /. ((len f) -' 1)) `1 )
by A19, A9, A15, A12, SPPOL_1:def 3;
A26:
(
(f /. (1 + 1)) `2 <= (f /. ((len f) -' 1)) `2 or
(f /. (1 + 1)) `2 >= (f /. ((len f) -' 1)) `2 )
;
A27:
(
(S-min (L~ f)) `2 <= (f /. (1 + 1)) `2 &
(S-min (L~ f)) `2 <= (f /. ((len f) -' 1)) `2 )
by A7, A17, A11, PSCOMP_1:71;
(
LSeg f,1
= LSeg (f /. 1),
(f /. (1 + 1)) &
LSeg f,
((len f) -' 1) = LSeg (f /. 1),
(f /. ((len f) -' 1)) )
by A2, A18, A13, A14, TOPREAL1:def 5;
then
(
f /. ((len f) -' 1) in LSeg f,1 or
f /. (1 + 1) in LSeg f,
((len f) -' 1) )
by A6, A8, A18, A25, A27, A26, GOBOARD7:8;
then
(
f /. ((len f) -' 1) in (LSeg f,((len f) -' 1)) /\ (LSeg f,1) or
f /. (1 + 1) in (LSeg f,((len f) -' 1)) /\ (LSeg f,1) )
by A15, A12, XBOOLE_0:def 4;
then A28:
(LSeg f,((len f) -' 1)) /\ (LSeg f,1) <> {(f /. 1)}
by A6, A8, A18, A23, A21, TARSKI:def 1;
f . 1
= f /. 1
by A20, PARTFUN1:def 8;
hence
contradiction
by A28, JORDAN4:54;
verum
end; now per cases
( LSeg f,((len f) -' 1) is horizontal or LSeg f,1 is horizontal )
by A24, SPPOL_1:41;
suppose
LSeg f,
((len f) -' 1) is
horizontal
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 then A29:
(S-min (L~ f)) `2 = (f /. ((len f) -' 1)) `2
by A19, A15, SPPOL_1:def 2;
then A30:
f /. ((len f) -' 1) in S-most (L~ f)
by A2, A7, A16, Th15, GOBOARD1:16;
then A31:
(f /. ((len f) -' 1)) `1 >= (S-min (L~ f)) `1
by PSCOMP_1:118;
(f /. ((len f) -' 1)) `1 <> (S-min (L~ f)) `1
by A6, A8, A22, A18, A13, A16, A29, GOBOARD7:31, TOPREAL3:11;
then A32:
(f /. ((len f) -' 1)) `1 > (S-min (L~ f)) `1
by A31, XXREAL_0:1;
(f /. ((len f) -' 1)) `1 <= (S-max (L~ f)) `1
by A30, PSCOMP_1:118;
hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
by A32, XXREAL_0:2;
verum end; suppose
LSeg f,1 is
horizontal
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 then A33:
(S-min (L~ f)) `2 = (f /. (1 + 1)) `2
by A9, A12, SPPOL_1:def 2;
then A34:
f /. (1 + 1) in S-most (L~ f)
by A2, A7, A10, Th15, GOBOARD1:16;
then A35:
(f /. (1 + 1)) `1 >= (S-min (L~ f)) `1
by PSCOMP_1:118;
(f /. (1 + 1)) `1 <> (S-min (L~ f)) `1
by A6, A8, A20, A18, A10, A33, GOBOARD7:31, TOPREAL3:11;
then A36:
(f /. (1 + 1)) `1 > (S-min (L~ f)) `1
by A35, XXREAL_0:1;
(f /. (1 + 1)) `1 <= (S-max (L~ f)) `1
by A34, PSCOMP_1:118;
hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
by A36, XXREAL_0:2;
verum end; hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
;
verum end; suppose that A37:
1
< (S-min (L~ f)) .. f
and A38:
(S-min (L~ f)) .. f < len f
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 A39:
(((S-min (L~ f)) .. f) -' 1) + 1
= (S-min (L~ f)) .. f
by A37, XREAL_1:237;
then A40:
((S-min (L~ f)) .. f) -' 1
>= 1
by A37, NAT_1:13;
then A41:
f /. (((S-min (L~ f)) .. f) -' 1) in LSeg f,
(((S-min (L~ f)) .. f) -' 1)
by A38, A39, TOPREAL1:27;
((S-min (L~ f)) .. f) -' 1
<= (S-min (L~ f)) .. f
by A39, NAT_1:11;
then
((S-min (L~ f)) .. f) -' 1
<= len f
by A38, XXREAL_0:2;
then A42:
((S-min (L~ f)) .. f) -' 1
in dom f
by A40, FINSEQ_3:27;
then A43:
f /. (((S-min (L~ f)) .. f) -' 1) in L~ f
by A1, GOBOARD1:16, XXREAL_0:2;
A44:
((S-min (L~ f)) .. f) + 1
<= len f
by A38, NAT_1:13;
then A45:
f /. (((S-min (L~ f)) .. f) + 1) in LSeg f,
((S-min (L~ f)) .. f)
by A37, TOPREAL1:27;
((S-min (L~ f)) .. f) + 1
>= 1
by NAT_1:11;
then A46:
((S-min (L~ f)) .. f) + 1
in dom f
by A44, FINSEQ_3:27;
then A47:
f /. (((S-min (L~ f)) .. f) + 1) in L~ f
by A1, GOBOARD1:16, XXREAL_0:2;
A48:
S-min (L~ f) <> f /. (((S-min (L~ f)) .. f) + 1)
by A3, A6, A46, FINSEQ_4:30, GOBOARD7:31;
A49:
S-min (L~ f) in LSeg f,
((S-min (L~ f)) .. f)
by A6, A37, A44, TOPREAL1:27;
A50:
S-min (L~ f) in LSeg f,
(((S-min (L~ f)) .. f) -' 1)
by A6, A38, A39, A40, TOPREAL1:27;
A51:
S-min (L~ f) <> f /. (((S-min (L~ f)) .. f) -' 1)
by A4, A6, A39, A42, GOBOARD7:31;
A52:
( not
LSeg f,
(((S-min (L~ f)) .. f) -' 1) is
vertical or not
LSeg f,
((S-min (L~ f)) .. f) is
vertical )
proof
assume
(
LSeg f,
(((S-min (L~ f)) .. f) -' 1) is
vertical &
LSeg f,
((S-min (L~ f)) .. f) is
vertical )
;
contradiction
then A53:
(
(S-min (L~ f)) `1 = (f /. (((S-min (L~ f)) .. f) + 1)) `1 &
(S-min (L~ f)) `1 = (f /. (((S-min (L~ f)) .. f) -' 1)) `1 )
by A50, A49, A41, A45, SPPOL_1:def 3;
A54:
(
(f /. (((S-min (L~ f)) .. f) + 1)) `2 <= (f /. (((S-min (L~ f)) .. f) -' 1)) `2 or
(f /. (((S-min (L~ f)) .. f) + 1)) `2 >= (f /. (((S-min (L~ f)) .. f) -' 1)) `2 )
;
A55:
(
(S-min (L~ f)) `2 <= (f /. (((S-min (L~ f)) .. f) + 1)) `2 &
(S-min (L~ f)) `2 <= (f /. (((S-min (L~ f)) .. f) -' 1)) `2 )
by A7, A43, A47, PSCOMP_1:71;
(
LSeg f,
((S-min (L~ f)) .. f) = LSeg (f /. ((S-min (L~ f)) .. f)),
(f /. (((S-min (L~ f)) .. f) + 1)) &
LSeg f,
(((S-min (L~ f)) .. f) -' 1) = LSeg (f /. ((S-min (L~ f)) .. f)),
(f /. (((S-min (L~ f)) .. f) -' 1)) )
by A37, A38, A39, A40, A44, TOPREAL1:def 5;
then
(
f /. (((S-min (L~ f)) .. f) -' 1) in LSeg f,
((S-min (L~ f)) .. f) or
f /. (((S-min (L~ f)) .. f) + 1) in LSeg f,
(((S-min (L~ f)) .. f) -' 1) )
by A6, A53, A55, A54, GOBOARD7:8;
then
(
f /. (((S-min (L~ f)) .. f) -' 1) in (LSeg f,(((S-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((S-min (L~ f)) .. f)) or
f /. (((S-min (L~ f)) .. f) + 1) in (LSeg f,(((S-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((S-min (L~ f)) .. f)) )
by A41, A45, XBOOLE_0:def 4;
then
(
((((S-min (L~ f)) .. f) -' 1) + 1) + 1
= (((S-min (L~ f)) .. f) -' 1) + (1 + 1) &
(LSeg f,(((S-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((S-min (L~ f)) .. f)) <> {(f /. ((S-min (L~ f)) .. f))} )
by A6, A51, A48, TARSKI:def 1;
hence
contradiction
by A39, A40, A44, TOPREAL1:def 8;
verum
end; now per cases
( LSeg f,(((S-min (L~ f)) .. f) -' 1) is horizontal or LSeg f,((S-min (L~ f)) .. f) is horizontal )
by A52, SPPOL_1:41;
suppose
LSeg f,
(((S-min (L~ f)) .. f) -' 1) is
horizontal
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 then A56:
(S-min (L~ f)) `2 = (f /. (((S-min (L~ f)) .. f) -' 1)) `2
by A50, A41, SPPOL_1:def 2;
then A57:
f /. (((S-min (L~ f)) .. f) -' 1) in S-most (L~ f)
by A2, A7, A42, Th15, GOBOARD1:16;
then A58:
(f /. (((S-min (L~ f)) .. f) -' 1)) `1 >= (S-min (L~ f)) `1
by PSCOMP_1:118;
(f /. (((S-min (L~ f)) .. f) -' 1)) `1 <> (S-min (L~ f)) `1
by A4, A6, A39, A42, A56, GOBOARD7:31, TOPREAL3:11;
then A59:
(f /. (((S-min (L~ f)) .. f) -' 1)) `1 > (S-min (L~ f)) `1
by A58, XXREAL_0:1;
(f /. (((S-min (L~ f)) .. f) -' 1)) `1 <= (S-max (L~ f)) `1
by A57, PSCOMP_1:118;
hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
by A59, XXREAL_0:2;
verum end; suppose
LSeg f,
((S-min (L~ f)) .. f) is
horizontal
;
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 then A60:
(S-min (L~ f)) `2 = (f /. (((S-min (L~ f)) .. f) + 1)) `2
by A49, A45, SPPOL_1:def 2;
then A61:
f /. (((S-min (L~ f)) .. f) + 1) in S-most (L~ f)
by A2, A7, A46, Th15, GOBOARD1:16;
then A62:
(f /. (((S-min (L~ f)) .. f) + 1)) `1 >= (S-min (L~ f)) `1
by PSCOMP_1:118;
(f /. (((S-min (L~ f)) .. f) + 1)) `1 <> (S-min (L~ f)) `1
by A4, A6, A46, A60, GOBOARD7:31, TOPREAL3:11;
then A63:
(f /. (((S-min (L~ f)) .. f) + 1)) `1 > (S-min (L~ f)) `1
by A62, XXREAL_0:1;
(f /. (((S-min (L~ f)) .. f) + 1)) `1 <= (S-max (L~ f)) `1
by A61, PSCOMP_1:118;
hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
by A63, XXREAL_0:2;
verum end; hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
;
verum end;