:: JORDAN1D semantic presentation
begin
1 = (2 * 0) + 1
;
then Lm1: 1 div 2 = 0
by NAT_D:def_1;
2 = (2 * 1) + 0
;
then Lm2: 2 div 2 = 1
by NAT_D:def_1;
Lm3: for x, A, B, C, D being set holds
( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) )
proof
let x, A, B, C, D be set ; ::_thesis: ( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) )
hereby ::_thesis: ( ( x in A or x in B or x in C or x in D ) implies x in ((A \/ B) \/ C) \/ D )
assume x in ((A \/ B) \/ C) \/ D ; ::_thesis: ( x in A or x in B or x in C or x in D )
then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def_3;
then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def_3;
hence ( x in A or x in B or x in C or x in D ) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume ( x in A or x in B or x in C or x in D ) ; ::_thesis: x in ((A \/ B) \/ C) \/ D
then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def_3;
then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def_3;
hence x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; ::_thesis: verum
end;
Lm4: for A, B, C, D being set holds union {A,B,C,D} = ((A \/ B) \/ C) \/ D
proof
let A, B, C, D be set ; ::_thesis: union {A,B,C,D} = ((A \/ B) \/ C) \/ D
A1: B in {A,B,C,D} by ENUMSET1:def_2;
A2: D in {A,B,C,D} by ENUMSET1:def_2;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((A \/ B) \/ C) \/ D c= union {A,B,C,D}
let x be set ; ::_thesis: ( x in union {A,B,C,D} implies x in ((A \/ B) \/ C) \/ D )
assume x in union {A,B,C,D} ; ::_thesis: x in ((A \/ B) \/ C) \/ D
then consider Z being set such that
A3: x in Z and
A4: Z in {A,B,C,D} by TARSKI:def_4;
( Z = A or Z = B or Z = C or Z = D ) by A4, ENUMSET1:def_2;
hence x in ((A \/ B) \/ C) \/ D by A3, Lm3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((A \/ B) \/ C) \/ D or x in union {A,B,C,D} )
A5: C in {A,B,C,D} by ENUMSET1:def_2;
assume x in ((A \/ B) \/ C) \/ D ; ::_thesis: x in union {A,B,C,D}
then A6: ( x in A or x in B or x in C or x in D ) by Lm3;
A in {A,B,C,D} by ENUMSET1:def_2;
hence x in union {A,B,C,D} by A6, A1, A5, A2, TARSKI:def_4; ::_thesis: verum
end;
theorem Th1: :: JORDAN1D:1
for A, B being set st ( for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ) holds
union A c= union B
proof
let A, B be set ; ::_thesis: ( ( for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ) implies union A c= union B )
assume A1: for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ; ::_thesis: union A c= union B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union A or a in union B )
assume a in union A ; ::_thesis: a in union B
then consider Z being set such that
A2: a in Z and
A3: Z in A by TARSKI:def_4;
consider K being set such that
A4: K c= B and
A5: Z c= union K by A1, A3;
ex S being set st
( a in S & S in K ) by A2, A5, TARSKI:def_4;
hence a in union B by A4, TARSKI:def_4; ::_thesis: verum
end;
registration
let m be non empty Element of NAT ;
cluster2 |^ m -> even ;
coherence
2 |^ m is even
proof
defpred S1[ Nat] means ( not m is empty implies 2 |^ m is even );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
S1[k] and
not k + 1 is empty ; ::_thesis: 2 |^ (k + 1) is even
2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6;
hence 2 |^ (k + 1) is even ; ::_thesis: verum
end;
A2: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence 2 |^ m is even ; ::_thesis: verum
end;
end;
registration
let n be even Element of NAT ;
let m be non empty Element of NAT ;
clustern |^ m -> even ;
coherence
n |^ m is even
proof
defpred S1[ Element of NAT ] means ( not n is empty implies n |^ n is even );
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
S1[k] and
not k + 1 is empty ; ::_thesis: n |^ (k + 1) is even
n |^ (k + 1) = n * (n |^ k) by NEWTON:6;
hence n |^ (k + 1) is even ; ::_thesis: verum
end;
A2: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1);
hence n |^ m is even ; ::_thesis: verum
end;
end;
theorem Th2: :: JORDAN1D:2
for i being Element of NAT
for r being real number st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i
proof
let i be Element of NAT ; ::_thesis: for r being real number st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i
let r be real number ; ::_thesis: ( r <> 0 implies (1 / r) * (r |^ (i + 1)) = r |^ i )
assume A1: r <> 0 ; ::_thesis: (1 / r) * (r |^ (i + 1)) = r |^ i
thus (1 / r) * (r |^ (i + 1)) = (1 / r) * ((r |^ i) * r) by NEWTON:6
.= ((1 / r) * r) * (r |^ i)
.= 1 * (r |^ i) by A1, XCMPLX_1:106
.= r |^ i ; ::_thesis: verum
end;
Lm5: now__::_thesis:_for_m_being_real_number_st_2_<=_m_holds_
(2_*_m)_-_2_>=_0
let m be real number ; ::_thesis: ( 2 <= m implies (2 * m) - 2 >= 0 )
assume 2 <= m ; ::_thesis: (2 * m) - 2 >= 0
then 2 * m >= 2 * 2 by XREAL_1:66;
then (2 * m) - 2 >= 4 - 2 by XREAL_1:9;
hence (2 * m) - 2 >= 0 ; ::_thesis: verum
end;
Lm6: now__::_thesis:_for_m_being_real_number_st_1_<=_m_holds_
(2_*_m)_-_1_>=_0
let m be real number ; ::_thesis: ( 1 <= m implies (2 * m) - 1 >= 0 )
assume 1 <= m ; ::_thesis: (2 * m) - 1 >= 0
then 2 * m >= 2 * 1 by XREAL_1:66;
then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;
hence (2 * m) - 1 >= 0 ; ::_thesis: verum
end;
Lm7: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_
(2_*_m)_-_2_=_(2_*_m)_-'_2
let m be Element of NAT ; ::_thesis: ( 2 <= m implies (2 * m) - 2 = (2 * m) -' 2 )
assume 2 <= m ; ::_thesis: (2 * m) - 2 = (2 * m) -' 2
then (2 * m) - 2 >= 0 by Lm5;
hence (2 * m) - 2 = (2 * m) -' 2 by XREAL_0:def_2; ::_thesis: verum
end;
Lm8: now__::_thesis:_for_m_being_Element_of_NAT_st_1_<=_m_holds_
(2_*_m)_-_1_=_(2_*_m)_-'_1
let m be Element of NAT ; ::_thesis: ( 1 <= m implies (2 * m) - 1 = (2 * m) -' 1 )
assume 1 <= m ; ::_thesis: (2 * m) - 1 = (2 * m) -' 1
then (2 * m) - 1 >= 0 by Lm6;
hence (2 * m) - 1 = (2 * m) -' 1 by XREAL_0:def_2; ::_thesis: verum
end;
Lm9: now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_1_holds_
((2_*_m)_-'_2)_+_1_=_(2_*_m)_-'_1
let m be Element of NAT ; ::_thesis: ( m >= 1 implies ((2 * m) -' 2) + 1 = (2 * m) -' 1 )
assume A1: m >= 1 ; ::_thesis: ((2 * m) -' 2) + 1 = (2 * m) -' 1
then 2 * m >= 2 * 1 by XREAL_1:64;
then (2 * m) - 1 >= 2 - 1 by XREAL_1:9;
then A2: (2 * m) -' 1 >= 1 by A1, Lm8;
thus ((2 * m) -' 2) + 1 = (((2 * m) -' 1) -' 1) + 1 by NAT_D:45
.= (2 * m) -' 1 by A2, XREAL_1:235 ; ::_thesis: verum
end;
Lm10: for m, i being Element of NAT
for x being real number st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
proof
let m, i be Element of NAT ; ::_thesis: for x being real number st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
let x be real number ; ::_thesis: ( 2 <= m implies (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) )
assume 2 <= m ; ::_thesis: (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
then A1: (2 * m) - 2 >= 0 by Lm5;
thus (x / (2 |^ i)) * (m - 2) = x / ((2 |^ i) / (m - 2)) by XCMPLX_1:81
.= x / (((2 |^ i) * 2) / ((m - 2) * 2)) by XCMPLX_1:91
.= (x / ((2 |^ i) * 2)) * ((m - 2) * 2) by XCMPLX_1:81
.= (x / (2 |^ (i + 1))) * (((2 * m) - 2) - 2) by NEWTON:6
.= (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) by A1, XREAL_0:def_2 ; ::_thesis: verum
end;
Lm11: for m being Element of NAT st 2 <= m holds
1 <= (2 * m) -' 2
proof
let m be Element of NAT ; ::_thesis: ( 2 <= m implies 1 <= (2 * m) -' 2 )
assume A1: 2 <= m ; ::_thesis: 1 <= (2 * m) -' 2
then 2 * 2 <= 2 * m by XREAL_1:66;
then A2: 4 - 2 <= (2 * m) - 2 by XREAL_1:9;
(2 * m) -' 2 = (2 * m) - 2 by A1, Lm7;
hence 1 <= (2 * m) -' 2 by A2, XXREAL_0:2; ::_thesis: verum
end;
Lm12: for m being Element of NAT st 1 <= m holds
1 <= (2 * m) -' 1
proof
let m be Element of NAT ; ::_thesis: ( 1 <= m implies 1 <= (2 * m) -' 1 )
assume A1: 1 <= m ; ::_thesis: 1 <= (2 * m) -' 1
then 2 * 1 <= 2 * m by XREAL_1:66;
then 2 - 1 <= (2 * m) - 1 by XREAL_1:9;
hence 1 <= (2 * m) -' 1 by A1, Lm8; ::_thesis: verum
end;
Lm13: for m, i being Element of NAT st m < (2 |^ i) + 3 holds
(2 * m) -' 2 < (2 |^ (i + 1)) + 3
proof
let m, i be Element of NAT ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )
percases ( m = 0 or m = 1 or 2 <= m ) by NAT_1:26;
suppose ( m = 0 or m = 1 ) ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )
hence ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) by NAT_2:8; ::_thesis: verum
end;
supposeA1: 2 <= m ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )
assume m < (2 |^ i) + 3 ; ::_thesis: (2 * m) -' 2 < (2 |^ (i + 1)) + 3
then m + 1 <= (2 |^ i) + 3 by NAT_1:13;
then 2 * (m + 1) <= 2 * ((2 |^ i) + 3) by XREAL_1:64;
then (2 * m) + (2 * 1) <= (2 * (2 |^ i)) + (2 * 3) ;
then (2 * m) + (2 * 1) <= (2 |^ (i + 1)) + 6 by NEWTON:6;
then ((2 * m) + 2) - 4 <= ((2 |^ (i + 1)) + 6) - 4 by XREAL_1:9;
then (2 * m) - 2 <= (2 |^ (i + 1)) + 2 ;
then A2: (2 * m) -' 2 <= (2 |^ (i + 1)) + 2 by A1, Lm7;
(2 |^ (i + 1)) + 2 < (2 |^ (i + 1)) + 3 by XREAL_1:6;
hence (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by A2, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
Lm14: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_
(((2_*_m)_-'_2)_+_1)_-_2_=_(2_*_m)_-_3
let m be Element of NAT ; ::_thesis: ( 2 <= m implies (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 )
assume 2 <= m ; ::_thesis: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3
hence (((2 * m) -' 2) + 1) - 2 = (((2 * m) - 2) + 1) - 2 by Lm7
.= (2 * m) - 3 ;
::_thesis: verum
end;
begin
theorem Th3: :: JORDAN1D:3
for m, i, a, b being Element of NAT
for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
proof
let m, i, a, b be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) implies ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 )
set I = Gauge (D,i);
set J = Gauge (D,(i + 1));
set z = N-bound D;
set e = E-bound D;
set s = S-bound D;
set w = W-bound D;
assume that
A1: 2 <= m and
A2: m < len (Gauge (D,i)) and
A3: 1 <= a and
A4: a <= len (Gauge (D,i)) and
A5: 1 <= b and
A6: b <= len (Gauge (D,(i + 1))) ; ::_thesis: ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
m < (2 |^ i) + 3 by A2, JORDAN8:def_1;
then (2 * m) -' 2 <= (2 |^ (i + 1)) + 3 by Lm13;
then A7: (2 * m) -' 2 <= len (Gauge (D,(i + 1))) by JORDAN8:def_1;
A8: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1;
1 <= (2 * m) -' 2 by A1, Lm11;
then A9: [((2 * m) -' 2),b] in Indices (Gauge (D,(i + 1))) by A5, A6, A8, A7, MATRIX_1:36;
A10: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1;
1 <= m by A1, XXREAL_0:2;
then [m,a] in Indices (Gauge (D,i)) by A2, A3, A4, A10, MATRIX_1:36;
hence ((Gauge (D,i)) * (m,a)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (a - 2)))]| `1 by JORDAN8:def_1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2)) by EUCLID:52
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)) by A1, Lm10
.= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (b - 2)))]| `1 by EUCLID:52
.= ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 by A9, JORDAN8:def_1 ;
::_thesis: verum
end;
theorem Th4: :: JORDAN1D:4
for n, i, a, b being Element of NAT
for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2
proof
let n, i, a, b be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2
let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) implies ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 )
set I = Gauge (D,i);
set J = Gauge (D,(i + 1));
set z = N-bound D;
set e = E-bound D;
set s = S-bound D;
set w = W-bound D;
assume that
A1: 2 <= n and
A2: n < len (Gauge (D,i)) and
A3: 1 <= a and
A4: a <= len (Gauge (D,i)) and
A5: 1 <= b and
A6: b <= len (Gauge (D,(i + 1))) ; ::_thesis: ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2
n < (2 |^ i) + 3 by A2, JORDAN8:def_1;
then (2 * n) -' 2 <= (2 |^ (i + 1)) + 3 by Lm13;
then A7: (2 * n) -' 2 <= len (Gauge (D,(i + 1))) by JORDAN8:def_1;
A8: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1;
1 <= (2 * n) -' 2 by A1, Lm11;
then A9: [b,((2 * n) -' 2)] in Indices (Gauge (D,(i + 1))) by A5, A6, A8, A7, MATRIX_1:36;
A10: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1;
1 <= n by A1, XXREAL_0:2;
then [a,n] in Indices (Gauge (D,i)) by A2, A3, A4, A10, MATRIX_1:36;
hence ((Gauge (D,i)) * (a,n)) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (a - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)))]| `2 by JORDAN8:def_1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)) by EUCLID:52
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)) by A1, Lm10
.= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (b - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)))]| `2 by EUCLID:52
.= ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 by A9, JORDAN8:def_1 ;
::_thesis: verum
end;
Lm15: for m, i being Element of NAT
for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge (D,i)) holds
(2 * m) -' 1 < len (Gauge (D,(i + 1)))
proof
let m, i be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge (D,i)) holds
(2 * m) -' 1 < len (Gauge (D,(i + 1)))
let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( m + 1 < len (Gauge (D,i)) implies (2 * m) -' 1 < len (Gauge (D,(i + 1))) )
assume m + 1 < len (Gauge (D,i)) ; ::_thesis: (2 * m) -' 1 < len (Gauge (D,(i + 1)))
then m + 1 < (2 |^ i) + 3 by JORDAN8:def_1;
then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ;
then A1: 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34;
(2 * m) -' 1 <= 2 * m by NAT_D:44;
then (2 * m) -' 1 < (2 |^ (i + 1)) + 3 by A1, XXREAL_0:2;
hence (2 * m) -' 1 < len (Gauge (D,(i + 1))) by JORDAN8:def_1; ::_thesis: verum
end;
theorem Th5: :: JORDAN1D:5
for m, i, n being Element of NAT
for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds
cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)))
proof
let m, i, n be Element of NAT ; ::_thesis: for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds
cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)))
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) implies cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) )
set I = Gauge (D,i);
set J = Gauge (D,(i + 1));
set z = N-bound D;
set e = E-bound D;
set s = S-bound D;
set w = W-bound D;
assume that
A1: 2 <= m and
A2: m + 1 < len (Gauge (D,i)) and
A3: 2 <= n and
A4: n + 1 < len (Gauge (D,i)) ; ::_thesis: cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)))
A5: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1;
A6: (2 * n) - 3 < (2 * n) - 2 by XREAL_1:15;
(N-bound D) - (S-bound D) >= 0 by SPRECT_1:22, XREAL_1:48;
then (((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3) <= (((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2) by A6, XREAL_1:64;
then A7: (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3)) <= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)) by XREAL_1:6;
A8: m <= m + 1 by NAT_1:11;
A9: ((2 * (n + 1)) -' 2) - 2 = (((2 * n) + (2 * 1)) -' 2) - 2
.= (2 * n) - 2 by NAT_D:34 ;
A10: 1 <= ((2 * m) -' 2) + 1 by NAT_1:11;
A11: 1 <= len (Gauge (D,(i + 1))) by GOBRD11:34;
A12: 1 <= n by A3, XXREAL_0:2;
then A13: 1 <= (2 * n) -' 1 by Lm12;
(2 * n) -' 1 <= 2 * n by NAT_D:35;
then A14: 1 <= 2 * n by A13, XXREAL_0:2;
A15: ((2 * n) -' 1) + 1 = 2 * n by A12, Lm12, NAT_D:43;
A16: (2 * n) -' 1 < len (Gauge (D,(i + 1))) by A4, Lm15;
then ((2 * n) -' 1) + 1 <= len (Gauge (D,(i + 1))) by NAT_1:13;
then [1,(2 * n)] in Indices (Gauge (D,(i + 1))) by A5, A15, A11, A14, MATRIX_1:36;
then A17: ((Gauge (D,(i + 1))) * (1,(2 * n))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)))]| `2 by JORDAN8:def_1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)) by EUCLID:52 ;
A18: (2 * m) -' 1 = (2 * m) - 1 by A1, Lm8, XXREAL_0:2;
A19: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 by A1, Lm14;
A20: 1 <= ((2 * n) -' 2) + 1 by NAT_1:11;
A21: (2 * m) -' 1 < len (Gauge (D,(i + 1))) by A2, Lm15;
A22: n <= n + 1 by NAT_1:11;
A23: ((2 * n) -' 2) + 1 = (2 * n) -' 1 by A3, Lm9, XXREAL_0:2;
A24: ((2 * (m + 1)) -' 2) - 2 = (((2 * m) + (2 * 1)) -' 2) - 2
.= (2 * m) - 2 by NAT_D:34 ;
A25: m < len (Gauge (D,i)) by A2, NAT_1:13;
then m < (2 |^ i) + 3 by JORDAN8:def_1;
then (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then A26: (2 * m) -' 2 < len (Gauge (D,(i + 1))) by JORDAN8:def_1;
then ((2 * m) -' 2) + 1 <= len (Gauge (D,(i + 1))) by NAT_1:13;
then [(((2 * m) -' 2) + 1),1] in Indices (Gauge (D,(i + 1))) by A5, A11, A10, MATRIX_1:36;
then A27: ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1 by JORDAN8:def_1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2)) by EUCLID:52 ;
A28: 1 <= m by A1, XXREAL_0:2;
then A29: 1 < len (Gauge (D,i)) by A25, XXREAL_0:2;
then A30: ((Gauge (D,i)) * (m,1)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 by A1, A25, A11, Th3;
A31: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1;
then A32: n < width (Gauge (D,i)) by A4, NAT_1:13;
then A33: ((Gauge (D,i)) * (1,n)) `2 = ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 by A3, A31, A29, A11, Th4;
A34: 1 <= (2 * m) -' 2 by A1, Lm11;
then A35: cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A26, A16, GOBRD11:32;
(2 * m) -' 2 = (2 * m) - 2 by A1, Lm7;
then (2 * m) -' 2 < (2 * m) -' 1 by A18, XREAL_1:15;
then A36: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 < ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 by A5, A11, A34, A21, GOBOARD5:3;
A37: (2 * n) -' 1 = (2 * n) - 1 by A3, Lm8, XXREAL_0:2;
A38: (((2 * n) -' 2) + 1) - 2 = (2 * n) - 3 by A3, Lm14;
n < (2 |^ i) + 3 by A31, A32, JORDAN8:def_1;
then (2 * n) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then A39: (2 * n) -' 2 < width (Gauge (D,(i + 1))) by A5, JORDAN8:def_1;
then ((2 * n) -' 2) + 1 <= len (Gauge (D,(i + 1))) by A5, NAT_1:13;
then [1,(((2 * n) -' 2) + 1)] in Indices (Gauge (D,(i + 1))) by A5, A11, A20, MATRIX_1:36;
then A40: ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)))]| `2 by JORDAN8:def_1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)) by EUCLID:52 ;
A41: 1 <= (2 * n) -' 2 by A3, Lm11;
then A42: cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 ) } by A34, A26, A39, GOBRD11:32;
A43: 1 <= (2 * m) -' 1 by A28, Lm12;
then A44: cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 ) } by A41, A39, A21, GOBRD11:32;
A45: cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A43, A16, A21, GOBRD11:32;
A46: cell ((Gauge (D,i)),m,n) = { |[r,q]| where r, q is Real : ( ((Gauge (D,i)) * (m,1)) `1 <= r & r <= ((Gauge (D,i)) * ((m + 1),1)) `1 & ((Gauge (D,i)) * (1,n)) `2 <= q & q <= ((Gauge (D,i)) * (1,(n + 1))) `2 ) } by A28, A12, A25, A32, GOBRD11:32;
1 <= n + 1 by NAT_1:11;
then [1,(n + 1)] in Indices (Gauge (D,i)) by A4, A31, A29, MATRIX_1:36;
then A47: ((Gauge (D,i)) * (1,(n + 1))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2)))]| `2 by JORDAN8:def_1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2)) by EUCLID:52
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * (n + 1)) -' 2) - 2)) by A3, A22, Lm10, XXREAL_0:2 ;
1 <= m + 1 by NAT_1:11;
then [(m + 1),1] in Indices (Gauge (D,i)) by A2, A31, A29, MATRIX_1:36;
then A48: ((Gauge (D,i)) * ((m + 1),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (1 - 2)))]| `1 by JORDAN8:def_1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2)) by EUCLID:52
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * (m + 1)) -' 2) - 2)) by A1, A8, Lm10, XXREAL_0:2 ;
(2 * n) -' 2 = (2 * n) - 2 by A3, Lm7;
then (2 * n) -' 2 < (2 * n) -' 1 by A37, XREAL_1:15;
then A49: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 < ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 by A5, A11, A41, A16, GOBOARD5:4;
A50: ((2 * m) -' 1) + 1 = 2 * m by A28, Lm12, NAT_D:43;
(2 * m) -' 1 <= 2 * m by NAT_D:35;
then A51: 1 <= 2 * m by A43, XXREAL_0:2;
((2 * m) -' 1) + 1 <= len (Gauge (D,(i + 1))) by A21, NAT_1:13;
then [(2 * m),1] in Indices (Gauge (D,(i + 1))) by A5, A50, A11, A51, MATRIX_1:36;
then A52: ((Gauge (D,(i + 1))) * ((2 * m),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1 by JORDAN8:def_1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2)) by EUCLID:52 ;
A53: ((2 * m) -' 2) + 1 = (2 * m) -' 1 by A1, Lm9, XXREAL_0:2;
thus cell ((Gauge (D,i)),m,n) c= (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) :: according to XBOOLE_0:def_10 ::_thesis: (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) c= cell ((Gauge (D,i)),m,n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell ((Gauge (D,i)),m,n) or x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) )
assume x in cell ((Gauge (D,i)),m,n) ; ::_thesis: x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)))
then consider r, q being Real such that
A54: x = |[r,q]| and
A55: ((Gauge (D,i)) * (m,1)) `1 <= r and
A56: r <= ((Gauge (D,i)) * ((m + 1),1)) `1 and
A57: ((Gauge (D,i)) * (1,n)) `2 <= q and
A58: q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A46;
( ( r <= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q <= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r >= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q <= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r <= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q >= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r >= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q >= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) ) ;
then ( |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ) by A53, A23, A24, A9, A50, A15, A42, A44, A35, A45, A52, A17, A48, A47, A30, A33, A55, A56, A57, A58;
hence x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) by A54, Lm3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) or x in cell ((Gauge (D,i)),m,n) )
A59: (2 * m) - 3 < (2 * m) - 2 by XREAL_1:15;
(E-bound D) - (W-bound D) >= 0 by SPRECT_1:21, XREAL_1:48;
then (((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3) <= (((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2) by A59, XREAL_1:64;
then A60: (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3)) <= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2)) by XREAL_1:6;
assume A61: x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) ; ::_thesis: x in cell ((Gauge (D,i)),m,n)
percases ( x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ) by A61, Lm3;
suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n)
then consider r, q being Real such that
A62: x = |[r,q]| and
A63: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r and
A64: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 and
A65: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q and
A66: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 by A42;
A67: q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A38, A9, A7, A40, A47, A66, XXREAL_0:2;
r <= ((Gauge (D,i)) * ((m + 1),1)) `1 by A19, A24, A60, A27, A48, A64, XXREAL_0:2;
hence x in cell ((Gauge (D,i)),m,n) by A46, A30, A33, A62, A63, A65, A67; ::_thesis: verum
end;
suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n)
then consider r, q being Real such that
A68: x = |[r,q]| and
A69: ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r and
A70: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 and
A71: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q and
A72: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 by A44;
A73: ((Gauge (D,i)) * (m,1)) `1 <= r by A30, A36, A69, XXREAL_0:2;
q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A38, A9, A7, A40, A47, A72, XXREAL_0:2;
hence x in cell ((Gauge (D,i)),m,n) by A24, A50, A46, A52, A48, A33, A68, A70, A71, A73; ::_thesis: verum
end;
suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n)
then consider r, q being Real such that
A74: x = |[r,q]| and
A75: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r and
A76: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 and
A77: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q and
A78: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 by A35;
A79: ((Gauge (D,i)) * (1,n)) `2 <= q by A33, A49, A77, XXREAL_0:2;
r <= ((Gauge (D,i)) * ((m + 1),1)) `1 by A19, A24, A60, A27, A48, A76, XXREAL_0:2;
hence x in cell ((Gauge (D,i)),m,n) by A9, A15, A46, A17, A47, A30, A74, A75, A78, A79; ::_thesis: verum
end;
suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n)
then consider r, q being Real such that
A80: x = |[r,q]| and
A81: ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r and
A82: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 and
A83: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q and
A84: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 by A45;
A85: ((Gauge (D,i)) * (1,n)) `2 <= q by A33, A49, A83, XXREAL_0:2;
((Gauge (D,i)) * (m,1)) `1 <= r by A30, A36, A81, XXREAL_0:2;
hence x in cell ((Gauge (D,i)),m,n) by A24, A9, A50, A15, A46, A52, A17, A48, A47, A80, A82, A84, A85; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN1D:6
for m, i, n being Element of NAT
for D being compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds
cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
proof
let m, i, n be Element of NAT ; ::_thesis: for D being compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds
cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds
cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
let k be Element of NAT ; ::_thesis: ( 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) implies cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } )
assume that
A1: 2 <= m and
A2: m + 1 < len (Gauge (D,i)) and
A3: 2 <= n and
A4: n + 1 < len (Gauge (D,i)) ; ::_thesis: cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
deffunc H1( Element of NAT ) -> set = { (cell ((Gauge (D,(i + $1))),a,b)) where a, b is Element of NAT : ( (((2 |^ $1) * m) - (2 |^ ($1 + 1))) + 2 <= a & a <= (((2 |^ $1) * m) - (2 |^ $1)) + 1 & (((2 |^ $1) * n) - (2 |^ ($1 + 1))) + 2 <= b & b <= (((2 |^ $1) * n) - (2 |^ $1)) + 1 ) } ;
defpred S1[ Element of NAT ] means cell ((Gauge (D,i)),m,n) = union H1($1);
A5: for w being Element of NAT st S1[w] holds
S1[w + 1]
proof
let w be Element of NAT ; ::_thesis: ( S1[w] implies S1[w + 1] )
assume A6: S1[w] ; ::_thesis: S1[w + 1]
A7: len (Gauge (D,(i + w))) = (2 |^ (i + w)) + 3 by JORDAN8:def_1;
A8: (i + w) + 1 = i + (w + 1) ;
H1(w + 1) is_finer_than H1(w)
proof
A9: now__::_thesis:_for_a_being_odd_Element_of_NAT_holds_2_*_((a_div_2)_+_1)_=_a_+_1
let a be odd Element of NAT ; ::_thesis: 2 * ((a div 2) + 1) = a + 1
consider e being Element of NAT such that
A10: a = (2 * e) + 1 by ABIAN:9;
A11: (2 * e) mod 2 = 0 by NAT_D:13;
thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1)
.= (2 * (((2 * e) div 2) + (1 div 2))) + 2 by A10, A11, NAT_D:19
.= (2 * (e + 0)) + (1 + 1) by Lm1, NAT_D:20
.= a + 1 by A10 ; ::_thesis: verum
end;
A12: now__::_thesis:_for_m_being_Element_of_NAT_holds_2_*_((((2_|^_w)_*_m)_-_(2_|^_w))_+_1)_=_((((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1)_+_1
let m be Element of NAT ; ::_thesis: 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1
thus 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ w))) + (1 + 1)
.= (((2 * (2 |^ w)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:6
.= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:6
.= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ; ::_thesis: verum
end;
A13: now__::_thesis:_for_m_being_Element_of_NAT_
for_a_being_odd_Element_of_NAT_st_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_
(a_div_2)_+_1_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1
let m be Element of NAT ; ::_thesis: for a being odd Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds
(a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
let a be odd Element of NAT ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 )
assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
then A14: a + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:6;
2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A12;
then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A9, A14;
hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:68; ::_thesis: verum
end;
A15: now__::_thesis:_for_a_being_even_Element_of_NAT_holds_2_*_((a_div_2)_+_1)_=_a_+_2
let a be even Element of NAT ; ::_thesis: 2 * ((a div 2) + 1) = a + 2
A16: ex e being Element of NAT st a = 2 * e by ABIAN:def_2;
thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1)
.= a + 2 by A16, NAT_D:20 ; ::_thesis: verum
end;
A17: now__::_thesis:_for_m_being_Element_of_NAT_
for_a_being_even_Element_of_NAT_st_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_
(a_div_2)_+_1_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1
let m be Element of NAT ; ::_thesis: for a being even Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds
(a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
let a be even Element of NAT ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 )
assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
then a < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XXREAL_0:1;
then a + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by INT_1:7;
then (a + 1) + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:6;
then A18: a + (1 + 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ;
2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A12;
then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A15, A18;
hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:68; ::_thesis: verum
end;
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not X in H1(w + 1) or ex b1 being set st
( b1 in H1(w) & X c= b1 ) )
assume X in H1(w + 1) ; ::_thesis: ex b1 being set st
( b1 in H1(w) & X c= b1 )
then consider a, b being Element of NAT such that
A19: X = cell ((Gauge (D,(i + (w + 1)))),a,b) and
A20: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a and
A21: a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 and
A22: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= b and
A23: b <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 ;
take Y = cell ((Gauge (D,(i + w))),((a div 2) + 1),((b div 2) + 1)); ::_thesis: ( Y in H1(w) & X c= Y )
deffunc H2( Element of NAT , Element of NAT ) -> Element of K10( the U1 of (TOP-REAL 2)) = cell ((Gauge (D,((i + w) + 1))),((2 * ((a div 2) + 1)) -' $1),((2 * ((b div 2) + 1)) -' $2));
A24: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_m_holds_
0_+_2_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2
let a, m be Element of NAT ; ::_thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 )
A25: 2 |^ ((w + 1) + 1) = (2 |^ (w + 1)) * (2 |^ 1) by NEWTON:8
.= (2 |^ (w + 1)) * 2 by NEWTON:5 ;
assume 2 <= m ; ::_thesis: 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2
then (2 |^ (w + 1)) * m >= 2 |^ ((w + 1) + 1) by A25, XREAL_1:64;
then 0 <= ((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1)) by XREAL_1:48;
hence 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by XREAL_1:6; ::_thesis: verum
end;
then 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by A1;
then 2 <= a by A20, XXREAL_0:2;
then 2 div 2 <= a div 2 by NAT_2:24;
then A26: 1 + 1 <= (a div 2) + 1 by Lm2, XREAL_1:6;
A27: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_m_+_1_<_len_(Gauge_(D,i))_&_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_
((a_div_2)_+_1)_+_1_<_len_(Gauge_(D,(i_+_w)))
let a, m be Element of NAT ; ::_thesis: ( m + 1 < len (Gauge (D,i)) & a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) )
assume m + 1 < len (Gauge (D,i)) ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) )
then m + 1 < (2 |^ i) + 3 by JORDAN8:def_1;
then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ;
then 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34;
then (1 / 2) * (2 * m) < (1 / 2) * ((2 |^ (i + 1)) + 3) by XREAL_1:68;
then m < ((1 / 2) * (2 |^ (i + 1))) + ((1 / 2) * 3) ;
then A28: m < (2 |^ i) + ((1 / 2) * 3) by Th2;
(2 |^ i) + (3 / 2) < (2 |^ i) + 2 by XREAL_1:6;
then m < (2 |^ i) + 2 by A28, XXREAL_0:2;
then m + 1 <= (2 |^ i) + 2 by NAT_1:13;
then (m + 1) - 2 <= ((2 |^ i) + 2) - 2 by XREAL_1:9;
then (2 |^ (w + 1)) * (m - 1) <= (2 |^ (w + 1)) * (2 |^ i) by XREAL_1:64;
then ((2 |^ (w + 1)) * (m - 1)) + 5 < ((2 |^ (w + 1)) * (2 |^ i)) + 6 by XREAL_1:8;
then A29: ((2 |^ (w + 1)) * (m - 1)) + 5 < (2 |^ ((w + 1) + i)) + 6 by NEWTON:8;
then A30: (((2 |^ (w + 1)) * (m - 1)) + 1) + (3 + 1) < (2 * (2 |^ (i + w))) + 6 by A8, NEWTON:6;
A31: ((((2 |^ (w + 1)) * (m - 1)) + 1) + 3) + 1 < (2 * (2 |^ (i + w))) + (2 * 3) by A8, A29, NEWTON:6;
assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: ((a div 2) + 1) + 1 < len (Gauge (D,(i + w)))
then a + 3 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3 by XREAL_1:6;
then A32: (a + 3) + 0 < (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by XREAL_1:8;
then A33: (a + 3) + 1 <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by INT_1:7;
now__::_thesis:_2_*_(((a_div_2)_+_1)_+_1)_<_2_*_((2_|^_(i_+_w))_+_3)
percases ( a is odd or a is even ) ;
supposeA34: a is odd ; ::_thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3)
2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1)
.= (a + 1) + 2 by A9, A34
.= a + (1 + 2) ;
hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A32, A30, XXREAL_0:2; ::_thesis: verum
end;
supposeA35: a is even ; ::_thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3)
2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1)
.= (a + 2) + 2 by A15, A35
.= a + (2 + 2) ;
hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A33, A31, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A7, XREAL_1:64; ::_thesis: verum
end;
then A36: ((b div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A4, A23;
2 <= (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 by A3, A24;
then 2 <= b by A22, XXREAL_0:2;
then 2 div 2 <= b div 2 by NAT_2:24;
then A37: 1 + 1 <= (b div 2) + 1 by Lm2, XREAL_1:6;
((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A2, A21, A27;
then A38: Y = ((H2(2,2) \/ H2(1,2)) \/ H2(2,1)) \/ H2(1,1) by A26, A37, A36, Th5;
A39: now__::_thesis:_for_m_being_Element_of_NAT_holds_2_*_((((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2)_=_((((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2)_+_2
let m be Element of NAT ; ::_thesis: 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2
thus 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ (w + 1)))) + (2 + 2)
.= (((2 * (2 |^ w)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:6
.= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:6
.= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 ; ::_thesis: verum
end;
A40: now__::_thesis:_for_m_being_Element_of_NAT_
for_a_being_even_Element_of_NAT_st_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2_<=_a_holds_
(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_(a_div_2)_+_1
let m be Element of NAT ; ::_thesis: for a being even Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
let a be even Element of NAT ; ::_thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 )
assume (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; ::_thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
then A41: ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 <= a + 2 by XREAL_1:6;
2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A39;
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A15, A41;
hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:68; ::_thesis: verum
end;
A42: now__::_thesis:_for_m_being_Element_of_NAT_
for_a_being_odd_Element_of_NAT_st_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2_<=_a_holds_
(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_(a_div_2)_+_1
let m be Element of NAT ; ::_thesis: for a being odd Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
let a be odd Element of NAT ; ::_thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 )
assume (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; ::_thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 < a by XXREAL_0:1;
then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1 < a + 1 by XREAL_1:6;
then A43: (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) + 1 <= a + 1 by INT_1:7;
2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A39;
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A9, A43;
hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:68; ::_thesis: verum
end;
percases ( ( a is odd & b is odd ) or ( a is odd & b is even ) or ( a is even & b is odd ) or ( a is even & b is even ) ) ;
supposeA44: ( a is odd & b is odd ) ; ::_thesis: ( Y in H1(w) & X c= Y )
then A45: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A42;
A46: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A13, A44;
A47: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A13, A44;
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A42, A44;
hence Y in H1(w) by A46, A45, A47; ::_thesis: X c= Y
A48: (2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A9, A44
.= b by NAT_D:34 ;
(2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A9, A44
.= a by NAT_D:34 ;
hence X c= Y by A19, A38, A48, XBOOLE_1:7; ::_thesis: verum
end;
supposeA49: ( a is odd & b is even ) ; ::_thesis: ( Y in H1(w) & X c= Y )
then A50: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A40;
A51: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A13, A49;
A52: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A17, A49;
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A42, A49;
hence Y in H1(w) by A51, A50, A52; ::_thesis: X c= Y
A53: H2(2,2) \/ H2(1,2) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by XBOOLE_1:7;
H2(1,2) c= H2(2,2) \/ H2(1,2) by XBOOLE_1:7;
then A54: H2(1,2) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by A53, XBOOLE_1:1;
A55: (H2(2,2) \/ H2(1,2)) \/ H2(2,1) c= Y by A38, XBOOLE_1:7;
A56: (2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A15, A49
.= b by NAT_D:34 ;
(2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A9, A49
.= a by NAT_D:34 ;
hence X c= Y by A19, A56, A54, A55, XBOOLE_1:1; ::_thesis: verum
end;
supposeA57: ( a is even & b is odd ) ; ::_thesis: ( Y in H1(w) & X c= Y )
then A58: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A42;
A59: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A17, A57;
A60: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A13, A57;
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A40, A57;
hence Y in H1(w) by A59, A58, A60; ::_thesis: X c= Y
A61: H2(2,1) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by XBOOLE_1:7;
A62: (H2(2,2) \/ H2(1,2)) \/ H2(2,1) c= Y by A38, XBOOLE_1:7;
A63: (2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A9, A57
.= b by NAT_D:34 ;
(2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A15, A57
.= a by NAT_D:34 ;
hence X c= Y by A19, A63, A61, A62, XBOOLE_1:1; ::_thesis: verum
end;
supposeA64: ( a is even & b is even ) ; ::_thesis: ( Y in H1(w) & X c= Y )
then A65: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A40;
A66: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A17, A64;
A67: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A17, A64;
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A40, A64;
hence Y in H1(w) by A66, A65, A67; ::_thesis: X c= Y
A68: (2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A15, A64
.= b by NAT_D:34 ;
(2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A15, A64
.= a by NAT_D:34 ;
then X c= H2(2,2) \/ ((H2(1,2) \/ H2(2,1)) \/ H2(1,1)) by A19, A68, XBOOLE_1:7;
then X c= (H2(2,2) \/ (H2(1,2) \/ H2(2,1))) \/ H2(1,1) by XBOOLE_1:4;
hence X c= Y by A38, XBOOLE_1:4; ::_thesis: verum
end;
end;
end;
then A69: union H1(w + 1) c= union H1(w) by SETFAM_1:13;
A70: len (Gauge (D,i)) = (2 |^ i) + 3 by JORDAN8:def_1;
for x being set st x in H1(w) holds
ex K being set st
( K c= H1(w + 1) & x c= union K )
proof
let x be set ; ::_thesis: ( x in H1(w) implies ex K being set st
( K c= H1(w + 1) & x c= union K ) )
assume x in H1(w) ; ::_thesis: ex K being set st
( K c= H1(w + 1) & x c= union K )
then consider a, b being Element of NAT such that
A71: x = cell ((Gauge (D,(i + w))),a,b) and
A72: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a and
A73: a <= (((2 |^ w) * m) - (2 |^ w)) + 1 and
A74: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= b and
A75: b <= (((2 |^ w) * n) - (2 |^ w)) + 1 ;
take K = {(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1)))}; ::_thesis: ( K c= H1(w + 1) & x c= union K )
A76: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_
0_+_2_<=_(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2
let m be Element of NAT ; ::_thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 )
assume 2 <= m ; ::_thesis: 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2
then (2 |^ w) * m >= (2 |^ w) * 2 by XREAL_1:64;
then (2 |^ w) * m >= 2 |^ (w + 1) by NEWTON:6;
then 0 <= ((2 |^ w) * m) - (2 |^ (w + 1)) by XREAL_1:48;
hence 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by XREAL_1:6; ::_thesis: verum
end;
then A77: 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by A1;
then A78: 2 <= a by A72, XXREAL_0:2;
A79: (2 * a) -' 2 = (2 * a) - 2 by A72, A77, Lm7, XXREAL_0:2;
A80: 2 <= (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 by A3, A76;
then A81: 2 <= b by A74, XXREAL_0:2;
A82: (2 * b) -' 2 = (2 * b) - 2 by A74, A80, Lm7, XXREAL_0:2;
(2 * b) -' 1 = (2 * b) - 1 by A81, Lm8, XXREAL_0:2;
then A83: (2 * b) -' 2 < (2 * b) -' 1 by A82, XREAL_1:15;
(2 * a) -' 1 = (2 * a) - 1 by A78, Lm8, XXREAL_0:2;
then A84: (2 * a) -' 2 < (2 * a) -' 1 by A79, XREAL_1:15;
hereby :: according to TARSKI:def_3 ::_thesis: x c= union K
A85: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_a_&_a_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1_holds_
(2_*_a)_-'_2_<_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1
let a, m be Element of NAT ; ::_thesis: ( 2 <= a & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 )
assume A86: 2 <= a ; ::_thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 )
assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; ::_thesis: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1
then 2 * a <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by XREAL_1:64;
then 2 * a <= (((2 * (2 |^ w)) * m) - (2 * (2 |^ w))) + 2 ;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 * (2 |^ w))) + 2 by NEWTON:6;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2 by NEWTON:6;
then (2 * a) - 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by XREAL_1:9;
then A87: (2 * a) -' 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by A86, Lm7;
(((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 0 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XREAL_1:6;
hence (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A87, XXREAL_0:2; ::_thesis: verum
end;
then A88: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A73, A78;
then ((2 * a) -' 2) + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by INT_1:7;
then A89: (2 * a) -' 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A78, Lm9, XXREAL_0:2;
A90: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_a_&_(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_a_holds_
(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_(4_-_2)_<=_(2_*_a)_-'_2
let a, m be Element of NAT ; ::_thesis: ( 2 <= a & (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 )
assume A91: 2 <= a ; ::_thesis: ( (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 )
assume (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a ; ::_thesis: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * a by XREAL_1:64;
then (((2 * (2 |^ w)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a ;
then (((2 |^ (w + 1)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a by NEWTON:6;
then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4 <= 2 * a by NEWTON:6;
then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) - 2 <= (2 * a) - 2 by XREAL_1:9;
hence (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 by A91, Lm7; ::_thesis: verum
end;
then A92: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 2 by A74, A81;
then A93: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 1 by A83, XXREAL_0:2;
let q be set ; ::_thesis: ( q in K implies q in H1(w + 1) )
assume q in K ; ::_thesis: q in H1(w + 1)
then A94: ( q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 2)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 2)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 1)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 1)) ) by ENUMSET1:def_2;
A95: (2 * b) -' 2 < (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A75, A81, A85;
then ((2 * b) -' 2) + 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by INT_1:7;
then A96: (2 * b) -' 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A81, Lm9, XXREAL_0:2;
A97: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 2 by A72, A78, A90;
then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 1 by A84, XXREAL_0:2;
hence q in H1(w + 1) by A97, A88, A89, A92, A95, A96, A93, A94; ::_thesis: verum
end;
A98: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_m_+_1_<_len_(Gauge_(D,i))_&_a_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1_holds_
a_+_1_<_len_(Gauge_(D,(i_+_w)))
let a, m be Element of NAT ; ::_thesis: ( m + 1 < len (Gauge (D,i)) & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge (D,(i + w))) )
assume m + 1 < len (Gauge (D,i)) ; ::_thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge (D,(i + w))) )
then (m + 1) - 2 < ((2 |^ i) + 3) - 2 by A70, XREAL_1:9;
then m - 1 < (2 |^ i) + (3 - 2) ;
then m - 1 <= (2 |^ i) + 0 by INT_1:7;
then (2 |^ w) * (m - 1) <= (2 |^ w) * (2 |^ i) by XREAL_1:64;
then (2 |^ w) * (m - 1) <= 2 |^ (w + i) by NEWTON:8;
then A99: ((2 |^ w) * (m - 1)) + 3 <= (2 |^ (w + i)) + 3 by XREAL_1:6;
assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; ::_thesis: a + 1 < len (Gauge (D,(i + w)))
then a + 1 <= ((((2 |^ w) * m) - (2 |^ w)) + 1) + 1 by XREAL_1:6;
then a + 1 < (((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) + 1 by XREAL_1:145;
hence a + 1 < len (Gauge (D,(i + w))) by A7, A99, XXREAL_0:2; ::_thesis: verum
end;
then A100: b + 1 < len (Gauge (D,(i + w))) by A4, A75;
a + 1 < len (Gauge (D,(i + w))) by A2, A73, A98;
then cell ((Gauge (D,(i + w))),a,b) = (((cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2)))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1)))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1))) by A78, A81, A100, Th5;
hence x c= union K by A71, Lm4; ::_thesis: verum
end;
hence cell ((Gauge (D,i)),m,n) c= union H1(w + 1) by A6, Th1; :: according to XBOOLE_0:def_10 ::_thesis: union H1(w + 1) c= cell ((Gauge (D,i)),m,n)
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in union H1(w + 1) or d in cell ((Gauge (D,i)),m,n) )
assume d in union H1(w + 1) ; ::_thesis: d in cell ((Gauge (D,i)),m,n)
hence d in cell ((Gauge (D,i)),m,n) by A6, A69; ::_thesis: verum
end;
A101: now__::_thesis:_for_m_being_Element_of_NAT_holds_
(_(((2_|^_0)_*_m)_-_(2_|^_(0_+_1)))_+_2_=_m_&_(((2_|^_0)_*_m)_-_(2_|^_0))_+_1_=_m_)
let m be Element of NAT ; ::_thesis: ( (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = m & (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m )
A102: (2 |^ 0) * m = 1 * m by NEWTON:4;
hence (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = (m - 2) + 2 by NEWTON:5
.= m ;
::_thesis: (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m
thus (((2 |^ 0) * m) - (2 |^ 0)) + 1 = (m - 1) + 1 by A102, NEWTON:4
.= m ; ::_thesis: verum
end;
H1( 0 ) = {(cell ((Gauge (D,i)),m,n))}
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(cell ((Gauge (D,i)),m,n))} c= H1( 0 )
let x be set ; ::_thesis: ( x in H1( 0 ) implies x in {(cell ((Gauge (D,i)),m,n))} )
assume x in H1( 0 ) ; ::_thesis: x in {(cell ((Gauge (D,i)),m,n))}
then consider a, b being Element of NAT such that
A103: x = cell ((Gauge (D,(i + 0))),a,b) and
A104: (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a and
A105: a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 and
A106: (((2 |^ 0) * n) - (2 |^ (0 + 1))) + 2 <= b and
A107: b <= (((2 |^ 0) * n) - (2 |^ 0)) + 1 ;
A108: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_(((2_|^_0)_*_m)_-_(2_|^_(0_+_1)))_+_2_<=_a_&_a_<=_(((2_|^_0)_*_m)_-_(2_|^_0))_+_1_holds_
a_=_m
let a, m be Element of NAT ; ::_thesis: ( (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 implies a = m )
assume that
A109: (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a and
A110: a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 ; ::_thesis: a = m
A111: (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m by A101;
(((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = m by A101;
hence a = m by A109, A110, A111, XXREAL_0:1; ::_thesis: verum
end;
then A112: b = n by A106, A107;
a = m by A104, A105, A108;
hence x in {(cell ((Gauge (D,i)),m,n))} by A103, A112, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(cell ((Gauge (D,i)),m,n))} or x in H1( 0 ) )
assume x in {(cell ((Gauge (D,i)),m,n))} ; ::_thesis: x in H1( 0 )
then A113: x = cell ((Gauge (D,(i + 0))),m,n) by TARSKI:def_1;
A114: m <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 by A101;
A115: n <= (((2 |^ 0) * n) - (2 |^ 0)) + 1 by A101;
A116: (((2 |^ 0) * n) - (2 |^ (0 + 1))) + 2 <= n by A101;
(((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= m by A101;
hence x in H1( 0 ) by A113, A114, A116, A115; ::_thesis: verum
end;
then A117: S1[ 0 ] by ZFMISC_1:25;
for w being Element of NAT holds S1[w] from NAT_1:sch_1(A117, A5);
hence cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } ; ::_thesis: verum
end;
theorem Th7: :: JORDAN1D:7
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (north_halfline (N-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:86, PSCOMP_1:42;
A2: p in (north_halfline (N-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in north_halfline (N-max C) by XBOOLE_0:def_4;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len (Cage (C,n)) and
A6: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A7: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A4, A5, TOPREAL1:def_3;
A8: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A9: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A10: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A8, XREAL_1:235, XXREAL_0:2;
then A11: (len (Gauge (C,n))) -' 1 < len (Gauge (C,n)) by NAT_1:13;
A12: N-max C = |[((N-max C) `1),((N-max C) `2)]| by EUCLID:53;
A13: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44;
A14: (N-max C) `2 = N-bound C by EUCLID:52
.= ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 by A9, JORDAN8:14 ;
A15: N-max C in N-most C by PSCOMP_1:42;
A16: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A4, A5, NAT_1:13; ::_thesis: N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A18: ((Cage (C,n)) /. i) `2 = p `2 by A3, A6, A15, A7, JORDAN1A:78, SPPOL_1:40;
A19: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A6, A17, A15, A7, JORDAN1A:78, SPPOL_1:40;
A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A21: [i1,j1] in Indices (Gauge (C,n)) and
A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A23: [i2,j2] in Indices (Gauge (C,n)) and
A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A5, JORDAN8:3;
A26: 1 <= i1 by A21, MATRIX_1:38;
A27: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38;
A28: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38;
A29: 1 <= j1 by A21, MATRIX_1:38;
p `2 = N-bound (L~ (Cage (C,n))) by A2, JORDAN1A:82, PSCOMP_1:42;
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `2 by A22, A18, A26, A28, JORDAN1A:70;
then A30: len (Gauge (C,n)) <= j1 by A16, A26, A28, A29, GOBOARD5:4;
A31: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38;
then A32: j1 = len (Gauge (C,n)) by A16, A30, XXREAL_0:1;
A33: 1 <= j2 by A23, MATRIX_1:38;
A34: j1 = j2
proof
assume j1 <> j2 ; ::_thesis: contradiction
then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
hence contradiction by A22, A24, A25, A18, A19, A26, A28, A29, A27, A33, A31, GOBOARD5:4; ::_thesis: verum
end;
A35: 1 <= i2 by A23, MATRIX_1:38;
A36: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38;
i1 <= i1 + 1 by NAT_1:11;
then A37: ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A26, A36, A29, A27, A34, A30, JORDAN10:4, JORDAN1A:18;
then p `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A6, A7, TOPREAL1:3;
then (N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),(len (Gauge (C,n))))) `1 by A3, A4, A5, A21, A22, A23, A24, A25, A16, A34, A32, JORDAN10:4, TOPREAL1:def_10;
then A38: (N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A35, A36, A34, A30, A9, GOBOARD5:2, JORDAN10:4;
((Cage (C,n)) /. i) `1 <= p `1 by A6, A7, A37, TOPREAL1:3;
then ((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `1 <= (N-max C) `1 by A3, A22, A32, TOPREAL1:def_10;
then A39: ((Gauge (C,n)) * (i1,1)) `1 <= (N-max C) `1 by A16, A26, A28, A9, GOBOARD5:2;
len (Gauge (C,n)) >= 1 + 1 by A8, XXREAL_0:2;
then A40: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2;
then ((Gauge (C,n)) * (1,j1)) `2 >= (N-max C) `2 by A16, A32, A9, A14, A13, SPRECT_3:12;
then A41: N-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j1 -' 1))) `2 <= s & s <= ((Gauge (C,n)) * (1,j1)) `2 ) } by A32, A14, A39, A38, A12;
A42: 1 <= i1 by A21, MATRIX_1:38;
i1 < len (Gauge (C,n)) by A4, A5, A21, A22, A23, A24, A25, A16, A36, A34, A30, JORDAN10:4, NAT_1:13;
then N-max C in cell ((Gauge (C,n)),i1,(j1 -' 1)) by A16, A32, A42, A40, A10, A11, A41, GOBRD11:32;
hence N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A4, A5, A20, A21, A22, A23, A24, A25, A16, A34, A30, GOBRD13:24, JORDAN10:4; ::_thesis: verum
end;
theorem :: JORDAN1D:8
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th7;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: N-max C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence N-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th9: :: JORDAN1D:9
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (east_halfline (E-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:87, PSCOMP_1:50;
A2: p in (east_halfline (E-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in east_halfline (E-min C) by XBOOLE_0:def_4;
len (Gauge (C,n)) < (len (Gauge (C,n))) + 1 by NAT_1:13;
then A4: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:19;
A5: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44;
A6: E-min C = |[((E-min C) `1),((E-min C) `2)]| by EUCLID:53;
A7: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A8: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A9: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A7, XREAL_1:235, XXREAL_0:2;
A10: (E-min C) `1 = E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A8, JORDAN8:12 ;
A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A12: E-min C in E-most C by PSCOMP_1:50;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A13: 1 <= i and
A14: i + 1 <= len (Cage (C,n)) and
A15: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A16: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A13, A14, TOPREAL1:def_3;
thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A13, A14, NAT_1:13; ::_thesis: E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A18: ((Cage (C,n)) /. i) `1 = p `1 by A3, A15, A12, A16, JORDAN1A:79, SPPOL_1:41;
A19: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A15, A17, A12, A16, JORDAN1A:79, SPPOL_1:41;
A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A21: [i1,j1] in Indices (Gauge (C,n)) and
A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A23: [i2,j2] in Indices (Gauge (C,n)) and
A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13, A14, JORDAN8:3;
A26: 1 <= i1 by A21, MATRIX_1:38;
A27: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38;
A28: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38;
A29: 1 <= i2 by A23, MATRIX_1:38;
A30: 1 <= j1 by A21, MATRIX_1:38;
p `1 = E-bound (L~ (Cage (C,n))) by A2, JORDAN1A:83, PSCOMP_1:50;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A22, A18, A11, A30, A27, JORDAN1A:71;
then A31: len (Gauge (C,n)) <= i1 by A26, A30, A27, GOBOARD5:3;
A32: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38;
then A33: i1 = len (Gauge (C,n)) by A31, XXREAL_0:1;
A34: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38;
A35: i1 = i2
proof
assume i1 <> i2 ; ::_thesis: contradiction
then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
hence contradiction by A22, A24, A25, A18, A19, A26, A32, A29, A34, A30, A28, GOBOARD5:3; ::_thesis: verum
end;
then A36: j2 < width (Gauge (C,n)) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10:1, NAT_1:13;
A37: 1 <= j2 by A23, MATRIX_1:38;
j2 <= j2 + 1 by NAT_1:11;
then A38: ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10:1, JORDAN1A:19;
then p `2 <= ((Cage (C,n)) /. i) `2 by A15, A16, TOPREAL1:4;
then (E-min C) `2 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(j2 + 1))) `2 by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10:1, TOPREAL1:def_11;
then A39: (E-min C) `2 <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 by A13, A14, A21, A22, A23, A24, A25, A29, A30, A27, A35, A33, GOBOARD5:1, JORDAN10:1;
((Cage (C,n)) /. (i + 1)) `2 <= p `2 by A15, A16, A38, TOPREAL1:4;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j2)) `2 <= (E-min C) `2 by A3, A24, A35, A33, TOPREAL1:def_11;
then A40: ((Gauge (C,n)) * (1,j2)) `2 <= (E-min C) `2 by A29, A28, A37, A35, A33, GOBOARD5:1;
len (Gauge (C,n)) >= 1 + 1 by A7, XXREAL_0:2;
then A41: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2;
then ((Gauge (C,n)) * (i1,1)) `1 >= (E-min C) `1 by A11, A33, A8, A10, A5, SPRECT_3:13;
then E-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A10, A40, A39, A6;
then E-min C in cell ((Gauge (C,n)),(i2 -' 1),j2) by A37, A35, A33, A36, A41, A4, A9, GOBRD11:32;
hence E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13:28, JORDAN10:1; ::_thesis: verum
end;
theorem :: JORDAN1D:10
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th9;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: E-min C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence E-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th11: :: JORDAN1D:11
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:87, PSCOMP_1:50;
A2: p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in east_halfline (E-max C) by XBOOLE_0:def_4;
len (Gauge (C,n)) < (len (Gauge (C,n))) + 1 by NAT_1:13;
then A4: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:19;
A5: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44;
A6: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A8: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A6, XREAL_1:235, XXREAL_0:2;
A9: (E-max C) `1 = E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A7, JORDAN8:12 ;
A10: E-max C = |[((E-max C) `1),((E-max C) `2)]| by EUCLID:53;
A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A12: E-max C in E-most C by PSCOMP_1:50;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A13: 1 <= i and
A14: i + 1 <= len (Cage (C,n)) and
A15: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A16: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A13, A14, TOPREAL1:def_3;
thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A13, A14, NAT_1:13; ::_thesis: E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A18: ((Cage (C,n)) /. i) `1 = p `1 by A3, A15, A12, A16, JORDAN1A:79, SPPOL_1:41;
A19: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A15, A17, A12, A16, JORDAN1A:79, SPPOL_1:41;
A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A21: [i1,j1] in Indices (Gauge (C,n)) and
A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A23: [i2,j2] in Indices (Gauge (C,n)) and
A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13, A14, JORDAN8:3;
A26: 1 <= i1 by A21, MATRIX_1:38;
A27: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38;
A28: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38;
A29: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38;
A30: 1 <= j1 by A21, MATRIX_1:38;
p `1 = E-bound (L~ (Cage (C,n))) by A2, JORDAN1A:83, PSCOMP_1:50;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A22, A18, A11, A30, A27, JORDAN1A:71;
then A31: len (Gauge (C,n)) <= i1 by A26, A30, A27, GOBOARD5:3;
A32: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38;
then A33: i1 = len (Gauge (C,n)) by A31, XXREAL_0:1;
A34: 1 <= i2 by A23, MATRIX_1:38;
A35: i1 = i2
proof
assume i1 <> i2 ; ::_thesis: contradiction
then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
hence contradiction by A22, A24, A25, A18, A19, A26, A32, A34, A28, A30, A29, GOBOARD5:3; ::_thesis: verum
end;
then A36: j2 < width (Gauge (C,n)) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10:1, NAT_1:13;
A37: 1 <= j2 by A23, MATRIX_1:38;
j2 <= j2 + 1 by NAT_1:11;
then A38: ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10:1, JORDAN1A:19;
then p `2 <= ((Cage (C,n)) /. i) `2 by A15, A16, TOPREAL1:4;
then (E-max C) `2 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(j2 + 1))) `2 by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10:1, TOPREAL1:def_11;
then A39: (E-max C) `2 <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 by A13, A14, A21, A22, A23, A24, A25, A30, A27, A35, A31, A7, GOBOARD5:1, JORDAN10:1;
((Cage (C,n)) /. (i + 1)) `2 <= p `2 by A15, A16, A38, TOPREAL1:4;
then ((Gauge (C,n)) * ((len (Gauge (C,n))),j2)) `2 <= (E-max C) `2 by A3, A24, A35, A33, TOPREAL1:def_11;
then A40: ((Gauge (C,n)) * (1,j2)) `2 <= (E-max C) `2 by A29, A37, A7, GOBOARD5:1;
len (Gauge (C,n)) >= 1 + 1 by A6, XXREAL_0:2;
then A41: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2;
then ((Gauge (C,n)) * (i1,1)) `1 >= (E-max C) `1 by A11, A33, A7, A9, A5, SPRECT_3:13;
then E-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A9, A40, A39, A10;
then E-max C in cell ((Gauge (C,n)),(i2 -' 1),j2) by A37, A35, A33, A36, A41, A4, A8, GOBRD11:32;
hence E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13:28, JORDAN10:1; ::_thesis: verum
end;
theorem :: JORDAN1D:12
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th11;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: E-max C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence E-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th13: :: JORDAN1D:13
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (south_halfline (S-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:88, PSCOMP_1:58;
A2: p in (south_halfline (S-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in south_halfline (S-min C) by XBOOLE_0:def_4;
A4: S-min C = |[((S-min C) `1),((S-min C) `2)]| by EUCLID:53;
A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A6: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A8: 1 <= i and
A9: i + 1 <= len (Cage (C,n)) and
A10: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A11: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A8, A9, TOPREAL1:def_3;
A12: (S-min C) `2 = S-bound C by EUCLID:52
.= ((Gauge (C,n)) * (1,2)) `2 by A7, JORDAN8:13 ;
A13: S-min C in S-most C by PSCOMP_1:58;
thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A8, A9, NAT_1:13; ::_thesis: S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A15: ((Cage (C,n)) /. i) `2 = p `2 by A3, A10, A13, A11, JORDAN1A:80, SPPOL_1:40;
A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A17: [i1,j1] in Indices (Gauge (C,n)) and
A18: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A19: [i2,j2] in Indices (Gauge (C,n)) and
A20: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A21: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A8, A9, JORDAN8:3;
A22: 1 <= i1 by A17, MATRIX_1:38;
A23: 1 <= j2 by A19, MATRIX_1:38;
A24: i2 <= i2 + 1 by NAT_1:11;
A25: j2 <= width (Gauge (C,n)) by A19, MATRIX_1:38;
A26: i1 <= len (Gauge (C,n)) by A17, MATRIX_1:38;
A27: j1 <= width (Gauge (C,n)) by A17, MATRIX_1:38;
p `2 = S-bound (L~ (Cage (C,n))) by A2, JORDAN1A:84, PSCOMP_1:58;
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,1)) `2 by A18, A15, A22, A26, JORDAN1A:72;
then A28: 1 >= j1 by A22, A26, A27, GOBOARD5:4;
A29: 1 <= j1 by A17, MATRIX_1:38;
then A30: j1 = 1 by A28, XXREAL_0:1;
A31: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A10, A14, A13, A11, JORDAN1A:80, SPPOL_1:40;
A32: j1 = j2
proof
assume j1 <> j2 ; ::_thesis: contradiction
then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5:4; ::_thesis: verum
end;
then A33: i2 < len (Gauge (C,n)) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10:3, NAT_1:13;
1 <= i2 by A19, MATRIX_1:38;
then A34: ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10:3, JORDAN1A:18;
then p `1 <= ((Cage (C,n)) /. i) `1 by A10, A11, TOPREAL1:3;
then A35: (S-min C) `1 <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10:3, TOPREAL1:def_12;
((Cage (C,n)) /. (i + 1)) `1 <= p `1 by A10, A11, A34, TOPREAL1:3;
then A36: ((Gauge (C,n)) * (i2,1)) `1 <= (S-min C) `1 by A3, A20, A32, A30, TOPREAL1:def_12;
A37: 1 <= i2 by A19, MATRIX_1:38;
1 + 1 <= len (Gauge (C,n)) by A6, XXREAL_0:2;
then ((Gauge (C,n)) * (1,j1)) `2 <= (S-min C) `2 by A5, A30, A7, A12, SPRECT_3:12;
then S-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4;
then S-min C in cell ((Gauge (C,n)),i2,j1) by A5, A30, A37, A33, A7, GOBRD11:32;
hence S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13:26, JORDAN10:3; ::_thesis: verum
end;
theorem :: JORDAN1D:14
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: S-min C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence S-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th15: :: JORDAN1D:15
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:88, PSCOMP_1:58;
A2: p in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in south_halfline (S-max C) by XBOOLE_0:def_4;
A4: S-max C = |[((S-max C) `1),((S-max C) `2)]| by EUCLID:53;
A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A6: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A8: 1 <= i and
A9: i + 1 <= len (Cage (C,n)) and
A10: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A11: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A8, A9, TOPREAL1:def_3;
A12: (S-max C) `2 = S-bound C by EUCLID:52
.= ((Gauge (C,n)) * (1,2)) `2 by A7, JORDAN8:13 ;
A13: S-max C in S-most C by PSCOMP_1:58;
thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A8, A9, NAT_1:13; ::_thesis: S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A15: ((Cage (C,n)) /. i) `2 = p `2 by A3, A10, A13, A11, JORDAN1A:80, SPPOL_1:40;
A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A17: [i1,j1] in Indices (Gauge (C,n)) and
A18: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A19: [i2,j2] in Indices (Gauge (C,n)) and
A20: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A21: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A8, A9, JORDAN8:3;
A22: 1 <= i1 by A17, MATRIX_1:38;
A23: 1 <= j2 by A19, MATRIX_1:38;
A24: i2 <= i2 + 1 by NAT_1:11;
A25: j2 <= width (Gauge (C,n)) by A19, MATRIX_1:38;
A26: i1 <= len (Gauge (C,n)) by A17, MATRIX_1:38;
A27: j1 <= width (Gauge (C,n)) by A17, MATRIX_1:38;
p `2 = S-bound (L~ (Cage (C,n))) by A2, JORDAN1A:84, PSCOMP_1:58;
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,1)) `2 by A18, A15, A22, A26, JORDAN1A:72;
then A28: 1 >= j1 by A22, A26, A27, GOBOARD5:4;
A29: 1 <= j1 by A17, MATRIX_1:38;
then A30: j1 = 1 by A28, XXREAL_0:1;
A31: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A10, A14, A13, A11, JORDAN1A:80, SPPOL_1:40;
A32: j1 = j2
proof
assume j1 <> j2 ; ::_thesis: contradiction
then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5:4; ::_thesis: verum
end;
then A33: i2 < len (Gauge (C,n)) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10:3, NAT_1:13;
1 <= i2 by A19, MATRIX_1:38;
then A34: ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10:3, JORDAN1A:18;
then p `1 <= ((Cage (C,n)) /. i) `1 by A10, A11, TOPREAL1:3;
then A35: (S-max C) `1 <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10:3, TOPREAL1:def_12;
((Cage (C,n)) /. (i + 1)) `1 <= p `1 by A10, A11, A34, TOPREAL1:3;
then A36: ((Gauge (C,n)) * (i2,1)) `1 <= (S-max C) `1 by A3, A20, A32, A30, TOPREAL1:def_12;
A37: 1 <= i2 by A19, MATRIX_1:38;
1 + 1 <= len (Gauge (C,n)) by A6, XXREAL_0:2;
then ((Gauge (C,n)) * (1,j1)) `2 <= (S-max C) `2 by A5, A30, A7, A12, SPRECT_3:12;
then S-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4;
then S-max C in cell ((Gauge (C,n)),i2,j1) by A5, A30, A37, A33, A7, GOBRD11:32;
hence S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13:26, JORDAN10:3; ::_thesis: verum
end;
theorem :: JORDAN1D:16
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th15;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: S-max C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence S-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th17: :: JORDAN1D:17
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:89, PSCOMP_1:34;
A2: p in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in west_halfline (W-min C) by XBOOLE_0:def_4;
A4: W-min C = |[((W-min C) `1),((W-min C) `2)]| by EUCLID:53;
A5: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A6: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A7: (W-min C) `1 = W-bound C by EUCLID:52
.= ((Gauge (C,n)) * (2,1)) `1 by A6, JORDAN8:11 ;
A8: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A9: W-min C in W-most C by PSCOMP_1:34;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A10: 1 <= i and
A11: i + 1 <= len (Cage (C,n)) and
A12: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A13: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A10, A11, TOPREAL1:def_3;
thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A10, A11, NAT_1:13; ::_thesis: W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A15: ((Cage (C,n)) /. i) `1 = p `1 by A3, A12, A9, A13, JORDAN1A:81, SPPOL_1:41;
A16: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A12, A14, A9, A13, JORDAN1A:81, SPPOL_1:41;
A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A18: [i1,j1] in Indices (Gauge (C,n)) and
A19: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A20: [i2,j2] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A22: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;
A23: i1 <= len (Gauge (C,n)) by A18, MATRIX_1:38;
A24: i2 <= len (Gauge (C,n)) by A20, MATRIX_1:38;
A25: j2 <= width (Gauge (C,n)) by A20, MATRIX_1:38;
A26: j1 <= width (Gauge (C,n)) by A18, MATRIX_1:38;
A27: 1 <= j1 by A18, MATRIX_1:38;
p `1 = W-bound (L~ (Cage (C,n))) by A2, JORDAN1A:85, PSCOMP_1:34;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (1,j1)) `1 by A19, A15, A8, A27, A26, JORDAN1A:73;
then A28: 1 >= i1 by A23, A27, A26, GOBOARD5:3;
A29: 1 <= i1 by A18, MATRIX_1:38;
then A30: i1 = 1 by A28, XXREAL_0:1;
A31: 1 <= i2 by A20, MATRIX_1:38;
A32: i1 = i2
proof
assume i1 <> i2 ; ::_thesis: contradiction
then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5:3; ::_thesis: verum
end;
then A33: j1 < width (Gauge (C,n)) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10:2, NAT_1:13;
j1 <= j1 + 1 by NAT_1:11;
then A34: ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10:2, JORDAN1A:19;
then p `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A12, A13, TOPREAL1:4;
then A35: (W-min C) `2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10:2, TOPREAL1:def_13;
((Cage (C,n)) /. i) `2 <= p `2 by A12, A13, A34, TOPREAL1:4;
then A36: ((Gauge (C,n)) * (1,j1)) `2 <= (W-min C) `2 by A3, A19, A30, TOPREAL1:def_13;
1 + 1 <= len (Gauge (C,n)) by A5, XXREAL_0:2;
then ((Gauge (C,n)) * (i1,1)) `1 <= (W-min C) `1 by A8, A30, A6, A7, SPRECT_3:13;
then W-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4;
then W-min C in cell ((Gauge (C,n)),i1,j1) by A27, A30, A33, A6, GOBRD11:32;
hence W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13:22, JORDAN10:2; ::_thesis: verum
end;
theorem :: JORDAN1D:18
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th17;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: W-min C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence W-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th19: :: JORDAN1D:19
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (west_halfline (W-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:89, PSCOMP_1:34;
A2: p in (west_halfline (W-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1;
then A3: p in west_halfline (W-max C) by XBOOLE_0:def_4;
A4: W-max C = |[((W-max C) `1),((W-max C) `2)]| by EUCLID:53;
A5: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A6: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A7: (W-max C) `1 = W-bound C by EUCLID:52
.= ((Gauge (C,n)) * (2,1)) `1 by A6, JORDAN8:11 ;
A8: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A9: W-max C in W-most C by PSCOMP_1:34;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A10: 1 <= i and
A11: i + 1 <= len (Cage (C,n)) and
A12: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A13: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A10, A11, TOPREAL1:def_3;
thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A10, A11, NAT_1:13; ::_thesis: W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A15: ((Cage (C,n)) /. i) `1 = p `1 by A3, A12, A9, A13, JORDAN1A:81, SPPOL_1:41;
A16: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A12, A14, A9, A13, JORDAN1A:81, SPPOL_1:41;
A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A18: [i1,j1] in Indices (Gauge (C,n)) and
A19: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A20: [i2,j2] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A22: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;
A23: i1 <= len (Gauge (C,n)) by A18, MATRIX_1:38;
A24: i2 <= len (Gauge (C,n)) by A20, MATRIX_1:38;
A25: j2 <= width (Gauge (C,n)) by A20, MATRIX_1:38;
A26: j1 <= width (Gauge (C,n)) by A18, MATRIX_1:38;
A27: 1 <= j1 by A18, MATRIX_1:38;
p `1 = W-bound (L~ (Cage (C,n))) by A2, JORDAN1A:85, PSCOMP_1:34;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (1,j1)) `1 by A19, A15, A8, A27, A26, JORDAN1A:73;
then A28: 1 >= i1 by A23, A27, A26, GOBOARD5:3;
A29: 1 <= i1 by A18, MATRIX_1:38;
then A30: i1 = 1 by A28, XXREAL_0:1;
A31: 1 <= i2 by A20, MATRIX_1:38;
A32: i1 = i2
proof
assume i1 <> i2 ; ::_thesis: contradiction
then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5:3; ::_thesis: verum
end;
then A33: j1 < width (Gauge (C,n)) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10:2, NAT_1:13;
j1 <= j1 + 1 by NAT_1:11;
then A34: ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10:2, JORDAN1A:19;
then p `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A12, A13, TOPREAL1:4;
then A35: (W-max C) `2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10:2, TOPREAL1:def_13;
((Cage (C,n)) /. i) `2 <= p `2 by A12, A13, A34, TOPREAL1:4;
then A36: ((Gauge (C,n)) * (1,j1)) `2 <= (W-max C) `2 by A3, A19, A30, TOPREAL1:def_13;
1 + 1 <= len (Gauge (C,n)) by A5, XXREAL_0:2;
then ((Gauge (C,n)) * (i1,1)) `1 <= (W-max C) `1 by A8, A30, A6, A7, SPRECT_3:13;
then W-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4;
then W-max C in cell ((Gauge (C,n)),i1,j1) by A27, A30, A33, A6, GOBRD11:32;
hence W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13:22, JORDAN10:2; ::_thesis: verum
end;
theorem :: JORDAN1D:20
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) )
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
consider i being Element of NAT such that
A2: 1 <= i and
A3: i < len (Cage (C,n)) and
A4: W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th19;
take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) )
thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: W-max C in right_cell ((Cage (C,n)),i)
i + 1 <= len (Cage (C,n)) by A3, NAT_1:13;
then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33;
hence W-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum
end;
theorem Th21: :: JORDAN1D:21
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:39;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = N-min (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = N-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
thus A7: ( 1 <= i & i <= len (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n))))
A8: 1 <= j by A5, MATRIX_1:38;
A9: now__::_thesis:_not_j_<_width_(Gauge_(C,n))
assume j < width (Gauge (C,n)) ; ::_thesis: contradiction
then (N-min (L~ (Cage (C,n)))) `2 < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by A4, A6, A7, A8, GOBOARD5:4;
then N-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:70; ::_thesis: verum
end;
j <= width (Gauge (C,n)) by A5, MATRIX_1:38;
hence N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:22
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
N-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:40;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = N-max (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = N-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
thus A7: ( 1 <= i & i <= len (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n))))
A8: 1 <= j by A5, MATRIX_1:38;
A9: now__::_thesis:_not_j_<_width_(Gauge_(C,n))
assume j < width (Gauge (C,n)) ; ::_thesis: contradiction
then (N-max (L~ (Cage (C,n)))) `2 < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by A4, A6, A7, A8, GOBOARD5:4;
then N-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:70; ::_thesis: verum
end;
j <= width (Gauge (C,n)) by A5, MATRIX_1:38;
hence N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:23
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )
consider i being Element of NAT such that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) and
A3: N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by Th21;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )
thus ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:39; ::_thesis: verum
end;
theorem Th24: :: JORDAN1D:24
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
E-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:45;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = E-min (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = E-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j)
A8: 1 <= i by A5, MATRIX_1:38;
A9: now__::_thesis:_not_i_<_len_(Gauge_(C,n))
assume i < len (Gauge (C,n)) ; ::_thesis: contradiction
then (E-min (L~ (Cage (C,n)))) `1 < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A6, A7, A8, GOBOARD5:3;
then E-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:71; ::_thesis: verum
end;
i <= len (Gauge (C,n)) by A5, MATRIX_1:38;
hence E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:25
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = E-max (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = E-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j)
A8: 1 <= i by A5, MATRIX_1:38;
A9: now__::_thesis:_not_i_<_len_(Gauge_(C,n))
assume i < len (Gauge (C,n)) ; ::_thesis: contradiction
then (E-max (L~ (Cage (C,n)))) `1 < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A6, A7, A8, GOBOARD5:3;
then E-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:71; ::_thesis: verum
end;
i <= len (Gauge (C,n)) by A5, MATRIX_1:38;
hence E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:26
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) )
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by Th24;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) )
thus ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:45; ::_thesis: verum
end;
theorem Th27: :: JORDAN1D:27
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
S-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:41;
then consider m being Nat such that
A1: m in dom (Cage (C,n)) and
A2: (Cage (C,n)) . m = S-min (L~ (Cage (C,n))) by FINSEQ_2:10;
A3: (Cage (C,n)) /. m = S-min (L~ (Cage (C,n))) by A1, A2, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A1, GOBOARD1:def_9;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
thus A6: ( 1 <= i & i <= len (Gauge (C,n)) ) by A4, MATRIX_1:38; ::_thesis: S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
A7: j <= width (Gauge (C,n)) by A4, MATRIX_1:38;
A8: now__::_thesis:_not_j_>_1
assume j > 1 ; ::_thesis: contradiction
then (S-min (L~ (Cage (C,n)))) `2 > ((Gauge (C,n)) * (i,1)) `2 by A3, A5, A6, A7, GOBOARD5:4;
then S-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (i,1)) `2 by EUCLID:52;
hence contradiction by A6, JORDAN1A:72; ::_thesis: verum
end;
1 <= j by A4, MATRIX_1:38;
hence S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:28
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42;
then consider m being Nat such that
A1: m in dom (Cage (C,n)) and
A2: (Cage (C,n)) . m = S-max (L~ (Cage (C,n))) by FINSEQ_2:10;
A3: (Cage (C,n)) /. m = S-max (L~ (Cage (C,n))) by A1, A2, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A1, GOBOARD1:def_9;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
thus A6: ( 1 <= i & i <= len (Gauge (C,n)) ) by A4, MATRIX_1:38; ::_thesis: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
A7: j <= width (Gauge (C,n)) by A4, MATRIX_1:38;
A8: now__::_thesis:_not_j_>_1
assume j > 1 ; ::_thesis: contradiction
then (S-max (L~ (Cage (C,n)))) `2 > ((Gauge (C,n)) * (i,1)) `2 by A3, A5, A6, A7, GOBOARD5:4;
then S-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (i,1)) `2 by EUCLID:52;
hence contradiction by A6, JORDAN1A:72; ::_thesis: verum
end;
1 <= j by A4, MATRIX_1:38;
hence S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:29
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) )
consider i being Element of NAT such that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) and
A3: S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by Th27;
take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) )
thus ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:41; ::_thesis: verum
end;
theorem Th30: :: JORDAN1D:30
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = W-min (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = W-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j)
A8: i <= len (Gauge (C,n)) by A5, MATRIX_1:38;
A9: now__::_thesis:_not_i_>_1
assume i > 1 ; ::_thesis: contradiction
then (W-min (L~ (Cage (C,n)))) `1 > ((Gauge (C,n)) * (1,j)) `1 by A4, A6, A7, A8, GOBOARD5:3;
then W-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (1,j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:73; ::_thesis: verum
end;
1 <= i by A5, MATRIX_1:38;
hence W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:31
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
W-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:44;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = W-max (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = W-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge (C,n)) and
A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j)
A8: i <= len (Gauge (C,n)) by A5, MATRIX_1:38;
A9: now__::_thesis:_not_i_>_1
assume i > 1 ; ::_thesis: contradiction
then (W-max (L~ (Cage (C,n)))) `1 > ((Gauge (C,n)) * (1,j)) `1 by A4, A6, A7, A8, GOBOARD5:3;
then W-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (1,j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:73; ::_thesis: verum
end;
1 <= i by A5, MATRIX_1:38;
hence W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum
end;
theorem :: JORDAN1D:32
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) )
consider j being Element of NAT such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by Th30;
take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) )
thus ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:43; ::_thesis: verum
end;