let f be V22() standard special_circular_sequence; (N-min (L~ f)) `1 < (N-max (L~ f)) `1
set p = N-min (L~ f);
set i = (N-min (L~ f)) .. f;
A1:
len f > 3 + 1
by GOBOARD7:34;
A2:
len f >= 1 + 1
by GOBOARD7:34, XXREAL_0:2;
A3:
N-min (L~ f) in rng f
by Th39;
then A4:
(N-min (L~ f)) .. f in dom f
by FINSEQ_4:20;
then A5:
( 1 <= (N-min (L~ f)) .. f & (N-min (L~ f)) .. f <= len f )
by FINSEQ_3:25;
A6: N-min (L~ f) =
f . ((N-min (L~ f)) .. f)
by A3, FINSEQ_4:19
.=
f /. ((N-min (L~ f)) .. f)
by A4, PARTFUN1:def 6
;
A7:
(N-min (L~ f)) `2 = N-bound (L~ f)
by EUCLID:52;
per cases
( (N-min (L~ f)) .. f = 1 or (N-min (L~ f)) .. f = len f or ( 1 < (N-min (L~ f)) .. f & (N-min (L~ f)) .. f < len f ) )
by A5, XXREAL_0:1;
suppose A8:
(
(N-min (L~ f)) .. f = 1 or
(N-min (L~ f)) .. f = len f )
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 then
N-min (L~ f) = f /. 1
by A6, FINSEQ_6:def 1;
then A9:
N-min (L~ f) in LSeg (
f,1)
by A2, TOPREAL1:21;
A10:
1
+ 1
in dom f
by A2, FINSEQ_3:25;
then A11:
f /. (1 + 1) in L~ f
by A1, GOBOARD1:1, XXREAL_0:2;
A12:
f /. (1 + 1) in LSeg (
f,1)
by A2, TOPREAL1:21;
A13:
((len f) -' 1) + 1
= len f
by A1, XREAL_1:235, XXREAL_0:2;
then
(len f) -' 1
> 3
by A1, XREAL_1:6;
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:21;
(len f) -' 1
<= len f
by A13, NAT_1:11;
then A16:
(len f) -' 1
in dom f
by A14, FINSEQ_3:25;
then A17:
f /. ((len f) -' 1) in L~ f
by A1, GOBOARD1:1, XXREAL_0:2;
A18:
f /. 1
= f /. (len f)
by FINSEQ_6:def 1;
then A19:
N-min (L~ f) in LSeg (
f,
((len f) -' 1))
by A6, A8, A13, A14, TOPREAL1:21;
A20:
1
in dom f
by FINSEQ_5:6;
then A21:
N-min (L~ f) <> f /. (1 + 1)
by A6, A8, A18, A10, GOBOARD7:29;
A22:
len f in dom f
by FINSEQ_5:6;
then A23:
N-min (L~ f) <> f /. ((len f) -' 1)
by A6, A8, A18, A13, A16, GOBOARD7:29;
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:
(
(N-min (L~ f)) `1 = (f /. (1 + 1)) `1 &
(N-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:
(
(N-min (L~ f)) `2 >= (f /. (1 + 1)) `2 &
(N-min (L~ f)) `2 >= (f /. ((len f) -' 1)) `2 )
by A7, A17, A11, PSCOMP_1:24;
(
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 3;
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:7;
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 6;
hence
contradiction
by A28, JORDAN4:42;
verum
end; now (N-min (L~ f)) `1 < (N-max (L~ f)) `1 per cases
( LSeg (f,((len f) -' 1)) is horizontal or LSeg (f,1) is horizontal )
by A24, SPPOL_1:19;
suppose
LSeg (
f,
((len f) -' 1)) is
horizontal
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 then A29:
(N-min (L~ f)) `2 = (f /. ((len f) -' 1)) `2
by A19, A15, SPPOL_1:def 2;
then A30:
f /. ((len f) -' 1) in N-most (L~ f)
by A2, A7, A16, Th10, GOBOARD1:1;
then A31:
(f /. ((len f) -' 1)) `1 >= (N-min (L~ f)) `1
by PSCOMP_1:39;
(f /. ((len f) -' 1)) `1 <> (N-min (L~ f)) `1
by A6, A8, A22, A18, A13, A16, A29, GOBOARD7:29, TOPREAL3:6;
then A32:
(f /. ((len f) -' 1)) `1 > (N-min (L~ f)) `1
by A31, XXREAL_0:1;
(f /. ((len f) -' 1)) `1 <= (N-max (L~ f)) `1
by A30, PSCOMP_1:39;
hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
by A32, XXREAL_0:2;
verum end; suppose
LSeg (
f,1) is
horizontal
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 then A33:
(N-min (L~ f)) `2 = (f /. (1 + 1)) `2
by A9, A12, SPPOL_1:def 2;
then A34:
f /. (1 + 1) in N-most (L~ f)
by A2, A7, A10, Th10, GOBOARD1:1;
then A35:
(f /. (1 + 1)) `1 >= (N-min (L~ f)) `1
by PSCOMP_1:39;
(f /. (1 + 1)) `1 <> (N-min (L~ f)) `1
by A6, A8, A20, A18, A10, A33, GOBOARD7:29, TOPREAL3:6;
then A36:
(f /. (1 + 1)) `1 > (N-min (L~ f)) `1
by A35, XXREAL_0:1;
(f /. (1 + 1)) `1 <= (N-max (L~ f)) `1
by A34, PSCOMP_1:39;
hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
by A36, XXREAL_0:2;
verum end; hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
;
verum end; suppose that A37:
1
< (N-min (L~ f)) .. f
and A38:
(N-min (L~ f)) .. f < len f
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 A39:
(((N-min (L~ f)) .. f) -' 1) + 1
= (N-min (L~ f)) .. f
by A37, XREAL_1:235;
then A40:
((N-min (L~ f)) .. f) -' 1
>= 1
by A37, NAT_1:13;
then A41:
f /. (((N-min (L~ f)) .. f) -' 1) in LSeg (
f,
(((N-min (L~ f)) .. f) -' 1))
by A38, A39, TOPREAL1:21;
((N-min (L~ f)) .. f) -' 1
<= (N-min (L~ f)) .. f
by A39, NAT_1:11;
then
((N-min (L~ f)) .. f) -' 1
<= len f
by A38, XXREAL_0:2;
then A42:
((N-min (L~ f)) .. f) -' 1
in dom f
by A40, FINSEQ_3:25;
then A43:
f /. (((N-min (L~ f)) .. f) -' 1) in L~ f
by A1, GOBOARD1:1, XXREAL_0:2;
A44:
((N-min (L~ f)) .. f) + 1
<= len f
by A38, NAT_1:13;
then A45:
f /. (((N-min (L~ f)) .. f) + 1) in LSeg (
f,
((N-min (L~ f)) .. f))
by A37, TOPREAL1:21;
((N-min (L~ f)) .. f) + 1
>= 1
by NAT_1:11;
then A46:
((N-min (L~ f)) .. f) + 1
in dom f
by A44, FINSEQ_3:25;
then A47:
f /. (((N-min (L~ f)) .. f) + 1) in L~ f
by A1, GOBOARD1:1, XXREAL_0:2;
A48:
N-min (L~ f) <> f /. (((N-min (L~ f)) .. f) + 1)
by A3, A6, A46, FINSEQ_4:20, GOBOARD7:29;
A49:
N-min (L~ f) in LSeg (
f,
((N-min (L~ f)) .. f))
by A6, A37, A44, TOPREAL1:21;
A50:
N-min (L~ f) in LSeg (
f,
(((N-min (L~ f)) .. f) -' 1))
by A6, A38, A39, A40, TOPREAL1:21;
A51:
N-min (L~ f) <> f /. (((N-min (L~ f)) .. f) -' 1)
by A4, A6, A39, A42, GOBOARD7:29;
A52:
( not
LSeg (
f,
(((N-min (L~ f)) .. f) -' 1)) is
vertical or not
LSeg (
f,
((N-min (L~ f)) .. f)) is
vertical )
proof
assume
(
LSeg (
f,
(((N-min (L~ f)) .. f) -' 1)) is
vertical &
LSeg (
f,
((N-min (L~ f)) .. f)) is
vertical )
;
contradiction
then A53:
(
(N-min (L~ f)) `1 = (f /. (((N-min (L~ f)) .. f) + 1)) `1 &
(N-min (L~ f)) `1 = (f /. (((N-min (L~ f)) .. f) -' 1)) `1 )
by A50, A49, A41, A45, SPPOL_1:def 3;
A54:
(
(f /. (((N-min (L~ f)) .. f) + 1)) `2 <= (f /. (((N-min (L~ f)) .. f) -' 1)) `2 or
(f /. (((N-min (L~ f)) .. f) + 1)) `2 >= (f /. (((N-min (L~ f)) .. f) -' 1)) `2 )
;
A55:
(
(N-min (L~ f)) `2 >= (f /. (((N-min (L~ f)) .. f) + 1)) `2 &
(N-min (L~ f)) `2 >= (f /. (((N-min (L~ f)) .. f) -' 1)) `2 )
by A7, A43, A47, PSCOMP_1:24;
(
LSeg (
f,
((N-min (L~ f)) .. f))
= LSeg (
(f /. ((N-min (L~ f)) .. f)),
(f /. (((N-min (L~ f)) .. f) + 1))) &
LSeg (
f,
(((N-min (L~ f)) .. f) -' 1))
= LSeg (
(f /. ((N-min (L~ f)) .. f)),
(f /. (((N-min (L~ f)) .. f) -' 1))) )
by A37, A38, A39, A40, A44, TOPREAL1:def 3;
then
(
f /. (((N-min (L~ f)) .. f) -' 1) in LSeg (
f,
((N-min (L~ f)) .. f)) or
f /. (((N-min (L~ f)) .. f) + 1) in LSeg (
f,
(((N-min (L~ f)) .. f) -' 1)) )
by A6, A53, A55, A54, GOBOARD7:7;
then
(
f /. (((N-min (L~ f)) .. f) -' 1) in (LSeg (f,(((N-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((N-min (L~ f)) .. f))) or
f /. (((N-min (L~ f)) .. f) + 1) in (LSeg (f,(((N-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((N-min (L~ f)) .. f))) )
by A41, A45, XBOOLE_0:def 4;
then
(
((((N-min (L~ f)) .. f) -' 1) + 1) + 1
= (((N-min (L~ f)) .. f) -' 1) + (1 + 1) &
(LSeg (f,(((N-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((N-min (L~ f)) .. f))) <> {(f /. ((N-min (L~ f)) .. f))} )
by A6, A51, A48, TARSKI:def 1;
hence
contradiction
by A39, A40, A44, TOPREAL1:def 6;
verum
end; now (N-min (L~ f)) `1 < (N-max (L~ f)) `1 per cases
( LSeg (f,(((N-min (L~ f)) .. f) -' 1)) is horizontal or LSeg (f,((N-min (L~ f)) .. f)) is horizontal )
by A52, SPPOL_1:19;
suppose
LSeg (
f,
(((N-min (L~ f)) .. f) -' 1)) is
horizontal
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 then A56:
(N-min (L~ f)) `2 = (f /. (((N-min (L~ f)) .. f) -' 1)) `2
by A50, A41, SPPOL_1:def 2;
then A57:
f /. (((N-min (L~ f)) .. f) -' 1) in N-most (L~ f)
by A2, A7, A42, Th10, GOBOARD1:1;
then A58:
(f /. (((N-min (L~ f)) .. f) -' 1)) `1 >= (N-min (L~ f)) `1
by PSCOMP_1:39;
(f /. (((N-min (L~ f)) .. f) -' 1)) `1 <> (N-min (L~ f)) `1
by A4, A6, A39, A42, A56, GOBOARD7:29, TOPREAL3:6;
then A59:
(f /. (((N-min (L~ f)) .. f) -' 1)) `1 > (N-min (L~ f)) `1
by A58, XXREAL_0:1;
(f /. (((N-min (L~ f)) .. f) -' 1)) `1 <= (N-max (L~ f)) `1
by A57, PSCOMP_1:39;
hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
by A59, XXREAL_0:2;
verum end; suppose
LSeg (
f,
((N-min (L~ f)) .. f)) is
horizontal
;
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 then A60:
(N-min (L~ f)) `2 = (f /. (((N-min (L~ f)) .. f) + 1)) `2
by A49, A45, SPPOL_1:def 2;
then A61:
f /. (((N-min (L~ f)) .. f) + 1) in N-most (L~ f)
by A2, A7, A46, Th10, GOBOARD1:1;
then A62:
(f /. (((N-min (L~ f)) .. f) + 1)) `1 >= (N-min (L~ f)) `1
by PSCOMP_1:39;
(f /. (((N-min (L~ f)) .. f) + 1)) `1 <> (N-min (L~ f)) `1
by A4, A6, A46, A60, GOBOARD7:29, TOPREAL3:6;
then A63:
(f /. (((N-min (L~ f)) .. f) + 1)) `1 > (N-min (L~ f)) `1
by A62, XXREAL_0:1;
(f /. (((N-min (L~ f)) .. f) + 1)) `1 <= (N-max (L~ f)) `1
by A61, PSCOMP_1:39;
hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
by A63, XXREAL_0:2;
verum end; hence
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
;
verum end;