:: ARYTM_2 semantic presentation

definition

func DEDEKIND_CUTS -> Subset-Family of RAT+ equals :: ARYTM_2:def 1
{ b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) } \ {RAT+ };
coherence

proof end;

end;

:: deftheorem Def1 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 ) \ { { b₂ where B is Element of RAT+ : b₂ < b₁ } where B is Element of RAT+ : b₁ <> {} } ;
coherence ;

end;

:: deftheorem Def2 defines REAL+ ARYTM_2:def 2 :

set c₁ = { b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) } ;

set c₂ = { { b₂ where B is Element of RAT+ : b₂ < b₁ } where B is Element of RAT+ : b₁ <> {} } ;

Lemma1: for b₁, b₂ being set holds not [b₁,b₂] in { b₃ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₄ in b₃ holds
( ( for b₂ being Element of RAT+ st b₅ <=' b₄ holds
b₅ in b₃ ) & ex b₂ being Element of RAT+ st
( b₅ in b₃ & b₄ < b₅ ) ) }

proof end;

Lemma2: RAT+ c= RAT+ \/ DEDEKIND_CUTS
by XBOOLE_1:7;

Lemma3: RAT+ misses { { b₂ where B is Element of RAT+ : b₂ < b₁ } where B is Element of RAT+ : b₁ <> {} }

proof end;

theorem Th1: :: ARYTM_2:1

RAT+ c= REAL+ by Lemma2, Lemma3, XBOOLE_1:86;

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

DEDEKIND_CUTS c= { b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) }
by XBOOLE_1:36;

then RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) }
by XBOOLE_1:9;

then Lemma6: REAL+ c= RAT+ \/ { b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) }
by Lemma5, XBOOLE_1:1;

REAL+ = RAT+ \/ (({ b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) } \ {RAT+ }) \ { { b₂ where B is Element of RAT+ : b₂ < b₁ } where B is Element of RAT+ : b₁ <> {} } )
by Lemma3, XBOOLE_1:87;

then Lemma7: DEDEKIND_CUTS \ { { b₂ where B is Element of RAT+ : b₂ < b₁ } where B is Element of RAT+ : b₁ <> {} } 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 c₃ be Element of REAL+ ;
func DEDEKIND_CUT c₁ -> Element of DEDEKIND_CUTS means :Def3: :: ARYTM_2:def 3
ex b₁ being Element of RAT+ st
( a₁ = b₁ & a₂ = { b₂ where B is Element of RAT+ : b₂ < b₁ } ) if a₁ in RAT+
otherwise a₂ = a₁;
existence

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def 3 :

theorem Th3: :: ARYTM_2:3

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

proof end;

Lemma10: for b₁, b₂ being Element of RAT+ st ( for b₃ being Element of RAT+ holds
( b₃ < b₁ iff b₃ < b₂ ) ) holds
b₁ = b₂

proof end;

definition

let c₃ be Element of DEDEKIND_CUTS ;
func GLUED c₁ -> Element of REAL+ means :Def4: :: ARYTM_2:def 4
ex b₁ being Element of RAT+ st
( a₂ = b₁ & ( for b₂ being Element of RAT+ holds
( b₂ in a₁ iff b₂ < b₁ ) ) ) if ex b₁ being Element of RAT+ st
for b₂ being Element of RAT+ holds
( b₂ in a₁ iff b₂ < b₁ )
otherwise a₂ = a₁;
uniqueness

proof end;

existence

proof end;

consistency ;

end;

:: deftheorem Def4 defines GLUED ARYTM_2:def 4 :

Lemma12: for b₁ being Element of RAT+
for b₂ being set st b₂ in DEDEKIND_CUTS & b₁ in b₂ holds
ex b₃ being Element of RAT+ st
( b₃ in b₂ & b₁ < b₃ )

proof end;

Lemma13: {} in DEDEKIND_CUTS

proof end;

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

proof end;

Lemma15: for b₁ being Element of REAL+ holds
( DEDEKIND_CUT b₁ = {} iff b₁ = {} )

proof end;

Lemma16: for b₁ being Element of DEDEKIND_CUTS holds
( GLUED b₁ = {} iff b₁ = {} )

proof end;

Lemma17: for b₁ being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED b₁) = b₁

proof end;

Lemma18: for b₁, b₂ being set st b₁ in { b₃ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₄ in b₃ holds
( ( for b₂ being Element of RAT+ st b₅ <=' b₄ holds
b₅ in b₃ ) & ex b₂ being Element of RAT+ st
( b₅ in b₃ & b₄ < b₅ ) ) } & b₂ in { b₃ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₄ in b₃ holds
( ( for b₂ being Element of RAT+ st b₅ <=' b₄ holds
b₅ in b₃ ) & ex b₂ being Element of RAT+ st
( b₅ in b₃ & b₄ < b₅ ) ) } & not b₁ c= b₂ holds
b₂ c= b₁

