:: by Andrzej Trybulec

::

:: Received March 7, 1998

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

definition

{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+} is Subset-Family of RAT+
end;

func DEDEKIND_CUTS -> Subset-Family of RAT+ equals :: ARYTM_2:def 1

{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+};

coherence { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+};

{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+} is Subset-Family of RAT+

proof end;

:: deftheorem defines DEDEKIND_CUTS ARYTM_2:def 1 :

DEDEKIND_CUTS = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+};

DEDEKIND_CUTS = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+};

registration
end;

definition

(RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } is set ;

end;

func REAL+ -> set equals :: ARYTM_2:def 2

(RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;

coherence (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;

(RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } is set ;

:: deftheorem defines REAL+ ARYTM_2:def 2 :

REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;

REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;

set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } ;

set RA = { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;

Lm1: for x, y being object holds not [x,y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) }

proof end;

Lm2: RAT+ misses { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }

proof end;

RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) }

by XBOOLE_1:9;

then Lm3: REAL+ c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) }

;

REAL+ = RAT+ \/ (( { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } )

by Lm2, XBOOLE_1:87;

then Lm4: DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } c= REAL+

by XBOOLE_1:7;

Lm5: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_coprime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega

by XBOOLE_1:7;

definition

let x be Element of REAL+ ;

( ( x in RAT+ implies ex b_{1} being Element of DEDEKIND_CUTS ex r being Element of RAT+ st

( x = r & b_{1} = { s where s is Element of RAT+ : s < r } ) ) & ( not x in RAT+ implies ex b_{1} being Element of DEDEKIND_CUTS st b_{1} = x ) )

for b_{1}, b_{2} being Element of DEDEKIND_CUTS holds

( ( x in RAT+ & ex r being Element of RAT+ st

( x = r & b_{1} = { s where s is Element of RAT+ : s < r } ) & ex r being Element of RAT+ st

( x = r & b_{2} = { s where s is Element of RAT+ : s < r } ) implies b_{1} = b_{2} ) & ( not x in RAT+ & b_{1} = x & b_{2} = x implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Element of DEDEKIND_CUTS holds verum
;

end;
func DEDEKIND_CUT x -> Element of DEDEKIND_CUTS means :Def3: :: ARYTM_2:def 3

ex r being Element of RAT+ st

( x = r & it = { s where s is Element of RAT+ : s < r } ) if x in RAT+

otherwise it = x;

existence ex r being Element of RAT+ st

( x = r & it = { s where s is Element of RAT+ : s < r } ) if x in RAT+

otherwise it = x;

( ( x in RAT+ implies ex b

( x = r & b

proof end;

uniqueness for b

( ( x in RAT+ & ex r being Element of RAT+ st

( x = r & b

( x = r & b

consistency

for b

:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def 3 :

for x being Element of REAL+

for b_{2} being Element of DEDEKIND_CUTS holds

( ( x in RAT+ implies ( b_{2} = DEDEKIND_CUT x iff ex r being Element of RAT+ st

( x = r & b_{2} = { s where s is Element of RAT+ : s < r } ) ) ) & ( not x in RAT+ implies ( b_{2} = DEDEKIND_CUT x iff b_{2} = x ) ) );

for x being Element of REAL+

for b

( ( x in RAT+ implies ( b

( x = r & b

Lm6: for s, t being Element of RAT+ st ( for r being Element of RAT+ holds

( r < s iff r < t ) ) holds

s = t

proof end;

definition

let x be Element of DEDEKIND_CUTS ;

for b_{1}, b_{2} being Element of REAL+ holds

( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) & ex r being Element of RAT+ st

( b_{1} = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) & ex r being Element of RAT+ st

( b_{2} = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) implies b_{1} = b_{2} ) & ( ( for r being Element of RAT+ holds

not for s being Element of RAT+ holds

( s in x iff s < r ) ) & b_{1} = x & b_{2} = x implies b_{1} = b_{2} ) )

( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) implies ex b_{1} being Element of REAL+ ex r being Element of RAT+ st

( b_{1} = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) ) & ( ( for r being Element of RAT+ holds

not for s being Element of RAT+ holds

( s in x iff s < r ) ) implies ex b_{1} being Element of REAL+ st b_{1} = x ) )

for b_{1} being Element of REAL+ holds verum
;

end;
func GLUED x -> Element of REAL+ means :Def4: :: ARYTM_2:def 4

ex r being Element of RAT+ st

( it = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) if ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r )

otherwise it = x;

uniqueness ex r being Element of RAT+ st

( it = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) if ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r )

otherwise it = x;

for b

( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) & ex r being Element of RAT+ st

( b

( s in x iff s < r ) ) ) & ex r being Element of RAT+ st

( b

( s in x iff s < r ) ) ) implies b

not for s being Element of RAT+ holds

( s in x iff s < r ) ) & b

proof end;

existence ( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) implies ex b

( b

( s in x iff s < r ) ) ) ) & ( ( for r being Element of RAT+ holds

not for s being Element of RAT+ holds

( s in x iff s < r ) ) implies ex b

proof end;

consistency for b

:: deftheorem Def4 defines GLUED ARYTM_2:def 4 :

for x being Element of DEDEKIND_CUTS

for b_{2} being Element of REAL+ holds

( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) implies ( b_{2} = GLUED x iff ex r being Element of RAT+ st

( b_{2} = r & ( for s being Element of RAT+ holds

( s in x iff s < r ) ) ) ) ) & ( ( for r being Element of RAT+ holds

not for s being Element of RAT+ holds

( s in x iff s < r ) ) implies ( b_{2} = GLUED x iff b_{2} = x ) ) );

for x being Element of DEDEKIND_CUTS

for b

( ( ex r being Element of RAT+ st

for s being Element of RAT+ holds

( s in x iff s < r ) implies ( b

( b

( s in x iff s < r ) ) ) ) ) & ( ( for r being Element of RAT+ holds

not for s being Element of RAT+ holds

( s in x iff s < r ) ) implies ( b

Lm7: for r being Element of RAT+

for B being set st B in DEDEKIND_CUTS & r in B holds

ex s being Element of RAT+ st

( s in B & r < s )

proof end;

Lm8: {} in DEDEKIND_CUTS

proof end;

Lm9: DEDEKIND_CUTS /\ RAT+ = {{}}

proof end;

Lm10: for x being Element of REAL+ holds

( DEDEKIND_CUT x = {} iff x = {} )

proof end;

Lm11: for A being Element of DEDEKIND_CUTS holds

( GLUED A = {} iff A = {} )

proof end;

Lm12: for A being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED A) = A

proof end;

Lm13: for x, y being set st x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } & y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } & not x c= y holds

