rat_1.miz



    begin

    reserve x for object,

a,b for Real,

k,k1,i1,j1,w for Nat,

m,m1,n,n1 for Integer;

    

     Lm1: omega c= (({ [c, d] where c,d be Element of omega : (c,d) are_coprime & d <> {} } \ the set of all [k, 1] where k be Element of omega ) \/ omega ) by XBOOLE_1: 7;

    

     Lm2: ( quotient (i1,j1)) = (i1 / j1)

    proof

      set x = ( quotient (i1,j1));

      per cases ;

        suppose

         A1: j1 = {} ;

        

        hence x = {} by ARYTM_3:def 10

        .= (i1 / j1) by A1;

      end;

        suppose

         A2: j1 <> 0 ;

        ( + (( In ( 0 , REAL )),( opp ( In ( 0 , REAL ))))) = 0 by ARYTM_0:def 3;

        then

         A3: ( opp ( In ( 0 , REAL ))) = 0 by ARYTM_0: 11;

        reconsider y = 1 as Element of REAL by NUMBERS: 19;

        (j1 * (j1 " )) = 1 by A2, XCMPLX_0:def 7;

        then

        consider x1,x2,y1,y2 be Element of REAL such that

         A4: j1 = [*x1, x2*] and

         A5: (j1 " ) = [*y1, y2*] and

         A6: y = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;

        

         A7: j1 in REAL by XREAL_0:def 1;

        ( + (( * (x1,y2)),( * (x2,y1)))) = 0 by A6, ARYTM_0: 24;

        

        then

         A8: 1 = ( + (( * (x1,y1)),( opp ( * (x2,y2))))) by A6, ARYTM_0:def 5

        .= ( + (( * (x1,y1)),( opp ( In ( 0 , REAL ))))) by A4, ARYTM_0: 12, ARYTM_0: 24, A7

        .= ( * (x1,y1)) by A3, ARYTM_0: 11;

        j1 in REAL by XREAL_0:def 1;

        then x2 = 0 by A4, ARYTM_0: 24;

        then

         A9: j1 = x1 by A4, ARYTM_0:def 5;

        then x1 in omega by ORDINAL1:def 12;

        then

        reconsider xx = x1 as Element of RAT+ by Lm1;

        consider yy be Element of RAT+ such that

         A10: (xx *' yy) = one by A2, A9, ARYTM_3: 54;

        reconsider xx1 = xx, yy1 = yy as Element of REAL+ by ARYTM_2: 1;

        

         A11: ex x9,y9 be Element of RAT+ st xx1 = x9 & yy1 = y9 & (xx1 *' yy1) = (x9 *' y9) by ARYTM_2: 21;

        reconsider xx1, yy1 as Element of REAL by ARYTM_0: 1;

        ex x9,y9 be Element of REAL+ st xx1 = x9 & yy1 = y9 & ( * (xx1,yy1)) = (x9 *' y9) by ARYTM_0:def 2;

        then

         A12: yy = y1 by A2, A9, A8, A10, A11, ARYTM_0: 18;

        then

         A13: y1 in RAT+ ;

        (j1 " ) in REAL by XREAL_0:def 1;

        then y2 = 0 by A5, ARYTM_0: 24;

        then

         A14: (j1 " ) = y1 by A5, ARYTM_0:def 5;

        

         A15: j1 in omega by ORDINAL1:def 12;

        then

        reconsider a = x, b = j1 as Element of RAT+ by Lm1;

        consider x91,x92,y91,y92 be Element of REAL such that

         A16: i1 = [*x91, x92*] and

         A17: (j1 " ) = [*y91, y92*] and

         A18: (i1 * (j1 " )) = [*( + (( * (x91,y91)),( opp ( * (x92,y92))))), ( + (( * (x91,y92)),( * (x92,y91))))*] by XCMPLX_0:def 5;

        (i1 * (j1 " )) in REAL by XREAL_0:def 1;

        then

         A19: ( + (( * (x91,y92)),( * (x92,y91)))) = 0 by A18, ARYTM_0: 24;

        x1 in omega by A9, ORDINAL1:def 12;

        then

        consider x19,y19 be Element of REAL+ such that

         A20: x1 = x19 and

         A21: y1 = y19 and

         A22: ( * (x1,y1)) = (x19 *' y19) by A13, ARYTM_0:def 2, ARYTM_2: 1, ARYTM_2: 2;

        

         A23: ex x199,y199 be Element of RAT+ st x19 = x199 & y19 = y199 & (x19 *' y19) = (x199 *' y199) by A9, A12, A15, A20, A21, Lm1, ARYTM_2: 21;

        (j1 " ) in REAL by XREAL_0:def 1;

        then

         A24: y92 = 0 by A17, ARYTM_0: 24;

        then (j1 " ) = y91 by A17, ARYTM_0:def 5;

        

        then

         A25: (i1 * (j1 " )) = ( + (( * (x91,y1)),( opp ( * (x92,( In ( 0 , REAL ))))))) by A14, A18, A24, A19, ARYTM_0:def 5

        .= ( + (( * (x91,y1)),( In ( 0 , REAL )))) by A3, ARYTM_0: 12

        .= ( * (x91,y1)) by ARYTM_0: 11;

        i1 in REAL by XREAL_0:def 1;

        then x92 = 0 by A16, ARYTM_0: 24;

        then

         A26: i1 = x91 by A16, ARYTM_0:def 5;

        then

         A27: x91 in omega by ORDINAL1:def 12;

        then x91 in RAT+ by Lm1;

        then

        consider x9,y9 be Element of REAL+ such that

         A28: x91 = x9 and

         A29: y1 = y9 and

         A30: (i1 * (j1 " )) = (x9 *' y9) by A25, A13, ARYTM_0:def 2, ARYTM_2: 1;

        consider x99,y99 be Element of RAT+ such that

         A31: x9 = x99 and

         A32: y9 = y99 and

         A33: (i1 * (j1 " )) = (x99 *' y99) by A27, A12, A28, A29, A30, Lm1, ARYTM_2: 21;

        (a *' b) = (( quotient (i1,j1)) *' ( quotient (j1, one ))) by ARYTM_3: 40

        .= ( quotient ((i1 *^ j1),(j1 *^ one ))) by ARYTM_3: 49

        .= (( quotient (i1, one )) *' ( quotient (j1,j1))) by ARYTM_3: 49

        .= (( quotient (i1, one )) *' one ) by A2, ARYTM_3: 41

        .= ( quotient (i1, one )) by ARYTM_3: 53

        .= i1 by ARYTM_3: 40

        .= (x99 *' one ) by A26, A28, A31, ARYTM_3: 53

        .= ((x99 *' y99) *' b) by A9, A8, A29, A32, A20, A21, A22, A23, ARYTM_3: 52;

        hence thesis by A2, A33, ARYTM_3: 56;

      end;

    end;

    

     Lm3: for Z9 be Element of REAL+ st Z9 = 0 holds for x9 be Element of REAL+ st x9 = a holds (Z9 - x9) = ( - a)

    proof

      let Z9 be Element of REAL+ such that

       A0: Z9 = 0 ;

      let xx be Element of REAL+ such that

       A1: xx = a;

      per cases ;

        suppose xx = 0 ;

        hence thesis by A0, A1, ARYTM_1: 18;

      end;

        suppose

         A2: xx <> 0 ;

        set b = (Z9 - xx);

        

         A3: Z9 <=' xx by A0, ARYTM_1: 6;

        then not xx <=' Z9 by A0, A2, ARYTM_1: 4;

        then

         A4: b = [ {} , (xx -' Z9)] by ARYTM_1:def 2;

        now

          assume b = [ 0 , 0 ];

          then (xx -' Z9) = 0 by A4, XTUPLE_0: 1;

          hence contradiction by A0, A2, A3, ARYTM_1: 10;

        end;

        then

         A5: not b in { [ 0 , 0 ]} by TARSKI:def 1;

        

         A6: (xx -' Z9) = ((xx -' Z9) + Z9) by A0, ARYTM_2:def 8

        .= xx by A3, ARYTM_1:def 1;

         0 in { 0 } by TARSKI:def 1;

        then

         A7: b in [: { 0 }, REAL+ :] by A4, ZFMISC_1: 87;

        then b in ( REAL+ \/ [: { 0 }, REAL+ :]) by XBOOLE_0:def 3;

        then

        reconsider b as Element of REAL by A5, NUMBERS:def 1, XBOOLE_0:def 5;

        consider x1,x2,y1,y2 be Element of REAL such that

         A8: a = [*x1, x2*] and

         A9: b = [*y1, y2*] and

         A10: (a + b) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

        (a + b) in REAL by XREAL_0:def 1;

        then ( + (x2,y2)) = 0 by A10, ARYTM_0: 24;

        then

         A11: (a + b) = ( + (x1,y1)) by A10, ARYTM_0:def 5;

        a in REAL by XREAL_0:def 1;

        then x2 = 0 by A8, ARYTM_0: 24;

        then

         A12: a = x1 by A8, ARYTM_0:def 5;

        y2 = 0 by A9, ARYTM_0: 24;

        then

         A13: b = y1 by A9, ARYTM_0:def 5;

        then

        consider x9,y9 be Element of REAL+ such that

         A14: x1 = x9 and

         A15: y1 = [ 0 , y9] and

         A16: ( + (x1,y1)) = (x9 - y9) by A1, A7, A12, ARYTM_0:def 1;

        y9 = (xx -' Z9) by A4, A13, A15, XTUPLE_0: 1;

        then (a + b) = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1: 18;

        hence thesis;

      end;

    end;

    

     Lm4: x in RAT implies ex m, n st x = (m / n)

    proof

      assume

       A1: x in RAT ;

      per cases by A1, NUMBERS:def 3, XBOOLE_0:def 3;

        suppose x in RAT+ ;

        then

        reconsider x as Element of RAT+ ;

        take ( numerator x), ( denominator x);

        ( quotient (( numerator x),( denominator x))) = x by ARYTM_3: 39;

        hence thesis by Lm2;

      end;

        suppose

         A2: x in [: { 0 }, RAT+ :];

        

         A3: not x in { [ 0 , 0 ]} by A1, NUMBERS:def 3, XBOOLE_0:def 5;

        consider x1,x2 be object such that

         A4: x1 in { 0 } and

         A5: x2 in RAT+ and

         A6: x = [x1, x2] by A2, ZFMISC_1: 84;

        reconsider x2 as Element of RAT+ by A5;

        reconsider x9 = x2 as Element of REAL+ by ARYTM_2: 1;

        x = [ 0 , x9] by A4, A6, TARSKI:def 1;

        then

         A7: x2 <> 0 by A3, TARSKI:def 1;

        take m = ( - ( numerator x2)), n = ( denominator x2);

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

        

         A8: x2 = ( quotient (( numerator x2),( denominator x2))) by ARYTM_3: 39

        .= (( numerator x2) / n) by Lm2;

        x1 = 0 by A4, TARSKI:def 1;

        

        hence x = (Z9 - x9) by A6, A7, ARYTM_1: 19

        .= ( - (( numerator x2) / n)) by A8, Lm3

        .= (m / n);

      end;

    end;

    

     Lm5: x = (m / w) implies x in RAT

    proof

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

      

       A1: m is Element of INT by INT_1:def 2;

      assume

       A2: x = (m / w);

      then x in REAL by XREAL_0:def 1;

      then

       A3: not x in { [ 0 , 0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;

      reconsider w as Element of NAT by ORDINAL1:def 12;

      per cases ;

        suppose w = 0 ;

        

        then x = (m * ( 0 " )) by A2

        .= 0 ;

        then x in ( RAT+ \/ [: { 0 }, RAT+ :]) by Lm1, XBOOLE_0:def 3;

        hence thesis by A3, NUMBERS:def 3, XBOOLE_0:def 5;

      end;

        suppose ex k be Nat st m = k;

        then

        consider k be Nat such that

         A4: m = k;

        x = ( quotient (k,w)) by A2, A4, Lm2;

        then x in ( RAT+ \/ [: { 0 }, RAT+ :]) by XBOOLE_0:def 3;

        hence thesis by A3, NUMBERS:def 3, XBOOLE_0:def 5;

      end;

        suppose that

         A5: w <> 0 and

         A6: for k be Nat holds m <> k;

        consider k be Nat such that

         A7: m = ( - k) by A1, A6, INT_1:def 1;

        

         A8: (k / w) = ( quotient (k,w)) by Lm2;

        then (k / w) in RAT+ ;

        then

        reconsider x9 = (k / w) as Element of REAL+ by ARYTM_2: 1;

        

         A9: 0 in { 0 } by TARSKI:def 1;

        

         A10: x = ( - (k / w)) by A2, A7;

        m <> 0 by A6;

        then

         A11: x9 <> 0 by A2, A5, A10, XCMPLX_1: 50;

        x = (Z9 - x9) by A10, Lm3

        .= [ 0 , x9] by A11, ARYTM_1: 19;

        then x in [: { 0 }, RAT+ :] by A8, A9, ZFMISC_1: 87;

        then x in ( RAT+ \/ [: { 0 }, RAT+ :]) by XBOOLE_0:def 3;

        hence thesis by A3, NUMBERS:def 3, XBOOLE_0:def 5;

      end;

    end;

    

     Lm6: x = (m / n) implies x in RAT

    proof

      assume

       A1: x = (m / n);

      n is Element of INT by INT_1:def 2;

      then

      consider k be Nat such that

       A2: n = k or n = ( - k) by INT_1:def 1;

      per cases by A2;

        suppose n = k;

        hence thesis by A1, Lm5;

      end;

        suppose n = ( - k);

        then x = (( - m) / k) by A1, XCMPLX_1: 192;

        hence thesis by Lm5;

      end;

    end;

    definition

      :: original: RAT

      redefine

      :: RAT_1:def1

      func RAT means

      : Def1: x in it iff ex m, n st x = (m / n);

      compatibility

      proof

        let R be set;

        thus R = RAT implies for x holds x in R iff ex m, n st x = (m / n) by Lm4, Lm6;

        assume

         A1: for x holds x in R iff ex m, n st x = (m / n);

        thus R c= RAT

        proof

          let x be object;

          assume x in R;

          then ex m, n st x = (m / n) by A1;

          hence thesis by Lm6;

        end;

        let x be object;

        assume x in RAT ;

        then ex m, n st x = (m / n) by Lm4;

        hence thesis by A1;

      end;

    end

    definition

      let r be object;

      :: RAT_1:def2

      attr r is rational means r in RAT ;

    end

    registration

      cluster rational for Real;

      existence

      proof

        reconsider a = 0 , b = 1 as Integer;

        take x = (a / b);

        thus x in RAT by Def1;

      end;

    end

    registration

      cluster rational for number;

      existence

      proof

        reconsider a = 0 , b = 1 as Integer;

        take x = (a / b);

        thus x in RAT by Def1;

      end;

    end

    definition

      mode Rational is rational Number;

    end

    theorem :: RAT_1:1

    

     Th1: x in RAT implies ex m, n st n <> 0 & x = (m / n)

    proof

      assume

       A1: x in RAT ;

      per cases ;

        suppose x = 0 ;

        then x = ( 0 / 1);

        hence thesis;

      end;

        suppose

         A2: x <> 0 ;

        consider m, n such that

         A3: x = (m / n) by A1, Def1;

        take m, n;

        hereby

          assume n = 0 ;

          then (n " ) = 0 ;

          hence contradiction by A2, A3;

        end;

        thus thesis by A3;

      end;

    end;

    theorem :: RAT_1:2

    

     Th2: x is rational implies ex m, n st n <> 0 & x = (m / n) by Th1;

    registration

      cluster rational -> real for object;

      coherence by NUMBERS: 12;

    end

    theorem :: RAT_1:3

    

     Th3: (m / n) is rational by Def1;

    registration

      cluster integer -> rational for object;

      coherence

      proof

        let x be object;

        assume x is integer;

        then

        reconsider x as Integer;

        x = (x / 1);

        hence thesis by Th3;

      end;

    end

    reserve p,q for Rational;

    registration

      let p,q be Rational;

      cluster (p * q) -> rational;

      coherence

      proof

        consider m2,n2 be Integer such that n2 <> 0 and

         A1: q = (m2 / n2) by Th2;

        consider m1,n1 be Integer such that n1 <> 0 and

         A2: p = (m1 / n1) by Th2;

        (p * q) = ((m1 * m2) / (n1 * n2)) by A2, A1, XCMPLX_1: 76;

        hence thesis by Th3;

      end;

      cluster (p + q) -> rational;

      coherence

      proof

        consider m2,n2 be Integer such that

         A3: n2 <> 0 and

         A4: q = (m2 / n2) by Th2;

        consider m1,n1 be Integer such that

         A5: n1 <> 0 and

         A6: p = (m1 / n1) by Th2;

        (p + q) = (((m1 * n2) + (m2 * n1)) / (n1 * n2)) by A5, A6, A3, A4, XCMPLX_1: 116;

        hence thesis by Th3;

      end;

      cluster (p - q) -> rational;

      coherence

      proof

        consider m2,n2 be Integer such that

         A7: n2 <> 0 and

         A8: q = (m2 / n2) by Th2;

        consider m1,n1 be Integer such that

         A9: n1 <> 0 and

         A10: p = (m1 / n1) by Th2;

        (p - q) = (((m1 * n2) - (m2 * n1)) / (n1 * n2)) by A9, A10, A7, A8, XCMPLX_1: 130;

        hence thesis by Th3;

      end;

      cluster (p / q) -> rational;

      coherence

      proof

        consider m1,n1 be Integer such that n1 <> 0 and

         A11: p = (m1 / n1) by Th2;

        consider m2,n2 be Integer such that n2 <> 0 and

         A12: q = (m2 / n2) by Th2;

        (p / q) = (p * (1 / (m2 / n2))) by A12

        .= (p * ((1 * n2) / m2)) by XCMPLX_1: 77

        .= ((m1 * n2) / (n1 * m2)) by A11, XCMPLX_1: 76;

        hence thesis by Th3;

      end;

    end

    registration

      let p be Rational;

      cluster ( - p) -> rational;

      coherence

      proof

        consider m, n such that n <> 0 and

         A1: p = (m / n) by Th2;

        ( - p) = (( - m) / n) by A1;

        hence thesis;

      end;

      cluster (p " ) -> rational;

      coherence

      proof

        (p " ) = (1 / p);

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: RAT_1:7

    a < b implies ex p st a < p & p < b

    proof

      set d = (b - a);

      set m = ( [\(d " )/] + 1);

      set l = ( [\(m * a)/] + 1);

      set p = (l / m);

      assume a < b;

      then

       A1: (a - a) < (b - a) by XREAL_1: 9;

      then

       A2: 0 < m by INT_1: 29;

      ((d " ) - 1) < [\(d " )/] by INT_1:def 6;

      then (d " ) < ( [\(d " )/] + 1) by XREAL_1: 19;

      then ((d " ) * d) < (m * d) by A1, XREAL_1: 68;

      then

       A3: 1 < (m * d) by A1, XCMPLX_0:def 7;

      take p;

      

       A4: 0 <> m by A1, INT_1: 29;

      ((m * a) - 1) < [\(m * a)/] by INT_1:def 6;

      then (m * a) < ( [\(m * a)/] + 1) by XREAL_1: 19;

      then ((m " ) * (m * a)) < ((m " ) * l) by A2, XREAL_1: 68;

      then (((m " ) * m) * a) < ((m " ) * l);

      then (1 * a) < ((m " ) * l) by A4, XCMPLX_0:def 7;

      hence a < p;

       [\(m * a)/] <= (m * a) by INT_1:def 6;

      then ( [\(m * a)/] + 1) < ((m * a) + (m * d)) by A3, XREAL_1: 8;

      then ((m " ) * l) < ((m " ) * (m * b)) by A2, XREAL_1: 68;

      then ((m " ) * l) < (((m " ) * m) * b);

      then ((m " ) * l) < (1 * b) by A4, XCMPLX_0:def 7;

      hence p < b;

    end;

    theorem :: RAT_1:8

    

     Th5: ex m, k st k <> 0 & p = (m / k)

    proof

      consider m, n such that

       A1: n <> 0 and

       A2: p = (m / n) by Th2;

      per cases by A1;

        suppose 0 < n;

        then n is Element of NAT by INT_1: 3;

        hence thesis by A1, A2;

      end;

        suppose

         A3: n < 0 ;

        

         A4: p = ( - (( - m) / n)) by A2

        .= (( - m) / ( - n)) by XCMPLX_1: 188;

        

         A5: ( - n) <> 0 by A1;

        ( - n) is Element of NAT by A3, INT_1: 3;

        hence thesis by A4, A5;

      end;

    end;

    theorem :: RAT_1:9

    

     Th6: ex m, k st k <> 0 & p = (m / k) & for n, w st w <> 0 & p = (n / w) holds k <= w

    proof

      defpred P[ Nat] means ($1 <> 0 & ex m1 st p = (m1 / $1));

      ex m, k st k <> 0 & p = (m / k) by Th5;

      then

       A1: ex l be Nat st P[l];

      ex k1 be Nat st P[k1] & for l1 be Nat st P[l1] holds k1 <= l1 from NAT_1:sch 5( A1);

      then

      consider k1 be Nat such that

       A2: k1 <> 0 and

       A3: ex m1 st p = (m1 / k1) and

       A4: for l1 be Nat st (l1 <> 0 & ex n1 st p = (n1 / l1)) holds k1 <= l1;

      reconsider k1 as Element of NAT by ORDINAL1:def 12;

      consider m1 such that

       A5: p = (m1 / k1) and

       A6: for l1 be Nat st (l1 <> 0 & ex n1 st p = (n1 / l1)) holds k1 <= l1 by A3, A4;

      take m1, k1;

      thus k1 <> 0 by A2;

      thus (m1 / k1) = p by A5;

      thus thesis by A6;

    end;

    definition

      let p be Rational;

      :: RAT_1:def3

      func denominator (p) -> Nat means

      : Def3: it <> 0 & (ex m st p = (m / it )) & for n, k st k <> 0 & p = (n / k) holds it <= k;

      existence

      proof

        consider m, k such that

         A1: k <> 0 and

         A2: p = (m / k) and

         A3: for n, w st w <> 0 & p = (n / w) holds k <= w by Th6;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        take IT = k;

        thus thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let k,l be Nat such that

         A4: k <> 0 and

         A5: ex m st p = (m / k) and

         A6: for m1, k1 st k1 <> 0 & p = (m1 / k1) holds k <= k1 and

         A7: l <> 0 and

         A8: ex n st p = (n / l) and

         A9: for n1, k1 st k1 <> 0 & p = (n1 / k1) holds l <= k1;

        

         A10: l <= k by A4, A5, A9;

        k <= l by A6, A7, A8;

        hence thesis by A10, XXREAL_0: 1;

      end;

    end

    definition

      let p be Rational;

      :: RAT_1:def4

      func numerator (p) -> Integer equals (( denominator p) * p);

      coherence

      proof

        

         A1: ( denominator p) <> 0 by Def3;

        ex m st p = (m / ( denominator p)) by Def3;

        hence thesis by A1, XCMPLX_1: 87;

      end;

    end

    theorem :: RAT_1:10

    

     Th7: 0 < ( denominator p)

    proof

       0 <> ( denominator p) by Def3;

      hence thesis;

    end;

    registration

      let p;

      cluster ( denominator p) -> positive;

      coherence by Th7;

    end

    theorem :: RAT_1:11

    

     Th8: 1 <= ( denominator p)

    proof

      ( 0 + 1) <= ( denominator p) by NAT_1: 13;

      hence thesis;

    end;

    theorem :: RAT_1:12

     0 < (( denominator p) " );

    theorem :: RAT_1:13

    

     Th10: 1 >= (( denominator p) " )

    proof

      (1 * (( denominator p) " )) <= (( denominator p) * (( denominator p) " )) by Th8, XREAL_1: 64;

      hence thesis by XCMPLX_0:def 7;

    end;

    theorem :: RAT_1:14

    

     Th11: ( numerator p) = 0 iff p = 0 by XCMPLX_1: 6;

    theorem :: RAT_1:15

    

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

    proof

      set x = ( denominator p);

      

      thus (( numerator p) / ( denominator p)) = (p * (x * (x " )))

      .= (p * 1) by XCMPLX_0:def 7

      .= p;

      hence thesis;

    end;

    theorem :: RAT_1:16

    p <> 0 implies ( denominator p) = (( numerator p) / p)

    proof

      

       A1: (((p " ) * p) * ( denominator p)) = ((p " ) * ( numerator p));

      assume p <> 0 ;

      then (1 * ( denominator p)) = ((p " ) * ( numerator p)) by A1, XCMPLX_0:def 7;

      hence thesis;

    end;

    theorem :: RAT_1:17

    

     Th14: p is Integer implies ( denominator p) = 1 & ( numerator p) = p

    proof

      assume p is Integer;

      then

      reconsider m = p as Integer;

      p = (m / 1);

      then

       A1: ( denominator p) <= 1 by Def3;

      1 <= ( denominator p) by Th8;

      hence ( denominator p) = 1 by A1, XXREAL_0: 1;

      hence thesis;

    end;

    theorem :: RAT_1:18

    

     Th15: (( numerator p) = p or ( denominator p) = 1) implies p is Integer

    proof

      assume

       A1: ( numerator p) = p or ( denominator p) = 1;

      per cases by A1;

        suppose ( numerator p) = p;

        hence thesis;

      end;

        suppose ( denominator p) = 1;

        then ( numerator p) = p;

        hence thesis;

      end;

    end;

    theorem :: RAT_1:19

    ( numerator p) = p iff ( denominator p) = 1 by Th14;

    theorem :: RAT_1:20

    (( numerator p) = p or ( denominator p) = 1) & 0 <= p implies p is Element of NAT

    proof

      assume that

       A1: ( numerator p) = p or ( denominator p) = 1 and

       A2: 0 <= p;

      p is Integer by A1, Th15;

      hence thesis by A2, INT_1: 3;

    end;

    theorem :: RAT_1:21

    1 < ( denominator p) iff not p is integer

    proof

      now

        assume

         A1: not p is Integer;

        ( denominator p) >= 1 by Th8;

        hence ( denominator p) > 1 by A1, Th15, XXREAL_0: 1;

      end;

      hence thesis by Th14;

    end;

    

     Lm7: (1 " ) = 1;

    theorem :: RAT_1:22

    1 > (( denominator p) " ) iff not p is integer

    proof

      

       A1: (( denominator p) " ) <= 1 by Th10;

      now

        assume not p is Integer;

        then (( denominator p) " ) <> 1 by Lm7, Th15;

        hence (( denominator p) " ) < 1 by A1, XXREAL_0: 1;

      end;

      hence thesis by Lm7, Th14;

    end;

    theorem :: RAT_1:23

    

     Th20: ( numerator p) = ( denominator p) iff p = 1

    proof

      hereby

        assume ( numerator p) = ( denominator p);

        then (( numerator p) / ( denominator p)) = 1 by XCMPLX_1: 60;

        hence p = 1 by Th12;

      end;

      thus thesis;

    end;

    theorem :: RAT_1:24

    

     Th21: ( numerator p) = ( - ( denominator p)) iff p = ( - 1)

    proof

      hereby

        assume ( numerator p) = ( - ( denominator p));

        

        hence p = (( - ( denominator p)) / ( denominator p)) by Th12

        .= ( - (( denominator p) / ( denominator p)))

        .= ( - 1) by XCMPLX_1: 60;

      end;

      thus thesis;

    end;

    theorem :: RAT_1:25

    ( - ( numerator p)) = ( denominator p) iff p = ( - 1)

    proof

      ( - ( numerator p)) = ( denominator p) iff ( numerator p) = ( - ( denominator p));

      hence thesis by Th21;

    end;

    theorem :: RAT_1:26

    

     Th23: m <> 0 implies p = ((( numerator p) * m) / (( denominator p) * m))

    proof

      assume m <> 0 ;

      then (( numerator p) / ( denominator p)) = ((( numerator p) * m) / (( denominator p) * m)) by XCMPLX_1: 91;

      hence thesis by Th12;

    end;

    theorem :: RAT_1:27

    

     Th24: k <> 0 & p = (m / k) implies ex w st m = (( numerator p) * w) & k = (( denominator p) * w)

    proof

      assume that

       A1: k <> 0 and

       A2: p = (m / k);

      

       A3: (p * k) = m by A1, A2, XCMPLX_1: 87;

      defpred P[ Nat] means ($1 * ( denominator p)) <= k;

      

       A5: for l be Nat st P[l] holds l <= k

      proof

        ( 0 + 1) <= ( denominator p) by NAT_1: 13;

        then

         A6: (k * 1) <= (k * ( denominator p)) by NAT_1: 4;

        let l be Nat such that

         A7: (l * ( denominator p)) <= k;

        assume not thesis;

        then (k * ( denominator p)) < (l * ( denominator p)) by XREAL_1: 68;

        hence contradiction by A7, A6, XXREAL_0: 2;

      end;

      

       A8: (1 * ( denominator p)) <= k by A1, A2, Def3;

      then

       A9: ex l1 be Nat st P[l1];

      consider l be Nat such that

       A10: P[l] and

       A11: for l1 be Nat st P[l1] holds l1 <= l from NAT_1:sch 6( A5, A9);

      reconsider l as Element of NAT by ORDINAL1:def 12;

      take l;

      

       A12: 0 <> l by A8, A11;

      then

       A13: (l * ( denominator p)) <> 0 by XCMPLX_1: 6;

       A14:

      now

        assume

         A15: (l * ( denominator p)) < k;

        then ( 0 + (l * ( denominator p))) < k;

        then 0 <= (k - (l * ( denominator p))) by XREAL_1: 20;

        then

        reconsider x = (k - (l * ( denominator p))) as Element of NAT by INT_1: 3;

        

         A16: 0 <> x by A15;

        (m / k) = ((( numerator p) * l) / (l * ( denominator p))) by A2, A12, Th23;

        then p = ((m - (( numerator p) * l)) / x) by A2, A13, A15, XCMPLX_1: 123;

        then ( denominator p) <= (k - (l * ( denominator p))) by A16, Def3;

        then ((l * ( denominator p)) + (1 * ( denominator p))) <= k by XREAL_1: 19;

        then ((l + 1) * ( denominator p)) <= k;

        then (l + 1) <= l by A11;

        hence contradiction by NAT_1: 13;

      end;

      then k = (( denominator p) * l) by A10, XXREAL_0: 1;

      

      hence m = ((( numerator p) / ( denominator p)) * (( denominator p) * l)) by A3, Th12

      .= (((( numerator p) / ( denominator p)) * ( denominator p)) * l)

      .= (( numerator p) * l) by XCMPLX_1: 87;

      thus thesis by A10, A14, XXREAL_0: 1;

    end;

    theorem :: RAT_1:28

    p = (m / n) & n <> 0 implies ex m1 st m = (( numerator p) * m1) & n = (( denominator p) * m1)

    proof

      assume that

       A1: p = (m / n) and

       A2: n <> 0 ;

      per cases by A2;

        suppose n < 0 ;

        then

        reconsider x = ( - n) as Element of NAT by INT_1: 3;

        

         A3: p = ( - (( - m) / n)) by A1

        .= (( - m) / x) by XCMPLX_1: 188;

        x <> 0 by A2;

        then

        consider k such that

         A4: ( - m) = (( numerator p) * k) and

         A5: x = (( denominator p) * k) by A3, Th24;

        take y = ( - k);

        

        thus m = ( - (( numerator p) * k)) by A4

        .= (( numerator p) * y);

        

        thus n = ( - (( denominator p) * k)) by A5

        .= (( denominator p) * y);

      end;

        suppose 0 < n;

        then

        reconsider x = n as Element of NAT by INT_1: 3;

        consider k such that

         A6: m = (( numerator p) * k) and

         A7: x = (( denominator p) * k) by A1, A2, Th24;

        reconsider y = k as Integer;

        take y;

        thus thesis by A6, A7;

      end;

    end;

    theorem :: RAT_1:29

    

     Th26: not ex w st 1 < w & ex m, k st ( numerator p) = (m * w) & ( denominator p) = (k * w)

    proof

      assume not thesis;

      then

      consider w such that

       A1: 1 < w and

       A2: ex m, k st ( numerator p) = (m * w) & ( denominator p) = (k * w);

      consider m, k such that

       A3: ( numerator p) = (m * w) and

       A4: ( denominator p) = (k * w) by A2;

      

       A5: p = ((m * w) / (k * w)) by A3, A4, Th12

      .= ((m / k) * (w / w)) by XCMPLX_1: 76

      .= ((m / k) * 1) by A1, XCMPLX_1: 60

      .= (m / k);

      

       A6: k <> 0 by A4;

      then (k * 1) < (k * w) by A1, XREAL_1: 68;

      hence contradiction by A4, A6, A5, Def3;

    end;

    theorem :: RAT_1:30

    

     Th27: (p = (m / k) & k <> 0 & not ex w st 1 < w & ex m1, k1 st m = (m1 * w) & k = (k1 * w)) implies k = ( denominator p) & m = ( numerator p)

    proof

      assume that

       A1: p = (m / k) and

       A2: k <> 0 and

       A3: not ex w st 1 < w & ex m1, k1 st m = (m1 * w) & k = (k1 * w);

      consider w such that

       A4: m = (( numerator p) * w) and

       A5: k = (( denominator p) * w) by A1, A2, Th24;

       0 < w by A2, A5;

      then

       A6: ( 0 + 1) <= w by NAT_1: 13;

      w <= 1 by A3, A4, A5;

      then

       A7: w = 1 by A6, XXREAL_0: 1;

      hence k = ( denominator p) by A5;

      thus thesis by A4, A7;

    end;

    theorem :: RAT_1:31

    

     Th28: p < ( - 1) iff ( numerator p) < ( - ( denominator p))

    proof

      hereby

        assume p < ( - 1);

        then (( numerator p) / ( denominator p)) < ( - 1) by Th12;

        then ((( numerator p) / ( denominator p)) * ( denominator p)) < (( - 1) * ( denominator p)) by XREAL_1: 68;

        hence ( numerator p) < ( - ( denominator p)) by XCMPLX_1: 87;

      end;

      assume ( numerator p) < ( - ( denominator p));

      then (( numerator p) * (( denominator p) " )) < ((( - 1) * ( denominator p)) * (( denominator p) " )) by XREAL_1: 68;

      then (( numerator p) * (( denominator p) " )) < (( - 1) * (( denominator p) * (( denominator p) " )));

      then (( numerator p) * (( denominator p) " )) < (( - 1) * 1) by XCMPLX_0:def 7;

      hence p < ( - 1) by Th12;

    end;

    theorem :: RAT_1:32

    

     Th29: p <= ( - 1) iff ( numerator p) <= ( - ( denominator p))

    proof

      hereby

        assume

         A2: p <= ( - 1);

        per cases by A2, XXREAL_0: 1;

          suppose p = ( - 1);

          hence ( numerator p) <= ( - ( denominator p));

        end;

          suppose p < ( - 1);

          hence ( numerator p) <= ( - ( denominator p)) by Th28;

        end;

      end;

      assume

       A3: ( numerator p) <= ( - ( denominator p));

      per cases by A3, XXREAL_0: 1;

        suppose ( numerator p) = ( - ( denominator p));

        hence p <= ( - 1) by Th21;

      end;

        suppose ( numerator p) < ( - ( denominator p));

        hence p <= ( - 1) by Th28;

      end;

    end;

    theorem :: RAT_1:33

    p < ( - 1) iff ( denominator p) < ( - ( numerator p))

    proof

      ( denominator p) < ( - ( numerator p)) iff ( - ( - ( numerator p))) < ( - ( denominator p)) by XREAL_1: 24;

      hence thesis by Th28;

    end;

    theorem :: RAT_1:34

    p <= ( - 1) iff ( denominator p) <= ( - ( numerator p))

    proof

      ( denominator p) <= ( - ( numerator p)) iff ( - ( - ( numerator p))) <= ( - ( denominator p)) by XREAL_1: 24;

      hence thesis by Th29;

    end;

    theorem :: RAT_1:35

    

     Th32: p < 1 iff ( numerator p) < ( denominator p)

    proof

       A3:

      now

        assume ( numerator p) < ( denominator p);

        then (( numerator p) * (( denominator p) " )) < (( denominator p) * (( denominator p) " )) by XREAL_1: 68;

        then (( numerator p) * (( denominator p) " )) < 1 by XCMPLX_0:def 7;

        hence p < 1 by Th12;

      end;

      now

        assume p < 1;

        then (( numerator p) / ( denominator p)) < 1 by Th12;

        then ((( numerator p) / ( denominator p)) * ( denominator p)) < (1 * ( denominator p)) by XREAL_1: 68;

        hence ( numerator p) < ( denominator p) by XCMPLX_1: 87;

      end;

      hence thesis by A3;

    end;

    theorem :: RAT_1:36

    p <= 1 iff ( numerator p) <= ( denominator p)

    proof

       A1:

      now

        assume

         A2: p <= 1;

        per cases by A2, XXREAL_0: 1;

          suppose p = 1;

          hence ( numerator p) <= ( denominator p);

        end;

          suppose p < 1;

          hence ( numerator p) <= ( denominator p) by Th32;

        end;

      end;

      now

        assume

         A3: ( numerator p) <= ( denominator p);

        per cases by A3, XXREAL_0: 1;

          suppose ( numerator p) = ( denominator p);

          hence p <= 1 by Th20;

        end;

          suppose ( numerator p) < ( denominator p);

          hence p <= 1 by Th32;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: RAT_1:37

    p < 0 iff ( numerator p) < 0

    proof

      now

        assume p < 0 ;

        then (( numerator p) / ( denominator p)) < 0 by Th12;

        hence ( numerator p) < 0 ;

      end;

      hence thesis;

    end;

    theorem :: RAT_1:38

    

     Th35: p <= 0 iff ( numerator p) <= 0

    proof

      now

        assume

         A1: ( numerator p) <= 0 ;

        per cases by A1;

          suppose ( numerator p) = 0 ;

          hence p <= 0 by Th11;

        end;

          suppose ( numerator p) < 0 ;

          hence p <= 0 ;

        end;

      end;

      hence thesis;

    end;

    theorem :: RAT_1:39

    

     Th36: a < p iff (a * ( denominator p)) < ( numerator p)

    proof

       A3:

      now

        assume (a * ( denominator p)) < ( numerator p);

        then ((a * ( denominator p)) * (( denominator p) " )) < (( numerator p) * (( denominator p) " )) by XREAL_1: 68;

        then (a * (( denominator p) * (( denominator p) " ))) < (( numerator p) * (( denominator p) " ));

        then (a * 1) < (( numerator p) * (( denominator p) " )) by XCMPLX_0:def 7;

        hence a < p by Th12;

      end;

      thus thesis by A3, XREAL_1: 68;

    end;

    theorem :: RAT_1:40

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

    proof

       A2:

      now

        assume

         A3: (a * ( denominator p)) <= ( numerator p);

        per cases by A3, XXREAL_0: 1;

          suppose (a * ( denominator p)) = ( numerator p);

          

          then p = ((a * ( denominator p)) / (1 * ( denominator p))) by Th12

          .= ((a / 1) * (( denominator p) / ( denominator p)))

          .= a by XCMPLX_1: 60;

          hence a <= p;

        end;

          suppose (a * ( denominator p)) < ( numerator p);

          hence a <= p by Th36;

        end;

      end;

      now

        assume

         A4: a <= p;

        per cases by A4, XXREAL_0: 1;

          suppose a = p;

          hence ( numerator p) >= (a * ( denominator p));

        end;

          suppose a < p;

          hence (a * ( denominator p)) <= ( numerator p) by Th36;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: RAT_1:41

    ( denominator p) = ( denominator q) & ( numerator p) = ( numerator q) implies p = q

    proof

      assume that

       A1: ( denominator p) = ( denominator q) and

       A2: ( numerator p) = ( numerator q);

      

      thus p = (( numerator q) / ( denominator q)) by A1, A2, Th12

      .= q by Th12;

    end;

    theorem :: RAT_1:42

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

    proof

      p < q iff (( numerator p) / ( denominator p)) < q by Th12;

      then p < q iff (( numerator p) / ( denominator p)) < (( numerator q) / ( denominator q)) by Th12;

      hence thesis by XREAL_1: 102, XREAL_1: 106;

    end;

    theorem :: RAT_1:43

    

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

    proof

      

       A2: p = ( - ( - p))

      .= ( - (( numerator ( - p)) / ( denominator ( - p)))) by Th12

      .= (( - ( numerator ( - p))) / ( denominator ( - p)));

      consider w such that ( - ( numerator ( - p))) = (( numerator p) * w) and

       A3: ( denominator ( - p)) = (( denominator p) * w) by A2, Th24;

      ( - p) = ( - (( numerator p) / ( denominator p))) by Th12

      .= (( - ( numerator p)) / ( denominator p));

      then

      consider k such that

       A4: ( - ( numerator p)) = (( numerator ( - p)) * k) and

       A5: ( denominator p) = (( denominator ( - p)) * k) by Th24;

      ( denominator p) = ((( denominator p) * w) * k) by A5, A3

      .= (( denominator p) * (w * k));

      then

       A6: k = 1 by NAT_1: 15, XCMPLX_1: 7;

      hence ( denominator p) = ( denominator ( - p)) by A5;

      thus thesis by A4, A6;

    end;

    theorem :: RAT_1:44

    

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

    proof

       A1:

      now

        set x = ( denominator p);

        assume that

         A2: 0 < p and

         A3: q = (1 / p);

        

         A4: q = (1 / (( numerator p) / ( denominator p))) by A3, Th12

        .= ((1 * ( denominator p)) / ( numerator p)) by XCMPLX_1: 77

        .= (( denominator p) / ( numerator p));

        reconsider y = ( numerator p) as Element of NAT by A2, INT_1: 3;

        

         A5: not ex k st 1 < k & ex m, w st x = (m * k) & y = (w * k)

        proof

          assume not thesis;

          then

          consider k such that

           A6: 1 < k and

           A7: ex m, w st x = (m * k) & y = (w * k);

          consider m, w such that

           A8: x = (m * k) and

           A9: y = (w * k) by A7;

           0 <= m by A8;

          then

          reconsider z = m as Element of NAT by INT_1: 3;

          ( denominator p) = (z * k) by A8;

          hence contradiction by A6, A9, Th26;

        end;

         0 <> ( numerator p) by A2, Th35;

        hence ( numerator p) = ( denominator q) & ( denominator p) = ( numerator q) by A4, A5, Th27;

      end;

      now

        assume that

         A10: ( numerator q) = ( denominator p) and

         A11: ( denominator q) = ( numerator p);

        thus 0 < p by A11;

        

        thus q = ((1 * ( denominator p)) / ( numerator p)) by A10, A11, Th12

        .= (1 / (( numerator p) / ( denominator p))) by XCMPLX_1: 77

        .= (1 / p) by Th12;

      end;

      hence thesis by A1;

    end;

    theorem :: RAT_1:45

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

    proof

       A1:

      now

        set s = ( - q);

        set r = ( - p);

        assume that

         A2: p < 0 and

         A3: q = (1 / p);

        

         A4: s = (1 / r) by A3, XCMPLX_1: 188;

        

         A5: 0 < r by A2, XREAL_1: 58;

        then ( numerator s) = ( denominator r) by A4, Th41;

        then ( - ( numerator q)) = ( denominator r) by Th40;

        then

         A6: ( - ( - ( numerator q))) = ( - ( denominator p)) by Th40;

        ( denominator s) = ( numerator r) by A5, A4, Th41;

        then ( denominator q) = ( numerator r) by Th40;

        hence ( numerator q) = ( - ( denominator p)) & ( denominator q) = ( - ( numerator p)) by A6, Th40;

      end;

      now

        assume that

         A7: ( numerator q) = ( - ( denominator p)) and

         A8: ( denominator q) = ( - ( numerator p));

        thus p < 0 by A8;

        

        thus q = (( - ( denominator p)) / ( - ( numerator p))) by A7, A8, Th12

        .= ( - (( denominator p) / ( - ( numerator p))))

        .= ( - ( - (( denominator p) / ( numerator p)))) by XCMPLX_1: 188

        .= ((1 * ( denominator p)) / ( numerator p))

        .= (1 / (( numerator p) / ( denominator p))) by XCMPLX_1: 77

        .= (1 / p) by Th12;

      end;

      hence thesis by A1;

    end;