:: Strong arithmetic of real numbers
::  by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XREAL_0, ORDINAL1, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1,
      XXREAL_0, NUMBERS, ARYTM_0, FUNCOP_1, XBOOLE_0, TARSKI, NAT_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;
 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, XTUPLE_0;

begin

reserve r,s for real number;

Lm1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9 & s
= y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9 being
Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ & r in
[:{0},REAL+:] implies r <= s
proof
  assume
A1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9
  & s = y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9
being Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ &
  r in [:{0},REAL+:];
  per cases;
  case
    r in REAL+ & s in REAL+;
    hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
  end;
  case
    r in [:{0},REAL+:] & s in [:{0},REAL+:];
    hence thesis 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 Nat,
  i for Element of NAT;

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 5;
    hence contradiction by A2,ARYTM_0:8;
  end;
  hence thesis by A1,ARYTM_0:def 5;
end;

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

Lm4: {} in {{}} by TARSKI:def 1;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

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

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:4;
A6: X c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_1:1;
A7: Y c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_1:1;
A8: ex x2 being Element of REAL st x2 in Y by A4,SUBSET_1:4;
    thus thesis
    proof
      per cases;
      suppose that
A9:     X misses REAL+ and
A10:    Y misses [:{0},REAL+:];
        take z = 0;
        let x,y such that
A11:    x in X and
A12:    y in Y;
        ( not z in [:{0},REAL+:])& not x in REAL+ by A9,A11,ARYTM_0:5
,ARYTM_2:20,XBOOLE_0:3;
        hence x <= z by XXREAL_0:def 5;
        Y c= REAL+ by A7,A10,XBOOLE_1:73;
        then reconsider y9 = y as Element of REAL+ by A12;
        o <=' y9 by ARYTM_1:6;
        hence thesis by Lm1;
      end;
      suppose
