let i, m, n be Nat; :: thesis: 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 ) }
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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 ) }
let k be 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 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 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( Nat) -> set = { (cell ((Gauge (D,(i + $1))),a,b)) where a, b is 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[ Nat] means cell ((Gauge (D,i)),m,n) = union H1($1);
A5: for w being Nat st S1[w] holds
S1[w + 1]
proof
let w be 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 Nat holds 2 * ((a div 2) + 1) = a + 1
let a be odd Nat; :: thesis: 2 * ((a div 2) + 1) = a + 1
consider e being 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:18
.= a + 1 by A10 ; :: thesis: verum
end;
A12: now :: thesis: for m being Nat holds 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1
let m be 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 Nat
for a being odd 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 Nat; :: thesis: for a being odd 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 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 Nat holds 2 * ((a div 2) + 1) = a + 2
let a be even Nat; :: thesis: 2 * ((a div 2) + 1) = a + 2
A16: ex e being 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:18 ; :: thesis: verum
end;
A17: now :: thesis: for m being Nat
for a being even 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 Nat; :: thesis: for a being even 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 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 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( Nat, 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 Nat st 2 <= m holds
0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2
let a, m be 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 ;
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 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 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)
per cases ( a is odd or a is even ) ;
suppose A34: 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;
suppose A35: 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 Nat holds 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2
let m be 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 Nat
for a being even 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 Nat; :: thesis: for a being even 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 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 Nat
for a being odd 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 Nat; :: thesis: for a being odd 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 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;
per cases ( ( 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 ) ) ;
suppose A44: ( 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;
suppose A49: ( 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;
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; :: thesis: verum
end;
suppose A57: ( 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; :: thesis: verum
end;
suppose A64: ( 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 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 Nat st 2 <= m holds
0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2
let m be 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 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 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 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 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 object ; :: 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 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 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 object ; :: 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 Nat holds
( (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = m & (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m )
let m be 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
.= 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 object ; :: 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 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 Nat st (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 holds
a = m
let a, m be 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 object ; :: 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 Nat holds S1[w] from NAT_1:sch 2(A117, A5);
 hence 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 ) } ; :: thesis: verum