y c= x

proof end;

definition

let x, y be Element of REAL+ ;

( ( x in RAT+ & y in RAT+ & x in RAT+ & not y in RAT+ implies ( ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff x in y ) ) & ( x in RAT+ & y in RAT+ & not x in RAT+ & y in RAT+ implies ( ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff not y in x ) ) & ( x in RAT+ & not y in RAT+ & not x in RAT+ & y in RAT+ implies ( x in y iff not y in x ) ) ) ;

connectedness

for x, y being Element of REAL+ st ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) holds

( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )

end;
pred x <=' y means :Def5: :: ARYTM_2:def 5

ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) if ( x in RAT+ & y in RAT+ )

x in y if ( x in RAT+ & not y in RAT+ )

not y in x if ( not x in RAT+ & y in RAT+ )

otherwise x c= y;

consistency ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) if ( x in RAT+ & y in RAT+ )

x in y if ( x in RAT+ & not y in RAT+ )

not y in x if ( not x in RAT+ & y in RAT+ )

otherwise x c= y;

( ( x in RAT+ & y in RAT+ & x in RAT+ & not y in RAT+ implies ( ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff x in y ) ) & ( x in RAT+ & y in RAT+ & not x in RAT+ & y in RAT+ implies ( ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff not y in x ) ) & ( x in RAT+ & not y in RAT+ & not x in RAT+ & y in RAT+ implies ( x in y iff not y in x ) ) ) ;

connectedness

for x, y being Element of REAL+ st ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) holds

( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )

proof end;

:: deftheorem Def5 defines <=' ARYTM_2:def 5 :

for x, y being Element of REAL+ holds

( ( x in RAT+ & y in RAT+ implies ( x <=' y iff ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in RAT+ & not y in RAT+ implies ( x <=' y iff x in y ) ) & ( not x in RAT+ & y in RAT+ implies ( x <=' y iff not y in x ) ) & ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) implies ( x <=' y iff x c= y ) ) );

for x, y being Element of REAL+ holds

