:: Introduction to Arithmetic of Real Numbers
:: by Library Committee
::
:: Received February 11, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

definition
let r be number ;
attr r is real means :Def1: :: XREAL_0:def 1
r in REAL ;
end;

:: deftheorem Def1 defines real XREAL_0:def 1 :
for r being number holds
( r is real iff r in REAL );

registration
cluster -> real for Element of REAL ;
coherence
for b1 being Element of REAL holds b1 is real
proof end;
end;

registration
cluster -infty -> non real ;
coherence
not -infty is real
proof end;
cluster +infty -> non real ;
coherence
not +infty is real
proof end;
end;

registration
cluster natural -> real for set ;
coherence
for b1 being number st b1 is natural holds
b1 is real
proof end;
cluster real -> complex for set ;
coherence
for b1 being number st b1 is real holds
b1 is complex
proof end;
end;

registration
cluster real for set ;
existence
ex b1 being number st b1 is real
proof end;
cluster real -> ext-real for set ;
coherence
for b1 being number st b1 is real holds
b1 is ext-real
proof end;
end;

Lm1: for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )

proof end;

registration
let x be real number ;
cluster - x -> real ;
coherence
- x is real
proof end;
cluster x " -> real ;
coherence
x " is real
proof end;
let y be real number ;
cluster x + y -> real ;
coherence
x + y is real
proof end;
cluster x * y -> real ;
coherence
x * y is real
proof end;
end;

registration
let x, y be real number ;
cluster x - y -> real ;
coherence
x - y is real
;
cluster x / y -> real ;
coherence
x / y is real
;
end;

begin

Lm2: for r, s being real number st ( ( 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+:] ) ) holds
r <= s

proof end;

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

Lm4: for r, s being real number st r <= s & s <= r holds
r = s

proof end;

Lm5: for r, s, t being real number st r <= s holds
r + t <= s + t

proof end;

Lm6: for r, s, t being real number st r <= s & s <= t holds
r <= t

proof end;

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

Lm7: not 0 in [:{0},REAL+:]
by ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3;

reconsider j = 1 as Element of REAL+ by ARYTM_2:20;

z <=' j
by ARYTM_1:6;

then Lm8: 0 <= 1
by Lm2;

1 + (- 1) = 0
;

