:: RAT_1 semantic presentation

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

Lemma2: for b₁, b₂ being Nat holds quotient b₁,b₂ = b₁ / b₂

proof end;

0 in omega
;

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

Lemma3: for b₁ being real number
for b₂ being Element of REAL+ st b₂ = b₁ holds
c₁ - b₂ = - b₁

proof end;

Lemma4: for b₁ being set st b₁ in RAT holds
ex b₂, b₃ being Integer st b₁ = b₂ / b₃

proof end;

Lemma5: for b₁ being set
for b₂ being Nat
for b₃ being Integer st b₁ = b₃ / b₂ holds
b₁ in RAT

proof end;

Lemma6: for b₁ being set
for b₂, b₃ being Integer st b₁ = b₂ / b₃ holds
b₁ in RAT

proof end;

definition

redefine func RAT -> set means :Def1: :: RAT_1:def 1
for b₁ being set holds
( b₁ in a₁ iff ex b₂, b₃ being Integer st b₁ = b₂ / b₃ );
compatibility

proof end;

end;

:: deftheorem Def1 defines RAT RAT_1:def 1 :

definition

let c₂ be number ;
attr a₁ is rational means :Def2: :: RAT_1:def 2
a₁ in RAT ;

end;

:: deftheorem Def2 defines rational RAT_1:def 2 :

registration

cluster rational Element of REAL ;
existence

proof end;

end;

registration

cluster rational set ;
existence

proof end;

end;

definition

mode Rational is rational number ;

end;

theorem Th1: :: RAT_1:1

for b₁ being set st b₁ in RAT holds
ex b₂, b₃ being Integer st
( b₃ <> 0 & b₁ = b₂ / b₃ )

proof end;

theorem Th2: :: RAT_1:2

canceled;

theorem Th3: :: RAT_1:3

for b₁ being set st b₁ is Rational holds
ex b₂, b₃ being Integer st
( b₃ <> 0 & b₁ = b₂ / b₃ )

proof end;

registration

cluster rational -> real set ;
coherence

proof end;

end;

theorem Th4: :: RAT_1:4

canceled;

theorem Th5: :: RAT_1:5

canceled;

theorem Th6: :: RAT_1:6

for b₁ being set st ex b₂, b₃ being Integer st b₁ = b₂ / b₃ holds
b₁ is rational

proof end;

theorem Th7: :: RAT_1:7

for b₁ being Integer holds b₁ is Rational

proof end;

registration

cluster integer -> real rational set ;
coherence by Th7;

end;

registration

let c₂, c₃ be Rational;
cluster a₁ * a₂ -> rational ;
coherence

proof end;

cluster a₁ + a₂ -> rational ;
coherence

proof end;

cluster a₁ - a₂ -> rational ;
coherence

proof end;

end;

registration

let c₂ be Rational;
let c₃ be Integer;
cluster a₁ + a₂ -> rational ;
coherence ;
cluster a₁ - a₂ -> rational ;
coherence ;
cluster a₁ * a₂ -> rational ;
coherence ;

end;

registration

let c₂ be Integer;
let c₃ be Rational;
cluster a₁ + a₂ -> rational ;
coherence ;
cluster a₁ - a₂ -> rational ;
coherence ;
cluster a₁ * a₂ -> rational ;
coherence ;

end;

registration

let c₂ be Rational;
let c₃ be Nat;
cluster a₁ + a₂ -> rational ;
coherence ;
cluster a₁ - a₂ -> rational ;
coherence ;
cluster a₁ * a₂ -> rational ;
coherence ;

end;

registration

let c₂ be Nat;
let c₃ be Rational;
cluster a₁ + a₂ -> rational ;
coherence ;
cluster a₁ - a₂ -> rational ;
coherence ;
cluster a₁ * a₂ -> rational ;
coherence ;

end;

registration

let c₂ be Rational;
cluster - a₁ -> rational ;
coherence

proof end;

end;

theorem Th8: :: RAT_1:8

canceled;

theorem Th9: :: RAT_1:9

canceled;

theorem Th10: :: RAT_1:10

canceled;

theorem Th11: :: RAT_1:11

canceled;

theorem Th12: :: RAT_1:12

canceled;

theorem Th13: :: RAT_1:13

canceled;

theorem Th14: :: RAT_1:14

canceled;

theorem Th15: :: RAT_1:15

canceled;

theorem Th16: :: RAT_1:16

for b₁, b₂ being Rational holds b₁ / b₂ is Rational

proof end;

registration

let c₂, c₃ be rational number ;
cluster a₁ / a₂ -> rational ;
coherence by Th16;

end;

theorem Th17: :: RAT_1:17

canceled;

theorem Th18: :: RAT_1:18

canceled;

theorem Th19: :: RAT_1:19

canceled;

theorem Th20: :: RAT_1:20

canceled;

theorem Th21: :: RAT_1:21

for b₁ being Rational holds b₁ " is Rational

proof end;

registration

let c₂ be rational number ;
cluster a₁ " -> rational ;
coherence by Th21;

