let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat
for f being non constant standard special_circular_sequence st f is_sequence_on Gauge (C,n) & ( for k being Element of 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 Element of 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; for f being non constant standard special_circular_sequence st f is_sequence_on Gauge (C,n) & ( for k being Element of 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 Element of 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; ( f is_sequence_on Gauge (C,n) & ( for k being Element of 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 Element of 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 Element of 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 )
; ( for i being Element of 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 Element of NAT by ORDINAL1:def 12;
consider i, j being Element of 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 Element of 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))
; 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_1:38;
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_1:38;
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_1:38;
A28:
j <= width (Gauge (C,n))
by A5, MATRIX_1:38;
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_1:36;
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:
n in NAT
by ORDINAL1:def 12;
then A47:
((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `2 = N-bound C
by A9, A34, JORDAN8:14;
A48:
N-min C = |[((N-min C) `1),((N-min C) `2)]|
by EUCLID:53;
A49:
( (NW-corner C) `2 = N-bound C & (NE-corner C) `2 = N-bound C )
by EUCLID:52;
A50:
( (NW-corner C) `1 = W-bound C & (NE-corner C) `1 = E-bound C )
by EUCLID:52;
A51:
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 A52:
((Gauge (C,n)) * (i9,((len (Gauge (C,n))) -' 1))) `1 < (N-min C) `1
by A11, A14, A33, A37, A43, A48, A15, A47, XXREAL_0:1;
A53:
((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
;
N-min (L~ f) = f /. 1then A54:
m + 1
<= len f
by NAT_1:13;
then consider i1,
j1,
i2,
j2 being
Element of
NAT such that A55:
(
[i1,j1] in Indices (Gauge (C,n)) &
f /. m = (Gauge (C,n)) * (
i1,
j1) )
and A56:
[i2,j2] in Indices (Gauge (C,n))
and A57:
f /. (m + 1) = (Gauge (C,n)) * (
i2,
j2)
and A58:
( (
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;
A59:
right_cell (
f,
m,
(Gauge (C,n)))
meets C
by A2, A45, A54;
then consider p being
set such that A60:
p in right_cell (
f,
m,
(Gauge (C,n)))
and A61:
p in C
by XBOOLE_0:3;
reconsider p =
p as
Point of
(TOP-REAL 2) by A60;
A62:
(
W-bound C <= p `1 &
p `1 <= E-bound C )
by A61, PSCOMP_1:24;
A63:
(N-min C) `2 = N-bound C
by EUCLID:52;
then A64:
p `2 <= (N-min C) `2
by A61, PSCOMP_1:24;
A65:
((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2
by A51, A24, A25, A26, GOBOARD5:4;
A66:
((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 = N-bound C
by A24, A46, JORDAN8:14;
A67:
j2 <= len (Gauge (C,n))
by A51, A56, MATRIX_1:38;
now 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, A55, A58, GOBOARD1:5;
suppose A68:
(
i + 1
= i2 &
len (Gauge (C,n)) = j2 )
;
N-min (L~ f) = f /. 1A69:
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 A51, 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, A54, A56, A57, A68, GOBRD13:24;
then consider r,
s being
Real such that A70:
p = |[r,s]|
and
((Gauge (C,n)) * (i,1)) `1 <= r
and A71:
r <= ((Gauge (C,n)) * ((i + 1),1)) `1
and A72:
((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 A60, A69;
p `2 = s
by A70, EUCLID:52;
then
p `2 = N-bound C
by A63, A64, A66, A72, XXREAL_0:1;
then
p in LSeg (
(NW-corner C),
(NE-corner C))
by A50, A49, A62, GOBOARD7:8;
then
p in (LSeg ((NW-corner C),(NE-corner C))) /\ C
by A61, XBOOLE_0:def 4;
then A73:
(N-min C) `1 <= p `1
by PSCOMP_1:39;
p `1 = r
by A70, EUCLID:52;
then
(N-min C) `1 <= ((Gauge (C,n)) * ((i + 1),1)) `1
by A71, A73, XXREAL_0:2;
then A74:
N-min C in cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
by A33, A4, A7, A6, A36, A53, A42, A44, A48, A63, A66, A65, A69;
N-min C <> (Gauge (C,n)) * (
i,
((len (Gauge (C,n))) -' 1))
by A34, A33, A19, A25, A26, A52, A39, SPRECT_3:13;
hence
N-min (L~ f) = f /. 1
by A9, A10, A11, A13, A14, A33, A4, A7, A6, A19, A36, A41, A74, Th31;
verum end; suppose
(
i = i2 + 1 &
len (Gauge (C,n)) = j2 )
;
N-min (L~ f) = f /. 1then
(
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, A54, A56, A57, GOBRD13:26, NAT_1:13;
hence
N-min (L~ f) = f /. 1
by A2, A45, A54, JORDAN8:15;
verum end; suppose A75:
(
i = i2 &
len (Gauge (C,n)) = j2 + 1 )
;
N-min (L~ f) = f /. 1then A76:
j2 = (len (Gauge (C,n))) -' 1
by NAT_D:34;
then A77:
right_cell (
f,
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
(i -' 1),
((len (Gauge (C,n))) -' 1))
by A1, A45, A5, A6, A36, A54, A56, A57, A75, GOBRD13:28;
m -' 1
<= m
by NAT_D:35;
then A78:
m -' 1
<= len f
by A21, XXREAL_0:2;
now
1
<= i9 + 1
by A9, NAT_1:13;
then A79:
((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 A80:
m = 1
;
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, A57, A75, A76, A80, A79, GOBOARD5:4;
verum then
m > 1
by A45, XXREAL_0:1;
then A81:
m -' 1
>= 1
by NAT_D:49;
A82:
(m -' 1) + 1
= m
by A45, XREAL_1:235;
then consider i19,
j19,
i29,
j29 being
Element of
NAT such that A83:
[i19,j19] in Indices (Gauge (C,n))
and A84:
f /. (m -' 1) = (Gauge (C,n)) * (
i19,
j19)
and A85:
(
[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, A81, JORDAN8:3;
A86:
1
<= i19
by A83, MATRIX_1:38;
A87:
i19 <= len (Gauge (C,n))
by A83, MATRIX_1:38;
now 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, A85, GOBOARD1:5;
suppose A88:
(
i19 = i &
j19 + 1
= len (Gauge (C,n)) )
;
contradictionthen
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, A81, A82, A83, A84, A88, GOBRD13:21;
hence
contradiction
by A2, A21, A59, A77, A81, A82;
verum end; suppose A89:
(
i19 + 1
= i &
j19 = len (Gauge (C,n)) )
;
contradictionA90:
(
((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, A86, A87, GOBOARD5:1;
m -' 1
in dom f
by A81, A78, FINSEQ_3:25;
then A91:
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, A84, A89, A90, GOBOARD7:8;
then A92:
f /. (m -' 1) in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f)
by A91, XBOOLE_0:def 4;
i19 < i
by A89, NAT_1:13;
then
(f /. (m -' 1)) `1 < (f /. m) `1
by A6, A27, A22, A28, A36, A84, A86, A89, GOBOARD5:3;
hence
contradiction
by A4, A7, A92, PSCOMP_1:39;
verum end; suppose
(
i19 = i + 1 &
j19 = len (Gauge (C,n)) )
;
contradictionthen
right_cell (
f,
(m -' 1),
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i,
(len (Gauge (C,n))))
by A1, A21, A5, A6, A36, A81, A82, A83, A84, GOBRD13:26;
hence
contradiction
by A2, A21, A27, A81, A82, JORDAN8:15;
verum end; hence
N-min (L~ f) = f /. 1
;
verum end; hence
N-min (L~ f) = f /. 1
;
verum end;