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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds
((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds
((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds
((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
set LS = Lower_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 RLS = Rev (Lower_Seq (C,n));
set FiP = First_Point ((L~ (Rev (Lower_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)));
set LaP = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));
A2:
L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n))
by SPPOL_2:22;
A3:
len (Rev (Lower_Seq (C,n))) = len (Lower_Seq (C,n))
by FINSEQ_5:def 3;
defpred S1[ Nat] means ( 1 <= $1 & $1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_Seq (C,n))) /. $1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 );
A4:
rng (Rev (Lower_Seq (C,n))) = rng (Lower_Seq (C,n))
by FINSEQ_5:57;
A5:
W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n)))
by SPRECT_1:31;
then A6:
W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by XREAL_1:226;
A7:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n)))
by A5, XREAL_1:226;
A8:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
A9:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:21;
then
W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN6:1;
then A10:
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by EUCLID:52;
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
<= E-bound (L~ (Cage (C,n)))
by A9, JORDAN6:1;
then A11:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
<= (E-max (L~ (Cage (C,n)))) `1
by EUCLID:52;
A12:
(Rev (Lower_Seq (C,n))) /. (len (Rev (Lower_Seq (C,n)))) =
(Lower_Seq (C,n)) /. 1
by A3, FINSEQ_5:65
.=
E-max (L~ (Cage (C,n)))
by JORDAN1F:6
;
set GC1 =
(Gauge (C,n)) * (
(Center (Gauge (C,n))),1);
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A13:
( 1
<= k &
k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies
((Rev (Lower_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 A14:
1
<= width (Gauge (C,n))
by JORDAN8:def 1;
then A15:
((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
;
A16:
(
(Lower_Seq (C,n)) /. 1
= E-max (L~ (Cage (C,n))) &
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) )
by JORDAN1F:6, JORDAN1F:8;
then A17:
L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))),
W-min (L~ (Cage (C,n)))
by TOPREAL1:25;
A18:
1
<= Center (Gauge (C,n))
by JORDAN1B:11;
A19:
(Rev (Lower_Seq (C,n))) /. 1 =
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by FINSEQ_5:65
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))),
E-max (L~ (Cage (C,n)))
by A16, JORDAN5B:14, TOPREAL1:25;
then
(
L~ (Lower_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) &
(L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is
closed )
by A10, A11, JORDAN6:49;
then A20:
First_Point (
(L~ (Rev (Lower_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)))
= Last_Point (
(L~ (Lower_Seq (C,n))),
(E-max (L~ (Cage (C,n)))),
(W-min (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
by A2, A17, JORDAN5C:18;
then A21:
(First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) in dom (Rev (Lower_Seq (C,n)))
by A1, A4, Th48, FINSEQ_4:20;
then A22:
1
<= (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))
by FINSEQ_3:25;
A23:
k >= 1
by NAT_1:14;
reconsider kk =
k as
Nat ;
assume that A24:
1
<= k + 1
and A25:
k + 1
< (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))
;
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
A26:
(First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) <= len (Rev (Lower_Seq (C,n)))
by A21, FINSEQ_3:25;
then A27:
k + 1
<= len (Rev (Lower_Seq (C,n)))
by A25, XXREAL_0:2;
Lower_Seq (
C,
n)
is_sequence_on Gauge (
C,
n)
by Th5;
then
Rev (Lower_Seq (C,n)) is_sequence_on Gauge (
C,
n)
by JORDAN9:5;
then consider i1,
j1,
i2,
j2 being
Nat such that A28:
[i1,j1] in Indices (Gauge (C,n))
and A29:
(Rev (Lower_Seq (C,n))) /. kk = (Gauge (C,n)) * (
i1,
j1)
and A30:
[i2,j2] in Indices (Gauge (C,n))
and A31:
(Rev (Lower_Seq (C,n))) /. (kk + 1) = (Gauge (C,n)) * (
i2,
j2)
and A32:
( (
i1 = i2 &
j1 + 1
= j2 ) or (
i1 + 1
= i2 &
j1 = j2 ) or (
i1 = i2 + 1 &
j1 = j2 ) or (
i1 = i2 &
j1 = j2 + 1 ) )
by A23, A27, JORDAN8:3;
A33:
1
<= i1
by A28, MATRIX_0:32;
A34:
( 1
<= j1 &
j1 <= width (Gauge (C,n)) )
by A28, MATRIX_0:32;
A35:
i2 <= len (Gauge (C,n))
by A30, MATRIX_0:32;
A36:
i1 <= len (Gauge (C,n))
by A28, MATRIX_0:32;
A37:
j2 <= width (Gauge (C,n))
by A30, MATRIX_0:32;
A38:
( 1
<= i2 & 1
<= j2 )
by A30, MATRIX_0:32;
A39:
(
Center (Gauge (C,n)) <= len (Gauge (C,n)) &
i1 + 1
>= 1 )
by JORDAN1B:13, NAT_1:11;
now ((Rev (Lower_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 A32;
suppose
(
i1 = i2 &
j1 + 1
= j2 )
;
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2then ((Rev (Lower_Seq (C,n))) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A29, A33, A36, A34, GOBOARD5:2
.=
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1
by A31, A35, A38, A37, GOBOARD5:2
;
hence
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A13, A25, NAT_1:13, NAT_1:14;
verum end; suppose A40:
(
i1 + 1
= i2 &
j1 = j2 )
;
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2A41:
now not ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2assume
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
;
contradictionthen
(Rev (Lower_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 A43:
(Rev (Lower_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;
A44:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
<= (E-max (L~ (Cage (C,n)))) `1
by A7, EUCLID:52;
(
L~ (Rev (Lower_Seq (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))),
E-max (L~ (Cage (C,n))) &
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )
by A6, A19, A12, EUCLID:52, TOPREAL1:25;
then A45:
L~ (Rev (Lower_Seq (C,n))) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)
by A44, JORDAN6:49;
A46:
(Rev (Lower_Seq (C,n))) /. ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) = First_Point (
(L~ (Rev (Lower_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 A1, A4, A20, Th48, FINSEQ_5:38;
A47:
k + 1
>= 1
+ 1
by A23, XREAL_1:7;
len (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) =
(((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) -' 1) + 1
by A22, A26, JORDAN4:8
.=
(First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))
by A22, XREAL_1:235
;
then A48:
rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) c= L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))))
by A25, A47, SPPOL_2:18, XXREAL_0:2;
A49:
k + 1
in dom (Rev (Lower_Seq (C,n)))
by A24, A27, FINSEQ_3:25;
(
Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is
closed &
Rev (Lower_Seq (C,n)) is
being_S-Seq )
by JORDAN6:30;
then A50:
(L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Rev (Lower_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 A1, A4, A20, A19, A12, A45, A42, Th48, Th50;
A51:
(
mid (
(Rev (Lower_Seq (C,n))),1,
((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))
= (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) &
(Rev (Lower_Seq (C,n))) | (Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))) = (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) )
by A22, FINSEQ_1:def 15, FINSEQ_6:116;
k + 1
in Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))
by A24, A25, FINSEQ_1:1;
then
(Rev (Lower_Seq (C,n))) /. (k + 1) in rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))))
by A51, A49, PARTFUN2:18;
then
(Rev (Lower_Seq (C,n))) /. (k + 1) in {(First_Point ((L~ (Rev (Lower_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 A43, A48, A50, XBOOLE_0:def 4;
then
(Rev (Lower_Seq (C,n))) /. (k + 1) = First_Point (
(L~ (Rev (Lower_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 A25, A21, A49, A46, PARTFUN2:10;
verum end;
i1 < Center (Gauge (C,n))
by A13, A25, A29, A36, A34, A18, A14, A15, JORDAN1A:18, NAT_1:13, NAT_1:14;
then
i1 + 1
<= Center (Gauge (C,n))
by NAT_1:13;
then
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A31, A34, A14, A15, A39, A40, JORDAN1A:18;
hence
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A41, XXREAL_0:1;
verum end; suppose
(
i1 = i2 + 1 &
j1 = j2 )
;
((Rev (Lower_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
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((Rev (Lower_Seq (C,n))) /. k) `1
by A29, A31, A36, A34, A38, A37, JORDAN1A:18;
hence
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A13, A25, NAT_1:13, NAT_1:14, XXREAL_0:2;
verum end; suppose
(
i1 = i2 &
j1 = j2 + 1 )
;
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2then ((Rev (Lower_Seq (C,n))) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A29, A33, A36, A34, GOBOARD5:2
.=
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1
by A31, A35, A38, A37, GOBOARD5:2
;
hence
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A13, A25, NAT_1:13, NAT_1:14;
verum end; end; end;
hence
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
;
verum
end;
A52:
S1[1]
proof
assume that
1
<= 1
and
1
< (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))
;
((Rev (Lower_Seq (C,n))) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
(Rev (Lower_Seq (C,n))) /. 1 =
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by FINSEQ_5:65
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
hence
((Rev (Lower_Seq (C,n))) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A6, EUCLID:52;
verum
end;
A53:
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A52, A8);
let k be Nat; ( 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) )
; ((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
hence
((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A53; verum