then consider x1, x2, y1, y2 being Element of REAL such that
Lm9: 1 = [*x1,x2*] and
Lm10: ( - 1 = [*y1,y2*] & 0 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by XCMPLX_0:def 4;

Lm11: x1 = 1
by Lm1, Lm9;

Lm12: ( y1 = - 1 & + (x1,y1) = 0 )
by Lm1, Lm10;

Lm13: now :: thesis: not - 1 in REAL+
assume - 1 in REAL+ ; :: thesis: contradiction
then ex x9, y9 being Element of REAL+ st
( x1 = x9 & y1 = y9 & z = x9 + y9 ) by Lm11, Lm12, ARYTM_0:def 1, ARYTM_2:20;
hence contradiction by Lm11, ARYTM_2:5; :: thesis: verum
end;

Lm14: for r, s being real number st r >= 0 & s > 0 holds
r + s > 0

proof end;

Lm15: for r, s being real number st r <= 0 & s < 0 holds
r + s < 0

proof end;

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

Lm16: for r, s, t being real number st r <= s & 0 <= t holds
r * t <= s * t

proof end;

Lm17: for r, s being real number st r > 0 & s > 0 holds
r * s > 0

proof end;

Lm18: for r, s being real number st r > 0 & s < 0 holds
r * s < 0

proof end;

Lm19: for s, t being real number st s <= t holds
- t <= - s

proof end;

Lm20: for r, s being real number st r <= 0 & s >= 0 holds
r * s <= 0

proof end;

registration
cluster complex ext-real positive real for set ;
existence
ex b1 being real number st b1 is positive
proof end;
cluster complex ext-real negative real for set ;
existence
ex b1 being real number st b1 is negative
proof end;
cluster zero complex ext-real real for set ;
existence
ex b1 being real number st b1 is zero
proof end;
end;

registration
let r, s be non negative real number ;
cluster r + s -> non negative ;
coherence
not r + s is negative
proof end;
end;

registration
let r, s be non positive real number ;
cluster r + s -> non positive ;
coherence
not r + s is positive
proof end;
end;

registration
let r be positive real number ;
let s be non negative real number ;
cluster r + s -> positive ;
coherence
r + s is positive
proof end;
cluster s + r -> positive ;
coherence
s + r is positive
;
end;

registration
let r be negative real number ;
let s be non positive real number ;
cluster r + s -> negative ;
coherence
r + s is negative
proof end;
cluster s + r -> negative ;
coherence
s + r is negative
;
end;

registration
let r be non positive real number ;
cluster - r -> non negative ;
coherence
not - r is negative
proof end;
end;

registration
let r be non negative real number ;
cluster - r -> non positive ;
coherence
not - r is positive
proof end;
end;

registration
let r be non negative real number ;
let s be non positive real number ;
cluster r - s -> non negative ;
coherence
not r - s is negative
;
cluster s - r -> non positive ;
coherence
not s - r is positive
;
end;

registration
let r be positive real number ;
let s be non positive real number ;
cluster r - s -> positive ;
coherence
r - s is positive
;
cluster s - r -> negative ;
coherence
s - r is negative
;
end;

registration
let r be negative real number ;
let s be non negative real number ;
cluster r - s -> negative ;
coherence
r - s is negative
;
cluster s - r -> positive ;
coherence
s - r is positive
;
end;

registration
let r be non positive real number ;
let s be non negative real number ;
cluster r * s -> non positive ;
coherence
not r * s is positive
proof end;
cluster s * r -> non positive ;
coherence
not s * r is positive
;
end;

registration
let r, s be non positive real number ;
cluster r * s -> non negative ;
coherence
not r * s is negative
proof end;
end;

registration
let r, s be non negative real number ;
cluster r * s -> non negative ;
coherence
not r * s is negative
proof end;
end;

registration
let r be positive real number ;
cluster r " -> positive ;
coherence
r " is positive
proof end;
end;

registration
let r be non positive real number ;
cluster r " -> non positive ;
coherence
not r " is positive
proof end;
end;

registration
let r be negative real number ;
cluster r " -> negative ;
coherence
r " is negative
;
end;

registration
let r be non negative real number ;
cluster r " -> non negative ;
coherence
not r " is negative
proof end;
end;

registration
let r be non negative real number ;
let s be non positive real number ;
cluster r / s -> non positive ;
coherence
not r / s is positive
;
cluster s / r -> non positive ;
coherence
not s / r is positive
;
end;

registration
let r, s be non negative real number ;
cluster r / s -> non negative ;
coherence
not r / s is negative
;
end;

registration
let r, s be non positive real number ;
cluster r / s -> non negative ;
coherence
not r / s is negative
;
end;

begin

registration
let r, s be real number ;
cluster min (r,s) -> real ;
coherence
min (r,s) is real
by XXREAL_0:15;
cluster max (r,s) -> real ;
coherence
max (r,s) is real
by XXREAL_0:16;
end;

definition
let r, s be real number ;
func r -' s -> set equals :Def2: :: XREAL_0:def 2
r - s if r - s >= 0
otherwise 0 ;
correctness
coherence
( ( r - s >= 0 implies r - s is set ) & ( not r - s >= 0 implies 0 is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem Def2 defines -' XREAL_0:def 2 :
for r, s being real number holds
( ( r - s >= 0 implies r -' s = r - s ) & ( not r - s >= 0 implies r -' s = 0 ) );

registration
let r, s be real number ;
cluster r -' s -> real ;
coherence
r -' s is real
proof end;
end;

registration
let r, s be real number ;
cluster r -' s -> non negative real for real number ;
coherence
for b1 being real number st b1 = r -' s holds
not b1 is negative
proof end;
end;