:: Gauges and Cages. { P } art { II }
:: by Artur Korni{\l}owicz and Robert Milewski
::
:: Received November 6, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


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 end;

Lm4: for A, B, C, D being set holds union {A,B,C,D} = ((A \/ B) \/ C) \/ D
proof 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 end;

registration
let m be non zero Nat;
cluster 2 |^ m -> even ;
coherence
2 |^ m is even
proof end;
end;

registration
let n be even Nat;
let m be non zero Nat;
cluster n |^ m -> even ;
coherence
n |^ m is even
proof end;
end;

theorem Th2: :: JORDAN1D:2
for i being Nat
for r being Real st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i
proof end;

Lm5: now :: thesis: for m being Real st 2 <= m holds
(2 * m) - 2 >= 0
let m be Real; :: 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 st 1 <= m holds
(2 * m) - 1 >= 0
let m be Real; :: 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: for m being Nat st 2 <= m holds
(2 * m) - 2 = (2 * m) -' 2
by Lm5, XREAL_0:def 2;

Lm8: for m being Nat st 1 <= m holds
(2 * m) - 1 = (2 * m) -' 1
by Lm6, XREAL_0:def 2;

Lm9: now :: thesis: for m being Nat st m >= 1 holds
((2 * m) -' 2) + 1 = (2 * m) -' 1
let m be 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 i, m being Nat
for x being Real st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
proof end;

Lm11: for m being Nat st 2 <= m holds
1 <= (2 * m) -' 2
proof end;

Lm12: for m being Nat st 1 <= m holds
1 <= (2 * m) -' 1
proof end;

Lm13: for i, m being Nat st m < (2 |^ i) + 3 holds
(2 * m) -' 2 < (2 |^ (i + 1)) + 3
proof end;

Lm14: now :: thesis: for m being Nat st 2 <= m holds
(((2 * m) -' 2) + 1) - 2 = (2 * m) - 3
let m be 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;

theorem Th3: :: JORDAN1D:3
for a, b, i, m being 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 end;

theorem Th4: :: JORDAN1D:4
for a, b, i, n being 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 end;

Lm15: for i, m being 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 end;

theorem Th5: :: JORDAN1D:5
for i, m, n being 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 end;

theorem :: JORDAN1D:6
for i, m, n being Nat
for D being compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being 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 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 end;

theorem Th7: :: JORDAN1D:7
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:8
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th9: :: JORDAN1D:9
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:10
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th11: :: JORDAN1D:11
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:12
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th13: :: JORDAN1D:13
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:14
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th15: :: JORDAN1D:15
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:16
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th17: :: JORDAN1D:17
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:18
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th19: :: JORDAN1D:19
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
proof end;

theorem :: JORDAN1D:20
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) )
proof end;

theorem Th21: :: JORDAN1D:21
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
proof end;

theorem :: JORDAN1D:22
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
proof end;

theorem :: JORDAN1D:23
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) )
proof end;

theorem Th24: :: JORDAN1D:24
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
proof end;

theorem :: JORDAN1D:25
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) )
proof end;

theorem :: JORDAN1D:26
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) )
proof end;

theorem Th27: :: JORDAN1D:27
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
proof end;

theorem :: JORDAN1D:28
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
proof end;

theorem :: JORDAN1D:29
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) )
proof end;

theorem Th30: :: JORDAN1D:30
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
proof end;

theorem :: JORDAN1D:31
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) )
proof end;

theorem :: JORDAN1D:32
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Nat st
( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) )
proof end;