:: Strong arithmetic of real numbers
::  by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies BOOLE, ARYTM, ARYTM_2, ARYTM_3, ORDINAL2, ARYTM_1, COMPLEX1,
      RELAT_1, FUNCOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
      NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, XXREAL_0;
 constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
 registrations ORDINAL1, ARYTM_2, NUMBERS, XREAL_0, XBOOLE_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, XXREAL_0, ARYTM_3;
 theorems XBOOLE_0, ARYTM_0, ZFMISC_1, TARSKI, ARYTM_1, ARYTM_2, SUBSET_1,
      ORDINAL1, XBOOLE_1, XREAL_0, XCMPLX_0, NUMBERS, XXREAL_0;

begin

reserve r,s for real number;

Lm1: (r in REAL+ & s in REAL+ &
ex x',y' being Element of REAL+ st r = x' & s = y' & x' <=' y') or
(r in [:{0},REAL+:] & s in [:{0},REAL+:] &
ex x',y' being Element of REAL+ st r = [0,x'] & s = [0,y'] & y' <=' x') or
s in REAL+ & r in [:{0},REAL+:] implies r <= s
proof
  assume
A1: (r in REAL+ & s in REAL+ &
  ex x',y' being Element of REAL+ st r = x' & s = y' & x' <=' y') or
  (r in [:{0},REAL+:] & s in [:{0},REAL+:] &
  ex x',y' being Element of REAL+ st r = [0,x'] & s = [0,y'] & y' <=' x') or
  ( s in REAL+ & r in [:{0},REAL+:]);
  per cases;
  case r in REAL+ & s in REAL+;
    hence ex x',y' being Element of REAL+ st r = x' & s = y' & x' <=' y' by A1,
    ARYTM_0:5,XBOOLE_0:3;
  end;
  case r in [:{0},REAL+:] & s in [:{0},REAL+:];

hence ex x',y' being Element of REAL+ st r = [0,x'] & s = [0,y'] & y' <=' x'
    by A1,ARYTM_0:5,XBOOLE_0:3;
  end;
  case not(r in REAL+ & s in REAL+) &
    not (r in [:{0},REAL+:] & s in [:{0},REAL+:]);
    hence thesis by A1;
  end;
end;

reserve x,y,z for real number,
  k for natural number,
  i for Element of NAT;

canceled 18;

theorem
  ex y st x + y = 0
proof
  take y = -x;
  thus x + y = 0;
end;

theorem
  x <> 0 implies ex y st x * y = 1
proof
  assume
A1: x <> 0;
  take y = x";
  thus x * y = 1 by A1,XCMPLX_0:def 7;
end;

Lm2: for x being real number, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof
  let x be real number, x1,x2 being Element of REAL;
  assume
A1: x = [*x1,x2*];
A2: x in REAL by XREAL_0:def 1;
  thus now
    assume x2 <> 0;
    then x = (0,1) --> (x1,x2) by A1,ARYTM_0:def 7;
    hence contradiction by A2,ARYTM_0:10;
  end;
  hence x = x1 by A1,ARYTM_0:def 7;
end;

Lm3: for x',y' being Element of REAL, x,y st x' = x & y' = y
holds +(x',y') = x + y
proof
  let x',y' be Element of REAL, x,y such that
A1: x' = x & y' = y;
  consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] and
A3: y = [*y1,y2*] and
A4: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A5: x = x1 & y = y1 by A2,A3,Lm2;
  x2 = 0 & y2 = 0 by A2,A3,Lm2;
  then +(x2,y2) = 0 by ARYTM_0:13;
  hence +(x',y') = x + y by A1,A4,A5,ARYTM_0:def 7;
end;

Lm4: {} in {{}} by TARSKI:def 1;
reconsider o = 0 as Element of REAL+ by ARYTM_2:21;

reserve r,r1,r2 for Element of REAL+;

canceled 5;

theorem
  for X,Y being Subset of REAL st for x,y st x in X & y in Y holds x <= y
  ex z st for x,y st x in X & y in Y holds x <= z & z <= y
proof
  let X,Y be Subset of REAL;
  assume
A1: for x,y st x in X & y in Y holds x <= y;
  per cases;
  suppose
A2: X = 0 or Y = 0;
    take 1;
    thus thesis by A2;
  end;
  suppose that
A3: X <> 0 and
A4: Y <> 0;
    consider x1 being Element of REAL such that
A5: x1 in X by A3,SUBSET_1:10;
    consider x2 being Element of REAL such that
A6: x2 in Y by A4,SUBSET_1:10;
A7: X c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_1:1;
A8: Y c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_1:1;
    thus thesis
    proof
      per cases;
      suppose that
A9:     X misses REAL+ and
A10:    Y misses [:{0},REAL+:];
A11:    Y c= REAL+ by A8,A10,XBOOLE_1:73;
        take z = 0;
        let x,y such that
A12:    x in X and
A13:    y in Y;
        not z in [:{0},REAL+:] & not x in REAL+
        by A9,A12,ARYTM_0:5,ARYTM_2:21,XBOOLE_0:3;
        hence x <= z by XXREAL_0:def 5;
        reconsider y' = y as Element of REAL+ by A11,A13;
        o <=' y' by ARYTM_1:6;
        hence z <= y by Lm1;
      end;
      suppose Y meets [:{0},REAL+:];
        then consider e being set such that
A14:    e in Y and
A15:    e in [:{0},REAL+:] by XBOOLE_0:3;
        consider u,y1 being set such that
A16:    u in {0} and
A17:    y1 in REAL+ and
A18:    e = [u,y1] by A15,ZFMISC_1:103;
        reconsider y1 as Element of REAL+ by A17;
        e in REAL by A14;
        then
A19:    [0,y1] in REAL by A16,A18,TARSKI:def 1;
        then reconsider y0 = [0,y1] as real number by XREAL_0:def 1;
        {r: [0,r] in Y} c= REAL+
        proof
          let u be set;
          assume u in {r: [0,r] in Y};
          then ex r st u = r & [0,r] in Y;
          hence thesis;
        end;
        then reconsider Y' = {r : [0,r] in Y} as Subset of REAL+;
A20:    y0 in [:{0},REAL+:] by Lm4,ZFMISC_1:106;
A21:    y0 in Y by A14,A16,A18,TARSKI:def 1;
        then
A22:    y1 in Y';
A23:    X c= [:{0},REAL+:]
        proof
          let u be set;
          assume
A24:      u in X;
          then reconsider x = u as real number by XREAL_0:def 1;
          now
            assume
A25:        x in REAL+;
A26:        x <= y0 by A1,A21,A24;
            not y0 in REAL+ & not x in
            [:{0},REAL+:] by A20,A25,ARYTM_0:5,XBOOLE_0:3;
            hence contradiction by A26,XXREAL_0:def 5;
          end;
          hence u in [:{0},REAL+:] by A7,A24,XBOOLE_0:def 2;
        end;
        then consider e,x3 being set such that
A27:    e in {0} and
A28:    x3 in REAL+ and
A29:    x1 = [e,x3] by A5,ZFMISC_1:103;
        reconsider x3 as Element of REAL+ by A28;
A30:    x1 = [0,x3] by A27,A29,TARSKI:def 1;
        {r: [0,r] in X} c= REAL+
        proof
          let u be set;
          assume u in {r: [0,r] in X};
          then ex r st u = r & [0,r] in X;
          hence thesis;
        end;
        then reconsider X' = {r: [0,r] in X} as Subset of REAL+;
A31:    x3 in X' by A5,A30;
        for y',x' being Element of REAL+ st y' in Y' & x' in X' holds y' <='
        x'
        proof
          let y',x' be Element of REAL+;
          assume y' in Y';
          then consider r1 such that
A32:      y' = r1 and
A33:      [0,r1] in Y;
          assume x' in X';
          then consider r2 such that
A34:      x' = r2 and
A35:      [0,r2] in X;
          reconsider x = [0,x'], y = [0,y'] as real number
          by A32,A33,A34,A35,XREAL_0:def 1;
A36:      x in [:{0},REAL+:] & y in [:{0},REAL+:] by Lm4,ZFMISC_1:106;
          x <= y by A1,A32,A33,A34,A35;
          then consider x'',y'' being Element of REAL+ such that
A37:      x = [0,x''] and
A38:      y = [0,y''] and
A39:      y'' <=' x'' by A36,XXREAL_0:def 5;
          x' = x'' & y' = y'' by A37,A38,ZFMISC_1:33;
          hence y' <=' x' by A39;
        end;
        then consider z' being Element of REAL+ such that
A40:    for y',x' being Element of REAL+ st y' in Y' & x' in X'
        holds y' <=' z' & z' <=' x' by A22,A31,ARYTM_2:9;
A41:    y1 <> 0 by A19,ARYTM_0:3;
        y1 <=' z' by A22,A31,A40;
        then [0,z'] in REAL by A41,ARYTM_0:2,ARYTM_1:5;
        then reconsider z = [0,z'] as real number by XREAL_0:def 1;
        take z;
A42:    z in [:{0},REAL+:] by Lm4,ZFMISC_1:106;
        let x,y such that
A43:    x in X and
A44:    y in Y;
        consider e,x' being set such that
A45:    e in {0} and
A46:    x' in REAL+ and
A47:    x = [e,x'] by A23,A43,ZFMISC_1:103;
        reconsider x' as Element of REAL+ by A46;
A48:    x = [0,x'] by A45,A47,TARSKI:def 1;
        then
A49:    x' in X' by A43;
        now
          per cases by A8,A44,XBOOLE_0:def 2;
          suppose
A50:        y in REAL+;
            y1 <=' z' & z' <=' x' by A22,A40,A49;
            hence x <= z by A23,A42,A43,A48,Lm1;

not z in REAL+ & not y in [:{0},REAL+:] by A42,A50,ARYTM_0:5,XBOOLE_0:3;
            hence z <= y by XXREAL_0:def 5;
          end;
          suppose
A51:        y in [:{0},REAL+:];
            then consider e,y' being set such that
A52:        e in {0} and
A53:        y' in REAL+ and
A54:        y = [e,y'] by ZFMISC_1:103;
            reconsider y' as Element of REAL+ by A53;
A55:        y = [0,y'] by A52,A54,TARSKI:def 1;
            then y' in Y' by A44;
            then y' <=' z' & z' <=' x' by A40,A49;
            hence x <= z & z <= y by A23,A42,A43,A48,A51,A55,Lm1;
          end;
        end;
        hence thesis;
      end;
      suppose X meets REAL+;
        then consider x1 being set such that
A56:    x1 in X and
A57:    x1 in REAL+ by XBOOLE_0:3;
        reconsider x1 as Element of REAL+ by A57;
        x1 in REAL+;
        then reconsider x0 = x1 as real number by ARYTM_0:1,XREAL_0:def 1;
        reconsider X' = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A58:    x0 in X' by A56,XBOOLE_0:def 3;
A59:    Y c= REAL+
        proof
          let u be set;
          assume
A60:      u in Y;
          then reconsider y = u as real number by XREAL_0:def 1;
          now
            assume
A61:        y in [:{0},REAL+:];
A62:        x0 <= y by A1,A56,A60;
            not y in REAL+ & not x0 in [:{0},REAL+:] by A61,ARYTM_0:5
            ,XBOOLE_0:3;
            hence contradiction by A62,XXREAL_0:def 5;
          end;
          hence u in REAL+ by A8,A60,XBOOLE_0:def 2;
        end;
        then reconsider Y' = Y as Subset of REAL+;
        for x',y' being Element of REAL+ st x' in X' & y' in Y' holds x' <='
        y'
        proof
          let x',y' be Element of REAL+;
          assume
A63:      x' in X' & y' in Y';
          x' in REAL+ & y' in REAL+;

then reconsider x = x', y = y' as real number by ARYTM_0:1,XREAL_0:def 1;
          X' c= X by XBOOLE_1:17;
          then x <= y by A1,A63;
          then ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'
          by XXREAL_0:def 5;
          hence x' <=' y';
        end;
        then consider z' being Element of REAL+ such that
A64:    for x',y' being Element of REAL+ st x' in X' & y' in Y'
        holds x' <=' z' & z' <=' y' by A6,A58,ARYTM_2:9;
        z' in REAL+;
        then reconsider z = z' as real number by ARYTM_0:1,XREAL_0:def 1;
        take z;
        let x,y such that
A65:    x in X and
A66:    y in Y;
        reconsider y' = y as Element of REAL+ by A59,A66;
        now
          per cases by A7,A65,XBOOLE_0:def 2;
          suppose x in REAL+;
            then reconsider x' = x as Element of REAL+;
            x' in X' & y' in Y' by A65,A66,XBOOLE_0:def 3;
            then x' <=' z' & z' <=' y' by A64;
            hence x <= z & z <= y by Lm1;
          end;
          suppose x in [:{0},REAL+:];

then not x in REAL+ & not z in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
            hence x <= z by XXREAL_0:def 5;
            x1 <=' z' & z' <=' y' by A58,A64,A66;
            hence z <= y by Lm1;
          end;
        end;
        hence thesis;
      end;
    end;
  end;
end;

canceled;

theorem
  x in NAT & y in NAT implies x + y in NAT
proof
  reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;
A1: +(x1,y1) = x + y by Lm3;
  assume
A2: x in NAT & y in NAT;
  then ex x',y' being Element of REAL+ st
  x1 = x' & y1 = y' & +(x1,y1) = x' + y' by ARYTM_0:def 2,ARYTM_2:2;
  hence x + y in NAT by A1,A2,ARYTM_2:17;
end;

theorem
  for A being Subset of REAL st 0 in A & for x st x in A holds x + 1 in A
  holds NAT c= A
proof
  let A be Subset of REAL such that
A1: 0 in A and
A2: for x st x in A holds x + 1 in A;
  reconsider B = A /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A3: 0 in B by A1,ARYTM_2:21,XBOOLE_0:def 3;
A4: B c= A by XBOOLE_1:17;
  for x',y' being Element of REAL+ st x' in B & y' = 1 holds x' + y' in B
  proof
    let x',y' be Element of REAL+ such that
A5: x' in B and
A6: y' = 1;
    x' in REAL+;
    then reconsider x = x' as Element of REAL by ARYTM_0:1;
    reconsider xx = x as real number by XREAL_0:def 1;
    consider x'',y'' being Element of REAL+ such that
A7: x = x'' and
A8: 1 = y'' and
A9: +(x,1) = x'' + y'' by ARYTM_0:def 2,ARYTM_2:21;
    xx+1 in A by A2,A4,A5;
    then +(x,1) in A by Lm3;
    hence x' + y' in B by A6,A7,A8,A9,XBOOLE_0:def 3;
  end;
  then NAT c= B by A3,ARYTM_2:18;
  hence NAT c= A by A4,XBOOLE_1:1;
end;

theorem
  k = { i: i < k }
proof
  thus k c= { i: i < k }
  proof
    let e be set;
    reconsider k' = k as Element of NAT by ORDINAL1:def 13;
A1: k' c= NAT by ORDINAL1:def 2;
    assume
A2: e in k;
    then reconsider j = e as Element of NAT by A1;
    k' in NAT;
    then reconsider x' = k' as Element of REAL+ by ARYTM_2:2;
    e in NAT by A1,A2;
    then reconsider y' = e as Element of REAL+ by ARYTM_2:2;
    y' in x' by A2;
    then
A3: y' in NAT & y' <> x' & y' <=' x' by ARYTM_2:19;
    then j <= k by Lm1;
    then j < k by A3,XXREAL_0:1;
    hence e in { i: i < k };
  end;
  let e be set;
  assume e in { i: i < k };
  then consider i be Element of NAT such that
A4: e = i and
A5: not k <= i;
A6: k in NAT & i in NAT by ORDINAL1:def 13;
  then reconsider x' = e, y' = k as Element of REAL+ by A4,ARYTM_2:2;
  not y' <=' x' by A4,A5,Lm1;
  hence e in k by A4,A5,A6,ARYTM_2:19;
end;