let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat st n > 0 holds
for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
let n be Nat; ( n > 0 implies for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )
assume A1:
n > 0
; for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
set US = Upper_Seq (C,n);
set sr = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2;
set Ebo = E-bound (L~ (Cage (C,n)));
set Wbo = W-bound (L~ (Cage (C,n)));
set Emax = E-max (L~ (Cage (C,n)));
set Wmin = W-min (L~ (Cage (C,n)));
set FiP = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));
defpred S1[ Nat] means ( 1 <= $1 & $1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. $1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 );
A2:
W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n)))
by SPRECT_1:31;
then A3:
W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by XREAL_1:226;
A4:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n)))
by A2, XREAL_1:226;
A5:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
set GC1 =
(Gauge (C,n)) * (
(Center (Gauge (C,n))),1);
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A6:
( 1
<= k &
k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )
;
S1[k + 1]
4
<= len (Gauge (C,n))
by JORDAN8:10;
then
1
<= len (Gauge (C,n))
by XXREAL_0:2;
then A7:
1
<= width (Gauge (C,n))
by JORDAN8:def 1;
then A8:
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 =
((W-bound C) + (E-bound C)) / 2
by A1, Th35
.=
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by Th33
;
A9:
k >= 1
by NAT_1:14;
A10:
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
A11:
First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (Cage (C,n)))),
(E-max (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
in rng (Upper_Seq (C,n))
by A1, Th47;
then A12:
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by FINSEQ_4:20;
then A13:
1
<= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))
by FINSEQ_3:25;
A14:
1
<= Center (Gauge (C,n))
by JORDAN1B:11;
A15:
(Upper_Seq (C,n)) /. 1
= W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
reconsider kk =
k as
Nat ;
assume that A16:
1
<= k + 1
and A17:
k + 1
< (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))
;
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
A18:
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n))
by A12, FINSEQ_3:25;
then A19:
k + 1
<= len (Upper_Seq (C,n))
by A17, XXREAL_0:2;
Upper_Seq (
C,
n)
is_sequence_on Gauge (
C,
n)
by Th4;
then consider i1,
j1,
i2,
j2 being
Nat such that A20:
[i1,j1] in Indices (Gauge (C,n))
and A21:
(Upper_Seq (C,n)) /. kk = (Gauge (C,n)) * (
i1,
j1)
and A22:
[i2,j2] in Indices (Gauge (C,n))
and A23:
(Upper_Seq (C,n)) /. (kk + 1) = (Gauge (C,n)) * (
i2,
j2)
and A24:
( (
i1 = i2 &
j1 + 1
= j2 ) or (
i1 + 1
= i2 &
j1 = j2 ) or (
i1 = i2 + 1 &
j1 = j2 ) or (
i1 = i2 &
j1 = j2 + 1 ) )
by A9, A19, JORDAN8:3;
A25:
1
<= i1
by A20, MATRIX_0:32;
A26:
( 1
<= j1 &
j1 <= width (Gauge (C,n)) )
by A20, MATRIX_0:32;
A27:
j2 <= width (Gauge (C,n))
by A22, MATRIX_0:32;
A28:
( 1
<= i2 & 1
<= j2 )
by A22, MATRIX_0:32;
A29:
i2 <= len (Gauge (C,n))
by A22, MATRIX_0:32;
A30:
i1 <= len (Gauge (C,n))
by A20, MATRIX_0:32;
A31:
(
Center (Gauge (C,n)) <= len (Gauge (C,n)) &
i1 + 1
>= 1 )
by JORDAN1B:13, NAT_1:11;
now ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A24;
suppose
(
i1 = i2 &
j1 + 1
= j2 )
;
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2then ((Upper_Seq (C,n)) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A21, A25, A30, A26, GOBOARD5:2
.=
((Upper_Seq (C,n)) /. (k + 1)) `1
by A23, A29, A28, A27, GOBOARD5:2
;
hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A6, A17, NAT_1:13, NAT_1:14;
verum end; suppose A32:
(
i1 + 1
= i2 &
j1 = j2 )
;
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2A33:
now not ((Upper_Seq (C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2A34:
k + 1
>= 1
+ 1
by A9, XREAL_1:7;
len (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) =
(((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) -' 1) + 1
by A13, A18, JORDAN4:8
.=
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))
by A13, XREAL_1:235
;
then A35:
rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) c= L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))))
by A17, A34, SPPOL_2:18, XXREAL_0:2;
A36:
(Upper_Seq (C,n)) /. ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) = First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (Cage (C,n)))),
(E-max (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
by A11, FINSEQ_5:38;
A38:
(
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 &
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
<= (E-max (L~ (Cage (C,n)))) `1 )
by A3, A4, EUCLID:52;
A39:
(
Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is
closed &
L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))),
E-max (L~ (Cage (C,n))) )
by A15, A10, JORDAN6:30, TOPREAL1:25;
First_Point (
(L~ (Upper_Seq (C,n))),
((Upper_Seq (C,n)) /. 1),
((Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
in rng (Upper_Seq (C,n))
by A1, A15, A10, Th47;
then A40:
(L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))}
by A15, A10, A39, A38, A37, Th50, JORDAN6:49;
A41:
(
mid (
(Upper_Seq (C,n)),1,
((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))
= (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) &
(Upper_Seq (C,n)) | (Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))) = (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) )
by A13, FINSEQ_1:def 15, FINSEQ_6:116;
assume
((Upper_Seq (C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
;
contradictionthen
(Upper_Seq (C,n)) /. (k + 1) in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 }
;
then A42:
(Upper_Seq (C,n)) /. (k + 1) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)
by JORDAN6:def 6;
A43:
k + 1
in dom (Upper_Seq (C,n))
by A16, A19, FINSEQ_3:25;
k + 1
in Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))
by A16, A17, FINSEQ_1:1;
then
(Upper_Seq (C,n)) /. (k + 1) in rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))))
by A41, A43, PARTFUN2:18;
then
(Upper_Seq (C,n)) /. (k + 1) in {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))}
by A42, A35, A40, XBOOLE_0:def 4;
then
(Upper_Seq (C,n)) /. (k + 1) = First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (Cage (C,n)))),
(E-max (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
by TARSKI:def 1;
hence
contradiction
by A17, A12, A43, A36, PARTFUN2:10;
verum end;
i1 < Center (Gauge (C,n))
by A6, A17, A21, A30, A26, A14, A7, A8, JORDAN1A:18, NAT_1:13, NAT_1:14;
then
i1 + 1
<= Center (Gauge (C,n))
by NAT_1:13;
then
((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A23, A26, A7, A8, A31, A32, JORDAN1A:18;
hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A33, XXREAL_0:1;
verum end; suppose
(
i1 = i2 + 1 &
j1 = j2 )
;
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2then
i2 < i1
by NAT_1:13;
then
((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((Upper_Seq (C,n)) /. k) `1
by A21, A23, A30, A26, A28, A27, JORDAN1A:18;
hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A6, A17, NAT_1:13, NAT_1:14, XXREAL_0:2;
verum end; suppose
(
i1 = i2 &
j1 = j2 + 1 )
;
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2then ((Upper_Seq (C,n)) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A21, A25, A30, A26, GOBOARD5:2
.=
((Upper_Seq (C,n)) /. (k + 1)) `1
by A23, A29, A28, A27, GOBOARD5:2
;
hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A6, A17, NAT_1:13, NAT_1:14;
verum end; end; end;
hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
;
verum
end;
A44:
S1[1]
proof
assume that
1
<= 1
and
1
< (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))
;
((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
(Upper_Seq (C,n)) /. 1
= W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
hence
((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A3, EUCLID:52;
verum
end;
A45:
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A44, A5);
let k be Nat; ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )
assume
( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) )
; ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
hence
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A45; verum