end;

theorem Th22: :: RAT_1:22

for b₁, b₂ being real number st b₁ < b₂ holds
ex b₃ being Rational st
( b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th23: :: RAT_1:23

canceled;

theorem Th24: :: RAT_1:24

for b₁ being Rational ex b₂ being Integerex b₃ being Nat st
( b₃ <> 0 & b₁ = b₂ / b₃ )

proof end;

theorem Th25: :: RAT_1:25

for b₁ being Rational ex b₂ being Integerex b₃ being Nat st
( b₃ <> 0 & b₁ = b₂ / b₃ & ( for b₄ being Integer
for b₅ being Nat st b₅ <> 0 & b₁ = b₄ / b₅ holds
b₃ <= b₅ ) )

proof end;

definition

let c₂ be Rational;
func denominator c₁ -> Nat means :Def3: :: RAT_1:def 3
( a₂ <> 0 & ex b₁ being Integer st a₁ = b₁ / a₂ & ( for b₁ being Integer
for b₂ being Nat st b₂ <> 0 & a₁ = b₁ / b₂ holds
a₂ <= b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines denominator RAT_1:def 3 :

definition

let c₂ be Rational;
func numerator c₁ -> Integer equals :: RAT_1:def 4
(denominator a₁) * a₁;
coherence

proof end;

end;

:: deftheorem Def4 defines numerator RAT_1:def 4 :

theorem Th26: :: RAT_1:26

canceled;

theorem Th27: :: RAT_1:27

for b₁ being Rational holds 0 < denominator b₁

proof end;

theorem Th28: :: RAT_1:28

canceled;

theorem Th29: :: RAT_1:29

for b₁ being Rational holds 1 <= denominator b₁

proof end;

theorem Th30: :: RAT_1:30

for b₁ being Rational holds 0 < (denominator b₁) "

proof end;

theorem Th31: :: RAT_1:31

canceled;

theorem Th32: :: RAT_1:32

canceled;

theorem Th33: :: RAT_1:33

canceled;

theorem Th34: :: RAT_1:34

for b₁ being Rational holds 1 >= (denominator b₁) "

proof end;

theorem Th35: :: RAT_1:35

canceled;

theorem Th36: :: RAT_1:36

for b₁ being Rational holds
( numerator b₁ = 0 iff b₁ = 0 )

proof end;

theorem Th37: :: RAT_1:37

for b₁ being Rational holds
( b₁ = (numerator b₁) / (denominator b₁) & b₁ = (numerator b₁) * ((denominator b₁) " ) & b₁ = ((denominator b₁) " ) * (numerator b₁) )

proof end;

theorem Th38: :: RAT_1:38

for b₁ being Rational st b₁ <> 0 holds
denominator b₁ = (numerator b₁) / b₁

proof end;

theorem Th39: :: RAT_1:39

canceled;

theorem Th40: :: RAT_1:40

for b₁ being Rational st b₁ is Integer holds
( denominator b₁ = 1 & numerator b₁ = b₁ )

proof end;

theorem Th41: :: RAT_1:41

for b₁ being Rational st ( numerator b₁ = b₁ or denominator b₁ = 1 ) holds
b₁ is Integer

proof end;

theorem Th42: :: RAT_1:42

for b₁ being Rational holds
( numerator b₁ = b₁ iff denominator b₁ = 1 ) by Th40;

theorem Th43: :: RAT_1:43

canceled;

theorem Th44: :: RAT_1:44

for b₁ being Rational st ( numerator b₁ = b₁ or denominator b₁ = 1 ) & 0 <= b₁ holds
b₁ is Nat

proof end;

theorem Th45: :: RAT_1:45

for b₁ being Rational holds
( 1 < denominator b₁ iff not b₁ is integer )

proof end;

Lemma26: 1 " = 1
;

theorem Th46: :: RAT_1:46

for b₁ being Rational holds
( 1 > (denominator b₁) " iff not b₁ is integer )

proof end;

theorem Th47: :: RAT_1:47

for b₁ being Rational holds
( numerator b₁ = denominator b₁ iff b₁ = 1 )

proof end;

theorem Th48: :: RAT_1:48

for b₁ being Rational holds
( numerator b₁ = - (denominator b₁) iff b₁ = - 1 )

proof end;

theorem Th49: :: RAT_1:49

for b₁ being Rational holds
( - (numerator b₁) = denominator b₁ iff b₁ = - 1 )

proof end;

theorem Th50: :: RAT_1:50

for b₁ being Integer
for b₂ being Rational st b₁ <> 0 holds
b₂ = ((numerator b₂) * b₁) / ((denominator b₂) * b₁)

proof end;

theorem Th51: :: RAT_1:51

canceled;

theorem Th52: :: RAT_1:52

canceled;

theorem Th53: :: RAT_1:53

canceled;

theorem Th54: :: RAT_1:54

canceled;

theorem Th55: :: RAT_1:55

canceled;

theorem Th56: :: RAT_1:56

canceled;

theorem Th57: :: RAT_1:57

canceled;

theorem Th58: :: RAT_1:58

canceled;

theorem Th59: :: RAT_1:59

canceled;

theorem Th60: :: RAT_1:60

for b₁ being Nat
for b₂ being Integer
for b₃ being Rational st b₁ <> 0 & b₃ = b₂ / b₁ holds
ex b₄ being Nat st
( b₂ = (numerator b₃) * b₄ & b₁ = (denominator b₃) * b₄ )

proof end;

theorem Th61: :: RAT_1:61

for b₁, b₂ being Integer
for b₃ being Rational st b₃ = b₁ / b₂ & b₂ <> 0 holds
ex b₄ being Integer st
( b₁ = (numerator b₃) * b₄ & b₂ = (denominator b₃) * b₄ )

proof end;

theorem Th62: :: RAT_1:62

for b₁ being Rational
for b₂ being Nat holds
( not 1 < b₂ or for b₃ being Integer
for b₄ being Nat holds
( not numerator b₁ = b₃ * b₂ or not denominator b₁ = b₄ * b₂ ) )

proof end;

theorem Th63: :: RAT_1:63

for b₁ being Nat
for b₂ being Integer
for b₃ being Rational st b₃ = b₂ / b₁ & b₁ <> 0 & ( for b₄ being Nat holds
( not 1 < b₄ or for b₅ being Integer
for b₆ being Nat holds
( not b₂ = b₅ * b₄ or not b₁ = b₆ * b₄ ) ) ) holds
( b₁ = denominator b₃ & b₂ = numerator b₃ )

proof end;

theorem Th64: :: RAT_1:64

for b₁ being Rational holds
( b₁ < - 1 iff numerator b₁ < - (denominator b₁) )

proof end;

theorem Th65: :: RAT_1:65

for b₁ being Rational holds
( b₁ <= - 1 iff numerator b₁ <= - (denominator b₁) )

proof end;

theorem Th66: :: RAT_1:66

for b₁ being Rational holds
( b₁ < - 1 iff denominator b₁ < - (numerator b₁) )

proof end;

theorem Th67: :: RAT_1:67

for b₁ being Rational holds
( b₁ <= - 1 iff denominator b₁ <= - (numerator b₁) )

proof end;

theorem Th68: :: RAT_1:68

canceled;

theorem Th69: :: RAT_1:69

canceled;

theorem Th70: :: RAT_1:70

canceled;

theorem Th71: :: RAT_1:71

canceled;

theorem Th72: :: RAT_1:72

for b₁ being Rational holds
( b₁ < 1 iff numerator b₁ < denominator b₁ )

proof end;

theorem Th73: :: RAT_1:73

for b₁ being Rational holds
( b₁ <= 1 iff numerator b₁ <= denominator b₁ )

proof end;

theorem Th74: :: RAT_1:74

canceled;

theorem Th75: :: RAT_1:75

canceled;

theorem Th76: :: RAT_1:76

for b₁ being Rational holds
( b₁ < 0 iff numerator b₁ < 0 )

proof end;

theorem Th77: :: RAT_1:77

for b₁ being Rational holds
( b₁ <= 0 iff numerator b₁ <= 0 )

proof end;

theorem Th78: :: RAT_1:78

canceled;

theorem Th79: :: RAT_1:79

canceled;

theorem Th80: :: RAT_1:80

for b₁ being real number
for b₂ being Rational holds
( b₁ < b₂ iff b₁ * (denominator b₂) < numerator b₂ )

proof end;

theorem Th81: :: RAT_1:81

for b₁ being real number
for b₂ being Rational holds
( b₁ <= b₂ iff b₁ * (denominator b₂) <= numerator b₂ )

proof end;

theorem Th82: :: RAT_1:82

canceled;

theorem Th83: :: RAT_1:83

canceled;

theorem Th84: :: RAT_1:84

for b₁, b₂ being Rational st denominator b₁ = denominator b₂ & numerator b₁ = numerator b₂ holds
b₁ = b₂

proof end;

theorem Th85: :: RAT_1:85

canceled;

theorem Th86: :: RAT_1:86

for b₁, b₂ being Rational holds
( b₁ < b₂ iff (numerator b₁) * (denominator b₂) < (numerator b₂) * (denominator b₁) )

proof end;

theorem Th87: :: RAT_1:87

for b₁ being Rational holds
( denominator (- b₁) = denominator b₁ & numerator (- b₁) = - (numerator b₁) )

proof end;

theorem Th88: :: RAT_1:88

for b₁, b₂ being Rational holds
( 0 < b₁ & b₂ = 1 / b₁ iff ( numerator b₂ = denominator b₁ & denominator b₂ = numerator b₁ ) )

proof end;

theorem Th89: :: RAT_1:89

for b₁, b₂ being Rational holds
( b₁ < 0 & b₂ = 1 / b₁ iff ( numerator b₂ = - (denominator b₁) & denominator b₂ = - (numerator b₁) ) )

proof end;