let i, j be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of st i <= j holds
for a, b being Element of NAT st 2 <= a & a <= (len (Gauge C,i)) - 1 & 2 <= b & b <= (len (Gauge C,i)) - 1 holds
ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
let C be compact non horizontal non vertical Subset of ; :: thesis: ( i <= j implies for a, b being Element of NAT st 2 <= a & a <= (len (Gauge C,i)) - 1 & 2 <= b & b <= (len (Gauge C,i)) - 1 holds
ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )
A1: 0 <> 2 |^ i by NEWTON:102;
assume A2: i <= j ; :: thesis: for a, b being Element of NAT st 2 <= a & a <= (len (Gauge C,i)) - 1 & 2 <= b & b <= (len (Gauge C,i)) - 1 holds
ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
then A3: (2 |^ (j -' i)) * (2 |^ i) = ((2 |^ j) / (2 |^ i)) * (2 |^ i) by TOPREAL6:15
.= 2 |^ j by A1, XCMPLX_1:88 ;
let a, b be Element of NAT ; :: thesis: ( 2 <= a & a <= (len (Gauge C,i)) - 1 & 2 <= b & b <= (len (Gauge C,i)) - 1 implies ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )
assume that
A4: 2 <= a and
A5: a <= (len (Gauge C,i)) - 1 and
A6: 2 <= b and
A7: b <= (len (Gauge C,i)) - 1 ; :: thesis: ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
A8: ( 1 <= a & 1 <= b ) by A4, A6, XXREAL_0:2;
set c = 2 + ((2 |^ (j -' i)) * (a -' 2));
set d = 2 + ((2 |^ (j -' i)) * (b -' 2));
A9: 0 <= b - 2 by A6, XREAL_1:50;
set n = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
A10: 0 <> 2 |^ j by NEWTON:102;
A11: (((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2) = (((N-bound C) - (S-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2)) by A2, TOPREAL6:15
.= ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2)
.= (((N-bound C) - (S-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2) by XCMPLX_1:82
.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b -' 2) by A10, XCMPLX_1:52
.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2) by A9, XREAL_0:def 2 ;
take 2 + ((2 |^ (j -' i)) * (a -' 2)) ; :: thesis: ex d being Element of NAT st
( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),d & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
take 2 + ((2 |^ (j -' i)) * (b -' 2)) ; :: thesis: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge C,j)) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge C,j)) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
A12: 2 + 0 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XREAL_1:8;
then A13: 1 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XXREAL_0:2;
((2 |^ i) + 2) - 2 >= 0 ;
then A14: ((2 |^ i) + 2) -' 2 = (2 |^ i) + 0 by XREAL_0:def 2;
A15: 0 <= a - 2 by A4, XREAL_1:50;
A16: (((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2) = (((E-bound C) - (W-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2)) by A2, TOPREAL6:15
.= ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2)
.= (((E-bound C) - (W-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2) by XCMPLX_1:82
.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a -' 2) by A10, XCMPLX_1:52
.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2) by A15, XREAL_0:def 2 ;
A17: (len (Gauge C,j)) - 1 < (len (Gauge C,j)) - 0 by XREAL_1:17;
A18: (len (Gauge C,i)) - 1 = ((2 |^ i) + 3) - 1 by JORDAN8:def 1
.= (2 |^ i) + 2 ;
then a -' 2 <= ((2 |^ i) + 2) -' 2 by A5, NAT_D:42;
then A19: (2 |^ (j -' i)) * (a -' 2) <= 2 |^ j by A14, A3, XREAL_1:66;
b -' 2 <= ((2 |^ i) + 2) -' 2 by A7, A18, NAT_D:42;
then A20: (2 |^ (j -' i)) * (b -' 2) <= 2 |^ j by A14, A3, XREAL_1:66;
A21: (len (Gauge C,i)) - 1 < (len (Gauge C,i)) - 0 by XREAL_1:17;
then A22: a <= len (Gauge C,i) by A5, XXREAL_0:2;
(len (Gauge C,j)) - 1 = ((2 |^ j) + 3) - 1 by JORDAN8:def 1
.= (2 |^ j) + 2 ;
hence A23: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge C,j)) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge C,j)) - 1 ) by A19, A20, A12, XREAL_1:8; :: thesis: ( [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
then A24: 1 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) by XXREAL_0:2;
width (Gauge C,j) = len (Gauge C,j) by JORDAN8:def 1;
then A25: 2 + ((2 |^ (j -' i)) * (b -' 2)) <= width (Gauge C,j) by A23, A17, XXREAL_0:2;
2 + ((2 |^ (j -' i)) * (a -' 2)) <= len (Gauge C,j) by A23, A17, XXREAL_0:2;
hence [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge C,j) by A13, A24, A25, MATRIX_1:37; :: thesis: ( (Gauge C,i) * a,b = (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
then A26: (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2)))]| by JORDAN8:def 1;
width (Gauge C,i) = len (Gauge C,i) by JORDAN8:def 1;
then b <= width (Gauge C,i) by A7, A21, XXREAL_0:2;
then [a,b] in Indices (Gauge C,i) by A22, A8, MATRIX_1:37;
then A27: (Gauge C,i) * a,b = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def 1;
then A28: ((Gauge C,i) * a,b) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)) by EUCLID:56
.= ((Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) `2 by A26, A11, EUCLID:56 ;
((Gauge C,i) * a,b) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27, EUCLID:56
.= ((Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) `1 by A26, A16, EUCLID:56 ;
hence (Gauge C,i) * a,b = (Gauge C,j) * (2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))) by A28, TOPREAL3:11; :: thesis: ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
thus ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) ; :: thesis: verum