let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set i1 = (S-max (L~ z)) .. z;
set i2 = (S-min (L~ z)) .. z;
set j = (N-max (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
(S-max (L~ z)) .. z >= (S-min (L~ z)) .. z
; :: thesis: contradiction
A3:
N-max (L~ z) in rng z
by Th44;
A4:
S-min (L~ z) in rng z
by Th45;
A5:
S-max (L~ z) in rng z
by Th46;
then A6:
(S-max (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A7:
( 1 <= (S-max (L~ z)) .. z & (S-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A8:
(S-min (L~ z)) .. z in dom z
by A4, FINSEQ_4:30;
then A9:
( 1 <= (S-min (L~ z)) .. z & (S-min (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A10: z /. ((S-min (L~ z)) .. z) =
z . ((S-min (L~ z)) .. z)
by A8, PARTFUN1:def 8
.=
S-min (L~ z)
by A4, FINSEQ_4:29
;
A11: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by A6, PARTFUN1:def 8
.=
S-max (L~ z)
by A5, FINSEQ_4:29
;
S-min (L~ z) <> S-max (L~ z)
by Th60;
then A12:
(S-max (L~ z)) .. z > (S-min (L~ z)) .. z
by A2, A10, A11, XXREAL_0:1;
A13:
z /. 1 = z /. (len z)
by FINSEQ_6:def 1;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-max (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:56;
then
N-min (L~ z) <> S-max (L~ z)
by TOPREAL5:22;
then A14:
(S-max (L~ z)) .. z < len z
by A1, A7, A11, A13, XXREAL_0:1;
A15:
len z in dom z
by FINSEQ_5:6;
A16:
(N-max (L~ z)) .. z in dom z
by A3, FINSEQ_4:30;
then A17:
( 1 <= (N-max (L~ z)) .. z & (N-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A18: z /. ((N-max (L~ z)) .. z) =
z . ((N-max (L~ z)) .. z)
by A16, PARTFUN1:def 8
.=
N-max (L~ z)
by A3, FINSEQ_4:29
;
then A19:
(z /. ((N-max (L~ z)) .. z)) `2 = N-bound (L~ z)
by EUCLID:56;
A20:
(S-min (L~ z)) .. z > (N-max (L~ z)) .. z
by A1, Lm6;
N-min (L~ z) <> N-max (L~ z)
by Th56;
then A21:
1 < (N-max (L~ z)) .. z
by A1, A17, A18, XXREAL_0:1;
then reconsider h = mid z,((S-min (L~ z)) .. z),((N-max (L~ z)) .. z) as S-Sequence_in_R2 by A9, A20, Th41;
A22:
len h >= 2
by TOPREAL1:def 10;
A23:
h is_in_the_area_of z
by A8, A16, Th25, Th26;
h /. 1 = S-min (L~ z)
by A8, A10, A16, Th12;
then A24:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:56;
h /. (len h) = z /. ((N-max (L~ z)) .. z)
by A8, A16, Th13;
then A25:
h is_a_v.c._for z
by A19, A23, A24, Def3;
(S-max (L~ z)) .. z > 1
by A1, A17, Lm5, XXREAL_0:2;
then reconsider M = mid z,(len z),((S-max (L~ z)) .. z) as S-Sequence_in_R2 by A14, Th41;
A26:
L~ h misses L~ M
by A7, A12, A20, A21, Th53;
A27:
M /. (len M) = S-max (L~ z)
by A6, A11, A15, Th13;
A28:
len M = ((len z) -' ((S-max (L~ z)) .. z)) + 1
by A7, JORDAN4:21;
((S-max (L~ z)) .. z) + 1 <= len z
by A14, NAT_1:13;
then
(len z) - ((S-max (L~ z)) .. z) >= 1
by XREAL_1:21;
then
(len z) -' ((S-max (L~ z)) .. z) >= 1
by NAT_D:39;
then A29:
((len z) -' ((S-max (L~ z)) .. z)) + 1 >= 1 + 1
by XREAL_1:8;
then A30:
M /. (len M) in L~ M
by A28, JORDAN3:34;
A31:
1 in dom M
by FINSEQ_5:6;
A32:
M /. 1 = z /. (len z)
by A6, A15, Th12;
per cases
( ( NW-corner (L~ z) = N-min (L~ z) & SE-corner (L~ z) = S-max (L~ z) ) or ( NW-corner (L~ z) = N-min (L~ z) & SE-corner (L~ z) <> S-max (L~ z) ) or ( NW-corner (L~ z) <> N-min (L~ z) & SE-corner (L~ z) = S-max (L~ z) ) or ( NW-corner (L~ z) <> N-min (L~ z) & SE-corner (L~ z) <> S-max (L~ z) ) )
;
suppose that A33:
NW-corner (L~ z) = N-min (L~ z)
and A34:
SE-corner (L~ z) = S-max (L~ z)
;
:: thesis: contradictionA35:
M is_in_the_area_of z
by A6, A15, Th25, Th26;
A36:
(M /. 1) `1 = W-bound (L~ z)
by A1, A13, A32, A33, EUCLID:56;
(M /. (len M)) `1 = E-bound (L~ z)
by A27, A34, EUCLID:56;
then
M is_a_h.c._for z
by A35, A36, Def2;
hence
contradiction
by A22, A25, A26, A28, A29, Th33;
:: thesis: verum end; suppose that A37:
NW-corner (L~ z) = N-min (L~ z)
and A38:
SE-corner (L~ z) <> S-max (L~ z)
;
:: thesis: contradictionreconsider g =
M ^ <*(SE-corner (L~ z))*> as
S-Sequence_in_R2 by A6, A11, A15, A38, Th68;
A39:
len g >= 2
by TOPREAL1:def 10;
A40:
M is_in_the_area_of z
by A6, A15, Th25, Th26;
<*(SE-corner (L~ z))*> is_in_the_area_of z
by Th31;
then A41:
g is_in_the_area_of z
by A40, Th28;
g /. 1 =
M /. 1
by A31, FINSEQ_4:83
.=
z /. 1
by A6, A13, A15, Th12
;
then A42:
(g /. 1) `1 = W-bound (L~ z)
by A1, A37, EUCLID:56;
len g =
(len M) + (len <*(SE-corner (L~ z))*>)
by FINSEQ_1:35
.=
(len M) + 1
by FINSEQ_1:56
;
then
g /. (len g) = SE-corner (L~ z)
by FINSEQ_4:82;
then
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
then A43:
g is_a_h.c._for z
by A41, A42, Def2;
A44:
L~ g = (L~ M) \/ (LSeg (M /. (len M)),(SE-corner (L~ z)))
by SPPOL_2:19;
(LSeg (M /. (len M)),(SE-corner (L~ z))) /\ (L~ h) c= (LSeg (M /. (len M)),(SE-corner (L~ z))) /\ (L~ z)
by A9, A17, JORDAN4:47, XBOOLE_1:26;
then
(LSeg (M /. (len M)),(SE-corner (L~ z))) /\ (L~ h) c= {(M /. (len M))}
by A27, PSCOMP_1:122;
hence
contradiction
by A22, A25, A26, A30, A39, A43, A44, Th33, ZFMISC_1:149;
:: thesis: verum end; suppose that A45:
NW-corner (L~ z) <> N-min (L~ z)
and A46:
SE-corner (L~ z) = S-max (L~ z)
;
:: thesis: contradictionreconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A6, A13, A15, A45, Th70;
A47:
len g >= 2
by TOPREAL1:def 10;
A48:
M is_in_the_area_of z
by A6, A15, Th25, Th26;
<*(NW-corner (L~ z))*> is_in_the_area_of z
by Th30;
then A49:
g is_in_the_area_of z
by A48, Th28;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:16;
then A50:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
A51:
len M in dom M
by FINSEQ_5:6;
len g = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:35;
then g /. (len g) =
M /. (len M)
by A51, FINSEQ_4:84
.=
S-max (L~ z)
by A6, A11, A15, Th13
;
then
(g /. (len g)) `1 = E-bound (L~ z)
by A46, EUCLID:56;
then A52:
g is_a_h.c._for z
by A49, A50, Def2;
A53:
L~ g = (L~ M) \/ (LSeg (NW-corner (L~ z)),(M /. 1))
by SPPOL_2:20;
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= (LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ z)
by A9, A17, JORDAN4:47, XBOOLE_1:26;
then A54:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= {(M /. 1)}
by A1, A13, A32, PSCOMP_1:102;
M /. 1
in L~ M
by A28, A29, JORDAN3:34;
hence
contradiction
by A22, A25, A26, A47, A52, A53, A54, Th33, ZFMISC_1:149;
:: thesis: verum end; suppose that A55:
NW-corner (L~ z) <> N-min (L~ z)
and A56:
SE-corner (L~ z) <> S-max (L~ z)
;
:: thesis: contradictionset K =
<*(NW-corner (L~ z))*> ^ M;
reconsider g =
(<*(NW-corner (L~ z))*> ^ M) ^ <*(SE-corner (L~ z))*> as
S-Sequence_in_R2 by A1, A6, A11, A13, A15, A55, A56, Lm3;
A57:
len g >= 2
by TOPREAL1:def 10;
A58:
M is_in_the_area_of z
by A6, A15, Th25, Th26;
<*(NW-corner (L~ z))*> is_in_the_area_of z
by Th30;
then A59:
<*(NW-corner (L~ z))*> ^ M is_in_the_area_of z
by A58, Th28;
<*(SE-corner (L~ z))*> is_in_the_area_of z
by Th31;
then A60:
g is_in_the_area_of z
by A59, Th28;
1
in dom (<*(NW-corner (L~ z))*> ^ M)
by FINSEQ_5:6;
then g /. 1 =
(<*(NW-corner (L~ z))*> ^ M) /. 1
by FINSEQ_4:83
.=
NW-corner (L~ z)
by FINSEQ_5:16
;
then A61:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
len g =
(len (<*(NW-corner (L~ z))*> ^ M)) + (len <*(SE-corner (L~ z))*>)
by FINSEQ_1:35
.=
(len (<*(NW-corner (L~ z))*> ^ M)) + 1
by FINSEQ_1:56
;
then
g /. (len g) = SE-corner (L~ z)
by FINSEQ_4:82;
then
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
then A62:
g is_a_h.c._for z
by A60, A61, Def2;
A63:
L~ (<*(NW-corner (L~ z))*> ^ M) = (L~ M) \/ (LSeg (NW-corner (L~ z)),(M /. 1))
by SPPOL_2:20;
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= (LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ z)
by A9, A17, JORDAN4:47, XBOOLE_1:26;
then A64:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= {(M /. 1)}
by A1, A13, A32, PSCOMP_1:102;
M /. 1
in L~ M
by A28, A29, JORDAN3:34;
then A65:
L~ (<*(NW-corner (L~ z))*> ^ M) misses L~ h
by A26, A63, A64, ZFMISC_1:149;
len (<*(NW-corner (L~ z))*> ^ M) = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:35;
then
len (<*(NW-corner (L~ z))*> ^ M) >= len M
by NAT_1:11;
then
len (<*(NW-corner (L~ z))*> ^ M) >= 2
by A28, A29, XXREAL_0:2;
then A66:
(<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)) in L~ (<*(NW-corner (L~ z))*> ^ M)
by JORDAN3:34;
A67:
L~ g = (L~ (<*(NW-corner (L~ z))*> ^ M)) \/ (LSeg ((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(SE-corner (L~ z)))
by SPPOL_2:19;
A68:
len M in dom M
by FINSEQ_5:6;
len (<*(NW-corner (L~ z))*> ^ M) = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:35;
then A69:
(<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)) =
M /. (len M)
by A68, FINSEQ_4:84
.=
z /. ((S-max (L~ z)) .. z)
by A6, A15, Th13
.=
S-max (L~ z)
by A5, FINSEQ_5:41
;
(LSeg ((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(SE-corner (L~ z))) /\ (L~ h) c= (LSeg ((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(SE-corner (L~ z))) /\ (L~ z)
by A9, A17, JORDAN4:47, XBOOLE_1:26;
then
(LSeg ((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(SE-corner (L~ z))) /\ (L~ h) c= {((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)))}
by A69, PSCOMP_1:122;
hence
contradiction
by A22, A25, A57, A62, A65, A66, A67, Th33, ZFMISC_1:149;
:: thesis: verum end;