:: Strong arithmetic of real numbers
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2026 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 ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0, NUMBERS,
ARYTM_0, FUNCOP_1, XBOOLE_0, TARSKI, NAT_1, REAL_1, ORDINAL1;
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, XREAL_0;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, XXREAL_0;
equalities XBOOLE_0, ARYTM_3, ORDINAL1;
expansions TARSKI;
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;
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;
Lm2: for x being Real, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof
let x be Real, 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;
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,o = 0 as Element of REAL+ by A12,ARYTM_2:20;
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 object;
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 object;
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 object such that
A14: e in Y and
A15: e in [:{0},REAL+:] by A13,XBOOLE_0:3;
consider u,y1 being object 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;
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 object;
assume
A24: u in X;
then reconsider x = u as Real;
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 object 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 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;
take z;
let x,y such that
A37: x in X and
A38: y in Y;
consider e,x9 being object 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;
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 object 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;
suppose
A52: X meets REAL+;
reconsider X9 = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
consider x1 being object 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 by ARYTM_0:1;
A55: Y c= REAL+
proof
let u be object;
assume
A56: u in Y;
then reconsider y = u as Real;
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 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 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;
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;
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;
reconsider x = x9 as Element of REAL by ARYTM_0:1;
reconsider y = 1 as Element of REAL by NUMBERS:19;
reconsider xx = x as Real;
xx+1 in A by A2,A3,A5;
then (ex x99,y99 being Element of REAL+ st x = x99 & 1 = y99 & +(x,y) =
x99 + y99 )& +(x,y) 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;
end;
theorem
for k being natural Number holds k = { i where i is Nat: i < k }
proof
let k be natural Number;
A1: k in NAT by ORDINAL1:def 12;
set Y = { i where i is Nat: i < k };
reconsider K = k as Element of NAT by ORDINAL1:def 12;
for e being object holds e in K iff e in Y
proof
let e be object;
thus e in K implies e in Y
proof
assume
A2: e in K;
A3: K 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;
reconsider x9 = K as Element of REAL+ by ARYTM_2:2;
y9 <=' x9 by A2,ARYTM_2:18;
then
A4: j <= k by Lm1;
reconsider yy9 = y9 as set;
not yy9 in yy9; then
y9 <> x9 by A2;
then j < k by A4,XXREAL_0:1;
hence thesis;
end;
assume e in Y;
then consider i be Nat such that
A5: e = i and
A6: not k <= i;
A7: i in NAT by ORDINAL1:def 12;
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,A7,ARYTM_2:18;
end;
hence thesis by TARSKI:2;
end;