:: XREAL_0 semantic presentation

definition

let c₁ be number ;
attr a₁ is real means :Def1: :: XREAL_0:def 1
a₁ in REAL ;

end;

:: deftheorem Def1 defines real XREAL_0:def 1 :

registration

cluster natural -> real set ;
coherence

proof end;

cluster real -> complex set ;
coherence

proof end;

end;

registration

cluster complex real set ;
existence

proof end;

end;

definition

let c₁, c₂ be real number ;
pred c₁ <= c₂ means :Def2: :: XREAL_0:def 2
ex b₁, b₂ being Element of REAL+ st
( a₁ = b₁ & a₂ = b₂ & b₁ <=' b₂ ) if ( a₁ in REAL+ & a₂ in REAL+ )
ex b₁, b₂ being Element of REAL+ st
( a₁ = [0,b₁] & a₂ = [0,b₂] & b₂ <=' b₁ ) if ( a₁ in [:{0},REAL+ :] & a₂ in [:{0},REAL+ :] )
otherwise ( a₂ in REAL+ & a₁ in [:{0},REAL+ :] );
consistency by ARYTM_0:5, XBOOLE_0:3;
reflexivity

proof end;

connectedness

proof end;

end;

:: deftheorem Def2 defines <= XREAL_0:def 2 :

notation

let c₁, c₂ be real number ;
synonym c₂ >= c₁ for c₁ <= c₂;
antonym c₂ < c₁ for c₁ <= c₂;
antonym c₁ > c₂ for c₁ <= c₂;

end;

definition

let c₁ be real number ;
attr a₁ is positive means :Def3: :: XREAL_0:def 3
a₁ > 0;
attr a₁ is negative means :Def4: :: XREAL_0:def 4
a₁ < 0;

end;

:: deftheorem Def3 defines positive XREAL_0:def 3 :

:: deftheorem Def4 defines negative XREAL_0:def 4 :

Lemma5: for b₁ being real number
for b₂, b₃ being Element of REAL st b₁ = [*b₂,b₃*] holds
( b₃ = 0 & b₁ = b₂ )

proof end;

registration

let c₁ be real number ;
cluster - a₁ -> real ;
coherence

proof end;

cluster a₁ " -> real ;
coherence

proof end;

let c₂ be real number ;
cluster a₁ + a₂ -> real ;
coherence

proof end;

cluster a₁ * a₂ -> real ;
coherence

proof end;

end;

registration

let c₁, c₂ be real number ;
cluster a₁ - a₂ -> real ;
coherence ;
cluster a₁ / a₂ -> real ;
coherence ;

end;

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

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

Lemma8: for b₁, b₂ being real number st b₁ <= b₂ & b₂ <= b₁ holds
b₁ = b₂

proof end;

Lemma9: for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
b₁ + b₃ <= b₂ + b₃

proof end;

Lemma10: for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
b₁ <= b₃

proof end;

reconsider c₁ = 0 as Element of REAL+ by ARYTM_2:21;

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

reconsider c₂ = 1 as Element of REAL+ by Lemma6, ARYTM_2:21;

c₁ <=' c₂
by ARYTM_1:6;

then Lemma12: 0 <= 1
by Def2;

1 + (- 1) = 0
;

then consider c₃, c₄, c₅, c₆ being Element of REAL such that
Lemma13: 1 = [*c₃,c₄*] and
Lemma14: - 1 = [*c₅,c₆*] and
Lemma15: 0 = [*(+ c₃,c₅),(+ c₄,c₆)*] by XCMPLX_0:def 4;

Lemma16: c₃ = 1
by Lemma5, Lemma13;

Lemma17: c₅ = - 1
by Lemma5, Lemma14;

Lemma18: + c₃,c₅ = 0
by Lemma5, Lemma15;

E19: now

assume - 1 in REAL+ ;
then ex b₁, b₂ being Element of REAL+ st
( c₃ = b₁ & c₅ = b₂ & c₁ = b₁ + b₂ ) by Lemma6, Lemma16, Lemma17, Lemma18, ARYTM_0:def 2, ARYTM_2:21;
hence contradiction by Lemma16, ARYTM_2:6;

end;

Lemma20: for b₁, b₂ being real number st b₁ >= 0 & b₂ > 0 holds
b₁ + b₂ > 0

proof end;

Lemma21: for b₁, b₂ being real number st b₁ <= 0 & b₂ < 0 holds
b₁ + b₂ < 0

proof end;

reconsider c₇ = 0 as Element of REAL+ by ARYTM_2:21;

Lemma22: for b₁, b₂, b₃ being real number st b₁ <= b₂ & 0 <= b₃ holds
b₁ * b₃ <= b₂ * b₃

proof end;

Lemma23: for b₁, b₂, b₃ being real number holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)
;

Lemma24: for b₁, b₂ being real number holds
( not b₁ * b₂ = 0 or b₁ = 0 or b₂ = 0 )

proof end;

Lemma25: for b₁, b₂ being real number st b₁ > 0 & b₂ > 0 holds
b₁ * b₂ > 0

proof end;

Lemma26: for b₁, b₂ being real number st b₁ > 0 & b₂ < 0 holds
b₁ * b₂ < 0

proof end;

Lemma27: for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
b₁ - b₃ <= b₂ - b₃
by Lemma9;

Lemma28: for b₁, b₂ being real number st b₁ <= b₂ holds
- b₂ <= - b₁

proof end;

Lemma29: for b₁, b₂ being real number st b₁ <= 0 & b₂ >= 0 holds
b₁ * b₂ <= 0

proof end;

registration

cluster real positive -> non zero complex real non negative set ;
coherence

proof end;

cluster non zero real non negative -> complex real positive set ;
coherence

proof end;

cluster real negative -> non zero complex real non positive set ;
coherence

proof end;

cluster non zero real non positive -> complex real negative set ;
coherence

proof end;

cluster zero real -> complex real non positive non negative set ;
coherence

proof end;

cluster real non positive non negative -> zero complex real set ;
coherence

proof end;

end;

registration

cluster non zero complex real positive non negative set ;
existence

proof end;

cluster non zero complex real non positive negative set ;
existence

proof end;

cluster zero complex real non positive non negative set ;
existence

proof end;

end;

registration

let c₈, c₉ be real non negative number ;
cluster a₁ + a₂ -> real non negative ;
coherence

proof end;

end;

registration

let c₈, c₉ be real non positive number ;
cluster a₁ + a₂ -> real non positive ;
coherence

proof end;

end;

registration

let c₈ be real positive number ;
let c₉ be real non negative number ;
cluster a₁ + a₂ -> non zero real positive non negative ;
coherence

proof end;

cluster a₂ + a₁ -> non zero real positive non negative ;
coherence ;

end;

registration

let c₈ be real negative number ;
let c₉ be real non positive number ;
cluster a₁ + a₂ -> non zero real non positive negative ;
coherence

proof end;

cluster a₂ + a₁ -> non zero real non positive negative ;
coherence ;

end;

registration

let c₈ be real non positive number ;
cluster - a₁ -> real non negative ;
coherence

proof end;

end;

registration

let c₈ be real non negative number ;
cluster - a₁ -> real non positive ;
coherence

proof end;

end;

registration

let c₈ be real non negative number ;
let c₉ be real non positive number ;
cluster a₁ - a₂ -> real non negative ;
coherence ;
cluster a₂ - a₁ -> real non positive ;
coherence ;

end;

registration

let c₈ be real positive number ;
let c₉ be real non positive number ;
cluster a₁ - a₂ -> non zero real positive non negative ;
coherence ;
cluster a₂ - a₁ -> non zero real non positive negative ;
coherence ;

end;

registration

let c₈ be real negative number ;
let c₉ be real non negative number ;
cluster a₁ - a₂ -> non zero real non positive negative ;
coherence ;
cluster a₂ - a₁ -> non zero real positive non negative ;
coherence ;

end;

registration

let c₈ be real non positive number ;
let c₉ be real non negative number ;
cluster a₁ * a₂ -> real non positive ;
coherence

proof end;

cluster a₂ * a₁ -> real non positive ;
coherence ;

end;

registration

let c₈, c₉ be real non positive number ;
cluster a₁ * a₂ -> real non negative ;
coherence

proof end;

end;

registration

let c₈, c₉ be real non negative number ;
cluster a₁ * a₂ -> real non negative ;
coherence

proof end;

end;

Lemma30: for b₁ being real number st b₁ " = 0 holds
b₁ = 0

proof end;

registration

let c₈ be real non positive number ;
cluster a₁ " -> real non positive ;
coherence

proof end;

end;

registration

let c₈ be real non negative number ;
cluster a₁ " -> real non negative ;
coherence

proof end;

end;

registration

let c₈ be real non negative number ;
let c₉ be real non positive number ;
cluster a₁ / a₂ -> real non positive ;
coherence ;
cluster a₂ / a₁ -> real non positive ;
coherence ;

end;

registration

let c₈, c₉ be real non negative number ;
cluster a₁ / a₂ -> real non negative ;
coherence ;

end;

registration

let c₈, c₉ be real non positive number ;
cluster a₁ / a₂ -> real non negative ;
coherence ;

end;