let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (E-max (L~ z)) .. z < (S-max (L~ z)) .. z )
set i1 = (E-max (L~ z)) .. z;
set i2 = (S-max (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
(E-max (L~ z)) .. z >= (S-max (L~ z)) .. z
; :: thesis: contradiction
A3:
E-max (L~ z) in rng z
by Th50;
A4:
S-max (L~ z) in rng z
by Th46;
A5:
(E-max (L~ z)) .. z in dom z
by A3, FINSEQ_4:30;
then A6:
( 1 <= (E-max (L~ z)) .. z & (E-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A7:
(S-max (L~ z)) .. z in dom z
by A4, FINSEQ_4:30;
then A8:
( 1 <= (S-max (L~ z)) .. z & (S-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A9: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by A7, PARTFUN1:def 8
.=
S-max (L~ z)
by A4, FINSEQ_4:29
;
A10:
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
A11: z /. ((E-max (L~ z)) .. z) =
z . ((E-max (L~ z)) .. z)
by A5, PARTFUN1:def 8
.=
E-max (L~ z)
by A3, FINSEQ_4:29
;
A12:
(E-min (L~ z)) `2 < (E-max (L~ z)) `2
by Th57;
E-min (L~ z) in L~ z
by SPRECT_1:16;
then
S-bound (L~ z) <= (E-min (L~ z)) `2
by PSCOMP_1:71;
then
E-max (L~ z) <> S-max (L~ z)
by A12, EUCLID:56;
then A13:
(E-max (L~ z)) .. z > (S-max (L~ z)) .. z
by A2, A9, A11, XXREAL_0:1;
then A14:
(E-max (L~ z)) .. z > 1
by A8, XXREAL_0:2;
A15:
len z in dom z
by FINSEQ_5:6;
A16:
z /. 1 = z /. (len z)
by FINSEQ_6:def 1;
A17:
2 <= len z
by REALSET1:13;
then A18:
2 in dom z
by FINSEQ_3:27;
z /. 2 in N-most (L~ z)
by A1, Th34;
then A19: (z /. 2) `2 =
(N-min (L~ z)) `2
by PSCOMP_1:98
.=
N-bound (L~ z)
by EUCLID:56
;
A20:
(z /. 1) `2 = N-bound (L~ z)
by A1, EUCLID:56;
A21:
(S-max (L~ z)) .. z <> 0
by A7, FINSEQ_3:27;
A22:
(z /. ((S-max (L~ z)) .. z)) `2 = S-bound (L~ z)
by A9, EUCLID:56;
S-bound (L~ z) < N-bound (L~ z)
by TOPREAL5:22;
then A23:
(S-max (L~ z)) .. z > 2
by A19, A20, A21, A22, NAT_1:27;
then reconsider h = mid z,((S-max (L~ z)) .. z),2 as S-Sequence_in_R2 by A8, Th41;
A24:
len h >= 2
by TOPREAL1:def 10;
A25:
h is_in_the_area_of z
by A7, A18, Th25, Th26;
h /. 1 = S-max (L~ z)
by A7, A9, A18, Th12;
then A26:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:56;
h /. (len h) = z /. 2
by A7, A18, Th13;
then A27:
h is_a_v.c._for z
by A19, A25, A26, Def3;
A28:
(N-min (L~ z)) `1 < (N-max (L~ z)) `1
by Th55;
N-max (L~ z) in L~ z
by SPRECT_1:13;
then
(N-max (L~ z)) `1 <= E-bound (L~ z)
by PSCOMP_1:71;
then
(E-max (L~ z)) .. z <> len z
by A10, A11, A28, EUCLID:56;
then A29:
(E-max (L~ z)) .. z < len z
by A6, XXREAL_0:1;
then reconsider M = mid z,(len z),((E-max (L~ z)) .. z) as S-Sequence_in_R2 by A14, Th41;
A30:
len M >= 2
by TOPREAL1:def 10;
A31:
L~ M misses L~ h
by A6, A13, A23, Th53;
A32: M /. (len M) =
z /. ((E-max (L~ z)) .. z)
by A5, A15, Th13
.=
E-max (L~ z)
by A3, FINSEQ_5:41
;
A33:
len M = ((len z) -' ((E-max (L~ z)) .. z)) + 1
by A6, JORDAN4:21;
((E-max (L~ z)) .. z) + 1 <= len z
by A29, NAT_1:13;
then
(len z) - ((E-max (L~ z)) .. z) >= 1
by XREAL_1:21;
then
(len z) -' ((E-max (L~ z)) .. z) >= 1
by NAT_D:39;
then A34:
((len z) -' ((E-max (L~ z)) .. z)) + 1 >= 1 + 1
by XREAL_1:8;
A35:
M /. 1 = z /. 1
by A5, A15, A16, Th12;
per cases
( NW-corner (L~ z) = N-min (L~ z) or NW-corner (L~ z) <> N-min (L~ z) )
;
suppose A36:
NW-corner (L~ z) = N-min (L~ z)
;
:: thesis: contradictionA37:
M is_in_the_area_of z
by A5, A15, Th25, Th26;
M /. 1
= z /. (len z)
by A5, A15, Th12;
then A38:
(M /. 1) `1 = W-bound (L~ z)
by A1, A16, A36, EUCLID:56;
(M /. (len M)) `1 = E-bound (L~ z)
by A32, EUCLID:56;
then
M is_a_h.c._for z
by A37, A38, Def2;
hence
contradiction
by A24, A27, A30, A31, Th33;
:: thesis: verum end; suppose
NW-corner (L~ z) <> N-min (L~ z)
;
:: thesis: contradictionthen reconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A5, A15, A16, Th70;
A39:
len g >= 2
by TOPREAL1:def 10;
A40:
M is_in_the_area_of z
by A5, A15, Th25, Th26;
<*(NW-corner (L~ z))*> is_in_the_area_of z
by Th30;
then A41:
g is_in_the_area_of z
by A40, Th28;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:16;
then A42:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
A43:
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 A43, FINSEQ_4:84
.=
z /. ((E-max (L~ z)) .. z)
by A5, A15, Th13
.=
E-max (L~ z)
by A3, FINSEQ_5:41
;
then
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
then A44:
g is_a_h.c._for z
by A41, A42, Def2;
A45:
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 A8, A17, JORDAN4:47, XBOOLE_1:26;
then A46:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= {(M /. 1)}
by A1, A35, PSCOMP_1:102;
M /. 1
in L~ M
by A33, A34, JORDAN3:34;
hence
contradiction
by A24, A27, A31, A39, A44, A45, A46, Th33, ZFMISC_1:149;
:: thesis: verum end;