:: ARYTM_3 semantic presentation

Lemma1: one in omega
by ORDINAL1:41, ORDINAL2:19;

registration

let c₁ be Ordinal;
cluster -> ordinal Element of a₁;
coherence

proof end;

end;

registration

cluster empty -> natural set ;
coherence by ORDINAL2:19, ORDINAL2:def 21;
cluster one -> natural ;
coherence by Lemma1, ORDINAL2:def 21;
cluster -> ordinal natural Element of omega ;
coherence by ORDINAL2:def 21;

end;

registration

cluster non empty natural set ;
existence

proof end;

end;

registration

let c₁ be natural Ordinal;
cluster succ a₁ -> natural ;
coherence

proof end;

end;

scheme :: ARYTM_3:sch 1
s1{ P₁[ set ] } :

for b₁ being natural Ordinal holds P₁[b₁]

provided

E2: P₁[ {} ] and
E3: for b₁ being natural Ordinal st P₁[b₁] holds
P₁[ succ b₁]

proof end;

registration

let c₁, c₂ be natural Ordinal;
cluster a₁ +^ a₂ -> natural ;
coherence

proof end;

end;

theorem Th1: :: ARYTM_3:1

for b₁, b₂ being Ordinal st b₁ +^ b₂ is natural holds
( b₁ in omega & b₂ in omega )

proof end;

registration

let c₁, c₂ be natural Ordinal;
cluster a₁ -^ a₂ -> natural ;
coherence

proof end;

cluster a₁ *^ a₂ -> natural ;
coherence

proof end;

end;

theorem Th2: :: ARYTM_3:2

for b₁, b₂ being Ordinal st b₁ *^ b₂ is natural & not b₁ *^ b₂ is empty holds
( b₁ in omega & b₂ in omega )

proof end;

theorem Th3: :: ARYTM_3:3

for b₁, b₂ being natural Ordinal holds b₁ +^ b₂ = b₂ +^ b₁

proof end;

theorem Th4: :: ARYTM_3:4

for b₁, b₂ being natural Ordinal holds b₁ *^ b₂ = b₂ *^ b₁

proof end;

definition

let c₁, c₂ be natural Ordinal;
redefine func +^ as c₁ +^ c₂ -> set ;
commutativity by Th3;
redefine func *^ as c₁ *^ c₂ -> set ;
commutativity by Th4;

end;

definition

let c₁, c₂ be Ordinal;
pred c₁,c₂ are_relative_prime means :Def1: :: ARYTM_3:def 1
for b₁, b₂, b₃ being Ordinal st a₁ = b₁ *^ b₂ & a₂ = b₁ *^ b₃ holds
b₁ = one ;
symmetry ;

end;

:: deftheorem Def1 defines are_relative_prime ARYTM_3:def 1 :

theorem Th5: :: ARYTM_3:5

not {} , {} are_relative_prime

proof end;

theorem Th6: :: ARYTM_3:6

for b₁ being Ordinal holds one ,b₁ are_relative_prime

proof end;

theorem Th7: :: ARYTM_3:7

for b₁ being Ordinal st {} ,b₁ are_relative_prime holds
b₁ = one

proof end;

defpred S₁[ set ] means ex b₁ being Ordinal st
( b₁ c= a₁ & a₁ in omega & a₁ <> {} & ( for b₂, b₃, b₄ being natural Ordinal holds
( not b₃,b₄ are_relative_prime or not a₁ = b₂ *^ b₃ or not b₁ = b₂ *^ b₄ ) ) );

theorem Th8: :: ARYTM_3:8

for b₁, b₂ being natural Ordinal st ( b₁ <> {} or b₂ <> {} ) holds
ex b₃, b₄, b₅ being natural Ordinal st
( b₄,b₅ are_relative_prime & b₁ = b₃ *^ b₄ & b₂ = b₃ *^ b₅ )

proof end;

registration

let c₁, c₂ be natural Ordinal;
cluster a₁ div^ a₂ -> natural ;
coherence

proof end;

cluster a₁ mod^ a₂ -> natural ;
coherence

proof end;

end;

definition

let c₁, c₂ be Ordinal;
pred c₁ divides c₂ means :Def2: :: ARYTM_3:def 2
ex b₁ being Ordinal st a₂ = a₁ *^ b₁;
reflexivity

proof end;

end;

:: deftheorem Def2 defines divides ARYTM_3:def 2 :

theorem Th9: :: ARYTM_3:9

