:: ARYTM_2 semantic presentation

definition

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

proof end;

end;

:: deftheorem defines DEDEKIND_CUTS ARYTM_2:def 1 :

registration

cluster DEDEKIND_CUTS -> non empty ;
coherence

proof end;

end;

definition

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 ;

end;

:: deftheorem defines REAL+ ARYTM_2:def 2 :

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 set 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+ c= RAT+ \/ DEDEKIND_CUTS
by XBOOLE_1:7;

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

proof end;

theorem Th1: :: ARYTM_2:1

RAT+ c= REAL+ by Lm2, Lm3, XBOOLE_1:86;

Lm4: REAL+ c= RAT+ \/ DEDEKIND_CUTS
by XBOOLE_1:36;

DEDEKIND_CUTS c= { 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:36;

then 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 Lm5: 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 ) ) }
by Lm4, XBOOLE_1:1;

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 Lm3, XBOOLE_1:87;

then Lm6: DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } c= REAL+
by XBOOLE_1:7;

theorem Th2: :: ARYTM_2:2

omega c= REAL+ by Th1, ARYTM_3:34, XBOOLE_1:1;

registration

cluster REAL+ -> non empty ;
coherence by Th2, ORDINAL2:19;

end;

definition

let x be Element of REAL+ ;
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

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def 3 :

theorem :: ARYTM_2:3

for y being set holds not [{} ,y] in REAL+

proof end;

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

proof end;

existence

proof end;

consistency ;

end;

:: deftheorem Def4 defines GLUED ARYTM_2:def 4 :

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

Lm9: {} in DEDEKIND_CUTS

proof end;

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

proof end;

Lm11: for x being Element of REAL+ holds
( DEDEKIND_CUT x = {} iff x = {} )

proof end;

Lm12: for A being Element of DEDEKIND_CUTS holds
( GLUED A = {} iff A = {} )

proof end;

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

proof end;

Lm14: 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+ ;
pred x <=' y means :Def5: :: ARYTM_2:def 5
ex x', y' being Element of RAT+ st
( x = x' & y = y' & x' <=' y' ) 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 ;
connectedness

proof end;

end;

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

notation

let x, y be Element of REAL+ ;
antonym y < x for x <=' y;

end;

Lm15: for x', y' being Element of RAT+
for x, y being Element of REAL+ st x = x' & y = y' holds
( x <=' y iff x' <=' y' )

proof end;

Lm16: for B being set st B in DEDEKIND_CUTS & B <> {} holds
ex r being Element of RAT+ st
( r in B & r <> {} )

proof end;

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

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

proof end;

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

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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let A, B be Element of DEDEKIND_CUTS ;
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

proof end;

commutativity

proof end;

end;

:: deftheorem Def6 defines + ARYTM_2:def 6 :

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

proof end;

commutativity

proof end;

end;

:: deftheorem defines *' ARYTM_2:def 7 :

definition

let x, y be Element of REAL+ ;
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 ;
consistency ;
commutativity ;
func x *' y -> Element of REAL+ equals :: ARYTM_2:def 9
GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));
coherence ;
commutativity ;

end;

:: deftheorem Def8 defines + ARYTM_2:def 8 :

:: deftheorem defines *' ARYTM_2:def 9 :

theorem Th4: :: ARYTM_2:4

for x, y being Element of REAL+ st x = {} holds
x *' y = {}

proof end;

theorem :: ARYTM_2:5

canceled;

theorem Th6: :: ARYTM_2:6

for x, y being Element of REAL+ st x + y = {} holds
x = {}

proof end;

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

proof end;

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

proof end;

Lm28: for A, B being Element of DEDEKIND_CUTS holds
( not A + B = {} or A = {} or B = {} )

proof end;

theorem Th7: :: ARYTM_2:7

for x, y, z being Element of REAL+ holds x + (y + z) = (x + y) + z

proof end;

theorem :: ARYTM_2:8

{ 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

proof end;

Lm29: for e being set st e in REAL+ holds
e <> RAT+

proof end;

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

Lm31: for y, x being Element of REAL+ st y < x holds
ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

proof end;

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

proof end;

theorem :: ARYTM_2:9

for X, Y being Subset of REAL+ st ex x being Element of REAL+ st x in X & 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 )

proof end;

Lm33: one = one
;

Lm34: {} = {}
;

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

proof end;

Lm36: for x, y being Element of REAL+ st x + y = x holds
y = {}

proof end;

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

Lm38: for x, y being Element of REAL+ st x <=' y holds
DEDEKIND_CUT x c= DEDEKIND_CUT y

proof end;

theorem Th10: :: ARYTM_2:10

for x, y being Element of REAL+ st x <=' y holds
ex z being Element of REAL+ st x + z = y

proof end;

theorem Th11: :: ARYTM_2:11

for x, y being Element of REAL+ ex z being Element of REAL+ st
( x + z = y or y + z = x )

proof end;

theorem Th12: :: ARYTM_2:12

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

proof end;

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

proof end;

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

proof end;

theorem :: ARYTM_2:13

for x, y, z being Element of REAL+ holds x *' (y *' z) = (x *' y) *' z

proof end;

Lm41: for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )

proof end;

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

proof end;

theorem :: ARYTM_2:14

for x, y, z being Element of REAL+ holds x *' (y + z) = (x *' y) + (x *' z)

proof end;

one in RAT+
;

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

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

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

theorem :: ARYTM_2:15

for x being Element of REAL+ st x <> {} holds
ex y being Element of REAL+ st x *' y = one

proof end;

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

theorem :: ARYTM_2:16

for x, y being Element of REAL+ st x = one holds
x *' y = y

proof end;

Lm46: for i, j being Element of omega
for x', y' being Element of RAT+ st i = x' & j = y' holds
i +^ j = x' + y'

proof end;

reconsider one' = one as Element of omega by ORDINAL2:def 21;

Lm47: for z', x', y' being Element of RAT+ st z' < x' + y' & x' <> {} & y' <> {} holds
ex r, s being Element of RAT+ st
( z' = r + s & r < x' & s < y' )

proof end;

Lm48: for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds
ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )

proof end;

theorem :: ARYTM_2:17

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

proof end;

theorem :: ARYTM_2:18

for A being Subset of REAL+ st {} in A & ( for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ) holds
omega c= A

proof end;

theorem :: ARYTM_2:19

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

proof end;

theorem :: ARYTM_2:20

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

proof end;

theorem :: ARYTM_2:21

( {} in REAL+ & one in REAL+ )

proof end;

theorem :: ARYTM_2:22

for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds
ex x', y' being Element of RAT+ st
( x = x' & y = y' & x *' y = x' *' y' )

proof end;