( ( x in RAT+ & y in RAT+ implies ( x <=' y iff ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in RAT+ & not y in RAT+ implies ( x <=' y iff x in y ) ) & ( not x in RAT+ & y in RAT+ implies ( x <=' y iff not y in x ) ) & ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) implies ( x <=' y iff x c= y ) ) );

Lm14: for x9, y9 being Element of RAT+

for x, y being Element of REAL+ st x = x9 & y = y9 holds

( x <=' y iff x9 <=' y9 )

proof end;

Lm15: for B being set st B in DEDEKIND_CUTS & B <> {} holds

ex r being Element of RAT+ st

( r in B & r <> {} )

proof end;

Lm16: for r, s being Element of RAT+

for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds

s in B

proof end;

Lm17: for B being set st B in DEDEKIND_CUTS & B <> {} holds

{} in B

proof end;

Lm18: for r being Element of RAT+

for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds

ex s being Element of RAT+ st

( not s in B & s < r )

proof end;

Lm19: for x being Element of REAL+ st DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } holds

x in RAT+

proof end;

Lm20: for x, y being Element of REAL+ st DEDEKIND_CUT x c= DEDEKIND_CUT y holds

x <=' y

proof end;

Lm21: for x, y being Element of REAL+ st x <=' y & y <=' x holds

x = y

proof end;

Lm22: for x, y being Element of REAL+ st DEDEKIND_CUT x = DEDEKIND_CUT y holds

x = y

proof end;

Lm23: for x being Element of REAL+ holds GLUED (DEDEKIND_CUT x) = x

proof end;

definition

let A, B be Element of DEDEKIND_CUTS ;

{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

for b_{1}, A, B being Element of DEDEKIND_CUTS st b_{1} = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds

b_{1} = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }

end;
func A + B -> Element of DEDEKIND_CUTS equals :Def6: :: ARYTM_2:def 6

{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

coherence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

proof end;

commutativity for b

b

proof end;

:: deftheorem Def6 defines + ARYTM_2:def 6 :

for A, B being Element of DEDEKIND_CUTS holds A + B = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

for A, B being Element of DEDEKIND_CUTS holds A + B = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

Lm24: for B being set st B in DEDEKIND_CUTS holds

ex r being Element of RAT+ st not r in B

proof end;

definition

let A, B be Element of DEDEKIND_CUTS ;

{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

for b_{1}, A, B being Element of DEDEKIND_CUTS st b_{1} = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds

b_{1} = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) }

end;
func A *' B -> Element of DEDEKIND_CUTS equals :: ARYTM_2:def 7

{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

coherence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

proof end;

commutativity for b

b

proof end;

:: deftheorem defines *' ARYTM_2:def 7 :

for A, B being Element of DEDEKIND_CUTS holds A *' B = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

for A, B being Element of DEDEKIND_CUTS holds A *' B = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;

definition

let x, y be Element of REAL+ ;

( ( y = {} implies x is Element of REAL+ ) & ( x = {} implies y is Element of REAL+ ) & ( not y = {} & not x = {} implies GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) is Element of REAL+ ) ) ;

consistency

for b_{1} being Element of REAL+ st y = {} & x = {} holds

( b_{1} = x iff b_{1} = y )
;

commutativity

for b_{1}, x, y being Element of REAL+ st ( y = {} implies b_{1} = x ) & ( x = {} implies b_{1} = y ) & ( not y = {} & not x = {} implies b_{1} = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) holds

( ( x = {} implies b_{1} = y ) & ( y = {} implies b_{1} = x ) & ( not x = {} & not y = {} implies b_{1} = GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT x)) ) )
;

GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) is Element of REAL+ ;

commutativity

for b_{1}, x, y being Element of REAL+ st b_{1} = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) holds

b_{1} = GLUED ((DEDEKIND_CUT y) *' (DEDEKIND_CUT x))
;

end;
func x + y -> Element of REAL+ equals :Def8: :: ARYTM_2:def 8

x if y = {}

y if x = {}

otherwise GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y));

coherence x if y = {}

y if x = {}

otherwise GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y));

( ( y = {} implies x is Element of REAL+ ) & ( x = {} implies y is Element of REAL+ ) & ( not y = {} & not x = {} implies GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) is Element of REAL+ ) ) ;

consistency

for b

( b

commutativity

for b

( ( x = {} implies b

func x *' y -> Element of REAL+ equals :: ARYTM_2:def 9

GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));

coherence GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));

GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) is Element of REAL+ ;