for b₁, b₂ being natural Ordinal holds
( b₁ divides b₂ iff ex b₃ being natural Ordinal st b₂ = b₁ *^ b₃ )

proof end;

theorem Th10: :: ARYTM_3:10

for b₁, b₂ being natural Ordinal st {} in b₁ holds
b₂ mod^ b₁ in b₁

proof end;

theorem Th11: :: ARYTM_3:11

for b₁, b₂ being natural Ordinal holds
( b₂ divides b₁ iff b₁ = b₂ *^ (b₁ div^ b₂) )

proof end;

theorem Th12: :: ARYTM_3:12

canceled;

theorem Th13: :: ARYTM_3:13

for b₁, b₂ being natural Ordinal st b₁ divides b₂ & b₂ divides b₁ holds
b₁ = b₂

proof end;

theorem Th14: :: ARYTM_3:14

for b₁ being natural Ordinal holds
( b₁ divides {} & one divides b₁ )

proof end;

theorem Th15: :: ARYTM_3:15

for b₁, b₂ being natural Ordinal st {} in b₂ & b₁ divides b₂ holds
b₁ c= b₂

proof end;

theorem Th16: :: ARYTM_3:16

for b₁, b₂, b₃ being natural Ordinal st b₁ divides b₂ & b₁ divides b₂ +^ b₃ holds
b₁ divides b₃

proof end;

definition

