:: by Library Committee

::

:: Received February 11, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

:: deftheorem Def1 defines real XREAL_0:def 1 :

for r being object holds

( r is real iff r in REAL );

for r being object holds

( r is real iff r in REAL );

registration

coherence

for b_{1} being object st b_{1} is natural holds

b_{1} is real
by NUMBERS:19;

coherence

for b_{1} being object st b_{1} is real holds

b_{1} is complex
;

end;
for b

b

coherence

for b

b

registration

existence

ex b_{1} being object st b_{1} is real

ex b_{1} being number st b_{1} is real

for b_{1} being object st b_{1} is real holds

b_{1} is ext-real

end;
ex b

proof end;

existence ex b

proof end;

coherence for b

b

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

coherence

- x is real

x " is real

coherence

x + y is real

x * y is real

end;
coherence

- x is real

proof end;

coherence x " is real

proof end;

let y be Real;coherence

x + y is real

proof end;

coherence x * y is real

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

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

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;

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

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

existence

ex b_{1} being Real st b_{1} is positive

ex b_{1} being Real st b_{1} is negative

ex b_{1} being Real st b_{1} is zero

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

registration

let r be positive Real;

let s be non negative Real;

coherence

r + s is positive

s + r is positive ;

end;
let s be non negative Real;

coherence

r + s is positive

proof end;

coherence s + r is positive ;

registration

let r be negative Real;

let s be non positive Real;

coherence

r + s is negative

s + r is negative ;

end;
let s be non positive Real;

coherence

r + s is negative

proof end;

coherence s + r is negative ;

registration
end;

registration
end;

registration

let r be non negative Real;

let s be non positive Real;

coherence

not r - s is negative ;

coherence

not s - r is positive ;

end;
let s be non positive Real;

coherence

not r - s is negative ;

coherence

not s - r is positive ;

registration

let r be positive Real;

let s be non positive Real;

coherence

r - s is positive ;

coherence

s - r is negative ;

end;
let s be non positive Real;

coherence

r - s is positive ;

coherence

s - r is negative ;

registration

let r be negative Real;

let s be non negative Real;

coherence

r - s is negative ;

coherence

s - r is positive ;

end;
let s be non negative Real;

coherence

r - s is negative ;

coherence

s - r is positive ;

registration

let r be non positive Real;

let s be non negative Real;

coherence

not r * s is positive

not s * r is positive ;

end;
let s be non negative Real;

coherence

not r * s is positive

proof end;

coherence not s * r is positive ;

registration
end;

registration
end;

registration
end;

registration

let r be non negative Real;

let s be non positive Real;

coherence

not r / s is positive ;

coherence

not s / r is positive ;

end;
let s be non positive Real;

coherence

not r / s is positive ;

coherence

not s / r is positive ;

registration
end;

registration
end;

registration

let r, s be Real;

coherence

min (r,s) is real by XXREAL_0:15;

coherence

max (r,s) is real by XXREAL_0:16;

end;
coherence

min (r,s) is real by XXREAL_0:15;

coherence

max (r,s) is real by XXREAL_0:16;

definition

let r, s be Real;

correctness

coherence

( ( r - s >= 0 implies r - s is set ) & ( not r - s >= 0 implies 0 is set ) );

consistency

for b_{1} being set holds verum;

;

end;
correctness

coherence

( ( r - s >= 0 implies r - s is set ) & ( not r - s >= 0 implies 0 is set ) );

consistency

for b

;

:: 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 ) );

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;

coherence

for b_{1} being Real st b_{1} = r -' s holds

not b_{1} is negative

end;
coherence

for b

not b

proof end;

:: 16.04.20121, A.T.

registration
end;