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
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
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:11
.= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:11
.= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ; :: thesis: verum
end;
A13: now
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:8;
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:70; :: thesis: verum
end;
A15: now
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
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:20;
then (a + 1) + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:8;
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:70; :: 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
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:13
.= (2 |^ (w + 1)) * 2 by NEWTON:10 ;
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:66;
then 0 <= ((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1)) by XREAL_1:50;
hence 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by XREAL_1:8; :: 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:26;
then A26: 1 + 1 <= (a div 2) + 1 by Lm2, XREAL_1:8;
A27: now
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:70;
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:8;
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:11;
then (2 |^ (w + 1)) * (m - 1) <= (2 |^ (w + 1)) * (2 |^ i) by XREAL_1:66;
then ((2 |^ (w + 1)) * (m - 1)) + 5 < ((2 |^ (w + 1)) * (2 |^ i)) + 6 by XREAL_1:10;
then A29: ((2 |^ (w + 1)) * (m - 1)) + 5 < (2 |^ ((w + 1) + i)) + 6 by NEWTON:13;
then A30: (((2 |^ (w + 1)) * (m - 1)) + 1) + (3 + 1) < (2 * (2 |^ (i + w))) + 6 by A8, NEWTON:11;
A31: ((((2 |^ (w + 1)) * (m - 1)) + 1) + 3) + 1 < (2 * (2 |^ (i + w))) + (2 * 3) by A8, A29, NEWTON:11;
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:8;
then A32: (a + 3) + 0 < (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by XREAL_1:10;
then A33: (a + 3) + 1 <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by INT_1:20;
now
per cases ( not a is even or a is even ) ;
suppose A34: not 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 + 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:66; :: 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:26;
then A37: 1 + 1 <= (b div 2) + 1 by Lm2, XREAL_1:8;
((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, Th9;
A39: now
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:11
.= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:11
.= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 ; :: thesis: verum
end;
A40: now
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:8;
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:70; :: thesis: verum
end;
A42: now
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:8;
then A43: (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) + 1 <= a + 1 by INT_1:20;
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:70; :: thesis: verum
end;
per cases ( ( not a is even & not b is even ) or ( not a is even & b is even ) or ( a is even & not b is even ) or ( a is even & b is even ) ) ;
suppose A44: ( not a is even & not b is even ) ; :: 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: ( not a is even & 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;
suppose A57: ( a is even & not b is even ) ; :: 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;
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:18;
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
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:66;
then (2 |^ w) * m >= 2 |^ (w + 1) by NEWTON:11;
then 0 <= ((2 |^ w) * m) - (2 |^ (w + 1)) by XREAL_1:50;
hence 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by XREAL_1:8; :: 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:17;
(2 * a) -' 1 = (2 * a) - 1 by A78, Lm8, XXREAL_0:2;
then A84: (2 * a) -' 2 < (2 * a) -' 1 by A79, XREAL_1:17;
hereby :: according to TARSKI:def 3 :: thesis: x c= union K
A85: now
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:66;
then 2 * a <= (((2 * (2 |^ w)) * m) - (2 * (2 |^ w))) + 2 ;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 * (2 |^ w))) + 2 by NEWTON:11;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2 by NEWTON:11;
then (2 * a) - 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by XREAL_1:11;
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:8;
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:20;
then A89: (2 * a) -' 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A78, Lm9, XXREAL_0:2;
A90: now
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:66;
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:11;
then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4 <= 2 * a by NEWTON:11;
then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) - 2 <= (2 * a) - 2 by XREAL_1:11;
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:20;
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
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:11;
then m - 1 < (2 |^ i) + (3 - 2) ;
then m - 1 <= (2 |^ i) + 0 by INT_1:20;
then (2 |^ w) * (m - 1) <= (2 |^ w) * (2 |^ i) by XREAL_1:66;
then (2 |^ w) * (m - 1) <= 2 |^ (w + i) by NEWTON:13;
then A99: ((2 |^ w) * (m - 1)) + 3 <= (2 |^ (w + i)) + 3 by XREAL_1:8;
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:8;
then a + 1 < (((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) + 1 by XREAL_1:147;
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, Th9;
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
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:9;
hence (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 = (m - 2) + 2 by NEWTON:10
.= m ;
:: thesis: (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = m
thus (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = (m - 1) + 1 by A102, NEWTON:9
.= 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
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:31;
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