A13:    Y meets [:{0},REAL+:];
        {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 X9 = {r: [0,r] in X} as Subset of REAL+;
        {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 Y9 = {r : [0,r] in Y} as Subset of REAL+;
        consider e being set such that
A14:    e in Y and
A15:    e in [:{0},REAL+:] by A13,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:84;
        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;
A20:    y0 in Y by A14,A16,A18,TARSKI:def 1;
        then
A21:    y1 in Y9;
A22:    y0 in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
A23:    X c= [:{0},REAL+:]
        proof
          let u be set;
          assume
A24:      u in X;
          then reconsider x = u as real number;
          now
            assume x in REAL+;
            then
A25:        not x in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
            x <= y0 & not y0 in REAL+ by A1,A22,A20,A24,ARYTM_0:5,XBOOLE_0:3;
            hence contradiction by A25,XXREAL_0:def 5;
          end;
          hence thesis by A6,A24,XBOOLE_0:def 3;
        end;
        then consider e,x3 being set such that
A26:    e in {0} and
A27:    x3 in REAL+ and
A28:    x1 = [e,x3] by A5,ZFMISC_1:84;
        reconsider x3 as Element of REAL+ by A27;
        x1 = [0,x3] by A26,A28,TARSKI:def 1;
        then
A29:    x3 in X9 by A5;
        for y9,x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds y9 <=' x9
        proof
          let y9,x9 be Element of REAL+;
          assume y9 in Y9;
          then
A30:      ex r1 st y9 = r1 & [0,r1] in Y;
          assume x9 in X9;
          then
A31:      ex r2 st x9 = r2 & [0,r2] in X;
          then reconsider x = [0,x9], y = [0,y9] as real number by A30;
A32:      x in [:{0},REAL+:] & y in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
          x <= y by A1,A30,A31;
          then consider x99,y99 being Element of REAL+ such that
A33:      x = [0,x99] and
A34:      y = [0,y99] & y99 <=' x99 by A32,XXREAL_0:def 5;
          x9 = x99 by A33,XTUPLE_0:1;
          hence thesis by A34,XTUPLE_0:1;
        end;
        then consider z9 being Element of REAL+ such that
A35:    for y9,x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds
        y9 <=' z9 & z9 <=' x9 by A29,ARYTM_2:8;
A36:    y1 <> 0 by A19,ARYTM_0:3;
        y1 <=' z9 by A21,A29,A35;
        then [0,z9] in REAL by A36,ARYTM_0:2,ARYTM_1:5;
        then reconsider z = [0,z9] as real number;
        take z;
        let x,y such that
A37:    x in X and
A38:    y in Y;
        consider e,x9 being set such that
A39:    e in {0} and
A40:    x9 in REAL+ and
A41:    x = [e,x9] by A23,A37,ZFMISC_1:84;
        reconsider x9 as Element of REAL+ by A40;
A42:    z in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
A43:    x = [0,x9] by A39,A41,TARSKI:def 1;
        then
A44:    x9 in X9 by A37;
        now
          per cases by A7,A38,XBOOLE_0:def 3;
          suppose
A45:        y in REAL+;
            z9 <=' x9 by A21,A35,A44;
            hence x <= z by A23,A42,A37,A43,Lm1;
A46:        not y in [:{0},REAL+:] by A45,ARYTM_0:5,XBOOLE_0:3;
            not z in REAL+ by A42,ARYTM_0:5,XBOOLE_0:3;
            hence z <= y by A46,XXREAL_0:def 5;
          end;
          suppose
A47:        y in [:{0},REAL+:];
            then consider e,y9 being set such that
A48:        e in {0} and
A49:        y9 in REAL+ and
A50:        y = [e,y9] by ZFMISC_1:84;
            reconsider y9 as Element of REAL+ by A49;
A51:        y = [0,y9] by A48,A50,TARSKI:def 1;
            then y9 in Y9 by A38;
            then y9 <=' z9 & z9 <=' x9 by A35,A44;
            hence thesis by A23,A42,A37,A43,A47,A51,Lm1;
          end;
        end;
        hence thesis;
      end;
      suppose
A52:    X meets REAL+;
        reconsider X9 = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
        consider x1 being set such that
A53:    x1 in X and
A54:    x1 in REAL+ by A52,XBOOLE_0:3;
        reconsider x1 as Element of REAL+ by A54;
        x1 in REAL+;
        then reconsider x0 = x1 as real number by ARYTM_0:1;
A55:    Y c= REAL+
        proof
          let u be set;
          assume
A56:      u in Y;
          then reconsider y = u as real number;
          now
            assume y in [:{0},REAL+:];
            then
A57:        not y in REAL+ by ARYTM_0:5,XBOOLE_0:3;
            x0 <= y & not x0 in [:{0},REAL+:] by A1,A53,A56,ARYTM_0:5
,XBOOLE_0:3;
            hence contradiction by A57,XXREAL_0:def 5;
          end;
          hence thesis by A7,A56,XBOOLE_0:def 3;
        end;
        then reconsider Y9 = Y as Subset of REAL+;
        for x9,y9 being Element of REAL+ st x9 in X9 & y9 in Y9 holds x9 <=' y9
        proof
          let x9,y9 be Element of REAL+;
A58:      X9 c= X by XBOOLE_1:17;
          x9 in REAL+ & y9 in REAL+;
          then reconsider x = x9, y = y9 as real number by ARYTM_0:1
;
          assume x9 in X9 & y9 in Y9;
          then x <= y by A1,A58;
          then ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & x9 <=' y9
          by XXREAL_0:def 5;
          hence thesis;
        end;
        then consider z9 being Element of REAL+ such that
A59:    for x9,y9 being Element of REAL+ st x9 in X9 & y9 in Y9
        holds x9 <=' z9 & z9 <=' y9 by A8,ARYTM_2:8;
        z9 in REAL+;
        then reconsider z = z9 as real number by ARYTM_0:1;
        take z;
        let x,y such that
A60:    x in X and
A61:    y in Y;
        reconsider y9 = y as Element of REAL+ by A55,A61;
A62:    x0 in X9 by A53,XBOOLE_0:def 4;
        now
          per cases by A6,A60,XBOOLE_0:def 3;
          suppose
            x in REAL+;
            then reconsider x9 = x as Element of REAL+;
            x9 in X9 by A60,XBOOLE_0:def 4;
            then x9 <=' z9 & z9 <=' y9 by A59,A61;
            hence thesis by Lm1;
          end;
          suppose
A63:        x in [:{0},REAL+:];
A64:        not z in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
            not x in REAL+ by A63,ARYTM_0:5,XBOOLE_0:3;
            hence x <= z by A64,XXREAL_0:def 5;
            z9 <=' y9 by A62,A59,A61;
            hence z <= y by Lm1;
          end;
        end;
        hence thesis;
      end;
    end;
  end;
end;

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 x9,y9 being Element of REAL+ st x1 = x9 & y1 = y9 & +(x1,y1) = x9 +
  y9 by ARYTM_0:def 1,ARYTM_2:2;
  hence thesis by A1,A2,ARYTM_2:16;
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: B c= A by XBOOLE_1:17;
A4: for x9,y9 being Element of REAL+ st x9 in B & y9 = 1 holds x9 + y9 in B
  proof
    let x9,y9 be Element of REAL+ such that
A5: x9 in B and
A6: y9 = 1;
    x9 in REAL+;
    then reconsider x = x9 as Element of REAL by ARYTM_0:1;
    reconsider xx = x as real number;
    xx+1 in A by A2,A3,A5;
    then (ex x99,y99 being Element of REAL+ st x = x99 & 1 = y99 & +(x,1) =
    x99 + y99 )& +(x,1) in A by Lm3,ARYTM_0:def 1,ARYTM_2:20;
    hence thesis by A6,XBOOLE_0:def 4;
  end;
  0 in B by A1,ARYTM_2:20,XBOOLE_0:def 4;
  then NAT c= B by A4,ARYTM_2:17;
  hence thesis by A3,XBOOLE_1:1;
end;

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