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