let c₁, c₂ be natural Ordinal;
func c₁ lcm c₂ -> Element of omega means :Def3: :: ARYTM_3:def 3
( a₁ divides a₃ & a₂ divides a₃ & ( for b₁ being natural Ordinal st a₁ divides b₁ & a₂ divides b₁ holds
a₃ divides b₁ ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines lcm ARYTM_3:def 3 :

theorem Th17: :: ARYTM_3:17

for b₁, b₂ being natural Ordinal holds b₁ lcm b₂ divides b₁ *^ b₂

proof end;

theorem Th18: :: ARYTM_3:18

for b₁, b₂ being natural Ordinal st b₁ <> {} holds
(b₂ *^ b₁) div^ (b₂ lcm b₁) divides b₂

proof end;

definition

let c₁, c₂ be natural Ordinal;
func c₁ hcf c₂ -> Element of omega means :Def4: :: ARYTM_3:def 4
( a₃ divides a₁ & a₃ divides a₂ & ( for b₁ being natural Ordinal st b₁ divides a₁ & b₁ divides a₂ holds
b₁ divides a₃ ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def4 defines hcf ARYTM_3:def 4 :

theorem Th19: :: ARYTM_3:19

for b₁ being natural Ordinal holds
( b₁ hcf {} = b₁ & b₁ lcm {} = {} )

proof end;

theorem Th20: :: ARYTM_3:20

for b₁, b₂ being natural Ordinal st b₁ hcf b₂ = {} holds
b₁ = {}

proof end;

theorem Th21: :: ARYTM_3:21

for b₁ being natural Ordinal holds
( b₁ hcf b₁ = b₁ & b₁ lcm b₁ = b₁ )

proof end;

theorem Th22: :: ARYTM_3:22

for b₁, b₂, b₃ being natural Ordinal holds (b₁ *^ b₂) hcf (b₃ *^ b₂) = (b₁ hcf b₃) *^ b₂

proof end;

theorem Th23: :: ARYTM_3:23

for b₁, b₂ being natural Ordinal st b₁ <> {} holds
( b₂ hcf b₁ <> {} & b₁ div^ (b₂ hcf b₁) <> {} )

proof end;

theorem Th24: :: ARYTM_3:24

for b₁, b₂ being natural Ordinal st ( b₁ <> {} or b₂ <> {} ) holds
b₁ div^ (b₁ hcf b₂),b₂ div^ (b₁ hcf b₂) are_relative_prime

proof end;

theorem Th25: :: ARYTM_3:25

for b₁, b₂ being natural Ordinal holds
( b₁,b₂ are_relative_prime iff b₁ hcf b₂ = one )

proof end;

definition

let c₁, c₂ be natural Ordinal;
func RED c₁,c₂ -> Element of omega equals :: ARYTM_3:def 5
a₁ div^ (a₁ hcf a₂);
coherence by ORDINAL2:def 21;

end;

:: deftheorem Def5 defines RED ARYTM_3:def 5 :

theorem Th26: :: ARYTM_3:26

for b₁, b₂ being natural Ordinal holds (RED b₁,b₂) *^ (b₁ hcf b₂) = b₁

proof end;

theorem Th27: :: ARYTM_3:27

for b₁, b₂ being natural Ordinal st ( b₁ <> {} or b₂ <> {} ) holds
RED b₁,b₂, RED b₂,b₁ are_relative_prime by Th24;

theorem Th28: :: ARYTM_3:28

for b₁, b₂ being natural Ordinal st b₁,b₂ are_relative_prime holds
RED b₁,b₂ = b₁

proof end;

theorem Th29: :: ARYTM_3:29

for b₁ being natural Ordinal holds
( RED b₁,one = b₁ & RED one ,b₁ = one )

proof end;

theorem Th30: :: ARYTM_3:30

for b₁, b₂ being natural Ordinal st b₁ <> {} holds
RED b₁,b₂ <> {} by Th23;

theorem Th31: :: ARYTM_3:31

for b₁ being natural Ordinal holds
( RED {} ,b₁ = {} & ( b₁ <> {} implies RED b₁,{} = one ) )

proof end;

theorem Th32: :: ARYTM_3:32

for b₁ being natural Ordinal st b₁ <> {} holds
RED b₁,b₁ = one

proof end;

theorem Th33: :: ARYTM_3:33

for b₁, b₂, b₃ being natural Ordinal st b₁ <> {} holds
RED (b₂ *^ b₁),(b₃ *^ b₁) = RED b₂,b₃

proof end;

set c₁ = { [b₁,b₂] where B is Element of omega , B is Element of omega : ( b₁,b₂ are_relative_prime & b₂ <> {} ) } ;

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

( c₂ <> {} & c₂,c₂ are_relative_prime )
by Th6;

then [c₂,c₂] in { [b₁,b₂] where B is Element of omega , B is Element of omega : ( b₁,b₂ are_relative_prime & b₂ <> {} ) }
;

then reconsider c₃ = { [b₁,b₂] where B is Element of omega , B is Element of omega : ( b₁,b₂ are_relative_prime & b₂ <> {} ) } as non empty set ;

Lemma37: for b₁, b₂ being natural Ordinal st [b₁,b₂] in c₃ holds
( b₁,b₂ are_relative_prime & b₂ <> {} )

proof end;

definition

func RAT+ -> set equals :: ARYTM_3:def 6
({ [b₁,b₂] where B is Element of omega , B is Element of omega : ( b₁,b₂ are_relative_prime & b₂ <> {} ) } \ { [b₁,one ] where B is Element of omega : verum } ) \/ omega ;
correctness ;

end;

:: deftheorem Def6 defines RAT+ ARYTM_3:def 6 :

theorem Th34: :: ARYTM_3:34

omega c= RAT+ by XBOOLE_1:7;

registration

cluster RAT+ -> non empty ;
coherence ;

end;

registration

cluster non empty ordinal Element of RAT+ ;
existence by Lemma1, Th34;

end;

theorem Th35: :: ARYTM_3:35

for b₁ being Element of RAT+ holds
( b₁ in omega or ex b₂, b₃ being Element of omega st
( b₁ = [b₂,b₃] & b₂,b₃ are_relative_prime & b₃ <> {} & b₃ <> one ) )

proof end;

theorem Th36: :: ARYTM_3:36

for b₁, b₂ being set holds [b₁,b₂] is not Ordinal

proof end;

theorem Th37: :: ARYTM_3:37

for b₁ being Ordinal st b₁ in RAT+ holds
b₁ in omega

proof end;

registration

cluster ordinal -> ordinal natural Element of RAT+ ;
coherence

proof end;

end;

theorem Th38: :: ARYTM_3:38

for b₁, b₂ being set holds not [b₁,b₂] in omega

proof end;

theorem Th39: :: ARYTM_3:39

for b₁, b₂ being Element of omega holds
( [b₁,b₂] in RAT+ iff ( b₁,b₂ are_relative_prime & b₂ <> {} & b₂ <> one ) )

proof end;

definition

let c₄ be Element of RAT+ ;
func numerator c₁ -> Element of omega means :Def7: :: ARYTM_3:def 7
a₂ = a₁ if a₁ in omega
otherwise ex b₁ being natural Ordinal st a₁ = [a₂,b₁];
existence

proof end;

correctness by ZFMISC_1:33;
func denominator c₁ -> Element of omega means :Def8: :: ARYTM_3:def 8
a₂ = one if a₁ in omega
otherwise ex b₁ being natural Ordinal st a₁ = [b₁,a₂];
existence

proof end;

correctness by ZFMISC_1:33;

end;

:: deftheorem Def7 defines numerator ARYTM_3:def 7 :

:: deftheorem Def8 defines denominator ARYTM_3:def 8 :

theorem Th40: :: ARYTM_3:40

for b₁ being Element of RAT+ holds numerator b₁, denominator b₁ are_relative_prime

proof end;

theorem Th41: :: ARYTM_3:41

for b₁ being Element of RAT+ holds denominator b₁ <> {}

proof end;

theorem Th42: :: ARYTM_3:42

for b₁ being Element of RAT+ st not b₁ in omega holds
( b₁ = [(numerator b₁),(denominator b₁)] & denominator b₁ <> one )

proof end;

theorem Th43: :: ARYTM_3:43

for b₁ being Element of RAT+ holds
( b₁ <> {} iff numerator b₁ <> {} )

proof end;

theorem Th44: :: ARYTM_3:44

for b₁ being Element of RAT+ holds
( b₁ in omega iff denominator b₁ = one ) by Def8, Th42;

definition

let c₄, c₅ be natural Ordinal;
func c₁ / c₂ -> Element of RAT+ equals :Def9: :: ARYTM_3:def 9
{} if a₂ = {}
RED a₁,a₂ if RED a₂,a₁ = one
otherwise [(RED a₁,a₂),(RED a₂,a₁)];
coherence

proof end;

consistency by Th31;

end;

:: deftheorem Def9 defines / ARYTM_3:def 9 :

notation

let c₄, c₅ be natural Ordinal;
synonym quotient c₁,c₂ for c₁ / c₂;

end;

theorem Th45: :: ARYTM_3:45

for b₁ being Element of RAT+ holds (numerator b₁) / (denominator b₁) = b₁

proof end;

theorem Th46: :: ARYTM_3:46

for b₁, b₂ being natural Ordinal holds
( {} / b₁ = {} & b₂ / one = b₂ )

proof end;

theorem Th47: :: ARYTM_3:47

for b₁ being natural Ordinal st b₁ <> {} holds
b₁ / b₁ = one

proof end;

theorem Th48: :: ARYTM_3:48

for b₁, b₂ being natural Ordinal st b₁ <> {} holds
( numerator (b₂ / b₁) = RED b₂,b₁ & denominator (b₂ / b₁) = RED b₁,b₂ )

proof end;

theorem Th49: :: ARYTM_3:49

for b₁, b₂ being Element of omega st b₁,b₂ are_relative_prime & b₂ <> {} holds
( numerator (b₁ / b₂) = b₁ & denominator (b₁ / b₂) = b₂ )

proof end;

theorem Th50: :: ARYTM_3:50

for b₁, b₂, b₃ being natural Ordinal st b₁ <> {} holds
(b₂ *^ b₁) / (b₃ *^ b₁) = b₂ / b₃

proof end;

theorem Th51: :: ARYTM_3:51

for b₁, b₂, b₃, b₄ being natural Ordinal st b₂ <> {} & b₁ <> {} holds
( b₃ / b₂ = b₄ / b₁ iff b₃ *^ b₁ = b₂ *^ b₄ )

proof end;

definition

let c₄, c₅ be Element of RAT+ ;
func c₁ + c₂ -> Element of RAT+ equals :: ARYTM_3:def 10
(((numerator a₁) *^ (denominator a₂)) +^ ((numerator a₂) *^ (denominator a₁))) / ((denominator a₁) *^ (denominator a₂));
coherence ;
commutativity ;
func c₁ *' c₂ -> Element of RAT+ equals :: ARYTM_3:def 11
((numerator a₁) *^ (numerator a₂)) / ((denominator a₁) *^ (denominator a₂));
coherence ;
commutativity ;

end;

:: deftheorem Def10 defines + ARYTM_3:def 10 :

:: deftheorem Def11 defines *' ARYTM_3:def 11 :

theorem Th52: :: ARYTM_3:52

for b₁, b₂, b₃, b₄ being natural Ordinal st b₂ <> {} & b₁ <> {} holds
(b₃ / b₂) + (b₄ / b₁) = ((b₃ *^ b₁) +^ (b₂ *^ b₄)) / (b₂ *^ b₁)

proof end;

theorem Th53: :: ARYTM_3:53

for b₁, b₂, b₃ being natural Ordinal st b₁ <> {} holds
(b₂ / b₁) + (b₃ / b₁) = (b₂ +^ b₃) / b₁

proof end;

registration

cluster empty natural Element of RAT+ ;
existence by Th34, ORDINAL2:19;

end;

definition

redefine func {} as {} -> empty Element of RAT+ ;
coherence by Th34, ORDINAL2:19;
redefine func one as one -> non empty ordinal Element of RAT+ ;
coherence by Lemma1, Th34;

end;

theorem Th54: :: ARYTM_3:54

for b₁ being Element of RAT+ holds b₁ *' {} = {}

proof end;

theorem Th55: :: ARYTM_3:55

for b₁, b₂, b₃, b₄ being natural Ordinal holds (b₂ / b₃) *' (b₄ / b₁) = (b₂ *^ b₄) / (b₃ *^ b₁)

proof end;

theorem Th56: :: ARYTM_3:56

for b₁ being Element of RAT+ holds b₁ + {} = b₁

proof end;

theorem Th57: :: ARYTM_3:57

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

proof end;

theorem Th58: :: ARYTM_3:58

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

proof end;

theorem Th59: :: ARYTM_3:59

for b₁ being Element of RAT+ holds b₁ *' one = b₁

proof end;

theorem Th60: :: ARYTM_3:60

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

proof end;

theorem Th61: :: ARYTM_3:61

for b₁, b₂ being Element of RAT+ st b₁ <> {} holds
ex b₃ being Element of RAT+ st b₂ = b₁ *' b₃

proof end;

theorem Th62: :: ARYTM_3:62

for b₁, b₂, b₃ being Element of RAT+ st b₁ <> {} & b₁ *' b₂ = b₁ *' b₃ holds
b₂ = b₃

proof end;

theorem Th63: :: ARYTM_3:63

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

proof end;

theorem Th64: :: ARYTM_3:64

for b₁, b₂ being ordinal Element of RAT+ holds b₁ + b₂ = b₁ +^ b₂

proof end;

theorem Th65: :: ARYTM_3:65

for b₁, b₂ being ordinal Element of RAT+ holds b₁ *' b₂ = b₁ *^ b₂

proof end;

theorem Th66: :: ARYTM_3:66

for b₁ being Element of RAT+ ex b₂ being Element of RAT+ st b₁ = b₂ + b₂

proof end;

definition

let c₄, c₅ be Element of RAT+ ;
pred c₁ <=' c₂ means :Def12: :: ARYTM_3:def 12
ex b₁ being Element of RAT+ st a₂ = a₁ + b₁;
connectedness

proof end;

end;

:: deftheorem Def12 defines <=' ARYTM_3:def 12 :

notation

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

end;

theorem Th67: :: ARYTM_3:67

canceled;

theorem Th68: :: ARYTM_3:68

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

proof end;

theorem Th69: :: ARYTM_3:69

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

proof end;

theorem Th70: :: ARYTM_3:70

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

proof end;

theorem Th71: :: ARYTM_3:71

for b₁ being Element of RAT+ holds {} <=' b₁

proof end;

theorem Th72: :: ARYTM_3:72

for b₁ being Element of RAT+ st b₁ <=' {} holds
b₁ = {}

proof end;

theorem Th73: :: ARYTM_3:73

for b₁, b₂ being Element of RAT+ st b₁ <=' b₂ & b₂ <=' b₁ holds
b₁ = b₂

proof end;

theorem Th74: :: ARYTM_3:74

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

proof end;

theorem Th75: :: ARYTM_3:75

for b₁, b₂ being Element of RAT+ holds
( b₁ < b₂ iff ( b₁ <=' b₂ & b₁ <> b₂ ) ) by Th73;

theorem Th76: :: ARYTM_3:76

for b₁, b₂, b₃ being Element of RAT+ st ( ( b₁ < b₂ & b₂ <=' b₃ ) or ( b₁ <=' b₂ & b₂ < b₃ ) ) holds
b₁ < b₃ by Th74;

theorem Th77: :: ARYTM_3:77

for b₁, b₂, b₃ being Element of RAT+ st b₁ < b₂ & b₂ < b₃ holds
b₁ < b₃ by Th74;

theorem Th78: :: ARYTM_3:78

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

proof end;

theorem Th79: :: ARYTM_3:79

for b₁ being Element of RAT+
for b₂ being ordinal Element of RAT+ st b₂ < b₁ & b₁ < b₂ + one holds
not b₁ in omega

proof end;

theorem Th80: :: ARYTM_3:80

for b₁ being Element of RAT+ st b₁ <> {} holds
ex b₂ being Element of RAT+ st
( b₂ < b₁ & not b₂ in omega )

proof end;

theorem Th81: :: ARYTM_3:81

for b₁ being Element of RAT+ holds
( { b₂ where B is Element of RAT+ : b₂ < b₁ } in RAT+ iff b₁ = {} )

proof end;

theorem Th82: :: ARYTM_3:82

for b₁ being Subset of RAT+ st ex b₂ being Element of RAT+ st
( b₂ in b₁ & b₂ <> {} ) & ( for b₂, b₃ being Element of RAT+ st b₂ in b₁ & b₃ <=' b₂ holds
b₃ in b₁ ) holds
ex b₂, b₃, b₄ being Element of RAT+ st
( b₂ in b₁ & b₃ in b₁ & b₄ in b₁ & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ )

proof end;

theorem Th83: :: ARYTM_3:83

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

proof end;

theorem Th84: :: ARYTM_3:84

canceled;

theorem Th85: :: ARYTM_3:85

for b₁, b₂ being Element of RAT+ holds b₁ <=' b₁ + b₂

proof end;

theorem Th86: :: ARYTM_3:86

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

proof end;

theorem Th87: :: ARYTM_3:87

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

proof end;

theorem Th88: :: ARYTM_3:88

for b₁, b₂, b₃ being Element of RAT+ st b₁ <> {} & b₂ *' b₁ <=' b₃ *' b₁ holds
b₂ <=' b₃

proof end;

theorem Th89: :: ARYTM_3:89

for b₁, b₂, b₃, b₄ being Element of RAT+ holds
( not b₁ + b₂ = b₃ + b₄ or b₁ <=' b₃ or b₂ <=' b₄ )

proof end;

theorem Th90: :: ARYTM_3:90

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

proof end;

theorem Th91: :: ARYTM_3:91

for b₁, b₂, b₃, b₄ being Element of RAT+ holds
( not b₁ *' b₂ = b₃ *' b₄ or b₁ <=' b₃ or b₂ <=' b₄ )

proof end;

theorem Th92: :: ARYTM_3:92

for b₁, b₂ being Element of RAT+ holds
( b₁ = {} iff b₁ + b₂ = b₂ )

proof end;

theorem Th93: :: ARYTM_3:93

for b₁, b₂, b₃, b₄ being Element of RAT+ st b₁ + b₂ = b₃ + b₄ & b₁ <=' b₃ holds
b₄ <=' b₂

proof end;

theorem Th94: :: ARYTM_3:94

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

proof end;

theorem Th95: :: ARYTM_3:95

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

proof end;

theorem Th96: :: ARYTM_3:96

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

proof end;

theorem Th97: :: ARYTM_3:97

for b₁, b₂, b₃ being Element of RAT+ st b₁ <=' b₂ & b₂ <=' b₃ & b₂ <> b₃ holds
b₁ <> b₃ by Th73;

theorem Th98: :: ARYTM_3:98

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

proof end;

theorem Th99: :: ARYTM_3:99

for b₁ being non empty Subset of RAT+ st b₁ in RAT+ holds
ex b₂ being Element of RAT+ st
( b₂ in b₁ & ( for b₃ being Element of RAT+ st b₃ in b₁ holds
b₃ <=' b₂ ) )

proof end;

theorem Th100: :: ARYTM_3:100

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

proof end;

theorem Th101: :: ARYTM_3:101

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

proof end;

theorem Th102: :: ARYTM_3:102

for b₁ being Element of RAT+ ex b₂ being Element of RAT+ st b₁ < b₂

proof end;

theorem Th103: :: ARYTM_3:103

for b₁, b₂ being Element of RAT+ st b₁ <> {} holds
ex b₃ being Element of RAT+ st
( b₃ in omega & b₂ <=' b₃ *' b₁ )

proof end;

scheme :: ARYTM_3:sch 2
s2{ F₁() -> Element of RAT+ , F₂() -> Element of RAT+ , F₃() -> Element of RAT+ , P₁[ set ] } :

ex b₁ being Element of RAT+ st
( b₁ in omega & P₁[b₁] & P₁[b₁ + F₂()] )

provided

E86: F₂() = one and
E87: F₁() = {} and
E88: F₃() in omega and
E89: P₁[F₁()] and
E90: P₁[F₃()]

proof end;