commutativity

for b

b

:: deftheorem Def8 defines + ARYTM_2:def 8 :

for x, y being Element of REAL+ holds

( ( y = {} implies x + y = x ) & ( x = {} implies x + y = y ) & ( not y = {} & not x = {} implies x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) );

for x, y being Element of REAL+ holds

( ( y = {} implies x + y = x ) & ( x = {} implies x + y = y ) & ( not y = {} & not x = {} implies x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) );

:: deftheorem defines *' ARYTM_2:def 9 :

for x, y being Element of REAL+ holds x *' y = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));

for x, y being Element of REAL+ holds x *' y = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));

Lm25: for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) c= (A + B) + C

proof end;

Lm26: for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) = (A + B) + C

by Lm25;

Lm27: for A, B being Element of DEDEKIND_CUTS holds

( not A + B = {} or A = {} or B = {} )

proof end;

theorem :: ARYTM_2:7

{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } is c=-linear

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } is c=-linear

proof end;

Lm28: for e being set st e in REAL+ holds

e <> RAT+

proof end;

Lm29: for r, s being Element of RAT+

for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } & r in B & s <=' r holds

s in B

proof end;

Lm30: for x, y being Element of REAL+ st y < x holds

ex z being Element of REAL+ st

( z in RAT+ & z < x & y < z )

proof end;

Lm31: for x, y, z being Element of REAL+ st x <=' y & y <=' z holds

x <=' z

proof end;

theorem :: ARYTM_2:8

for X, Y being Subset of REAL+ st ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds

x <=' y ) holds

ex z being Element of REAL+ st

for x, y being Element of REAL+ st x in X & y in Y holds

( x <=' z & z <=' y )

x <=' y ) holds

ex z being Element of REAL+ st

for x, y being Element of REAL+ st x in X & y in Y holds

( x <=' z & z <=' y )

proof end;

Lm32: one = 1

;

Lm33: {} = {}

;

Lm34: for A, B being Element of DEDEKIND_CUTS st A + B = A & A <> {} holds

B = {}

proof end;

Lm35: for x, y being Element of REAL+ st x + y = x holds

y = {}

proof end;

Lm36: for A, B being Element of DEDEKIND_CUTS st A <> {} & A c= B & A <> B holds

ex C being Element of DEDEKIND_CUTS st A + C = B

proof end;

Lm37: for x, y being Element of REAL+ st x <=' y holds

DEDEKIND_CUT x c= DEDEKIND_CUT y

proof end;

Lm38: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) c= (A *' B) *' C

proof end;

Lm39: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) = (A *' B) *' C

by Lm38;

Lm40: for x, y being Element of REAL+ holds

( not x *' y = {} or x = {} or y = {} )

proof end;

Lm41: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B + C) = (A *' B) + (A *' C)

proof end;

reconsider rone = one as Element of REAL+ by Th1;

Lm42: for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } & B <> {} holds

ex r being Element of RAT+ st

( r in B & r <> {} )

proof end;

Lm43: for A being Element of DEDEKIND_CUTS st A <> {} holds

ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone

proof end;

Lm44: for A, B being Element of DEDEKIND_CUTS st A = { r where r is Element of RAT+ : r < one } holds

A *' B = B

proof end;

Lm45: for i, j being Element of omega

for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds

i +^ j = x9 + y9

proof end;

Lm46: for x9, y9, z9 being Element of RAT+ st z9 < x9 + y9 & x9 <> {} & y9 <> {} holds

ex r, s being Element of RAT+ st

( z9 = r + s & r < x9 & s < y9 )

proof end;

Lm47: for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds

ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x + y = x9 + y9 )

proof end;

theorem :: ARYTM_2:17

for A being Subset of REAL+ st 0 in A & ( for x, y being Element of REAL+ st x in A & y = one holds

x + y in A ) holds

omega c= A

x + y in A ) holds

omega c= A

proof end;

theorem :: ARYTM_2:18

for x being Element of REAL+ st x in omega holds

for y being Element of REAL+ holds

( y in x iff ( y in omega & y <> x & y <=' x ) )

for y being Element of REAL+ holds

( y in x iff ( y in omega & y <> x & y <=' x ) )

proof end;

theorem :: ARYTM_2:21

for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds

ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x *' y = x9 *' y9 )

ex x9, y9 being Element of RAT+ st

( x = x9 & y = y9 & x *' y = x9 *' y9 )

proof end;