:: Basic Properties of Rational Numbers :: 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 proofend; 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 proofend; Lm4: for x being set st x in RAT holds ex m, n being Integer st x = m / n proofend; Lm5: for x being set for l being Element of NAT for m being Integer st x = m / l holds x in RAT proofend; Lm6: for x being set for m, n being Integer st x = m / n holds x in RAT proofend; definition 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 b1 being set holds ( b1 = RAT iff for x being set holds ( x in b1 iff ex m, n being Integer st x = m / n ) ) proofend; end; :: deftheorem Def1 defines RAT RAT_1:def_1_:_ for b1 being set holds ( b1 = RAT iff for x being set holds ( x in b1 iff ex m, n being Integer st x = m / n ) ); definition let r be number ; attrr is rational means :Def2: :: RAT_1:def 2 r in RAT ; end; :: deftheorem Def2 defines rational RAT_1:def_2_:_ for r being number holds ( r is rational iff r in RAT ); registration cluster ext-real V31() real rational for Element of REAL ; existence ex b1 being Real st b1 is rational proofend; end; registration cluster rational for set ; existence ex b1 being number st b1 is rational proofend; end; definition mode Rational is rational number ; end; theorem Th1: :: RAT_1:1 for x being set st x in RAT holds ex m, n being Integer st ( n <> 0 & x = m / n ) proofend; theorem Th2: :: RAT_1:2 for x being set st x is Rational holds ex m, n being Integer st ( n <> 0 & x = m / n ) proofend; registration cluster rational -> real for set ; coherence for b1 being number st b1 is rational holds b1 is real proofend; end; theorem Th3: :: RAT_1:3 for m, n being Integer holds m / n is rational proofend; registration cluster integer -> rational for set ; coherence for b1 being number st b1 is integer holds b1 is rational proofend; 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; clusterp * q -> rational ; coherence p * q is rational proofend; clusterp + q -> rational ; coherence p + q is rational proofend; clusterp - q -> rational ; coherence p - q is rational proofend; clusterp / q -> rational ; coherence p / q is rational proofend; end; registration let p be Rational; cluster - p -> rational ; coherence - p is rational proofend; clusterp " -> rational ; coherence p " is rational proofend; end; theorem :: RAT_1:4 canceled; theorem :: RAT_1:5 canceled; theorem :: RAT_1:6 canceled; :: 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 number st a < b holds ex p being Rational st ( a < p & p < b ) proofend; theorem Th8: :: RAT_1:8 for p being Rational ex m being Integer ex k being Element of NAT st ( k <> 0 & p = m / k ) proofend; :: 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 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 ) ) proofend; definition let p be Rational; 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 ex b1 being Element of NAT st ( b1 <> 0 & ex m being Integer st p = m / b1 & ( for n being Integer for k being Element of NAT st k <> 0 & p = n / k holds b1 <= k ) ) proofend; uniqueness for b1, b2 being Element of NAT st b1 <> 0 & ex m being Integer st p = m / b1 & ( for n being Integer for k being Element of NAT st k <> 0 & p = n / k holds b1 <= k ) & b2 <> 0 & ex m being Integer st p = m / b2 & ( for n being Integer for k being Element of NAT st k <> 0 & p = n / k holds b2 <= k ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines denominator RAT_1:def_3_:_ for p being Rational for b2 being Element of NAT holds ( b2 = denominator p iff ( b2 <> 0 & ex m being Integer st p = m / b2 & ( for n being Integer for k being Element of NAT st k <> 0 & p = n / k holds b2 <= k ) ) ); definition let p be Rational; func numerator p -> Integer equals :: RAT_1:def 4 (denominator p) * p; coherence (denominator p) * p is Integer proofend; 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 Th10: :: RAT_1:10 for p being Rational holds 0 < denominator p proofend; theorem Th11: :: RAT_1:11 for p being Rational holds 1 <= denominator p proofend; theorem Th12: :: RAT_1:12 for p being Rational holds 0 < (denominator p) " proofend; theorem Th13: :: RAT_1:13 for p being Rational holds 1 >= (denominator p) " proofend; theorem Th14: :: RAT_1:14 for p being Rational holds ( numerator p = 0 iff p = 0 ) proofend; 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) ) proofend; theorem :: RAT_1:16 for p being Rational st p <> 0 holds denominator p = (numerator p) / p proofend; theorem Th17: :: RAT_1:17 for p being Rational st p is Integer holds ( denominator p = 1 & numerator p = p ) proofend; theorem Th18: :: RAT_1:18 for p being Rational st ( numerator p = p or denominator p = 1 ) holds p is Integer proofend; theorem :: RAT_1:19 for p being Rational holds ( numerator p = p iff denominator p = 1 ) by Th17; theorem :: RAT_1:20 for p being Rational st ( numerator p = p or denominator p = 1 ) & 0 <= p holds p is Element of NAT proofend; theorem :: RAT_1:21 for p being Rational holds ( 1 < denominator p iff not p is integer ) proofend; Lm7: 1 " = 1 ; theorem :: RAT_1:22 for p being Rational holds ( 1 > (denominator p) " iff not p is integer ) proofend; theorem Th23: :: RAT_1:23 for p being Rational holds ( numerator p = denominator p iff p = 1 ) proofend; theorem Th24: :: RAT_1:24 for p being Rational holds ( numerator p = - (denominator p) iff p = - 1 ) proofend; theorem :: RAT_1:25 for p being Rational holds ( - (numerator p) = denominator p iff p = - 1 ) proofend; :: We can multiple the numerator and the denominator of any rational number :: 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) proofend; 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 ) proofend; 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 ) proofend; :: 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 ) ) proofend; 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 ) proofend; theorem Th31: :: RAT_1:31 for p being Rational holds ( p < - 1 iff numerator p < - (denominator p) ) proofend; theorem Th32: :: RAT_1:32 for p being Rational holds ( p <= - 1 iff numerator p <= - (denominator p) ) proofend; theorem :: RAT_1:33 for p being Rational holds ( p < - 1 iff denominator p < - (numerator p) ) proofend; theorem :: RAT_1:34 for p being Rational holds ( p <= - 1 iff denominator p <= - (numerator p) ) proofend; theorem Th35: :: RAT_1:35 for p being Rational holds ( p < 1 iff numerator p < denominator p ) proofend; theorem :: RAT_1:36 for p being Rational holds ( p <= 1 iff numerator p <= denominator p ) proofend; theorem :: RAT_1:37 for p being Rational holds ( p < 0 iff numerator p < 0 ) proofend; theorem Th38: :: RAT_1:38 for p being Rational holds ( p <= 0 iff numerator p <= 0 ) proofend; theorem Th39: :: RAT_1:39 for a being real number for p being Rational holds ( a < p iff a * (denominator p) < numerator p ) proofend; theorem :: RAT_1:40 for a being real number for p being Rational holds ( a <= p iff a * (denominator p) <= numerator p ) proofend; theorem :: RAT_1:41 for p, q being Rational st denominator p = denominator q & numerator p = numerator q holds p = q proofend; theorem :: RAT_1:42 for p, q being Rational holds ( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) ) proofend; theorem Th43: :: RAT_1:43 for p being Rational holds ( denominator (- p) = denominator p & numerator (- p) = - (numerator p) ) proofend; 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 ) ) proofend; theorem :: RAT_1:45 for p, q being Rational holds ( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) ) proofend;