The Mizar article:

Heine--Borel's Covering Theorem

by
Agata Darmochwal, and
Yatsuka Nakamura

Received November 21, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: HEINE
[ MML identifier index ]


environ

 vocabulary ARYTM, PRE_TOPC, METRIC_1, ABSVALUE, ARYTM_1, FUNCT_1, RCOMP_1,
      BOOLE, GROUP_1, SEQ_1, ORDINAL2, RELAT_1, POWER, LIMFUNC1, FINSET_1,
      COMPTS_1, SETFAM_1, TOPMETR, PCOMPS_1, ARYTM_3, TARSKI, SEQM_3, SEQ_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      ORDINAL2, REAL_1, NAT_1, RELAT_1, FUNCT_2, METRIC_1, FINSET_1, BINOP_1,
      STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, ABSVALUE, SEQ_1, SEQ_2,
      SEQM_3, LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR;
 constructors REAL_1, NAT_1, TOPS_2, COMPTS_1, ABSVALUE, SEQ_2, SEQM_3,
      LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR, PARTFUN1, SEQ_4, MEMBERED,
      XBOOLE_0;
 clusters PRE_TOPC, FINSET_1, XREAL_0, METRIC_1, RELSET_1, SEQ_1, SEQM_3,
      ARYTM_3, NEWTON, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, SEQ_2, LIMFUNC1, COMPTS_1;
 theorems ABSVALUE, AXIOMS, FINSET_1, FUNCT_1, FUNCT_2, TOPMETR, LIMFUNC1,
      METRIC_1, NAT_1, NEWTON, POWER, PCOMPS_1, RCOMP_1, REAL_1, REAL_2, SEQ_1,
      SEQ_2, SEQ_4, SEQM_3, SQUARE_1, TARSKI, ZFMISC_1, XREAL_0, SETFAM_1,
      ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes RECDEF_1, NAT_1, SEQ_1;

begin

reserve a,b,x,y,z for real number, i,k,n,m for Nat;
reserve p,q,w for Real;

theorem Th1: for A being SubSpace of RealSpace, p,q being Point of A
 st x = p & y = q holds dist(p,q) = abs( x - y )
  proof
   let A be SubSpace of RealSpace, p,q be Point of A;
    assume A1: x = p & y = q;
A2: x is Real & y is Real by XREAL_0:def 1;
    thus dist(p,q) = (the distance of A).(p,q) by METRIC_1:def 1
            .= (real_dist).(x, y) by A1,METRIC_1:def 14,TOPMETR:def 1
            .= abs( x - y ) by A2,METRIC_1:def 13;
  end;

theorem Th2: x <= y & y <= z implies [. x,y .] \/ [. y,z .] = [. x,z .]
  proof
   assume A1: x <= y & y <= z;
   A2: [. x,y .] \/ [. y,z .] = [. x,y .] \/ {q:y<=q & q<=z} by RCOMP_1:def 1
        .= {p: x <= p & p <= y} \/ {q: y <= q & q <= z} by RCOMP_1:def 1;
        now let o be set;
   A3: now assume A4: o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z};
         now per cases by A4,XBOOLE_0:def 2;
        suppose o in {p: x <= p & p <= y};
         then consider a be Real such that A5: o=a & x <= a & a <= y;
             x <= a & a <= z by A1,A5,AXIOMS:22;
         hence o in {w: x <= w & w <= z} by A5;
        suppose o in {p: y <= p & p <= z};
         then consider a be Real such that A6: o=a & y <= a & a <= z;
            x <= a & a <= z by A1,A6,AXIOMS:22;
         hence o in {w: x <= w & w <= z} by A6;
        end;
       hence o in {w: x <= w & w <= z};
      end;
        now assume o in {w: x <= w & w <= z};
       then consider r be Real such that A7: o=r & x <= r & r <= z;
         x <= r & r <= y & r <= z or x <= r & y <= r & r <= z by A7;
       then o in {p: x <= p & p <= y} or o in {q: y <= q & q <= z} by A7;
       hence o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z} by XBOOLE_0:def
