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

for b_{1} being set holds

( b_{1} = RAT iff for x being object 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 object holds

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

compatibility for x being object 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 object holds

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

for b

( b

( x in b

:: deftheorem defines rational RAT_1:def 2 :

for r being object holds

( r is rational iff r in RAT );

for r being object 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;

::$CT 3

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

:: any two distinct real numbers.

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

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

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

ex b_{1} being Nat st

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

for k being Nat st k <> 0 & p = n / k holds

b_{1} <= k ) )

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

for k being 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 Nat st k <> 0 & p = n / k holds

b_{2} <= k ) holds

b_{1} = b_{2}

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

ex b

( b

for k being Nat st k <> 0 & p = n / k holds

b

proof end;

uniqueness for b

for k being Nat st k <> 0 & p = n / k holds

b

for k being 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 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 Nat st k <> 0 & p = n / k holds

b_{2} <= k ) ) );

for p being Rational

for b

( b

for k being 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).

registration
end;

theorem Th12: :: RAT_1:15

for p being Rational holds

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

( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator 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 Th23: :: 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 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 )

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 )

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

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 )

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 :: 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 Th40: :: 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 Th41: :: 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.