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

definition

let r be object ;

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 object holds
( r is real iff r in REAL );

registration

cluster -> real for Element of REAL ;

coherence
for b₁ being Element of REAL holds b₁ is real ;

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 object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is real by NUMBERS:19;

cluster real -> complex for object ;

coherence
for b₁ being object st b₁ is real holds
b₁ is complex ;

end;

registration

cluster real for object ;

existence
ex b₁ being object st b₁ is real

proof end;

cluster real for set ;

existence
ex b₁ being number st b₁ is real

proof end;

cluster real -> ext-real for object ;

coherence
for b₁ being object st b₁ is real holds
b₁ is ext-real

proof end;

end;

definition

mode Real is real Number ;

end;

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

proof end;

registration

let x be Real;

cluster - x -> real ;

coherence
- x is real

proof end;

cluster x " -> real ;

coherence
x " is real

proof end;

let y be Real;

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;

cluster x - y -> real ;

coherence
x - y is real ;

cluster x / y -> real ;

coherence
x / y is real ;

end;

Lm2: for r, s being Real 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 st r <= s & s <= r holds
r = s

proof end;

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

proof end;

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

proof end;

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

Lm8: 0 <= 1

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

cluster complex ext-real positive real for object ;

existence
ex b₁ being Real st b₁ is positive

proof end;

cluster complex ext-real negative real for object ;

existence
ex b₁ being Real st b₁ is negative

proof end;

cluster zero complex ext-real real for object ;

existence
ex b₁ being Real st b₁ is zero

proof end;

end;

registration

let r, s be non negative Real;

cluster r + s -> non negative ;

coherence
not r + s is negative

proof end;

end;

registration

let r, s be non positive Real;

cluster r + s -> non positive ;

coherence
not r + s is positive

proof end;

end;

registration

let r be positive Real;
let s be non negative Real;

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;
let s be non positive Real;

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;

cluster - r -> non negative ;

coherence
not - r is negative

proof end;

end;

registration

let r be non negative Real;

cluster - r -> non positive ;

coherence
not - r is positive

proof end;

end;

registration

let r be non negative Real;
let s be non positive Real;

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;
let s be non positive Real;

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;
let s be non negative Real;

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;
let s be non negative Real;

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;

cluster r * s -> non negative ;

coherence
not r * s is negative

proof end;

end;

registration

let r, s be non negative Real;

cluster r * s -> non negative ;

coherence
not r * s is negative

proof end;

end;

registration

let r be positive Real;

cluster r " -> positive ;

coherence
r " is positive

proof end;

end;

registration

let r be non positive Real;

cluster r " -> non positive ;

coherence
not r " is positive

proof end;

end;

registration

let r be negative Real;

cluster r " -> negative ;

coherence
r " is negative ;

end;

registration

let r be non negative Real;

cluster r " -> non negative ;

coherence
not r " is negative

proof end;

end;

registration

let r be non negative Real;
let s be non positive Real;

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;

cluster r / s -> non negative ;

coherence
not r / s is negative ;

end;

registration

let r, s be non positive Real;

cluster r / s -> non negative ;

coherence
not r / s is negative ;

end;

registration

let r, s be Real;

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;

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 b₁ being set holds verum;
;

end;

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

registration

let r, s be Real;

cluster r -' s -> real ;

coherence
r -' s is real

proof end;

end;

registration

let r, s be Real;

cluster r -' s -> non negative for Real;

coherence
for b₁ being Real st b₁ = r -' s holds
not b₁ is negative

proof end;

end;

registration

Real ex b₁ being set st
for b₂ being Real holds b₂ in b₁

proof end;

end;

:: 16.04.20121, A.T.

registration

let i be Real;

reduce In (i,REAL) to i;

reducibility
In (i,REAL) = i by Def1, SUBSET_1:def 8;

end;