2;
      end;
     hence o in {p: x <= p & p <= y} \/ {q: y <= q & q <= z} iff
      o in {w: x <= w & w <= z} by A3;
     end;
     then {p: x <= p & p <= y} \/ {q: y <= q & q <= z} = {w: x <= w & w <= z}
      by TARSKI:2;
     hence thesis by A2,RCOMP_1:def 1;
  end;

theorem Th3: x >= 0 & a + x <= b implies a <= b
 proof
  assume A1: x >= 0 & a + x <= b;
  then a + x - x <= b - x by REAL_1:49;
  then a <= b - x & b - x <= b by A1,REAL_2:173,XCMPLX_1:26;
  hence thesis by AXIOMS:22;
 end;

theorem Th4: x >= 0 & a - x >= b implies a >= b
 proof
  assume A1: x >= 0 & a - x >= b;
   then a - x + x >= b + x by AXIOMS:24;
   then a >= b + x & b + x >= b by A1,REAL_2:173,XCMPLX_1:27;
  hence thesis by AXIOMS:22;
 end;

theorem Th5: x > 0 implies x|^k > 0
 proof
  defpred P[Nat] means for x st x > 0 holds x|^$1 > 0;
  A1: P[0]
   proof
    let x; x|^0 = 1 by NEWTON:9;
    hence thesis;
    end;
  A2: for k holds P[k] implies P[k+1]
    proof
     let k such that A3: for x st x > 0 holds x|^k > 0;
     let x; assume x > 0;
     then x > 0 & x|^k > 0 & x|^(k+1) = x * x|^k by A3,NEWTON:11;
     hence thesis by REAL_2:122;
    end;
    for k holds P[k] from Ind(A1,A2);
  hence thesis;
 end;

reserve seq for Real_Sequence;

theorem Th6:
 seq is increasing & rng seq c= NAT implies n <= seq.n
 proof
  defpred P[Nat] means $1 <= seq.$1;
  assume that A1: seq is increasing and A2: rng seq c= NAT;
     0 in NAT;
   then 0 in dom seq by FUNCT_2:def 1;
   then seq.0 in rng seq by FUNCT_1:def 5;
   then seq.0 is natural by A2,ORDINAL2:def 21;
then A3: P[0] by NAT_1:18;
A4: for k st P[k] holds P[k+1]
    proof
     let k such that A5: k <= seq.k;
        k+1 in NAT;
      then k+1 in dom seq by FUNCT_2:def 1;
      then seq.(k+1) in rng seq by FUNCT_1:def 5;
      then reconsider k' = seq.(k+1) as Nat by A2;
        seq.k < seq.(k+1) by A1,SEQM_3:def 11;
      then k < k' by A5,AXIOMS:22;
      hence k+1 <= seq.(k+1) by NAT_1:38;
    end;
     for n holds P[n] from Ind(A3,A4);
   hence thesis;
 end;

definition let seq,k;
 func k to_power seq -> Real_Sequence means
  :Def1: for n holds it.n = k to_power (seq.n);
 existence
  proof
   deffunc F(Nat) = k to_power (seq.$1);
   thus ex s being Real_Sequence st for n holds
   s.n = F(n) from ExRealSeq;
  end;
 uniqueness
  proof
   let s1,s2 be Real_Sequence;
   assume that A1: for n holds s1.n = k to_power (seq.n) and
               A2: for n holds s2.n = k to_power (seq.n);
      now let n; thus s1.n = k to_power (seq.n) by A1 .= s2.n by A2; end;
    hence thesis by FUNCT_2:113;
  end;
