let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat
for f being non constant standard special_circular_sequence st f is_sequence_on Gauge (C,n) & ( for k being Nat st 1 <= k & k + 1 <= len f holds
( left_cell (f,k,(Gauge (C,n))) misses C & right_cell (f,k,(Gauge (C,n))) meets C ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) holds
N-min (L~ f) = f /. 1
let n be Nat; :: thesis: for f being non constant standard special_circular_sequence st f is_sequence_on Gauge (C,n) & ( for k being Nat st 1 <= k & k + 1 <= len f holds
( left_cell (f,k,(Gauge (C,n))) misses C & right_cell (f,k,(Gauge (C,n))) meets C ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) holds
N-min (L~ f) = f /. 1
set G = Gauge (C,n);
let f be non constant standard special_circular_sequence; :: thesis: ( f is_sequence_on Gauge (C,n) & ( for k being Nat st 1 <= k & k + 1 <= len f holds
( left_cell (f,k,(Gauge (C,n))) misses C & right_cell (f,k,(Gauge (C,n))) meets C ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) implies N-min (L~ f) = f /. 1 )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: for k being Nat st 1 <= k & k + 1 <= len f holds
( left_cell (f,k,(Gauge (C,n))) misses C & right_cell (f,k,(Gauge (C,n))) meets C ) ; :: thesis: ( for i being Nat holds
( not 1 <= i or not i + 1 <= len (Gauge (C,n)) or not f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) or not f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) or not N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) or not N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) or N-min (L~ f) = f /. 1 )
N-min (L~ f) in rng f by SPRECT_2:39;
then consider m being Nat such that
A3: m in dom f and
A4: f . m = N-min (L~ f) by FINSEQ_2:10;
reconsider m = m as Nat ;
consider i, j being Nat such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: f /. m = (Gauge (C,n)) * (i,j) by A1, A3, GOBOARD1:def 9;
A7: f /. m = f . m by A3, PARTFUN1:def 6;
A8: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
given i9 being Nat such that A9: 1 <= i9 and
A10: i9 + 1 <= len (Gauge (C,n)) and
A11: f /. 1 = (Gauge (C,n)) * (i9,(width (Gauge (C,n)))) and
A12: f /. 2 = (Gauge (C,n)) * ((i9 + 1),(width (Gauge (C,n)))) and
A13: N-min C in cell ((Gauge (C,n)),i9,((width (Gauge (C,n))) -' 1)) and
A14: N-min C <> (Gauge (C,n)) * (i9,((width (Gauge (C,n))) -' 1)) ; :: thesis: N-min (L~ f) = f /. 1
A15: ( (Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1)) = |[(((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `1),(((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `2)]| & (N-min C) `2 = N-bound C ) by EUCLID:52, EUCLID:53;
(Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A5, JORDAN8:def 1;
then A16: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)) = N-bound (L~ f) by A4, A7, A8, A6, EUCLID:52;
N-bound C > S-bound C by JORDAN8:9;
then ( 2 |^ n > 0 & (N-bound C) - (S-bound C) > 0 ) by NEWTON:83, XREAL_1:50;
then A17: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by XREAL_1:139;
A18: ( (NW-corner (L~ f)) `1 = W-bound (L~ f) & (NE-corner (L~ f)) `1 = E-bound (L~ f) ) by EUCLID:52;
A19: 1 <= i by A5, MATRIX_0:32;
A20: ( (NW-corner (L~ f)) `2 = N-bound (L~ f) & (NE-corner (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:52;
A21: m <= len f by A3, FINSEQ_3:25;
A22: 1 <= j by A5, MATRIX_0:32;
len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def 1;
then A23: len (Gauge (C,n)) >= 3 by NAT_1:12;
then A24: 1 < len (Gauge (C,n)) by XXREAL_0:2;
then A25: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;
then A26: (len (Gauge (C,n))) -' 1 < len (Gauge (C,n)) by NAT_D:51;
A27: i <= len (Gauge (C,n)) by A5, MATRIX_0:32;
A28: j <= width (Gauge (C,n)) by A5, MATRIX_0:32;
then A29: ((Gauge (C,n)) * (i,j)) `2 = ((Gauge (C,n)) * (1,j)) `2 by A19, A27, A22, GOBOARD5:1;
A30: len f > 4 by GOBOARD7:34;
1 in dom f by FINSEQ_5:6;
then A31: f /. 1 in L~ f by A30, GOBOARD1:1, XXREAL_0:2;
then A32: N-bound (L~ f) >= (f /. 1) `2 by PSCOMP_1:24;
A33: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A34: i9 < len (Gauge (C,n)) by A10, NAT_1:13;
then ((Gauge (C,n)) * (i9,j)) `2 = ((Gauge (C,n)) * (1,j)) `2 by A9, A22, A28, GOBOARD5:1;
then ((Gauge (C,n)) * (i,j)) `2 <= ((Gauge (C,n)) * (i9,(len (Gauge (C,n))))) `2 by A9, A34, A33, A22, A28, A29, SPRECT_3:12;
then A35: N-bound (L~ f) = (f /. 1) `2 by A11, A33, A4, A7, A8, A6, A32, XXREAL_0:1;
[i9,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A9, A34, A33, A24, MATRIX_0:30;
then (Gauge (C,n)) * (i9,(len (Gauge (C,n)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i9 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| by JORDAN8:def 1;
then (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)) = N-bound (L~ f) by A11, A33, A35, EUCLID:52;
then A36: (len (Gauge (C,n))) - 2 = j - 2 by A17, A16, XCMPLX_1:5;
then A37: ((Gauge (C,n)) * (i9,(len (Gauge (C,n))))) `1 = ((Gauge (C,n)) * (i9,1)) `1 by A9, A34, A33, A22, GOBOARD5:2;
( W-bound (L~ f) <= (f /. 1) `1 & (f /. 1) `1 <= E-bound (L~ f) ) by A31, PSCOMP_1:24;
then f /. 1 in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A35, A18, A20, GOBOARD7:8;
then f /. 1 in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) by A31, XBOOLE_0:def 4;
then A38: (N-min (L~ f)) `1 <= (f /. 1) `1 by PSCOMP_1:39;
then A39: i <= i9 by A9, A11, A33, A4, A7, A6, A27, A22, A36, GOBOARD5:3;
then A40: i < len (Gauge (C,n)) by A34, XXREAL_0:2;
then A41: i + 1 <= len (Gauge (C,n)) by NAT_1:13;
A42: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A23, XREAL_1:235, XXREAL_0:2;
then N-min C in { |[r9,s9]| where r9, s9 is Real : ( ((Gauge (C,n)) * (i9,1)) `1 <= r9 & r9 <= ((Gauge (C,n)) * ((i9 + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= s9 & s9 <= ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 ) } by A9, A13, A34, A33, A25, A26, GOBRD11:32;
then ex r9, s9 being Real st
( N-min C = |[r9,s9]| & ((Gauge (C,n)) * (i9,1)) `1 <= r9 & r9 <= ((Gauge (C,n)) * ((i9 + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= s9 & s9 <= ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 ) ;
then A43: (f /. 1) `1 <= (N-min C) `1 by A11, A33, A37, EUCLID:52;
then A44: (N-min (L~ f)) `1 <= (N-min C) `1 by A38, XXREAL_0:2;
A45: 1 <= m by A3, FINSEQ_3:25;
A46: ((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `2 = N-bound C by A9, A34, JORDAN8:14;
A47: N-min C = |[((N-min C) `1),((N-min C) `2)]| by EUCLID:53;
A48: ( (NW-corner C) `2 = N-bound C & (NE-corner C) `2 = N-bound C ) by EUCLID:52;
A49: ( (NW-corner C) `1 = W-bound C & (NE-corner C) `1 = E-bound C ) by EUCLID:52;
A50: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `1 = ((Gauge (C,n)) * (i9,1)) `1 by A9, A34, A33, A25, A26, GOBOARD5:2;
then A51: ((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `1 < (N-min C) `1 by A11, A14, A33, A37, A43, A47, A15, A46, XXREAL_0:1;
A52: ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `1 = ((Gauge (C,n)) * (i,1)) `1 by A19, A27, A22, A28, A36, GOBOARD5:2;
per cases ( m = len f or m < len f ) by A21, XXREAL_0:1;
suppose m = len f ; :: thesis: N-min (L~ f) = f /. 1
hence N-min (L~ f) = f /. 1 by A4, A7, FINSEQ_6:def 1; :: thesis: verum
end;
suppose m < len f ; :: thesis: N-min (L~ f) = f /. 1
then A53: m + 1 <= len f by NAT_1:13;
then consider i1, j1, i2, j2 being Nat such that
A54: ( [i1,j1] in Indices (Gauge (C,n)) & f /. m = (Gauge (C,n)) * (i1,j1) ) and
A55: [i2,j2] in Indices (Gauge (C,n)) and
A56: f /. (m + 1) = (Gauge (C,n)) * (i2,j2) and
A57: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A45, JORDAN8:3;
A58: right_cell (f,m,(Gauge (C,n))) meets C by A2, A45, A53;
then consider p being object such that
A59: p in right_cell (f,m,(Gauge (C,n))) and
A60: p in C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A59;
A61: ( W-bound C <= p `1 & p `1 <= E-bound C ) by A60, PSCOMP_1:24;
A62: (N-min C) `2 = N-bound C by EUCLID:52;
then A63: p `2 <= (N-min C) `2 by A60, PSCOMP_1:24;
A64: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 by A50, A24, A25, A26, GOBOARD5:4;
A65: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 = N-bound C by A24, JORDAN8:14;
A66: j2 <= len (Gauge (C,n)) by A50, A55, MATRIX_0:32;
now :: thesis: N-min (L~ f) = f /. 1
per cases ( ( i = i2 & (len (Gauge (C,n))) + 1 = j2 ) or ( i + 1 = i2 & len (Gauge (C,n)) = j2 ) or ( i = i2 + 1 & len (Gauge (C,n)) = j2 ) or ( i = i2 & len (Gauge (C,n)) = j2 + 1 ) ) by A5, A6, A36, A54, A57, GOBOARD1:5;
suppose ( i = i2 & (len (Gauge (C,n))) + 1 = j2 ) ; :: thesis: N-min (L~ f) = f /. 1
hence N-min (L~ f) = f /. 1 by A66, NAT_1:13; :: thesis: verum
end;
suppose A67: ( i + 1 = i2 & len (Gauge (C,n)) = j2 ) ; :: thesis: N-min (L~ f) = f /. 1
A68: cell ((Gauge (C,n)),i,((len (Gauge (C,n))) -' 1)) = { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= s & s <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 ) } by A50, A19, A25, A26, A40, GOBRD11:32;
right_cell (f,m,(Gauge (C,n))) = cell ((Gauge (C,n)),i,((len (Gauge (C,n))) -' 1)) by A1, A45, A5, A6, A36, A53, A55, A56, A67, GOBRD13:24;
then consider r, s being Real such that
A69: p = |[r,s]| and
((Gauge (C,n)) * (i,1)) `1 <= r and
A70: r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A71: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= s and
s <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A59, A68;
p `2 = s by A69, EUCLID:52;
then p `2 = N-bound C by A62, A63, A65, A71, XXREAL_0:1;
then p in LSeg ((NW-corner C),(NE-corner C)) by A49, A48, A61, GOBOARD7:8;
then p in (LSeg ((NW-corner C),(NE-corner C))) /\ C by A60, XBOOLE_0:def 4;
then A72: (N-min C) `1 <= p `1 by PSCOMP_1:39;
p `1 = r by A69, EUCLID:52;
then (N-min C) `1 <= ((Gauge (C,n)) * ((i + 1),1)) `1 by A70, A72, XXREAL_0:2;
then A73: N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) by A33, A4, A7, A6, A36, A52, A42, A44, A47, A62, A65, A64, A68;
N-min C <> (Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1)) by A34, A33, A19, A25, A26, A51, A39, SPRECT_3:13;
hence N-min (L~ f) = f /. 1 by A9, A10, A11, A13, A14, A33, A4, A7, A6, A19, A36, A41, A73, Th29; :: thesis: verum
end;
suppose ( i = i2 + 1 & len (Gauge (C,n)) = j2 ) ; :: thesis: N-min (L~ f) = f /. 1
then ( right_cell (f,m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(len (Gauge (C,n)))) & i2 < len (Gauge (C,n)) ) by A1, A45, A5, A6, A27, A36, A53, A55, A56, GOBRD13:26, NAT_1:13;
hence N-min (L~ f) = f /. 1 by A2, A45, A53, JORDAN8:15; :: thesis: verum
end;
suppose A74: ( i = i2 & len (Gauge (C,n)) = j2 + 1 ) ; :: thesis: N-min (L~ f) = f /. 1
then A75: j2 = (len (Gauge (C,n))) -' 1 by NAT_D:34;
then A76: right_cell (f,m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i -' 1),((len (Gauge (C,n))) -' 1)) by A1, A45, A5, A6, A36, A53, A55, A56, A74, GOBRD13:28;
m -' 1 <= m by NAT_D:35;
then A77: m -' 1 <= len f by A21, XXREAL_0:2;
now :: thesis: not m = 1
1 <= i9 + 1 by A9, NAT_1:13;
then A78: ((Gauge (C,n)) * ((i9 + 1),(len (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 by A10, A33, A24, GOBOARD5:1;
assume A79: m = 1 ; :: thesis: contradiction
((Gauge (C,n)) * (i9,(len (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 by A9, A34, A33, A24, GOBOARD5:1;
hence contradiction by A11, A12, A33, A6, A19, A27, A36, A25, A26, A56, A74, A75, A79, A78, GOBOARD5:4; :: thesis: verum
end;
then m > 1 by A45, XXREAL_0:1;
then A80: m -' 1 >= 1 by NAT_D:49;
A81: (m -' 1) + 1 = m by A45, XREAL_1:235;
then consider i19, j19, i29, j29 being Nat such that
A82: [i19,j19] in Indices (Gauge (C,n)) and
A83: f /. (m -' 1) = (Gauge (C,n)) * (i19,j19) and
A84: ( [i29,j29] in Indices (Gauge (C,n)) & f /. m = (Gauge (C,n)) * (i29,j29) & ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) ) by A1, A21, A80, JORDAN8:3;
A85: 1 <= i19 by A82, MATRIX_0:32;
A86: i19 <= len (Gauge (C,n)) by A82, MATRIX_0:32;
now :: thesis: contradiction
per cases ( ( i19 = i & j19 + 1 = len (Gauge (C,n)) ) or ( i19 + 1 = i & j19 = len (Gauge (C,n)) ) or ( i19 = i + 1 & j19 = len (Gauge (C,n)) ) or ( i19 = i & j19 = (len (Gauge (C,n))) + 1 ) ) by A5, A6, A36, A84, GOBOARD1:5;
suppose A87: ( i19 = i & j19 + 1 = len (Gauge (C,n)) ) ; :: thesis: contradiction
then j19 = (len (Gauge (C,n))) -' 1 by NAT_D:34;
then left_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i -' 1),((len (Gauge (C,n))) -' 1)) by A1, A21, A5, A6, A36, A80, A81, A82, A83, A87, GOBRD13:21;
hence contradiction by A2, A21, A58, A76, A80, A81; :: thesis: verum
end;
suppose A88: ( i19 + 1 = i & j19 = len (Gauge (C,n)) ) ; :: thesis: contradiction
A89: ( ((Gauge (C,n)) * (i19,j)) `2 = ((Gauge (C,n)) * (1,j)) `2 & ((Gauge (C,n)) * (i,j)) `2 = ((Gauge (C,n)) * (1,j)) `2 ) by A19, A27, A22, A28, A85, A86, GOBOARD5:1;
m -' 1 in dom f by A80, A77, FINSEQ_3:25;
then A90: f /. (m -' 1) in L~ f by A30, GOBOARD1:1, XXREAL_0:2;
then ( W-bound (L~ f) <= (f /. (m -' 1)) `1 & (f /. (m -' 1)) `1 <= E-bound (L~ f) ) by PSCOMP_1:24;
then f /. (m -' 1) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A4, A7, A8, A6, A36, A18, A20, A83, A88, A89, GOBOARD7:8;
then A91: f /. (m -' 1) in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) by A90, XBOOLE_0:def 4;
i19 < i by A88, NAT_1:13;
then (f /. (m -' 1)) `1 < (f /. m) `1 by A6, A27, A22, A28, A36, A83, A85, A88, GOBOARD5:3;
hence contradiction by A4, A7, A91, PSCOMP_1:39; :: thesis: verum
end;
suppose ( i19 = i + 1 & j19 = len (Gauge (C,n)) ) ; :: thesis: contradiction
then right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) by A1, A21, A5, A6, A36, A80, A81, A82, A83, GOBRD13:26;
hence contradiction by A2, A21, A27, A80, A81, JORDAN8:15; :: thesis: verum
end;
suppose ( i19 = i & j19 = (len (Gauge (C,n))) + 1 ) ; :: thesis: contradiction
then (len (Gauge (C,n))) + 1 <= (len (Gauge (C,n))) + 0 by A50, A82, MATRIX_0:32;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
end;
end;
hence N-min (L~ f) = f /. 1 ; :: thesis: verum
end;
end;
end;
hence N-min (L~ f) = f /. 1 ; :: thesis: verum
end;
end;