environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, EUCLID, RCOMP_1, SPPOL_1, RELAT_2, GOBOARD1, PRE_TOPC, RELAT_1, ARYTM_3, INT_1, CARD_1, FINSEQ_1, ABIAN, ARYTM_1, TOPREAL2, FUNCT_1, GOBOARD5, TOPREAL1, PSCOMP_1, MCART_1, RLTOPSP1, JORDAN2C, JORDAN6, TARSKI, XXREAL_1, XXREAL_0, REAL_1, TREES_1, MATRIX_1, PARTFUN1, TOPS_1, COMPLEX1, JORDAN8, NEWTON, CONNSP_1, JORDAN9, GOBOARD9, JORDAN1A, CONVEX1, XXREAL_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, STRUCT_0, FINSEQ_1, NEWTON, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, GOBOARD1, MATRIX_0, RCOMP_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, SPPOL_1, ABIAN, GOBOARD5, GOBOARD9, JORDAN6, JORDAN8, JORDAN9, JORDAN2C;
definitions TARSKI, ABIAN, XBOOLE_0;
theorems EUCLID, GOBOARD7, JORDAN8, JORDAN9, JORDAN10, PSCOMP_1, NAT_1, NEWTON, SPRECT_1, FUNCT_1, ABSVALUE, TOPREAL1, SPRECT_3, GOBRD11, GOBOARD5, JORDAN2C, GOBRD14, SUBSET_1, ZFMISC_1, TARSKI, TOPREAL3, FINSEQ_1, GOBOARD1, SPPOL_1, SPPOL_2, GOBOARD9, CONNSP_1, TOPREAL6, FINSEQ_6, SPRECT_2, INT_1, TOPS_1, JGRAPH_1, JORDAN6, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, PEPIN, XREAL_1, XXREAL_0, PREPOWER, ABIAN, NAT_D, PARTFUN1, MATRIX_0, XXREAL_1, RLTOPSP1;
schemes NAT_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, STRUCT_0, MONOID_0, EUCLID, JORDAN1, PSCOMP_1, SPRECT_1, SPRECT_2, SPRECT_3, JORDAN2C, TOPREAL6, JORDAN8, JORDAN10, FUNCT_1, NEWTON, INT_1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_D, RCOMP_1, NEWTON, ABIAN, TOPS_1, CONNSP_1, MONOID_0, PSCOMP_1, GOBOARD9, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, RELSET_1, CONVEX1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, PSCOMP_1;
expansions TARSKI, XBOOLE_0;
3 = (2 * 1) + 1
;
then Lm1:
3 div 2 = 1
by NAT_D:def 1;
1 = (2 * 0) + 1
;
then Lm2:
1 div 2 = 0
by NAT_D:def 1;
theorem Th33:
for
i,
j,
m,
n being
Nat for
D being non
empty Subset of
(TOP-REAL 2) st
m <= n & 1
< i &
i < len (Gauge (D,m)) & 1
< j &
j < width (Gauge (D,m)) holds
for
i1,
j1 being
Nat st
i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 &
j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
(Gauge (D,m)) * (
i,
j)
= (Gauge (D,n)) * (
i1,
j1)
Lm3:
now for D being non empty Subset of (TOP-REAL 2)
for n being Nat holds
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )
let D be non
empty Subset of
(TOP-REAL 2);
for n being Nat holds
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )let n be
Nat;
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )set G =
Gauge (
D,
n);
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1
by XREAL_1:6;
hence
1
<= Center (Gauge (D,n))
;
Center (Gauge (D,n)) <= len (Gauge (D,n))
0 < len (Gauge (D,n))
by JORDAN8:10;
then
(len (Gauge (D,n))) div 2
< len (Gauge (D,n))
by INT_1:56;
hence
Center (Gauge (D,n)) <= len (Gauge (D,n))
by NAT_1:13;
verum
end;
Lm4:
now for D being non empty Subset of (TOP-REAL 2)
for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))let n,
j be
Nat;
( 1 <= j & j <= len (Gauge (D,n)) implies [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) )set G =
Gauge (
D,
n);
assume A1:
( 1
<= j &
j <= len (Gauge (D,n)) )
;
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))A2:
(
len (Gauge (D,n)) = width (Gauge (D,n)) &
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1 )
by JORDAN8:def 1, XREAL_1:6;
Center (Gauge (D,n)) <= len (Gauge (D,n))
by Lm3;
hence
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))
by A1, A2, MATRIX_0:30;
verum
end;
Lm5:
now for D being non empty Subset of (TOP-REAL 2)
for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))let n,
j be
Nat;
( 1 <= j & j <= len (Gauge (D,n)) implies [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) )set G =
Gauge (
D,
n);
assume A1:
( 1
<= j &
j <= len (Gauge (D,n)) )
;
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))A2:
(
len (Gauge (D,n)) = width (Gauge (D,n)) &
0 + 1
<= ((len (Gauge (D,n))) div 2) + 1 )
by JORDAN8:def 1, XREAL_1:6;
Center (Gauge (D,n)) <= len (Gauge (D,n))
by Lm3;
hence
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))
by A1, A2, MATRIX_0:30;
verum
end;
Lm6:
for n being Nat
for D being non empty Subset of (TOP-REAL 2)
for w being Real st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2
Lm8:
for m, n being Nat
for c, d being Real st 0 <= c & m <= n holds
d + (c / (2 |^ n)) <= d + (c / (2 |^ m))
by XREAL_1:6, Lm7;
theorem Th36:
for
i,
j,
m,
n being
Nat for
D being non
empty Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (D,n)) & 1
<= j &
j <= len (Gauge (D,m)) & ( (
n > 0 &
m > 0 ) or (
n = 0 &
m = 0 ) ) holds
((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1
theorem
for
i,
j,
m,
n being
Nat for
D being non
empty Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (D,n)) & 1
<= j &
j <= len (Gauge (D,m)) & ( (
n > 0 &
m > 0 ) or (
n = 0 &
m = 0 ) ) holds
((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2
Lm11:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Nat st [i,1] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Nat st [i,1] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))let n,
i be
Nat;
( [i,1] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[i,1] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (i,1)) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (1 - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))
by EUCLID:52
;
verum
end;
Lm12:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Nat st [1,i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Nat st [1,i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))let n,
i be
Nat;
( [1,i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[1,i] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (1,i)) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))
by EUCLID:52
;
verum
end;
Lm13:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Nat st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Nat st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))let n,
i be
Nat;
( [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[i,(len (Gauge (D,n)))] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))
by EUCLID:52
.=
(N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
Lm14:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Nat st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Nat st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))let n,
i be
Nat;
( [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[(len (Gauge (D,n))),i] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))hence ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))
by EUCLID:52
.=
(E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))
by Lm10
;
verum
end;
theorem Th40:
for
i,
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (E,n)) & 1
<= j &
j <= len (Gauge (E,m)) &
m <= n holds
((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2
theorem
for
i,
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (E,n)) & 1
<= j &
j <= len (Gauge (E,m)) &
m <= n holds
((Gauge (E,n)) * ((len (Gauge (E,n))),i)) `1 <= ((Gauge (E,m)) * ((len (Gauge (E,m))),j)) `1
theorem
for
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n holds
LSeg (
((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n))))))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
theorem
for
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
theorem
for
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))
theorem Th47:
for
i,
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 1
< i &
i + 1
< len (Gauge (E,m)) & 1
< j &
j + 1
< width (Gauge (E,m)) holds
for
i1,
j1 being
Nat st
((2 |^ (n -' m)) * (i - 2)) + 2
<= i1 &
i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 &
((2 |^ (n -' m)) * (j - 2)) + 2
<= j1 &
j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds
cell (
(Gauge (E,n)),
i1,
j1)
c= cell (
(Gauge (E,m)),
i,
j)
theorem
for
i,
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m <= n & 3
<= i &
i < len (Gauge (E,m)) & 1
< j &
j + 1
< width (Gauge (E,m)) holds
for
i1,
j1 being
Nat st
i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 &
j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
cell (
(Gauge (E,n)),
(i1 -' 1),
j1)
c= cell (
(Gauge (E,m)),
(i -' 1),
j)
Lm15:
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )
Lm16:
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )
Lm17:
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )
theorem Th58:
for
k,
n,
t being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k <= len (Cage (C,n)) & 1
<= t &
t <= len (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
t,
(width (Gauge (C,n)))) holds
(Cage (C,n)) /. k in N-most (L~ (Cage (C,n)))
theorem Th61:
for
k,
n,
t being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= k &
k <= len (Cage (C,n)) & 1
<= t &
t <= width (Gauge (C,n)) &
(Cage (C,n)) /. k = (Gauge (C,n)) * (
(len (Gauge (C,n))),
t) holds
(Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))