fib_num.miz



    begin

    reserve k,m,n,p for Element of NAT ;

    theorem :: FIB_NUM:1

    

     Th1: for m,n be Element of NAT holds (m gcd n) = (m gcd (n + m))

    proof

      let m, n;

      set a = (m gcd n);

      set b = (m gcd (n + m));

      

       A1: a divides m by NAT_D:def 5;

      

       A2: b divides m by NAT_D:def 5;

      b divides (n + m) by NAT_D:def 5;

      then b divides n by A2, NAT_D: 10;

      then

       A3: b divides a by A2, NAT_D:def 5;

      a divides n by NAT_D:def 5;

      then a divides (n + m) by A1, NAT_D: 8;

      then a divides b by A1, NAT_D:def 5;

      hence thesis by A3, NAT_D: 5;

    end;

    theorem :: FIB_NUM:2

    

     Th2: for k,m,n be Element of NAT st (k gcd m) = 1 holds (k gcd (m * n)) = (k gcd n)

    proof

      defpred P[ Nat] means for m, n holds ($1 gcd m) = 1 implies ($1 gcd (m * n)) = ($1 gcd n);

      

       A1: for k be Nat holds (for a be Nat st a < k holds P[a]) implies P[k]

      proof

        let k be Nat;

        assume

         A2: for a be Nat st a < k holds P[a];

        per cases by NAT_1: 25;

          suppose

           A3: k = 0 ;

          let m, n;

          assume (k gcd m) = 1;

          then 1 = m by A3, NEWTON: 52;

          hence thesis;

        end;

          suppose

           A4: k = 1;

          let m, n;

          assume (k gcd m) = 1;

          (k gcd (m * n)) = 1 by A4, NEWTON: 51;

          hence thesis by A4, NEWTON: 51;

        end;

          suppose

           A5: k > 1;

          let m, n;

          set b = (k gcd (m * n));

          assume

           A6: (k gcd m) = 1;

          thus thesis

          proof

            per cases by NAT_1: 25;

              suppose b = 0 ;

              then 0 divides k by NAT_D:def 5;

              then k = 0 by INT_2: 3;

              hence thesis by A5;

            end;

              suppose

               A7: b = 1;

              set c = (k gcd n);

              

               A8: c divides k by NAT_D:def 5;

              

               A9: n divides (m * n) by NAT_D:def 3;

              c divides n by NAT_D:def 5;

              then c divides (m * n) by A9, NAT_D: 4;

              then c divides 1 by A7, A8, NAT_D:def 5;

              hence thesis by A7, WSIERP_1: 15;

            end;

              suppose b > 1;

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

              then

              consider p such that

               A10: p is prime and

               A11: p divides b by INT_2: 31;

              b divides k by NAT_D:def 5;

              then

               A12: p divides k by A11, NAT_D: 4;

              then

              consider s be Nat such that

               A13: k = (p * s) by NAT_D:def 3;

              

               A14: not p divides m

              proof

                assume p divides m;

                then p divides 1 by A6, A12, NAT_D:def 5;

                then p = 1 by WSIERP_1: 15;

                hence thesis by A10, INT_2:def 4;

              end;

              b divides (m * n) by NAT_D:def 5;

              then p divides (m * n) by A11, NAT_D: 4;

              then p divides n by A10, A14, NEWTON: 80;

              then

              consider r be Nat such that

               A15: n = (p * r) by NAT_D:def 3;

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

              

               A16: (s + 1) > s by XREAL_1: 29;

              p > 1 by A10, INT_2:def 4;

              then p >= (1 + 1) by NAT_1: 13;

              then

               A17: (s * p) >= (s * (1 + 1)) by NAT_1: 4;

              s <> 0 by A5, A13;

              then (s + s) > s by XREAL_1: 29;

              then (s + s) >= (s + 1) by NAT_1: 13;

              then k >= (s + 1) by A13, A17, XXREAL_0: 2;

              then

               A18: s < k by A16, XXREAL_0: 2;

              

               A19: (s gcd m) = 1

              proof

                set c = (s gcd m);

                

                 A20: c divides s by NAT_D:def 5;

                

                 A21: c divides m by NAT_D:def 5;

                s divides k by A13, NAT_D:def 3;

                then c divides k by A20, NAT_D: 4;

                then c divides 1 by A6, A21, NAT_D:def 5;

                hence thesis by WSIERP_1: 15;

              end;

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

              

               A22: (k gcd n) = (p * (s gcd r)) by A13, A15, PYTHTRIP: 8;

              (k gcd (m * n)) = ((p * s) gcd (p * (m * r))) by A13, A15

              .= (p * (s gcd (m * r))) by PYTHTRIP: 8;

              hence thesis by A2, A18, A19, A22;

            end;

          end;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    theorem :: FIB_NUM:3

    

     Th3: for s be Real st s > 0 holds ex n be Element of NAT st n > 0 & 0 < (1 / n) & (1 / n) <= s

    proof

      let s be Real;

      consider n be Nat such that

       A1: n > (1 / s) by SEQ_4: 3;

      

       A2: (1 / (1 / s)) = (1 / (s " ))

      .= s;

      

       A3: n in NAT by ORDINAL1:def 12;

      assume s > 0 ;

      then

       A4: (1 / s) > 0 ;

      take n;

      thus thesis by A4, A1, A2, XREAL_1: 85, A3;

    end;

    scheme :: FIB_NUM:sch1

    FibInd { P[ set] } :

for k be Nat holds P[k]

      provided

       A1: P[ 0 ]

       and

       A2: P[1]

       and

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

      let k be Nat;

      defpred Q[ Nat] means P[$1] & P[($1 + 1)];

      

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

      proof

        let k be Nat;

        

         A5: (k + 2) = ((k + 1) + 1);

        assume Q[k];

        hence thesis by A3, A5;

      end;

      

       A6: Q[ 0 ] by A1, A2;

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

      hence thesis;

    end;

    scheme :: FIB_NUM:sch2

    BinInd { P[ Nat, Nat] } :

for m,n be Element of NAT holds P[m, n]

      provided

       A1: for m,n be Element of NAT st P[m, n] holds P[n, m]

       and

       A2: for k be Element of NAT st (for m,n be Element of NAT st (m < k & n < k) holds P[m, n]) holds for m be Element of NAT st m <= k holds P[k, m];

      defpred Q[ Nat] means for m, n st (m <= $1 & n <= $1) holds P[m, n];

      

       A3: for k be Nat st (for r be Nat st r < k holds Q[r]) holds Q[k]

      proof

        let k be Nat;

        assume

         A4: for r be Nat st r < k holds Q[r];

        let m, n;

        assume that

         A5: m <= k and

         A6: n <= k;

        set s = ( max (m,n));

        

         A0: s is Nat by TARSKI: 1;

        

         A7: s <= k by A5, A6, XXREAL_0: 28;

        per cases by A7, XXREAL_0: 1;

          suppose s < k;

          then m <= s & n <= s implies P[m, n] by A4, A0;

          hence thesis by XXREAL_0: 25;

        end;

          suppose

           A8: s = k;

          

           A9: for m, n holds m < k & n < k implies P[m, n]

          proof

            let m, n;

            assume that

             A10: m < k and

             A11: n < k;

            set s = ( max (m,n));

            

             A0: s is Nat by TARSKI: 1;

            

             A12: m <= s by XXREAL_0: 25;

            

             A13: n <= s by XXREAL_0: 25;

            s < k by A10, A11, XXREAL_0: 16;

            hence thesis by A4, A0, A12, A13;

          end;

          thus thesis

          proof

            per cases by A8, XXREAL_0: 16;

              suppose k = m;

              hence thesis by A2, A6, A9;

            end;

              suppose k = n;

              then P[n, m] by A2, A5, A9;

              hence thesis by A1;

            end;

          end;

        end;

      end;

      

       A14: for k be Nat holds Q[k] from NAT_1:sch 4( A3);

      let m, n;

      set k = ( max (m,n));

      k is Nat by TARSKI: 1;

      then m <= k & n <= k implies P[m, n] by A14;

      hence thesis by XXREAL_0: 30;

    end;

    (( 0 + 1) + 1) = 2;

    then

     Lm1: ( Fib 2) = 1 by PRE_FF: 1;

    

     Lm2: ((1 + 1) + 1) = 3;

    

     Lm3: for k be Nat holds ( Fib (k + 1)) >= k

    proof

      defpred P[ Nat] means ( Fib ($1 + 1)) >= $1;

      (( 0 + 1) + 1) = 2;

      then

       A1: P[1] by PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        per cases ;

          suppose k = 0 ;

          hence thesis by Lm1, Lm2, PRE_FF: 1;

        end;

          suppose k <> 0 ;

          then 1 <= k by NAT_1: 14;

          then

           A5: (1 + (k + 1)) <= (k + (k + 1)) by XREAL_1: 6;

          

           A6: ( Fib ((k + 2) + 1)) = (( Fib ((k + 1) + 1)) + ( Fib (k + 1))) by PRE_FF: 1;

          

           A7: (k + (k + 1)) <= (( Fib (k + 1)) + (k + 1)) by A3, XREAL_1: 6;

          (( Fib (k + 1)) + (k + 1)) <= (( Fib ((k + 1) + 1)) + ( Fib (k + 1))) by A4, XREAL_1: 6;

          then (k + (k + 1)) <= ( Fib ((k + 2) + 1)) by A6, A7, XXREAL_0: 2;

          hence thesis by A5, XXREAL_0: 2;

        end;

      end;

      

       A8: P[ 0 ];

      thus for k be Nat holds P[k] from FibInd( A8, A1, A2);

    end;

    

     Lm4: for m be Nat holds ( Fib (m + 1)) >= ( Fib m)

    proof

      defpred P[ Nat] means ( Fib ($1 + 1)) >= ( Fib $1);

      

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

      proof

        let k be Nat;

        ( Fib ((k + 1) + 1)) = (( Fib (k + 1)) + ( Fib k)) by PRE_FF: 1;

        then ( Fib ((k + 1) + 1)) >= (( Fib (k + 1)) + 0 ) by XREAL_1: 6;

        hence thesis;

      end;

      

       A2: P[ 0 ] by PRE_FF: 1;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A2, A1);

    end;

    

     Lm5: for m,n be Element of NAT st m >= n holds ( Fib m) >= ( Fib n)

    proof

      

       A1: for k,n be Element of NAT holds ( Fib (n + k)) >= ( Fib n)

      proof

        defpred P[ Nat] means for n be Element of NAT holds ( Fib (n + $1)) >= ( Fib n);

        

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

        proof

          let k be Nat;

          assume

           A3: P[k];

          let n;

          (n + (k + 1)) = ((n + k) + 1);

          then

           A4: ( Fib (n + (k + 1))) >= ( Fib (n + k)) by Lm4;

          ( Fib (n + k)) >= ( Fib n) by A3;

          hence thesis by A4, XXREAL_0: 2;

        end;

        let k,n be Element of NAT ;

        

         A5: P[ 0 ];

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

        hence thesis;

      end;

      let m,n be Element of NAT ;

      assume m >= n;

      then

      consider k be Nat such that

       A6: m = (n + k) by NAT_1: 10;

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

      m = (n + k) by A6;

      hence thesis by A1;

    end;

    

     Lm6: for m be Element of NAT holds ( Fib (m + 1)) <> 0

    proof

      let m;

      per cases ;

        suppose m = 0 ;

        hence thesis by PRE_FF: 1;

      end;

        suppose m <> 0 ;

        hence thesis by Lm3, NAT_1: 3;

      end;

    end;

    theorem :: FIB_NUM:4

    

     Th4: for m,n be Nat holds ( Fib (m + (n + 1))) = ((( Fib n) * ( Fib m)) + (( Fib (n + 1)) * ( Fib (m + 1))))

    proof

      defpred P[ Nat] means for n be Nat holds ( Fib ($1 + (n + 1))) = ((( Fib n) * ( Fib $1)) + (( Fib (n + 1)) * ( Fib ($1 + 1))));

      

       A1: P[ 0 ] by PRE_FF: 1;

       A2:

      now

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        thus P[(k + 2)]

        proof

          let n be Nat;

          

           A5: ( Fib (((k + 1) + 1) + (n + 1))) = ( Fib (((k + (n + 1)) + 1) + 1))

          .= (( Fib (k + (n + 1))) + ( Fib ((k + 1) + (n + 1)))) by PRE_FF: 1;

          set a = (( Fib n) * ( Fib k)), b = (( Fib (n + 1)) * ( Fib (k + 1))), c = (( Fib n) * ( Fib (k + 1))), d = (( Fib (n + 1)) * ( Fib ((k + 1) + 1)));

          

           A6: ((a + b) + (c + d)) = ((a + c) + (b + d));

          

           A7: (b + d) = (( Fib (n + 1)) * (( Fib (k + 1)) + ( Fib ((k + 1) + 1))))

          .= (( Fib (n + 1)) * ( Fib (((k + 1) + 1) + 1))) by PRE_FF: 1;

          

           A8: (a + c) = (( Fib n) * (( Fib k) + ( Fib (k + 1))))

          .= (( Fib n) * ( Fib ((k + 1) + 1))) by PRE_FF: 1;

          ( Fib (k + (n + 1))) = ((( Fib n) * ( Fib k)) + (( Fib (n + 1)) * ( Fib (k + 1)))) by A3;

          hence thesis by A4, A5, A6, A8, A7;

        end;

      end;

      

       A9: P[1] by Lm1, PRE_FF: 1;

      thus for k be Nat holds P[k] from FibInd( A1, A9, A2);

    end;

    

     Lm7: for n be Nat holds (( Fib n) gcd ( Fib (n + 1))) = 1

    proof

      defpred P[ Nat] means (( Fib $1) gcd ( Fib ($1 + 1))) = 1;

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        (( Fib (k + 1)) gcd ( Fib ((k + 1) + 1))) = (( Fib (k + 1)) gcd (( Fib (k + 1)) + ( Fib k))) by PRE_FF: 1

        .= 1 by A2, Th1;

        hence P[(k + 1)];

      end;

      

       A3: P[ 0 ] by NEWTON: 52, PRE_FF: 1;

      thus for m be Nat holds P[m] from NAT_1:sch 2( A3, A1);

    end;

    theorem :: FIB_NUM:5

    for m,n be Element of NAT holds (( Fib m) gcd ( Fib n)) = ( Fib (m gcd n))

    proof

      defpred P[ Element of NAT , Element of NAT ] means (( Fib $1) gcd ( Fib $2)) = ( Fib ($1 gcd $2));

      

       A1: for k st (for m, n st (m < k & n < k) holds P[m, n]) holds for m st m <= k holds P[k, m]

      proof

        let k;

        assume

         A2: for m, n st m < k & n < k holds P[m, n];

        let m;

        assume

         A3: m <= k;

        per cases by A3, XXREAL_0: 1;

          suppose

           A4: m = k;

          

          hence (( Fib k) gcd ( Fib m)) = ( Fib k) by NAT_D: 32

          .= ( Fib (k gcd m)) by A4, NAT_D: 32;

        end;

          suppose

           A5: m < k;

          thus thesis

          proof

            per cases ;

              suppose

               A6: m = 0 ;

              then (( Fib k) gcd ( Fib m)) = ( Fib k) by NEWTON: 52, PRE_FF: 1;

              hence thesis by A6, NEWTON: 52;

            end;

              suppose

               A7: m > 0 ;

              thus thesis

              proof

                consider r be Nat such that

                 A8: k = (m + r) by A3, NAT_1: 10;

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

                

                 A9: r <= k by A8, NAT_1: 11;

                r <> 0 by A5, A8;

                then

                consider rr be Nat such that

                 A10: r = (rr + 1) by NAT_1: 6;

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

                ( Fib k) = ((( Fib (rr + 1)) * ( Fib (m + 1))) + (( Fib rr) * ( Fib m))) by A8, A10, Th4;

                then

                 A11: (( Fib k) gcd ( Fib m)) = (( Fib m) gcd (( Fib (m + 1)) * ( Fib r))) by A10, EULER_1: 8;

                (( Fib m) gcd ( Fib (m + 1))) = 1 by Lm7;

                then

                 A12: (( Fib k) gcd ( Fib m)) = (( Fib m) gcd ( Fib r)) by A11, Th2;

                r <> k by A7, A8;

                then

                 A13: r < k by A9, XXREAL_0: 1;

                (k gcd m) = (m gcd r) by A8, Th1;

                hence thesis by A2, A5, A12, A13;

              end;

            end;

          end;

        end;

      end;

      

       A14: for m, n holds P[m, n] implies P[n, m];

      thus for m, n holds P[m, n] from BinInd( A14, A1);

    end;

    begin

    reserve x,a,b,c for Real;

    theorem :: FIB_NUM:6

    

     Th6: for x,a,b,c be Real st a <> 0 & ( delta (a,b,c)) >= 0 holds (((a * (x ^2 )) + (b * x)) + c) = 0 iff (x = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) or x = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)))

    proof

      let x, a, b, c;

      set lh = (((a * (x ^2 )) + (b * x)) + c);

      set r1 = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a));

      set r2 = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a));

      assume that

       A1: a <> 0 and

       A2: ( delta (a,b,c)) >= 0 ;

      lh = ((a * (x - r1)) * (x - r2)) by A1, A2, QUIN_1: 16;

      hence thesis by A1, A2, QUIN_1: 15;

    end;

    definition

      :: FIB_NUM:def1

      func tau -> Real equals ((1 + ( sqrt 5)) / 2);

      correctness ;

    end

    definition

      :: FIB_NUM:def2

      func tau_bar -> Real equals ((1 - ( sqrt 5)) / 2);

      correctness ;

    end

    

     Lm8: ( tau ^2 ) = ( tau + 1) & ( tau_bar ^2 ) = ( tau_bar + 1)

    proof

      

       A1: ( delta (1,( - 1),( - 1))) = ((( - 1) ^2 ) - ((4 * 1) * ( - 1))) by QUIN_1:def 1

      .= 5;

      then

       A2: ((( - ( - 1)) - ( sqrt ( delta (1,( - 1),( - 1))))) / (2 * 1)) = tau_bar ;

      

       A3: for x holds (x = tau or x = tau_bar ) implies (x ^2 ) = (x + 1)

      proof

        let x;

        assume x = tau or x = tau_bar ;

        then (((1 * (x ^2 )) + (( - 1) * x)) + ( - 1)) = 0 by A1, A2, Th6;

        hence thesis;

      end;

      hence ( tau ^2 ) = ( tau + 1);

      thus thesis by A3;

    end;

    

     Lm9: 2 < ( sqrt 5) by SQUARE_1: 20, SQUARE_1: 27;

    

     Lm10: ( sqrt 5) <> 0 by SQUARE_1: 20, SQUARE_1: 27;

    

     Lm11: ( sqrt 5) < 3

    proof

      (3 ^2 ) = 9;

      then ( sqrt 9) = 3 by SQUARE_1: 22;

      hence thesis by SQUARE_1: 27;

    end;

    1 < tau

    proof

      2 < ( sqrt 5) by SQUARE_1: 20, SQUARE_1: 27;

      then 1 < ( sqrt 5) by XXREAL_0: 2;

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

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

      hence thesis;

    end;

    then

     Lm12: 0 < tau ;

    

     Lm13: tau_bar < 0

    proof

      2 < ( sqrt 5) by SQUARE_1: 20, SQUARE_1: 27;

      then not ( 0 + ( sqrt 5)) <= 1 by XXREAL_0: 2;

      then ( 0 * 2) > ((1 - ( sqrt 5)) / 1) by XREAL_1: 19;

      then ((1 - ( sqrt 5)) / 2) < ( 0 * 1) by XREAL_1: 113;

      hence thesis;

    end;

    

     Lm14: |. tau_bar .| < 1

    proof

      (( sqrt 5) - 1) < (3 - 1) by Lm11, XREAL_1: 9;

      then

       A1: ((( sqrt 5) - 1) / 2) < (2 / 2) by XREAL_1: 74;

       |. tau_bar .| = ( - ((1 - ( sqrt 5)) / 2)) by Lm13, ABSVALUE:def 1

      .= ((( sqrt 5) - 1) / 2);

      hence thesis by A1;

    end;

    theorem :: FIB_NUM:7

    

     Th7: for n be Nat holds ( Fib n) = ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5))

    proof

      defpred P[ Nat] means ( Fib $1) = ((( tau to_power $1) - ( tau_bar to_power $1)) / ( sqrt 5));

      

       A1: ( tau_bar to_power 1) = tau_bar by POWER: 25;

      ( tau_bar to_power 0 ) = 1 by POWER: 24;

      

      then ((( tau to_power 0 ) - ( tau_bar to_power 0 )) / ( sqrt 5)) = ((1 - 1) / ( sqrt 5)) by POWER: 24

      .= 0 ;

      then

       A2: P[ 0 ] by PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume that

         A4: P[k] and

         A5: P[(k + 1)];

        set a = ( tau to_power k), a1 = ( tau_bar to_power k), b = ( tau to_power (k + 1)), b1 = ( tau_bar to_power (k + 1)), c = ( tau to_power (k + 2)), c1 = ( tau_bar to_power (k + 2));

        

         A6: c1 = ( tau_bar |^ (k + 2)) by POWER: 41

        .= (( tau_bar |^ k) * ( tau_bar |^ (1 + 1))) by NEWTON: 8

        .= (( tau_bar |^ k) * ( tau_bar * ( tau_bar |^ 1))) by NEWTON: 6

        .= (( tau_bar |^ k) * ( tau_bar + 1)) by Lm8

        .= ((( tau_bar |^ k) * tau_bar ) + (( tau_bar |^ k) * 1))

        .= (( tau_bar |^ (k + 1)) + (( tau_bar |^ k) * 1)) by NEWTON: 6

        .= (b1 + ( tau_bar |^ k)) by POWER: 41

        .= (a1 + b1) by POWER: 41;

        

         A7: c = (( tau to_power 2) * ( tau to_power k)) by Lm12, POWER: 27

        .= (( tau to_power k) * ( tau + 1)) by Lm8, POWER: 46

        .= ((( tau to_power k) * tau ) + (( tau to_power k) * 1))

        .= ((( tau to_power k) * ( tau to_power 1)) + a) by POWER: 25

        .= (a + b) by Lm12, POWER: 27;

        ( Fib (k + 2)) = ( Fib ((k + 1) + 1))

        .= (((a - a1) / ( sqrt 5)) + ((b - b1) / ( sqrt 5))) by A4, A5, PRE_FF: 1

        .= ((c - c1) / ( sqrt 5)) by A7, A6;

        hence thesis;

      end;

      ( tau - tau_bar ) = ( sqrt 5);

      

      then ((( tau to_power 1) - ( tau_bar to_power 1)) / ( sqrt 5)) = (( sqrt 5) / ( sqrt 5)) by A1, POWER: 25

      .= ( Fib 1) by Lm10, PRE_FF: 1, XCMPLX_1: 60;

      then

       A8: P[1];

      thus for n be Nat holds P[n] from FibInd( A2, A8, A3);

    end;

    

     Lm15: for x be Real st |.x.| <= 1 holds |.(x |^ n).| <= 1

    proof

      let x;

      defpred P[ Nat] means |.(x |^ $1).| <= 1;

      assume

       A1: |.x.| <= 1;

      

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

      proof

        let k be Nat;

        

         A3: |.(x |^ (k + 1)).| = |.((x |^ k) * x).| by NEWTON: 6

        .= ( |.(x |^ k).| * |.x.|) by COMPLEX1: 65;

        assume P[k];

        hence thesis by A1, A3, COMPLEX1: 46, XREAL_1: 160;

      end;

       |.(x |^ 0 ).| = |.1.| by NEWTON: 4

      .= 1 by ABSVALUE:def 1;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    

     Lm16: for n holds |.(( tau_bar to_power n) / ( sqrt 5)).| < 1

    proof

      let n;

      set y = ( tau_bar to_power n), z = ( sqrt 5);

      

       A1: |.y.| = |.( tau_bar |^ n).| by POWER: 41;

      

       A2: |.(y / z).| = |.(y * (z " )).|

      .= ( |.y.| * |.(z " ).|) by COMPLEX1: 65;

      

       A3: (1 / z) < (1 / 2) by Lm9, XREAL_1: 88;

      z > 0 by Lm9;

      then

       A4: (z " ) > 0 ;

      then |.(z " ).| = (z " ) by ABSVALUE:def 1;

      then

       A5: |.(z " ).| < 1 by A3, XXREAL_0: 2;

       |.(z " ).| >= 0 by A4, ABSVALUE:def 1;

      hence thesis by A1, A2, A5, Lm14, Lm15, XREAL_1: 162;

    end;

    theorem :: FIB_NUM:8

    for n be Element of NAT holds |.(( Fib n) - (( tau to_power n) / ( sqrt 5))).| < 1

    proof

      let n;

      set k = ( Fib n), x = ( tau to_power n), y = ( tau_bar to_power n), z = ( sqrt 5);

      k = ((x - y) / z) by Th7

      .= ((x / z) - (y / z));

      then |.( - (k - (x / z))).| < 1 by Lm16;

      hence thesis by COMPLEX1: 52;

    end;

    reserve F,f,g,h for Real_Sequence;

    theorem :: FIB_NUM:9

    

     Th9: for f,g,h be Real_Sequence st g is non-zero holds ((f /" g) (#) (g /" h)) = (f /" h)

    proof

      let f,g,h be Real_Sequence;

      set f3 = (f /" g), g3 = (g /" h), h3 = (f /" h);

      assume

       A1: g is non-zero;

      for n holds ((f3 (#) g3) . n) = (h3 . n)

      proof

        let n;

        set a = (f . n), b = ((g . n) " ), c = (g . n), d = ((h . n) " );

        

         A2: (g3 . n) = (c * ((h " ) . n)) by SEQ_1: 8

        .= (c * d) by VALUED_1: 10;

        

         A3: (h3 . n) = (a * ((h " ) . n)) by SEQ_1: 8

        .= (a * d) by VALUED_1: 10;

        

         A4: (g . n) <> 0 by A1, SEQ_1: 5;

        

         A5: (b * c) = ((1 / c) * c)

        .= 1 by A4, XCMPLX_1: 106;

        (f3 . n) = (a * ((g " ) . n)) by SEQ_1: 8

        .= (a * b) by VALUED_1: 10;

        

        then ((f3 (#) g3) . n) = ((a * b) * (c * d)) by A2, SEQ_1: 8

        .= (((b * c) * a) * d)

        .= (h3 . n) by A3, A5;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FIB_NUM:10

    

     Th10: for f,g be Real_Sequence holds for n be Element of NAT holds ((f /" g) . n) = ((f . n) / (g . n)) & ((f /" g) . n) = ((f . n) * ((g . n) " ))

    proof

      let f, g;

      let n;

      

       A1: ((f /" g) . n) = ((f . n) * ((g " ) . n)) by SEQ_1: 8

      .= ((f . n) * ((g . n) " )) by VALUED_1: 10;

      hence ((f /" g) . n) = ((f . n) / (g . n));

      thus thesis by A1;

    end;

    theorem :: FIB_NUM:11

    for F be Real_Sequence st (for n be Element of NAT holds (F . n) = (( Fib (n + 1)) / ( Fib n))) holds F is convergent & ( lim F) = tau

    proof

      deffunc ff( Nat) = (( tau to_power $1) / ( sqrt 5));

      let F;

      consider f such that

       A1: for n be Nat holds (f . n) = ( Fib n) from SEQ_1:sch 1;

      set f2 = (f ^\ 2);

      set f1 = (f ^\ 1);

      

       A2: (f1 ^\ 1) = (f ^\ (1 + 1)) by NAT_1: 48

      .= f2;

      

       A3: for n holds (f2 . n) <> 0

      proof

        let n;

        (f2 . n) = (f . (n + 2)) by NAT_1:def 3

        .= ( Fib ((n + 1) + 1)) by A1;

        hence thesis by Lm3;

      end;

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

      

       A4: for n be Nat holds ((f2 /" f2) . n) = jj

      proof

        let n be Nat;

        

         A5: n in NAT by ORDINAL1:def 12;

        

        then ((f2 /" f2) . n) = ((f2 . n) * ((f2 . n) " )) by Th10

        .= ((f2 . n) * (1 / (f2 . n)))

        .= 1 by A3, A5, XCMPLX_1: 106;

        hence thesis;

      end;

      then

       A6: (f2 /" f2) is constant by VALUED_0:def 18;

      

       A7: ((f /" f) ^\ 2) = (f2 /" f2) by SEQM_3: 20;

      then

       A8: (f /" f) is convergent by A6, SEQ_4: 21;

      ((f2 /" f2) . 0 ) = 1 by A4;

      then ( lim (f2 /" f2)) = 1 by A6, SEQ_4: 25;

      then

       A9: ( lim (f /" f)) = 1 by A6, A7, SEQ_4: 22;

      ex g st for n be Nat holds (g . n) = ff(n) from SEQ_1:sch 1;

      then

      consider g such that

       A10: for n be Nat holds (g . n) = ff(n);

      set g1 = (g ^\ 1);

      

       A11: for n be Nat holds (g . n) <> 0

      proof

        let n be Nat;

        

         A12: (( sqrt 5) " ) <> 0 by SQUARE_1: 20, SQUARE_1: 27, XCMPLX_1: 202;

        

         A13: ( tau |^ n) <> 0 by Lm12, PREPOWER: 5;

        (g . n) = (( tau to_power n) / ( sqrt 5)) by A10

        .= (( tau to_power n) * (( sqrt 5) " ))

        .= (( tau |^ n) * (( sqrt 5) " )) by POWER: 41;

        hence thesis by A13, A12, XCMPLX_1: 6;

      end;

      then

       A14: g is non-zero by SEQ_1: 5;

      

       A15: (f2 /" f1) = ((f2 /" g1) (#) (g1 /" f1)) by Th9, A14;

      set g2 = (g1 ^\ 1);

      for n be Nat holds (f1 . n) <> 0

      proof

        let n be Nat;

        

         A16: n in NAT by ORDINAL1:def 12;

        (f1 . n) = (f . (n + 1)) by NAT_1:def 3

        .= ( Fib (n + 1)) by A1;

        hence thesis by Lm6, A16;

      end;

      then

       A17: f1 is non-zero by SEQ_1: 5;

      for n be Nat holds ((g2 /" f2) . n) <> 0

      proof

        let n be Nat;

        

         A18: n in NAT by ORDINAL1:def 12;

        

         A19: (g2 . n) <> 0 by A14, SEQ_1: 5;

        

         A20: ((g2 /" f2) . n) = ((g2 . n) * ((f2 . n) " )) by Th10, A18;

        ((f2 . n) " ) <> 0 by A17, A2, SEQ_1: 5, XCMPLX_1: 202;

        hence thesis by A19, A20, XCMPLX_1: 6;

      end;

      then

       A21: (g2 /" f2) is non-zero by SEQ_1: 5;

      g2 = (g ^\ (1 + 1)) by NAT_1: 48;

      then

       A22: (g2 /" f2) = ((g /" f) ^\ 2) by SEQM_3: 20;

      

       A23: for n holds (f1 . n) = ( Fib (n + 1))

      proof

        let n;

        (f1 . n) = (f . (n + 1)) by NAT_1:def 3

        .= ( Fib (n + 1)) by A1;

        hence thesis;

      end;

      assume

       A24: for n be Element of NAT holds (F . n) = (( Fib (n + 1)) / ( Fib n));

      for n holds (F . n) = ((f1 /" f) . n)

      proof

        let n;

        ((f1 /" f) . n) = ((f1 . n) / (f . n)) by Th10

        .= (( Fib (n + 1)) / (f . n)) by A23

        .= (( Fib (n + 1)) / ( Fib n)) by A1;

        hence thesis by A24;

      end;

      then F = (f1 /" f) by FUNCT_2: 63;

      then

       A25: (f2 /" f1) = (F ^\ 1) by A2, SEQM_3: 20;

      

       A26: (g2 /" g1) = ((g1 /" g) ^\ 1) by SEQM_3: 20;

      

       A27: for n be Nat holds ((g1 /" g) . n) = tau

      proof

        let n be Nat;

        

         A28: n in NAT by ORDINAL1:def 12;

        

         A29: (g . n) = (( tau to_power n) / ( sqrt 5)) by A10

        .= (( tau to_power n) * (( sqrt 5) " ))

        .= (( tau |^ n) * (( sqrt 5) " )) by POWER: 41;

        

         A30: (g . n) <> 0 by A11;

        (g1 . n) = (g . (n + 1)) by NAT_1:def 3

        .= (( tau to_power (n + 1)) / ( sqrt 5)) by A10

        .= (( tau to_power (n + 1)) * (( sqrt 5) " ))

        .= (( tau |^ (n + 1)) * (( sqrt 5) " )) by POWER: 41

        .= (( tau * ( tau |^ n)) * (( sqrt 5) " )) by NEWTON: 6

        .= ( tau * (g . n)) by A29;

        

        then ((g1 /" g) . n) = (( tau * (g . n)) * ((g . n) " )) by A28, Th10

        .= ( tau * ((g . n) * ((g . n) " )))

        .= ( tau * 1) by A30, XCMPLX_0:def 7

        .= tau ;

        hence thesis;

      end;

       tau in REAL by XREAL_0:def 1;

      then

       A31: (g1 /" g) is constant by A27, VALUED_0:def 18;

      

       A32: for x st 0 < x holds ex n be Nat st for m be Nat st n <= m holds |.(((f " ) . m) - 0 ).| < x

      proof

        let x;

        assume 0 < x;

        then

        consider k such that

         A33: k > 0 and 0 < (1 / k) and

         A34: (1 / k) <= x by Th3;

        for m be Nat st (k + 2) <= m holds |.(((f " ) . m) - 0 ).| < x

        proof

          let m be Nat;

          

           A35: m in NAT by ORDINAL1:def 12;

          (k + 2) = ((k + 1) + 1);

          then

           A36: ( Fib (k + 2)) >= (k + 1) by Lm3;

          assume (k + 2) <= m;

          then ( Fib (k + 2)) <= ( Fib m) by Lm5, A35;

          then (k + 1) <= ( Fib m) by A36, XXREAL_0: 2;

          then

           A37: (k + 1) <= (f . m) by A1;

          then 0 < (f . m);

          then

           A38: 0 <= ((f . m) " );

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

          then

           A39: (1 / (k + 1)) < (1 / k) by A33, XREAL_1: 88;

          

           A40: |.(((f " ) . m) - 0 ).| = |.((f . m) " ).| by VALUED_1: 10

          .= ((f . m) " ) by A38, ABSVALUE:def 1

          .= (1 / (f . m));

          (1 / (f . m)) <= (1 / (k + 1)) by A37, XREAL_1: 85;

          then (1 / (f . m)) < (1 / k) by A39, XXREAL_0: 2;

          hence thesis by A34, A40, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      then

       A41: (f " ) is convergent by SEQ_2:def 6;

      then

       A42: ( lim (f " )) = 0 by A32, SEQ_2:def 7;

      deffunc ff( Nat) = (( tau_bar to_power $1) / ( sqrt 5));

      ex h st for n be Nat holds (h . n) = ff(n) from SEQ_1:sch 1;

      then

      consider h such that

       A43: for n be Nat holds (h . n) = ff(n);

      

       A44: for n holds (f . n) = ((g . n) - (h . n))

      proof

        let n;

        (f . n) = ( Fib n) by A1

        .= ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5)) by Th7

        .= ((( tau to_power n) / ( sqrt 5)) - (( tau_bar to_power n) / ( sqrt 5)))

        .= ((g . n) - (( tau_bar to_power n) / ( sqrt 5))) by A10

        .= ((g . n) - (h . n)) by A43;

        hence thesis;

      end;

      for n be Nat holds (g . n) = ((f . n) + (h . n))

      proof

        let n be Nat;

        

         A45: n in NAT by ORDINAL1:def 12;

        (f . n) = ((g . n) - (h . n)) by A44, A45;

        hence thesis;

      end;

      then g = (f + h) by SEQ_1: 7;

      then

       A46: (g /" f) = ((f /" f) + (h /" f)) by SEQ_1: 49;

      for n be Nat holds |.(h . n).| < 1

      proof

        let n be Nat;

        

         A47: n in NAT by ORDINAL1:def 12;

        (h . n) = (( tau_bar to_power n) / ( sqrt 5)) by A43;

        hence thesis by Lm16, A47;

      end;

      then

       A48: h is bounded by SEQ_2: 3;

      (f " ) is convergent by A32, SEQ_2:def 6;

      then

       A49: (h /" f) is convergent by A48, A42, SEQ_2: 25;

      then

       A50: (g /" f) is convergent by A8, A46;

      ((g1 /" g) . 0 ) = tau by A27;

      then ( lim (g1 /" g)) = tau by A31, SEQ_4: 25;

      then

       A51: ( lim (g2 /" g1)) = tau by A31, A26, SEQ_4: 20;

      

       A52: (g1 /" f1) = ((g /" f) ^\ 1) by SEQM_3: 20;

      ( lim (h /" f)) = 0 by A48, A41, A42, SEQ_2: 26;

      

      then

       A53: ( lim (g /" f)) = (1 + 0 ) by A49, A8, A9, A46, SEQ_2: 6

      .= 1;

      then

       A54: ( lim (g2 /" f2)) = 1 by A50, A22, SEQ_4: 20;

      then ((g2 /" f2) " ) is convergent by A50, A22, A21, SEQ_2: 21;

      then

       A55: (f2 /" g2) is convergent by SEQ_1: 40;

      

       A56: (f2 /" g1) = ((f2 /" g2) (#) (g2 /" g1)) by A14, Th9;

      then

       A57: (f2 /" g1) is convergent by A31, A55, A26;

      then

       A58: (f2 /" f1) is convergent by A50, A52, A15;

      hence F is convergent by A25, SEQ_4: 21;

      ( lim ((g2 /" f2) " )) = (1 " ) by A50, A22, A54, A21, SEQ_2: 22

      .= 1;

      then ( lim (f2 /" g2)) = 1 by SEQ_1: 40;

      

      then

       A59: ( lim (f2 /" g1)) = (1 * tau ) by A31, A56, A55, A26, A51, SEQ_2: 15

      .= tau ;

      ( lim (g1 /" f1)) = 1 by A50, A53, A52, SEQ_4: 20;

      then ( lim (f2 /" f1)) = ( tau * 1) by A50, A59, A57, A52, A15, SEQ_2: 15;

      hence thesis by A58, A25, SEQ_4: 22;

    end;