end;

  defpred P[Nat] means 2|^$1 >= $1 + 1;
  Lm1: P[0] by NEWTON:9;
  Lm2: for n st P[n] holds P[n+1]
      proof
       let n; assume 2|^n >= n+1;
        then 2|^n - n >= 1 & 2 >= 0 by REAL_1:84;
        then A1: 2*(2|^n - n) >= 2*1 by AXIOMS:25;
           2|^(n+1) - (n + 1 + 1) = 2|^(n + 1) - (n + (1+1)) by XCMPLX_1:1
             .= 2*2|^n - (n + 2) by NEWTON:11
             .= 2*2|^n - (n + n - n + 2) by XCMPLX_1:26
             .= 2*2|^n - (2*n - n + 2) by XCMPLX_1:11
             .= 2*2|^n - (2*n - n) - 2 by XCMPLX_1:36
             .= 2*2|^n - 2*n + n - 2 by XCMPLX_1:37
             .= 2*(2|^n - n) + n - 2 by XCMPLX_1:40
             .= 2*(2|^n - n) + (n - 2) by XCMPLX_1:29;
         then 2|^(n+1) - (n + 1 + 1) >= 2 + (n - 2) by A1,AXIOMS:24;
         then 2|^(n+1) - (n + 1 + 1) >= n & n >= 0 by NAT_1:18,XCMPLX_1:27;
         then 2|^(n+1) >= 0 + (n + 1 + 1) by REAL_1:84;
        hence 2|^(n+1) >= n + 1 + 1;
      end;

theorem Th7:
  2|^n >= n + 1
   proof for n holds P[n] from Ind(Lm1,Lm2); hence thesis; end;

theorem Th8:
  2|^n > n
 proof
    2|^n >= n + 1 & n+1 > n by Th7,NAT_1:38;
  hence thesis by AXIOMS:22;
 end;

theorem
Th9: seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty
 proof
  assume A1: seq is divergent_to+infty;
  let r be Real;
   consider p being Nat such that A2: p > r by SEQ_4:10;
   consider n such that A3: for m st n <= m holds p < seq.m by A1,LIMFUNC1:def
4;
    take n; let m; assume m >= n;
     then p < seq.m & 2 > 1 & 2<>0 by A3;
     then 2 to_power p < 2 to_power (seq.m) & 2 to_power p = 2|^p & 2|^p > p
      by Th8,POWER:44,48;
     then p < 2 to_power (seq.m) by AXIOMS:22;
     then r < 2 to_power (seq.m) by A2,AXIOMS:22;
    hence r < (2 to_power seq).m by Def1;
 end;

theorem Th10:
 for T being TopSpace st the carrier of T is finite holds T is compact
  proof
   let T be TopSpace;
   assume A1: the carrier of T is finite;
   let F be Subset-Family of T such that
   A2: F is_a_cover_of T & F is open;
   reconsider F' = F as Subset-Family of T;
   take F';
   thus F' c= F & F' is_a_cover_of T by A2;
     bool(the carrier of T) is finite & F' c= bool(the carrier of T)
    by A1,FINSET_1:24;
   hence F' is finite by FINSET_1:13;
  end;

:: HEINE - BOREL THEOREM

