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