:: by Andrzej Kondracki

::

:: Received July 10, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega

by XBOOLE_1:7;

Lm2: for i1, j1 being Element of NAT holds quotient (i1,j1) = i1 / j1

proof end;

0 in omega

;

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

Lm3: for a being real number

for x9 being Element of REAL+ st x9 = a holds

09 - x9 = - a

proof end;

Lm4: for x being set st x in RAT holds

ex m, n being Integer st x = m / n

proof end;

Lm5: for x being set

for l being Element of NAT

for m being Integer st x = m / l holds

x in RAT

proof end;

Lm6: for x being set

for m, n being Integer st x = m / n holds

x in RAT

proof end;

definition

for b_{1} being set holds

( b_{1} = RAT iff for x being set holds

( x in b_{1} iff ex m, n being Integer st x = m / n ) )
end;

redefine func RAT means :Def1: :: RAT_1:def 1

for x being set holds

( x in it iff ex m, n being Integer st x = m / n );

compatibility for x being set holds

( x in it iff ex m, n being Integer st x = m / n );

for b

( b

( x in b

proof end;

:: deftheorem Def1 defines RAT RAT_1:def 1 :

for b_{1} being set holds

( b_{1} = RAT iff for x being set holds

( x in b_{1} iff ex m, n being Integer st x = m / n ) );

for b

( b

( x in b

:: deftheorem Def2 defines rational RAT_1:def 2 :

for r being number holds

( r is rational iff r in RAT );

for r being number holds

( r is rational iff r in RAT );

registration
end;

registration
end;

registration
end;

registration

let p, q be Rational;

coherence

p * q is rational

p + q is rational

p - q is rational

p / q is rational

end;
coherence

p * q is rational

proof end;

coherence p + q is rational

proof end;

coherence p - q is rational

proof end;

coherence p / q is rational

proof end;

registration
end;

:: RAT is dense, that is there exists at least one rational number between

:: any two distinct real numbers.

:: any two distinct real numbers.

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

:: 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 Th9: :: RAT_1:9

for p being Rational ex m being Integer ex k being Element of NAT st

( k <> 0 & p = m / k & ( for n being Integer

for l being Element of NAT st l <> 0 & p = n / l holds

k <= l ) )

( k <> 0 & p = m / k & ( for n being Integer

for l being Element of NAT st l <> 0 & p = n / l holds

k <= l ) )

proof end;

definition

let p be Rational;

ex b_{1} being Element of NAT st

( b_{1} <> 0 & ex m being Integer st p = m / b_{1} & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

b_{1} <= k ) )

for b_{1}, b_{2} being Element of NAT st b_{1} <> 0 & ex m being Integer st p = m / b_{1} & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

b_{1} <= k ) & b_{2} <> 0 & ex m being Integer st p = m / b_{2} & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

b_{2} <= k ) holds

b_{1} = b_{2}

end;
func denominator p -> Element of NAT means :Def3: :: RAT_1:def 3

( it <> 0 & ex m being Integer st p = m / it & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

it <= k ) );

existence ( it <> 0 & ex m being Integer st p = m / it & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

it <= k ) );

ex b

( b

for k being Element of NAT st k <> 0 & p = n / k holds

b

proof end;

uniqueness for b

for k being Element of NAT st k <> 0 & p = n / k holds

b

for k being Element of NAT st k <> 0 & p = n / k holds

b

b

proof end;

:: deftheorem Def3 defines denominator RAT_1:def 3 :

for p being Rational

for b_{2} being Element of NAT holds

( b_{2} = denominator p iff ( b_{2} <> 0 & ex m being Integer st p = m / b_{2} & ( for n being Integer

for k being Element of NAT st k <> 0 & p = n / k holds

b_{2} <= k ) ) );

for p being Rational

for b

( b

for k being Element of NAT st k <> 0 & p = n / k holds

b

:: deftheorem defines numerator RAT_1:def 4 :

for p being Rational holds numerator p = (denominator p) * p;

for p being Rational holds numerator p = (denominator p) * p;

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

theorem Th15: :: RAT_1:15

for p being Rational holds

( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) ") & p = ((denominator p) ") * (numerator p) )

( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) ") & p = ((denominator p) ") * (numerator p) )

proof end;

Lm7: 1 " = 1

;

:: We can multiple the numerator and the denominator of any rational number

:: by any integer (natural) number which is not equal to zero.

:: by any integer (natural) number which is not equal to zero.

theorem Th26: :: RAT_1:26

for m being Integer

for p being Rational st m <> 0 holds

p = ((numerator p) * m) / ((denominator p) * m)

for p being Rational st m <> 0 holds

p = ((numerator p) * m) / ((denominator p) * m)

proof end;

theorem Th27: :: RAT_1:27

for k being Element of NAT

for m being Integer

for p being Rational st k <> 0 & p = m / k holds

ex l being Element of NAT st

( m = (numerator p) * l & k = (denominator p) * l )

for m being Integer

for p being Rational st k <> 0 & p = m / k holds

ex l being Element of NAT st

( m = (numerator p) * l & k = (denominator p) * l )

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 )

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 Th29: :: RAT_1:29

for p being Rational

for l being Element of NAT holds

( not 1 < l or for m being Integer

for k being Element of NAT holds

( not numerator p = m * l or not denominator p = k * l ) )

for l being Element of NAT holds

( not 1 < l or for m being Integer

for k being Element of NAT holds

( not numerator p = m * l or not denominator p = k * l ) )

proof end;

theorem Th30: :: RAT_1:30

for k being Element of NAT

for m being Integer

for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds

( not 1 < l or for m1 being Integer

for k1 being Element of NAT holds

( not m = m1 * l or not k = k1 * l ) ) ) holds

( k = denominator p & m = numerator p )

for m being Integer

for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds

( not 1 < l or for m1 being Integer

for k1 being Element of NAT holds

( not m = m1 * l or not k = k1 * l ) ) ) holds

( k = denominator p & m = numerator p )

proof end;

theorem :: RAT_1:40

for a being real number

for p being Rational holds

( a <= p iff a * (denominator p) <= numerator p )

for p being Rational holds

( a <= p iff a * (denominator p) <= numerator p )

proof end;

theorem :: RAT_1:42

for p, q being Rational holds

( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )

( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )

proof end;

theorem Th43: :: RAT_1:43

for p being Rational holds

( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )

( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )

proof end;

theorem Th44: :: RAT_1:44

for p, q being Rational holds

( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )

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

( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) )

proof end;

:: or of natural denominator and numerator, etc., are all rational numbers.