proof end;

definition

let c₃, c₄ be Element of REAL+ ;
pred c₁ <=' c₂ means :Def5: :: ARYTM_2:def 5
ex b₁, b₂ being Element of RAT+ st
( a₁ = b₁ & a₂ = b₂ & b₁ <=' b₂ ) if ( a₁ in RAT+ & a₂ in RAT+ )
a₁ in a₂ if ( a₁ in RAT+ & not a₂ in RAT+ )
not a₂ in a₁ if ( not a₁ in RAT+ & a₂ in RAT+ )
otherwise a₁ c= a₂;
consistency ;
connectedness

proof end;

end;

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

notation

let c₃, c₄ be Element of REAL+ ;
antonym c₂ < c₁ for c₁ <=' c₂;

end;

Lemma20: for b₁, b₂ being Element of RAT+
for b₃, b₄ being Element of REAL+ st b₃ = b₁ & b₄ = b₂ holds
( b₃ <=' b₄ iff b₁ <=' b₂ )

proof end;

Lemma21: for b₁ being set st b₁ in DEDEKIND_CUTS & b₁ <> {} holds
ex b₂ being Element of RAT+ st
( b₂ in b₁ & b₂ <> {} )

proof end;

Lemma22: for b₁, b₂ being Element of RAT+
for b₃ being set st b₃ in DEDEKIND_CUTS & b₁ in b₃ & b₂ <=' b₁ holds
b₂ in b₃

proof end;

Lemma23: for b₁ being set st b₁ in DEDEKIND_CUTS & b₁ <> {} holds
{} in b₁

proof end;

Lemma24: for b₁ being Element of RAT+
for b₂ being set st b₂ in DEDEKIND_CUTS \ { { b₄ where B is Element of RAT+ : b₄ < b₃ } where B is Element of RAT+ : b₃ <> {} } & not b₁ in b₂ & b₂ <> {} holds
ex b₃ being Element of RAT+ st
( not b₃ in b₂ & b₃ < b₁ )

proof end;

Lemma25: for b₁ being Element of REAL+ st DEDEKIND_CUT b₁ in { { b₃ where B is Element of RAT+ : b₃ < b₂ } where B is Element of RAT+ : b₂ <> {} } holds
b₁ in RAT+

proof end;

Lemma26: for b₁, b₂ being Element of REAL+ st DEDEKIND_CUT b₁ c= DEDEKIND_CUT b₂ holds
b₁ <=' b₂

proof end;

Lemma27: for b₁, b₂ being Element of REAL+ st b₁ <=' b₂ & b₂ <=' b₁ holds
b₁ = b₂

proof end;

Lemma28: for b₁, b₂ being Element of REAL+ st DEDEKIND_CUT b₁ = DEDEKIND_CUT b₂ holds
b₁ = b₂

proof end;

Lemma29: for b₁ being Element of REAL+ holds GLUED (DEDEKIND_CUT b₁) = b₁

proof end;

definition

let c₃, c₄ be Element of DEDEKIND_CUTS ;
func c₁ + c₂ -> Element of DEDEKIND_CUTS equals :Def6: :: ARYTM_2:def 6
{ (b₁ + b₂) where B is Element of RAT+ , B is Element of RAT+ : ( b₁ in a₁ & b₂ in a₂ ) } ;
coherence

proof end;

commutativity

proof end;

end;

:: deftheorem Def6 defines + ARYTM_2:def 6 :

Lemma31: for b₁ being set st b₁ in DEDEKIND_CUTS holds
ex b₂ being Element of RAT+ st not b₂ in b₁

proof end;

definition

let c₃, c₄ be Element of DEDEKIND_CUTS ;
func c₁ *' c₂ -> Element of DEDEKIND_CUTS equals :: ARYTM_2:def 7
{ (b₁ *' b₂) where B is Element of RAT+ , B is Element of RAT+ : ( b₁ in a₁ & b₂ in a₂ ) } ;
coherence

proof end;

commutativity

proof end;

end;

:: deftheorem Def7 defines *' ARYTM_2:def 7 :

definition

let c₃, c₄ be Element of REAL+ ;
func c₁ + c₂ -> Element of REAL+ equals :Def8: :: ARYTM_2:def 8
a₁ if a₂ = {}
a₂ if a₁ = {}
otherwise GLUED ((DEDEKIND_CUT a₁) + (DEDEKIND_CUT a₂));
coherence ;
consistency ;
commutativity ;
func c₁ *' c₂ -> Element of REAL+ equals :: ARYTM_2:def 9
GLUED ((DEDEKIND_CUT a₁) *' (DEDEKIND_CUT a₂));
coherence ;
commutativity ;

end;

:: deftheorem Def8 defines + ARYTM_2:def 8 :

:: deftheorem Def9 defines *' ARYTM_2:def 9 :

theorem Th4: :: ARYTM_2:4

for b₁, b₂ being Element of REAL+ st b₁ = {} holds
b₁ *' b₂ = {}

proof end;

theorem Th5: :: ARYTM_2:5

canceled;

theorem Th6: :: ARYTM_2:6

for b₁, b₂ being Element of REAL+ st b₁ + b₂ = {} holds
b₁ = {}

proof end;

Lemma35: for b₁, b₂, b₃ being Element of DEDEKIND_CUTS holds b₁ + (b₂ + b₃) c= (b₁ + b₂) + b₃

proof end;

Lemma36: for b₁, b₂, b₃ being Element of DEDEKIND_CUTS holds b₁ + (b₂ + b₃) = (b₁ + b₂) + b₃

proof end;

Lemma37: for b₁, b₂ being Element of DEDEKIND_CUTS holds
( not b₁ + b₂ = {} or b₁ = {} or b₂ = {} )

proof end;

theorem Th7: :: ARYTM_2:7

for b₁, b₂, b₃ being Element of REAL+ holds b₁ + (b₂ + b₃) = (b₁ + b₂) + b₃

proof end;

theorem Th8: :: ARYTM_2:8

{ b₁ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₂ in b₁ holds
( ( for b₂ being Element of RAT+ st b₃ <=' b₂ holds
b₃ in b₁ ) & ex b₂ being Element of RAT+ st
( b₃ in b₁ & b₂ < b₃ ) ) } is c=-linear

proof end;

Lemma39: for b₁ being set st b₁ in REAL+ holds
b₁ <> RAT+

proof end;

Lemma40: for b₁, b₂ being Element of RAT+
for b₃ being set st b₃ in { b₄ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₅ in b₄ holds
( ( for b₂ being Element of RAT+ st b₆ <=' b₅ holds
b₆ in b₄ ) & ex b₂ being Element of RAT+ st
( b₆ in b₄ & b₅ < b₆ ) ) } & b₁ in b₃ & b₂ <=' b₁ holds
b₂ in b₃

proof end;

Lemma41: for b₁, b₂ being Element of REAL+ st b₁ < b₂ holds
ex b₃ being Element of REAL+ st
( b₃ in RAT+ & b₃ < b₂ & b₁ < b₃ )

proof end;

Lemma42: for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₂ <=' b₃ holds
b₁ <=' b₃

proof end;

theorem Th9: :: ARYTM_2:9

for b₁, b₂ being Subset of REAL+ st ex b₃ being Element of REAL+ st b₃ in b₁ & ex b₃ being Element of REAL+ st b₃ in b₂ & ( for b₃, b₄ being Element of REAL+ st b₃ in b₁ & b₄ in b₂ holds
b₃ <=' b₄ ) holds
ex b₃ being Element of REAL+ st
for b₄, b₅ being Element of REAL+ st b₄ in b₁ & b₅ in b₂ holds
( b₄ <=' b₃ & b₃ <=' b₅ )

proof end;

Lemma43: one = one
;

Lemma44: {} = {}
;

Lemma45: for b₁, b₂ being Element of DEDEKIND_CUTS st b₁ + b₂ = b₁ & b₁ <> {} holds
b₂ = {}

proof end;

Lemma46: for b₁, b₂ being Element of REAL+ st b₁ + b₂ = b₁ holds
b₂ = {}

proof end;

Lemma47: for b₁, b₂ being Element of DEDEKIND_CUTS st b₁ <> {} & b₁ c= b₂ & b₁ <> b₂ holds
ex b₃ being Element of DEDEKIND_CUTS st b₁ + b₃ = b₂

proof end;

Lemma48: for b₁, b₂ being Element of REAL+ st b₁ <=' b₂ holds
DEDEKIND_CUT b₁ c= DEDEKIND_CUT b₂

proof end;

theorem Th10: :: ARYTM_2:10

for b₁, b₂ being Element of REAL+ st b₁ <=' b₂ holds
ex b₃ being Element of REAL+ st b₁ + b₃ = b₂

proof end;

theorem Th11: :: ARYTM_2:11

for b₁, b₂ being Element of REAL+ ex b₃ being Element of REAL+ st
( b₁ + b₃ = b₂ or b₂ + b₃ = b₁ )

proof end;

theorem Th12: :: ARYTM_2:12

for b₁, b₂, b₃ being Element of REAL+ st b₁ + b₂ = b₁ + b₃ holds
b₂ = b₃

proof end;

Lemma52: for b₁, b₂, b₃ being Element of DEDEKIND_CUTS holds b₁ *' (b₂ *' b₃) c= (b₁ *' b₂) *' b₃

proof end;

Lemma53: for b₁, b₂, b₃ being Element of DEDEKIND_CUTS holds b₁ *' (b₂ *' b₃) = (b₁ *' b₂) *' b₃

proof end;

theorem Th13: :: ARYTM_2:13

for b₁, b₂, b₃ being Element of REAL+ holds b₁ *' (b₂ *' b₃) = (b₁ *' b₂) *' b₃

proof end;

Lemma54: for b₁, b₂ being Element of REAL+ holds
( not b₁ *' b₂ = {} or b₁ = {} or b₂ = {} )

proof end;

Lemma55: for b₁, b₂, b₃ being Element of DEDEKIND_CUTS holds b₁ *' (b₂ + b₃) = (b₁ *' b₂) + (b₁ *' b₃)

proof end;

theorem Th14: :: ARYTM_2:14

for b₁, b₂, b₃ being Element of REAL+ holds b₁ *' (b₂ + b₃) = (b₁ *' b₂) + (b₁ *' b₃)

proof end;

one in RAT+
;

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

Lemma56: for b₁ being set st b₁ in { b₂ where B is Subset of RAT+ : for b₁ being Element of RAT+ st b₃ in b₂ holds
( ( for b₂ being Element of RAT+ st b₄ <=' b₃ holds
b₄ in b₂ ) & ex b₂ being Element of RAT+ st
( b₄ in b₂ & b₃ < b₄ ) ) } & b₁ <> {} holds
ex b₂ being Element of RAT+ st
( b₂ in b₁ & b₂ <> {} )

proof end;

Lemma57: for b₁ being Element of DEDEKIND_CUTS st b₁ <> {} holds
ex b₂ being Element of DEDEKIND_CUTS st b₁ *' b₂ = DEDEKIND_CUT c₃

proof end;

theorem Th15: :: ARYTM_2:15

for b₁ being Element of REAL+ st b₁ <> {} holds
ex b₂ being Element of REAL+ st b₁ *' b₂ = one

proof end;

Lemma58: for b₁, b₂ being Element of DEDEKIND_CUTS st b₁ = { b₃ where B is Element of RAT+ : b₃ < one } holds
b₁ *' b₂ = b₂

proof end;

theorem Th16: :: ARYTM_2:16

for b₁, b₂ being Element of REAL+ st b₁ = one holds
b₁ *' b₂ = b₂

proof end;

Lemma59: for b₁, b₂ being Element of omega
for b₃, b₄ being Element of RAT+ st b₁ = b₃ & b₂ = b₄ holds
b₁ +^ b₂ = b₃ + b₄

proof end;

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

Lemma60: for b₁, b₂, b₃ being Element of RAT+ st b₁ < b₂ + b₃ & b₂ <> {} & b₃ <> {} holds
ex b₄, b₅ being Element of RAT+ st
( b₁ = b₄ + b₅ & b₄ < b₂ & b₅ < b₃ )

proof end;

Lemma61: for b₁, b₂ being Element of REAL+ st b₁ in RAT+ & b₂ in RAT+ holds
ex b₃, b₄ being Element of RAT+ st
( b₁ = b₃ & b₂ = b₄ & b₁ + b₂ = b₃ + b₄ )

proof end;

theorem Th17: :: ARYTM_2:17

for b₁, b₂ being Element of REAL+ st b₁ in omega & b₂ in omega holds
b₂ + b₁ in omega

proof end;

theorem Th18: :: ARYTM_2:18

for b₁ being Subset of REAL+ st {} in b₁ & ( for b₂, b₃ being Element of REAL+ st b₂ in b₁ & b₃ = one holds
b₂ + b₃ in b₁ ) holds
omega c= b₁

proof end;

theorem Th19: :: ARYTM_2:19

for b₁ being Element of REAL+ st b₁ in omega holds
for b₂ being Element of REAL+ holds
( b₂ in b₁ iff ( b₂ in omega & b₂ <> b₁ & b₂ <=' b₁ ) )

proof end;

theorem Th20: :: ARYTM_2:20

for b₁, b₂, b₃ being Element of REAL+ st b₁ = b₂ + b₃ holds
b₃ <=' b₁

proof end;

theorem Th21: :: ARYTM_2:21

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

proof end;

theorem Th22: :: ARYTM_2:22

for b₁, b₂ being Element of REAL+ st b₁ in RAT+ & b₂ in RAT+ holds
ex b₃, b₄ being Element of RAT+ st
( b₁ = b₃ & b₂ = b₄ & b₁ *' b₂ = b₃ *' b₄ )

proof end;