real_3.miz



    begin

    reserve a,b,k,n,m for Nat,

i for Integer,

r for Real,

p for Rational,

c for Complex,

x for object,

f for Function;

    

     Lm1: for a,b,c,d be Real st ((a / b) - c) <> 0 & d <> 0 & b <> 0 & a = ((b * c) + d) holds (1 / ((a / b) - c)) = (b / d)

    proof

      let a,b,c,d be Real;

      assume that

       A1: ((a / b) - c) <> 0 & d <> 0 and

       A2: b <> 0 ;

      assume a = ((b * c) + d);

      

      then d = (b * ((a - (b * c)) / b)) by A2, XCMPLX_1: 87

      .= (b * ((a / b) - ((b * c) / b)));

      then (1 * d) = (b * ((a / b) - c)) by A2, XCMPLX_1: 89;

      hence thesis by A1, XCMPLX_1: 94;

    end;

    registration

      let n;

      cluster (n div 0 ) -> zero;

      coherence by NAT_D:def 1;

      cluster (n mod 0 ) -> zero;

      coherence by NAT_D:def 2;

      cluster ( 0 div n) -> zero;

      coherence by NAT_2: 2;

      cluster ( 0 mod n) -> zero;

      coherence by NAT_D: 26;

    end

    registration

      let c;

      cluster (c - c) -> zero;

      coherence by XCMPLX_1: 14;

      cluster (c / 0 ) -> zero;

      coherence ;

    end

    registration

      cluster [\ 0 /] -> zero;

      coherence by INT_1: 25;

    end

    theorem :: REAL_3:1

    

     Th1: 0 < r & r < 1 implies 1 < (1 / r)

    proof

      assume that

       A1: 0 < r and

       A2: r < 1;

      (1 * (r " )) > (r * (r " )) by A1, A2, XREAL_1: 68;

      hence thesis by A1, XCMPLX_0:def 7;

    end;

    theorem :: REAL_3:2

    

     Th2: i <= r & r < (i + 1) implies [\r/] = i

    proof

      assume

       A1: i <= r;

      assume r < (i + 1);

      then (r - 1) < ((i + 1) - 1) by XREAL_1: 14;

      hence thesis by A1, INT_1:def 6;

    end;

    theorem :: REAL_3:3

     [\(m / n)/] = (m div n);

    theorem :: REAL_3:4

    

     Th4: (m mod n) = 0 implies (m / n) = (m div n)

    proof

      reconsider i = m as Integer;

      assume

       A1: (m mod n) = 0 ;

      per cases ;

        suppose

         A2: n = 0 ;

        

        hence (m / n) = 0

        .= (m div n) by A2;

      end;

        suppose

         A3: n <> 0 ;

        then (i - ((i div n) * n)) = 0 by A1, INT_1:def 10;

        hence thesis by A3, XCMPLX_1: 89;

      end;

    end;

    theorem :: REAL_3:5

    

     Th5: (m / n) = (m div n) implies (m mod n) = 0

    proof

      assume

       A1: (m / n) = (m div n);

      per cases ;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose

         A2: n > 0 ;

        then (m + 0 ) = ((n * (m / n)) + (m mod n)) by A1, NAT_D: 2;

        then ((m mod n) - 0 ) = (m - (n * (m / n)));

        

        hence (m mod n) = (m - m) by A2, XCMPLX_1: 87

        .= 0 ;

      end;

    end;

    theorem :: REAL_3:6

    

     Th6: ( frac (m / n)) = ((m mod n) / n)

    proof

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ( frac (m / n)) = ( frac 0 )

        .= ((m mod n) / n) by A1;

      end;

        suppose

         A2: n > 0 ;

        then m = ((n * (m div n)) + (m mod n)) by NAT_D: 2;

        then ((m / n) + 0 ) = ((m div n) + ((m mod n) / n)) by A2, XCMPLX_1: 113;

        hence thesis;

      end;

    end;

    theorem :: REAL_3:7

    

     Th7: p >= 0 implies ex m,n be Nat st n <> 0 & p = (m / n)

    proof

      consider m be Integer, k be Nat such that

       A1: k <> 0 & p = (m / k) by RAT_1: 8;

      assume p >= 0 ;

      then k > 0 & m >= 0 or k < 0 & m <= 0 by A1, XREAL_1: 141;

      then

      reconsider m as Element of NAT by INT_1: 3;

      take m, k;

      thus thesis by A1;

    end;

    registration

      cluster INT -valued for Real_Sequence;

      existence

      proof

        set s = ( NAT --> 1);

        

         A1: ( dom s) = NAT by FUNCOP_1: 13;

        for n be Nat holds (s . n) is real;

        then

        reconsider s as Real_Sequence by SEQ_1: 2, A1;

        take s;

        thus thesis;

      end;

    end

    definition

      mode Integer_Sequence is INT -valued Real_Sequence;

    end

    theorem :: REAL_3:8

    

     Th8: f is Integer_Sequence iff ( dom f) = NAT & for x st x in NAT holds (f . x) is integer

    proof

      thus f is Integer_Sequence implies ( dom f) = NAT & for x st x in NAT holds (f . x) is integer by SEQ_1: 1;

      assume that

       A1: ( dom f) = NAT and

       A2: for x st x in NAT holds (f . x) is integer;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: y = (f . x) by FUNCT_1:def 3;

        (f . x) is integer by A1, A2, A3;

        hence y in INT by A4;

      end;

      then

       A5: ( rng f) c= INT ;

      for x st x in NAT holds (f . x) is real

      proof

        let x;

        assume x in NAT ;

        then (f . x) is integer by A2;

        hence thesis;

      end;

      hence thesis by A1, A5, RELAT_1:def 19, SEQ_1: 1;

    end;

    theorem :: REAL_3:9

    

     Th9: f is sequence of INT iff f is Integer_Sequence

    proof

      hereby

        assume f is sequence of INT ;

        then

        reconsider g = f as sequence of INT ;

        ( dom g) = NAT & for x st x in NAT holds (g . x) is integer by FUNCT_2:def 1;

        hence f is Integer_Sequence by Th8;

      end;

      assume f is Integer_Sequence;

      then ( dom f) = NAT & ( rng f) c= INT by FUNCT_2:def 1, RELAT_1:def 19;

      hence thesis by FUNCT_2: 2;

    end;

    theorem :: REAL_3:10

    f is sequence of NAT iff ( dom f) = NAT & for x st x in NAT holds (f . x) is natural

    proof

      thus f is sequence of NAT implies ( dom f) = NAT & for x st x in NAT holds (f . x) is natural by FUNCT_2:def 1;

      assume that

       A1: ( dom f) = NAT and

       A2: for x st x in NAT holds (f . x) is natural;

      ( rng f) c= NAT

      proof

        let x be object;

        assume x in ( rng f);

        then ex y be object st y in NAT & x = (f . y) by A1, FUNCT_1:def 3;

        then x is natural by A2;

        hence thesis by ORDINAL1:def 12;

      end;

      hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: REAL_3:11

    f is sequence of NAT iff f is sequence of NAT ;

    begin

    definition

      deffunc F( Nat, Nat, Nat) = ($2 mod $3);

      let m,n be Nat;

      set a = (m mod n);

      set b = (n mod (m mod n));

      :: REAL_3:def1

      func modSeq (m,n) -> sequence of NAT means

      : Def1: (it . 0 ) = (m mod n) & (it . 1) = (n mod (m mod n)) & for k be Nat holds (it . (k + 2)) = ((it . k) mod (it . (k + 1)));

      existence

      proof

        consider f be sequence of NAT such that

         A1: (f . 0 ) = a & (f . 1) = b and

         A2: for n be Nat holds (f . (n + 2)) = F(n,.,.) from RECDEF_2:sch 5;

        reconsider f as sequence of NAT ;

        take f;

        thus (f . 0 ) = a & (f . 1) = b by A1;

        let k be Nat;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be sequence of NAT such that

         A3: (f . 0 ) = a & (f . 1) = b and

         A4: for n be Nat holds (f . (n + 2)) = ((f . n) mod (f . (n + 1))) and

         A5: (g . 0 ) = a & (g . 1) = b and

         A6: for n be Nat holds (g . (n + 2)) = ((g . n) mod (g . (n + 1)));

        reconsider f, g as sequence of NAT ;

        

         A7: (g . 0 ) = a & (g . 1) = b by A5;

        

         A8: for n be Nat holds (g . (n + 2)) = F(n,.,.) by A6;

        

         A9: for n be Nat holds (f . (n + 2)) = F(n,.,.) by A4;

        

         A10: (f . 0 ) = a & (f . 1) = b by A3;

        f = g from RECDEF_2:sch 7( A10, A9, A7, A8);

        hence thesis;

      end;

    end

    definition

      let m,n be Nat;

      set a = (m div n);

      set b = (n div (m mod n));

      deffunc F( Nat, Nat, Nat) = ((( modSeq (m,n)) . $1) div (( modSeq (m,n)) . ($1 + 1)));

      :: REAL_3:def2

      func divSeq (m,n) -> sequence of NAT means

      : Def2: (it . 0 ) = (m div n) & (it . 1) = (n div (m mod n)) & for k be Nat holds (it . (k + 2)) = ((( modSeq (m,n)) . k) div (( modSeq (m,n)) . (k + 1)));

      existence

      proof

        consider f be sequence of NAT such that

         A1: (f . 0 ) = a & (f . 1) = b and

         A2: for n be Nat holds (f . (n + 2)) = F(n,.,.) from RECDEF_2:sch 5;

        reconsider f as sequence of NAT ;

        take f;

        thus (f . 0 ) = a & (f . 1) = b by A1;

        let k be Nat;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be sequence of NAT such that

         A3: (f . 0 ) = a & (f . 1) = b and

         A4: for k be Nat holds (f . (k + 2)) = ((( modSeq (m,n)) . k) div (( modSeq (m,n)) . (k + 1))) and

         A5: (g . 0 ) = a & (g . 1) = b and

         A6: for k be Nat holds (g . (k + 2)) = ((( modSeq (m,n)) . k) div (( modSeq (m,n)) . (k + 1)));

        reconsider f, g as sequence of NAT ;

        

         A7: (g . 0 ) = a & (g . 1) = b by A5;

        

         A8: for n be Nat holds (g . (n + 2)) = F(n,,) by A6;

        

         A9: for n be Nat holds (f . (n + 2)) = F(n,.,.) by A4;

        

         A10: (f . 0 ) = a & (f . 1) = b by A3;

        f = g from RECDEF_2:sch 7( A10, A9, A7, A8);

        hence thesis;

      end;

    end

    theorem :: REAL_3:12

    

     Th12: (( divSeq (m,n)) . 1) = (n div (( modSeq (m,n)) . 0 ))

    proof

      

      thus (( divSeq (m,n)) . 1) = (n div (m mod n)) by Def2

      .= (n div (( modSeq (m,n)) . 0 )) by Def1;

    end;

    theorem :: REAL_3:13

    

     Th13: (( modSeq (m,n)) . 1) = (n mod (( modSeq (m,n)) . 0 ))

    proof

      

      thus (( modSeq (m,n)) . 1) = (n mod (m mod n)) by Def1

      .= (n mod (( modSeq (m,n)) . 0 )) by Def1;

    end;

    theorem :: REAL_3:14

    

     Th14: a <= b & (( modSeq (m,n)) . a) = 0 implies (( modSeq (m,n)) . b) = 0

    proof

      set fm = ( modSeq (m,n));

      assume that

       A1: a <= b and

       A2: (fm . a) = 0 ;

      

       A3: a < b or a = b by A1, XXREAL_0: 1;

      defpred P[ Nat] means a < $1 implies (fm . $1) = 0 ;

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A5: P[k];

        assume

         A6: a < (k + 1);

        then

         A7: a <= k by NAT_1: 13;

        per cases by NAT_1: 25;

          suppose

           A8: k = 0 ;

          then

           A9: a = 0 by A6, NAT_1: 13;

          

          thus (fm . (k + 1)) = (n mod (fm . 0 )) by A8, Th13

          .= 0 by A2, A9;

        end;

          suppose

           A10: k = 1;

          then

           A11: a = 0 or a = 1 by A7, NAT_1: 25;

          2 = (2 + 0 );

          

          hence (fm . (k + 1)) = ((fm . 0 ) mod (fm . ( 0 + 1))) by A10, Def1

          .= 0 by A2, A11;

        end;

          suppose k > 1;

          then

          reconsider k1 = (k - 1) as Nat;

          per cases by A7, XXREAL_0: 1;

            suppose

             A12: a = k;

            

            thus (fm . (k + 1)) = (fm . (k1 + 2))

            .= ((fm . k1) mod (fm . (k1 + 1))) by Def1

            .= 0 by A2, A12;

          end;

            suppose

             A13: a < k;

            

            thus (fm . (k + 1)) = (fm . (k1 + 2))

            .= ((fm . k1) mod (fm . (k1 + 1))) by Def1

            .= 0 by A5, A13;

          end;

        end;

      end;

      

       A14: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A14, A4);

      hence thesis by A2, A3;

    end;

    

     Lm2: (( modSeq (m,n)) . a) > (( modSeq (m,n)) . (a + 1)) or (( modSeq (m,n)) . a) = 0

    proof

      set fm = ( modSeq (m,n));

      per cases by NAT_1: 25;

        suppose

         A1: a = 0 ;

        (fm . ( 0 + 1)) = (n mod (m mod n)) & (fm . 0 ) = (m mod n) by Def1;

        hence thesis by A1, NAT_D: 1;

      end;

        suppose

         A2: a = 1;

        (fm . ( 0 + 2)) = ((fm . 0 ) mod (fm . ( 0 + 1))) by Def1;

        hence thesis by A2, NAT_D: 1;

      end;

        suppose a > 1;

        then

        reconsider a1 = (a - 1) as Nat;

        (fm . (a + 1)) = (fm . (a1 + (1 + 1)))

        .= ((fm . a1) mod (fm . (a1 + 1))) by Def1;

        hence thesis by NAT_D: 1;

      end;

    end;

    theorem :: REAL_3:15

    

     Th15: a < b implies (( modSeq (m,n)) . a) > (( modSeq (m,n)) . b) or (( modSeq (m,n)) . a) = 0

    proof

      set fm = ( modSeq (m,n));

      assume

       A1: a < b;

      per cases ;

        suppose (fm . a) = 0 ;

        hence thesis;

      end;

        suppose

         A2: (fm . a) > 0 ;

        defpred P[ Nat] means a < $1 implies (fm . a) > (fm . $1);

        

         A3: for x be Nat st P[x] holds P[(x + 1)]

        proof

          let x be Nat such that

           A4: P[x];

          assume a < (x + 1);

          then

           A5: a <= x by NAT_1: 13;

          per cases by A5, XXREAL_0: 1;

            suppose a = x;

            hence (fm . a) > (fm . (x + 1)) by A2, Lm2;

          end;

            suppose

             A6: a < x;

            thus (fm . a) > (fm . (x + 1))

            proof

              per cases by Lm2;

                suppose (fm . x) > (fm . (x + 1));

                hence thesis by A4, A6, XXREAL_0: 2;

              end;

                suppose (fm . x) = 0 ;

                hence thesis by A2, Th14, NAT_1: 11;

              end;

            end;

          end;

        end;

        

         A7: P[ 0 ];

        for x be Nat holds P[x] from NAT_1:sch 2( A7, A3);

        hence thesis by A1;

      end;

    end;

    theorem :: REAL_3:16

    

     Th16: (( divSeq (m,n)) . (a + 1)) = 0 implies (( modSeq (m,n)) . a) = 0

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      defpred P[ Nat] means (fd . ($1 + 1)) = 0 implies (fm . $1) = 0 ;

      

       A1: P[b] implies P[(b + 1)]

      proof

        assume P[b];

        set x = (fm . (b + 1));

        assume (fd . ((b + 1) + 1)) = 0 ;

        then (fd . (b + (1 + 1))) = 0 ;

        then

         A2: ((fm . b) div (fm . (b + 1))) = 0 by Def2;

        assume

         A3: (fm . (b + 1)) <> 0 ;

        then (fm . b) = ((x * ((fm . b) div x)) + ((fm . b) mod x)) by NAT_D: 2;

        then

         A4: (fm . b) < x by A2, A3, NAT_D: 1;

        

         A5: (b + 0 ) < (b + 1) by XREAL_1: 6;

        then (fm . b) <> 0 by A3, Th14;

        hence thesis by A4, A5, Th15;

      end;

      

       A6: P[ 0 ]

      proof

        set x = (m mod n);

        assume (fd . ( 0 + 1)) = 0 ;

        then

         A7: (n div (fm . 0 )) = 0 by Th12;

        assume

         A8: (fm . 0 ) <> 0 ;

        then (m mod n) <> 0 by Def1;

        then

         A9: n <> 0 ;

        

         A10: (fm . 0 ) = x by Def1;

        then n = ((x * (n div x)) + (n mod x)) by A8, NAT_D: 2;

        then n < x by A7, A10, A8, NAT_D: 1;

        hence thesis by A9, NAT_D: 1;

      end;

       P[b] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    

     Lm3: (( modSeq (m,n)) . a) = 0 implies (( divSeq (m,n)) . (a + 1)) = 0

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      defpred P[ Nat] means (fm . $1) = 0 implies (fd . ($1 + 1)) = 0 ;

      

       A1: P[b] implies P[(b + 1)]

      proof

        assume that P[b] and

         A2: (fm . (b + 1)) = 0 ;

        

        thus (fd . ((b + 1) + 1)) = (fd . (b + (1 + 1)))

        .= ((fm . b) div (fm . (b + 1))) by Def2

        .= 0 by A2;

      end;

      

       A3: P[ 0 ]

      proof

        assume

         A4: (fm . 0 ) = 0 ;

        

        thus (fd . ( 0 + 1)) = (n div (fm . 0 )) by Th12

        .= 0 by A4;

      end;

       P[b] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: REAL_3:17

    

     Th17: a <> 0 & a <= b & (( divSeq (m,n)) . a) = 0 implies (( divSeq (m,n)) . b) = 0

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      assume that

       A1: a <> 0 and

       A2: a <= b and

       A3: (fd . a) = 0 ;

      

       A4: a < b or a = b by A2, XXREAL_0: 1;

      defpred P[ Nat] means a < $1 implies (fd . $1) = 0 & (fm . $1) = 0 ;

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A6: P[k];

        assume

         A7: a < (k + 1);

        then

         A8: a <= k by NAT_1: 13;

        per cases by NAT_1: 25;

          suppose k = 0 ;

          hence thesis by A1, A7, NAT_1: 13;

        end;

          suppose

           A9: k = 1;

          then (fd . ( 0 + 1)) = 0 by A1, A3, A8, NAT_1: 25;

          then

           A10: (fm . 0 ) = 0 by Th16;

          

           A11: 2 = (2 + 0 );

          

          hence (fd . (k + 1)) = ((fm . 0 ) div (fm . ( 0 + 1))) by A9, Def2

          .= 0 by A10;

          

          thus (fm . (k + 1)) = ((fm . 0 ) mod (fm . ( 0 + 1))) by A9, A11, Def1

          .= 0 by A10;

        end;

          suppose k > 1;

          then

          reconsider k1 = (k - 1) as Nat;

          

           A12: k = (k1 + 1);

          per cases by A8, XXREAL_0: 1;

            suppose a = k;

            then

             A13: (fm . k1) = 0 by A3, A12, Th16;

            

            thus (fd . (k + 1)) = (fd . (k1 + 2))

            .= ((fm . k1) div (fm . (k1 + 1))) by Def2

            .= 0 by A13;

            

            thus (fm . (k + 1)) = (fm . (k1 + 2))

            .= ((fm . k1) mod (fm . (k1 + 1))) by Def1

            .= 0 by A13;

          end;

            suppose

             A14: a < k;

            

            thus (fd . (k + 1)) = (fd . (k1 + 2))

            .= ((fm . k1) div (fm . (k1 + 1))) by Def2

            .= 0 by A6, A14;

            

            thus (fm . (k + 1)) = (fm . (k1 + 2))

            .= ((fm . k1) mod (fm . (k1 + 1))) by Def1

            .= 0 by A6, A14;

          end;

        end;

      end;

      

       A15: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A15, A5);

      hence thesis by A3, A4;

    end;

    theorem :: REAL_3:18

    

     Th18: a < b & (( modSeq (m,n)) . a) = 0 implies (( divSeq (m,n)) . b) = 0

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      assume a < b;

      then

       A1: (a + 1) <= b by NAT_1: 13;

      assume (fm . a) = 0 ;

      then (fd . (a + 1)) = 0 by Lm3;

      hence thesis by A1, Th17;

    end;

    theorem :: REAL_3:19

    

     Th19: n <> 0 implies m = (((( divSeq (m,n)) . 0 ) * n) + (( modSeq (m,n)) . 0 ))

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      assume

       A1: n <> 0 ;

      (fd . 0 ) = (m div n) & (fm . 0 ) = (m mod n) by Def1, Def2;

      hence thesis by A1, NAT_D: 2;

    end;

    theorem :: REAL_3:20

    n <> 0 implies (m / n) = ((( divSeq (m,n)) . 0 ) + (1 / (n / (( modSeq (m,n)) . 0 ))))

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      assume

       A1: n <> 0 ;

      

      hence (m / n) = ((((fd . 0 ) * n) + (fm . 0 )) / n) by Th19

      .= (((fm . 0 ) / n) + (fd . 0 )) by A1, XCMPLX_1: 113

      .= ((fd . 0 ) + (1 / (n / (fm . 0 )))) by XCMPLX_1: 57;

    end;

    set g = ( NAT --> 0 );

    theorem :: REAL_3:21

    

     Th21: ( divSeq (m, 0 )) = ( NAT --> 0 )

    proof

      set g = ( NAT --> 0 );

      set fd = ( divSeq (m, 0 ));

      

       A1: for x be object st x in ( dom fd) holds (fd . x) = (g . x)

      proof

        defpred P[ Nat] means (fd . $1) = 0 ;

        let x be object;

        assume x in ( dom fd);

        then

        reconsider x as Element of NAT ;

        

         A2: for n be Nat holds P[n] implies P[(n + 1)]

        proof

          let n be Nat;

          assume

           A3: P[n];

          per cases ;

            suppose

             A4: n = 0 ;

            (fd . 1) = ( 0 div (m mod 0 )) by Def2

            .= 0 ;

            hence thesis by A4;

          end;

            suppose 0 <> n;

            hence thesis by A3, Th17, NAT_1: 11;

          end;

        end;

        (fd . 0 ) = (m div 0 ) by Def2

        .= 0 ;

        then

         A5: P[ 0 ];

        for n be Nat holds P[n] from NAT_1:sch 2( A5, A2);

        then (fd . x) = 0 ;

        hence thesis by FUNCOP_1: 7;

      end;

      ( dom fd) = NAT by FUNCT_2:def 1;

      hence thesis by A1;

    end;

    theorem :: REAL_3:22

    

     Th22: ( modSeq (m, 0 )) = ( NAT --> 0 )

    proof

      set fm = ( modSeq (m, 0 ));

      

       A1: for x be object st x in ( dom fm) holds (fm . x) = (g . x)

      proof

        defpred P[ Nat] means (fm . $1) = 0 ;

        let x be object;

        assume x in ( dom fm);

        then

        reconsider x as Element of NAT ;

        (fm . 0 ) = (m mod 0 ) by Def1

        .= 0 ;

        then

         A2: P[ 0 ];

        

         A3: for n be Nat holds P[n] implies P[(n + 1)] by Th14, NAT_1: 11;

        for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

        then (fm . x) = 0 ;

        hence thesis by FUNCOP_1: 7;

      end;

      ( dom fm) = NAT by FUNCT_2:def 1;

      hence thesis by A1;

    end;

    theorem :: REAL_3:23

    ( divSeq ( 0 ,n)) = ( NAT --> 0 )

    proof

      set fd = ( divSeq ( 0 ,n));

      

       A1: for x be object st x in ( dom fd) holds (fd . x) = (g . x)

      proof

        defpred P[ Nat] means (fd . $1) = 0 ;

        let x be object;

        assume x in ( dom fd);

        then

        reconsider x as Element of NAT ;

        

         A2: for x be Nat holds P[x] implies P[(x + 1)]

        proof

          let x be Nat;

          assume

           A3: P[x];

          per cases ;

            suppose

             A4: x = 0 ;

            (fd . 1) = (n div ( 0 mod n)) by Def2

            .= (n div 0 );

            hence thesis by A4;

          end;

            suppose 0 <> x;

            hence thesis by A3, Th17, NAT_1: 11;

          end;

        end;

        (fd . 0 ) = ( 0 div n) by Def2

        .= 0 ;

        then

         A5: P[ 0 ];

        for n be Nat holds P[n] from NAT_1:sch 2( A5, A2);

        then (fd . x) = 0 ;

        hence thesis by FUNCOP_1: 7;

      end;

      ( dom fd) = NAT by FUNCT_2:def 1;

      hence thesis by A1;

    end;

    theorem :: REAL_3:24

    ( modSeq ( 0 ,n)) = ( NAT --> 0 )

    proof

      set fm = ( modSeq ( 0 ,n));

      

       A1: for x be object st x in ( dom fm) holds (fm . x) = (g . x)

      proof

        defpred P[ Nat] means (fm . $1) = 0 ;

        let x be object;

        assume x in ( dom fm);

        then

        reconsider x as Element of NAT ;

        (fm . 0 ) = ( 0 mod n) by Def1

        .= 0 ;

        then

         A2: P[ 0 ];

        

         A3: for x be Nat holds P[x] implies P[(x + 1)] by Th14, NAT_1: 11;

        for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

        then (fm . x) = 0 ;

        hence thesis by FUNCOP_1: 7;

      end;

      ( dom fm) = NAT by FUNCT_2:def 1;

      hence thesis by A1;

    end;

    

     Lm4: ex k st (( modSeq (m,n)) . k) = 0

    proof

      set f = ( modSeq (m,n));

      defpred P[ Nat] means ex k st (f . k) = $1;

      

       A1: for a be Nat st a <> 0 & P[a] holds ex w be Nat st w < a & P[w]

      proof

        let a be Nat such that

         A2: a <> 0 ;

        given k such that

         A3: (f . k) = a;

        take w = (f . (k + 1));

        (k + 0 ) < (k + 1) by XREAL_1: 6;

        hence w < a by A2, A3, Th15;

        thus thesis;

      end;

      

       A4: ex a be Nat st P[a]

      proof

        take (f . 0 ), 0 ;

        thus thesis;

      end;

      thus P[ 0 ] from NAT_1:sch 7( A4, A1);

    end;

    theorem :: REAL_3:25

    

     Th25: ex k be Nat st (( divSeq (m,n)) . k) = 0 & (( modSeq (m,n)) . k) = 0

    proof

      set f = ( modSeq (m,n));

      consider k such that

       A1: (f . k) = 0 by Lm4;

      take (k + 1);

      

       A2: (k + 0 ) < (k + 1) by XREAL_1: 6;

      hence (( divSeq (m,n)) . (k + 1)) = 0 by A1, Th18;

      thus (f . (k + 1)) = 0 by A1, A2, Th14;

    end;

    begin

    defpred P[ set, Element of REAL , object] means $3 = (1 / ( frac $2));

    definition

      let r be Real;

      :: REAL_3:def3

      func remainders_for_scf r -> Real_Sequence means

      : Def3: (it . 0 ) = r & for n be Nat holds (it . (n + 1)) = (1 / ( frac (it . n)));

      existence

      proof

        reconsider r1 = r as Element of REAL by XREAL_0:def 1;

        

         A1: for n be Nat holds for x be Element of REAL holds ex y be Element of REAL st P[n, x, y]

        proof

          let n be Nat, x be Element of REAL ;

          consider y be Real such that

           A2: P[n, x, y];

          reconsider y as Element of REAL by XREAL_0:def 1;

          take y;

          thus P[n, x, y] by A2;

        end;

        consider f be sequence of REAL such that

         A3: (f . 0 ) = r1 and

         A4: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        take f;

        thus (f . 0 ) = r by A3;

        let n;

        thus thesis by A4;

      end;

      uniqueness

      proof

        

         A5: for n be Nat, x,y1,y2 be Element of REAL st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

        reconsider r1 = r as Element of REAL by XREAL_0:def 1;

        let g1,g2 be Real_Sequence such that

         A6: (g1 . 0 ) = r and

         A7: for n be Nat holds (g1 . (n + 1)) = (1 / ( frac (g1 . n))) and

         A8: (g2 . 0 ) = r and

         A9: for n be Nat holds (g2 . (n + 1)) = (1 / ( frac (g2 . n)));

        

         A10: for n be Nat holds P[n, (g1 . n), (g1 . (n + 1))] by A7;

        

         A11: for n be Nat holds P[n, (g2 . n), (g2 . (n + 1))] by A9;

        

         A12: (g2 . 0 ) = r1 by A8;

        

         A13: (g1 . 0 ) = r1 by A6;

        thus g1 = g2 from NAT_1:sch 14( A13, A10, A12, A11, A5);

      end;

    end

    notation

      let r be Real;

      synonym rfs r for remainders_for_scf r;

    end

    definition

      let r be Real;

      :: REAL_3:def4

      func SimpleContinuedFraction r -> Integer_Sequence means

      : Def4: for n be Nat holds (it . n) = [\(( rfs r) . n)/];

      existence

      proof

        defpred P[ set, set] means $2 = [\(( rfs r) . $1)/];

        

         A1: for x be Element of NAT holds ex y be Element of INT st P[x, y]

        proof

          let x be Element of NAT ;

          reconsider y = [\(( rfs r) . x)/] as Element of INT by INT_1:def 2;

          take y;

          thus thesis;

        end;

        consider f be sequence of INT such that

         A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        reconsider f as Integer_Sequence by Th9;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Integer_Sequence such that

         A3: for n be Nat holds (f1 . n) = [\(( rfs r) . n)/] and

         A4: for n be Nat holds (f2 . n) = [\(( rfs r) . n)/];

        let n be Element of NAT ;

        

        thus (f1 . n) = [\(( rfs r) . n)/] by A3

        .= (f2 . n) by A4;

      end;

    end

    notation

      let r be Real;

      synonym scf r for SimpleContinuedFraction r;

    end

    theorem :: REAL_3:26

    

     Th26: (( rfs r) . (n + 1)) = (1 / ((( rfs r) . n) - (( scf r) . n)))

    proof

      

      thus (( rfs r) . (n + 1)) = (1 / ( frac (( rfs r) . n))) by Def3

      .= (1 / ((( rfs r) . n) - (( scf r) . n))) by Def4;

    end;

    theorem :: REAL_3:27

    

     Th27: (( rfs r) . n) = 0 & n <= m implies (( rfs r) . m) = 0

    proof

      assume that

       A1: (( rfs r) . n) = 0 and

       A2: n <= m;

      per cases by A2, XXREAL_0: 1;

        suppose n = m;

        hence thesis by A1;

      end;

        suppose

         A3: n < m;

        defpred P[ Nat] means n < $1 implies (( rfs r) . $1) = 0 ;

        

         A4: for a be Nat st P[a] holds P[(a + 1)]

        proof

          let a be Nat;

          assume

           A5: P[a];

          assume n < (a + 1);

          then

           A6: n <= a by NAT_1: 13;

          per cases by A6, XXREAL_0: 1;

            suppose

             A7: n = a;

            

            thus (( rfs r) . (a + 1)) = (1 / ( frac (( rfs r) . a))) by Def3

            .= (1 / ((( rfs r) . a) - (( rfs r) . a))) by A1, A7

            .= 0 ;

          end;

            suppose

             A8: n < a;

            

            thus (( rfs r) . (a + 1)) = (1 / ( frac (( rfs r) . a))) by Def3

            .= (1 / ((( rfs r) . a) - (( rfs r) . a))) by A5, A8

            .= 0 ;

          end;

        end;

        

         A9: P[ 0 ];

        for a be Nat holds P[a] from NAT_1:sch 2( A9, A4);

        hence thesis by A3;

      end;

    end;

    theorem :: REAL_3:28

    (( rfs r) . n) = 0 & n <= m implies (( scf r) . m) = 0

    proof

      assume

       A1: (( rfs r) . n) = 0 & n <= m;

      

      thus (( scf r) . m) = [\(( rfs r) . m)/] by Def4

      .= [\ 0 /] by A1, Th27

      .= 0 ;

    end;

    theorem :: REAL_3:29

    

     Th29: (( rfs i) . (n + 1)) = 0

    proof

      defpred P[ Nat] means (( rfs i) . ($1 + 1)) = 0 ;

      

       A1: (( rfs i) . 0 ) = i by Def3;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A3: P[n];

        

        thus (( rfs i) . ((n + 1) + 1)) = (1 / ( frac (( rfs i) . (n + 1)))) by Def3

        .= (1 / ( 0 - 0 )) by A3

        .= 0 ;

      end;

      (( rfs i) . ( 0 + 1)) = (1 / ( frac (( rfs i) . 0 ))) by Def3

      .= (1 / (i - i)) by A1, INT_1: 25

      .= 0 ;

      then

       A4: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: REAL_3:30

    

     Th30: (( scf i) . 0 ) = i & (( scf i) . (n + 1)) = 0

    proof

      defpred P[ Nat] means (( rfs i) . ($1 + 1)) = 0 & (( scf i) . ($1 + 1)) = 0 ;

      

      thus (( scf i) . 0 ) = [\(( rfs i) . 0 )/] by Def4

      .= [\i/] by Def3

      .= i by INT_1: 25;

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A2: P[n];

        

        thus (( rfs i) . ((n + 1) + 1)) = (1 / ( frac (( rfs i) . (n + 1)))) by Def3

        .= (1 / ( 0 - 0 )) by A2

        .= 0 ;

        

        thus (( scf i) . ((n + 1) + 1)) = [\(( rfs i) . ((n + 1) + 1))/] by Def4

        .= [\ 0 /] by Th29

        .= 0 ;

      end;

      (( scf i) . ( 0 + 1)) = [\(( rfs i) . ( 0 + 1))/] by Def4

      .= [\ 0 /] by Th29

      .= 0 ;

      then

       A3: P[ 0 ] by Th29;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm5: i > 1 implies (( rfs (1 / i)) . 1) = i & (( rfs (1 / i)) . (n + 2)) = 0 & (( scf (1 / i)) . 0 ) = 0 & (( scf (1 / i)) . 1) = i & (( scf (1 / i)) . (n + 2)) = 0

    proof

      set r = (1 / i);

      defpred P[ Nat] means (( rfs r) . ($1 + 2)) = 0 & (( scf r) . ($1 + 2)) = 0 ;

      assume

       A1: i > 1;

      then

       A2: r < ( 0 + 1) by XREAL_1: 189;

      

       A3: [\(( rfs r) . 0 )/] = [\r/] by Def3

      .= 0 by A1, A2, Th2;

      

      thus

       A4: (( rfs r) . 1) = (( rfs r) . ( 0 + 1))

      .= (1 / ( frac (( rfs r) . 0 ))) by Def3

      .= (1 / (r - 0 )) by A3, Def3

      .= i;

      then

       A5: (( scf r) . 1) = [\i/] by Def4;

      

       A6: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A7: P[n];

        

        thus (( rfs r) . ((n + 1) + 2)) = (( rfs r) . ((n + 2) + 1))

        .= (1 / ( frac (( rfs r) . (n + 2)))) by Def3

        .= (1 / ( 0 - 0 )) by A7

        .= 0 ;

        

        hence (( scf r) . ((n + 1) + 2)) = [\ 0 /] by Def4

        .= 0 ;

      end;

      

       A8: (( rfs r) . ( 0 + 2)) = (( rfs r) . (1 + 1))

      .= (1 / ( frac (( rfs r) . 1))) by Def3

      .= (1 / (i - i)) by A4, INT_1: 25

      .= 0 ;

      

      then (( scf r) . ( 0 + 2)) = [\ 0 /] by Def4

      .= 0 ;

      then

       A9: P[ 0 ] by A8;

      

       A10: for n holds P[n] from NAT_1:sch 2( A9, A6);

      (( scf r) . 0 ) = [\(( rfs r) . 0 )/] by Def4

      .= [\r/] by Def3

      .= 0 by A1, A2, Th2;

      hence thesis by A5, A10, INT_1: 25;

    end;

    theorem :: REAL_3:31

    i > 1 implies (( rfs (1 / i)) . 1) = i & (( rfs (1 / i)) . (n + 2)) = 0 by Lm5;

    theorem :: REAL_3:32

    i > 1 implies (( scf (1 / i)) . 0 ) = 0 & (( scf (1 / i)) . 1) = i & (( scf (1 / i)) . (n + 2)) = 0 by Lm5;

    theorem :: REAL_3:33

    

     Th33: (for n holds (( scf r) . n) = 0 ) implies (( rfs r) . n) = 0

    proof

      assume that

       A1: for n holds (( scf r) . n) = 0 and

       A2: (( rfs r) . n) <> 0 ;

      

       A3: (( scf r) . n) = 0 by A1;

      set x = (( rfs r) . n);

      

       A4: (( scf r) . n) = [\x/] by Def4;

      per cases by A2;

        suppose x < 0 ;

        hence thesis by A3, A4, INT_1:def 6;

      end;

        suppose x >= 1;

        hence thesis by A3, A4, INT_1: 54;

      end;

        suppose 0 < x & x < 1;

        then

         A5: (1 / x) > 1 by Th1;

        

         A6: (( scf r) . (n + 1)) = 0 & (( scf r) . (n + 1)) = [\(( rfs r) . (n + 1))/] by A1, Def4;

        (( rfs r) . (n + 1)) = (1 / ( frac x)) by Def3

        .= (1 / (x - (( scf r) . n))) by Def4

        .= (1 / (x - 0 )) by A1

        .= (1 / x);

        hence thesis by A5, A6, INT_1: 54;

      end;

    end;

    theorem :: REAL_3:34

    

     Th34: (for n holds (( scf r) . n) = 0 ) implies r = 0

    proof

      assume for n holds (( scf r) . n) = 0 ;

      then (( rfs r) . 0 ) = 0 by Th33;

      hence thesis by Def3;

    end;

    

     Lm6: (( rfs (1 / (r - (( scf r) . 0 )))) . n) = (( rfs r) . (n + 1)) & (( scf (1 / (r - (( scf r) . 0 )))) . n) = (( scf r) . (n + 1))

    proof

      set x = (r - (( scf r) . 0 ));

      defpred P[ Nat] means (( rfs (1 / x)) . $1) = (( rfs r) . ($1 + 1)) & (( scf (1 / x)) . $1) = (( scf r) . ($1 + 1));

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume P[n];

        

        hence (( rfs (1 / x)) . (n + 1)) = (1 / ( frac (( rfs r) . (n + 1)))) by Def3

        .= (( rfs r) . ((n + 1) + 1)) by Def3;

        

        hence (( scf (1 / x)) . (n + 1)) = [\(( rfs r) . ((n + 1) + 1))/] by Def4

        .= (( scf r) . ((n + 1) + 1)) by Def4;

      end;

      

       A2: (( rfs (1 / x)) . 0 ) = (1 / x) by Def3

      .= (1 / ((( rfs r) . 0 ) - (( scf r) . 0 ))) by Def3

      .= (1 / ( frac (( rfs r) . 0 ))) by Def4

      .= (( rfs r) . ( 0 + 1)) by Def3;

      

      then (( scf (1 / x)) . 0 ) = [\(( rfs r) . 1)/] by Def4

      .= (( scf r) . ( 0 + 1)) by Def4;

      then

       A3: P[ 0 ] by A2;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: REAL_3:35

    

     Th35: ( frac r) = (r - (( scf r) . 0 ))

    proof

      

      thus ( frac r) = (r - [\(( rfs r) . 0 )/]) by Def3

      .= (r - (( scf r) . 0 )) by Def4;

    end;

    theorem :: REAL_3:36

    (( rfs r) . (n + 1)) = (( rfs (1 / ( frac r))) . n)

    proof

      ( frac r) = (r - (( scf r) . 0 )) by Th35;

      hence thesis by Lm6;

    end;

    theorem :: REAL_3:37

    

     Th37: (( scf r) . (n + 1)) = (( scf (1 / ( frac r))) . n)

    proof

      ( frac r) = (r - (( scf r) . 0 )) by Th35;

      hence thesis by Lm6;

    end;

    theorem :: REAL_3:38

    

     Th38: n >= 1 implies (( scf r) . n) >= 0

    proof

      defpred P[ Nat] means (( scf r) . $1) >= 0 ;

       [\r/] <= r by INT_1:def 6;

      then ( frac r) >= 0 by XREAL_1: 48;

      then

       A1: ((1 / ( frac r)) - 1) >= ( 0 - 1) by XREAL_1: 9;

      

       A2: for n be Nat st n >= 1 holds P[n] implies P[(n + 1)]

      proof

        let n be Nat;

        assume n >= 1;

         [\(( rfs r) . n)/] <= (( rfs r) . n) by INT_1:def 6;

        then ( frac (( rfs r) . n)) >= 0 by XREAL_1: 48;

        then

         A3: ((1 / ( frac (( rfs r) . n))) - 1) >= ( 0 - 1) by XREAL_1: 9;

        (( scf r) . (n + 1)) = [\(( rfs r) . (n + 1))/] by Def4

        .= [\(1 / ( frac (( rfs r) . n)))/] by Def3;

        then (( scf r) . (n + 1)) > ((1 / ((( rfs r) . n) - [\(( rfs r) . n)/])) - 1) by INT_1:def 6;

        then ((( scf r) . (n + 1)) - ( - 1)) > (((1 / ( frac (( rfs r) . n))) - 1) - ((1 / ( frac (( rfs r) . n))) - 1)) by A3, XREAL_1: 14;

        hence thesis by INT_1: 7;

      end;

      (( scf r) . 1) = [\(( rfs r) . ( 0 + 1))/] by Def4

      .= [\(1 / ( frac (( rfs r) . 0 )))/] by Def3

      .= [\(1 / ( frac r))/] by Def3;

      then (( scf r) . 1) > ((1 / ( frac r)) - 1) by INT_1:def 6;

      then ((( scf r) . 1) - ( - 1)) > (((1 / ( frac r)) - 1) - ((1 / ( frac r)) - 1)) by A1, XREAL_1: 14;

      then

       A4: P[1] by INT_1: 7;

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A4, A2);

      hence thesis;

    end;

    theorem :: REAL_3:39

    n >= 1 implies (( scf r) . n) in NAT by Th38, INT_1: 3;

    theorem :: REAL_3:40

    

     Th40: n >= 1 & (( scf r) . n) <> 0 implies (( scf r) . n) >= 1

    proof

      assume n >= 1 & (( scf r) . n) <> 0 ;

      then (( scf r) . n) > 0 by Th38;

      then (( scf r) . n) >= ( 0 + 1) by INT_1: 7;

      hence thesis;

    end;

    theorem :: REAL_3:41

    

     Th41: (( scf (m / n)) . k) = (( divSeq (m,n)) . k) & (( rfs (m / n)) . 1) = (n / (( modSeq (m,n)) . 0 )) & (( rfs (m / n)) . (k + 2)) = ((( modSeq (m,n)) . k) / (( modSeq (m,n)) . (k + 1)))

    proof

      set fd = ( divSeq (m,n));

      set fm = ( modSeq (m,n));

      set r = (m / n);

      

       A1: (( scf r) . 0 ) = [\(( rfs r) . 0 )/] by Def4

      .= (m div n) by Def3;

      per cases ;

        suppose

         A2: n = 0 ;

        then

         A3: fm = ( NAT --> 0 ) by Th22;

        

         A4: fd = ( NAT --> 0 ) by A2, Th21;

        

         A5: k in NAT by ORDINAL1:def 12;

        k = 0 or ex x be Nat st k = (x + 1) by NAT_1: 6;

        

        hence (( scf r) . k) = 0 by A2, Th30

        .= (fd . k) by A4, A5, FUNCOP_1: 7;

        

        thus (( rfs (m / n)) . 1) = (( rfs r) . ( 0 + 1))

        .= (n / (fm . 0 )) by A2, Th29;

        

        thus (( rfs (m / n)) . (k + 2)) = (( rfs r) . ((k + 1) + 1))

        .= ( 0 / (fm . (k + 1))) by A2, Th29

        .= ((fm . k) / (fm . (k + 1))) by A3, A5, FUNCOP_1: 7;

      end;

        suppose

         A6: 0 < n;

        then m = ((n * (m div n)) + (m mod n)) by NAT_D: 2;

        then

         A7: r = ((m div n) + ((m mod n) / n)) by A6, XCMPLX_1: 113;

        defpred P[ Nat] means (for i be Nat st i <= $1 holds (( scf r) . i) = (fd . i)) & for i be Nat st (i + 1) <= $1 holds (( rfs r) . (i + 2)) = ((fm . i) / (fm . (i + 1)));

        

         A8: (( rfs r) . ( 0 + 1)) = (1 / ( frac (( rfs r) . 0 ))) by Def3

        .= (1 / ((( rfs r) . 0 ) - (( scf r) . 0 ))) by Def4

        .= (1 / (r - (m div n))) by A1, Def3

        .= (n / (m mod n)) by A7, XCMPLX_1: 57

        .= (n / (fm . 0 )) by Def1;

        

         A9: P[ 0 ]

        proof

          hereby

            let i be Nat;

            assume i <= 0 ;

            then i = 0 ;

            hence (( scf r) . i) = (fd . i) by A1, Def2;

          end;

          let i be Nat;

          assume (i + 1) <= 0 ;

          hence thesis;

        end;

        

         A10: for a be Nat st P[a] holds P[(a + 1)]

        proof

          let a be Nat such that

           A11: P[a];

          per cases ;

            suppose

             A12: a = 0 ;

            set x = (m mod n);

            

             A13: (( scf r) . ( 0 + 1)) = (( scf (1 / ( frac r))) . 0 ) by Th37

            .= [\(( rfs (1 / ( frac r))) . 0 )/] by Def4

            .= [\(1 / ( frac r))/] by Def3

            .= [\(1 / ((m mod n) / n))/] by Th6

            .= (n div (m mod n)) by XCMPLX_1: 57

            .= (n div (fm . 0 )) by Def1

            .= (fd . 1) by Th12;

            hereby

              let i be Nat;

              assume i <= (a + 1);

              then i = 0 or i = 1 by A12, NAT_1: 25;

              hence (( scf r) . i) = (fd . i) by A9, A13;

            end;

            let i be Nat;

            assume (i + 1) <= (a + 1);

            then

             A14: (i + 1) = 0 or (i + 1) = ( 0 + 1) by A12, NAT_1: 25;

            per cases ;

              suppose

               A15: x = 0 ;

              

              thus (( rfs r) . (i + 2)) = (( rfs r) . (1 + 1)) by A14

              .= (1 / ( frac (( rfs r) . 1))) by Def3

              .= (1 / ((n / (fm . 0 )) - (fd . 1))) by A8, A13, Def4

              .= (1 / ((n / x) - (fd . 1))) by Def1

              .= (1 / ((n / x) - (n div x))) by Def2

              .= (1 / ( 0 - (n div x))) by A15

              .= (1 / ( 0 - 0 )) by A15

              .= ((fm . i) / 0 )

              .= ((fm . i) / (n mod x)) by A15

              .= ((fm . i) / (fm . (i + 1))) by A14, Def1;

            end;

              suppose

               A16: 0 < x;

              then

               A17: (n + 0 ) = ((x * (n div x)) + (n mod x)) by NAT_D: 2;

              per cases ;

                suppose

                 A18: (n mod x) = 0 ;

                then

                 A19: (n div x) = (n / x) by Th4;

                

                thus (( rfs r) . (i + 2)) = (( rfs r) . (1 + 1)) by A14

                .= (1 / ( frac (( rfs r) . 1))) by Def3

                .= (1 / ((n / (fm . 0 )) - (fd . 1))) by A8, A13, Def4

                .= (1 / ((n / x) - (fd . 1))) by Def1

                .= (1 / ((n / x) - (n div x))) by Def2

                .= (1 / 0 ) by A19

                .= ((fm . i) / (n mod x)) by A18

                .= ((fm . i) / (fm . (i + 1))) by A14, Def1;

              end;

                suppose

                 A20: (n mod x) <> 0 ;

                then

                 A21: ((n / x) - (n div x)) <> 0 by Th5;

                

                thus (( rfs r) . (i + 2)) = (( rfs r) . (1 + 1)) by A14

                .= (1 / ( frac (( rfs r) . 1))) by Def3

                .= (1 / ((n / (fm . 0 )) - (fd . 1))) by A8, A13, Def4

                .= (1 / ((n / x) - (fd . 1))) by Def1

                .= (1 / ((n / x) - (n div x))) by Def2

                .= (x / (n mod x)) by A16, A17, A20, A21, Lm1

                .= ((fm . i) / (n mod x)) by A14, Def1

                .= ((fm . i) / (fm . (i + 1))) by A14, Def1;

              end;

            end;

          end;

            suppose a > 0 ;

            then

             A22: ( 0 + 1) <= a by NAT_1: 13;

            now

              let b be Nat;

              assume b <= (a + 1);

              then

               A24: b < (a + 1) or b = (a + 1) by XXREAL_0: 1;

              per cases by A24, NAT_1: 13;

                suppose b <= a;

                hence (( scf r) . b) = (fd . b) by A11;

              end;

                suppose

                 A25: (b - 1) = a;

                reconsider a2 = (a - 1) as Element of NAT by A22, INT_1: 5;

                

                 A26: b = ((a - 1) + 2) by A25;

                

                thus (( scf r) . b) = [\(( rfs r) . b)/] by Def4

                .= ((fm . a2) div (fm . (a2 + 1))) by A11, A26

                .= (fd . b) by A26, Def2;

              end;

            end;

            let b be Nat;

            assume

             A27: (b + 1) <= (a + 1);

            per cases by A27, XXREAL_0: 1;

              suppose (b + 1) < (a + 1);

              then (b + 1) <= a by NAT_1: 13;

              hence thesis by A11;

            end;

              suppose

               A28: (b + 1) = (a + 1);

              then

              reconsider b1 = (b - 1) as Element of NAT by A22, INT_1: 5;

              

               A29: (b + 1) = (b1 + (1 + 1));

              

               A30: (b1 + 2) = ((b1 + 1) + 1);

              

               A31: (b + 2) = ((b + 1) + 1);

              per cases ;

                suppose

                 A32: 0 = (fm . (b1 + 1));

                

                thus (( rfs r) . (b + 2)) = (1 / ((( rfs r) . (b + 1)) - (( scf r) . (b + 1)))) by A31, Th26

                .= (1 / ((( rfs r) . (b + 1)) - (fd . (b + 1)))) by A23, A28

                .= (1 / (((fm . b1) / (fm . (b1 + 1))) - (fd . ((b1 + 1) + 1)))) by A11, A28, A29

                .= (1 / (((fm . b1) / 0 ) - ((fm . b1) div 0 ))) by A30, A32, Def2

                .= ((fm . b) / (fm . (b + 1))) by A32;

              end;

                suppose

                 A33: 0 < (fm . (b1 + 1));

                then

                 A34: ((fm . b1) + 0 ) = (((fm . (b1 + 1)) * ((fm . b1) div (fm . (b1 + 1)))) + ((fm . b1) mod (fm . (b1 + 1)))) by NAT_D: 2;

                per cases ;

                  suppose

                   A35: ((fm . b1) mod (fm . (b1 + 1))) = 0 ;

                  then ((fm . b1) / (fm . (b1 + 1))) = ((fm . b1) div (fm . (b1 + 1))) by Th4;

                  then

                   A36: (((fm . b1) / (fm . (b1 + 1))) - ((fm . b1) div (fm . (b1 + 1)))) = 0 ;

                  

                  thus (( rfs r) . (b + 2)) = (1 / ((( rfs r) . (b + 1)) - (( scf r) . (b + 1)))) by A31, Th26

                  .= (1 / ((( rfs r) . (b + 1)) - (fd . (b + 1)))) by A23, A28

                  .= (1 / (((fm . b1) / (fm . (b1 + 1))) - (fd . ((b1 + 1) + 1)))) by A11, A28, A29

                  .= (1 / 0 ) by A30, A36, Def2

                  .= ((fm . (b1 + 1)) / ((fm . b1) mod (fm . (b1 + 1)))) by A35

                  .= ((fm . b) / (fm . (b + 1))) by A30, Def1;

                end;

                  suppose

                   A37: ((fm . b1) mod (fm . (b1 + 1))) <> 0 ;

                  then

                   A38: (((fm . b1) / (fm . (b1 + 1))) - ((fm . b1) div (fm . (b1 + 1)))) <> 0 by Th5;

                  

                  thus (( rfs r) . (b + 2)) = (1 / ((( rfs r) . (b + 1)) - (( scf r) . (b + 1)))) by A31, Th26

                  .= (1 / ((( rfs r) . (b + 1)) - (fd . (b + 1)))) by A23, A28

                  .= (1 / (((fm . b1) / (fm . (b1 + 1))) - (fd . ((b1 + 1) + 1)))) by A11, A28, A29

                  .= (1 / (((fm . b1) / (fm . (b1 + 1))) - ((fm . b1) div (fm . (b1 + 1))))) by A30, Def2

                  .= ((fm . (b1 + 1)) / ((fm . b1) mod (fm . (b1 + 1)))) by A33, A34, A37, A38, Lm1

                  .= ((fm . b) / (fm . (b + 1))) by A30, Def1;

                end;

              end;

            end;

          end;

        end;

        for a be Nat holds P[a] from NAT_1:sch 2( A9, A10);

        hence thesis by A8;

      end;

    end;

    theorem :: REAL_3:42

    

     Th42: r is rational iff ex n st for m st m >= n holds (( scf r) . m) = 0

    proof

      defpred A[ Nat] means for s be Real st for m st m >= $1 holds (( scf s) . m) = 0 holds s is rational;

      

       A1: for m st A[m] holds A[(m + 1)]

      proof

        let m;

        assume

         A2: A[m];

        let s be Real such that

         A3: for n st n >= (m + 1) holds (( scf s) . n) = 0 ;

        set B = (1 / (s - (( scf s) . 0 )));

        for n st n >= m holds (( scf B) . n) = 0

        proof

          let n;

          assume n >= m;

          then

           A4: (n + 1) >= (m + 1) by XREAL_1: 6;

          

          thus (( scf B) . n) = (( scf s) . (n + 1)) by Lm6

          .= 0 by A3, A4;

        end;

        then

        reconsider B as Rational by A2;

        ((( scf s) . 0 ) + (1 / B)) is rational;

        hence thesis;

      end;

      thus r is rational implies ex n st for m st m >= n holds (( scf r) . m) = 0

      proof

        assume r is rational;

        then

        reconsider r as Rational;

        consider m,n be Nat such that

         A5: n <> 0 and

         A6: ( frac r) = (m / n) by Th7, INT_1: 43;

        ( frac r) < 1 by INT_1: 43;

        then

         A7: m < n by A5, A6, XREAL_1: 181;

        set fm = ( modSeq (n,m));

        set fd = ( divSeq (n,m));

        per cases ;

          suppose

           A8: m = 0 ;

          take 1;

          let a;

          assume a >= 1;

          then ex x be Nat st a = (x + 1) by NAT_1: 6;

          hence thesis by A6, A8, Th30;

        end;

          suppose

           A9: m <> 0 ;

          consider k such that

           A10: (fd . k) = 0 and (fm . k) = 0 by Th25;

           A11:

          now

            assume

             A12: k = 0 ;

            m <= 0 or (n div m) <> 0 by A7, NAT_2: 12;

            hence contradiction by A9, A10, A12, Def2;

          end;

          take (k + 1);

          let a;

          assume

           A13: a >= (k + 1);

          1 <= (k + 1) by NAT_1: 11;

          then

          reconsider a1 = (a - 1) as Element of NAT by A13, INT_1: 5, XXREAL_0: 2;

          

           A14: a = (a1 + 1);

          (k + 0 ) < (k + 1) by XREAL_1: 6;

          then k < a by A13, XXREAL_0: 2;

          then

           A15: k <= a1 by A14, NAT_1: 13;

          (( scf r) . a) = (( scf (1 / ( frac r))) . a1) by A14, Th37

          .= (( scf (n / m)) . a1) by A6, XCMPLX_1: 57

          .= (fd . a1) by Th41

          .= 0 by A10, A11, A15, Th17;

          hence thesis;

        end;

      end;

      given n such that

       A16: for m st m >= n holds (( scf r) . m) = 0 ;

      

       A17: A[ 0 ]

      proof

        let s be Real;

        assume for m st m >= 0 holds (( scf s) . m) = 0 ;

        then for m holds (( scf s) . m) = 0 ;

        hence thesis by Th34;

      end;

      for n holds A[n] from NAT_1:sch 2( A17, A1);

      hence thesis by A16;

    end;

    theorem :: REAL_3:43

    (for n holds (( scf r) . n) <> 0 ) implies r is irrational

    proof

      assume

       A1: for n holds (( scf r) . n) <> 0 ;

       not ex n st for m st m >= n holds (( scf r) . m) = 0

      proof

        let n;

        take n;

        thus thesis by A1;

      end;

      hence thesis by Th42;

    end;

    begin

    reserve l,n1,n2 for Nat;

    reserve s1,s2 for Real_Sequence;

    definition

      let r be Real;

      :: REAL_3:def5

      func convergent_numerators (r) -> Real_Sequence means

      : Def5: (it . 0 ) = (( scf r) . 0 ) & (it . 1) = (((( scf r) . 1) * (( scf r) . 0 )) + 1) & for n be Nat holds (it . (n + 2)) = (((( scf r) . (n + 2)) * (it . (n + 1))) + (it . n));

      existence

      proof

        set s = ( scf r);

        deffunc U( Nat, Real, Real) = ( In ((((s . ($1 + 2)) * $3) + $2), REAL ));

        reconsider s0 = (s . 0 ), s1 = (((s . 1) * (s . 0 )) + 1) as Element of REAL by XREAL_0:def 1;

        consider f be Real_Sequence such that

         A1: (f . 0 ) = s0 & (f . 1) = s1 and

         A2: for n be Nat holds (f . (n + 2)) = U(n,.,.) from RECDEF_2:sch 5;

        take f;

        thus (f . 0 ) = (s . 0 ) & (f . 1) = (((s . 1) * (s . 0 )) + 1) by A1;

        let n;

        (f . (n + 2)) = U(n,.,.) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        set s = ( scf r);

        deffunc U( Nat, Real, Real) = ( In ((((s . ($1 + 2)) * $3) + $2), REAL ));

        let f,g be Real_Sequence such that

         A3: (f . 0 ) = (s . 0 ) & (f . 1) = (((s . 1) * (s . 0 )) + 1) and

         A4: for k be Nat holds (f . (k + 2)) = (((s . (k + 2)) * (f . (k + 1))) + (f . k)) and

         A5: (g . 0 ) = (s . 0 ) & (g . 1) = (((s . 1) * (s . 0 )) + 1) and

         A6: for k be Nat holds (g . (k + 2)) = (((s . (k + 2)) * (g . (k + 1))) + (g . k));

        reconsider s0 = (s . 0 ), s1 = (((s . 1) * (s . 0 )) + 1) as Element of REAL by XREAL_0:def 1;

        

         A7: (g . 0 ) = s0 & (g . 1) = s1 by A5;

        

         A8: for k be Nat holds (g . (k + 2)) = U(k,.,.) by A6;

        

         A9: for k be Nat holds (f . (k + 2)) = U(k,.,.) by A4;

        

         A10: (f . 0 ) = s0 & (f . 1) = s1 by A3;

        f = g from RECDEF_2:sch 7( A10, A9, A7, A8);

        hence thesis;

      end;

    end

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    definition

      let r be Real;

      set s = ( scf r);

      :: REAL_3:def6

      func convergent_denominators (r) -> Real_Sequence means

      : Def6: (it . 0 ) = 1 & (it . 1) = (( scf r) . 1) & for n be Nat holds (it . (n + 2)) = (((( scf r) . (n + 2)) * (it . (n + 1))) + (it . n));

      existence

      proof

        deffunc U( Nat, Real, Real) = ( In ((((s . ($1 + 2)) * $3) + $2), REAL ));

        consider f be Real_Sequence such that

         A1: (f . 0 ) = jj & (f . 1) = (s . 1) and

         A2: for n be Nat holds (f . (n + 2)) = U(n,.,.) from RECDEF_2:sch 5;

        take f;

        thus (f . 0 ) = 1 & (f . 1) = (( scf r) . 1) by A1;

        let n be Nat;

        (f . (n + 2)) = U(n,.,.) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc U( Nat, Real, Real) = ( In ((((s . ($1 + 2)) * $3) + $2), REAL ));

        let f,g be Real_Sequence such that

         A3: (f . 0 ) = 1 & (f . 1) = (s . 1) and

         A4: for k be Nat holds (f . (k + 2)) = (((s . (k + 2)) * (f . (k + 1))) + (f . k)) and

         A5: (g . 0 ) = 1 & (g . 1) = (s . 1) and

         A6: for k be Nat holds (g . (k + 2)) = (((s . (k + 2)) * (g . (k + 1))) + (g . k));

        

         A7: (g . 0 ) = jj & (g . 1) = (s . 1) by A5;

        

         A8: for k be Nat holds (g . (k + 2)) = U(k,.,.) by A6;

        

         A9: for k be Nat holds (f . (k + 2)) = U(k,.,.) by A4;

        

         A10: (f . 0 ) = jj & (f . 1) = (s . 1) by A3;

        f = g from RECDEF_2:sch 7( A10, A9, A7, A8);

        hence thesis;

      end;

    end

    notation

      let r be Real;

      synonym c_n (r) for convergent_numerators (r);

      synonym c_d (r) for convergent_denominators (r);

    end

    theorem :: REAL_3:44

    

     Th44: (( scf r) . 0 ) > 0 implies for n holds (( c_n r) . n) in NAT

    proof

      set s1 = ( c_n r);

      set s = ( scf r);

      defpred P[ Nat] means (s1 . $1) in NAT ;

      

       A1: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A2: (s1 . n) in NAT and

         A3: (s1 . (n + 1)) in NAT ;

        reconsider n2 = (s1 . (n + 1)) as Element of NAT by A3;

        reconsider n1 = (s1 . n) as Element of NAT by A2;

        (n + 2) >= ( 0 + 1) by XREAL_1: 7;

        then

        reconsider n3 = (s . (n + 2)) as Element of NAT by Th38, INT_1: 3;

        ((n3 * n2) + n1) in NAT ;

        hence thesis by Def5;

      end;

      assume

       A4: (( scf r) . 0 ) > 0 ;

      

       A5: P[1]

      proof

        reconsider n2 = (s . 0 ) as Element of NAT by A4, INT_1: 3;

        reconsider n1 = (s . 1) as Element of NAT by Th38, INT_1: 3;

        ((n1 * n2) + 1) in NAT ;

        hence thesis by Def5;

      end;

      let n;

      (s . 0 ) in NAT by A4, INT_1: 3;

      then

       A6: P[ 0 ] by Def5;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A6, A5, A1);

      hence thesis;

    end;

    theorem :: REAL_3:45

    

     Th45: (( scf r) . 0 ) > 0 implies for n holds (( c_n r) . n) > 0

    proof

      assume

       A1: (( scf r) . 0 ) > 0 ;

      set s1 = ( c_n r);

      set s = ( scf r);

      defpred P[ Nat] means (s1 . $1) > 0 ;

      (s1 . 1) = (((s . 1) * (s . 0 )) + 1) & (s . 1) >= 0 by Def5, Th38;

      then

       A2: P[1] by A1;

      let n;

      

       A3: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume

         A4: (s1 . n) > 0 & (s1 . (n + 1)) > 0 ;

        (n + 2) > (1 + 0 ) by XREAL_1: 8;

        then

         A5: (s . (n + 2)) >= 0 by Th38;

        (s1 . (n + 2)) = (((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) by Def5;

        hence thesis by A5, A4;

      end;

      

       A6: P[ 0 ] by A1, Def5;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A6, A2, A3);

      hence thesis;

    end;

    theorem :: REAL_3:46

    (( scf r) . 0 ) > 0 implies for n holds (( c_n r) . (n + 2)) > ((( scf r) . (n + 2)) * (( c_n r) . (n + 1)))

    proof

      assume

       A1: (( scf r) . 0 ) > 0 ;

      let n;

      set s = ( scf r);

      set s1 = ( c_n r);

      set m = ((s . (n + 2)) * (s1 . (n + 1)));

      ((s1 . (n + 2)) - m) = ((m + (s1 . n)) - m) by Def5;

      then ((s1 . (n + 2)) - ((s . (n + 2)) * (s1 . (n + 1)))) > 0 by A1, Th45;

      then (((s1 . (n + 2)) - m) + m) > ( 0 + m) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: REAL_3:47

    (( scf r) . 0 ) > 0 implies for n st n1 = (( c_n r) . (n + 1)) & n2 = (( c_n r) . n) holds (n1 gcd n2) = 1

    proof

      set s1 = ( c_n r);

      set s = ( scf r);

      defpred X[ Nat] means for n1, n2 st n1 = (s1 . ($1 + 1)) & n2 = (s1 . $1) holds (n1 gcd n2) = 1;

      assume

       A1: (( scf r) . 0 ) > 0 ;

      

       A2: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        reconsider n3 = (s1 . (k + 2)) as Element of NAT by A1, Th44;

        reconsider n2 = (s1 . k) as Element of NAT by A1, Th44;

        (k + 2) >= ( 0 + 1) by XREAL_1: 7;

        then

        reconsider n4 = (s . (k + 2)) as Element of NAT by Th38, INT_1: 3;

        reconsider n1 = (s1 . (k + 1)) as Element of NAT by A1, Th44;

        assume for n1, n2 st n1 = (s1 . (k + 1)) & n2 = (s1 . k) holds (n1 gcd n2) = 1;

        then

         A3: (n1 gcd n2) = 1;

        n3 = ((n4 * n1) + n2) by Def5;

        hence thesis by A3, EULER_1: 8;

      end;

      

       A4: X[ 0 ]

      proof

        reconsider u = (s . 1) as Element of NAT by Th38, INT_1: 3;

        let n1, n2 such that

         A5: n1 = (s1 . ( 0 + 1)) and

         A6: n2 = (s1 . 0 );

        n1 = ((u * (s . 0 )) + 1) by A5, Def5;

        then

         A7: n1 = ((u * n2) + 1) by A6, Def5;

        (1 gcd n2) = 1 by NEWTON: 51;

        hence thesis by A7, EULER_1: 8;

      end;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: REAL_3:48

    (( scf r) . 0 ) > 0 & (for n holds (( scf r) . n) <> 0 ) implies for n holds (( c_n r) . n) >= ( tau |^ n)

    proof

      assume that

       A1: (( scf r) . 0 ) > 0 and

       A2: for n holds (( scf r) . n) <> 0 ;

      set s = ( scf r);

      

       A3: (s . 0 ) >= ( 0 + 1) by A1, INT_1: 7;

      set s1 = ( c_n r);

      defpred P[ Nat] means (s1 . $1) >= ( tau |^ $1);

      

       A4: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A5: (s1 . n) >= ( tau |^ n) and

         A6: (s1 . (n + 1)) >= ( tau |^ (n + 1));

        

         A7: (( tau |^ (n + 1)) + ( tau |^ n)) = (((((1 + ( sqrt 5)) / 2) |^ n) * ((1 + ( sqrt 5)) / 2)) + (((1 + ( sqrt 5)) / 2) |^ n)) by FIB_NUM:def 1, NEWTON: 6

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((6 + (2 * ( sqrt 5))) / 4));

        ( sqrt 5) >= 0 by SQUARE_1:def 2;

        then ((1 + ( sqrt 5)) / 2) > 0 by XREAL_1: 139;

        then

         A8: ( tau |^ (n + 1)) > 0 by FIB_NUM:def 1, PREPOWER: 6;

        

         A9: ( tau |^ (n + 2)) = ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + ( sqrt 5)) / 2) |^ 2)) by FIB_NUM:def 1, NEWTON: 8

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + ( sqrt 5)) / 2) ^2 )) by WSIERP_1: 1

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((((1 ^2 ) + ((2 * 1) * ( sqrt 5))) + (( sqrt 5) ^2 )) / 4))

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + (2 * ( sqrt 5))) + 5) / 4)) by SQUARE_1:def 2

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((6 + (2 * ( sqrt 5))) / 4));

        

         A10: (s1 . ((n + 1) + 1)) = (((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) by Def5;

        (n + 2) >= ( 0 + 1) by XREAL_1: 7;

        then (s . (n + 2)) >= 1 by A2, Th40;

        then ((s . (n + 2)) * (s1 . (n + 1))) >= (1 * ( tau |^ (n + 1))) by A6, A8, XREAL_1: 66;

        hence thesis by A5, A10, A7, A9, XREAL_1: 7;

      end;

      (s1 . 0 ) = (s . 0 ) by Def5;

      then

       A11: P[ 0 ] by A3, NEWTON: 4;

      (s . 1) >= 1 by A2, Th40;

      then ((s . 1) * (s . 0 )) >= 1 by A3, XREAL_1: 159;

      then

       A12: (((s . 1) * (s . 0 )) + 1) >= (1 + 1) by XREAL_1: 6;

      let n;

      ( sqrt 5) < ( sqrt (3 ^2 )) by SQUARE_1: 27;

      then ( sqrt 5) < 3 by SQUARE_1: 22;

      then (1 + ( sqrt 5)) < (1 + 3) by XREAL_1: 8;

      then

       A13: ((1 + ( sqrt 5)) / 2) < (4 / 2) by XREAL_1: 74;

      (s1 . 1) = (((s . 1) * (s . 0 )) + 1) & (((1 + ( sqrt 5)) / 2) |^ 1) = ((1 + ( sqrt 5)) / 2) by Def5;

      then

       A14: P[1] by A12, A13, FIB_NUM:def 1, XXREAL_0: 2;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A11, A14, A4);

      hence thesis;

    end;

    theorem :: REAL_3:49

    (( scf r) . 0 ) > 0 & (for n holds (( scf r) . n) <= b) implies for n holds (( c_n r) . n) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))

    proof

      assume that

       A1: (( scf r) . 0 ) > 0 and

       A2: for n holds (( scf r) . n) <= b;

      set s1 = ( c_n r);

      set s = ( scf r);

      

       A3: (s . 0 ) <= b by A2;

      defpred P[ Nat] means (s1 . $1) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ($1 + 1));

      

       A4: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A5: (s1 . n) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) and

         A6: (s1 . (n + 1)) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1));

        (n + 2) >= ( 0 + 1) by XREAL_1: 7;

        then

         A7: (s . (n + 2)) >= 0 by Th38;

        (s . (n + 2)) <= b & (s1 . (n + 1)) > 0 by A1, A2, Th45;

        then

         A8: ((s . (n + 2)) * (s1 . (n + 1))) <= (b * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1))) by A6, A7, XREAL_1: 66;

        

         A9: ((b * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1))) + (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))) = ((b * ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((b + ( sqrt ((b ^2 ) + 4))) / 2))) + (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))) by NEWTON: 6

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2));

        

         A10: (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 2) + 1)) = (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 2))

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ 2)) by NEWTON: 8

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * (((b + ( sqrt ((b ^2 ) + 4))) / 2) ^2 )) by WSIERP_1: 1

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + (( sqrt ((b ^2 ) + 4)) ^2 )) / (2 * 2)))

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + ((b ^2 ) + 4)) / (2 * 2))) by SQUARE_1:def 2

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2));

        (s1 . ((n + 1) + 1)) = (((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) by Def5;

        hence thesis by A5, A8, A9, A10, XREAL_1: 7;

      end;

      let n;

      ((b ^2 ) + 4) > (b ^2 ) by XREAL_1: 39;

      then ( sqrt ((b ^2 ) + 4)) > ( sqrt (b ^2 )) by SQUARE_1: 27;

      then

       A11: ( sqrt ((b ^2 ) + 4)) > b by SQUARE_1: 22;

      then (b + ( sqrt ((b ^2 ) + 4))) > (b + b) by XREAL_1: 8;

      then ((b + ( sqrt ((b ^2 ) + 4))) / 2) > ((2 * b) / 2) by XREAL_1: 74;

      then

       A12: (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ( 0 + 1)) > b;

      

       A13: (s . 1) >= 0 by Th38;

      

       A14: (s1 . 1) = (((s . 1) * (s . 0 )) + 1) by Def5;

      (s . 1) <= b by A2;

      then ((s . 1) * (s . 0 )) <= (b ^2 ) by A1, A3, A13, XREAL_1: 66;

      then

       A15: (s1 . 1) <= ((b ^2 ) + 1) by A14, XREAL_1: 6;

      (b * ( sqrt ((b ^2 ) + 4))) >= (b * b) by A11, XREAL_1: 64;

      then ((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) >= ((b ^2 ) + (b * b)) by XREAL_1: 6;

      then (((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) >= (((b ^2 ) + (b ^2 )) + 2) by XREAL_1: 6;

      then

       A16: ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2) >= ((2 * ((b ^2 ) + 1)) / 2) by XREAL_1: 72;

      (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (1 + 1)) = (((b + ( sqrt ((b ^2 ) + 4))) / 2) ^2 ) by WSIERP_1: 1

      .= ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + (( sqrt ((b ^2 ) + 4)) ^2 )) / (2 * 2))

      .= ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + ((b ^2 ) + 4)) / (2 * 2)) by SQUARE_1:def 2

      .= ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2);

      then

       A17: P[1] by A15, A16, XXREAL_0: 2;

      (s1 . 0 ) = (s . 0 ) by Def5;

      then

       A18: P[ 0 ] by A3, A12, XXREAL_0: 2;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A18, A17, A4);

      hence thesis;

    end;

    theorem :: REAL_3:50

    

     Th50: (( c_d r) . n) in NAT

    proof

      set s = ( scf r);

      set s2 = ( c_d r);

      defpred P[ Nat] means (s2 . $1) in NAT ;

      (s2 . 0 ) = 1 by Def6;

      then

       A1: P[ 0 ];

      

       A2: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A3: (s2 . n) in NAT and

         A4: (s2 . (n + 1)) in NAT ;

        reconsider n2 = (s2 . (n + 1)) as Element of NAT by A4;

        reconsider n1 = (s2 . n) as Element of NAT by A3;

        (n + 2) >= ( 0 + 1) by XREAL_1: 7;

        then

        reconsider n3 = (s . (n + 2)) as Element of NAT by Th38, INT_1: 3;

        ((n3 * n2) + n1) in NAT ;

        hence thesis by Def6;

      end;

      (s2 . 1) = (s . 1) by Def6;

      then

       A5: P[1] by Th38, INT_1: 3;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A1, A5, A2);

      hence thesis;

    end;

    theorem :: REAL_3:51

    

     Th51: (( c_d r) . n) >= 0

    proof

      set s = ( scf r);

      set s1 = ( c_d r);

      defpred P[ Nat] means (s1 . $1) >= 0 ;

      

       A1: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume

         A2: (s1 . n) >= 0 ;

        

         A3: (s1 . (n + 2)) = (((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) by Def6;

        (n + 2) > (1 + 0 ) by XREAL_1: 8;

        then

         A4: (s . (n + 2)) >= 0 by Th38;

        assume (s1 . (n + 1)) >= 0 ;

        hence thesis by A4, A3, A2;

      end;

      (s . 1) >= 0 by Th38;

      then

       A5: P[1] by Def6;

      

       A6: P[ 0 ] by Def6;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A6, A5, A1);

      hence thesis;

    end;

    theorem :: REAL_3:52

    

     Th52: (( scf r) . 1) > 0 implies for n holds (( c_d r) . n) > 0

    proof

      set s = ( scf r);

      set s1 = ( c_d r);

      defpred P[ Nat] means (s1 . $1) > 0 ;

      assume (( scf r) . 1) > 0 ;

      then

       A1: P[1] by Def6;

      let n;

      

       A2: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume

         A3: (s1 . n) > 0 ;

        

         A4: (s1 . (n + 2)) = (((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) by Def6;

        (n + 2) > (1 + 0 ) by XREAL_1: 8;

        then

         A5: (s . (n + 2)) >= 0 by Th38;

        assume (s1 . (n + 1)) > 0 ;

        hence thesis by A5, A4, A3;

      end;

      

       A6: P[ 0 ] by Def6;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A6, A1, A2);

      hence thesis;

    end;

    theorem :: REAL_3:53

    (( c_d r) . (n + 2)) >= ((( scf r) . (n + 2)) * (( c_d r) . (n + 1)))

    proof

      set s = ( scf r);

      set s1 = ( c_d r);

      set m = ((s . (n + 2)) * (s1 . (n + 1)));

      ((s1 . (n + 2)) - ((s . (n + 2)) * (s1 . (n + 1)))) = ((((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) - ((s . (n + 2)) * (s1 . (n + 1)))) by Def6;

      then ((s1 . (n + 2)) - ((s . (n + 2)) * (s1 . (n + 1)))) >= 0 by Th51;

      then (((s1 . (n + 2)) - m) + m) >= ( 0 + m) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: REAL_3:54

    (( scf r) . 1) > 0 implies for n holds (( c_d r) . (n + 2)) > ((( scf r) . (n + 2)) * (( c_d r) . (n + 1)))

    proof

      assume

       A1: (( scf r) . 1) > 0 ;

      let n;

      set s1 = ( c_d r);

      set s = ( scf r);

      set m = ((s . (n + 2)) * (s1 . (n + 1)));

      ((s1 . (n + 2)) - ((s . (n + 2)) * (s1 . (n + 1)))) = ((((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) - ((s . (n + 2)) * (s1 . (n + 1)))) by Def6;

      then ((s1 . (n + 2)) - ((s . (n + 2)) * (s1 . (n + 1)))) > 0 by A1, Th52;

      then (((s1 . (n + 2)) - m) + m) > ( 0 + m) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: REAL_3:55

    (for n holds (( scf r) . n) > 0 ) implies for n st n >= 1 holds (1 / ((( c_d r) . n) * (( c_d r) . (n + 1)))) < (1 / ((( scf r) . (n + 1)) * ((( c_d r) . n) ^2 )))

    proof

      set s = ( scf r), s2 = ( c_d r);

      defpred X[ Nat] means (1 / ((s2 . $1) * (s2 . ($1 + 1)))) < (1 / ((s . ($1 + 1)) * ((s2 . $1) ^2 )));

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      then

       A2: (s . 2) > 0 ;

      

       A3: (( scf r) . 1) > 0 by A1;

      

       A4: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and (1 / ((s2 . n) * (s2 . (n + 1)))) < (1 / ((( scf r) . (n + 1)) * ((s2 . n) ^2 )));

        

         A5: (s2 . (n + 1)) > 0 by A3, Th52;

        then

         A6: ((s2 . (n + 1)) ^2 ) > 0 by SQUARE_1: 12;

        (s . (n + 2)) > 0 by A1;

        then

         A7: ((s . (n + 2)) * ((s2 . (n + 1)) ^2 )) > 0 by A6, XREAL_1: 129;

        (s2 . n) > 0 by A3, Th52;

        then

         A8: ((s2 . (n + 1)) * (s2 . n)) > 0 by A5, XREAL_1: 129;

        ((s2 . (n + 1)) * (s2 . ((n + 1) + 1))) = ((s2 . (n + 1)) * (((s . (n + 2)) * (s2 . (n + 1))) + (s2 . n))) by Def6

        .= (((s . (n + 2)) * ((s2 . (n + 1)) ^2 )) + ((s2 . (n + 1)) * (s2 . n)));

        hence thesis by A8, A7, XREAL_1: 29, XREAL_1: 76;

      end;

      

       A9: (s . 1) > 0 by A1;

      then ((s . 1) ^2 ) > 0 by SQUARE_1: 12;

      then ((s . 2) * ((s . 1) ^2 )) > 0 by A2, XREAL_1: 129;

      then

       A10: (1 / (((s . 2) * ((s . 1) ^2 )) + (s . 1))) < (1 / ((s . 2) * ((s . 1) ^2 ))) by A9, XREAL_1: 29, XREAL_1: 76;

      let n;

      (1 / ((s2 . 1) * (s2 . (1 + 1)))) = (1 / ((s2 . 1) * (((s . ( 0 + 2)) * (s2 . ( 0 + 1))) + (s2 . 0 )))) by Def6

      .= (1 / ((s2 . 1) * (((s . 2) * (s . 1)) + (s2 . 0 )))) by Def6

      .= (1 / ((s . 1) * (((s . 2) * (s . 1)) + (s2 . 0 )))) by Def6

      .= (1 / ((s . 1) * (((s . 2) * (s . 1)) + 1))) by Def6

      .= (1 / (((s . 2) * ((s . 1) ^2 )) + (s . 1)));

      then

       A11: X[1] by A10, Def6;

      for n be Nat st n >= 1 holds X[n] from NAT_1:sch 8( A11, A4);

      hence thesis;

    end;

    theorem :: REAL_3:56

    (for n holds (( scf r) . n) <= b) implies for n holds (( c_d r) . (n + 1)) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))

    proof

      set s = ( scf r);

      set s2 = ( c_d r);

      defpred P[ Nat] means (s2 . ($1 + 1)) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ($1 + 1));

      assume

       A1: for n holds (( scf r) . n) <= b;

      then

       A2: (s . 1) <= b;

      

       A3: (s . 2) <= b by A1;

      (s . 2) >= 0 & (s . 1) >= 0 by Th38;

      then

       A4: ((s . 2) * (s . 1)) <= (b ^2 ) by A2, A3, XREAL_1: 66;

      (s2 . (1 + 1)) = (((s . ( 0 + 2)) * (s2 . ( 0 + 1))) + (s2 . 0 )) by Def6

      .= (((s . 2) * (s2 . 1)) + 1) by Def6

      .= (((s . 2) * (s . 1)) + 1) by Def6;

      then

       A5: (s2 . (1 + 1)) <= ((b ^2 ) + 1) by A4, XREAL_1: 6;

      let n;

      ((b ^2 ) + 4) > (b ^2 ) by XREAL_1: 39;

      then ( sqrt ((b ^2 ) + 4)) > ( sqrt (b ^2 )) by SQUARE_1: 27;

      then

       A6: ( sqrt ((b ^2 ) + 4)) > b by SQUARE_1: 22;

      then (b + ( sqrt ((b ^2 ) + 4))) > (b + b) by XREAL_1: 8;

      then ((b + ( sqrt ((b ^2 ) + 4))) / 2) > ((2 * b) / 2) by XREAL_1: 74;

      then

       A7: (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ( 0 + 1)) > b;

      

       A8: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A9: (s2 . (n + 1)) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) and

         A10: (s2 . ((n + 1) + 1)) <= (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1));

        

         A11: ((b * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1))) + (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))) = ((b * ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((b + ( sqrt ((b ^2 ) + 4))) / 2))) + (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1))) by NEWTON: 6

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2));

        (n + 3) >= ( 0 + 1) by XREAL_1: 7;

        then

         A12: (s . (n + 3)) >= 0 by Th38;

        

         A13: (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 2) + 1)) = (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 2))

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ 2)) by NEWTON: 8

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * (((b + ( sqrt ((b ^2 ) + 4))) / 2) ^2 )) by WSIERP_1: 1

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + (( sqrt ((b ^2 ) + 4)) ^2 )) / (2 * 2)))

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + ((b ^2 ) + 4)) / (2 * 2))) by SQUARE_1:def 2

        .= ((((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (n + 1)) * ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2));

        

         A14: (s2 . ((n + 2) + 1)) = (((s . ((n + 1) + 2)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1))) by Def6

        .= (((s . (n + 3)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1)));

        (s . (n + 3)) <= b & (s2 . ((n + 1) + 1)) >= 0 by A1, Th51;

        then ((s . (n + 3)) * (s2 . ((n + 1) + 1))) <= (b * (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ ((n + 1) + 1))) by A10, A12, XREAL_1: 66;

        hence thesis by A9, A14, A11, A13, XREAL_1: 7;

      end;

      (b * ( sqrt ((b ^2 ) + 4))) >= (b * b) by A6, XREAL_1: 64;

      then ((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) >= ((b ^2 ) + (b * b)) by XREAL_1: 6;

      then (((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) >= (((b ^2 ) + (b ^2 )) + 2) by XREAL_1: 6;

      then

       A15: ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2) >= ((2 * ((b ^2 ) + 1)) / 2) by XREAL_1: 72;

      (((b + ( sqrt ((b ^2 ) + 4))) / 2) |^ (1 + 1)) = (((b + ( sqrt ((b ^2 ) + 4))) / 2) ^2 ) by WSIERP_1: 1

      .= ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + (( sqrt ((b ^2 ) + 4)) ^2 )) / (2 * 2))

      .= ((((b ^2 ) + ((2 * b) * ( sqrt ((b ^2 ) + 4)))) + ((b ^2 ) + 4)) / (2 * 2)) by SQUARE_1:def 2

      .= ((((b ^2 ) + (b * ( sqrt ((b ^2 ) + 4)))) + 2) / 2);

      then

       A16: P[1] by A5, A15, XXREAL_0: 2;

      (s2 . ( 0 + 1)) = (s . 1) by Def6;

      then

       A17: P[ 0 ] by A2, A7, XXREAL_0: 2;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A17, A16, A8);

      hence thesis;

    end;

    theorem :: REAL_3:57

    n1 = (( c_d r) . (n + 1)) & n2 = (( c_d r) . n) implies (n1 gcd n2) = 1

    proof

      set s = ( scf r);

      set s2 = ( c_d r);

      defpred X[ Nat] means for n1, n2 st n1 = (s2 . ($1 + 1)) & n2 = (s2 . $1) holds (n1 gcd n2) = 1;

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        (k + 2) >= ( 0 + 1) by XREAL_1: 7;

        then

        reconsider n4 = (s . (k + 2)) as Element of NAT by Th38, INT_1: 3;

        reconsider n3 = (s2 . (k + 2)) as Element of NAT by Th50;

        reconsider n2 = (s2 . k) as Element of NAT by Th50;

        reconsider n1 = (s2 . (k + 1)) as Element of NAT by Th50;

        assume for n1, n2 st n1 = (s2 . (k + 1)) & n2 = (s2 . k) holds (n1 gcd n2) = 1;

        then

         A2: (n1 gcd n2) = 1;

        n3 = ((n4 * n1) + n2) by Def6;

        hence thesis by A2, EULER_1: 8;

      end;

      

       A3: X[ 0 ]

      proof

        let n1, n2 such that n1 = (s2 . ( 0 + 1)) and

         A4: n2 = (s2 . 0 );

        (n1 gcd 1) = 1 by NEWTON: 51;

        hence thesis by A4, Def6;

      end;

      for n holds X[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: REAL_3:58

    

     Th58: (for n holds (( scf r) . n) > 0 ) implies for n holds ((( c_d r) . (n + 1)) / (( c_d r) . n)) >= (1 / (( scf r) . (n + 2)))

    proof

      set s = ( scf r);

      set s1 = ( c_d r);

      defpred X[ Nat] means ((s1 . ($1 + 1)) / (s1 . $1)) >= (1 / (s . ($1 + 2)));

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      then

       A2: (( scf r) . 1) <> 0 ;

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume ((s1 . (n + 1)) / (s1 . n)) >= (1 / (s . (n + 2)));

        set r = (s1 . (n + 1));

        

         A4: (s . 1) > 0 by A1;

        then

         A5: (s1 . (n + 1)) > 0 by Th52;

        (n + 3) >= ( 0 + 1) & (s . (n + 3)) <> 0 by A1, XREAL_1: 7;

        then (s . (n + 3)) >= 1 by Th40;

        then

         A6: (1 / (s . (n + 3))) <= (1 / 1) by XREAL_1: 118;

        (n + 2) >= ( 0 + 1) & (s . (n + 2)) <> 0 by A1, XREAL_1: 7;

        then

         A7: (s . (n + 2)) >= 1 by Th40;

        

         A8: (s1 . n) > 0 by A4, Th52;

        ((s1 . (n + 2)) / (s1 . (n + 1))) = ((((s . (n + 2)) * r) + (s1 . n)) / r) by Def6

        .= ((((s . (n + 2)) * r) / r) + ((s1 . n) / r))

        .= (((s . (n + 2)) * (r / r)) + ((s1 . n) / r))

        .= ((s . (n + 2)) + ((s1 . n) / r)) by A5, XCMPLX_1: 88;

        then ((s1 . (n + 2)) / (s1 . (n + 1))) >= (1 + 0 ) by A5, A8, A7, XREAL_1: 7;

        hence thesis by A6, XXREAL_0: 2;

      end;

      (( scf r) . 2) <> 0 by A1;

      then (s . ( 0 + 2)) >= 1 by Th40;

      then

       A9: (1 / (s . ( 0 + 2))) <= (1 / 1) by XREAL_1: 118;

      (s1 . 0 ) = 1 & (s1 . 1) = (s . 1) by Def6;

      then ((s1 . ( 0 + 1)) / (s1 . 0 )) >= 1 by A2, Th40;

      then

       A10: X[ 0 ] by A9, XXREAL_0: 2;

      for n holds X[n] from NAT_1:sch 2( A10, A3);

      hence thesis;

    end;

    theorem :: REAL_3:59

    (for n holds (( scf r) . n) > 0 ) implies for n holds (( c_d r) . (n + 2)) <= ((2 * (( scf r) . (n + 2))) * (( c_d r) . (n + 1)))

    proof

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      let n;

      set s = ( scf r);

      set s1 = ( c_d r);

      

       A2: (s . (n + 2)) > 0 by A1;

      (s . 1) > 0 by A1;

      then

       A3: (s1 . n) > 0 by Th52;

      

       A4: ((s1 . (n + 1)) / (s1 . n)) >= (1 / (s . (n + 2))) by A1, Th58;

      (((s1 . (n + 1)) / (s1 . n)) * (s1 . n)) = (((s1 . n) / (s1 . n)) * (s1 . (n + 1)))

      .= (s1 . (n + 1)) by A3, XCMPLX_1: 88;

      then

       A5: (s1 . (n + 1)) >= ((s1 . n) / (s . (n + 2))) by A4, A3, XREAL_1: 64;

      (((s1 . n) / (s . (n + 2))) * (s . (n + 2))) = (((s . (n + 2)) / (s . (n + 2))) * (s1 . n))

      .= (s1 . n) by A2, XCMPLX_1: 88;

      then ((s1 . (n + 1)) * (s . (n + 2))) >= (s1 . n) by A5, A2, XREAL_1: 64;

      then (((s1 . (n + 1)) * (s . (n + 2))) + ((s1 . (n + 1)) * (s . (n + 2)))) >= ((s1 . n) + ((s1 . (n + 1)) * (s . (n + 2)))) by XREAL_1: 6;

      hence thesis by Def6;

    end;

    theorem :: REAL_3:60

    (for n holds (( scf r) . n) <> 0 ) implies for n holds (1 / ((( scf r) . (n + 1)) * ((( c_d r) . n) ^2 ))) <= (1 / ((( c_d r) . n) ^2 ))

    proof

      assume

       A1: for n holds (( scf r) . n) <> 0 ;

      let n;

      set s = ( scf r);

      set s2 = ( c_d r);

      (s . 1) <> 0 by A1;

      then (s . 1) > 0 by Th38;

      then

       A2: (s2 . n) > 0 by Th52;

      (n + 1) >= (1 + 0 ) & (s . (n + 1)) <> 0 by A1, XREAL_1: 7;

      then ((s . (n + 1)) * ((s2 . n) ^2 )) >= (1 * ((s2 . n) ^2 )) by A2, Th40, XREAL_1: 64;

      hence thesis by A2, SQUARE_1: 12, XREAL_1: 118;

    end;

    theorem :: REAL_3:61

    (for n holds (( scf r) . n) <> 0 ) implies for n holds (( c_d r) . (n + 1)) >= ( tau |^ n)

    proof

      set s2 = ( c_d r);

      set s = ( scf r);

      defpred P[ Nat] means (s2 . ($1 + 1)) >= ( tau |^ $1);

      ( sqrt 5) < ( sqrt (3 ^2 )) by SQUARE_1: 27;

      then ( sqrt 5) < 3 by SQUARE_1: 22;

      then (1 + ( sqrt 5)) < (1 + 3) by XREAL_1: 8;

      then

       A1: (((1 + ( sqrt 5)) / 2) |^ 1) = ((1 + ( sqrt 5)) / 2) & ((1 + ( sqrt 5)) / 2) < (4 / 2) by XREAL_1: 74;

      assume

       A2: for n holds (( scf r) . n) <> 0 ;

      then

       A3: (s . 1) >= 1 by Th40;

      then (s2 . ( 0 + 1)) >= 1 by Def6;

      then

       A4: P[ 0 ] by NEWTON: 4;

      let n;

      

       A5: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A6: (s2 . (n + 1)) >= ( tau |^ n) and

         A7: (s2 . ((n + 1) + 1)) >= ( tau |^ (n + 1));

        

         A8: (( tau |^ (n + 1)) + ( tau |^ n)) = (((((1 + ( sqrt 5)) / 2) |^ n) * ((1 + ( sqrt 5)) / 2)) + (((1 + ( sqrt 5)) / 2) |^ n)) by FIB_NUM:def 1, NEWTON: 6

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((6 + (2 * ( sqrt 5))) / 4));

        ( sqrt 5) >= 0 by SQUARE_1:def 2;

        then ((1 + ( sqrt 5)) / 2) > 0 by XREAL_1: 139;

        then

         A9: ( tau |^ (n + 1)) > 0 by FIB_NUM:def 1, PREPOWER: 6;

        

         A10: ( tau |^ (n + 2)) = ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + ( sqrt 5)) / 2) |^ 2)) by FIB_NUM:def 1, NEWTON: 8

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + ( sqrt 5)) / 2) ^2 )) by WSIERP_1: 1

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((((1 ^2 ) + ((2 * 1) * ( sqrt 5))) + (( sqrt 5) ^2 )) / 4))

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * (((1 + (2 * ( sqrt 5))) + 5) / 4)) by SQUARE_1:def 2

        .= ((((1 + ( sqrt 5)) / 2) |^ n) * ((6 + (2 * ( sqrt 5))) / 4));

        

         A11: (s2 . ((n + 2) + 1)) = (((s . ((n + 1) + 2)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1))) by Def6

        .= (((s . (n + 3)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1)));

        (n + 3) >= ( 0 + 1) by XREAL_1: 7;

        then (s . (n + 3)) >= 1 by A2, Th40;

        then ((s . (n + 3)) * (s2 . ((n + 1) + 1))) >= (1 * ( tau |^ (n + 1))) by A7, A9, XREAL_1: 66;

        hence thesis by A6, A11, A8, A10, XREAL_1: 7;

      end;

      (s . 2) >= 1 by A2, Th40;

      then ((s . 2) * (s . 1)) >= 1 by A3, XREAL_1: 159;

      then

       A12: (((s . 2) * (s . 1)) + 1) >= (1 + 1) by XREAL_1: 6;

      (s2 . (1 + 1)) = (((s . ( 0 + 2)) * (s2 . ( 0 + 1))) + (s2 . 0 )) by Def6

      .= (((s . 2) * (s2 . 1)) + 1) by Def6

      .= (((s . 2) * (s . 1)) + 1) by Def6;

      then

       A13: P[1] by A12, A1, FIB_NUM:def 1, XXREAL_0: 2;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A4, A13, A5);

      hence thesis;

    end;

    theorem :: REAL_3:62

    a > 0 & (for n holds (( scf r) . n) >= a) implies for n holds (( c_d r) . (n + 1)) >= (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n)

    proof

      assume that

       A1: a > 0 and

       A2: for n holds (( scf r) . n) >= a;

      set s = ( scf r);

      set s2 = ( c_d r);

      defpred P[ Nat] means (s2 . ($1 + 1)) >= (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ $1);

      

       A3: (s . 1) > 0 by A1, A2;

      then (s . 1) >= 1 by Th40;

      then (s2 . ( 0 + 1)) >= 1 by Def6;

      then

       A4: P[ 0 ] by NEWTON: 4;

      (s . 2) > 0 by A1, A2;

      then ((s . 2) * (s . 1)) >= (1 * (s . 1)) by A3, Th40, XREAL_1: 64;

      then

       A5: (((s . 2) * (s . 1)) + 1) >= ((s . 1) + 1) by XREAL_1: 6;

      (s . 1) >= a by A2;

      then ((s . 1) + 1) >= (a + 1) by XREAL_1: 6;

      then

       A6: (((s . 2) * (s . 1)) + 1) >= (a + 1) by A5, XXREAL_0: 2;

      (4 * a) > 0 by A1, XREAL_1: 129;

      then ((a ^2 ) + 4) < (((a ^2 ) + 4) + (4 * a)) by XREAL_1: 39;

      then ( sqrt ((a ^2 ) + 4)) < ( sqrt ((a + 2) ^2 )) by SQUARE_1: 27;

      then ( sqrt ((a ^2 ) + 4)) < (a + 2) by SQUARE_1: 22;

      then (a + ( sqrt ((a ^2 ) + 4))) < (a + (a + 2)) by XREAL_1: 8;

      then

       A7: (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ 1) = ((a + ( sqrt ((a ^2 ) + 4))) / 2) & ((a + ( sqrt ((a ^2 ) + 4))) / 2) < (((2 * a) + (2 * 1)) / 2) by XREAL_1: 74;

      let n;

      

       A8: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A9: (s2 . (n + 1)) >= (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) and

         A10: (s2 . ((n + 1) + 1)) >= (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1));

        

         A11: ((a * (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1))) + (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n)) = ((a * ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((a + ( sqrt ((a ^2 ) + 4))) / 2))) + (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n)) by NEWTON: 6

        .= ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + (a * ( sqrt ((a ^2 ) + 4)))) + 2) / 2));

        ( sqrt ((a ^2 ) + 4)) > 0 by SQUARE_1: 25;

        then ((a + ( sqrt ((a ^2 ) + 4))) / 2) > 0 by XREAL_1: 139;

        then

         A12: (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1)) > 0 by PREPOWER: 6;

        

         A13: (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ (n + 2)) = ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ 2)) by NEWTON: 8

        .= ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * (((a + ( sqrt ((a ^2 ) + 4))) / 2) ^2 )) by WSIERP_1: 1

        .= ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + ((2 * a) * ( sqrt ((a ^2 ) + 4)))) + (( sqrt ((a ^2 ) + 4)) ^2 )) / (2 * 2)))

        .= ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + ((2 * a) * ( sqrt ((a ^2 ) + 4)))) + ((a ^2 ) + 4)) / (2 * 2))) by SQUARE_1:def 2

        .= ((((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + (a * ( sqrt ((a ^2 ) + 4)))) + 2) / 2));

        

         A14: (s2 . ((n + 2) + 1)) = (((s . ((n + 1) + 2)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1))) by Def6

        .= (((s . (n + 3)) * (s2 . ((n + 1) + 1))) + (s2 . (n + 1)));

        (s . (n + 3)) >= a by A2;

        then ((s . (n + 3)) * (s2 . ((n + 1) + 1))) >= (a * (((a + ( sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1))) by A10, A12, XREAL_1: 66;

        hence thesis by A9, A14, A11, A13, XREAL_1: 7;

      end;

      (s2 . (1 + 1)) = (((s . ( 0 + 2)) * (s2 . ( 0 + 1))) + (s2 . 0 )) by Def6

      .= (((s . 2) * (s2 . 1)) + 1) by Def6

      .= (((s . 2) * (s . 1)) + 1) by Def6;

      then

       A15: P[1] by A6, A7, XXREAL_0: 2;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A4, A15, A8);

      hence thesis;

    end;

    theorem :: REAL_3:63

    ((( c_n r) . (n + 2)) / (( c_d r) . (n + 2))) = ((((( scf r) . (n + 2)) * (( c_n r) . (n + 1))) + (( c_n r) . n)) / (((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)))

    proof

      (( c_n r) . (n + 2)) = (((( scf r) . (n + 2)) * (( c_n r) . (n + 1))) + (( c_n r) . n)) by Def5;

      hence thesis by Def6;

    end;

    theorem :: REAL_3:64

    

     Th64: (((( c_n r) . (n + 1)) * (( c_d r) . n)) - ((( c_n r) . n) * (( c_d r) . (n + 1)))) = (( - 1) |^ n)

    proof

      set s = ( scf r), s1 = ( c_n r), s2 = ( c_d r);

      defpred G[ Nat] means (((s1 . ($1 + 1)) * (s2 . $1)) - ((s1 . $1) * (s2 . ($1 + 1)))) = (( - 1) |^ $1);

      

       A1: (s2 . 0 ) = 1 & (s2 . 1) = (s . 1) by Def6;

      

       A2: for n st G[n] holds G[(n + 1)]

      proof

        let l;

        assume

         A3: (((s1 . (l + 1)) * (s2 . l)) - ((s1 . l) * (s2 . (l + 1)))) = (( - 1) |^ l);

        (((s1 . (l + 2)) * (s2 . (l + 1))) - ((s1 . (l + 1)) * (s2 . (l + 2)))) = (((((s . (l + 2)) * (s1 . (l + 1))) + (s1 . l)) * (s2 . (l + 1))) - ((s1 . (l + 1)) * (s2 . (l + 2)))) by Def5

        .= (((((s . (l + 2)) * (s1 . (l + 1))) * (s2 . (l + 1))) + ((s1 . l) * (s2 . (l + 1)))) - ((s1 . (l + 1)) * (((s . (l + 2)) * (s2 . (l + 1))) + (s2 . l)))) by Def6

        .= (( - 1) * (((s1 . (l + 1)) * (s2 . l)) - ((s1 . l) * (s2 . (l + 1)))))

        .= (( - 1) |^ (l + 1)) by A3, NEWTON: 6;

        hence thesis;

      end;

      (s1 . 0 ) = (s . 0 ) & (s1 . 1) = (((s . 1) * (s . 0 )) + 1) by Def5;

      then

       A4: G[ 0 ] by A1, NEWTON: 4;

      for n holds G[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: REAL_3:65

    

     Th65: (for n holds (( c_d r) . n) <> 0 ) implies (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((( c_n r) . n) / (( c_d r) . n))) = ((( - 1) |^ n) / ((( c_d r) . (n + 1)) * (( c_d r) . n)))

    proof

      set s1 = ( c_n r), s2 = ( c_d r);

      assume for n holds (s2 . n) <> 0 ;

      then (s2 . n) <> 0 & (s2 . (n + 1)) <> 0 ;

      

      then (((s1 . (n + 1)) / (s2 . (n + 1))) - ((s1 . n) / (s2 . n))) = ((((s1 . (n + 1)) * (s2 . n)) - ((s1 . n) * (s2 . (n + 1)))) / ((s2 . (n + 1)) * (s2 . n))) by XCMPLX_1: 130

      .= ((( - 1) |^ n) / ((s2 . (n + 1)) * (s2 . n))) by Th64;

      hence thesis;

    end;

    theorem :: REAL_3:66

    

     Th66: (((( c_n r) . (n + 2)) * (( c_d r) . n)) - ((( c_n r) . n) * (( c_d r) . (n + 2)))) = ((( - 1) |^ n) * (( scf r) . (n + 2)))

    proof

      set s1 = ( c_n r), s2 = ( c_d r), s = ( scf r);

      (((s1 . (n + 2)) * (s2 . n)) - ((s1 . n) * (s2 . (n + 2)))) = (((((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) * (s2 . n)) - ((s1 . n) * (s2 . (n + 2)))) by Def5

      .= (((((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) * (s2 . n)) - ((s1 . n) * (((s . (n + 2)) * (s2 . (n + 1))) + (s2 . n)))) by Def6

      .= ((s . (n + 2)) * (((s1 . (n + 1)) * (s2 . n)) - ((s1 . n) * (s2 . (n + 1)))))

      .= ((( - 1) |^ n) * (s . (n + 2))) by Th64;

      hence thesis;

    end;

    theorem :: REAL_3:67

    (for n holds (( c_d r) . n) <> 0 ) implies (((( c_n r) . (n + 2)) / (( c_d r) . (n + 2))) - ((( c_n r) . n) / (( c_d r) . n))) = (((( - 1) |^ n) * (( scf r) . (n + 2))) / ((( c_d r) . (n + 2)) * (( c_d r) . n)))

    proof

      set s1 = ( c_n r), s2 = ( c_d r), s = ( scf r);

      assume for n holds (s2 . n) <> 0 ;

      then (s2 . n) <> 0 & (s2 . (n + 2)) <> 0 ;

      

      then (((s1 . (n + 2)) / (s2 . (n + 2))) - ((s1 . n) / (s2 . n))) = ((((s1 . (n + 2)) * (s2 . n)) - ((s1 . n) * (s2 . (n + 2)))) / ((s2 . (n + 2)) * (s2 . n))) by XCMPLX_1: 130

      .= (((( - 1) |^ n) * (s . (n + 2))) / ((s2 . (n + 2)) * (s2 . n))) by Th66;

      hence thesis;

    end;

    theorem :: REAL_3:68

    (for n holds (( scf r) . n) <> 0 ) implies for n st n >= 1 holds ((( c_n r) . n) / (( c_d r) . n)) = (((( c_n r) . (n + 1)) - (( c_n r) . (n - 1))) / ((( c_d r) . (n + 1)) - (( c_d r) . (n - 1))))

    proof

      set s1 = ( c_n r), s2 = ( c_d r);

      set s = ( scf r);

      defpred P[ Nat] means ((s1 . $1) / (s2 . $1)) = (((s1 . ($1 + 1)) - (s1 . ($1 - 1))) / ((s2 . ($1 + 1)) - (s2 . ($1 - 1))));

      assume

       A1: for n holds (( scf r) . n) <> 0 ;

      

       A2: for n be Nat st n >= 1 holds P[n] implies P[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and ((s1 . n) / (s2 . n)) = (((s1 . (n + 1)) - (s1 . (n - 1))) / ((s2 . (n + 1)) - (s2 . (n - 1))));

        ((((s . (n + 2)) * (s1 . (n + 1))) + (s1 . n)) - (s1 . n)) = ((s1 . (n + 2)) - (s1 . n)) & ((s2 . (n + 2)) - (s2 . n)) = ((((s . (n + 2)) * (s2 . (n + 1))) + (s2 . n)) - (s2 . n)) by Def5, Def6;

        hence thesis by A1, XCMPLX_1: 91;

      end;

      let n;

      (((s1 . (1 + 1)) - (s1 . (1 - 1))) / ((s2 . (1 + 1)) - (s2 . (1 - 1)))) = (((((s . (2 + 0 )) * (s1 . ( 0 + 1))) + (s1 . 0 )) - (s1 . 0 )) / ((s2 . (2 + 0 )) - (s2 . 0 ))) by Def5

      .= (((((s . 2) * (s1 . 1)) + (s1 . 0 )) - (s1 . 0 )) / ((((s . 2) * (s2 . 1)) + (s2 . 0 )) - (s2 . 0 ))) by Def6

      .= ((s1 . 1) / (s2 . 1)) by A1, XCMPLX_1: 91;

      then

       A3: P[1];

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A3, A2);

      hence thesis;

    end;

    theorem :: REAL_3:69

    (for n holds (( c_d r) . n) <> 0 ) implies for n holds |.(((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((( c_n r) . n) / (( c_d r) . n))).| = (1 / |.((( c_d r) . (n + 1)) * (( c_d r) . n)).|)

    proof

      set s1 = ( c_n r), s2 = ( c_d r);

      assume

       A1: for n holds (s2 . n) <> 0 ;

      let n;

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

       |.(((s1 . (n + 1)) / (s2 . (n + 1))) - ((s1 . n) / (s2 . n))).| = |.((( - 1) |^ n) / ((s2 . (n + 1)) * (s2 . n))).| by A1, Th65

      .= ( |.(( - 1) |^ n).| / |.((s2 . (n + 1)) * (s2 . n)).|) by COMPLEX1: 67

      .= ( |.(( - 1) to_power n).| / |.((s2 . (n + 1)) * (s2 . n)).|) by POWER: 41

      .= (( |.( - 1).| to_power n) / |.((s2 . (n + 1)) * (s2 . n)).|) by SERIES_1: 2

      .= ((( - ( - 1)) to_power n) / |.((s2 . (n + 1)) * (s2 . n)).|) by ABSVALUE:def 1

      .= (1 / |.((s2 . (n + 1)) * (s2 . n)).|) by POWER: 26;

      hence thesis;

    end;

    theorem :: REAL_3:70

    (( scf r) . 1) > 0 implies for n holds ((( c_n r) . ((2 * n) + 1)) / (( c_d r) . ((2 * n) + 1))) > ((( c_n r) . (2 * n)) / (( c_d r) . (2 * n)))

    proof

      set s1 = ( c_n r), s2 = ( c_d r), s = ( scf r);

      defpred X[ Nat] means ((s1 . ((2 * $1) + 1)) / (s2 . ((2 * $1) + 1))) > ((s1 . (2 * $1)) / (s2 . (2 * $1)));

      

       A1: ((s1 . (2 * 0 )) / (s2 . (2 * 0 ))) = ((s . 0 ) / (s2 . 0 )) by Def5

      .= ((s . 0 ) / 1) by Def6

      .= (s . 0 );

      assume

       A2: (( scf r) . 1) > 0 ;

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume ((s1 . ((2 * n) + 1)) / (s2 . ((2 * n) + 1))) > ((s1 . (2 * n)) / (s2 . (2 * n)));

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

        (((s1 . ((2 * (n + 1)) + 1)) * (s2 . (2 * (n + 1)))) - ((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) + 1)))) = (( - 1) |^ (2 * (n + 1))) by Th64

        .= (1 |^ (2 * (n + 1))) by WSIERP_1: 2

        .= 1;

        then

         A4: ((s1 . ((2 * (n + 1)) + 1)) * (s2 . (2 * (n + 1)))) > ((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) + 1))) by XREAL_1: 47;

        (s2 . ((2 * (n + 1)) + 1)) > 0 & (s2 . (2 * (n + 1))) > 0 by A2, Th52;

        hence thesis by A4, XREAL_1: 106;

      end;

      ((s1 . ((2 * 0 ) + 1)) / (s2 . ((2 * 0 ) + 1))) = ((((s . 1) * (s . 0 )) + 1) / (s2 . 1)) by Def5

      .= ((((s . 1) * (s . 0 )) + 1) / (s . 1)) by Def6

      .= ((s . 0 ) + (1 / (s . 1))) by A2, XCMPLX_1: 113;

      then

       A5: X[ 0 ] by A2, A1, XREAL_1: 29;

      for n holds X[n] from NAT_1:sch 2( A5, A3);

      hence thesis;

    end;

    definition

      let r be Real;

      ::$Notion-Name

      :: REAL_3:def7

      func convergents_of_continued_fractions (r) -> Real_Sequence equals (( c_n r) /" ( c_d r));

      coherence ;

    end

    notation

      let r be Real;

      synonym cocf (r) for convergents_of_continued_fractions (r);

    end

    theorem :: REAL_3:71

    (( cocf r) . 0 ) = (( scf r) . 0 )

    proof

      

      thus (( cocf r) . 0 ) = ((( c_n r) . 0 ) * ((( c_d r) " ) . 0 )) by SEQ_1: 8

      .= ((( c_n r) . 0 ) * ((( c_d r) . 0 ) " )) by VALUED_1: 10

      .= ((( c_n r) . 0 ) * (1 / (( c_d r) . 0 )))

      .= ((( c_n r) . 0 ) / (( c_d r) . 0 ))

      .= ((( scf r) . 0 ) / (( c_d r) . 0 )) by Def5

      .= ((( scf r) . 0 ) / 1) by Def6

      .= (( scf r) . 0 );

    end;

    theorem :: REAL_3:72

    

     Th72: (( scf r) . 1) <> 0 implies (( cocf r) . 1) = ((( scf r) . 0 ) + (1 / (( scf r) . 1)))

    proof

      set s = ( scf r);

      assume

       A1: (( scf r) . 1) <> 0 ;

      

      thus (( cocf r) . 1) = ((( c_n r) . 1) * ((( c_d r) " ) . 1)) by SEQ_1: 8

      .= ((( c_n r) . 1) * ((( c_d r) . 1) " )) by VALUED_1: 10

      .= ((( c_n r) . 1) * (1 / (( c_d r) . 1)))

      .= ((( c_n r) . 1) / (( c_d r) . 1))

      .= ((((s . 1) * (s . 0 )) + 1) / (( c_d r) . 1)) by Def5

      .= ((((s . 1) * (s . 0 )) + 1) / (s . 1)) by Def6

      .= ((s . 0 ) + (1 / (s . 1))) by A1, XCMPLX_1: 113;

    end;

    theorem :: REAL_3:73

    

     Th73: (for n holds (( scf r) . n) > 0 ) implies (( cocf r) . 2) = ((( scf r) . 0 ) + (1 / ((( scf r) . 1) + (1 / (( scf r) . 2)))))

    proof

      set s = ( scf r);

      

       A1: (( cocf r) . 2) = ((( c_n r) . 2) * ((( c_d r) " ) . 2)) by SEQ_1: 8

      .= ((( c_n r) . 2) * ((( c_d r) . 2) " )) by VALUED_1: 10

      .= ((( c_n r) . 2) * (1 / (( c_d r) . 2)))

      .= ((( c_n r) . 2) / (( c_d r) . 2));

      assume

       A2: for n holds (( scf r) . n) > 0 ;

      then

       A3: (s . 1) > 0 ;

      

       A4: (( c_d r) . 2) = (((s . ( 0 + 2)) * (( c_d r) . ( 0 + 1))) + (( c_d r) . 0 )) by Def6

      .= (((s . 2) * (s . 1)) + (( c_d r) . 0 )) by Def6

      .= (((s . 2) * (s . 1)) + 1) by Def6;

      

       A5: (( c_n r) . 2) = (((s . ( 0 + 2)) * (( c_n r) . ( 0 + 1))) + (( c_n r) . 0 )) by Def5

      .= (((s . 2) * (((s . 1) * (s . 0 )) + 1)) + (( c_n r) . 0 )) by Def5

      .= (((((s . 2) * (s . 1)) * (s . 0 )) + (s . 2)) + (s . 0 )) by Def5;

      

       A6: (s . 2) > 0 by A2;

      

      then ((s . 0 ) + (1 / ((s . 1) + (1 / (s . 2))))) = ((s . 0 ) + (1 / ((((s . 1) * (s . 2)) + 1) / (s . 2)))) by XCMPLX_1: 113

      .= ((s . 0 ) + ((s . 2) / (((s . 1) * (s . 2)) + 1))) by XCMPLX_1: 57

      .= ((((s . 0 ) * (((s . 1) * (s . 2)) + 1)) + (s . 2)) / (((s . 1) * (s . 2)) + 1)) by A3, A6, XCMPLX_1: 113

      .= (( cocf r) . 2) by A1, A5, A4;

      hence thesis;

    end;

    theorem :: REAL_3:74

    

     Th74: (for n holds (( scf r) . n) > 0 ) implies (( cocf r) . 3) = ((( scf r) . 0 ) + (1 / ((( scf r) . 1) + (1 / ((( scf r) . 2) + (1 / (( scf r) . 3)))))))

    proof

      set s = ( scf r);

      

       A1: (( cocf r) . 3) = ((( c_n r) . 3) * ((( c_d r) " ) . 3)) by SEQ_1: 8

      .= ((( c_n r) . 3) * ((( c_d r) . 3) " )) by VALUED_1: 10

      .= ((( c_n r) . 3) * (1 / (( c_d r) . 3)))

      .= ((( c_n r) . 3) / (( c_d r) . 3));

      assume

       A2: for n holds (( scf r) . n) > 0 ;

      then

       A3: (s . 1) > 0 ;

      

       A4: (( c_d r) . 2) = (((s . ( 0 + 2)) * (( c_d r) . ( 0 + 1))) + (( c_d r) . 0 )) by Def6

      .= (((s . 2) * (s . 1)) + (( c_d r) . 0 )) by Def6

      .= (((s . 2) * (s . 1)) + 1) by Def6;

      

       A5: (( c_d r) . 3) = (((s . (1 + 2)) * (( c_d r) . (1 + 1))) + (( c_d r) . 1)) by Def6

      .= (((s . 3) * (((s . 2) * (s . 1)) + 1)) + (s . 1)) by A4, Def6

      .= (((s . 1) * (((s . 2) * (s . 3)) + 1)) + (s . 3));

      

       A6: (( c_n r) . 2) = (((s . ( 0 + 2)) * (( c_n r) . ( 0 + 1))) + (( c_n r) . 0 )) by Def5

      .= (((s . 2) * (((s . 1) * (s . 0 )) + 1)) + (( c_n r) . 0 )) by Def5

      .= (((((s . 2) * (s . 1)) * (s . 0 )) + (s . 2)) + (s . 0 )) by Def5;

      

       A7: (( c_n r) . 3) = (((s . (1 + 2)) * (( c_n r) . (1 + 1))) + (( c_n r) . 1)) by Def5

      .= (((s . 3) * (((((s . 2) * (s . 1)) * (s . 0 )) + (s . 2)) + (s . 0 ))) + (((s . 1) * (s . 0 )) + 1)) by A6, Def5

      .= ((((((((s . 3) * (s . 2)) * (s . 1)) * (s . 0 )) + ((s . 3) * (s . 2))) + ((s . 3) * (s . 0 ))) + ((s . 1) * (s . 0 ))) + 1);

      

       A8: (s . 2) > 0 by A2;

      

       A9: (s . 3) > 0 by A2;

      

      then ((s . 0 ) + (1 / ((s . 1) + (1 / ((s . 2) + (1 / (s . 3))))))) = ((s . 0 ) + (1 / ((s . 1) + (1 / ((((s . 2) * (s . 3)) + 1) / (s . 3)))))) by XCMPLX_1: 113

      .= ((s . 0 ) + (1 / ((s . 1) + ((s . 3) / (((s . 2) * (s . 3)) + 1))))) by XCMPLX_1: 57

      .= ((s . 0 ) + (1 / ((((s . 1) * (((s . 2) * (s . 3)) + 1)) + (s . 3)) / (((s . 2) * (s . 3)) + 1)))) by A8, A9, XCMPLX_1: 113

      .= ((s . 0 ) + ((((s . 2) * (s . 3)) + 1) / (((s . 1) * (((s . 2) * (s . 3)) + 1)) + (s . 3)))) by XCMPLX_1: 57

      .= ((((s . 0 ) * (((s . 1) * (((s . 2) * (s . 3)) + 1)) + (s . 3))) + (((s . 2) * (s . 3)) + 1)) / (((s . 1) * (((s . 2) * (s . 3)) + 1)) + (s . 3))) by A3, A8, A9, XCMPLX_1: 113;

      hence thesis by A1, A7, A5;

    end;

    theorem :: REAL_3:75

    (for n holds (( scf r) . n) > 0 ) implies for n st n >= 1 holds ((( c_n r) . ((2 * n) + 1)) / (( c_d r) . ((2 * n) + 1))) < ((( c_n r) . ((2 * n) - 1)) / (( c_d r) . ((2 * n) - 1)))

    proof

      set s = ( scf r), s1 = ( c_n r), s2 = ( c_d r);

      defpred X[ Nat] means ((s1 . ((2 * $1) + 1)) / (s2 . ((2 * $1) + 1))) < ((s1 . ((2 * $1) - 1)) / (s2 . ((2 * $1) - 1)));

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      then

       A2: (s . 3) > 0 ;

      (( cocf r) . 3) = ((( c_n r) . 3) * ((( c_d r) " ) . 3)) by SEQ_1: 8

      .= ((( c_n r) . 3) * ((( c_d r) . 3) " )) by VALUED_1: 10

      .= ((( c_n r) . 3) * (1 / (( c_d r) . 3)))

      .= ((( c_n r) . 3) / (( c_d r) . 3));

      

      then

       A3: ((s1 . ((2 * 1) + 1)) / (s2 . ((2 * 1) + 1))) = ((s . 0 ) + (1 / ((s . 1) + (1 / ((s . 2) + (1 / (s . 3))))))) by A1, Th74

      .= ((s . 0 ) + (1 / ((s . 1) + (1 / ((((s . 2) * (s . 3)) + 1) / (s . 3)))))) by A2, XCMPLX_1: 113

      .= ((s . 0 ) + (1 / ((s . 1) + ((s . 3) / (((s . 2) * (s . 3)) + 1))))) by XCMPLX_1: 57;

      let n;

      

       A4: (s . 1) > 0 by A1;

      

       A5: (( scf r) . 1) > 0 by A1;

      

       A6: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and ((s1 . ((2 * n) + 1)) / (s2 . ((2 * n) + 1))) < ((s1 . ((2 * n) - 1)) / (s2 . ((2 * n) - 1)));

        (((s1 . ((2 * (n + 1)) + 1)) * (s2 . ((2 * (n + 1)) - 1))) - ((s1 . ((2 * (n + 1)) - 1)) * (s2 . ((2 * (n + 1)) + 1)))) = (((((s . (((2 * n) + 1) + 2)) * (s1 . (((2 * n) + 1) + 1))) + (s1 . ((2 * n) + 1))) * (s2 . ((2 * n) + 1))) - ((s1 . ((2 * n) + 1)) * (s2 . ((2 * n) + 3)))) by Def5

        .= (((((s . (((2 * n) + 1) + 2)) * (s1 . (((2 * n) + 1) + 1))) + (s1 . ((2 * n) + 1))) * (s2 . ((2 * n) + 1))) - ((s1 . ((2 * n) + 1)) * (((s . (((2 * n) + 1) + 2)) * (s2 . (((2 * n) + 1) + 1))) + (s2 . ((2 * n) + 1))))) by Def6

        .= ((s . (((2 * n) + 1) + 2)) * (((s1 . (((2 * n) + 1) + 1)) * (s2 . ((2 * n) + 1))) - ((s1 . ((2 * n) + 1)) * (s2 . (((2 * n) + 1) + 1)))))

        .= ((s . (((2 * n) + 1) + 2)) * (( - 1) |^ ((2 * n) + 1))) by Th64

        .= ((s . (((2 * n) + 1) + 2)) * ( - (1 |^ ((2 * n) + 1)))) by WSIERP_1: 2

        .= ((s . (((2 * n) + 1) + 2)) * ( - 1));

        then (((s1 . ((2 * (n + 1)) + 1)) * (s2 . ((2 * (n + 1)) - 1))) - ((s1 . ((2 * (n + 1)) - 1)) * (s2 . ((2 * (n + 1)) + 1)))) < 0 by A1, XREAL_1: 132;

        then

         A7: ((s1 . ((2 * (n + 1)) + 1)) * (s2 . ((2 * (n + 1)) - 1))) < ((s1 . ((2 * (n + 1)) - 1)) * (s2 . ((2 * (n + 1)) + 1))) by XREAL_1: 48;

        (s2 . ((2 * n) + 1)) > 0 & (s2 . ((2 * n) + 3)) > 0 by A5, Th52;

        hence thesis by A7, XREAL_1: 106;

      end;

      (s . 2) > 0 by A1;

      then ((s . 3) / (((s . 2) * (s . 3)) + 1)) > 0 by A2, XREAL_1: 139;

      then

       A8: (1 / ((s . 1) + ((s . 3) / (((s . 2) * (s . 3)) + 1)))) < (1 / (s . 1)) by A4, XREAL_1: 29, XREAL_1: 76;

      ((s1 . ((2 * 1) - 1)) / (s2 . ((2 * 1) - 1))) = ((((s . 1) * (s . 0 )) + 1) / (s2 . 1)) by Def5

      .= ((((s . 1) * (s . 0 )) + 1) / (s . 1)) by Def6

      .= ((s . 0 ) + (1 / (s . 1))) by A4, XCMPLX_1: 113;

      then

       A9: X[1] by A8, A3, XREAL_1: 8;

      for n be Nat st n >= 1 holds X[n] from NAT_1:sch 8( A9, A6);

      hence thesis;

    end;

    theorem :: REAL_3:76

    (for n holds (( scf r) . n) > 0 ) implies for n st n >= 1 holds ((( c_n r) . (2 * n)) / (( c_d r) . (2 * n))) > ((( c_n r) . ((2 * n) - 2)) / (( c_d r) . ((2 * n) - 2)))

    proof

      set s = ( scf r), s1 = ( c_n r), s2 = ( c_d r);

      defpred X[ Nat] means ((s1 . (2 * $1)) / (s2 . (2 * $1))) > ((s1 . ((2 * $1) - 2)) / (s2 . ((2 * $1) - 2)));

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      then

       A2: (s . 1) > 0 ;

      

       A3: (( scf r) . 1) > 0 by A1;

      

       A4: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and ((s1 . (2 * n)) / (s2 . (2 * n))) > ((s1 . ((2 * n) - 2)) / (s2 . ((2 * n) - 2)));

        (((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) - 2))) - ((s1 . ((2 * (n + 1)) - 2)) * (s2 . (2 * (n + 1))))) = (((((s . ((2 * n) + 2)) * (s1 . ((2 * n) + 1))) + (s1 . (2 * n))) * (s2 . (2 * n))) - ((s1 . (2 * n)) * (s2 . ((2 * n) + 2)))) by Def5

        .= (((((s . ((2 * n) + 2)) * (s1 . ((2 * n) + 1))) + (s1 . (2 * n))) * (s2 . (2 * n))) - ((s1 . (2 * n)) * (((s . ((2 * n) + 2)) * (s2 . ((2 * n) + 1))) + (s2 . (2 * n))))) by Def6

        .= ((s . ((2 * n) + 2)) * (((s1 . ((2 * n) + 1)) * (s2 . (2 * n))) - ((s1 . (2 * n)) * (s2 . ((2 * n) + 1)))))

        .= ((s . ((2 * n) + 2)) * (( - 1) |^ (2 * n))) by Th64

        .= ((s . ((2 * n) + 2)) * (1 |^ (2 * n))) by WSIERP_1: 2

        .= ((s . ((2 * n) + 2)) * 1)

        .= (s . ((2 * n) + 2));

        then

         A5: ((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) - 2))) > ((s1 . ((2 * (n + 1)) - 2)) * (s2 . (2 * (n + 1)))) by A1, XREAL_1: 47;

        (s2 . (2 * n)) > 0 & (s2 . ((2 * n) + 2)) > 0 by A3, Th52;

        hence thesis by A5, XREAL_1: 106;

      end;

      let n;

      

       A6: ((s1 . ((2 * 1) - 2)) / (s2 . ((2 * 1) - 2))) = ((s . 0 ) / (s2 . 0 )) by Def5

      .= ((s . 0 ) / 1) by Def6

      .= (s . 0 );

      

       A7: (s . 2) > 0 by A1;

      (( cocf r) . 2) = ((( c_n r) . 2) * ((( c_d r) " ) . 2)) by SEQ_1: 8

      .= ((( c_n r) . 2) * ((( c_d r) . 2) " )) by VALUED_1: 10

      .= ((( c_n r) . 2) * (1 / (( c_d r) . 2)))

      .= ((( c_n r) . 2) / (( c_d r) . 2));

      

      then ((s1 . (2 * 1)) / (s2 . (2 * 1))) = ((s . 0 ) + (1 / ((s . 1) + (1 / (s . 2))))) by A1, Th73

      .= ((s . 0 ) + (1 / ((((s . 1) * (s . 2)) + 1) / (s . 2)))) by A7, XCMPLX_1: 113

      .= ((s . 0 ) + ((s . 2) / (((s . 1) * (s . 2)) + 1))) by XCMPLX_1: 57;

      then

       A8: X[1] by A2, A7, A6, XREAL_1: 29, XREAL_1: 139;

      for n be Nat st n >= 1 holds X[n] from NAT_1:sch 8( A8, A4);

      hence thesis;

    end;

    theorem :: REAL_3:77

    (for n holds (( scf r) . n) > 0 ) implies for n st n >= 1 holds ((( c_n r) . (2 * n)) / (( c_d r) . (2 * n))) < ((( c_n r) . ((2 * n) - 1)) / (( c_d r) . ((2 * n) - 1)))

    proof

      set s = ( scf r), s1 = ( c_n r), s2 = ( c_d r);

      defpred X[ Nat] means ((s1 . (2 * $1)) / (s2 . (2 * $1))) < ((s1 . ((2 * $1) - 1)) / (s2 . ((2 * $1) - 1)));

      assume

       A1: for n holds (( scf r) . n) > 0 ;

      then (s . 1) > 0 & (s . 2) > 0 ;

      then

       A2: (1 / ((s . 1) + (1 / (s . 2)))) < (1 / (s . 1)) by XREAL_1: 29, XREAL_1: 76;

      let n;

      

       A3: (( scf r) . 1) > 0 by A1;

      

       A4: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and ((s1 . (2 * n)) / (s2 . (2 * n))) < ((s1 . ((2 * n) - 1)) / (s2 . ((2 * n) - 1)));

        (((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) - 1))) - ((s1 . ((2 * (n + 1)) - 1)) * (s2 . (2 * (n + 1))))) = (((s1 . (((2 * n) + 1) + 1)) * (s2 . ((2 * n) + 1))) - ((s1 . ((2 * n) + 1)) * (s2 . (((2 * n) + 1) + 1))))

        .= (( - 1) |^ ((2 * n) + 1)) by Th64

        .= ( - (1 |^ ((2 * n) + 1))) by WSIERP_1: 2

        .= ( - 1);

        then

         A5: ((s1 . (2 * (n + 1))) * (s2 . ((2 * (n + 1)) - 1))) < ((s1 . ((2 * (n + 1)) - 1)) * (s2 . (2 * (n + 1)))) by XREAL_1: 48;

        (s2 . ((2 * n) + 1)) > 0 & (s2 . ((2 * n) + 2)) > 0 by A3, Th52;

        hence thesis by A5, XREAL_1: 106;

      end;

      (( cocf r) . 1) = ((( c_n r) . 1) * ((( c_d r) " ) . 1)) by SEQ_1: 8

      .= ((( c_n r) . 1) * ((( c_d r) . 1) " )) by VALUED_1: 10

      .= ((( c_n r) . 1) * (1 / (( c_d r) . 1)))

      .= ((s1 . ((2 * 1) - 1)) / (s2 . ((2 * 1) - 1)));

      then

       A6: ((s1 . ((2 * 1) - 1)) / (s2 . ((2 * 1) - 1))) = ((s . 0 ) + (1 / (s . 1))) by A3, Th72;

      (( cocf r) . 2) = ((( c_n r) . 2) * ((( c_d r) " ) . 2)) by SEQ_1: 8

      .= ((( c_n r) . 2) * ((( c_d r) . 2) " )) by VALUED_1: 10

      .= ((( c_n r) . 2) * (1 / (( c_d r) . 2)))

      .= ((s1 . (2 * 1)) / (s2 . (2 * 1)));

      then ((s1 . (2 * 1)) / (s2 . (2 * 1))) = ((s . 0 ) + (1 / ((s . 1) + (1 / (s . 2))))) by A1, Th73;

      then

       A7: X[1] by A6, A2, XREAL_1: 8;

      for n be Nat st n >= 1 holds X[n] from NAT_1:sch 8( A7, A4);

      hence thesis;

    end;

    definition

      let r be Real;

      set s = ( scf r);

      :: REAL_3:def8

      func backContinued_fraction r -> Real_Sequence means

      : Def8: (it . 0 ) = (( scf r) . 0 ) & for n be Nat holds (it . (n + 1)) = ((1 / (it . n)) + (( scf r) . (n + 1)));

      existence

      proof

        deffunc U( Nat, Real) = ( In (((1 / $2) + (s . ($1 + 1))), REAL ));

        consider f be Real_Sequence such that

         A1: (f . 0 ) = (s . 0 ) and

         A2: for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

        take f;

        thus (f . 0 ) = (( scf r) . 0 ) by A1;

        let n;

        (f . (n + 1)) = U(n,.) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let s1, s2;

        assume that

         A3: (s1 . 0 ) = (s . 0 ) and

         A4: for n holds (s1 . (n + 1)) = ((1 / (s1 . n)) + (s . (n + 1))) and

         A5: (s2 . 0 ) = (s . 0 ) and

         A6: for n holds (s2 . (n + 1)) = ((1 / (s2 . n)) + (s . (n + 1)));

        defpred X[ Nat] means (s1 . $1) = (s2 . $1);

        

         A7: for k st X[k] holds X[(k + 1)]

        proof

          let k;

          assume (s1 . k) = (s2 . k);

          

          hence (s1 . (k + 1)) = ((1 / (s2 . k)) + (s . (k + 1))) by A4

          .= (s2 . (k + 1)) by A6;

        end;

        let x be Element of NAT ;

        

         A8: X[ 0 ] by A3, A5;

        for n holds X[n] from NAT_1:sch 2( A8, A7);

        hence (s1 . x) = (s2 . x);

      end;

    end

    notation

      let r be Real;

      synonym bcf r for backContinued_fraction r;

    end

    theorem :: REAL_3:78

    (( scf r) . 0 ) > 0 implies for n holds (( bcf r) . (n + 1)) = ((( c_n r) . (n + 1)) / (( c_n r) . n))

    proof

      set s1 = ( c_n r);

      set s = ( scf r);

      defpred X[ Nat] means (( bcf r) . ($1 + 1)) = ((s1 . ($1 + 1)) / (s1 . $1));

      set s3 = ( bcf r);

      assume

       A1: (( scf r) . 0 ) > 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( bcf r) . (n + 1)) = ((s1 . (n + 1)) / (s1 . n));

        

         A4: (s1 . (n + 1)) > 0 by A1, Th45;

        (( bcf r) . ((n + 1) + 1)) = ((1 / (s3 . (n + 1))) + (s . ((n + 1) + 1))) by Def8

        .= (((s1 . n) / (s1 . (n + 1))) + (s . ((n + 1) + 1))) by A3, XCMPLX_1: 57

        .= (((s1 . n) + ((s . (n + 2)) * (s1 . (n + 1)))) / (s1 . (n + 1))) by A4, XCMPLX_1: 113

        .= ((s1 . (n + 2)) / (s1 . (n + 1))) by Def5;

        hence thesis;

      end;

      (( bcf r) . ( 0 + 1)) = ((1 / (s3 . 0 )) + (s . ( 0 + 1))) by Def8

      .= ((1 / (s . 0 )) + (s . 1)) by Def8

      .= ((1 + ((s . 0 ) * (s . 1))) / (s . 0 )) by A1, XCMPLX_1: 113

      .= ((s1 . 1) / (s . 0 )) by Def5

      .= ((s1 . ( 0 + 1)) / (s1 . 0 )) by Def5;

      then

       A5: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;