let m, n, i, j be Element of NAT ; :: thesis:
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
assume that
A1: m <= n and
A2: 1 <= i and
A3: i + 1 <= len (Gauge C,n) and
A4: 1 <= j and
A5: j + 1 <= width (Gauge C,n) ; :: thesis:
reconsider i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/], j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] as Element of NAT by A2, A4, Th41;
set Gm = Gauge C,m;
set Gn = Gauge C,n;
A6: 2 |^ (n -' m) > n -' m by NEWTON:105;
take i1 ; :: thesis:
take j1 ; :: thesis:
thus i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; :: thesis:
thus j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] ; :: thesis:
let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: e in cell (Gauge C,n),i,j ; :: thesis:
then reconsider p = e as Point of (TOP-REAL 2) ;
A8: p `2 <= ((Gauge C,n) * i,(j + 1)) `2 by A2, A3, A4, A5, A7, JORDAN9:19;
( i <= len (Gauge C,n) & j <= width (Gauge C,n) ) by A3, A5, NAT_1:13;
then [i,j] in Indices (Gauge C,n) by A2, A4, MATRIX_1:37;
then A9: (Gauge C,n) * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def 1;
then A10: ((Gauge C,n) * i,j) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i - 2) / 1)) by EUCLID:56
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i - 2) / (2 |^ n))) by XCMPLX_1:86 ;
A11: ((Gauge C,n) * i,j) `1 <= p `1 by A2, A3, A4, A5, A7, JORDAN9:19;
A12: ((Gauge C,n) * i,j) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j - 2) / 1)) by A9, EUCLID:56
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j - 2) / (2 |^ n))) by XCMPLX_1:86 ;
A13: p `1 <= ((Gauge C,n) * (i + 1),j) `1 by A2, A3, A4, A5, A7, JORDAN9:19;
E-bound C >= (W-bound C) + 0 by SPRECT_1:23;
then A14: (E-bound C) - (W-bound C) >= 0 by XREAL_1:21;
( 1 <= j + 1 & i <= len (Gauge C,n) ) by A3, NAT_1:11, NAT_1:13;
then [i,(j + 1)] in Indices (Gauge C,n) by A2, A5, MATRIX_1:37;
then (Gauge C,n) * i,(j + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by JORDAN8:def 1;
then A15: ((Gauge C,n) * i,(j + 1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((j + 1) - 2) / 1)) by EUCLID:56
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j + 1) - 2) / (2 |^ n))) by XCMPLX_1:86 ;
( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:104, XREAL_1:8;
then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2;
then A16: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:122;
A17: ((Gauge C,n) * i,j) `2 <= p `2 by A2, A3, A4, A5, A7, JORDAN9:19;
( 1 <= i + 1 & j <= width (Gauge C,n) ) by A5, NAT_1:11, NAT_1:13;
then [(i + 1),j] in Indices (Gauge C,n) by A3, A4, MATRIX_1:37;
then (Gauge C,n) * (i + 1),j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def 1;
then A18: ((Gauge C,n) * (i + 1),j) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (((i + 1) - 2) / 1)) by EUCLID:56
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i + 1) - 2) / (2 |^ n))) by XCMPLX_1:86 ;
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A19: ((i - 2) / (2 |^ (n -' m))) + 1 < i1 by INT_1:def 4;
1 - 2 <= i - 2 by A2, XREAL_1:11;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:74;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:8;
then A20: i1 >= 1 + 0 by A19, INT_1:20;
N-bound C >= (S-bound C) + 0 by SPRECT_1:24;
then A21: (N-bound C) - (S-bound C) >= 0 by XREAL_1:21;
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 < i1 by INT_1:def 4;
then ((i - 2) / (2 |^ (n -' m))) + 2 < i1 + 1 by XREAL_1:21;
then (i - 2) / (2 |^ (n -' m)) < (i1 + 1) - 2 by XREAL_1:22;
then (i - 2) + 1 <= ((i1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:20, XREAL_1:79;
then ((i + 1) - 2) / (2 |^ (n -' m)) <= (i1 + 1) - 2 by A6, XREAL_1:81;
then (((i + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((i1 + 1) - 2) / (2 |^ m) by XREAL_1:74;
then ((i + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((i1 + 1) - 2) / (2 |^ m) by XCMPLX_1:79;
then ((i + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((i1 + 1) - 2) / (2 |^ m) by NEWTON:13;
then ((i + 1) - 2) / (2 |^ n) <= ((i1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:237;
then A22: ((E-bound C) - (W-bound C)) * (((i + 1) - 2) / (2 |^ n)) <= ((E-bound C) - (W-bound C)) * (((i1 + 1) - 2) / (2 |^ m)) by A14, XREAL_1:66;
i1 <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def 4;
then i1 - 2 <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:22;
then (i1 - 2) / (2 |^ m) <= ((i - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:74;
then (i1 - 2) / (2 |^ m) <= (i - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:79;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ ((n -' m) + m)) by NEWTON:13;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ n) by A1, XREAL_1:237;
then A23: ((E-bound C) - (W-bound C)) * ((i1 - 2) / (2 |^ m)) <= ((E-bound C) - (W-bound C)) * ((i - 2) / (2 |^ n)) by A14, XREAL_1:66;
j1 <= ((j - 2) / (2 |^ (n -' m))) + 2 by INT_1:def 4;
then j1 - 2 <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:22;
then (j1 - 2) / (2 |^ m) <= ((j - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:74;
then (j1 - 2) / (2 |^ m) <= (j - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:79;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ ((n -' m) + m)) by NEWTON:13;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ n) by A1, XREAL_1:237;
then A24: ((N-bound C) - (S-bound C)) * ((j1 - 2) / (2 |^ m)) <= ((N-bound C) - (S-bound C)) * ((j - 2) / (2 |^ n)) by A21, XREAL_1:66;
(((j - 2) / (2 |^ (n -' m))) + 2) - 1 = ((j - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A25: ((j - 2) / (2 |^ (n -' m))) + 1 < j1 by INT_1:def 4;
1 - 2 <= j - 2 by A4, XREAL_1:11;
then (- 1) / (2 |^ (n -' m)) <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:74;
then - 1 <= (j - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((j - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:8;
then A26: j1 >= 1 + 0 by A25, INT_1:20;
(((j - 2) / (2 |^ (n -' m))) + 2) - 1 < j1 by INT_1:def 4;
then ((j - 2) / (2 |^ (n -' m))) + 2 < j1 + 1 by XREAL_1:21;
then (j - 2) / (2 |^ (n -' m)) < (j1 + 1) - 2 by XREAL_1:22;
then (j - 2) + 1 <= ((j1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:20, XREAL_1:79;
then ((j + 1) - 2) / (2 |^ (n -' m)) <= (j1 + 1) - 2 by A6, XREAL_1:81;
then (((j + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((j1 + 1) - 2) / (2 |^ m) by XREAL_1:74;
then ((j + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((j1 + 1) - 2) / (2 |^ m) by XCMPLX_1:79;
then ((j + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((j1 + 1) - 2) / (2 |^ m) by NEWTON:13;
then ((j + 1) - 2) / (2 |^ n) <= ((j1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:237;
then A27: ((N-bound C) - (S-bound C)) * (((j + 1) - 2) / (2 |^ n)) <= ((N-bound C) - (S-bound C)) * (((j1 + 1) - 2) / (2 |^ m)) by A21, XREAL_1:66;
( len (Gauge C,m) = width (Gauge C,m) & len (Gauge C,n) = width (Gauge C,n) ) by JORDAN8:def 1;
then A28: j1 + 1 <= width (Gauge C,m) by A1, A4, A5, Th42;
then A29: j1 <= width (Gauge C,m) by NAT_1:13;
A30: i1 + 1 <= len (Gauge C,m) by A1, A2, A3, Th42;
then ( 1 <= j1 + 1 & i1 <= len (Gauge C,m) ) by NAT_1:11, NAT_1:13;
then [i1,(j1 + 1)] in Indices (Gauge C,m) by A20, A28, MATRIX_1:37;
then (Gauge C,m) * i1,(j1 + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 + 1) - 2)))]| by JORDAN8:def 1;
then ((Gauge C,m) * i1,(j1 + 1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (((j1 + 1) - 2) / 1)) by EUCLID:56
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:86 ;
then ((Gauge C,n) * i,(j + 1)) `2 <= ((Gauge C,m) * i1,(j1 + 1)) `2 by A15, A27, XREAL_1:8;
then A31: p `2 <= ((Gauge C,m) * i1,(j1 + 1)) `2 by A8, XXREAL_0:2;
i1 <= len (Gauge C,m) by A30, NAT_1:13;
then [i1,j1] in Indices (Gauge C,m) by A20, A26, A29, MATRIX_1:37;
then A32: (Gauge C,m) * i1,j1 = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def 1;
then ((Gauge C,m) * i1,j1) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 - 2) / 1)) by EUCLID:56
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i1 - 2) / (2 |^ m))) by XCMPLX_1:86 ;
then ((Gauge C,m) * i1,j1) `1 <= ((Gauge C,n) * i,j) `1 by A10, A23, XREAL_1:8;
then A33: ((Gauge C,m) * i1,j1) `1 <= p `1 by A11, XXREAL_0:2;
((Gauge C,m) * i1,j1) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 - 2) / 1)) by A32, EUCLID:56
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j1 - 2) / (2 |^ m))) by XCMPLX_1:86 ;
then ((Gauge C,m) * i1,j1) `2 <= ((Gauge C,n) * i,j) `2 by A12, A24, XREAL_1:8;
then A34: ((Gauge C,m) * i1,j1) `2 <= p `2 by A17, XXREAL_0:2;
( 1 <= i1 + 1 & j1 <= width (Gauge C,m) ) by A28, NAT_1:11, NAT_1:13;
then [(i1 + 1),j1] in Indices (Gauge C,m) by A26, A30, MATRIX_1:37;
then (Gauge C,m) * (i1 + 1),j1 = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def 1;
then ((Gauge C,m) * (i1 + 1),j1) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (((i1 + 1) - 2) / 1)) by EUCLID:56
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:86 ;
then ((Gauge C,n) * (i + 1),j) `1 <= ((Gauge C,m) * (i1 + 1),j1) `1 by A18, A22, XREAL_1:8;
then p `1 <= ((Gauge C,m) * (i1 + 1),j1) `1 by A13, XXREAL_0:2;
hence e in cell (Gauge C,m),i1,j1 by A20, A26, A30, A28, A33, A34, A31, JORDAN9:19; :: thesis: