Copyright (c) 1995 Association of Mizar Users
environ
vocabulary ARYTM_2, BOOLE, ARYTM_1, ARYTM_3, ORDINAL2, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ARYTM_2, ARYTM_1,
ARYTM_0;
constructors ARYTM_1, ARYTM_0;
clusters ARYTM_2, ARYTM_0;
requirements BOOLE, SUBSET;
theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, ORDINAL2, XBOOLE_1,
ARYTM_0;
begin
definition let r be number;
attr r is real means
:Def2: r in REAL;
end;
definition
cluster real number;
existence
proof
consider r being Element of REAL;
take r;
thus r in REAL;
end;
end;
definition let x,y be real number;
A1: x in REAL & y in REAL by Def2;
func x + y means :Def3:
ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' + y'
if x in REAL+ & y in REAL+,
ex x',y' being Element of REAL+ st x = x' & y = [{},y'] & it = x' - y'
if x in REAL+ & y in [:{{}},REAL+:],
ex x',y' being Element of REAL+ st x = [{},x'] & y = y' & it = y' - x'
if y in REAL+ & x in [:{{}},REAL+:]
otherwise
ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & it = [{}
,y'+x'];
existence
proof
hereby assume x in REAL+ & y in REAL+;
then reconsider x'=x, y'=y as Element of REAL+;
reconsider IT = x' + y' as number;
take IT,x',y';
thus x = x' & y = y' & IT = x' + y';
end;
hereby assume x in REAL+;
then reconsider x'=x as Element of REAL+;
assume y in [:{{}},REAL+:];
then consider z,y' being set such that
A2: z in{{}} and
A3: y' in REAL+ and
A4: y = [z,y'] by ZFMISC_1:103;
reconsider y' as Element of REAL+ by A3;
reconsider IT = x' - y' as number;
take IT,x',y';
z = {} by A2,TARSKI:def 1;
hence x = x' & y = [{},y'] & IT = x' - y' by A4;
end;
hereby assume y in REAL+;
then reconsider y'=y as Element of REAL+;
assume x in [:{{}},REAL+:];
then consider z,x' being set such that
A5: z in{{}} and
A6: x' in REAL+ and
A7: x = [z,x'] by ZFMISC_1:103;
reconsider x' as Element of REAL+ by A6;
reconsider IT = y' - x' as number;
take IT,x',y';
z = {} by A5,TARSKI:def 1;
hence x = [{},x'] & y = y' & IT = y' - x' by A7;
end;
x in REAL+ \/ [:{{}},REAL+:] & y in REAL+ \/ [:{{}},REAL+:]
by A1,ARYTM_0:def 1,XBOOLE_0:def 4; then
A8: (x in REAL+ or x in [:{{}},REAL+:]) &
(y in REAL+ or y in [:{{}},REAL+:]) by XBOOLE_0:def 2;
assume
A9: not(x in REAL+ & y in REAL+) &
not(x in REAL+ & y in [:{{}},REAL+:]) &
not(y in REAL+ & x in [:{{}},REAL+:]);
then x in [:{{}},REAL+:] by A8;
then consider z1,x' being set such that
A10: z1 in{{}} and
A11: x' in REAL+ and
A12: x = [z1,x'] by ZFMISC_1:103;
reconsider x' as Element of REAL+ by A11;
y in [:{{}},REAL+:] by A9,A8;
then consider z2,y' being set such that
A13: z2 in{{}} and
A14: y' in REAL+ and
A15: y = [z2,y'] by ZFMISC_1:103;
reconsider y' as Element of REAL+ by A14;
reconsider IT = [{},y' + x'] as number;
take IT,x',y';
z1 = {} & z2 = {} by A10,A13,TARSKI:def 1;
hence x = [{},x'] & y = [{},y'] & IT = [{},y' + x'] by A12,A15;
end;
uniqueness
proof let IT1,IT2 be number;
thus x in REAL+ & y in REAL+ &
(ex x',y' being Element of REAL+ st x = x' & y = y' & IT1 = x' + y') &
(ex x',y' being Element of REAL+ st x = x' & y = y' & IT2 = x' + y')
implies IT1 = IT2;
thus x in REAL+ & y in [:{{}},REAL+:] &
(ex x',y' being Element of REAL+ st x = x' & y = [{},y'] & IT1 = x' - y')
& (ex x'',y'' being Element of REAL+ st x = x'' & y = [{},y''] &
IT2 = x'' - y'') implies IT1 = IT2 by ZFMISC_1:33;
thus y in REAL+ & x in [:{{}},REAL+:] &
(ex x',y' being Element of REAL+ st x = [{},x'] & y = y' & IT1 = y' - x')
& (ex x'',y'' being Element of REAL+ st x = [{},x''] & y = y'' &
IT2 = y'' - x'') implies IT1 = IT2 by ZFMISC_1:33;
assume
not(x in REAL+ & y in REAL+) &
not(x in REAL+ & y in [:{{}},REAL+:]) &
not(y in REAL+ & x in [:{{}},REAL+:]);
given x',y' being Element of REAL+ such that
A16: x = [{},x'] & y = [{},y'] and
A17: IT1 = [{},y'+x'];
given x'',y'' being Element of REAL+ such that
A18: x = [{},x''] & y = [{},y''] and
A19: IT2 = [{},y''+x''];
x' = x'' & y' = y'' by A16,A18,ZFMISC_1:33;
hence thesis by A17,A19;
end;
consistency by XBOOLE_0:3,ARYTM_0:5;
commutativity;
func x * y means :Def4:
ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' *' y'
if x in REAL+ & y in REAL+,
ex x',y' being Element of REAL+ st x = x' & y = [{},y'] & it = [{},x' *' y']
if x in REAL+ & y in [:{{}},REAL+:] & x <> {},
ex x',y' being Element of REAL+ st x = [{},x'] & y = y' & it = [{},y' *' x']
if y in REAL+ & x in [:{{}},REAL+:] & y <> {},
ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & it = y' *' x'
if x in [:{{}},REAL+:] & y in [:{{}},REAL+:]
otherwise it = {};
existence
proof
hereby assume x in REAL+ & y in REAL+;
then reconsider x'=x, y'=y as Element of REAL+;
reconsider IT = x' *' y' as number;
take IT,x',y';
thus x = x' & y = y' & IT = x' *' y';
end;
hereby assume x in REAL+;
then reconsider x'=x as Element of REAL+;
assume y in [:{{}},REAL+:];
then consider z,y' being set such that
A20: z in{{}} and
A21: y' in REAL+ and
A22: y = [z,y'] by ZFMISC_1:103;
reconsider y' as Element of REAL+ by A21;
assume x <> {};
reconsider IT = [{},x' *' y'] as number;
take IT,x',y';
z = {} by A20,TARSKI:def 1;
hence x = x' & y = [{},y'] & IT = [{},x' *' y'] by A22;
end;
hereby assume y in REAL+;
then reconsider y'=y as Element of REAL+;
assume x in [:{{}},REAL+:];
then consider z,x' being set such that
A23: z in{{}} and
A24: x' in REAL+ and
A25: x = [z,x'] by ZFMISC_1:103;
reconsider x' as Element of REAL+ by A24;
assume y <> {};
reconsider IT = [{},y' *' x'] as number;
take IT,x',y';
z = {} by A23,TARSKI:def 1;
hence x = [{},x'] & y = y' & IT = [{},y' *' x'] by A25;
end;
hereby assume x in [:{{}},REAL+:];
then consider z1,x' being set such that
A26: z1 in{{}} and
A27: x' in REAL+ and
A28: x = [z1,x'] by ZFMISC_1:103;
reconsider x' as Element of REAL+ by A27;
assume y in [:{{}},REAL+:];
then consider z2,y' being set such that
A29: z2 in{{}} and
A30: y' in REAL+ and
A31: y = [z2,y'] by ZFMISC_1:103;
reconsider y' as Element of REAL+ by A30;
reconsider IT = y' *' x' as number;
take IT,x',y';
z1 = {} & z2 = {} by A26,A29,TARSKI:def 1;
hence x = [{},x'] & y = [{},y'] & IT = y' *' x' by A28,A31;
end;
thus thesis;
end;
uniqueness
proof let IT1,IT2 be number;
thus x in REAL+ & y in REAL+ &
(ex x',y' being Element of REAL+ st x = x' & y = y' & IT1 = x' *' y') &
(ex x',y' being Element of REAL+ st x = x' & y = y' & IT2 = x' *' y')
implies IT1 = IT2;
thus x in REAL+ & y in [:{{}},REAL+:] & x <> {} &
(ex x',y' being Element of REAL+ st x = x' & y = [{},y'] &
IT1 = [{},x' *' y']) &
(ex x'',y'' being Element of REAL+ st x = x'' & y = [{},y''] &
IT2 = [{},x'' *' y'']) implies IT1 = IT2 by ZFMISC_1:33;
thus y in REAL+ & x in [:{{}},REAL+:] & y <> {} &
(ex x',y' being Element of REAL+ st x = [{},x'] & y = y' &
IT1 = [{},y' *' x']) &
(ex x'',y'' being Element of REAL+ st x = [{},x''] & y = y'' &
IT2 = [{},y'' *' x'']) implies IT1 = IT2 by ZFMISC_1:33;
hereby assume
x in [:{{}},REAL+:] & y in [:{{}},REAL+:];
given x',y' being Element of REAL+ such that
A32: x = [{},x'] & y = [{},y'] and
A33: IT1 = y' *' x';
given x'',y'' being Element of REAL+ such that
A34: x = [{},x''] & y = [{},y''] and
A35: IT2 = y'' *' x'';
x' = x'' & y' = y'' by A32,A34,ZFMISC_1:33;
hence IT1 = IT2 by A33,A35;
end;
thus thesis;
end;
consistency by XBOOLE_0:3,ARYTM_0:5;
commutativity;
pred x <= y means
ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'
if x in REAL+ & y in REAL+,
ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & y' <=' x'
if x in [:{{}},REAL+:] & y in [:{{}},REAL+:]
otherwise y in REAL+ & x in [:{{}},REAL+:];
consistency by XBOOLE_0:3,ARYTM_0:5;
reflexivity
proof let x be real number such that
A36: not((x in REAL+ & x in REAL+ implies
ex x',y' being Element of REAL+ st x = x' & x = y' & x' <=' y') &
(x in [:{{}},REAL+:] & x in [:{{}},REAL+:] implies
ex x',y' being Element of REAL+ st x = [{},x'] & x = [{}
,y'] & y' <=' x') &
(not(x in REAL+ & x in REAL+) & not(x in [:{{}},REAL+:] & x in
[:{{}},REAL+:])
implies x in REAL+ & x in [:{{}},REAL+:]));
x in REAL by Def2; then
(x in REAL+ \/ [:{{}},REAL+:]) by ARYTM_0:def 1,XBOOLE_0:def 4; then
(x in REAL+ or x in [:{{}},REAL+:]) by XBOOLE_0:def 2; then
A37: (x in REAL+ iff not x in [:{{}},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
per cases by A36;
suppose that
A38: x in REAL+ and
A39: not ex x',y' being Element of REAL+ st x = x' & x = y' & x' <=' y';
reconsider x' = x as Element of REAL+ by A38;
not x' <=' x' by A39;
hence thesis;
suppose that
A40: x in [:{{}},REAL+:] and
A41: not ex x',y' being Element of REAL+
st x = [{},x'] & x = [{},y'] & y' <=' x';
consider z,x' being set such that
A42: z in {{}} and
A43: x' in REAL+ and
A44: x = [z,x'] by A40,ZFMISC_1:103;
reconsider x' as Element of REAL+ by A43;
z = {} by A42,TARSKI:def 1; then
x = [{},x'] by A44; then
not x' <=' x' by A41;
hence thesis;
suppose not(not x in REAL+ & not x in [:{{}},REAL+:]
implies x in REAL+ & x in [:{{}},REAL+:]);
hence thesis by A37;
end;
connectedness
proof let x,y be real number such that
A45: not((x in REAL+ & y in REAL+ implies
ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y') &
(x in [:{{}},REAL+:] & y in [:{{}},REAL+:] implies
ex x',y' being Element of REAL+ st x = [{},x'] & y = [{}
,y'] & y' <=' x') &
(not(x in REAL+ & y in REAL+) & not(x in [:{{}},REAL+:] & y in
[:{{}},REAL+:])
implies y in REAL+ & x in [:{{}},REAL+:]));
x in REAL & y in REAL by Def2; then
(x in REAL+ \/ [:{{}},REAL+:]) &
(y in REAL+ \/ [:{{}},REAL+:]) by ARYTM_0:def 1,XBOOLE_0:def 4; then
(x in REAL+ or x in [:{{}},REAL+:]) &
(y in REAL+ or y in [:{{}},REAL+:]) by XBOOLE_0:def 2; then
A46: (x in REAL+ iff not x in [:{{}},REAL+:]) &
(y in REAL+ iff not y in [:{{}},REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
per cases by A45;
suppose that
A47: x in REAL+ & y in REAL+ and
A48: not ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y';
hereby assume y in REAL+ & x in REAL+;
then reconsider x' = x, y' = y as Element of REAL+;
take y',x';
thus y = y' & x = x';
not x' <=' y' by A48;
hence y' <=' x';
end;
thus thesis by A47,A46;
suppose that
A49: x in [:{{}},REAL+:] & y in [:{{}},REAL+:] and
A50: not ex x',y' being Element of REAL+
st x = [{},x'] & y = [{},y'] & y' <=' x';
now assume y in [:{{}},REAL+:];
then consider z,y' being set such that
A51: z in {{}} and
A52: y' in REAL+ and
A53: y = [z,y'] by ZFMISC_1:103;
A54: z = {} by A51,TARSKI:def 1;
assume x in [:{{}},REAL+:];
then consider z,x' being set such that
A55: z in {{}} and
A56: x' in REAL+ and
A57: x = [z,x'] by ZFMISC_1:103;
A58: z = {} by A55,TARSKI:def 1;
reconsider x',y' as Element of REAL+ by A52,A56;
take y',x';
thus y = [{},y'] & x = [{},x'] by A54,A58,A53,A57;
then not y' <=' x' by A50;
hence x' <=' y';
end;
hence thesis by A49,A46;
suppose not(not(x in REAL+ & y in REAL+) &
not(x in [:{{}},REAL+:] & y in [:{{}},REAL+:])
implies y in REAL+ & x in [:{{}},REAL+:]);
hence thesis by A46;
end;
synonym y >= x;
antonym y < x;
antonym x > y;
end;
definition let x,y be real number;
cluster x + y -> real;
coherence
proof
per cases;
suppose x in REAL+ & y in REAL+; then
consider x',y' being Element of REAL+ such that
A1: x = x' & y = y' & x + y = x' + y' by Def3;
x' + y' in REAL+;
hence x + y in REAL by A1,ARYTM_0:1;
suppose x in REAL+ & y in [:{{}},REAL+:]; then
consider x',y' being Element of REAL+ such that
A2: x = x' & y = [{},y'] & x + y = x' - y' by Def3;
x' - y' in REAL by ARYTM_0:4;
hence x + y in REAL by A2;
suppose y in REAL+ & x in [:{{}},REAL+:]; then
consider x',y' being Element of REAL+ such that
A3: x = [{},x'] & y = y' & x + y = y' - x' by Def3;
y' - x' in REAL by ARYTM_0:4;
hence x + y in REAL by A3;
suppose not (x in REAL+ & y in REAL+) &
not (x in REAL+ & y in [:{{}},REAL+:]) &
not (y in REAL+ & x in [:{{}},REAL+:]); then
consider x',y' being Element of REAL+ such that
A4: x = [{},x'] & y = [{},y'] & x + y = [{},y'+x'] by Def3;
y in REAL by Def2; then
y' <> {} by A4,ARYTM_0:3; then
y'+x' <> {} by ARYTM_2:5; then
[{},y'+x'] in REAL by ARYTM_0:2;
hence x + y in REAL by A4;
end;
cluster x * y -> real;
coherence
proof
per cases;
suppose x in REAL+ & y in REAL+; then
consider x',y' being Element of REAL+ such that
A5: x = x' & y = y' & x * y = x' *' y' by Def4;
x' *' y' in REAL+;
hence x * y in REAL by A5,ARYTM_0:1;
suppose that
A6: x in REAL+ & y in [:{{}},REAL+:] and
A7: x <> {};
consider x',y' being Element of REAL+ such that
A8: x = x' & y = [{},y'] & x * y = [{},x' *' y'] by A6,A7,Def4;
y in REAL by Def2; then
y' <> {} by A8,ARYTM_0:3; then
x' *' y' <> {} by A8,A7,ARYTM_1:2;
hence x * y in REAL by A8,ARYTM_0:2;
suppose
A9: y in REAL+ & x in [:{{}},REAL+:] & y <> {}; then
consider x',y' being Element of REAL+ such that
A10: x = [{},x'] & y = y' & x * y = [{},y' *' x'] by Def4;
x in REAL by Def2; then
x' <> {} by A10,ARYTM_0:3; then
y' *' x' <> {} by A10,A9,ARYTM_1:2;
hence x * y in REAL by A10,ARYTM_0:2;
suppose x in [:{{}},REAL+:] & y in [:{{}},REAL+:]; then
consider x',y' being Element of REAL+ such that
A11: x = [{},x'] & y = [{},y'] & x * y = y' *' x' by Def4;
y' *' x' in REAL+;
hence x * y in REAL by A11,ARYTM_0:1;
suppose not (x in REAL+ & y in REAL+) &
not (x in REAL+ & y in [:{{}},REAL+:] & x <> {}) &
not (y in REAL+ & x in [:{{}},REAL+:] & y <> {}) &
not (x in [:{{}},REAL+:] & y in [:{{}},REAL+:]); then
x*y = {} by Def4;
hence x*y in REAL by ARYTM_0:1,ARYTM_2:20;
end;
end;
definition
cluster -> real Element of REAL;
coherence
proof
let r be Element of REAL;
thus r in REAL;
end;
end;
definition let x,y be Element of REAL;
redefine func x + y -> Element of REAL;
coherence by Def2;
redefine func x * y -> Element of REAL;
coherence by Def2;
end;
definition
cluster natural -> real number;
coherence
proof
let x be number;
assume x is natural; then
x in NAT by ORDINAL2:def 21;
hence x in REAL;
end;
end;