let C be Simple_closed_curve; :: thesis: for i, j, k, n being Nat st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i < len (Gauge (C,n))
let i, j, k, n be Nat; :: thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies i < len (Gauge (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span (C,n)) and
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; :: thesis: i < len (Gauge (C,n))
A6: len (Span (C,n)) > 4 by GOBOARD7:34;
SpanStart (C,n) in BDD C by A1, Th6;
then A7: E-bound C >= E-bound (BDD C) by JORDAN1C:7;
A8: 1 <= j by A4, MATRIX_0:32;
k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25;
then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2;
then A9: E-bound (L~ (Span (C,n))) >= ((Gauge (C,n)) * (i,j)) `1 by A5, PSCOMP_1:24;
A10: BDD C c= Cl (BDD C) by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then A12: Cl (BDD C) is compact by TOPREAL6:79;
SpanStart (C,n) in BDD C by A1, Th6;
then A13: E-bound (BDD C) = E-bound (Cl (BDD C)) by A11, TOPREAL6:86;
L~ (Span (C,n)) c= BDD C by A1, Th21;
then E-bound (L~ (Span (C,n))) <= E-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:67, XBOOLE_1:1;
then A14: E-bound (BDD C) >= ((Gauge (C,n)) * (i,j)) `1 by A13, A9, XXREAL_0:2;
A15: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then len (Gauge (C,n)) >= 1 + 1 by XXREAL_0:2;
then A16: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
A17: (len (Gauge (C,n))) -' 1 >= 1 by A16, XREAL_0:def 2;
A18: j <= width (Gauge (C,n)) by A4, MATRIX_0:32;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A8, A18, JORDAN8:12;
then A19: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 >= ((Gauge (C,n)) * (i,j)) `1 by A7, A14, XXREAL_0:2;
i <= len (Gauge (C,n)) by A4, MATRIX_0:32;
then i <= (len (Gauge (C,n))) -' 1 by A8, A18, A17, A19, GOBOARD5:3;
then i < ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
hence i < len (Gauge (C,n)) by A15, XREAL_1:235, XXREAL_0:2; :: thesis: verum