:: XREAL_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 natural -> real set ;
coherence
for b1 being number st b1 is natural holds
b1 is real
proof end;
cluster real -> complex set ;
coherence
for b1 being number st b1 is real holds
b1 is complex
proof end;
end;

registration
cluster complex real set ;
existence
ex b1 being number st b1 is real
proof end;
end;

definition
let x, y be real number ;
pred x <= y means :Def2: :: XREAL_0:def 2
 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 = [0,x'] & y = [0,y'] & y' <=' x' ) if ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] )
otherwise ( y in REAL+ & x in [:{0},REAL+ :] );
consistency
( x in REAL+ & y in REAL+ & x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & x' <=' y' ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & y' <=' x' ) ) ) by ARYTM_0:5, XBOOLE_0:3;
reflexivity
for x being real number holds
( ( x in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & x = y' & x' <=' y' ) ) & ( x in [:{0},REAL+ :] & x in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0,x'] & x = [0,y'] & y' <=' x' ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+ :] or not x in [:{0},REAL+ :] ) implies ( x in REAL+ & x in [:{0},REAL+ :] ) ) )
proof end;
connectedness
for x, y being real number st ( ( x in REAL+ & y in REAL+ & ( for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) or ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0,x'] or not y = [0,y'] or not y' <=' x' ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) & not ( y in REAL+ & x in [:{0},REAL+ :] ) ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0},REAL+ :] & x in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0,x'] & x = [0,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+ :] or not x in [:{0},REAL+ :] ) implies ( x in REAL+ & y in [:{0},REAL+ :] ) ) )
proof end;
end;

:: deftheorem Def2 defines <= XREAL_0:def 2 :
for x, y being real number holds
( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x', y' being Element of REAL+ st
( x = x' & y = y' & x' <=' y' ) ) ) & ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( x <= y iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & y' <=' x' ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) implies ( x <= y iff ( y in REAL+ & x in [:{0},REAL+ :] ) ) ) );

notation
let x, y be real number ;
synonym y >= x for x <= y;
antonym y < x for x <= y;
antonym x > y for x <= y;
end;

definition
let x be real number ;
attr x is positive means :Def3: :: XREAL_0:def 3
x > 0;
attr x is negative means :Def4: :: XREAL_0:def 4
x < 0;
end;

:: deftheorem Def3 defines positive XREAL_0:def 3 :
for x being real number holds
( x is positive iff x > 0 );

:: deftheorem Def4 defines negative XREAL_0:def 4 :
for x being real number holds
( x is negative iff x < 0 );

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;

Lm2: one = succ 0 by ORDINAL2:def 4
.= 1 ;

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

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

reconsider j = 1 as Element of REAL+ by Lm2, ARYTM_2:21;

z <=' j
by ARYTM_1:6;

then Lm8: 0 <= 1
by Def2;

1 + (- 1) = 0
;

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

Lm12: x1 = 1
by Lm1, Lm9;

Lm13: y1 = - 1
by Lm1, Lm10;

Lm14: + x1,y1 = 0
by Lm1, Lm11;

Lm15: now
assume - 1 in REAL+ ; :: thesis: contradiction
then ex x', y' being Element of REAL+ st
( x1 = x' & y1 = y' & z = x' + y' ) by Lm2, Lm12, Lm13, Lm14, ARYTM_0:def 2, ARYTM_2:21;
hence contradiction by Lm12, ARYTM_2:6; :: thesis: verum
end;

Lm16: for r, s being real number st r >= 0 & s > 0 holds
r + s > 0
proof end;

Lm17: 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:21;

Lm18: for r, s, t being real number st r <= s & 0 <= t holds
r * t <= s * t
proof end;

Lm19: for r, s, t being real number holds (r * s) * t = r * (s * t)
;

Lm20: for r, s being real number holds
( not r * s = 0 or r = 0 or s = 0 )
proof end;

Lm21: for r, s being real number st r > 0 & s > 0 holds
r * s > 0
proof end;

Lm22: for r, s being real number st r > 0 & s < 0 holds
r * s < 0
proof end;

Lm23: for r, s, t being real number st r <= s holds
r - t <= s - t
by Lm5;

Lm24: for s, t being real number st s <= t holds
- t <= - s
proof end;

Lm25: for r, s being real number st r <= 0 & s >= 0 holds
r * s <= 0
proof end;

registration
cluster real positive -> non zero complex real non negative set ;
coherence
for b1 being real number st b1 is positive holds
( not b1 is negative & not b1 is empty )
proof end;
cluster non zero real non negative -> complex real positive set ;
coherence
for b1 being real number st not b1 is negative & not b1 is empty holds
b1 is positive
proof end;
cluster real negative -> non zero complex real non positive set ;
coherence
for b1 being real number st b1 is negative holds
( not b1 is positive & not b1 is empty )
proof end;
cluster non zero real non positive -> complex real negative set ;
coherence
for b1 being real number st not b1 is positive & not b1 is empty holds
b1 is negative
proof end;
cluster zero real -> complex real non positive non negative set ;
coherence
for b1 being real number st b1 is empty holds
( not b1 is negative & not b1 is positive )
proof end;
cluster real non positive non negative -> zero complex real set ;
coherence
for b1 being real number st not b1 is negative & not b1 is positive holds
b1 is empty
proof end;
end;

registration
cluster non zero complex real positive non negative set ;
existence
ex b1 being real number st b1 is positive
proof end;
cluster non zero complex real non positive negative set ;
existence
ex b1 being real number st b1 is negative
proof end;
cluster zero complex real non positive non negative set ;
existence
ex b1 being real number st b1 is empty
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

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

Lm26: for r being real number st r " = 0 holds
r = 0
proof end;

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

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

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

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

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