theorem
   a <= b implies Closed-Interval-TSpace(a,b) is compact
  proof
   set M = Closed-Interval-MSpace(a,b);
   assume A1: a <= b;
   reconsider a, b as Real by XREAL_0:def 1;
   set r = b-a;
    now per cases by A1,SQUARE_1:12;
   suppose r = 0;
    then a = b by XCMPLX_1:15;
    then [. a,b .] = {a} & {a} is finite & the carrier of
     Closed-Interval-TSpace(a,b) = [. a,b .]
      by RCOMP_1:14,TOPMETR:25;
    hence Closed-Interval-TSpace(a,b) is compact by Th10;
   suppose A2: r > 0;
   assume A3: not Closed-Interval-TSpace(a,b) is compact;
      TopSpaceMetr M = Closed-Interval-TSpace(a,b) by TOPMETR:def 8;
    then not M is compact by A3,TOPMETR:def 6;
    then consider F being Subset-Family of M such that
   A4: F is_ball-family and
   A5: F is_a_cover_of M and
   A6: not ex G being Subset-Family of M st
       (G c= F & G is_a_cover_of M & G is finite) by TOPMETR:23;
     defpred P[Element of NAT, Element of REAL, Element of REAL] means
      ((not ex G being Subset-Family of M st G c= F &
        [. $2-(r/2|^($1+1)), $2 .] c= union G & G is finite) implies
       $3 = $2 - r/2|^($1+2)) &
      (not (not ex G being Subset-Family of M st G c= F &
        [. $2-r/2|^($1+1), $2 .] c= union G & G is finite) implies
      $3 = $2 + r/2|^($1+2));
   A7: for n,p ex w st P[n,p,w]
        proof
         let n,p;
           now per cases;
          suppose A8: not ex G being Subset-Family of M st G c= F &
           [. p-(r/2|^(n+1)), p .] c= union G & G is finite;
           take y = p - r/2|^(n+2);
          thus P[n,p,y] by A8;
          suppose A9: not not ex G being Subset-Family of M st G c= F &
           [. p-(r/2|^(n+1)), p .] c= union G & G is finite;
           take y = p + r/2|^(n+2);
          thus P[n,p,y] by A9;
         end;
        hence thesis;
        end;
     consider f being Function of NAT,REAL such that
   A10: f.0 = (a+b)/2 and
   A11: for n holds P[n,f.n,f.(n+1)] from RecExD(A7);
   A12: for n holds f.(n+1) = f.n + r/2|^(n+2) or f.(n+1) = f.n - r/2|^(n+2)
        proof
         let n; P[n,f.n,f.(n+1)] by A11;
         hence thesis;
        end;
       defpred Q[Nat] means a <= f.$1 - r/2|^($1+1) & f.$1 + r/2|^($1+1) <= b;
       A13: f.0 - r/2|^(0+1) = (a+b)/2 - r/2 by A10,NEWTON:10
           .= (a+b-(b-a))/2 by XCMPLX_1:121
           .= ((a+b)-b+a)/2 by XCMPLX_1:37
           .= (a+a)/2 by XCMPLX_1:26
           .= a by XCMPLX_1:65;
        A14: f.0 + r/2|^(0+1) = (a+b)/2 + r/2 by A10,NEWTON:10
           .= ((b-a)+(a+b))/2 by XCMPLX_1:63
           .= (b-a+a+b)/2 by XCMPLX_1:1
           .= (b+b)/2 by XCMPLX_1:27
           .= b by XCMPLX_1:65;
   then A15: Q[0] by A13;
   A16: for k st Q[k] holds Q[k+1]
        proof
         let k; assume Q[k];
          then A17: f.k - a >= r/2|^(k+1) & b - f.k >= r/2|^(k+1)
           by REAL_1:84,REAL_2:165;
          A18: r/(2*(2|^(k+1))) + r/(2*(2|^(k+1))) = r/2|^(k+1)
           by XCMPLX_1:119;
          A19: r/2|^(k+1) - r/2|^(k+(1+1))
               = r/2|^(k+1) - r/2|^((k+1)+1) by XCMPLX_1:1
              .= r/2|^(k+1) - r/(2*2|^(k+1)) by NEWTON:11
              .= r/(2*2|^(k+1)) by A18,XCMPLX_1:26
              .= r/2|^(k+1+1) by NEWTON:11
              .= r/2|^(k+(1+1)) by XCMPLX_1:1;
            now per cases by A12;
           suppose A20: f.(k+1) = f.k + r/2|^(k+2);
              2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
           then A21: r/2|^(k+1) >= 0 by REAL_2:125;
              f.(k+1) - a = f.k - a + r/2|^(k+2) by A20,XCMPLX_1:29;
            then f.(k+1) - a >= r/2|^(k+2) by A17,A21,REAL_2:173;
            then a <= f.(k+1) - r/2|^(k+(1+1)) by REAL_2:165;
           hence a <= f.(k+1) - r/2|^(k+1+1) by XCMPLX_1:1;
              b - f.(k+1) = b - f.k - r/2|^(k+2) by A20,XCMPLX_1:36;
            then b - f.(k+1) >= r/2|^(k+2) by A17,A19,REAL_1:49;
            then f.(k+1) + r/2|^(k+(1+1)) <= b by REAL_1:84;
           hence f.(k+1) + r/2|^(k+1+1) <= b by XCMPLX_1:1;
           suppose A22: f.(k+1) = f.k - r/2|^(k+2);
              2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
           then A23: r/2|^(k+1) >= 0 by REAL_2:125;
              f.(k+1) - a = f.k - a - r/2|^(k+2) by A22,XCMPLX_1:21;
            then f.(k+1) - a >= r/2|^(k+2) by A17,A19,REAL_1:49;
            then a <= f.(k+1) - r/2|^(k+(1+1)) by REAL_2:165;
           hence a <= f.(k+1) - r/2|^(k+1+1) by XCMPLX_1:1;
              b - f.(k+1) = b - f.k + r/2|^(k+2) by A22,XCMPLX_1:37;
            then b - f.(k+1) >= r/2|^(k+2) by A17,A23,REAL_2:173;
            then f.(k+1) + r/2|^(k+(1+1)) <= b by REAL_1:84;
           hence f.(k+1) + r/2|^(k+1+1) <= b by XCMPLX_1:1;
         end;
         hence thesis;
        end;
   A24: for k holds Q[k] from Ind(A15,A16);
   A25: rng f c= [. a,b .]
     proof
      let y be set; assume y in rng f;
      then consider x being set such that
     A26: x in dom f & y = f.x by FUNCT_1:def 5;
      reconsider n = x as Nat by A26,FUNCT_2:def 1;
        2|^(n+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
      then r/2|^(n+1) >= 0 & a <= f.n - r/2|^(n+1) & f.n + r/2|^(n+1) <= b
       by A24,REAL_2:125;
      then a <= f.n & f.n <= b by Th3,Th4;
      then y in { y1 where y1 is Real: a <= y1 & y1 <= b} by A26;
      hence y in [. a,b .] by RCOMP_1:def 1;
     end;
     defpred R[Nat] means not ex G being Subset-Family of M st
       (G c= F & [. f.$1 - r/2|^($1+1), f.$1 + r/2|^($1+1) .] c= union G &
        G is finite);
     A27: R[0]
      proof
       given G being Subset-Family of M such that
      A28: G c= F and
      A29: [. f.0 - r/2|^(0+1), f.0 + r/2|^(0+1) .] c= union G and
      A30: G is finite;
         the carrier of M c= union G by A1,A13,A14,A29,TOPMETR:14;
       then G is_a_cover_of M by TOPMETR:def 5;
       hence contradiction by A6,A28,A30;
      end;
     A31: for k st R[k] holds R[k+1]
      proof
       let k such that A32: R[k];
A33:       r/2|^(k+(1+1)) = r/2|^(k+1+1) by XCMPLX_1:1
                     .= r/((2|^(k+1))*2) by NEWTON:11
                     .= r/(2|^(k+1))/2 by XCMPLX_1:79;
       given G being Subset-Family of M such that
      A34: G c= F and
      A35: [. f.(k+1) - r/2|^(k+1+1), f.(k+1) + r/2|^(k+1+1) .] c= union G and
      A36: G is finite;
            now per cases;
           suppose A37: ex G being Subset-Family of M st G c= F &
            [. f.k - r/2|^(k+1), f.k .] c= union G & G is finite;
           then consider G1 being Subset-Family of M such that
            A38: G1 c= F and
            A39: [. f.k - r/2|^(k+1), f.k .] c= union G1 and
            A40: G1 is finite;
          A41: f.(k+1) = f.k + r/2|^(k+2) by A11,A37;
           then A42: f.(k+1) - r/2|^(k+1+1)
             = f.k + r/2|^(k+2) - r/2|^(k+(1+1)) by XCMPLX_1:1
            .= f.k by XCMPLX_1:26;
A43:           f.(k+1) + r/2|^(k+1+1)
             = f.k + r/2|^(k+2) + r/2|^(k+(1+1)) by A41,XCMPLX_1:1
            .= f.k + (r/2|^(k+2) + r/2|^(k+2)) by XCMPLX_1:1
            .= f.k + r/2|^(k+1) by A33,XCMPLX_1:66;
           reconsider G3 = G1 \/ G as Subset-Family of M;
             2|^(k+1) > 0 & r >= 0 by A1,Th5,SQUARE_1:12;
           then r/2|^(k+1) >= 0 by REAL_2:125;
           then f.k - r/2|^(k+1) <= f.k & f.k <=
 f.k + r/2|^(k+1) by REAL_2:173;
          then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] =
           [. f.k - r/2|^(k+1), f.k .] \/ [. f.k, f.k + r/2|^(k+1).] by Th2;
          then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G1 \/ union G
           by A35,A39,A42,A43,XBOOLE_1:13;
          then A44: [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G3
           by ZFMISC_1:96;
           A45: G3 is finite by A36,A40,FINSET_1:14;
             G3 c= F by A34,A38,XBOOLE_1:8;
          hence contradiction by A32,A44,A45;
          suppose A46: not (ex G being Subset-Family of M st G c= F &
           [. f.k - r/2|^(k+1), f.k .] c= union G & G is finite);
          then A47: f.(k+1) = f.k - r/2|^(k+2) by A11;
           then A48: f.(k+1) - r/2|^(k+1+1)
             = f.k - r/2|^(k+2) - r/2|^(k+(1+1)) by XCMPLX_1:1
            .= f.k - (r/2|^(k+2) + r/2|^(k+(1+1))) by XCMPLX_1:36
            .= f.k - r/2|^(k+1) by A33,XCMPLX_1:66;
            f.(k+1) + r/2|^(k+1+1)
             = f.k - r/2|^(k+2) + r/2|^(k+(1+1)) by A47,XCMPLX_1:1
            .= f.k by XCMPLX_1:27;
          hence contradiction by A34,A35,A36,A46,A48;
          end;
       hence thesis;
      end;
   A49: for k holds R[k] from Ind(A27,A31);
   A50: [. a,b .] is compact by RCOMP_1:24;
    reconsider f as Real_Sequence;
    consider s being Real_Sequence such that
   A51: s is_subsequence_of f and
   A52: s is convergent and
   A53: lim s in [. a,b .] by A25,A50,RCOMP_1:def 3;
     reconsider ls = lim s as Point of M by A1,A53,TOPMETR:14;
       the carrier of M c= union F & the carrier of M = [. a,b .]
      by A1,A5,TOPMETR:14,def 5;
     then consider Z being set such that A54: lim s in Z & Z in F by A53,TARSKI
:def 4;
     consider p being Point of M, r0 being Real such that
   A55: Z = Ball(p,r0) by A4,A54,TOPMETR:def 4;
     consider r1 being Real such that
   A56: r1 > 0 & Ball(ls,r1) c= Ball(p,r0) by A54,A55,PCOMPS_1:30;
     consider Nseq being increasing Seq_of_Nat such that
   A57: s = f*Nseq by A51,SEQM_3:def 10;
     A58: r1/2 > 0 by A56,REAL_2:127;
     then consider n being Nat such that
   A59: for m being Nat st m >= n holds abs( s.m - lim s ) < r1/2
      by A52,SEQ_2:def 7;
   A60: for m being Nat for q being Point of M st s.m = q & m >= n holds
         dist(ls, q) < r1/2
        proof
         let m be Nat, q be Point of M; assume A61: s.m = q & m >= n;
         then abs( s.m - lim s ) < r1/2 by A59;
         then A62: abs( -(s.m - lim s) ) < r1/2 by ABSVALUE:17;
           dist(ls, q)
             = (the distance of M).(lim s, s.m) by A61,METRIC_1:def 1
            .= (the distance of RealSpace).(ls, q) by A61,TOPMETR:def 1
            .= abs( lim s - s.m ) by A61,METRIC_1:def 13,def 14;
         hence thesis by A62,XCMPLX_1:143;
        end;
    A63: for m being Nat st m >= n holds (f*Nseq).m in Ball(ls, r1/2)
        proof
          let m be Nat such that A64: m >= n;
A65:           dom f = NAT by FUNCT_2:def 1;
             s.m = f.(Nseq.m) by A57,SEQM_3:31;
           then s.m in rng f by A65,FUNCT_1:def 5;
           then reconsider q = s.m as Point of M by A1,A25,TOPMETR:14;
             dist(ls, q) < r1/2 by A60,A64;
           hence (f*Nseq).m in Ball(ls, r1/2) by A57,METRIC_1:12;
        end;
       not Nseq is bounded_above
      proof
       let r be real number;
       consider n being Nat such that A66: n > r by SEQ_4:10;
          rng Nseq c= NAT by SEQM_3:def 8;
        then n <= Nseq.n by Th6;
        then r <= Nseq.n by A66,AXIOMS:22;
        hence thesis;
      end;
     then Nseq is divergent_to+infty by LIMFUNC1:58;
     then 2 to_power Nseq is divergent_to+infty by Th9;
    then A67: (2 to_power Nseq)" is convergent & lim (2 to_power Nseq)" = 0
       by LIMFUNC1:61;
      then A68: lim (r(#)((2 to_power Nseq)")) = r*0 by SEQ_2:22 .= 0;
        r(#)((2 to_power Nseq)") is convergent by A67,SEQ_2:21;
      then consider i such that
    A69: for m st i <= m holds abs( (r(#)((2 to_power Nseq)")).m - 0 ) < r1/2
        by A58,A68,SEQ_2:def 7;
       set l = i + 1 + n;
          l = n + 1 + i by XCMPLX_1:1;
       then A70: l >= n & l >= i by NAT_1:29;
       [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .] c=
          Ball(ls,r1)
       proof
        let z be set;
        assume z in [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .];
         then z in
          {m where m is Real:
          s.l - r*(2|^(Nseq.l+1))" <= m & m <= s.l + r*(2|^(Nseq.l+1))" }
          by RCOMP_1:def 1;
         then consider x be Real such that
         A71: x = z & s.l - r*(2|^(Nseq.l+1))" <= x &
          x <= s.l + r*(2|^(Nseq.l+1))";
           f.(Nseq.l) - r/(2|^(Nseq.l+1)) >= a &
          f.(Nseq.l) + r/(2|^(Nseq.l+1)) <= b & 2|^(Nseq.l+1) <> 0 by A24,Th5;
         then f.(Nseq.l) - r*(2|^(Nseq.l+1))" >= a &
          f.(Nseq.l) + r*(2|^(Nseq.l+1))" <= b by XCMPLX_0:def 9;
         then s.l - r*(2|^(Nseq.l+1))" >= a & s.l + r*(2|^(Nseq.l+1))" <= b
          by A57,SEQM_3:31;
         then x <= b & x >= a by A71,AXIOMS:22;
         then x in {m where m is Real : a <= m & m <= b};
         then the carrier of M = [. a,b .] & x in [. a,b .]
          by A1,RCOMP_1:def 1,TOPMETR:14;
         then reconsider x' = x as Point of M;
           s.l <= r*(2|^(Nseq.l+1))" + x & x - s.l <= r*(2|^(Nseq.l+1))"
           by A71,REAL_1:86;
         then s.l - x <= r*(2|^(Nseq.l+1))" & -(x - s.l) >= -r*(2|^(Nseq.l+1))
"
          by REAL_1:50,86;
         then s.l - x <= r*(2|^(Nseq.l+1))" & s.l - x >= - r*(2|^(Nseq.l+1))"
          by XCMPLX_1:143;
         then A72: abs( s.l - x ) <= r*(2|^(Nseq.l+1))" by ABSVALUE:12;
           abs( lim s - x ) = abs( (lim s - s.l) + (s.l - x) ) by XCMPLX_1:39;
         then A73: abs( lim s - x ) <= abs( lim s - s.l ) + abs( s.l - x )
           by ABSVALUE:13;
       A74: s.l in Ball(ls, r1/2) by A57,A63,A70;
         then reconsider sl = s.l as Point of M;
           dist(ls,sl) < r1/2 by A74,METRIC_1:12;
         then A75: abs( lim s - s.l ) < r1/2 by Th1;
          abs( (r(#)(2 to_power Nseq)").l - 0 ) < r1/2 by A69,A70;
        then abs( r*((2 to_power Nseq)").l ) < r1/2 by SEQ_1:13;
        then abs( r*((2 to_power Nseq).l)" ) < r1/2 by SEQ_1:def 8;
        then abs( r*(2 to_power (Nseq.l))" ) < r1/2 by Def1;
        then A76: abs( r*(2|^(Nseq.l))" ) < r1/2 by POWER:48;
          r >= 0 & 2|^(Nseq.l+1) > 0 by A1,Th5,SQUARE_1:12;
        then r >= 0 & (2|^(Nseq.l+1))" > 0 by REAL_1:72;
        then r*(2|^(Nseq.l+1))" >= 0 by REAL_2:121;
        then A77: abs( r*(2|^(Nseq.l+1))" ) = r*(2|^(Nseq.l+1))" by ABSVALUE:
def 1;
          2|^(Nseq.l+1) = 2*2|^Nseq.l & 2 > 1 & 2|^Nseq.l > 0
          by Th5,NEWTON:11;
        then 2|^(Nseq.l+1) > 2|^Nseq.l & 2|^Nseq.l > 0 by REAL_2:144;
        then 1/(2|^(Nseq.l+1)) < 1/(2|^Nseq.l) & 2|^Nseq.l <> 0 & 2 > 0
         by REAL_2:151;
        then 1/(2|^(Nseq.l+1)) < (2|^Nseq.l)" & r > 0 & 2|^(Nseq.l+1) <> 0
         by A2,Th5,XCMPLX_1:217;
        then (2|^(Nseq.l+1))" < (2|^Nseq.l)" & r > 0 by XCMPLX_1:217;
        then r*(2|^(Nseq.l+1))" < r*(2|^Nseq.l)" by REAL_1:70;
        then abs( r*(2|^(Nseq.l+1))" ) < abs( r*(2|^Nseq.l)" )
          by A77,ABSVALUE:12;
        then A78: abs( r*(2|^(Nseq.l+1))" ) < r1/2 by A76,AXIOMS:22;
          r >= 0 & 2|^(Nseq.l+1) > 0 by A1,Th5,SQUARE_1:12;
        then r >= 0 & (2|^(Nseq.l+1))" > 0 by REAL_1:72;
        then r*(2|^(Nseq.l+1))" >= 0 by REAL_2:121;
        then r*(2|^(Nseq.l+1))" < r1/2 by A78,ABSVALUE:def 1;
        then abs( s.l - x ) < r1/2 by A72,AXIOMS:22;
        then abs( lim s - s.l ) + abs( s.l - x ) < r1/2 + r1/2
        by A75,REAL_1:67;
        then abs( lim s - x ) < r1/2 + r1/2 by A73,AXIOMS:22;
        then abs( lim s - x ) < r1 by XCMPLX_1:66;
        then dist(ls,x') < r1 by Th1;
        hence z in Ball(ls,r1) by A71,METRIC_1:12;
       end;
     then [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .]
       c= Ball(p,r0) & 2|^(Nseq.l+1) <> 0 by A56,Th5,XBOOLE_1:1;
     then [. s.l - r/2|^(Nseq.l+1), s.l + r*(2|^(Nseq.l+1))" .]
       c= Ball(p,r0) by XCMPLX_0:def 9;
     then [. s.l - r/2|^(Nseq.l+1), s.l + r/2|^(Nseq.l+1) .]
       c= Ball(p,r0) by XCMPLX_0:def 9;
     then [. f.(Nseq.l) - r/(2|^(Nseq.l+1)), s.l + r/2|^(Nseq.l+1) .]
       c= Ball(p,r0) by A57,SEQM_3:31;
     then A79:
      [. f.(Nseq.l) - r/(2|^(Nseq.l+1)), f.(Nseq.l) + r/2|^(Nseq.l+1) .]
       c= Ball(p,r0) by A57,SEQM_3:31;
    set G = {Ball(p,r0)};
      G c= bool the carrier of M
     proof
      let a be set; assume a in G;
      then a = Ball(p,r0) by TARSKI:def 1;
      hence thesis;
     end;
    then G is Subset-Family of M by SETFAM_1:def 7;
    then reconsider G as Subset-Family of M;
     A80: G c= F by A54,A55,ZFMISC_1:37;
        [. f.(Nseq.l) - r/2|^(Nseq.l+1), f.(Nseq.l) + r/2|^(Nseq.l+1) .]
      c= union G by A79,ZFMISC_1:31;
    hence contradiction by A49,A80;
   end;
  hence thesis;
  end;

Back to top