let m, j, i, n be 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 Nat by A2, A4, Th35;
set Gm = Gauge (C,m);
set Gn = Gauge (C,n);
A6: 2 |^ (n -' m) > n -' m by NEWTON:86;
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 object ; :: 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:17;
( 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_0:30;
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:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i - 2) / (2 |^ n))) by XCMPLX_1:85 ;
A11: ((Gauge (C,n)) * (i,j)) `1 <= p `1 by A2, A3, A4, A5, A7, JORDAN9:17;
A12: ((Gauge (C,n)) * (i,j)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j - 2) / 1)) by A9, EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j - 2) / (2 |^ n))) by XCMPLX_1:85 ;
A13: p `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A2, A3, A4, A5, A7, JORDAN9:17;
E-bound C >= (W-bound C) + 0 by SPRECT_1:21;
then A14: (E-bound C) - (W-bound C) >= 0 by XREAL_1:19;
( 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_0:30;
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:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ;
( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2;
then A16: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
A17: ((Gauge (C,n)) * (i,j)) `2 <= p `2 by A2, A3, A4, A5, A7, JORDAN9:17;
( 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_0:30;
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:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ;
(((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 6;
1 - 2 <= i - 2 by A2, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then A20: i1 >= 1 + 0 by A19, INT_1:7;
N-bound C >= (S-bound C) + 0 by SPRECT_1:22;
then A21: (N-bound C) - (S-bound C) >= 0 by XREAL_1:19;
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 < i1 by INT_1:def 6;
then ((i - 2) / (2 |^ (n -' m))) + 2 < i1 + 1 by XREAL_1:19;
then (i - 2) / (2 |^ (n -' m)) < (i1 + 1) - 2 by XREAL_1:20;
then (i - 2) + 1 <= ((i1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77;
then ((i + 1) - 2) / (2 |^ (n -' m)) <= (i1 + 1) - 2 by A6, XREAL_1:79;
then (((i + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((i1 + 1) - 2) / (2 |^ m) by XREAL_1:72;
then ((i + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((i1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78;
then ((i + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((i1 + 1) - 2) / (2 |^ m) by NEWTON:8;
then ((i + 1) - 2) / (2 |^ n) <= ((i1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235;
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:64;
i1 <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def 6;
then i1 - 2 <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:20;
then (i1 - 2) / (2 |^ m) <= ((i - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72;
then (i1 - 2) / (2 |^ m) <= (i - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ n) by A1, XREAL_1:235;
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:64;
j1 <= ((j - 2) / (2 |^ (n -' m))) + 2 by INT_1:def 6;
then j1 - 2 <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:20;
then (j1 - 2) / (2 |^ m) <= ((j - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72;
then (j1 - 2) / (2 |^ m) <= (j - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ n) by A1, XREAL_1:235;
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:64;
(((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 6;
1 - 2 <= j - 2 by A4, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (j - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((j - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then A26: j1 >= 1 + 0 by A25, INT_1:7;
(((j - 2) / (2 |^ (n -' m))) + 2) - 1 < j1 by INT_1:def 6;
then ((j - 2) / (2 |^ (n -' m))) + 2 < j1 + 1 by XREAL_1:19;
then (j - 2) / (2 |^ (n -' m)) < (j1 + 1) - 2 by XREAL_1:20;
then (j - 2) + 1 <= ((j1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77;
then ((j + 1) - 2) / (2 |^ (n -' m)) <= (j1 + 1) - 2 by A6, XREAL_1:79;
then (((j + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((j1 + 1) - 2) / (2 |^ m) by XREAL_1:72;
then ((j + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((j1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78;
then ((j + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((j1 + 1) - 2) / (2 |^ m) by NEWTON:8;
then ((j + 1) - 2) / (2 |^ n) <= ((j1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235;
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:64;
( 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, Th36;
then A29: j1 <= width (Gauge (C,m)) by NAT_1:13;
A30: i1 + 1 <= len (Gauge (C,m)) by A1, A2, A3, Th36;
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_0:30;
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:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,n)) * (i,(j + 1))) `2 <= ((Gauge (C,m)) * (i1,(j1 + 1))) `2 by A15, A27, XREAL_1:6;
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_0:30;
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:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i1 - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,m)) * (i1,j1)) `1 <= ((Gauge (C,n)) * (i,j)) `1 by A10, A23, XREAL_1:6;
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:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j1 - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,m)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i,j)) `2 by A12, A24, XREAL_1:6;
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_0:30;
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:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,n)) * ((i + 1),j)) `1 <= ((Gauge (C,m)) * ((i1 + 1),j1)) `1 by A18, A22, XREAL_1:6;
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:17; :: thesis: