:: Basic Properties of Rational Numbers
:: by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

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

Lm2: for i1, j1 being Nat holds quotient (i1,j1) = i1 / j1

proof end;

Lm3: for a being Real
for Z9 being Element of REAL+ st Z9 = 0 holds
for x9 being Element of REAL+ st x9 = a holds
Z9 - x9 = - a

proof end;

Lm4: for x being object st x in RAT holds
ex m, n being Integer st x = m / n

proof end;

Lm5: for x being object
for w being Nat
for m being Integer st x = m / w holds
x in RAT

proof end;

Lm6: for x being object
for m, n being Integer st x = m / n holds
x in RAT

proof end;

definition

redefine func RAT means :Def1: :: RAT_1:def 1
for x being object holds
( x in it iff ex m, n being Integer st x = m / n );

compatibility
for b₁ being set holds
( b₁ = RAT iff for x being object holds
( x in b₁ iff ex m, n being Integer st x = m / n ) )

proof end;

end;

:: deftheorem Def1 defines RAT RAT_1:def 1 :
for b₁ being set holds
( b₁ = RAT iff for x being object holds
( x in b₁ iff ex m, n being Integer st x = m / n ) );

definition

let r be object ;

attr r is rational means :: RAT_1:def 2
r in RAT ;

end;

:: deftheorem defines rational RAT_1:def 2 :
for r being object holds
( r is rational iff r in RAT );

registration

cluster ext-real V34() real rational for object ;

existence
ex b₁ being Real st b₁ is rational

proof end;

end;

registration

cluster rational for set ;

existence
ex b₁ being number st b₁ is rational

proof end;

end;

definition

mode Rational is rational Number ;

end;

theorem Th1: :: RAT_1:1

for x being object st x in RAT holds
ex m, n being Integer st
( n <> 0 & x = m / n )

proof end;

theorem Th2: :: RAT_1:2

for x being object st x is rational holds
ex m, n being Integer st
( n <> 0 & x = m / n ) by Th1;

registration

cluster rational -> real for object ;

coherence
for b₁ being object st b₁ is rational holds
b₁ is real by NUMBERS:12;

end;

theorem Th3: :: RAT_1:3

for m, n being Integer holds m / n is rational by Def1;

registration

cluster integer -> rational for object ;

coherence
for b₁ being object st b₁ is integer holds
b₁ is rational

proof end;

end;

:: Now we prove that fractions of integer denominator and natural numerator
:: or of natural denominator and numerator, etc., are all rational numbers.

registration

let p, q be Rational;

cluster p * q -> rational ;

coherence
p * q is rational

proof end;

cluster p + q -> rational ;

coherence
p + q is rational

proof end;

cluster p - q -> rational ;

coherence
p - q is rational

proof end;

cluster p / q -> rational ;

coherence
p / q is rational

proof end;

end;

registration

let p be Rational;

cluster - p -> rational ;

coherence
- p is rational

proof end;

cluster p " -> rational ;

coherence
p " is rational

proof end;

end;

theorem :: RAT_1:4

canceled;

theorem :: RAT_1:5

canceled;

theorem :: RAT_1:6

canceled;

::$CT 3
:: RAT is dense, that is there exists at least one rational number between
:: any two distinct real numbers.

theorem :: RAT_1:7

for a, b being Real st a < b holds
ex p being Rational st
( a < p & p < b )

proof end;

theorem Th5: :: RAT_1:8

for p being Rational ex m being Integer ex k being Nat st
( k <> 0 & p = m / k )

proof end;

:: Each rational number can be uniquely expressed as a ratio of two
:: relatively prime numbers, the first is integer and the latter is natural
:: (but not equal to zero). Function denominator(p) is defined as the least
:: natural denominator of all denominators of fractions integer/natural=p.
:: Function numerator(p) is defined as a product of p and denominator(p).

theorem Th6: :: RAT_1:9

for p being Rational ex m being Integer ex k being Nat st
( k <> 0 & p = m / k & ( for n being Integer
for w being Nat st w <> 0 & p = n / w holds
k <= w ) )

proof end;

definition

let p be Rational;

func denominator p -> Nat means :Def3: :: RAT_1:def 3
( it <> 0 & ex m being Integer st p = m / it & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
it <= k ) );

existence
ex b₁ being Nat st
( b₁ <> 0 & ex m being Integer st p = m / b₁ & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
b₁ <= k ) )

proof end;

uniqueness
for b₁, b₂ being Nat st b₁ <> 0 & ex m being Integer st p = m / b₁ & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
b₁ <= k ) & b₂ <> 0 & ex m being Integer st p = m / b₂ & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
b₂ <= k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines denominator RAT_1:def 3 :
for p being Rational
for b₂ being Nat holds
( b₂ = denominator p iff ( b₂ <> 0 & ex m being Integer st p = m / b₂ & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
b₂ <= k ) ) );

definition

let p be Rational;

func numerator p -> Integer equals :: RAT_1:def 4
(denominator p) * p;

coherence
(denominator p) * p is Integer

proof end;

end;

:: deftheorem defines numerator RAT_1:def 4 :
for p being Rational holds numerator p = (denominator p) * p;

:: Some basic theorems concerning p, numerator(p) and denominator(p).

theorem Th7: :: RAT_1:10

for p being Rational holds 0 < denominator p

proof end;

registration

let p be Rational;

cluster denominator p -> positive ;

coherence
denominator p is positive by Th7;

end;

theorem Th8: :: RAT_1:11

for p being Rational holds 1 <= denominator p

proof end;

theorem :: RAT_1:12

for p being Rational holds 0 < (denominator p) " ;

theorem Th10: :: RAT_1:13

for p being Rational holds 1 >= (denominator p) "

proof end;

theorem Th11: :: RAT_1:14

for p being Rational holds
( numerator p = 0 iff p = 0 ) by XCMPLX_1:6;

theorem Th12: :: RAT_1:15

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

proof end;

theorem :: RAT_1:16

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

proof end;

theorem Th14: :: RAT_1:17

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

proof end;

theorem Th15: :: RAT_1:18

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

proof end;

theorem :: RAT_1:19

for p being Rational holds
( numerator p = p iff denominator p = 1 ) by Th14;

theorem :: RAT_1:20

for p being Rational st ( numerator p = p or denominator p = 1 ) & 0 <= p holds
p is Element of NAT

proof end;

theorem :: RAT_1:21

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

proof end;

Lm7: 1 " = 1
;

theorem :: RAT_1:22

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

proof end;

theorem Th20: :: RAT_1:23

for p being Rational holds
( numerator p = denominator p iff p = 1 )

proof end;

theorem Th21: :: RAT_1:24

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

proof end;

theorem :: RAT_1:25

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

proof end;

:: We can multiple the numerator and the denominator of any rational number
:: by any integer (natural) number which is not equal to zero.

theorem Th23: :: RAT_1:26

for m being Integer
for p being Rational st m <> 0 holds
p = ((numerator p) * m) / ((denominator p) * m)

proof end;

theorem Th24: :: RAT_1:27

for k being Nat
for m being Integer
for p being Rational st k <> 0 & p = m / k holds
ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w )

proof end;

theorem :: RAT_1:28

for m, n being Integer
for p being Rational st p = m / n & n <> 0 holds
ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )

proof end;

:: Fraction numerator(p)/denominator(p) is irreducible.

theorem Th26: :: RAT_1:29

for p being Rational
for w being Nat holds
( not 1 < w or for m being Integer
for k being Nat holds
( not numerator p = m * w or not denominator p = k * w ) )

proof end;

theorem Th27: :: RAT_1:30

for k being Nat
for m being Integer
for p being Rational st p = m / k & k <> 0 & ( for w being Nat holds
( not 1 < w or for m1 being Integer
for k1 being Nat holds
( not m = m1 * w or not k = k1 * w ) ) ) holds
( k = denominator p & m = numerator p )

proof end;

theorem Th28: :: RAT_1:31

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

proof end;

theorem Th29: :: RAT_1:32

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

proof end;

theorem :: RAT_1:33

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

proof end;

theorem :: RAT_1:34

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

proof end;

theorem Th32: :: RAT_1:35

for p being Rational holds
( p < 1 iff numerator p < denominator p )

proof end;

theorem :: RAT_1:36

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

proof end;

theorem :: RAT_1:37

for p being Rational holds
( p < 0 iff numerator p < 0 )

proof end;

theorem Th35: :: RAT_1:38

for p being Rational holds
( p <= 0 iff numerator p <= 0 )

proof end;

theorem Th36: :: RAT_1:39

for a being Real
for p being Rational holds
( a < p iff a * (denominator p) < numerator p )

proof end;

theorem :: RAT_1:40

for a being Real
for p being Rational holds
( a <= p iff a * (denominator p) <= numerator p )

proof end;

theorem :: RAT_1:41

for p, q being Rational st denominator p = denominator q & numerator p = numerator q holds
p = q

proof end;

theorem :: RAT_1:42

for p, q being Rational holds
( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )

proof end;

theorem Th40: :: RAT_1:43

for p being Rational holds
( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )

proof end;

theorem Th41: :: RAT_1:44

for p, q being Rational holds
( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )

proof end;

theorem :: RAT_1:45

for p, q being Rational holds
( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) )

proof end;