:: Basic Properties of Rational Numbers :: by Andrzej Kondracki :: :: Received July 10, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XREAL_0, ORDINAL1, SUBSET_1, INT_1, TARSKI, ARYTM_3, XBOOLE_0, CARD_1, ARYTM_0, RELAT_1, REAL_1, ARYTM_2, ORDINAL2, ARYTM_1, ZFMISC_1, XXREAL_0, NAT_1, RAT_1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL3, ARYTM_3, ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1, ARYTM_1, XXREAL_0; constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, INT_1, ORDINAL3; registrations ORDINAL1, ARYTM_3, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL3; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x for object, a,b for Real, k,k1,i1,j1,w for Nat, m,m1,n,n1 for Integer; definition redefine func RAT means :: RAT_1:def 1 x in it iff ex m,n st x = m/n; end; definition let r be object; attr r is rational means :: RAT_1:def 2 r in RAT; end; registration cluster rational for Real; end; registration cluster rational for number; end; definition mode Rational is rational Number; end; theorem :: RAT_1:1 x in RAT implies ex m,n st n<>0 & x = m/n; theorem :: RAT_1:2 x is rational implies ex m,n st n<>0 & x = m/n; registration cluster rational -> real for object; end; theorem :: RAT_1:3 m/n is rational; registration cluster integer -> rational for object; end; reserve p,q for Rational; :: 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; cluster p+q -> rational; cluster p-q -> rational; cluster p/q -> rational; end; registration let p be Rational; cluster -p -> rational; cluster p" -> rational; end; ::\$CT 3 :: RAT is dense, that is there exists at least one rational number between :: any two distinct real numbers. theorem :: RAT_1:7 a0 & p=m/k; :: 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 :: RAT_1:9 ex m,k st k<>0 & p=m/k & for n,w st w<>0 & p=n/w holds k<=w; definition let p be Rational; func denominator(p) -> Nat means :: RAT_1:def 3 it<>0 & (ex m st p=m/it) & for n,k st k<>0 & p=n/k holds it<=k; end; definition let p be Rational; func numerator(p) -> Integer equals :: RAT_1:def 4 denominator(p)*p; end; :: Some basic theorems concerning p, numerator(p) and denominator(p). theorem :: RAT_1:10 0 < denominator(p); registration let p; cluster denominator(p) -> positive; end; theorem :: RAT_1:11 1 <= denominator(p); theorem :: RAT_1:12 0 < denominator(p)"; theorem :: RAT_1:13 1 >= denominator(p)"; theorem :: RAT_1:14 numerator(p)=0 iff p=0; theorem :: RAT_1:15 p=numerator(p)/denominator(p) & p=numerator(p)*denominator(p)"; theorem :: RAT_1:16 p<>0 implies denominator(p)=numerator(p)/p; theorem :: RAT_1:17 p is Integer implies denominator(p)=1 & numerator(p)=p; theorem :: RAT_1:18 (numerator(p)=p or denominator(p)=1) implies p is Integer; theorem :: RAT_1:19 numerator(p)=p iff denominator(p)=1; theorem :: RAT_1:20 (numerator(p)=p or denominator(p)=1) & 0<=p implies p is Element of NAT; theorem :: RAT_1:21 1denominator(p)" iff p is not integer; theorem :: RAT_1:23 numerator(p)=denominator(p) iff p=1; theorem :: RAT_1:24 numerator(p)=-denominator(p) iff p=-1; theorem :: RAT_1:25 -numerator(p)=denominator(p) iff p=-1; :: We can multiple the numerator and the denominator of any rational number :: by any integer (natural) number which is not equal to zero. theorem :: RAT_1:26 m<>0 implies p=(numerator(p)*m)/(denominator(p)*m); theorem :: RAT_1:27 k<>0 & p=m/k implies ex w st m=numerator(p)*w & k=denominator(p)*w; theorem :: RAT_1:28 p=m/n & n<>0 implies ex m1 st m=numerator(p)*m1 & n=denominator(p)*m1; :: Fraction numerator(p)/denominator(p) is irreducible. theorem :: RAT_1:29 not ex w st 10 & not ex w st 1