fib_num4.miz

    begin



     Lm1: for m,n be Nat holds ( - m) <= (m * (( - 1) to_power n))

    proof

      let m,n be Nat;

      n is even or n is odd;

      then (( - 1) to_power n) = 1 or (( - 1) to_power n) = ( - 1) by FIB_NUM2: 2, FIB_NUM2: 3;

      hence thesis;

    end;



     Lm2: for m,n be Nat holds ( - (m * (( - 1) to_power n))) >= ( - m)

    proof

      let m,n be Nat;

      n is even or n is odd;

      then (( - 1) to_power n) = 1 or (( - 1) to_power n) = ( - 1) by FIB_NUM2: 2, FIB_NUM2: 3;

      hence thesis;

    end;

    theorem :: FIB_NUM4:1



     Th1: for a,b be Real, c be Nat holds ((a / b) to_power c) = ((a to_power c) / (b to_power c))

    proof

      let a,b be Real;

      let c be Nat;

      ((a / b) to_power c) = ((a * (1 / b)) |^ c) by XCMPLX_1: 99

      .= ((a to_power c) * ((1 / b) |^ c)) by NEWTON: 7

      .= ((a to_power c) * (1 / (b |^ c))) by PREPOWER: 7

      .= ((a to_power c) / (b |^ c)) by XCMPLX_1: 99;

      hence thesis;

    end;

    theorem :: FIB_NUM4:2



     Th2: for a be Real, b,c be Integer st a <> 0 holds (a to_power (b + c)) = ((a to_power b) * (a to_power c))

    proof

      let a be Real;

      let b,c be Integer;

      assume

       A1: a <> 0 ;



      thus ((a to_power b) * (a to_power c)) = ((a #Z b) * (a to_power c)) by POWER: 43

      .= ((a #Z b) * (a #Z c)) by POWER: 43

      .= (a #Z (b + c)) by A1, PREPOWER: 44

      .= (a to_power (b + c)) by POWER: 43;

    end;

    theorem :: FIB_NUM4:3



     Th3: for n be Nat, a be Real st n is even & a <> 0 holds (( - a) to_power n) = (a to_power n) by POWER: 47;

    theorem :: FIB_NUM4:4



     Th4: for n be Nat, a be Real st n is odd & a <> 0 holds (( - a) to_power n) = ( - (a to_power n)) by POWER: 48;



     Lm3: ( tau * tau_bar ) = ( - 1)

    proof

      ( tau * tau_bar ) = (((1 ^2 ) - (( sqrt 5) ^2 )) / 4) by FIB_NUM:def 1, FIB_NUM:def 2

      .= ((1 - 5) / 4) by SQUARE_1:def 2;

      hence thesis;

    end;



     Lm4: ( tau_bar / tau ) = ((( sqrt 5) - 3) / 2)

    proof

      ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1: 27;

      then ( - ( sqrt 5)) < ( - 1) by XREAL_1: 24;

      then

       A1: (( - ( sqrt 5)) + 1) < (( - 1) + 1) by XREAL_1: 6;

      ( tau_bar / tau ) = (((1 - ( sqrt 5)) * 2) / ((1 + ( sqrt 5)) * 2)) by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1: 84

      .= ((1 - ( sqrt 5)) / (1 + ( sqrt 5))) by XCMPLX_1: 91

      .= (((1 - ( sqrt 5)) * (1 - ( sqrt 5))) / ((1 + ( sqrt 5)) * (1 - ( sqrt 5)))) by A1, XCMPLX_1: 91

      .= (((1 - (2 * ( sqrt 5))) + (( sqrt 5) ^2 )) / ((1 ^2 ) - (( sqrt 5) ^2 )))

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

      .= ((6 - (2 * ( sqrt 5))) / ((1 ^2 ) - 5)) by SQUARE_1:def 2

      .= ((2 * (3 - ( sqrt 5))) / (( - 2) * 2));

      hence thesis;

    end;



     Lm5: ( tau / tau_bar ) = ((( - 3) - ( sqrt 5)) / 2)

    proof



       A1: ( sqrt 5) > 0 by SQUARE_1: 25;

      ( tau / tau_bar ) = (((1 + ( sqrt 5)) * 2) / ((1 - ( sqrt 5)) * 2)) by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1: 84

      .= ((1 + ( sqrt 5)) / (1 - ( sqrt 5))) by XCMPLX_1: 91

      .= (((1 + ( sqrt 5)) * (1 + ( sqrt 5))) / ((1 - ( sqrt 5)) * (1 + ( sqrt 5)))) by A1, XCMPLX_1: 91

      .= (((1 + ( sqrt 5)) * (1 + ( sqrt 5))) / (1 - (( sqrt 5) ^2 )))

      .= (((1 + ( sqrt 5)) * (1 + ( sqrt 5))) / (1 - 5)) by SQUARE_1:def 2

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

      .= (((1 + (2 * ( sqrt 5))) + 5) / ( - 4)) by SQUARE_1:def 2;

      hence thesis;

    end;



     Lm6: ( tau to_power 2) = ((3 + ( sqrt 5)) / 2)

    proof

      ( tau to_power 2) = (((1 + ( sqrt 5)) / 2) ^2 ) by FIB_NUM:def 1, POWER: 46

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

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

      .= ((2 * (3 + ( sqrt 5))) / (2 * 2));

      hence thesis;

    end;



     Lm7: ( tau_bar to_power 2) = ((3 - ( sqrt 5)) / 2)

    proof

      ( tau_bar to_power 2) = (((1 - ( sqrt 5)) / 2) ^2 ) by FIB_NUM:def 2, POWER: 46

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

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

      .= ((2 * (3 - ( sqrt 5))) / (2 * 2));

      hence thesis;

    end;



     Lm8: ( tau_bar to_power 3) = (2 - ( sqrt 5))

    proof

      1 < ( sqrt 5) by SQUARE_1: 18, SQUARE_1: 27;

      then

       A1: (1 - ( sqrt 5)) < (( sqrt 5) - ( sqrt 5)) by XREAL_1: 9;



      thus ( tau_bar to_power 3) = (((1 - ( sqrt 5)) / 2) to_power (2 + 1)) by FIB_NUM:def 2

      .= ((((1 - ( sqrt 5)) / 2) to_power 2) * (((1 - ( sqrt 5)) / 2) to_power 1)) by Th2, A1

      .= ((((1 - ( sqrt 5)) / 2) to_power 2) * ((1 - ( sqrt 5)) / 2))

      .= ((((1 - ( sqrt 5)) / 2) ^2 ) * ((1 - ( sqrt 5)) / 2)) by POWER: 46

      .= ((((1 - ((2 * 1) * ( sqrt 5))) + (( sqrt 5) ^2 )) * (1 - ( sqrt 5))) / 8)

      .= ((((1 - (2 * ( sqrt 5))) + 5) * (1 - ( sqrt 5))) / 8) by SQUARE_1:def 2

      .= (((6 - (8 * ( sqrt 5))) + (2 * (( sqrt 5) ^2 ))) / 8)

      .= (((6 - (8 * ( sqrt 5))) + (2 * 5)) / 8) by SQUARE_1:def 2

      .= (2 - ( sqrt 5));

    end;



     Lm9: ( tau_bar to_power 6) = (9 - (4 * ( sqrt 5)))

    proof



      thus ( tau_bar to_power 6) = ( tau_bar to_power (3 * 2))

      .= ((2 - ( sqrt 5)) to_power 2) by Lm8, NEWTON: 9

      .= ((2 - ( sqrt 5)) ^2 ) by POWER: 46

      .= (((2 ^2 ) - ((2 * 2) * ( sqrt 5))) + (( sqrt 5) ^2 ))

      .= ((4 - (4 * ( sqrt 5))) + 5) by SQUARE_1:def 2

      .= (9 - (4 * ( sqrt 5)));

    end;

    theorem :: FIB_NUM4:5



     Th5: |. tau_bar .| < 1

    proof

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

      then ( sqrt 5) < 3 by SQUARE_1:def 2;

      then (( sqrt 5) - 1) < ((2 + 1) - 1) by XREAL_1: 9;

      then ( - (( sqrt 5) - 1)) > ( - 2) by XREAL_1: 24;

      then ((1 - ( sqrt 5)) / 2) > (( - 2) / 2) by XREAL_1: 74;

      then

       A1: |. tau_bar .| < ( |.( - 1).| + |. 0 .|) by FIB_NUM:def 2, MEASURE6: 37;

       |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1;

      then |. tau_bar .| < (1 + 0 ) by A1;

      hence thesis;

    end;



     Lm10: for n be Nat holds (( |. tau_bar .| to_power n) * (1 / ( sqrt 5))) > 0

    proof

      let n be Nat;

      set b = tau_bar ;

      ( sqrt 5) > 0 by SQUARE_1: 25;

      then ( |.b.| to_power n) > 0 & (1 / ( sqrt 5)) > 0 by POWER: 34;

      hence thesis;

    end;



     Lm11: for n be Nat holds (( |. tau_bar .| to_power n) * (1 / ( sqrt 5))) < (1 / 2)

    proof

      let n be Nat;



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

      then

       A2: (2 / 2) < (( sqrt 5) / 2) by XREAL_1: 74;

      set b = tau_bar ;



       A3: ( sqrt 5) <> 0 by SQUARE_1: 17, SQUARE_1: 27;



       A4: ( sqrt 5) > 0 by SQUARE_1: 25;

      per cases ;

        suppose

         A5: n <> 0 ;

         |.b.| < 1 & |.b.| > 0 by Th5;

        then ( |.b.| to_power n) < (1 to_power n) by A5, POWER: 37;

        then ( |.b.| to_power n) < 1;

        then ( |.b.| to_power n) < (( sqrt 5) / 2) by A2, XXREAL_0: 2;

        then (( |.b.| to_power n) / (( sqrt 5) / 1)) < ((( sqrt 5) / 2) / (( sqrt 5) / 1)) by A4, XREAL_1: 74;

        then (( |.b.| to_power n) / ( sqrt 5)) < ((1 * ( sqrt 5)) / (2 * ( sqrt 5))) by XCMPLX_1: 84;

        then (( |.b.| to_power n) * (1 / ( sqrt 5))) < ((1 * ( sqrt 5)) / (2 * ( sqrt 5))) by XCMPLX_1: 99;

        hence thesis by A3, XCMPLX_1: 91;

      end;

        suppose n = 0 ;

        then ( |. tau_bar .| to_power n) = 1 by POWER: 24;

        hence thesis by A1, XREAL_1: 76;

      end;

    end;

    theorem :: FIB_NUM4:6



     Th6: for n be Nat, r be non zero Real st n is even holds (r to_power n) > 0

    proof

      let n be Nat;

      let r be non zero Real;

      assume

       A1: n is even;

      per cases ;

        suppose r > 0 ;

        hence thesis by POWER: 34;

      end;

        suppose

         A2: r < 0 ;

        (r to_power n) = (( - r) to_power n) by Th3, A1;

        hence thesis by A2, POWER: 34;

      end;

    end;

    theorem :: FIB_NUM4:7



     Th7: for n be Nat, r be Real st n is odd & r < 0 holds (r to_power n) < 0

    proof

      let n be Nat;

      let r be Real;

      assume

       A1: n is odd;

      assume

       A2: r < 0 ;



       A3: (r to_power n) = (( - ( - r)) to_power n)

      .= ( - (( - r) to_power n)) by Th4, A1, A2;

      (( - r) to_power n) > 0 by A2, POWER: 34;

      hence thesis by A3;

    end;

    theorem :: FIB_NUM4:8



     Th8: for n be Nat st n <> 0 holds ( tau_bar to_power n) < (1 / 2)

    proof

      let n be Nat;

      assume n <> 0 ;

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

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

      then

       A1: (n + 1) = 2 or n >= 2 by NAT_1: 8;

      per cases by A1;

        suppose n = 1;

        hence thesis;

      end;

        suppose n >= 2;

        then n <> 0 & n <> 1;

        then

         A2: n is non trivial Nat by NAT_2:def 1;

        ( tau_bar to_power n) < (1 / 2)

        proof

          defpred P[ Nat] means ( |. tau_bar .| to_power $1) < (1 / 2);



           A3: ( |. tau_bar .| to_power 2) = (( - tau_bar ) to_power 2) by ABSVALUE:def 1

          .= (( - tau_bar ) ^2 ) by POWER: 46

          .= ((((1 ^2 ) - ((2 * 1) * ( sqrt 5))) + (( sqrt 5) ^2 )) / 4) by FIB_NUM:def 2

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

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

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

          then ( - ( sqrt 5)) < ( - 2) by XREAL_1: 24;

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

          then

           A4: P[2] by A3, XREAL_1: 74;



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

          proof

            let k be non trivial Nat;

            assume P[k];

            then (( |. tau_bar .| to_power k) * |. tau_bar .|) < ((1 / 2) * |. tau_bar .|) by XREAL_1: 68;

            then

             A6: (( |. tau_bar .| to_power k) * ( |. tau_bar .| to_power 1)) < ((1 / 2) * |. tau_bar .|);

            ((1 / 2) * |. tau_bar .|) < ((1 / 2) * 1) by Th5, XREAL_1: 68;

            then (( |. tau_bar .| to_power k) * ( |. tau_bar .| to_power 1)) < (1 / 2) by A6, XXREAL_0: 2;

            hence thesis by Th2;

          end;



           A7: for n be non trivial Nat holds P[n] from NAT_2:sch 2( A4, A5);

          for n be non trivial Nat holds ( tau_bar to_power n) < (1 / 2)

          proof

            let n be non trivial Nat;

            ( |. tau_bar .| to_power n) < (1 / 2) by A7;

            then |.( tau_bar to_power n).| < (1 / 2) & ( tau_bar to_power n) <= |.( tau_bar to_power n).| by ABSVALUE: 4, SERIES_1: 2;

            hence thesis by XXREAL_0: 2;

          end;

          hence thesis by A2;

        end;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM4:9

    for n,m be Nat, r be Real st m is odd & n >= m & r < 0 & r > ( - 1) holds (r to_power n) >= (r to_power m)

    proof

      let n,m be Nat;

      let r be Real;

      assume

       A1: m is odd;

      assume

       A2: n >= m;

      assume

       A3: r < 0 & r > ( - 1);



       A4: (n + 1) > (m + 0 ) by A2, XREAL_1: 8;

      per cases by A4, NAT_1: 22;

        suppose n = m;

        hence thesis;

      end;

        suppose

         A5: n > m;

        then

        reconsider t = (n - m) as Nat by NAT_1: 21;



         A6: ((r to_power n) - (r to_power m)) = ((r to_power (t + m)) - (r to_power m))

        .= (((r to_power t) * (r to_power m)) - (1 * (r to_power m))) by Th2, A3

        .= (((r to_power t) - 1) * (r to_power m));



         A7: (r to_power m) <= 0 by Th7, A3, A1;



         A8: t <> 0 by A5;



         A9: |.r.| <= 1 by A3, ABSVALUE: 5;

         |.r.| <> 1

        proof

          assume |.r.| = 1;

          then |.r.| = |.1.|;

          hence thesis by A3, ABSVALUE: 28;

        end;

        then

         A10: |.r.| < 1 by A9, XXREAL_0: 1;

         |.r.| > 0 & t > 0 by A8, A3;

        then ( |.r.| to_power t) < (1 to_power t) by A10, POWER: 37;

        then ( |.r.| to_power t) < 1;

        then |.(r to_power t).| < 1 & (r to_power t) <= |.(r to_power t).| by ABSVALUE: 4, SERIES_1: 2;

        then (r to_power t) < 1 by XXREAL_0: 2;

        then ((r to_power t) - 1) <= (1 - 1) by XREAL_1: 9;

        then (((r to_power n) - (r to_power m)) + (r to_power m)) >= ( 0 + (r to_power m)) by A6, A7, XREAL_1: 6;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM4:10



     Th10: for n,m be Nat st m is odd & n >= m holds ( tau_bar to_power n) >= ( tau_bar to_power m)

    proof

      let n,m be Nat;

      assume

       A1: m is odd;

      assume n >= m;

      then

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

      per cases by A2, NAT_1: 22;

        suppose n = m;

        hence thesis;

      end;

        suppose

         A3: n > m;

        then

        reconsider t = (n - m) as Nat by NAT_1: 21;



         A4: (( tau_bar to_power n) - ( tau_bar to_power m)) = (( tau_bar to_power (t + m)) - ( tau_bar to_power m))

        .= ((( tau_bar to_power t) * ( tau_bar to_power m)) - (1 * ( tau_bar to_power m))) by Th2

        .= ((( tau_bar to_power t) - 1) * ( tau_bar to_power m));



         A5: ( tau_bar to_power m) <= 0 by Th7, A1;

        t <> 0 by A3;

        then |. tau_bar .| > 0 & t > 0 ;

        then ( |. tau_bar .| to_power t) < (1 to_power t) by Th5, POWER: 37;

        then ( |. tau_bar .| to_power t) < 1;

        then |.( tau_bar to_power t).| < 1 & ( tau_bar to_power t) <= |.( tau_bar to_power t).| by ABSVALUE: 4, SERIES_1: 2;

        then ( tau_bar to_power t) < 1 by XXREAL_0: 2;

        then (( tau_bar to_power t) - 1) <= (1 - 1) by XREAL_1: 9;

        then ((( tau_bar to_power n) - ( tau_bar to_power m)) + ( tau_bar to_power m)) >= ( 0 + ( tau_bar to_power m)) by A4, A5, XREAL_1: 6;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM4:11



     Th11: for n,m be Nat st n is even & m is even & n >= m holds ( tau_bar to_power n) <= ( tau_bar to_power m)

    proof

      let n,m be Nat;

      assume

       A1: n is even & m is even & n >= m;

      then

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

      per cases by A2, NAT_1: 22;

        suppose n = m;

        hence thesis;

      end;

        suppose

         A3: n > m;

        then

        reconsider t = (n - m) as Nat by NAT_1: 21;



         A4: (( tau_bar to_power n) - ( tau_bar to_power m)) = (( tau_bar to_power (t + m)) - ( tau_bar to_power m))

        .= ((( tau_bar to_power t) * ( tau_bar to_power m)) - (1 * ( tau_bar to_power m))) by Th2

        .= ((( tau_bar to_power t) - 1) * ( tau_bar to_power m));



         A5: ( tau_bar to_power m) > 0 by Th6, A1;

        (n - m) > (m - m) by A3, XREAL_1: 9;

        then ( tau_bar to_power t) < 1 by Th8, XXREAL_0: 2;

        then (( tau_bar to_power t) - 1) < (1 - 1) by XREAL_1: 9;

        then ((( tau_bar to_power n) - ( tau_bar to_power m)) + ( tau_bar to_power m)) < ( 0 + ( tau_bar to_power m)) by A4, A5, XREAL_1: 6;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM4:12



     Th12: for m,n be non zero Nat st m >= n holds ( Lucas m) >= ( Lucas n)

    proof

      let m,n be non zero Nat;

      assume

       A1: m >= n;

      per cases by A1, XXREAL_0: 1;

        suppose m = n;

        hence thesis;

      end;

        suppose

         A2: m > n;

        then

        consider k be Nat such that

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



         A4: for k,n be non zero Nat holds ( Lucas (n + k)) >= ( Lucas n)

        proof

          defpred P[ Nat] means for n be non zero Nat holds ( Lucas (n + $1)) >= ( Lucas n);



           A5: P[1]

          proof

            let n be non zero Nat;

            (n - 0 ) is Element of NAT & (n + 1) is Element of NAT by ORDINAL1:def 12;

            hence thesis by FIB_NUM3: 18;

          end;



           A6: for k be non zero Nat st P[k] holds P[(k + 1)]

          proof

            let k be non zero Nat;

            assume

             A7: P[k];

            for n be non zero Nat holds ( Lucas (n + (k + 1))) >= ( Lucas n)

            proof

              let n be non zero Nat;

              reconsider p = (n + k) as Element of NAT by ORDINAL1:def 12;

              p is non zero Element of NAT ;

              then ( Lucas (n + k)) >= ( Lucas n) & ( Lucas ((n + k) + 1)) >= ( Lucas (n + k)) by A7, FIB_NUM3: 18;

              hence thesis by XXREAL_0: 2;

            end;

            hence thesis;

          end;

          for k be non zero Nat holds P[k] from NAT_1:sch 10( A5, A6);

          hence thesis;

        end;

        k is non zero Nat & n is non zero Nat by A3, A2;

        hence thesis by A3, A4;

      end;

    end;



     Lm12: ( tau_bar ^2 ) = ((3 - ( sqrt 5)) / 2) by Lm7, POWER: 46;



     Lm13: ( sqrt 5) > 0 by SQUARE_1: 25;

    then (( sqrt 5) + 3) > (( - ( sqrt 5)) + 3) by XREAL_1: 6;

    then ((( sqrt 5) + 3) / 2) > ((( - ( sqrt 5)) + 3) / 2) by XREAL_1: 74;

    then

     Lm14: ( tau ^2 ) > ( tau_bar ^2 ) by Lm6, Lm12, POWER: 46;

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

    then ( sqrt 5) < 3 by SQUARE_1:def 2;

    then (( sqrt 5) - 3) < (3 - 3) by XREAL_1: 9;

    then

     Lm15: ((( sqrt 5) - 3) / 2) < 0 ;

    theorem :: FIB_NUM4:13

    for n be non zero Nat holds ( tau to_power n) > ( tau_bar to_power n)

    proof

      let n be non zero Nat;

      set tb = tau_bar ;

      per cases ;

        suppose

         A1: n is even;

        consider k be Nat such that

         A2: n = (2 * k) by A1, ABIAN:def 2;



         A3: k > 0 by A2;



         A4: ( tau to_power n) = (( tau to_power 2) to_power k) by A2, NEWTON: 9

        .= (( tau ^2 ) to_power k) by POWER: 46;

        ( tau_bar to_power n) = (( tau_bar to_power 2) to_power k) by A2, NEWTON: 9

        .= (( tau_bar ^2 ) to_power k) by POWER: 46;

        hence thesis by A3, A4, Lm14, POWER: 37;

      end;

        suppose n is odd;

        then

        consider k be Nat such that

         A5: n = ((2 * k) + 1) by ABIAN: 9;

        set kk = ( tau to_power (2 * k));



         A6: (( tau / tb) to_power (2 * k)) = ((( tau / tb) to_power 2) to_power k) by NEWTON: 9

        .= ((( tau / tb) ^2 ) to_power k) by POWER: 46;

        (tb to_power (2 * k)) = ((tb to_power 2) to_power k) by NEWTON: 9

        .= (( tau_bar ^2 ) to_power k) by POWER: 46;

        then

         A7: (tb to_power (2 * k)) > 0 by POWER: 34;

        (( tau / tb) to_power (2 * k)) > ((( sqrt 5) - 3) / 2) by A6, Lm15, POWER: 34;

        then ((( tau / tb) to_power (2 * k)) * ((( - 3) - ( sqrt 5)) / 2)) < ((tb / tau ) * ((( - 3) - ( sqrt 5)) / 2)) by Lm13, Lm4, XREAL_1: 69;

        then ((( tau / tb) to_power (2 * k)) * ( tau / tb)) < 1 by Lm5, XCMPLX_1: 112;

        then ((kk / (tb to_power (2 * k))) * ( tau / tb)) < 1 by Th1;

        then ((kk * (1 / (tb to_power (2 * k)))) * ( tau / tb)) < 1 by XCMPLX_1: 99;

        then (((kk * (1 / (tb to_power (2 * k)))) * ( tau / tb)) * (tb to_power (2 * k))) < (1 * (tb to_power (2 * k))) by A7, XREAL_1: 68;

        then ((kk * ( tau / tb)) * ((tb to_power (2 * k)) * (1 / (tb to_power (2 * k))))) < (1 * (tb to_power (2 * k)));

        then ((kk * ( tau / tb)) * ((tb to_power (2 * k)) / (tb to_power (2 * k)))) < (1 * (tb to_power (2 * k))) by XCMPLX_1: 99;

        then ((kk * ( tau / tb)) * 1) < (tb to_power (2 * k)) by A7, XCMPLX_1: 60;

        then ((kk * ( tau * (1 / tb))) * 1) < (tb to_power (2 * k)) by XCMPLX_1: 99;

        then (((kk * ( tau * (1 / tb))) * 1) * tb) > ((tb to_power (2 * k)) * tb) by XREAL_1: 69;

        then ((kk * tau ) * (((1 / tb) * 1) * tb)) > ((tb to_power (2 * k)) * tb);

        then ((kk * tau ) * (tb / tb)) > ((tb to_power (2 * k)) * tb) by XCMPLX_1: 99;

        then ((kk * tau ) * 1) > ((tb to_power (2 * k)) * tb) by XCMPLX_1: 60;

        then (kk * tau ) > ((tb to_power (2 * k)) * (tb to_power 1));

        then (kk * tau ) > (tb to_power ((2 * k) + 1)) by Th2;

        then (kk * ( tau to_power 1)) > (tb to_power ((2 * k) + 1));

        hence thesis by A5, Th2;

      end;

    end;

    theorem :: FIB_NUM4:14



     Th14: for n be Nat st n > 1 holds ( - (1 / 2)) < ( tau_bar to_power n)

    proof

      let n be Nat;

      assume

       A1: n > 1;



       A2: (n + 1) > (1 + 1) by A1, XREAL_1: 8;

      per cases ;

        suppose n is even;

        then

        consider k be Nat such that

         A3: n = (2 * k) by ABIAN:def 2;



         A4: ( 0 ^2 ) = 0 ;

        ( tau_bar to_power n) = (( tau_bar to_power k) to_power 2) by A3, NEWTON: 9

        .= (( tau_bar to_power k) ^2 ) by POWER: 46;

        hence thesis by A4, SQUARE_1: 12;

      end;

        suppose

         A5: n is odd;

        n >= 2 by A2, NAT_1: 13;

        then n = 2 or n > 2 by XXREAL_0: 1;

        then (n + 1) > (2 + 1) by A5, POLYFORM: 5, XREAL_1: 6;

        then n >= 3 by NAT_1: 13;

        then

         A6: ( tau_bar to_power n) >= ( tau_bar to_power 3) by Th10, POLYFORM: 6;

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

        then ( sqrt 5) < (5 / 2) by SQUARE_1:def 2;

        then (2 * ( sqrt 5)) < (2 * (5 / 2)) by XREAL_1: 68;

        then ( - (2 * ( sqrt 5))) > ( - 5) by XREAL_1: 24;

        then (( - (2 * ( sqrt 5))) + 4) > (( - 5) + 4) by XREAL_1: 6;

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

        hence thesis by A6, Lm8, XXREAL_0: 2;

      end;

    end;

    theorem :: FIB_NUM4:15



     Th15: for n be Nat st n > 2 holds ( tau_bar to_power n) >= ( - (1 / ( sqrt 5)))

    proof

      let n be Nat;

      assume n > 2;

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

      then

       A1: ( tau_bar to_power n) >= ( tau_bar to_power 3) by Th10, POLYFORM: 6;



       A2: ( sqrt 5) > 0 by SQUARE_1: 25;

      ( sqrt 5) >= 2 by SQUARE_1: 20, SQUARE_1: 26;

      then (2 * ( sqrt 5)) >= (2 * 2) by XREAL_1: 64;

      then ((2 * ( sqrt 5)) - 5) >= (4 - 5) by XREAL_1: 9;

      then ((2 * ( sqrt 5)) - (( sqrt 5) ^2 )) >= ( - 1) by SQUARE_1:def 2;

      then (((2 - ( sqrt 5)) * ( sqrt 5)) / ( sqrt 5)) >= (( - 1) / ( sqrt 5)) by A2, XREAL_1: 72;

      then (((2 - ( sqrt 5)) * ( sqrt 5)) / ( sqrt 5)) >= ( - (1 / ( sqrt 5))) by XCMPLX_1: 187;

      then (2 - ( sqrt 5)) >= ( - (1 / ( sqrt 5))) by A2, XCMPLX_1: 89;

      hence thesis by A1, Lm8, XXREAL_0: 2;

    end;

    theorem :: FIB_NUM4:16



     Th16: for n be Nat st n >= 2 holds ( tau_bar to_power n) <= (1 / ( sqrt 5))

    proof

      let n be Nat;

      assume

       A1: n >= 2;

      per cases ;

        suppose

         A2: n is even;



         A3: ( sqrt 5) > 0 by SQUARE_1: 25;



         A4: ( tau_bar to_power n) <= ((3 - ( sqrt 5)) / 2) by Lm7, A1, A2, Th11, POLYFORM: 5;

        ( sqrt 5) <= ( sqrt ((7 / 3) ^2 )) by SQUARE_1: 26;

        then ( sqrt 5) <= (7 / 3) by SQUARE_1:def 2;

        then (3 * ( sqrt 5)) <= ((7 / 3) * 3) by XREAL_1: 64;

        then ((3 * ( sqrt 5)) - 5) <= (7 - 5) by XREAL_1: 9;

        then ((3 * ( sqrt 5)) - (( sqrt 5) ^2 )) <= 2 by SQUARE_1:def 2;

        then (((3 * ( sqrt 5)) - (( sqrt 5) * ( sqrt 5))) / 2) <= (2 / 2) by XREAL_1: 72;

        then ((((3 - ( sqrt 5)) / 2) * ( sqrt 5)) / ( sqrt 5)) <= (1 / ( sqrt 5)) by A3, XREAL_1: 72;

        then ((3 - ( sqrt 5)) / 2) <= (1 / ( sqrt 5)) by A3, XCMPLX_1: 89;

        hence thesis by A4, XXREAL_0: 2;

      end;

        suppose n is odd;

        then

         A5: ( tau_bar to_power n) < 0 by Th7;

        ( sqrt 5) >= ( sqrt 0 ) by SQUARE_1: 26;

        hence thesis by A5, SQUARE_1: 17;

      end;

    end;

    theorem :: FIB_NUM4:17



     Th17: for n be Nat holds ((( tau_bar to_power n) / ( sqrt 5)) + (1 / 2)) > 0 & ((( tau_bar to_power n) / ( sqrt 5)) + (1 / 2)) < 1

    proof

      let n be Nat;

      set b = ((1 - ( sqrt 5)) / 2);



       A1: |.b.| = ( - b) by ABSVALUE:def 1, FIB_NUM:def 2;



       A2: (( |.b.| to_power n) * (1 / ( sqrt 5))) < (1 / 2) by Lm11, FIB_NUM:def 2;

      (((b to_power n) * (1 / ( sqrt 5))) + (1 / 2)) > 0 & (((b to_power n) * (1 / ( sqrt 5))) + (1 / 2)) < 1

      proof

        per cases ;

          suppose n is even;

          then ( |.b.| to_power n) = (b to_power n) by Th3, A1, FIB_NUM:def 2;

          then ((b to_power n) * (1 / ( sqrt 5))) > 0 & ((b to_power n) * (1 / ( sqrt 5))) < (1 / 2) by Lm10, Lm11, FIB_NUM:def 2;

          then ((b to_power n) * (1 / ( sqrt 5))) > 0 & (((b to_power n) * (1 / ( sqrt 5))) + (1 / 2)) < ((1 / 2) + (1 / 2)) by XREAL_1: 8;

          hence thesis;

        end;

          suppose n is odd;

          then ( |.b.| to_power n) = ( - (b to_power n)) by Th4, A1, FIB_NUM:def 2;

          then (( - (b to_power n)) * (1 / ( sqrt 5))) > 0 & ( - ((b to_power n) * (1 / ( sqrt 5)))) < (1 / 2) by Lm10, A2, FIB_NUM:def 2;

          then ( - ((b to_power n) / ( sqrt 5))) > 0 & ( - ((b to_power n) / ( sqrt 5))) < (1 / 2) by XCMPLX_1: 99;

          then ((b to_power n) / ( sqrt 5)) < 0 & ( - ( - ((b to_power n) / ( sqrt 5)))) > ( - (1 / 2)) by XREAL_1: 24;

          then (((b to_power n) / ( sqrt 5)) + (1 / 2)) < ( 0 + (1 / 2)) & (((b to_power n) / ( sqrt 5)) + (1 / 2)) > (( - (1 / 2)) + (1 / 2)) by XREAL_1: 8;

          then (((b to_power n) / ( sqrt 5)) + (1 / 2)) < 1 & (((b to_power n) / ( sqrt 5)) + (1 / 2)) > 0 by XXREAL_0: 2;

          hence thesis by XCMPLX_1: 99;

        end;

      end;

      hence thesis by FIB_NUM:def 2, XCMPLX_1: 99;

    end;

    begin

    theorem :: FIB_NUM4:18

    for n be Nat holds [\((( tau to_power n) / ( sqrt 5)) + (1 / 2))/] = ( Fib n)

    proof

      let n be Nat;

      set tn = ( tau_bar to_power n);



       A1: ( Fib n) = ((((( tau to_power n) - tn) / ( sqrt 5)) + (1 / 2)) - (1 / 2)) by FIB_NUM: 7

      .= ((((( tau to_power n) / ( sqrt 5)) - (tn / ( sqrt 5))) + (1 / 2)) - (1 / 2)) by XCMPLX_1: 120

      .= (((( tau to_power n) / ( sqrt 5)) + (1 / 2)) - ((tn / ( sqrt 5)) + (1 / 2)));

      ((tn / ( sqrt 5)) + (1 / 2)) > 0 by Th17;

      then

       A2: (((tn / ( sqrt 5)) + (1 / 2)) + ( Fib n)) > ( 0 + ( Fib n)) by XREAL_1: 6;

      ((tn / ( sqrt 5)) + (1 / 2)) < 1 by Th17;

      then (((tn / ( sqrt 5)) + (1 / 2)) - (1 / 2)) < (1 - (1 / 2)) by XREAL_1: 9;

      then ( - (tn / ( sqrt 5))) > ( - (1 / 2)) by XREAL_1: 24;

      then (( - (tn / ( sqrt 5))) + (( tau to_power n) / ( sqrt 5))) > (( - (1 / 2)) + (( tau to_power n) / ( sqrt 5))) by XREAL_1: 6;

      then ((( tau to_power n) / ( sqrt 5)) - (tn / ( sqrt 5))) > (( - (1 / 2)) + (( tau to_power n) / ( sqrt 5)));

      then ((( tau to_power n) - tn) / ( sqrt 5)) > (( - (1 / 2)) + (( tau to_power n) / ( sqrt 5))) by XCMPLX_1: 120;

      then ( Fib n) > (((( tau to_power n) / ( sqrt 5)) + (1 / 2)) - 1) by FIB_NUM: 7;

      hence thesis by A2, A1, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:19

    for n be Nat st n <> 0 holds [/((( tau to_power n) / ( sqrt 5)) - (1 / 2))\] = ( Fib n)

    proof

      let n be Nat;

      set tn = ( tau to_power n);

      set tbn = ( tau_bar to_power n);

      assume

       A1: n <> 0 ;



       A2: ( sqrt 5) > 0 by SQUARE_1: 25;



       A3: ((tn / ( sqrt 5)) - (1 / 2)) <= ( Fib n)

      proof

        1 <= ( sqrt 5) by SQUARE_1: 18, SQUARE_1: 26;

        then (1 / 2) <= (( sqrt 5) / 2) by XREAL_1: 72;

        then tbn <= (( sqrt 5) / 2) by A1, Th8, XXREAL_0: 2;

        then (tbn / ( sqrt 5)) <= ((( sqrt 5) / 2) / ( sqrt 5)) by A2, XREAL_1: 72;

        then (tbn / ( sqrt 5)) <= ((( sqrt 5) / ( sqrt 5)) / 2) by XCMPLX_1: 48;

        then (tbn / ( sqrt 5)) <= (1 / 2) by A2, XCMPLX_1: 60;

        then ( - (tbn / ( sqrt 5))) >= ( - (1 / 2)) by XREAL_1: 24;

        then (( - (tbn / ( sqrt 5))) + (tn / ( sqrt 5))) >= (( - (1 / 2)) + (tn / ( sqrt 5))) by XREAL_1: 6;

        then ((tn / ( sqrt 5)) - (tbn / ( sqrt 5))) >= (( - (1 / 2)) + (tn / ( sqrt 5)));

        then ((tn - tbn) / ( sqrt 5)) >= ((tn / ( sqrt 5)) - (1 / 2)) by XCMPLX_1: 120;

        hence thesis by FIB_NUM: 7;

      end;

      (((tn / ( sqrt 5)) - (1 / 2)) + 1) > ( Fib n)

      proof

        (n + 1) > ( 0 + 1) by A1, XREAL_1: 6;

        then

         A4: n >= 1 by NAT_1: 13;

        per cases by A4, XXREAL_0: 1;

          suppose

           A5: n = 1;



          then

           A6: (((tn / ( sqrt 5)) - (1 / 2)) + 1) = ((( tau / ( sqrt 5)) - (1 / 2)) + 1)

          .= ((((1 + ( sqrt 5)) / 2) / ( sqrt 5)) + (1 - (1 / 2))) by FIB_NUM:def 1

          .= ((((1 + ( sqrt 5)) / ( sqrt 5)) / 2) + (1 / 2)) by XCMPLX_1: 48

          .= ((((1 + ( sqrt 5)) / ( sqrt 5)) + 1) / 2)

          .= ((((1 / ( sqrt 5)) + (( sqrt 5) / ( sqrt 5))) + 1) / 2) by XCMPLX_1: 62

          .= ((((1 / ( sqrt 5)) + 1) + 1) / 2) by A2, XCMPLX_1: 60

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

          (((1 / ( sqrt 5)) / 2) + 1) > ( 0 + 1) by A2, XREAL_1: 6;

          hence thesis by A5, A6, PRE_FF: 1;

        end;

          suppose

           A7: n > 1;

          1 < ( sqrt 5) by SQUARE_1: 18, SQUARE_1: 27;

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

          then

           A8: ( - (1 / 2)) > ( - (( sqrt 5) / 2)) by XREAL_1: 24;

          tbn > ( - (1 / 2)) by A7, Th14;

          then tbn > ( - (( sqrt 5) / 2)) by A8, XXREAL_0: 2;

          then (tbn / ( sqrt 5)) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by A2, XREAL_1: 74;

          then (tbn / ( sqrt 5)) > ( - ((( sqrt 5) / 2) / ( sqrt 5))) by XCMPLX_1: 187;

          then (tbn / ( sqrt 5)) > ( - ((( sqrt 5) / ( sqrt 5)) / 2)) by XCMPLX_1: 48;

          then (tbn / ( sqrt 5)) > ( - (1 / 2)) by A2, XCMPLX_1: 60;

          then ( - (tbn / ( sqrt 5))) < ( - ( - (1 / 2))) by XREAL_1: 24;

          then (( - (tbn / ( sqrt 5))) + (tn / ( sqrt 5))) < ((1 / 2) + (tn / ( sqrt 5))) by XREAL_1: 6;

          then ((tn / ( sqrt 5)) - (tbn / ( sqrt 5))) < ((1 / 2) + (tn / ( sqrt 5)));

          then ((tn - tbn) / ( sqrt 5)) < ((1 / 2) + (tn / ( sqrt 5))) by XCMPLX_1: 120;

          hence thesis by FIB_NUM: 7;

        end;

      end;

      hence thesis by A3, INT_1:def 7;

    end;

    set s5 = ( sqrt 5);



     Lm16: 1 < s5 by SQUARE_1: 18, SQUARE_1: 27;

    (1 - s5) <> 0 by SQUARE_1: 18, SQUARE_1: 27;

    then ((1 - s5) ^2 ) > 0 by SQUARE_1: 12;

    then

     Lm17: ((1 - s5) to_power 2) > 0 by POWER: 46;



     Lm18: s5 > 0 by SQUARE_1: 25;

    (2 * 1) < (2 * s5) by Lm16, XREAL_1: 68;

    then ( - (2 * s5)) < ( - 2) by XREAL_1: 24;

    then (( - (2 * s5)) + 6) < (( - 2) + 6) by XREAL_1: 8;

    then ((1 - (2 * s5)) + 5) < 4;

    then (((1 ^2 ) - ((2 * 1) * s5)) + (s5 ^2 )) < 4 by SQUARE_1:def 2;

    then ((1 - s5) ^2 ) < (2 ^2 );

    then ((1 - s5) ^2 ) < (2 to_power 2) by POWER: 46;

    then

     Lm19: ((1 - s5) to_power 2) < (2 to_power 2) by POWER: 46;

    theorem :: FIB_NUM4:20

    for n be Nat st n <> 0 holds [\(( tau to_power (2 * n)) / ( sqrt 5))/] = ( Fib (2 * n))

    proof

      let n be Nat;

      assume

       A1: n <> 0 ;



       A2: ((( tau to_power (2 * n)) / s5) - 1) < ( Fib (2 * n))

      proof



         A3: (2 to_power (2 * n)) > 0 by POWER: 34;

        (((1 - s5) to_power 2) to_power n) < ((2 to_power 2) to_power n) by A1, Lm17, Lm19, POWER: 37;

        then (((1 - s5) to_power 2) to_power n) < (2 to_power (2 * n)) by POWER: 33;

        then ((1 - s5) to_power (2 * n)) < (2 to_power (2 * n)) by NEWTON: 9;

        then (((1 - s5) to_power (2 * n)) / (2 to_power (2 * n))) < ((2 to_power (2 * n)) / (2 to_power (2 * n))) by A3, XREAL_1: 74;

        then (((1 - s5) to_power (2 * n)) / (2 to_power (2 * n))) < 1 by A3, XCMPLX_1: 60;

        then ( tau_bar to_power (2 * n)) < 1 by Th1, FIB_NUM:def 2;

        then ( tau_bar to_power (2 * n)) < s5 by Lm16, XXREAL_0: 2;

        then (( tau_bar to_power (2 * n)) / s5) < (s5 / s5) by Lm18, XREAL_1: 74;

        then (( tau_bar to_power (2 * n)) / s5) < 1 by Lm18, XCMPLX_1: 60;

        then ( - (( tau_bar to_power (2 * n)) / s5)) > ( - 1) by XREAL_1: 24;

        then (( - (( tau_bar to_power (2 * n)) / s5)) + (( tau to_power (2 * n)) / s5)) > (( - 1) + (( tau to_power (2 * n)) / s5)) by XREAL_1: 8;

        then ((( tau to_power (2 * n)) / s5) - (( tau_bar to_power (2 * n)) / s5)) > (( - 1) + (( tau to_power (2 * n)) / s5));

        then ((( tau to_power (2 * n)) - ( tau_bar to_power (2 * n))) / s5) > (( - 1) + (( tau to_power (2 * n)) / ( sqrt 5))) by XCMPLX_1: 120;

        hence thesis by FIB_NUM: 7;

      end;

      ( tau_bar to_power (2 * n)) = (( tau_bar to_power 2) |^ n) by NEWTON: 9

      .= (( tau_bar ^2 ) to_power n) by POWER: 46;

      then ( tau_bar to_power (2 * n)) > 0 by POWER: 34;

      then (( - (( tau_bar to_power (2 * n)) / ( sqrt 5))) + (( tau to_power (2 * n)) / s5)) < ( 0 + (( tau to_power (2 * n)) / s5)) by Lm18, XREAL_1: 8;

      then ((( tau to_power (2 * n)) / s5) - (( tau_bar to_power (2 * n)) / s5)) < (( tau to_power (2 * n)) / s5);

      then ((( tau to_power (2 * n)) - ( tau_bar to_power (2 * n))) / s5) < (( tau to_power (2 * n)) / s5) by XCMPLX_1: 120;

      then ( Fib (2 * n)) <= (( tau to_power (2 * n)) / s5) by FIB_NUM: 7;

      hence thesis by A2, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:21

    for n be Nat holds [/(( tau to_power ((2 * n) + 1)) / ( sqrt 5))\] = ( Fib ((2 * n) + 1))

    proof

      let n be Nat;



       A1: ( Fib ((2 * n) + 1)) = ((( tau to_power ((2 * n) + 1)) - ( tau_bar to_power ((2 * n) + 1))) / ( sqrt 5)) by FIB_NUM: 7

      .= ((( tau to_power ((2 * n) + 1)) / ( sqrt 5)) - (( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5))) by XCMPLX_1: 120;



       A2: ( sqrt 5) > 0 by SQUARE_1: 17, SQUARE_1: 27;

      ( tau_bar to_power ((2 * n) + 1)) < 0

      proof

        set t = ( - tau_bar );



         A3: ( tau_bar to_power ((2 * n) + 1)) = (( - t) to_power ((2 * n) + 1))

        .= ( - (t to_power ((2 * n) + 1))) by Th4;

        (t to_power ((2 * n) + 1)) > 0 by POWER: 34;

        hence thesis by A3;

      end;

      then

       A4: (( tau to_power ((2 * n) + 1)) / ( sqrt 5)) <= ( Fib ((2 * n) + 1)) by A1, A2, XREAL_1: 46;

      ((( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5)) + (1 / 2)) > 0 by Th17;

      then (((( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5)) + (1 / 2)) - (1 / 2)) > ( 0 - (1 / 2)) by XREAL_1: 9;

      then (( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5)) > ( - 1) by XXREAL_0: 2;

      then ( - (( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5))) < ( - ( - 1)) by XREAL_1: 24;

      then (( - (( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5))) + (( tau to_power ((2 * n) + 1)) / ( sqrt 5))) < (1 + (( tau to_power ((2 * n) + 1)) / ( sqrt 5))) by XREAL_1: 8;

      then ((( tau to_power ((2 * n) + 1)) / ( sqrt 5)) - (( tau_bar to_power ((2 * n) + 1)) / ( sqrt 5))) < (1 + (( tau to_power ((2 * n) + 1)) / ( sqrt 5)));

      then ((( tau to_power ((2 * n) + 1)) - ( tau_bar to_power ((2 * n) + 1))) / ( sqrt 5)) < (1 + (( tau to_power ((2 * n) + 1)) / ( sqrt 5))) by XCMPLX_1: 120;

      then ( Fib ((2 * n) + 1)) < ((( tau to_power ((2 * n) + 1)) / ( sqrt 5)) + 1) by FIB_NUM: 7;

      hence thesis by A4, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:22



     Th22: for n be Nat st n >= 2 & n is even holds ( Fib (n + 1)) = [\(( tau * ( Fib n)) + 1)/]

    proof

      let n be Nat;

      assume

       A1: n >= 2 & n is even;

      set t = tau ;

      set tb = tau_bar ;



       A2: ( sqrt 5) > 0 by SQUARE_1: 17, SQUARE_1: 27;



       A3: (t * tb) = (((1 ^2 ) - (( sqrt 5) ^2 )) / 4) by FIB_NUM:def 1, FIB_NUM:def 2

      .= ((1 - 5) / 4) by SQUARE_1:def 2

      .= ( - 1);

      (tb to_power n) = (( - tb) to_power n) by A1, Th3;

      then

       A4: (tb to_power n) > 0 by POWER: 34;



       A5: ((tb to_power 2) + 1) = ((tb ^2 ) + 1) by POWER: 46

      .= (((((1 ^2 ) - ((2 * 1) * ( sqrt 5))) + (( sqrt 5) ^2 )) / 4) + 1) by FIB_NUM:def 2

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

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

      .= (((( sqrt 5) ^2 ) - ( sqrt 5)) / 2) by SQUARE_1:def 2

      .= ( - (( sqrt 5) * tb)) by FIB_NUM:def 2;

      (t * ( Fib n)) = (t * (((t to_power n) - (tb to_power n)) / ( sqrt 5))) by FIB_NUM: 7

      .= ((t * ((t to_power n) - (tb to_power n))) / ( sqrt 5)) by XCMPLX_1: 74

      .= (((t * (t to_power n)) - (t * (tb to_power n))) / ( sqrt 5))

      .= ((((t to_power 1) * (t to_power n)) - (t * (tb to_power n))) / ( sqrt 5))

      .= (((t to_power (n + 1)) - (t * (tb to_power ((n - 1) + 1)))) / ( sqrt 5)) by POWER: 27

      .= (((t to_power (n + 1)) - (t * ((tb to_power (n - 1)) * (tb to_power 1)))) / ( sqrt 5)) by Th2

      .= (((t to_power (n + 1)) - (t * ((tb to_power (n - 1)) * tb))) / ( sqrt 5))

      .= (((t to_power (n + 1)) - ((t * tb) * (tb to_power (n - 1)))) / ( sqrt 5))

      .= (((((t to_power (n + 1)) - (( - 1) * (tb to_power (n - 1)))) + (tb to_power (n - 1))) - (tb to_power (n - 1))) / ( sqrt 5)) by A3

      .= ((((t to_power (n + 1)) - (tb to_power (n + 1))) + ((tb to_power (n - 1)) + (tb to_power (n + 1)))) / ( sqrt 5))

      .= ((((t to_power (n + 1)) - (tb to_power (n + 1))) / ( sqrt 5)) + (((tb to_power (n - 1)) + (tb to_power ((n - 1) + 2))) / ( sqrt 5))) by XCMPLX_1: 62

      .= (( Fib (n + 1)) + (((tb to_power (n - 1)) + (tb to_power ((n - 1) + 2))) / ( sqrt 5))) by FIB_NUM: 7

      .= (( Fib (n + 1)) + ((((tb to_power (n - 1)) * 1) + ((tb to_power (n - 1)) * (tb to_power 2))) / ( sqrt 5))) by Th2

      .= (( Fib (n + 1)) + (((tb to_power (n - 1)) * (1 + (tb to_power 2))) / ( sqrt 5)))

      .= (( Fib (n + 1)) + (((tb to_power (n - 1)) * ( - (( sqrt 5) * tb))) / ( sqrt 5))) by A5

      .= (( Fib (n + 1)) + ((((( - 1) * (tb to_power (n - 1))) * tb) * ( sqrt 5)) / ( sqrt 5)))

      .= (( Fib (n + 1)) + ((( - 1) * (tb to_power (n - 1))) * tb)) by A2, XCMPLX_1: 89

      .= (( Fib (n + 1)) - ((tb to_power (n - 1)) * tb))

      .= (( Fib (n + 1)) - ((tb to_power (n - 1)) * (tb to_power 1)))

      .= (( Fib (n + 1)) - (tb to_power ((n - 1) + 1))) by Th2

      .= (( Fib (n + 1)) - (tb to_power n));

      then

       A6: ( Fib (n + 1)) = (((t * ( Fib n)) + 1) - (1 - (tb to_power n)));

      (tb to_power n) < 1 by Th8, A1, XXREAL_0: 2;

      then ( - (tb to_power n)) > ( - 1) by XREAL_1: 24;

      then (( - (tb to_power n)) + 1) > (( - 1) + 1) by XREAL_1: 8;

      then

       A7: ( Fib (n + 1)) < ((t * ( Fib n)) + 1) by A6, XREAL_1: 44;

      ((t * ( Fib n)) + 1) < (( Fib (n + 1)) + 1)

      proof



         A8: (t * ( Fib n)) = (t * (((t to_power n) - (tb to_power n)) / ( sqrt 5))) by FIB_NUM: 7

        .= ((t * ((t to_power n) - (tb to_power n))) / ( sqrt 5)) by XCMPLX_1: 74

        .= (((t * (t to_power n)) - (t * (tb to_power n))) / ( sqrt 5))

        .= ((((t to_power 1) * (t to_power n)) - (t * (tb to_power n))) / ( sqrt 5))

        .= (((t to_power (n + 1)) - (t * (tb to_power n))) / ( sqrt 5)) by POWER: 27

        .= (((t to_power (n + 1)) / ( sqrt 5)) - ((t * (tb to_power n)) / ( sqrt 5))) by XCMPLX_1: 120;



         A9: ( Fib (n + 1)) = (((t to_power (n + 1)) - (tb to_power (n + 1))) / ( sqrt 5)) by FIB_NUM: 7

        .= (((t to_power (n + 1)) / ( sqrt 5)) - ((tb to_power (n + 1)) / ( sqrt 5))) by XCMPLX_1: 120;

        ((tb to_power n) * t) > ((tb to_power n) * tb) by A4, XREAL_1: 68;

        then ((tb to_power n) * t) > ((tb to_power n) * (tb to_power 1));

        then ((t * (tb to_power n)) / ( sqrt 5)) > (((tb to_power n) * (tb to_power 1)) / ( sqrt 5)) by A2, XREAL_1: 74;

        then ((t * (tb to_power n)) / ( sqrt 5)) > ((tb to_power (n + 1)) / ( sqrt 5)) by Th2;

        then ( - ((t * (tb to_power n)) / ( sqrt 5))) < ( - ((tb to_power (n + 1)) / ( sqrt 5))) by XREAL_1: 24;

        then (( - ((t * (tb to_power n)) / ( sqrt 5))) + ((t to_power (n + 1)) / ( sqrt 5))) < (( - ((tb to_power (n + 1)) / ( sqrt 5))) + ((t to_power (n + 1)) / ( sqrt 5))) by XREAL_1: 8;

        hence thesis by A8, A9, XREAL_1: 8;

      end;

      then (((t * ( Fib n)) + 1) - 1) < ((( Fib (n + 1)) + 1) - 1) by XREAL_1: 9;

      hence thesis by A7, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:23



     Th23: for n be Nat st n >= 2 & n is odd holds ( Fib (n + 1)) = [/(( tau * ( Fib n)) - 1)\]

    proof

      let n be Nat;

      assume

       A1: n >= 2 & n is odd;



       A2: ( sqrt 5) > 0 by SQUARE_1: 17, SQUARE_1: 27;

      (( tau * ( tau_bar to_power n)) + ( sqrt 5)) >= ( tau_bar to_power (n + 1))

      proof

        set tbn = ( tau_bar to_power n);



         A3: tbn < 0 by A1, Th7;

        ( tau + (( sqrt 5) / tbn)) <= tau_bar

        proof

          n > 1 by A1, XXREAL_0: 2;

          then tbn >= ( - (1 / 2)) by Th14;

          then tbn > ( - 1) by XXREAL_0: 2;

          then (tbn + 1) >= (( - 1) + 1) by XREAL_1: 6;

          then ((tbn + 1) / tbn) <= ( 0 / tbn) by A3;

          then ((tbn / tbn) + (1 / tbn)) <= 0 by XCMPLX_1: 62;

          then (1 + (1 / tbn)) <= 0 by A3, XCMPLX_1: 60;

          then ((1 + (1 / tbn)) * ( sqrt 5)) <= ( 0 * ( sqrt 5)) by A2;

          then ((1 * ( sqrt 5)) + ((1 / tbn) * ( sqrt 5))) <= 0 ;

          then (( sqrt 5) + (( sqrt 5) / tbn)) <= 0 by XCMPLX_1: 74;

          then ((((( sqrt 5) / 2) + (( sqrt 5) / tbn)) + (( sqrt 5) / 2)) - (( sqrt 5) / 2)) <= ( 0 - (( sqrt 5) / 2)) by XREAL_1: 9;

          then (((( sqrt 5) / 2) + (( sqrt 5) / tbn)) + (1 / 2)) <= (( - (( sqrt 5) / 2)) + (1 / 2)) by XREAL_1: 6;

          hence thesis by FIB_NUM:def 1, FIB_NUM:def 2;

        end;

        then (( tau + (( sqrt 5) / tbn)) * tbn) >= ( tau_bar * tbn) by A3, XREAL_1: 65;

        then (( tau + (( sqrt 5) / tbn)) * tbn) >= (( tau_bar to_power 1) * tbn);

        then (( tau * tbn) + ((( sqrt 5) / tbn) * tbn)) >= ( tau_bar to_power (n + 1)) by Th2;

        hence thesis by A3, XCMPLX_1: 87;

      end;

      then ( - (( tau * ( tau_bar to_power n)) + ( sqrt 5))) <= ( - ( tau_bar to_power (n + 1))) by XREAL_1: 24;

      then ((( - ( tau * ( tau_bar to_power n))) - ( sqrt 5)) + ( tau to_power (n + 1))) <= (( - ( tau_bar to_power (n + 1))) + ( tau to_power (n + 1))) by XREAL_1: 6;

      then ((( tau to_power (n + 1)) - ( tau * ( tau_bar to_power n))) - ( sqrt 5)) <= (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1)));

      then (((( tau to_power 1) * ( tau to_power n)) - ( tau * ( tau_bar to_power n))) - ( sqrt 5)) <= (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) by POWER: 27;

      then ((( tau * ( tau to_power n)) - ( tau * ( tau_bar to_power n))) - ( sqrt 5)) <= (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1)));

      then ((( tau * (( tau to_power n) - ( tau_bar to_power n))) - ( sqrt 5)) / ( sqrt 5)) <= ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) by A2, XREAL_1: 72;

      then ((( tau * (( tau to_power n) - ( tau_bar to_power n))) / ( sqrt 5)) - (( sqrt 5) / ( sqrt 5))) <= ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) by XCMPLX_1: 120;

      then (( tau * ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5))) - (( sqrt 5) / ( sqrt 5))) <= ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) by XCMPLX_1: 74;

      then (( tau * ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5))) - 1) <= ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) by A2, XCMPLX_1: 60;

      then (( tau * ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5))) - 1) <= ( Fib (n + 1)) by FIB_NUM: 7;

      then

       A4: (( tau * ( Fib n)) - 1) <= ( Fib (n + 1)) by FIB_NUM: 7;

      ((( tau * ( Fib n)) - 1) + 1) > ( Fib (n + 1))

      proof

        set tn = ( tau to_power n);

        set tbn = ( tau_bar to_power n);



         A5: ( tau * ( Fib n)) = ( tau * ((tn - tbn) / ( sqrt 5))) by FIB_NUM: 7

        .= (( tau * (tn - tbn)) / ( sqrt 5)) by XCMPLX_1: 74;



         A6: tbn < 0 by Th7, A1;

        ( tau * tbn) < (( tau_bar to_power 1) * tbn) by A6, XREAL_1: 69;

        then ( tau * tbn) < ( tau_bar to_power (n + 1)) by Th2;

        then ( - ( tau * tbn)) > ( - ( tau_bar to_power (n + 1))) by XREAL_1: 24;

        then (( - ( tau * tbn)) + ( tau to_power (n + 1))) > (( - ( tau_bar to_power (n + 1))) + ( tau to_power (n + 1))) by XREAL_1: 6;

        then (( tau to_power (n + 1)) - ( tau * tbn)) > (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1)));

        then ((( tau to_power 1) * tn) - ( tau * tbn)) > (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) by Th2;

        then (( tau * tn) - ( tau * tbn)) > (( tau to_power (n + 1)) - ( tau_bar to_power (n + 1)));

        then (( tau * (tn - tbn)) / ( sqrt 5)) > ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) by A2, XREAL_1: 74;

        hence thesis by A5, FIB_NUM: 7;

      end;

      hence thesis by A4, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:24



     Th24: for n be Nat st n >= 2 holds ( Fib (n + 1)) = [\(((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2)/]

    proof

      let n be Nat;

      assume

       A1: n >= 2;



       A2: ( sqrt 5) > 0 by SQUARE_1: 25;

      set tn = ( tau to_power n);

      set tb = tau_bar ;

      set s5 = ( sqrt 5);

      set tbn = (tb to_power n);

      per cases ;

        suppose

         A3: n is even;

        then

         A4: tbn > 0 by Th6;



         A5: (((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2) >= ( Fib (n + 1))

        proof

          tbn <= (1 / 2) by Th8, A1;

          then (2 * tbn) <= (2 * (1 / 2)) by XREAL_1: 64;

          then ((2 * tbn) / tbn) <= (1 / tbn) by A4, XREAL_1: 72;

          then 2 <= (1 / tbn) by A4, XCMPLX_1: 89;

          then (2 * s5) <= ((1 / tbn) * s5) by A2, XREAL_1: 64;

          then (s5 + s5) <= ((1 * s5) / tbn) by XCMPLX_1: 74;

          then ((s5 + s5) - s5) <= (((1 * s5) / tbn) - s5) by XREAL_1: 9;

          then ( - s5) >= ( - ((s5 / tbn) - s5)) by XREAL_1: 24;

          then (( - s5) + 1) >= ((( - (s5 / tbn)) + s5) + 1) by XREAL_1: 6;

          then tau_bar >= (((s5 + 1) - (s5 / tbn)) / 2) by FIB_NUM:def 2, XREAL_1: 72;

          then ( tau_bar * tbn) >= (( tau - ((s5 / tbn) / 2)) * tbn) by A4, FIB_NUM:def 1, XREAL_1: 64;

          then (tb * tbn) >= (( tau - ((( sqrt 5) / 2) / tbn)) * tbn) by XCMPLX_1: 48;

          then (tb * tbn) >= (( tau * tbn) - (((s5 / 2) / tbn) * tbn));

          then (tb * tbn) >= (( tau * tbn) - (s5 / 2)) by A4, XCMPLX_1: 87;

          then ((tb to_power 1) * tbn) >= (( tau * tbn) - (s5 / 2));

          then (tb to_power (n + 1)) >= (( tau * tbn) - (s5 / 2)) by Th2;

          then ( - (tb to_power (n + 1))) <= ( - (( tau * tbn) - (s5 / 2))) by XREAL_1: 24;

          then (( - (tb to_power (n + 1))) + ( tau to_power (n + 1))) <= ((( - ( tau * tbn)) + (( sqrt 5) / 2)) + ( tau to_power (n + 1))) by XREAL_1: 6;

          then (( - (tb to_power (n + 1))) + ( tau to_power (n + 1))) <= ((( tau to_power (n + 1)) - ( tau * tbn)) + (s5 / 2));

          then (( - (tb to_power (n + 1))) + ( tau to_power (n + 1))) <= (((tn * ( tau to_power 1)) - ( tau * tbn)) + (s5 / 2)) by Th2;

          then (( - (tb to_power (n + 1))) + ( tau to_power (n + 1))) <= (((tn * tau ) - ( tau * tbn)) + (s5 / 2));

          then ((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) <= ((( tau * (tn - tbn)) + (s5 / 2)) / s5) by A2, XREAL_1: 72;

          then ( Fib (n + 1)) <= ((( tau * (tn - tbn)) + (s5 / 2)) / s5) by FIB_NUM: 7;

          then ( Fib (n + 1)) <= ((( tau * (tn - tbn)) / s5) + ((s5 / 2) / s5)) by XCMPLX_1: 62;

          then ( Fib (n + 1)) <= (( tau * ((tn - tbn) / s5)) + ((s5 / 2) / s5)) by XCMPLX_1: 74;

          then ( Fib (n + 1)) <= (( tau * ( Fib n)) + ((s5 / 2) / ( sqrt 5))) by FIB_NUM: 7;

          then ( Fib (n + 1)) <= (( tau * ( Fib n)) + ((s5 / s5) / 2)) by XCMPLX_1: 48;

          then ( Fib (n + 1)) <= (( tau * ( Fib n)) + (1 / 2)) by A2, XCMPLX_1: 60;

          hence thesis by FIB_NUM:def 1;

        end;

        ((((( Fib n) + (s5 * ( Fib n))) + 1) / 2) - 1) < ( Fib (n + 1))

        proof

          ( Fib (n + 1)) = [\(( tau * ( Fib n)) + 1)/] by A1, A3, Th22;

          then

           A6: ((( tau * ( Fib n)) + 1) - 1) < ( Fib (n + 1)) by INT_1:def 6;

          ((( Fib n) + (s5 * ( Fib n))) + 1) <= ((( Fib n) + (s5 * ( Fib n))) + 2) by XREAL_1: 6;

          then (((( Fib n) + (s5 * ( Fib n))) + 1) / 2) <= (((( Fib n) + (s5 * ( Fib n))) + 2) / 2) by XREAL_1: 72;

          then ((((( Fib n) + (s5 * ( Fib n))) + 1) / 2) - 1) <= ((( tau * ( Fib n)) + 1) - 1) by FIB_NUM:def 1, XREAL_1: 9;

          hence thesis by A6, XXREAL_0: 2;

        end;

        hence thesis by A5, INT_1:def 6;

      end;

        suppose

         A7: n is odd;



         A8: (((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2) >= ( Fib (n + 1))

        proof

          ( Fib (n + 1)) = [/(( tau * ( Fib n)) - 1)\] by A1, A7, Th23;

          then

           A9: ((( tau * ( Fib n)) - 1) + 1) > ( Fib (n + 1)) by INT_1:def 7;

          (1 + (( Fib n) + (( sqrt 5) * ( Fib n)))) > ( 0 + (( Fib n) + (( sqrt 5) * ( Fib n)))) by XREAL_1: 6;

          then (((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2) > ((( Fib n) + (( sqrt 5) * ( Fib n))) / 2) by XREAL_1: 74;

          hence thesis by A9, FIB_NUM:def 1, XXREAL_0: 2;

        end;

        ((((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2) - 1) < ( Fib (n + 1))

        proof

          n > 1 by A1, XXREAL_0: 2;

          then ((2 * ( sqrt 5)) * tbn) > ((2 * ( sqrt 5)) * ( - (1 / 2))) by A2, Th14, XREAL_1: 68;

          then ( - ((2 * ( sqrt 5)) * tbn)) < ( - ((2 * ( sqrt 5)) * ( - (1 / 2)))) by XREAL_1: 24;

          then (((((((1 * tn) + (( sqrt 5) * tn)) - ((2 * tau ) * tn)) + ((2 * tb) * tbn)) - (( sqrt 5) * tbn)) - (1 * tbn)) + ((2 * tau ) * tn)) < (( sqrt 5) + ((2 * tau ) * tn)) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1: 6;

          then (((((tn + (( sqrt 5) * tn)) + ((2 * tb) * tbn)) - (( sqrt 5) * tbn)) - tbn) - ((2 * tb) * tbn)) < ((( sqrt 5) + ((2 * tau ) * tn)) - ((2 * tb) * tbn)) by XREAL_1: 9;

          then (((1 + ( sqrt 5)) * (tn - tbn)) / ( sqrt 5)) < (((( sqrt 5) + ((2 * tau ) * tn)) - ((2 * tb) * tbn)) / ( sqrt 5)) by A2, XREAL_1: 74;

          then ((1 + ( sqrt 5)) * ((tn - tbn) / ( sqrt 5))) < (((( sqrt 5) + (2 * ( tau * tn))) - ((2 * tb) * tbn)) / ( sqrt 5)) by XCMPLX_1: 74;

          then ((1 + ( sqrt 5)) * ( Fib n)) < (((( sqrt 5) + (2 * ( tau * tn))) - ((2 * tb) * tbn)) / ( sqrt 5)) by FIB_NUM: 7;

          then ((1 + ( sqrt 5)) * ( Fib n)) < (((( sqrt 5) + (2 * (( tau to_power 1) * tn))) - ((2 * tb) * tbn)) / ( sqrt 5));

          then ((1 + ( sqrt 5)) * ( Fib n)) < (((( sqrt 5) + (2 * ( tau to_power (n + 1)))) - (2 * (tb * tbn))) / ( sqrt 5)) by Th2;

          then ((1 + ( sqrt 5)) * ( Fib n)) < (((( sqrt 5) + (2 * ( tau to_power (n + 1)))) - (2 * ((tb to_power 1) * tbn))) / ( sqrt 5));

          then ((1 + ( sqrt 5)) * ( Fib n)) < (((( sqrt 5) + (2 * ( tau to_power (n + 1)))) - (2 * (tb to_power (n + 1)))) / ( sqrt 5)) by Th2;

          then ((1 + ( sqrt 5)) * ( Fib n)) < ((( sqrt 5) + (2 * (( tau to_power (n + 1)) - (tb to_power (n + 1))))) / ( sqrt 5));

          then ((1 + ( sqrt 5)) * ( Fib n)) < ((( sqrt 5) / ( sqrt 5)) + ((2 * (( tau to_power (n + 1)) - (tb to_power (n + 1)))) / ( sqrt 5))) by XCMPLX_1: 62;

          then ((1 + ( sqrt 5)) * ( Fib n)) < ((( sqrt 5) / ( sqrt 5)) + (2 * ((( tau to_power (n + 1)) - (tb to_power (n + 1))) / ( sqrt 5)))) by XCMPLX_1: 74;

          then ((1 + ( sqrt 5)) * ( Fib n)) < ((( sqrt 5) / ( sqrt 5)) + (2 * ( Fib (n + 1)))) by FIB_NUM: 7;

          then ((1 + ( sqrt 5)) * ( Fib n)) < (1 + (2 * ( Fib (n + 1)))) by A2, XCMPLX_1: 60;

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

          then ((((1 + ( sqrt 5)) * ( Fib n)) / 2) - (1 / 2)) < (((1 / 2) + ( Fib (n + 1))) - (1 / 2)) by XREAL_1: 9;

          hence thesis;

        end;

        hence thesis by A8, INT_1:def 6;

      end;

    end;

    theorem :: FIB_NUM4:25

    for n be Nat st n >= 2 holds ( Fib (n + 1)) = [/(((( Fib n) + (( sqrt 5) * ( Fib n))) - 1) / 2)\]

    proof

      let n be Nat;

      assume

       A1: n >= 2;

      then ( Fib (n + 1)) = [\(((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2)/] by Th24;

      then

       A2: ((((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2) - 1) < ( Fib (n + 1)) by INT_1:def 6;

      ((((( Fib n) + (( sqrt 5) * ( Fib n))) - 1) / 2) + 1) > ( Fib (n + 1))

      proof

        ( Fib (n + 1)) = [\(((( Fib n) + (( sqrt 5) * ( Fib n))) + 1) / 2)/] by Th24, A1;

        then

         A3: ((((( Fib n) + (( sqrt 5) * ( Fib n))) - 1) / 2) + 1) >= ( Fib (n + 1)) by INT_1:def 6;

        ((((( Fib n) + (( sqrt 5) * ( Fib n))) - 1) / 2) + 1) <> ( Fib (n + 1))

        proof

          set tn = ( tau to_power n);

          set tbn = ( tau_bar to_power n);

          set t1 = ( tau to_power (n + 1));

          set t2 = ( tau_bar to_power (n + 1));

          set s5 = ( sqrt 5);



           A4: s5 > 0 by SQUARE_1: 25;

          assume ((((( Fib n) + (s5 * ( Fib n))) - 1) / 2) + 1) = ( Fib (n + 1));

          then ((( Fib n) * (1 + s5)) + 1) = (2 * ( Fib (n + 1)));

          then ((((tn - tbn) / s5) * (1 + s5)) + 1) = (2 * ( Fib (n + 1))) by FIB_NUM: 7;

          then (((((tn - tbn) / s5) * (1 + s5)) + 1) * s5) = ((2 * ((t1 - t2) / s5)) * s5) by FIB_NUM: 7;

          then (((((tn - tbn) / s5) * (1 + s5)) * s5) + (1 * s5)) = (2 * (((t1 - t2) / s5) * s5));

          then (((((tn - tbn) / s5) * (1 + s5)) * s5) + s5) = (2 * (t1 - t2)) by A4, XCMPLX_1: 87;

          then (((((tn - tbn) * (1 + s5)) / s5) * s5) + s5) = ((2 * t1) - (2 * t2)) by XCMPLX_1: 74;

          then (((tn - tbn) * (1 + s5)) + s5) = ((2 * t1) - (2 * t2)) by A4, XCMPLX_1: 87;

          then (((tn * (1 + s5)) - (tbn + (tbn * s5))) + s5) = ((2 * (tn * ( tau to_power 1))) - (2 * t2)) by Th2;

          then (((tn * (1 + s5)) - (tbn * (1 + s5))) + s5) = ((2 * (tn * ( tau to_power 1))) - (2 * (tbn * ( tau_bar to_power 1)))) by Th2;

          then (((tn * (1 + s5)) - (tbn * (1 + s5))) + s5) = ((2 * (tn * tau )) - (2 * (tbn * ( tau_bar to_power 1))));

          then (((tn - tbn) * (1 + s5)) + s5) = ((2 * (tn * tau )) - (2 * (tbn * tau_bar )));

          then (((tn * ((1 + s5) - (2 * tau ))) + (tbn * ((2 * tau_bar ) - (1 + s5)))) + s5) = 0 ;

          then ((( - (2 * tbn)) + 1) * ( sqrt 5)) = 0 by FIB_NUM:def 1, FIB_NUM:def 2;

          then (( - (2 * tbn)) + 1) = 0 by A4;

          hence contradiction by Th8, A1;

        end;

        hence thesis by A3, XXREAL_0: 1;

      end;

      hence thesis by A2, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:26

    for n be Nat holds ( Fib (n + 1)) = ((( Fib n) + ( sqrt ((5 * (( Fib n) ^2 )) + (4 * (( - 1) to_power n))))) / 2)

    proof

      let n be Nat;



       A1: (n - 0 ) is Element of NAT by NAT_1: 21;



       A2: (2 * ( Fib (n + 1))) = (( Fib n) + ( Lucas n)) by FIB_NUM3: 24;



       A3: ((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) = ((( Lucas n) to_power 2) - (5 * (( Fib n) ^2 ))) by POWER: 46

      .= ((( Lucas n) to_power 2) - (5 * (( Fib n) to_power 2))) by POWER: 46

      .= ( - ((5 * (( Fib n) |^ 2)) - (( Lucas n) |^ 2)))

      .= ( - (4 * (( - 1) to_power (n + 1)))) by A1, FIB_NUM3: 30

      .= (( - 1) * ((( - 1) to_power (n + 1)) * 4))

      .= ((( - 1) to_power 1) * ((( - 1) to_power (n + 1)) * 4))

      .= (((( - 1) to_power 1) * (( - 1) to_power (n + 1))) * 4)

      .= ((( - 1) to_power ((n + 1) + 1)) * 4) by Th2

      .= ((( - 1) to_power (n + 2)) * 4)

      .= (((( - 1) to_power n) * (( - 1) to_power 2)) * 4) by Th2

      .= (((( - 1) to_power n) * 1) * 4) by FIB_NUM2: 3, POLYFORM: 5;

      ( Fib (n + 1)) = ((( Fib n) + ( Lucas n)) / 2) by A2;

      hence thesis by A3, SQUARE_1:def 2;

    end;

    theorem :: FIB_NUM4:27

    for n be Nat st n >= 2 holds ( Fib (n + 1)) = [\(((( Fib n) + 1) + ( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1))) / 2)/]

    proof

      let n be Nat;

      assume

       A1: n >= 2;



       A2: (n - 0 ) is Element of NAT by NAT_1: 21;



       A3: (n - 1) >= (2 - 1) by A1, XREAL_1: 9;

      (((n + 1) -' 1) + 1) = (((n + 1) - 1) + 1) by NAT_D: 37

      .= (((n - 1) + 1) + 1)

      .= (((n -' 1) + 1) + 1) by A3, NAT_D: 39;



      then

       A4: ( Fib (n + 1)) = ( Fib (((n -' 1) + 1) + 1)) by NAT_D: 34

      .= (( Fib (n -' 1)) + ( Fib ((n -' 1) + 1))) by PRE_FF: 1

      .= (( Fib (n -' 1)) + ( Fib ((n + 1) -' 1))) by A1, NAT_D: 38, XXREAL_0: 2

      .= (( Fib (n -' 1)) + ( Fib n)) by NAT_D: 34;

      (n + 2) >= (2 + 2) by A1, XREAL_1: 6;

      then

      reconsider p = ((n + 2) - 1) as Nat by NAT_1: 21, XXREAL_0: 2;



       A5: (( Lucas n) - ( Fib n)) = (( Lucas ((n + 1) -' 1)) - ( Fib n)) by NAT_D: 34

      .= (( Lucas ((n -' 1) + 1)) - ( Fib n)) by A1, NAT_D: 38, XXREAL_0: 2

      .= ((( Fib (n -' 1)) + ( Fib ((n -' 1) + 2))) - ( Fib n)) by FIB_NUM3: 20

      .= ((( Fib (n -' 1)) + ( Fib ((n + 2) -' 1))) - ( Fib n)) by A1, NAT_D: 38, XXREAL_0: 2

      .= ((( Fib (n -' 1)) + ( Fib p)) - ( Fib n)) by NAT_D: 37

      .= (2 * ( Fib (n -' 1))) by A4;



       A6: ((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) = ((( Lucas n) ^2 ) - (5 * (( Fib n) to_power 2))) by POWER: 46

      .= ((( Lucas n) to_power 2) - (5 * (( Fib n) |^ 2))) by POWER: 46

      .= (( - 1) * ((5 * (( Fib n) |^ 2)) - (( Lucas n) |^ 2)))

      .= (( - 1) * (4 * (( - 1) to_power (n + 1)))) by A2, FIB_NUM3: 30

      .= (4 * (( - 1) * (( - 1) to_power (n + 1))))

      .= (4 * ((( - 1) to_power 1) * (( - 1) to_power (n + 1))))

      .= (4 * (( - 1) to_power (1 + (n + 1)))) by Th2

      .= (4 * (( - 1) to_power (n + 2)))

      .= (4 * ((( - 1) to_power n) * (( - 1) to_power 2))) by Th2

      .= (4 * ((( - 1) to_power n) * (( - 1) ^2 ))) by POWER: 46

      .= (4 * (( - 1) to_power n));

      (n -' 1) >= (2 -' 1) & (2 - 1) >= 1 by A1, NAT_D: 42;

      then (n -' 1) >= (2 - 1) by NAT_D: 39;

      then

       A7: ( Fib (n -' 1)) >= 1 by FIB_NUM2: 45, PRE_FF: 1;

      1 >= (( - 1) to_power n)

      proof

        per cases ;

          suppose n is even;

          hence thesis by FIB_NUM2: 3;

        end;

          suppose n is odd;

          hence thesis by FIB_NUM2: 2;

        end;

      end;

      then (( - 1) to_power n) <= ( Fib (n -' 1)) by A7, XXREAL_0: 2;

      then ((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) <= ((2 * 2) * ( Fib (n -' 1))) by A6, XREAL_1: 64;

      then (((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) - (2 * ( Lucas n))) <= (((2 * ( Lucas n)) - (2 * ( Fib n))) - (2 * ( Lucas n))) by A5, XREAL_1: 9;

      then ((((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) - (2 * ( Lucas n))) + 1) <= (( - (2 * ( Fib n))) + 1) by XREAL_1: 6;

      then

       A8: (((((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) - (2 * ( Lucas n))) + 1) + (5 * (( Fib n) ^2 ))) <= ((( - (2 * ( Fib n))) + 1) + (5 * (( Fib n) ^2 ))) by XREAL_1: 6;



       A9: ((n + 2) -' 1) = ((n + 2) - 1) by NAT_D: 37

      .= (n + 1);



       A10: ( Lucas n) = ( Lucas ((n + 1) -' 1)) by NAT_D: 34

      .= ( Lucas ((n -' 1) + 1)) by A1, NAT_D: 38, XXREAL_0: 2

      .= (( Fib (n -' 1)) + ( Fib ((n -' 1) + 2))) by FIB_NUM3: 20

      .= (( Fib (n -' 1)) + ( Fib ((n + 2) -' 1))) by A1, NAT_D: 38, XXREAL_0: 2

      .= ((2 * ( Fib (n + 1))) - ( Fib n)) by A4, A9;



       A11: (2 * ( Fib (n -' 1))) >= (2 * 0 );

      n >= 1 by A1, XXREAL_0: 2;

      then

       A12: ( Fib n) >= 1 by FIB_NUM2: 45, PRE_FF: 1;

      then ( - ( Fib n)) <= ( - 1) by XREAL_1: 24;

      then (( - ( Fib n)) + 1) <= (( - 1) + 1) by XREAL_1: 6;

      then ((2 * ( Fib (n -' 1))) + ( Fib n)) >= ((( - ( Fib n)) + 1) + ( Fib n)) by A11, XREAL_1: 6;

      then

       A13: (((2 * ( Fib (n -' 1))) + ( Fib n)) - 1) >= (1 - 1) by XREAL_1: 9;

      ( sqrt ((((2 * ( Fib (n + 1))) - ( Fib n)) - 1) ^2 )) <= ( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1)) by A10, A8, SQUARE_1: 26;

      then (((2 * ( Fib (n + 1))) - ( Fib n)) - 1) <= ( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1)) by A4, A13, SQUARE_1: 22;

      then ((((2 * ( Fib (n + 1))) - ( Fib n)) - 1) + ( Fib n)) <= (( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1)) + ( Fib n)) by XREAL_1: 6;

      then (((((2 * ( Fib (n + 1))) - ( Fib n)) - 1) + ( Fib n)) + 1) <= ((( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1)) + ( Fib n)) + 1) by XREAL_1: 6;

      then

       A14: ((2 * ( Fib (n + 1))) / 2) <= (((( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1)) + ( Fib n)) + 1) / 2) by XREAL_1: 72;



       A15: ((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) = (((5 * ( Fib n)) - 2) * ( Fib n));

      (5 * ( Fib n)) >= (5 * 1) by A12, XREAL_1: 64;

      then ((5 * ( Fib n)) - 2) >= (5 - 2) by XREAL_1: 9;

      then

       A16: ((5 * ( Fib n)) - 2) >= 0 by XXREAL_0: 2;



       A17: (((( Fib (n + 1)) + ( Fib (n + 1))) - ( Fib n)) + 1) = ((( Fib (n + 1)) + ( Fib (n -' 1))) + 1) by A4;

      ((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) > ( - (2 * (( Lucas n) + ( Fib n))))

      proof



         A18: ( Fib n) > 0 by A1, FIB_NUM2: 21, FIB_NUM2: 45;

        ( Lucas n) >= n by FIB_NUM3: 17;

        then ( Lucas n) >= 2 by A1, XXREAL_0: 2;

        then (( Lucas n) + ( Fib n)) > ( 0 + 2) by A18, XREAL_1: 8;

        then ((( Lucas n) + ( Fib n)) * 2) > (2 * 2) by XREAL_1: 68;

        then

         A19: ( - ((( Lucas n) + ( Fib n)) * 2)) < ( - 4) by XREAL_1: 24;

        ( - 4) <= (4 * (( - 1) to_power n)) by Lm1;

        hence thesis by A6, A19, XXREAL_0: 2;

      end;

      then (((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) + (2 * ( Lucas n))) > (( - (2 * (( Lucas n) + ( Fib n)))) + (2 * ( Lucas n))) by XREAL_1: 6;

      then ((((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) + (2 * ( Lucas n))) + (5 * (( Fib n) ^2 ))) > (( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) by XREAL_1: 6;

      then (((( Lucas n) ^2 ) + ((2 * ( Lucas n)) * 1)) + (1 ^2 )) > ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + (1 ^2 )) by XREAL_1: 6;

      then ( sqrt ((((2 * ( Fib (n + 1))) - ( Fib n)) + 1) ^2 )) > ( sqrt ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + 1)) by A16, A15, A10, SQUARE_1: 27;

      then (((2 * ( Fib (n + 1))) - ( Fib n)) + 1) > ( sqrt ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + 1)) by A17, SQUARE_1: 22;

      then ((((2 * ( Fib (n + 1))) - ( Fib n)) + 1) - 1) > (( sqrt ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + 1)) - 1) by XREAL_1: 9;

      then (((2 * ( Fib (n + 1))) - ( Fib n)) + ( Fib n)) > ((( sqrt ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + 1)) - 1) + ( Fib n)) by XREAL_1: 6;

      then ((2 * ( Fib (n + 1))) / 2) > (((( sqrt ((( - (2 * ( Fib n))) + (5 * (( Fib n) ^2 ))) + 1)) - 1) + ( Fib n)) / 2) by XREAL_1: 74;

      then ((((( Fib n) + 1) + ( sqrt (((5 * (( Fib n) ^2 )) - (2 * ( Fib n))) + 1))) / 2) - 1) < ( Fib (n + 1));

      hence thesis by A14, INT_1:def 6;

    end;



     Lm20: ( sqrt 5) > 0 by SQUARE_1: 25;



     Lm21: (( sqrt 5) / ((( sqrt 5) - 5) * tau )) = (( sqrt 5) / ((( sqrt 5) - (( sqrt 5) ^2 )) * tau )) by SQUARE_1:def 2

    .= (( sqrt 5) / (( sqrt 5) * ((1 - ( sqrt 5)) * tau )))

    .= ((( sqrt 5) / ( sqrt 5)) / ((1 - ( sqrt 5)) * tau )) by XCMPLX_1: 78

    .= (1 / (((1 - ( sqrt 5)) * (1 + ( sqrt 5))) / 2)) by Lm20, FIB_NUM:def 1, XCMPLX_1: 60

    .= ((1 * 2) / ((1 - ( sqrt 5)) * (1 + ( sqrt 5)))) by XCMPLX_1: 77

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

    .= (2 / ((1 ^2 ) - 5)) by SQUARE_1:def 2

    .= ( - (1 / 2));

    theorem :: FIB_NUM4:28

    for n be Nat st n >= 2 holds ( Fib n) = [\((1 / tau ) * (( Fib (n + 1)) + (1 / 2)))/]

    proof

      let n be Nat;

      assume

       A1: n >= 2;

      then

       A2: n > 1 by XXREAL_0: 2;

      set tbn = ( tau_bar to_power n);

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

      then ( sqrt 5) < 5 by SQUARE_1:def 2;

      then

       A3: (( sqrt 5) - 5) < (5 - 5) by XREAL_1: 9;



       A4: ((1 / tau ) * (( Fib (n + 1)) + (1 / 2))) >= ( Fib n)

      proof

        set tbm = ( tau_bar to_power (n + 1));

        set tn = ( tau to_power n);

        ((tbm / tau ) - (( sqrt 5) / (2 * tau ))) <= tbn

        proof

          per cases ;

            suppose

             A5: n is even;

            (( sqrt 5) / ((( sqrt 5) - 5) * tau )) <= tbn by Lm21, A2, Th14;

            then ((( sqrt 5) / ((( sqrt 5) - 5) * tau )) * ((( sqrt 5) - 5) * tau )) >= (tbn * ((( sqrt 5) - 5) * tau )) by A3, XREAL_1: 65;

            then

             A6: ( sqrt 5) >= (tbn * ((( sqrt 5) - 5) * tau )) by A3, XCMPLX_1: 87;



             A7: tbn > 0 by Th6, A5;

            then (( sqrt 5) / tbn) >= ((( tau * (( sqrt 5) - 5)) * tbn) / tbn) by A6, XREAL_1: 72;

            then (( sqrt 5) / tbn) >= ( tau * (( sqrt 5) - 5)) by A7, XCMPLX_1: 89;

            then ((( sqrt 5) / tbn) / tau ) >= (((( sqrt 5) - 5) * tau ) / tau ) by XREAL_1: 72;

            then ((( sqrt 5) / tbn) / tau ) >= (( sqrt 5) - 5) by XCMPLX_1: 89;

            then (( sqrt 5) / (tbn * tau )) >= (( sqrt 5) - 5) by XCMPLX_1: 78;

            then ((( sqrt 5) / (tbn * tau )) + (( - ( sqrt 5)) + 5)) >= ((( sqrt 5) - 5) + (( - ( sqrt 5)) + 5)) by XREAL_1: 6;

            then ( - (((( sqrt 5) / (tbn * tau )) - ( sqrt 5)) + 5)) <= 0 ;

            then (((( - (( sqrt 5) / (tbn * tau ))) + ( sqrt 5)) - 5) + 2) <= ( 0 + 2) by XREAL_1: 6;

            then ((( - (( sqrt 5) / (tbn * tau ))) + (( sqrt 5) - 3)) / 2) <= (2 / 2) by XREAL_1: 72;

            then (( - ((( sqrt 5) / (tbn * tau )) / 2)) + ( tau_bar / tau )) <= 1 by Lm4;

            then (( - (( sqrt 5) / ((tbn * tau ) * 2))) + ( tau_bar / tau )) <= 1 by XCMPLX_1: 78;

            then ((( tau_bar / tau ) - (( sqrt 5) / ((2 * tbn) * tau ))) * tbn) <= (1 * tbn) by A7, XREAL_1: 64;

            then ((( tau_bar / tau ) * tbn) - ((( sqrt 5) / ((2 * tbn) * tau )) * tbn)) <= tbn;

            then ((( tau_bar * tbn) / tau ) - ((( sqrt 5) / ((2 * tbn) * tau )) * tbn)) <= tbn by XCMPLX_1: 74;

            then (((( tau_bar to_power 1) * tbn) / tau ) - ((( sqrt 5) / ((2 * tbn) * tau )) * tbn)) <= tbn;

            then ((( tau_bar to_power (n + 1)) / tau ) - ((( sqrt 5) / ((2 * tau ) * tbn)) * tbn)) <= tbn by Th2;

            then ((( tau_bar to_power (n + 1)) / tau ) - (((( sqrt 5) / (2 * tau )) / tbn) * tbn)) <= tbn by XCMPLX_1: 78;

            hence thesis by A7, XCMPLX_1: 87;

          end;

            suppose n is odd;

            then

             A8: tbn < 0 by Th7;

            (( sqrt 5) / ( tau * (( sqrt 5) - 5))) <= tbn by Lm21, A2, Th14;

            then ((( sqrt 5) / ( tau * (( sqrt 5) - 5))) * (( sqrt 5) - 5)) >= (tbn * (( sqrt 5) - 5)) by A3, XREAL_1: 65;

            then (((( sqrt 5) / tau ) / (( sqrt 5) - 5)) * (( sqrt 5) - 5)) >= (tbn * (( sqrt 5) - 5)) by XCMPLX_1: 78;

            then (( sqrt 5) / tau ) >= (tbn * (( sqrt 5) - 5)) by A3, XCMPLX_1: 87;

            then ((( sqrt 5) / tau ) / tbn) <= ((tbn * (( sqrt 5) - 5)) / tbn) by A8, XREAL_1: 73;

            then (( sqrt 5) / ( tau * tbn)) <= ((tbn * (( sqrt 5) - 5)) / tbn) by XCMPLX_1: 78;

            then (( sqrt 5) / ( tau * tbn)) <= (( sqrt 5) - 5) by A8, XCMPLX_1: 89;

            then ( - (( sqrt 5) / ( tau * tbn))) >= ( - (( sqrt 5) - 5)) by XREAL_1: 24;

            then (( - (( sqrt 5) / ( tau * tbn))) + (( sqrt 5) - 3)) >= ((( - ( sqrt 5)) + 5) + (( sqrt 5) - 3)) by XREAL_1: 6;

            then ((( - (( sqrt 5) / ( tau * tbn))) + (( sqrt 5) - 3)) / 2) >= (2 / 2) by XREAL_1: 72;

            then (( tau_bar / tau ) - ((( sqrt 5) / ( tau * tbn)) / 2)) >= 1 by Lm4;

            then (( tau_bar / tau ) - (( sqrt 5) / (( tau * tbn) * 2))) >= 1 by XCMPLX_1: 78;

            then ((( tau_bar / tau ) - (( sqrt 5) / (( tau * tbn) * 2))) * tbn) <= (1 * tbn) by A8, XREAL_1: 65;

            then ((( tau_bar / tau ) * tbn) - ((( sqrt 5) / (( tau * 2) * tbn)) * tbn)) <= tbn;

            then ((( tau_bar / tau ) * tbn) - (((( sqrt 5) / ( tau * 2)) / tbn) * tbn)) <= tbn by XCMPLX_1: 78;

            then ((( tau_bar / tau ) * tbn) - (( sqrt 5) / ( tau * 2))) <= tbn by A8, XCMPLX_1: 87;

            then ((( tau_bar * tbn) / tau ) - (( sqrt 5) / ( tau * 2))) <= tbn by XCMPLX_1: 74;

            then (((( tau_bar to_power 1) * tbn) / tau ) - (( sqrt 5) / ( tau * 2))) <= tbn;

            hence thesis by Th2;

          end;

        end;

        then ( - ((tbm / tau ) - (( sqrt 5) / (2 * tau )))) >= ( - tbn) by XREAL_1: 24;

        then ((( - (tbm / tau )) + (( sqrt 5) / (2 * tau ))) + ((tn * tau ) / tau )) >= (( - tbn) + ((tn * tau ) / tau )) by XREAL_1: 6;

        then ((((tn * tau ) / tau ) - (tbm / tau )) + (( sqrt 5) / (2 * tau ))) >= (( - tbn) + ((tn * tau ) / tau ));

        then ((((tn * tau ) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) >= (( - tbn) + ((tn * tau ) / tau )) by XCMPLX_1: 120;

        then ((((tn * tau ) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) >= (( - tbn) + tn) by XCMPLX_1: 89;

        then ((((tn * ( tau to_power 1)) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) >= (tn - tbn);

        then (((( tau to_power (n + 1)) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) >= (tn - tbn) by Th2;

        then ((((( tau to_power (n + 1)) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) / ( sqrt 5)) >= ((tn - tbn) / ( sqrt 5)) by Lm20, XREAL_1: 72;

        then ((((( tau to_power (n + 1)) - tbm) / tau ) + (( sqrt 5) / (2 * tau ))) / ( sqrt 5)) >= ( Fib n) by FIB_NUM: 7;

        then ((((( tau to_power (n + 1)) - tbm) / tau ) / ( sqrt 5)) + ((( sqrt 5) / (2 * tau )) / ( sqrt 5))) >= ( Fib n) by XCMPLX_1: 62;

        then ((((( tau to_power (n + 1)) - tbm) / ( sqrt 5)) / tau ) + ((( sqrt 5) / (2 * tau )) / ( sqrt 5))) >= ( Fib n) by XCMPLX_1: 48;

        then ((( Fib (n + 1)) / tau ) + ((( sqrt 5) / (2 * tau )) / ( sqrt 5))) >= ( Fib n) by FIB_NUM: 7;

        then ((( Fib (n + 1)) / tau ) + ((1 / (2 * tau )) * (( sqrt 5) / ( sqrt 5)))) >= ( Fib n) by XCMPLX_1: 104;

        then ((( Fib (n + 1)) / tau ) + ((1 / (2 * tau )) * 1)) >= ( Fib n) by Lm20, XCMPLX_1: 60;

        then ((( Fib (n + 1)) / tau ) + ((1 / 2) / tau )) >= ( Fib n) by XCMPLX_1: 78;

        then ((( Fib (n + 1)) + (1 / 2)) / tau ) >= ( Fib n) by XCMPLX_1: 62;

        hence thesis by XCMPLX_1: 99;

      end;

      (((1 / tau ) * (( Fib (n + 1)) + (1 / 2))) - 1) < ( Fib n)

      proof

        1 < ( sqrt 5) by SQUARE_1: 18, SQUARE_1: 27;

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

        then tbn < (( sqrt 5) / 2) by Th8, A1, XXREAL_0: 2;

        then (tbn * ( sqrt 5)) < (( tau - (1 / 2)) * ( sqrt 5)) by Lm20, FIB_NUM:def 1, XREAL_1: 68;

        then ((tbn * tau ) - (tbn * tau_bar )) < (( tau * ( sqrt 5)) - ((1 * ( sqrt 5)) / 2)) by FIB_NUM:def 1, FIB_NUM:def 2;

        then ((tbn * tau ) - (tbn * ( tau_bar to_power 1))) < (( tau * ( sqrt 5)) - (( sqrt 5) / 2));

        then ((tbn * tau ) - ( tau_bar to_power (n + 1))) < (( tau * ( sqrt 5)) - (( sqrt 5) / 2)) by Th2;

        then (((tbn * tau ) - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) < ((( tau * ( sqrt 5)) - (( sqrt 5) / 2)) + (( sqrt 5) / 2)) by XREAL_1: 6;

        then ((((tbn * tau ) - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) - (tbn * tau )) < (( tau * ( sqrt 5)) - (tbn * tau )) by XREAL_1: 9;

        then ((( - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) - ( tau * ( sqrt 5))) < ((( tau * ( sqrt 5)) - (tbn * tau )) - ( tau * ( sqrt 5))) by XREAL_1: 9;

        then (((( - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) - ( tau * ( sqrt 5))) / tau ) < (( - (tbn * tau )) / tau ) by XREAL_1: 74;

        then (((( - ( tau_bar to_power (n + 1))) / tau ) + ((( sqrt 5) / 2) / tau )) - (( tau * ( sqrt 5)) / tau )) < (( - (tbn * tau )) / tau ) by XCMPLX_1: 124;

        then ((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - (( tau * ( sqrt 5)) / tau )) < ((( - tbn) * tau ) / tau ) by XCMPLX_1: 187;

        then ((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - (( tau * ( sqrt 5)) / tau )) < ( - tbn) by XCMPLX_1: 89;

        then ((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - ( sqrt 5)) < ( - tbn) by XCMPLX_1: 89;

        then (((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - ( sqrt 5)) + (( tau to_power n) * 1)) < (( - tbn) + ( tau to_power n)) by XREAL_1: 6;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - ( sqrt 5)) + (( tau to_power n) * 1)) / ( sqrt 5)) < ((( tau to_power n) - tbn) / ( sqrt 5)) by Lm20, XREAL_1: 74;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - ( sqrt 5)) + (( tau to_power n) * 1)) / ( sqrt 5)) < ( Fib n) by FIB_NUM: 7;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) - ( sqrt 5)) + (( tau to_power n) * ( tau / tau ))) / ( sqrt 5)) < ( Fib n) by XCMPLX_1: 60;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) + (( tau to_power n) * ( tau / tau ))) - ( sqrt 5)) / ( sqrt 5)) < ( Fib n);

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) + ((( tau to_power n) * tau ) / tau )) - ( sqrt 5)) / ( sqrt 5)) < ( Fib n) by XCMPLX_1: 74;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) + ((( tau to_power n) * tau ) / tau )) / ( sqrt 5)) - (( sqrt 5) / ( sqrt 5))) < ( Fib n) by XCMPLX_1: 120;

        then ((((( - (( tau_bar to_power (n + 1)) / tau )) + ((( sqrt 5) / 2) / tau )) + ((( tau to_power n) * tau ) / tau )) / ( sqrt 5)) - 1) < ( Fib n) by Lm20, XCMPLX_1: 60;

        then (((((( - ( tau_bar to_power (n + 1))) / tau ) + ((( sqrt 5) / 2) / tau )) + ((( tau to_power n) * tau ) / tau )) / ( sqrt 5)) - 1) < ( Fib n) by XCMPLX_1: 187;

        then (((((( - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) + (( tau to_power n) * tau )) / tau ) / ( sqrt 5)) - 1) < ( Fib n) by XCMPLX_1: 63;

        then (((((( - ( tau_bar to_power (n + 1))) + (( sqrt 5) / 2)) + (( tau to_power n) * tau )) / ( sqrt 5)) / tau ) - 1) < ( Fib n) by XCMPLX_1: 48;

        then (((((( - ( tau_bar to_power (n + 1))) + (( tau to_power n) * tau )) + (( sqrt 5) / 2)) / ( sqrt 5)) * (1 / tau )) - 1) < ( Fib n) by XCMPLX_1: 99;

        then (((((( - ( tau_bar to_power (n + 1))) + (( tau to_power n) * tau )) / ( sqrt 5)) + ((( sqrt 5) / 2) / ( sqrt 5))) * (1 / tau )) - 1) < ( Fib n) by XCMPLX_1: 62;

        then (((((( - ( tau_bar to_power (n + 1))) + (( tau to_power n) * ( tau to_power 1))) / ( sqrt 5)) + ((( sqrt 5) / 2) / ( sqrt 5))) * (1 / tau )) - 1) < ( Fib n);

        then (((((( - ( tau_bar to_power (n + 1))) + ( tau to_power (n + 1))) / ( sqrt 5)) + ((( sqrt 5) / 2) / ( sqrt 5))) * (1 / tau )) - 1) < ( Fib n) by Th2;

        then (((((( tau to_power (n + 1)) - ( tau_bar to_power (n + 1))) / ( sqrt 5)) + ((( sqrt 5) / 2) / ( sqrt 5))) * (1 / tau )) - 1) < ( Fib n);

        then (((( Fib (n + 1)) + ((( sqrt 5) / 2) / ( sqrt 5))) * (1 / tau )) - 1) < ( Fib n) by FIB_NUM: 7;

        then (((( Fib (n + 1)) + ((( sqrt 5) / ( sqrt 5)) / 2)) * (1 / tau )) - 1) < ( Fib n) by XCMPLX_1: 48;

        hence thesis by Lm20, XCMPLX_1: 60;

      end;

      hence thesis by A4, INT_1:def 6;

    end;



     Lm22: ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1: 27;

    then

     Lm23: (( sqrt 5) - 1) > (1 - 1) & ( sqrt 5) > 0 by XREAL_1: 9;

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

    then ( - ( sqrt 5)) < ( - 2) by XREAL_1: 24;

    then (( - ( sqrt 5)) + 5) < (( - 2) + 5) by XREAL_1: 6;

    then (( - ( sqrt 5)) + (( sqrt 5) ^2 )) < 3 by SQUARE_1:def 2;

    then ((( sqrt 5) * (( sqrt 5) - 1)) / 5) < (3 / 5) by XREAL_1: 74;

    then ((( sqrt 5) - 1) * (( sqrt 5) / 5)) < (6 / 10);

    then ((( sqrt 5) - 1) * (( sqrt 5) / (( sqrt 5) ^2 ))) < (6 / 10) by SQUARE_1:def 2;

    then ((( sqrt 5) - 1) * ((1 * ( sqrt 5)) / (( sqrt 5) * ( sqrt 5)))) < (6 / 10) & ( sqrt 5) > 0 by SQUARE_1: 25;

    then ((( sqrt 5) - 1) * (1 / ( sqrt 5))) < (6 / 10) by XCMPLX_1: 91;

    then

     Lm24: ((( sqrt 5) - 1) / ( sqrt 5)) < (6 / 10) by XCMPLX_1: 99;

    ( sqrt ((3 / 2) ^2 )) <= ( sqrt 5) by SQUARE_1: 26;

    then (3 / 2) <= ( sqrt 5) by SQUARE_1:def 2;

    then ((3 / 2) * 2) <= (( sqrt 5) * 2) by XREAL_1: 64;

    then

     Lm25: (3 / 4) <= ((2 * ( sqrt 5)) / (2 * 2)) by XREAL_1: 72;



     Lm26: (( sqrt 5) - 1) > (1 - 1) & ( sqrt 5) > 0 by Lm22, XREAL_1: 9;

    (( - 1) + ( sqrt 5)) < ( 0 + ( sqrt 5)) & ( sqrt 5) > 0 by SQUARE_1: 25, XREAL_1: 6;

    then ((( sqrt 5) - 1) / ( sqrt 5)) < (( sqrt 5) / ( sqrt 5)) & ( sqrt 5) > 0 by XREAL_1: 74;

    then

     Lm27: ((( sqrt 5) - 1) / ( sqrt 5)) < 1 by XCMPLX_1: 60;

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

    then ( sqrt 5) < 3 by SQUARE_1:def 2;

    then ( - ( sqrt 5)) > ( - 3) by XREAL_1: 24;

    then

     Lm28: (( - ( sqrt 5)) + 3) > (( - 3) + 3) by XREAL_1: 6;

    ( - ( sqrt 5)) < ( - 1) by Lm22, XREAL_1: 24;

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

    then

     Lm29: ((3 - ( sqrt 5)) / 2) < (2 / 2) by XREAL_1: 74;

    theorem :: FIB_NUM4:29

    for n,k be Nat st (n >= k & k > 1) or (k = 1 & n > k) holds [\((( tau to_power k) * ( Fib n)) + (1 / 2))/] = ( Fib (n + k))

    proof

      let n,k be Nat;

      set tb = tau_bar ;

      set tk = ( tau to_power k);

      set tbk = ( tau_bar to_power k);

      set ts = ( tau to_power (n + k));

      set tbs = ( tau_bar to_power (n + k));

      set tn = ( tau to_power n);

      set tbn = ( tau_bar to_power n);

      assume

       A1: (n >= k & k > 1) or (k = 1 & n > k);



       A2: (tk * ( Fib n)) = (tk * ((tn - tbn) / ( sqrt 5))) by FIB_NUM: 7

      .= ((tk * (tn - tbn)) / ( sqrt 5)) by XCMPLX_1: 74

      .= ((((tk * tn) - tbs) + (tbs - (tk * tbn))) / ( sqrt 5))

      .= (((ts - tbs) + (tbs - (tk * tbn))) / ( sqrt 5)) by Th2

      .= (((ts - tbs) / ( sqrt 5)) + ((tbs - (tk * tbn)) / ( sqrt 5))) by XCMPLX_1: 62

      .= (( Fib (n + k)) + ((tbs - (tk * tbn)) / ( sqrt 5))) by FIB_NUM: 7

      .= (( Fib (n + k)) + (((tbn * tbk) - (tk * tbn)) / ( sqrt 5))) by Th2

      .= (( Fib (n + k)) + ((( - tbn) * (tk - tbk)) / ( sqrt 5)))

      .= (( Fib (n + k)) + (( - tbn) * ((tk - tbk) / ( sqrt 5)))) by XCMPLX_1: 74

      .= (( Fib (n + k)) + (( - tbn) * ( Fib k))) by FIB_NUM: 7

      .= (( Fib (n + k)) - (tbn * ( Fib k)));



       A3: ((tk * ( Fib n)) + (1 / 2)) >= ( Fib (n + k))

      proof

        (tbn * ( Fib k)) <= (1 / 2)

        proof

          per cases ;

            suppose

             A4: n is even;

            consider m be Nat such that

             A5: n = (k + m) by A1, NAT_1: 10;



             A6: ( sqrt 5) > 0 by SQUARE_1: 25;

            set tbm = ( tau_bar to_power m);

            (tbm * ((( - 1) to_power k) - (tb to_power (2 * k)))) <= (( sqrt 5) / 2)

            proof

              per cases ;

                suppose

                 A7: k is even;

                (tb to_power (2 * k)) > 0 by Th6;

                then

                 A8: (( - (tb to_power (2 * k))) + 1) < ( 0 + 1) by XREAL_1: 6;

                (tb to_power (2 * k)) < 1 by Th8, A1, XXREAL_0: 2;

                then ( - (tb to_power (2 * k))) > ( - 1) by XREAL_1: 24;

                then

                 A9: (( - (tb to_power (2 * k))) + 1) > (( - 1) + 1) by XREAL_1: 6;

                m is even by A4, A5, A7;

                then

                 A10: tbm > 0 by Th6;

                tbm <= (( sqrt 5) / 2)

                proof



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

                  per cases ;

                    suppose

                     A12: m = 0 ;

                    (( sqrt 5) / 2) >= (2 / 2) by A11, XREAL_1: 72;

                    hence thesis by A12, POWER: 24;

                  end;

                    suppose

                     A13: m > 0 ;

                    ( sqrt 5) >= 1 by A11, XXREAL_0: 2;

                    then (( sqrt 5) / 2) >= (1 / 2) by XREAL_1: 72;

                    hence thesis by A13, Th8, XXREAL_0: 2;

                  end;

                end;

                then |.tbm.| <= (( sqrt 5) / 2) by A10, ABSVALUE:def 1;

                then

                 A14: ( |.tbm.| * (1 - (tb to_power (2 * k)))) <= ((( sqrt 5) / 2) * 1) by A8, A9, XREAL_1: 66;

                (tbm * (1 - (tb to_power (2 * k)))) <= ( |.tbm.| * (1 - (tb to_power (2 * k)))) by A9, ABSVALUE: 4, XREAL_1: 64;

                then (tbm * (1 - (tb to_power (2 * k)))) <= (( sqrt 5) / 2) by A14, XXREAL_0: 2;

                hence thesis by A7, FIB_NUM2: 3;

              end;

                suppose

                 A15: k is odd;

                then

                 A16: m is odd by A4, A5;

                m <> 0 by A15, A4, A5;

                then

                 A17: m >= 1 by NAT_1: 14;

                per cases by A17, XXREAL_0: 1;

                  suppose

                   A18: m = 1;

                  (tb * (( - 1) - (tb to_power (2 * k)))) <= (( sqrt 5) / 2)

                  proof



                     A19: (tb to_power (2 * k)) > 0 by Th6;

                    (tb to_power (2 * k)) < (1 / 2) by Th8, A1;

                    then ((tb to_power (2 * k)) + 1) < ((1 / 2) + 1) by XREAL_1: 6;

                    then (((( sqrt 5) - 1) / ( sqrt 5)) * (1 + (tb to_power (2 * k)))) < ((6 / 10) * (3 / 2)) by Lm23, Lm24, A19, XREAL_1: 98;

                    then (((( sqrt 5) - 1) / ( sqrt 5)) * (1 + (tb to_power (2 * k)))) < 1 & ( sqrt 5) > 0 by SQUARE_1: 25, XXREAL_0: 2;

                    then ((((( sqrt 5) - 1) / ( sqrt 5)) * (1 + (tb to_power (2 * k)))) * ( sqrt 5)) < (1 * ( sqrt 5)) by XREAL_1: 68;

                    then ((((( sqrt 5) - 1) * (1 / ( sqrt 5))) * (1 + (tb to_power (2 * k)))) * ( sqrt 5)) < ( sqrt 5) by XCMPLX_1: 99;

                    then (((( sqrt 5) - 1) * (1 + (tb to_power (2 * k)))) * (( sqrt 5) * (1 / ( sqrt 5)))) < ( sqrt 5);

                    then (((( sqrt 5) - 1) * (1 + (tb to_power (2 * k)))) * (( sqrt 5) / ( sqrt 5))) < (1 * ( sqrt 5)) & ( sqrt 5) > 0 by SQUARE_1: 25, XCMPLX_1: 99;

                    then (((( sqrt 5) - 1) * (1 + (tb to_power (2 * k)))) * 1) < ( sqrt 5) by XCMPLX_1: 60;

                    then (((1 - ( sqrt 5)) * (( - 1) - (tb to_power (2 * k)))) / 2) < (( sqrt 5) / 2) by XREAL_1: 74;

                    hence thesis by FIB_NUM:def 2;

                  end;

                  then (tbm * (( - 1) - (tb to_power (2 * k)))) <= (( sqrt 5) / 2) by A18;

                  hence thesis by A15, FIB_NUM2: 2;

                end;

                  suppose

                   A20: m > 1;



                   A21: tbm < 0 by A16, Th7;



                   A22: (tbm * (( - 1) - (tb to_power (2 * k)))) = ( - (tbm * (1 + (tb to_power (2 * k)))));



                   A23: (tb to_power (2 * k)) > 0 by Th6;

                  (tb to_power (2 * k)) <= (1 / 2) by A1, Th8;

                  then

                   A24: ((tb to_power (2 * k)) + 1) <= ((1 / 2) + 1) by XREAL_1: 6;

                  tbm > ( - (1 / 2)) by Th14, A20;

                  then ( - tbm) < ( - ( - (1 / 2))) by XREAL_1: 24;

                  then (( - tbm) * (1 + (tb to_power (2 * k)))) <= ((1 / 2) * (3 / 2)) by A21, A23, A24, XREAL_1: 66;

                  then ( - (tbm * (1 + (tb to_power (2 * k))))) <= (( sqrt 5) / 2) by Lm25, XXREAL_0: 2;

                  hence thesis by A15, A22, FIB_NUM2: 2;

                end;

              end;

            end;

            then (tbm * ((tk * tbk) - (tb to_power (k + k)))) <= (( sqrt 5) / 2) by Lm3, NEWTON: 7;

            then (tbm * ((tk * tbk) - (tbk * tbk))) <= (( sqrt 5) / 2) by Th2;

            then (((tbm * tbk) * (tk - tbk)) / ( sqrt 5)) <= ((( sqrt 5) / 2) / ( sqrt 5)) by A6, XREAL_1: 72;

            then ((tbm * tbk) * ((tk - tbk) / ( sqrt 5))) <= ((( sqrt 5) / 2) / ( sqrt 5)) by XCMPLX_1: 74;

            then ((tbm * tbk) * ( Fib k)) <= ((( sqrt 5) / 2) / ( sqrt 5)) by FIB_NUM: 7;

            then (tbn * ( Fib k)) <= ((( sqrt 5) / 2) / ( sqrt 5)) by A5, Th2;

            then (tbn * ( Fib k)) <= ((1 * ( sqrt 5)) / (2 * ( sqrt 5))) by XCMPLX_1: 78;

            hence thesis by A6, XCMPLX_1: 91;

          end;

            suppose n is odd;

            then tbn < 0 by Th7;

            hence thesis;

          end;

        end;

        then ( - (tbn * ( Fib k))) >= ( - (1 / 2)) by XREAL_1: 24;

        then (( - (tbn * ( Fib k))) + (1 / 2)) >= (( - (1 / 2)) + (1 / 2)) by XREAL_1: 6;

        then ((( - (tbn * ( Fib k))) + (1 / 2)) + ( Fib (n + k))) >= ( 0 + ( Fib (n + k))) by XREAL_1: 6;

        hence thesis by A2;

      end;

      (((tk * ( Fib n)) + (1 / 2)) - 1) < ( Fib (n + k))

      proof

        (tbn * ( Fib k)) > ( - (1 / 2))

        proof

          per cases ;

            suppose n is even;

            then tbn > 0 by Th6;

            hence thesis;

          end;

            suppose

             A25: n is odd;

            consider m be Nat such that

             A26: n = (k + m) by A1, NAT_1: 10;

            set tbm = ( tau_bar to_power m);

            per cases ;

              suppose

               A27: k is even;

              then

               A28: m is odd by A25, A26;

              then

               A29: tbm < 0 by Th7;



               A30: m >= 1 by A28, NAT_1: 14;

              per cases by A30, XXREAL_0: 1;

                suppose

                 A31: m = 1;

                (((3 - ( sqrt 5)) / 2) to_power k) < (1 to_power k) by Lm29, Lm28, A1, POWER: 37;

                then (((3 - ( sqrt 5)) / 2) to_power k) < 1;

                then ( - (((3 - ( sqrt 5)) / 2) to_power k)) > ( - 1) by XREAL_1: 24;

                then

                 A32: (( - (((3 - ( sqrt 5)) / 2) to_power k)) + 1) > (( - 1) + 1) by XREAL_1: 6;

                (((3 - ( sqrt 5)) / 2) to_power k) > 0 by Lm28, POWER: 34;

                then

                 A33: (( - (((3 - ( sqrt 5)) / 2) to_power k)) + 1) < ( 0 + 1) by XREAL_1: 6;



                 A34: (1 - (tb to_power (2 * k))) = ((( - 1) to_power k) - (tb to_power (2 * k))) by A27, FIB_NUM2: 3

                .= ((tk * tbk) - (tb to_power (k + k))) by Lm3, NEWTON: 7

                .= ((tk * tbk) - (tbk * tbk)) by Th2

                .= (tbk * (tk - tbk));

                (((( sqrt 5) - 1) / ( sqrt 5)) * (1 - (((3 - ( sqrt 5)) / 2) to_power k))) < (1 * 1) by Lm26, Lm27, A32, A33, XREAL_1: 98;

                then ( - (((( sqrt 5) - 1) / ( sqrt 5)) * (1 - (((3 - ( sqrt 5)) / 2) to_power k)))) > ( - 1) by XREAL_1: 24;

                then (( - ((( sqrt 5) - 1) / ( sqrt 5))) * (1 - (((3 - ( sqrt 5)) / 2) to_power k))) > ( - 1);

                then ((( - (( sqrt 5) - 1)) / ( sqrt 5)) * (1 - (((3 - ( sqrt 5)) / 2) to_power k))) > ( - 1) by XCMPLX_1: 187;

                then (((1 - ( sqrt 5)) / ( sqrt 5)) * (1 - (tb to_power (2 * k)))) > ( - 1) by Lm7, NEWTON: 9;

                then ((((1 - ( sqrt 5)) / ( sqrt 5)) * (1 - (tb to_power (2 * k)))) / 2) > (( - 1) / 2) by XREAL_1: 74;

                then (((1 - ( sqrt 5)) / ( sqrt 5)) * ((1 - (tb to_power (2 * k))) / 2)) > (( - 1) / 2);

                then (((1 - ( sqrt 5)) * (1 / ( sqrt 5))) * ((1 - (tb to_power (2 * k))) * (1 / 2))) > (( - 1) / 2) by XCMPLX_1: 99;

                then ((tb * (1 / ( sqrt 5))) * (1 - (tb to_power (2 * k)))) > ( - (1 / 2)) by FIB_NUM:def 2;

                then ((tb * (1 / ( sqrt 5))) * (tbk * (tk - tbk))) > ( - (1 / 2)) by A34;

                then ((tb * tbk) * ((tk - tbk) * (1 / ( sqrt 5)))) > ( - (1 / 2));

                then ((tb * tbk) * ((tk - tbk) / ( sqrt 5))) > ( - (1 / 2)) by XCMPLX_1: 99;

                then (((tb to_power 1) * tbk) * ((tk - tbk) / ( sqrt 5))) > ( - (1 / 2));

                then ((tb to_power (1 + k)) * ((tk - tbk) / ( sqrt 5))) > ( - (1 / 2)) by Th2;

                hence thesis by A31, A26, FIB_NUM: 7;

              end;

                suppose m > 1;

                then tbm > ( - (1 / 2)) by Th14;

                then

                 A35: ( - tbm) < ( - ( - (1 / 2))) by XREAL_1: 24;

                ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1: 27;

                then ( - ( sqrt 5)) < ( - 1) by XREAL_1: 24;

                then

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

                (tb to_power (2 * k)) > 0 & (tb to_power (2 * k)) < (1 / 2) by Th6, Th8, A1;

                then ( - (tb to_power (2 * k))) < 0 & ( - (tb to_power (2 * k))) > ( - (1 / 2)) by XREAL_1: 24;

                then (( - (tb to_power (2 * k))) + 1) < ( 0 + 1) & (( - (tb to_power (2 * k))) + 1) > (( - (1 / 2)) + 1) by XREAL_1: 6;

                then (( - tbm) * (1 - (tb to_power (2 * k)))) < ((1 / 2) * 1) by A35, A29, XREAL_1: 98;

                then ( - ( - (tbm * (1 - (tb to_power (2 * k)))))) > ( - (1 / 2)) by XREAL_1: 24;

                then (tbm * ((( - 1) to_power k) - (tb to_power (2 * k)))) > ( - (1 / 2)) by A27, FIB_NUM2: 3;

                then (tbm * ((( - 1) to_power k) - (tb to_power (2 * k)))) > ( - (( sqrt 5) / 2)) by A36, XXREAL_0: 2;

                then (tbm * ((tk * tbk) - (tb to_power (k + k)))) > ( - (( sqrt 5) / 2)) by Lm3, NEWTON: 7;

                then (tbm * ((tk * tbk) - (tbk * tbk))) > ( - (( sqrt 5) / 2)) by Th2;

                then ((tbm * tbk) * (tk - tbk)) > ( - (( sqrt 5) / 2));

                then (tbn * (tk - tbk)) > ( - (( sqrt 5) / 2)) & ( sqrt 5) > 0 by Th2, A26, SQUARE_1: 25;

                then ((tbn * (tk - tbk)) / ( sqrt 5)) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XREAL_1: 74;

                then (tbn * ((tk - tbk) / ( sqrt 5))) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XCMPLX_1: 74;

                then (tbn * ( Fib k)) > ((( - ( sqrt 5)) / 2) / ( sqrt 5)) by FIB_NUM: 7;

                then (tbn * ( Fib k)) > ((( - 1) * ( sqrt 5)) / (2 * ( sqrt 5))) & ( sqrt 5) > 0 by SQUARE_1: 25, XCMPLX_1: 78;

                then (tbn * ( Fib k)) > (( - 1) / 2) by XCMPLX_1: 91;

                hence thesis;

              end;

            end;

              suppose

               A37: k is odd;

              then

               A38: m is even by A25, A26;

              per cases ;

                suppose

                 A39: m = 0 ;

                per cases by A1;

                  suppose k = 1;

                  hence thesis by A1, A39, A26;

                end;

                  suppose k > 1;

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

                  then k = 2 or k > 2 by XXREAL_0: 1;

                  then (k + 1) > (2 + 1) by A37, POLYFORM: 5, XREAL_1: 6;

                  then k >= 3 by NAT_1: 13;

                  then (k * 2) >= (3 * 2) by XREAL_1: 64;

                  then (tb to_power (k * 2)) <= (tb to_power (3 * 2)) by Th11;

                  then

                   A40: ((tb to_power (2 * k)) + 1) <= ((9 - (4 * ( sqrt 5))) + 1) by Lm9, XREAL_1: 6;

                  ( sqrt ((20 / 9) ^2 )) < ( sqrt 5) by SQUARE_1: 27;

                  then (20 / 9) < ( sqrt 5) by SQUARE_1:def 2;

                  then ((20 / 9) * 9) < (9 * ( sqrt 5)) by XREAL_1: 68;

                  then (20 - (8 * ( sqrt 5))) < ((( sqrt 5) + (8 * ( sqrt 5))) - (8 * ( sqrt 5))) by XREAL_1: 9;

                  then ((20 - (8 * ( sqrt 5))) / 2) < (( sqrt 5) / 2) by XREAL_1: 74;

                  then ((tb to_power (2 * k)) + 1) < (( sqrt 5) / 2) by A40, XXREAL_0: 2;

                  then ( - ((tb to_power (2 * k)) + 1)) > ( - (( sqrt 5) / 2)) by XREAL_1: 24;

                  then (( - (tb to_power (2 * k))) + ( - 1)) > ( - (( sqrt 5) / 2));

                  then (( - (tb to_power (2 * k))) + (( - 1) to_power k)) > ( - (( sqrt 5) / 2)) by A37, FIB_NUM2: 2;

                  then (( - (tb to_power (k + k))) + (tk * tbk)) > ( - (( sqrt 5) / 2)) by Lm3, NEWTON: 7;

                  then (( - (tbk * tbk)) + (tk * tbk)) > ( - (( sqrt 5) / 2)) by Th2;

                  then (tbk * (( - tbk) + tk)) > ( - (( sqrt 5) / 2)) & ( sqrt 5) > 0 by SQUARE_1: 25;

                  then ((tbk * (( - tbk) + tk)) / ( sqrt 5)) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XREAL_1: 74;

                  then (tbk * ((tk - tbk) / ( sqrt 5))) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XCMPLX_1: 74;

                  then (tbk * ( Fib k)) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by FIB_NUM: 7;

                  then (tbk * ( Fib k)) > ( - ((( sqrt 5) / 2) / ( sqrt 5))) by XCMPLX_1: 187;

                  then (tbk * ( Fib k)) > ( - ((( sqrt 5) / ( sqrt 5)) / 2)) & ( sqrt 5) > 0 by SQUARE_1: 25, XCMPLX_1: 48;

                  hence thesis by A39, A26, XCMPLX_1: 60;

                end;

              end;

                suppose m > 0 ;

                then

                 A41: tbm > 0 & tbm < (1 / 2) by A38, Th6, Th8;

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

                then (3 / 2) < ( sqrt 5) by SQUARE_1:def 2;

                then ((3 / 2) * 2) < (( sqrt 5) * 2) by XREAL_1: 68;

                then

                 A42: (3 / (2 * 2)) < ((2 * ( sqrt 5)) / (2 * 2)) by XREAL_1: 74;



                 A43: (tb to_power (2 * k)) < (1 / 2) & (tb to_power (2 * k)) > 0 by Th8, A1, Th6;

                then ((tb to_power (2 * k)) + 1) < ((1 / 2) + 1) by XREAL_1: 6;

                then (tbm * ((tb to_power (2 * k)) + 1)) < ((1 / 2) * ((1 / 2) + 1)) by A41, A43, XREAL_1: 96;

                then (tbm * ((tb to_power (2 * k)) + 1)) < (( sqrt 5) / 2) by A42, XXREAL_0: 2;

                then ( - (tbm * ((tb to_power (2 * k)) + 1))) > ( - (( sqrt 5) / 2)) by XREAL_1: 24;

                then (tbm * (( - (tb to_power (2 * k))) + ( - 1))) > ( - (( sqrt 5) / 2));

                then (tbm * (( - (tb to_power (2 * k))) + (( - 1) to_power k))) > ( - (( sqrt 5) / 2)) by A37, FIB_NUM2: 2;

                then (tbm * (( - (tb to_power (k + k))) + (tk * tbk))) > ( - (( sqrt 5) / 2)) by Lm3, NEWTON: 7;

                then (tbm * (( - (tbk * tbk)) + (tk * tbk))) > ( - (( sqrt 5) / 2)) by Th2;

                then ((tbm * tbk) * (tk - tbk)) > ( - (( sqrt 5) / 2));

                then (tbn * (tk - tbk)) > ( - (( sqrt 5) / 2)) & ( sqrt 5) > 0 by A26, Th2, SQUARE_1: 25;

                then ((tbn * (tk - tbk)) / ( sqrt 5)) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XREAL_1: 74;

                then (tbn * ((tk - tbk) / ( sqrt 5))) > (( - (( sqrt 5) / 2)) / ( sqrt 5)) by XCMPLX_1: 74;

                then (tbn * ( Fib k)) > ((( - ( sqrt 5)) / 2) / ( sqrt 5)) by FIB_NUM: 7;

                then (tbn * ( Fib k)) > ((( - 1) * ( sqrt 5)) / (2 * ( sqrt 5))) & ( sqrt 5) > 0 by SQUARE_1: 25, XCMPLX_1: 78;

                then (tbn * ( Fib k)) > (( - 1) / 2) by XCMPLX_1: 91;

                hence thesis;

              end;

            end;

          end;

        end;

        then ( - (tbn * ( Fib k))) < ( - ( - (1 / 2))) by XREAL_1: 24;

        then (( - (tbn * ( Fib k))) + (1 / 2)) < ((1 / 2) + (1 / 2)) by XREAL_1: 6;

        then ((( - (tbn * ( Fib k))) + (1 / 2)) - 1) < (1 - 1) by XREAL_1: 9;

        then (((( - (tbn * ( Fib k))) + (1 / 2)) - 1) + ( Fib (n + k))) < ( 0 + ( Fib (n + k))) by XREAL_1: 6;

        hence thesis by A2;

      end;

      hence thesis by A3, INT_1:def 6;

    end;

    begin

    theorem :: FIB_NUM4:30

    for n be Nat st n >= 2 holds ( Lucas n) = [\(( tau to_power n) + (1 / 2))/]

    proof

      let n be Nat;

      assume

       A1: n >= 2;

      then (1 / 2) >= ( tau_bar to_power n) by Th8;

      then (( tau to_power n) + (1 / 2)) >= (( tau to_power n) + ( tau_bar to_power n)) by XREAL_1: 6;

      then

       A2: (( tau to_power n) + (1 / 2)) >= ( Lucas n) by FIB_NUM3: 21;

      n > 1 by A1, XXREAL_0: 2;

      then ((1 / 2) - 1) < ( tau_bar to_power n) by Th14;

      then (( tau to_power n) + ((1 / 2) - 1)) < (( tau to_power n) + ( tau_bar to_power n)) by XREAL_1: 6;

      then ((( tau to_power n) + (1 / 2)) - 1) < ( Lucas n) by FIB_NUM3: 21;

      hence thesis by A2, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:31

    for n be Nat st n >= 2 holds ( Lucas n) = [/(( tau to_power n) - (1 / 2))\]

    proof

      let n be Nat;

      assume

       A1: n >= 2;

      then n > 1 by XXREAL_0: 2;

      then ( - (1 / 2)) <= ( tau_bar to_power n) by Th14;

      then (( - (1 / 2)) + ( tau to_power n)) <= (( tau_bar to_power n) + ( tau to_power n)) by XREAL_1: 6;

      then

       A2: (( tau to_power n) - (1 / 2)) <= ( Lucas n) by FIB_NUM3: 21;

      ( tau_bar to_power n) < (1 / 2) by Th8, A1;

      then (( tau_bar to_power n) + ( tau to_power n)) < ((1 / 2) + ( tau to_power n)) by XREAL_1: 6;

      then ((( tau to_power n) - (1 / 2)) + 1) > ( Lucas n) by FIB_NUM3: 21;

      hence thesis by A2, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:32

    for n be Nat st n >= 2 holds ( Lucas (2 * n)) = [/( tau to_power (2 * n))\]

    proof

      let n be Nat;

      assume

       A1: n >= 2;



       A2: ( tau_bar to_power (2 * n)) = (( tau_bar to_power n) to_power 2) by NEWTON: 9

      .= (( tau_bar to_power n) ^2 ) by POWER: 46;

      (n - 0 ) is Element of NAT by NAT_1: 21;

      then ( tau_bar to_power n) <> 0 by FIB_NUM3: 1;

      then ( tau_bar to_power (2 * n)) > 0 by A2, SQUARE_1: 12;

      then ( 0 + ( tau to_power (2 * n))) <= (( tau to_power (2 * n)) + ( tau_bar to_power (2 * n))) by XREAL_1: 6;

      then

       A3: ( tau to_power (2 * n)) <= ( Lucas (2 * n)) by FIB_NUM3: 21;

      ( tau_bar to_power (2 * n)) < 1 by Th8, A1, XXREAL_0: 2;

      then (( tau_bar to_power (2 * n)) + ( tau to_power (2 * n))) < (1 + ( tau to_power (2 * n))) by XREAL_1: 6;

      then (( tau to_power (2 * n)) + 1) > ( Lucas (2 * n)) by FIB_NUM3: 21;

      hence thesis by A3, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:33

    for n be Nat st n >= 2 holds ( Lucas ((2 * n) + 1)) = [\( tau to_power ((2 * n) + 1))/]

    proof

      let n be Nat;

      assume n >= 2;

      then (2 * n) >= (2 * 2) by XREAL_1: 64;

      then ((2 * n) + 1) >= (4 + 1) by XREAL_1: 6;

      then

       A1: ((2 * n) + 1) > 1 by XXREAL_0: 2;

      ( tau_bar to_power ((2 * n) + 1)) <= 0 by Th7;

      then (( tau to_power ((2 * n) + 1)) + 0 ) >= (( tau to_power ((2 * n) + 1)) + ( tau_bar to_power ((2 * n) + 1))) by XREAL_1: 6;

      then

       A2: ( tau to_power ((2 * n) + 1)) >= ( Lucas ((2 * n) + 1)) by FIB_NUM3: 21;

      ( - (1 / 2)) <= ( tau_bar to_power ((2 * n) + 1)) by Th14, A1;

      then ( tau_bar to_power ((2 * n) + 1)) > ( - 1) by XXREAL_0: 2;

      then (( - 1) + ( tau to_power ((2 * n) + 1))) < (( tau to_power ((2 * n) + 1)) + ( tau_bar to_power ((2 * n) + 1))) by XREAL_1: 6;

      then (( tau to_power ((2 * n) + 1)) - 1) < ( Lucas ((2 * n) + 1)) by FIB_NUM3: 21;

      hence thesis by A2, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:34

    for n be Nat st n >= 2 & n is odd holds ( Lucas (n + 1)) = [\(( tau * ( Lucas n)) + 1)/]

    proof

      let n be Nat;

      set tn = ( tau_bar to_power n);

      assume

       A1: n >= 2 & n is odd;



       A2: (( tau * ( Lucas n)) + 1) >= ( Lucas (n + 1))

      proof

        per cases by A1, XXREAL_0: 1;

          suppose

           A3: n = 2;

          ( sqrt 5) >= 1 by SQUARE_1: 18, SQUARE_1: 26;

          then (( sqrt 5) * 3) >= (1 * 3) by XREAL_1: 64;

          then (5 + (( sqrt 5) * 3)) >= (3 + 5) by XREAL_1: 6;

          then ((5 + (( sqrt 5) * 3)) / 2) >= (8 / 2) by XREAL_1: 72;

          hence thesis by A3, FIB_NUM:def 1, FIB_NUM3: 14, FIB_NUM3: 15;

        end;

          suppose

           A4: n > 2;



           A5: ( sqrt 5) > 0 by SQUARE_1: 25;

          tn >= ( - (1 / ( sqrt 5))) & ( sqrt 5) > 0 by Th15, A4, SQUARE_1: 25;

          then (tn * ( sqrt 5)) >= (( - (1 / ( sqrt 5))) * ( sqrt 5)) by XREAL_1: 64;

          then (tn * ( sqrt 5)) >= (( sqrt 5) * (( - 1) / ( sqrt 5))) by XCMPLX_1: 187;

          then (tn * ( sqrt 5)) >= ((( sqrt 5) * ( - 1)) / ( sqrt 5)) by XCMPLX_1: 74;

          then (tn * ( sqrt 5)) >= ((( sqrt 5) / ( sqrt 5)) * ( - 1)) by XCMPLX_1: 74;

          then (tn * ( sqrt 5)) >= (1 * ( - 1)) by A5, XCMPLX_1: 60;

          then ( - (( tau_bar to_power n) * ( sqrt 5))) <= ( - ( - 1)) by XREAL_1: 24;

          then ((tn * tau_bar ) - (tn * tau )) <= 1 by FIB_NUM:def 1, FIB_NUM:def 2;

          then ((tn * ( tau_bar to_power 1)) - (tn * tau )) <= 1;

          then (( tau_bar to_power (n + 1)) - (tn * tau )) <= 1 by Th2;

          then ((( tau_bar to_power (n + 1)) - (tn * tau )) + (tn * tau )) <= (1 + (tn * tau )) by XREAL_1: 6;

          then (((tn * tau ) + 1) + ( tau to_power (n + 1))) >= (( tau_bar to_power (n + 1)) + ( tau to_power (n + 1))) by XREAL_1: 6;

          then (((tn * tau ) + 1) + (( tau to_power n) * ( tau to_power 1))) >= (( tau_bar to_power (n + 1)) + ( tau to_power (n + 1))) by Th2;

          then (((tn * tau ) + 1) + (( tau to_power n) * tau )) >= (( tau_bar to_power (n + 1)) + ( tau to_power (n + 1)));

          then (((tn + ( tau to_power n)) * tau ) + 1) >= (( tau_bar to_power (n + 1)) + ( tau to_power (n + 1)));

          then ((( Lucas n) * tau ) + 1) >= (( tau_bar to_power (n + 1)) + ( tau to_power (n + 1))) by FIB_NUM3: 21;

          hence thesis by FIB_NUM3: 21;

        end;

      end;

      ((( tau * ( Lucas n)) + 1) - 1) < ( Lucas (n + 1))

      proof



         A6: ( Lucas (n + 1)) = (( tau to_power (n + 1)) + ( tau_bar to_power (n + 1))) by FIB_NUM3: 21;



         A7: ( tau * ( Lucas n)) = ( tau * (( tau to_power n) + tn)) by FIB_NUM3: 21

        .= (( tau * ( tau to_power n)) + ( tau * ( tau_bar to_power n)))

        .= ((( tau to_power 1) * ( tau to_power n)) + ( tau * ( tau_bar to_power n)))

        .= (( tau to_power (n + 1)) + ( tau * ( tau_bar to_power n))) by Th2;

        tn < 0 by Th7, A1;

        then ( tau * tn) < ( tau_bar * tn) by XREAL_1: 69;

        then ( tau * tn) < (( tau_bar to_power 1) * tn);

        then ( tau * tn) < ( tau_bar to_power (n + 1)) by Th2;

        hence thesis by A6, A7, XREAL_1: 6;

      end;

      hence thesis by A2, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:35

    for n be Nat st n >= 2 & n is even holds ( Lucas (n + 1)) = [/(( tau * ( Lucas n)) - 1)\]

    proof

      let n be Nat;

      set tn = ( tau_bar to_power n);

      assume

       A1: n >= 2 & n is even;



       A2: ( Lucas (n + 1)) = (( tau to_power (n + 1)) + ( tau_bar to_power (n + 1))) by FIB_NUM3: 21;



       A3: ( tau * ( Lucas n)) = ( tau * (( tau to_power n) + ( tau_bar to_power n))) by FIB_NUM3: 21

      .= (( tau * ( tau to_power n)) + ( tau * ( tau_bar to_power n)))

      .= ((( tau to_power 1) * ( tau to_power n)) + ( tau * ( tau_bar to_power n)))

      .= (( tau to_power (n + 1)) + ( tau * tn)) by Th2;



       A4: (( tau * ( Lucas n)) - 1) <= ( Lucas (n + 1))

      proof

        (( tau * tn) - 1) <= ( tau_bar to_power (n + 1))

        proof



           A5: tn > 0 by Th6, A1;

          tn <= (1 / ( sqrt 5)) by Th16, A1;

          then (1 / tn) >= (1 / (1 / ( sqrt 5))) by Th6, A1, XREAL_1: 118;

          then (1 / tn) >= ( sqrt 5) by XCMPLX_1: 52;

          then ((1 / tn) * 2) >= (( sqrt 5) * 2) by XREAL_1: 64;

          then (((1 / tn) * 2) + 1) >= ((2 * ( sqrt 5)) + 1) by XREAL_1: 6;

          then ((((1 / tn) * 2) + 1) - ( sqrt 5)) >= (((2 * ( sqrt 5)) + 1) - ( sqrt 5)) by XREAL_1: 13;

          then ((((1 / tn) * 2) + (1 - ( sqrt 5))) / 2) >= ((( sqrt 5) + 1) / 2) by XREAL_1: 72;

          then (((1 / tn) + tau_bar ) * tn) >= ( tau * tn) by A5, FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1: 64;

          then (((1 / tn) * tn) + ( tau_bar * tn)) >= ( tau * tn);

          then (((1 / tn) * tn) + (( tau_bar to_power 1) * tn)) >= ( tau * tn);

          then (1 + (( tau_bar to_power 1) * tn)) >= ( tau * tn) by A5, XCMPLX_1: 87;

          then (1 + ( tau_bar to_power (n + 1))) >= ( tau * tn) by Th2;

          then ((1 + ( tau_bar to_power (n + 1))) - 1) >= (( tau * tn) - 1) by XREAL_1: 9;

          hence thesis;

        end;

        then (( tau to_power (n + 1)) + (( tau * tn) - 1)) <= (( tau to_power (n + 1)) + ( tau_bar to_power (n + 1))) by XREAL_1: 6;

        hence thesis by A3, FIB_NUM3: 21;

      end;

      ((( tau * ( Lucas n)) - 1) + 1) > ( Lucas (n + 1))

      proof

        tn = (( - tau_bar ) to_power n) by A1, Th3;

        then tn > 0 by POWER: 34;

        then ( tau * tn) > ( tau_bar * tn) by XREAL_1: 68;

        then ( tau * tn) > (( tau_bar to_power 1) * tn);

        then ( tau * tn) > ( tau_bar to_power (n + 1)) by Th2;

        hence thesis by A2, A3, XREAL_1: 6;

      end;

      hence thesis by A4, INT_1:def 7;

    end;

    theorem :: FIB_NUM4:36

    for n be Nat st n <> 1 holds ( Lucas (n + 1)) = ((( Lucas n) + ( sqrt (5 * ((( Lucas n) ^2 ) - (4 * (( - 1) to_power n)))))) / 2)

    proof

      let n be Nat;

      assume

       A1: n <> 1;



       A2: ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4)) >= 0

      proof

        per cases by A1, NAT_1: 25;

          suppose n = 0 ;

          then ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4)) = ((2 * 2) - (1 * 4)) by FIB_NUM3: 11, POWER: 24;

          hence thesis;

        end;

          suppose n > 1;

          then (n + 1) > (1 + 1) by XREAL_1: 8;

          then n >= 2 & ( Lucas n) >= n by FIB_NUM3: 17, NAT_1: 13;

          then ( Lucas n) >= 2 by XXREAL_0: 2;

          then (( Lucas n) ^2 ) >= (2 ^2 ) by SQUARE_1: 15;

          then (( Lucas n) ^2 ) >= (2 * 2) & ( - (4 * (( - 1) to_power n))) >= ( - 4) by Lm2;

          then ((( Lucas n) ^2 ) + ( - (4 * (( - 1) to_power n)))) >= ((2 * 2) + ( - 4)) by XREAL_1: 7;

          hence thesis;

        end;

      end;



       A3: (n - 0 ) is Element of NAT by NAT_1: 21;

      then (2 * ( Lucas (n + 1))) = ((( Lucas n) * 1) + ((5 * ( Fib n)) * 1)) by FIB_NUM3: 11, FIB_NUM3: 26, PRE_FF: 1;

      then

       A4: ( Lucas (n + 1)) = (((5 * ( Fib n)) + ( Lucas n)) / 2);

      ((( Lucas n) ^2 ) - (5 * (( Fib n) ^2 ))) = ((( Lucas n) to_power 2) - (5 * (( Fib n) ^2 ))) by POWER: 46

      .= ((( Lucas n) to_power 2) - (5 * (( Fib n) to_power 2))) by POWER: 46

      .= ( - ((5 * (( Fib n) |^ 2)) - (( Lucas n) |^ 2)))

      .= ( - (4 * (( - 1) to_power (n + 1)))) by A3, FIB_NUM3: 30

      .= (( - 1) * ((( - 1) to_power (n + 1)) * 4))

      .= ((( - 1) to_power 1) * ((( - 1) to_power (n + 1)) * 4))

      .= (((( - 1) to_power 1) * (( - 1) to_power (n + 1))) * 4)

      .= ((( - 1) to_power ((n + 1) + 1)) * 4) by Th2

      .= ((( - 1) to_power (n + 2)) * 4)

      .= (((( - 1) to_power n) * (( - 1) to_power 2)) * 4) by Th2

      .= (((( - 1) to_power n) * 1) * 4) by FIB_NUM2: 3, POLYFORM: 5;

      then ( Fib n) = ( sqrt (((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4)) / 5)) by SQUARE_1:def 2;



      then ( Lucas (n + 1)) = (((5 * (( sqrt ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4))) / ( sqrt 5))) + ( Lucas n)) / 2) by A2, A4, SQUARE_1: 30

      .= ((((( sqrt ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4))) * 5) / ( sqrt 5)) + ( Lucas n)) / 2) by XCMPLX_1: 74

      .= (((( sqrt ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4))) * (5 / ( sqrt 5))) + ( Lucas n)) / 2) by XCMPLX_1: 74

      .= (((( sqrt ((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4))) * ( sqrt 5)) + ( Lucas n)) / 2) by SQUARE_1: 34

      .= ((( sqrt (((( Lucas n) ^2 ) - ((( - 1) to_power n) * 4)) * 5)) + ( Lucas n)) / 2) by A2, SQUARE_1: 29;

      hence thesis;

    end;

    theorem :: FIB_NUM4:37

    for n be Nat st n >= 4 holds ( Lucas (n + 1)) = [\(((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) / 2)/]

    proof

      let n be Nat;

      set tb = tau_bar ;

      set tbn = ( tau_bar to_power n);

      set tn = ( tau to_power n);

      assume

       A1: n >= 4;



       A2: ( sqrt 5) > 0 by SQUARE_1: 25;



       A3: (((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) / 2) >= ( Lucas (n + 1))

      proof



         A4: (n - 0 ) is non zero Element of NAT by A1, NAT_1: 21;

        ( Lucas (n + 1)) >= (n + 1) & (n + 1) >= ( 0 + 1) by FIB_NUM3: 17, XREAL_1: 6;

        then ( Lucas (n + 1)) >= ( Lucas n) & ( Lucas (n + 1)) >= 1 by A4, FIB_NUM3: 18, XXREAL_0: 2;

        then (( Lucas (n + 1)) + ( Lucas (n + 1))) >= (( Lucas n) + 1) by XREAL_1: 7;

        then ((( Lucas (n + 1)) + ( Lucas (n + 1))) - ( Lucas n)) >= ((( Lucas n) + 1) - ( Lucas n)) by XREAL_1: 9;

        then

         A5: (((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) >= (1 - 1) by XREAL_1: 9;

        (((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) = (((2 * ( Lucas (n + 1))) - (tn + tbn)) - 1) by FIB_NUM3: 21

        .= (((2 * (( tau to_power (n + 1)) + ( tau_bar to_power (n + 1)))) - (tn + tbn)) - 1) by FIB_NUM3: 21

        .= (((2 * ((tn * ( tau to_power 1)) + ( tau_bar to_power (n + 1)))) - (tn + tbn)) - 1) by Th2

        .= (((2 * ((tn * tau ) + ( tau_bar to_power (n + 1)))) - (tn + tbn)) - 1)

        .= (((2 * ((tn * tau ) + (tbn * (tb to_power 1)))) - (tn + tbn)) - 1) by Th2

        .= (((2 * ((tn * tau ) + (tbn * tb))) - (tn + tbn)) - 1)

        .= (((tn - tbn) * ( sqrt 5)) - 1) by FIB_NUM:def 1, FIB_NUM:def 2

        .= (((((tn - tbn) / ( sqrt 5)) * ( sqrt 5)) * ( sqrt 5)) - 1) by A2, XCMPLX_1: 87

        .= (((( Fib n) * ( sqrt 5)) * ( sqrt 5)) - 1) by FIB_NUM: 7

        .= ((( Fib n) * (( sqrt 5) ^2 )) - 1)

        .= ((5 * ( Fib n)) - 1) by SQUARE_1:def 2;



        then

         A6: ((((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) ^2 ) = ((((5 * ( Fib n)) ^2 ) - ((2 * (5 * ( Fib n))) * 1)) + (1 ^2 )) by SQUARE_1: 5

        .= (((25 * (( Fib n) ^2 )) - (10 * ( Fib n))) + 1);

        ((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) >= ((25 * (( Fib n) ^2 )) - (10 * ( Fib n)))

        proof

          per cases by A1, XXREAL_0: 1;

            suppose n = 4;

            hence thesis by FIB_NUM2: 23, FIB_NUM3: 16;

          end;

            suppose n > 4;

            then

             A7: n >= (4 + 1) by NAT_1: 13;

            set s5 = ( sqrt 5);



             A8: ((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) = ((5 * (( Lucas n) ^2 )) - (2 * (tn + tbn))) by FIB_NUM3: 21

            .= ((5 * ((tn + tbn) ^2 )) - (2 * (tn + tbn))) by FIB_NUM3: 21

            .= (((((5 * (tn ^2 )) + (((5 * 2) * tn) * tbn)) + (5 * (tbn ^2 ))) - (2 * tn)) - (2 * tbn));



             A9: ((25 * (( Fib n) ^2 )) - (10 * ( Fib n))) = ((25 * (( Fib n) ^2 )) - (10 * ((tn - tbn) / s5))) by FIB_NUM: 7

            .= ((25 * (((tn - tbn) / s5) ^2 )) - (10 * ((tn - tbn) / s5))) by FIB_NUM: 7

            .= ((25 * (((tn - tbn) ^2 ) / (s5 ^2 ))) - (10 * ((tn - tbn) / s5))) by XCMPLX_1: 76

            .= ((25 * (((tn - tbn) ^2 ) / 5)) - (10 * ((tn - tbn) / s5))) by SQUARE_1:def 2

            .= ((((5 * (tn ^2 )) - (((5 * 2) * tn) * tbn)) + (5 * (tbn ^2 ))) - (10 * (((tn - tbn) * s5) / (s5 ^2 )))) by A2, XCMPLX_1: 91

            .= ((((5 * (tn ^2 )) - ((10 * tn) * tbn)) + (5 * (tbn ^2 ))) - (10 * (((tn - tbn) * s5) / 5))) by SQUARE_1:def 2

            .= (((((5 * (tn ^2 )) - ((10 * tn) * tbn)) + (5 * (tbn ^2 ))) - ((2 * tn) * s5)) + ((2 * tbn) * s5));



             A10: ((n -' 1) + 1) = ((n + 1) -' 1) by A1, NAT_D: 38, XXREAL_0: 2

            .= n by NAT_D: 34;



             A11: ( - 10) <= (10 * (( - 1) to_power n)) by Lm1;

            (n -' 1) >= (5 -' 1) by A7, NAT_D: 42;

            then (n -' 1) >= (5 - 1) by NAT_D: 39;

            then ( Lucas (n -' 1)) >= 7 by Th12, FIB_NUM3: 16;

            then ( Lucas (n -' 1)) >= 5 by XXREAL_0: 2;

            then (( Lucas (n -' 1)) * ( - 2)) <= (5 * ( - 2)) by XREAL_1: 65;

            then (( Lucas ((n -' 1) + 1)) - ((2 * ( Lucas (n -' 1))) + ( Lucas ((n -' 1) + 1)))) <= ( - 10);

            then (( Lucas n) - (5 * ( Fib n))) <= ( - 10) by A10, FIB_NUM3: 22;

            then ((tn + tbn) - (5 * ( Fib n))) <= ( - 10) by FIB_NUM3: 21;

            then ((tn + tbn) - (5 * ((tn - tbn) / s5))) <= ( - 10) by FIB_NUM: 7;

            then ((tn + tbn) - (5 * ((tn - tbn) * (1 / s5)))) <= ( - 10) by XCMPLX_1: 99;

            then ((tn + tbn) - ((5 * (1 / s5)) * (tn - tbn))) <= ( - 10);

            then ((tn + tbn) - (((s5 ^2 ) * (1 / s5)) * (tn - tbn))) <= ( - 10) by SQUARE_1:def 2;

            then ((tn + tbn) - ((s5 * (s5 * (1 / s5))) * (tn - tbn))) <= ( - 10);

            then ((tn + tbn) - ((s5 * (s5 / s5)) * (tn - tbn))) <= ( - 10) by XCMPLX_1: 99;

            then ((tn + tbn) - ((s5 * 1) * (tn - tbn))) <= ( - 10) by A2, XCMPLX_1: 60;

            then (((tn + tbn) - (s5 * tn)) + (s5 * tbn)) <= (10 * (( tau * tb) to_power n)) by Lm3, A11, XXREAL_0: 2;

            then ((((tn + tbn) - (s5 * tn)) + (( sqrt 5) * tbn)) - (10 * (( tau * tb) to_power n))) <= ((10 * (( tau * tb) to_power n)) - (10 * (( tau * tb) to_power n))) by XREAL_1: 9;

            then (((((tn + tbn) - (s5 * tn)) + (s5 * tbn)) - (10 * (( tau * tb) to_power n))) + (( sqrt 5) * tn)) <= ( 0 + (s5 * tn)) by XREAL_1: 6;

            then (((tn + tbn) + (s5 * tbn)) - (10 * (( tau * tb) to_power n))) <= (s5 * tn);

            then (((tn + tbn) + (s5 * tbn)) - (10 * (tn * tbn))) <= (s5 * tn) by NEWTON: 7;

            then ((((( - ((10 * tn) * tbn)) + tn) + tbn) + (tbn * s5)) * 2) <= ((tn * s5) * 2) by XREAL_1: 64;

            then ( - (((( - ((20 * tn) * tbn)) + (2 * tn)) + (2 * tbn)) + ((2 * tbn) * s5))) >= ( - ((2 * tn) * s5)) by XREAL_1: 24;

            then (((((((10 * tn) * tbn) - (2 * tn)) - (2 * tbn)) - ((2 * tbn) * s5)) + ((10 * tn) * tbn)) - ((10 * tn) * tbn)) >= (( - ((2 * tn) * s5)) - ((10 * tn) * tbn)) by XREAL_1: 9;

            then ((((((10 * tn) * tbn) - (2 * tn)) - (2 * tbn)) - ((2 * tbn) * s5)) + ((2 * tbn) * s5)) >= ((( - ((10 * tn) * tbn)) - ((2 * tn) * s5)) + ((2 * tbn) * s5)) by XREAL_1: 6;

            then (((((10 * tn) * tbn) - (2 * tn)) - (2 * tbn)) + (5 * (tbn ^2 ))) >= (((( - ((10 * tn) * tbn)) - ((2 * tn) * s5)) + ((2 * tbn) * s5)) + (5 * (tbn ^2 ))) by XREAL_1: 6;

            then ((((((10 * tn) * tbn) + (5 * (tbn ^2 ))) - (2 * tn)) - (2 * tbn)) + (5 * (tn ^2 ))) >= ((((( - ((10 * tn) * tbn)) + (5 * (tbn ^2 ))) - ((2 * tn) * s5)) + ((2 * tbn) * s5)) + (5 * (tn ^2 ))) by XREAL_1: 6;

            hence thesis by A8, A9;

          end;

        end;

        then (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1) >= ((((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) ^2 ) by A6, XREAL_1: 6;

        then ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1)) >= ( sqrt ((((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) ^2 )) by SQUARE_1: 26;

        then ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1)) >= (((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) by A5, SQUARE_1:def 2;

        then (( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1)) + (( Lucas n) + 1)) >= ((((2 * ( Lucas (n + 1))) - ( Lucas n)) - 1) + (( Lucas n) + 1)) by XREAL_1: 6;

        then (((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) / 2) >= ((2 * ( Lucas (n + 1))) / 2) by XREAL_1: 72;

        hence thesis;

      end;

      ((((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) / 2) - 1) < ( Lucas (n + 1))

      proof

        ( Lucas n) >= n by FIB_NUM3: 17;

        then

         A12: ( Lucas n) >= 4 by A1, XXREAL_0: 2;

        then

         A13: (( Lucas n) / 5) >= (4 / 5) by XREAL_1: 72;

        ( Fib n) >= 3 by A1, FIB_NUM2: 23, FIB_NUM2: 45;

        then (( Fib n) + (( Lucas n) / 5)) >= (3 + (4 / 5)) by A13, XREAL_1: 7;

        then

         A14: 2 < (( Fib n) + (( Lucas n) / 5)) by XXREAL_0: 2;

        n is even or n is odd;

        then (( - 1) to_power n) <= 1 by FIB_NUM2: 2, FIB_NUM2: 3;

        then (2 * (( - 1) to_power n)) <= (2 * 1) by XREAL_1: 64;

        then (2 * (( - 1) to_power n)) < (( Fib n) + (( Lucas n) / 5)) by A14, XXREAL_0: 2;

        then (2 * (( - 1) to_power n)) < (((tn - tbn) / ( sqrt 5)) + (( Lucas n) / 5)) by FIB_NUM: 7;

        then (2 * (( - 1) to_power n)) < (((tn - tbn) / ( sqrt 5)) + ((tn + tbn) / 5)) by FIB_NUM3: 21;

        then ((2 * (( - 1) to_power n)) * 10) < ((((tn - tbn) / ( sqrt 5)) + ((tn + tbn) / 5)) * 10) by XREAL_1: 68;

        then (20 * (( - 1) to_power n)) < ((((tn - tbn) / ( sqrt 5)) * (2 * 5)) + ((tn + tbn) * 2));

        then (20 * (( - 1) to_power n)) < ((((tn - tbn) / ( sqrt 5)) * (2 * (( sqrt 5) ^2 ))) + ((tn + tbn) * 2)) by SQUARE_1:def 2;

        then (20 * (( - 1) to_power n)) < (((((tn - tbn) / ( sqrt 5)) * ( sqrt 5)) * (( sqrt 5) * 2)) + ((tn + tbn) * 2));

        then (20 * (( - 1) to_power n)) < (((tn - tbn) * (2 * ( sqrt 5))) + ((tn + tbn) * 2)) by A2, XCMPLX_1: 87;

        then ((20 * (( - 1) to_power n)) + (((5 * (tn ^2 )) + (5 * (tbn ^2 ))) + 1)) < ((((tn - tbn) * (2 * ( sqrt 5))) + ((tn + tbn) * 2)) + (((5 * (tn ^2 )) + (5 * (tbn ^2 ))) + 1)) by XREAL_1: 6;

        then (((20 * (( - 1) to_power n)) + (((5 * (tn ^2 )) + (5 * (tbn ^2 ))) + 1)) - ((tn + tbn) * 2)) < (((((tn - tbn) * (2 * ( sqrt 5))) + ((tn + tbn) * 2)) + (((5 * (tn ^2 )) + (5 * (tbn ^2 ))) + 1)) - ((tn + tbn) * 2)) by XREAL_1: 9;

        then (((((((10 * (( - 1) to_power n)) + (10 * (( - 1) to_power n))) + (5 * (tn ^2 ))) + (5 * (tbn ^2 ))) + 1) - ((tn + tbn) * 2)) - (10 * (( - 1) to_power n))) < ((((tn - tbn) * (2 * ( sqrt 5))) + (((5 * (tn ^2 )) + (5 * (tbn ^2 ))) + 1)) - (10 * (( - 1) to_power n))) by XREAL_1: 9;

        then ((((5 * (((2 * (( tau * tau_bar ) to_power n)) + (tn ^2 )) + (tbn ^2 ))) + 1) - (2 * tn)) - (2 * tbn)) < (((((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * (tn ^2 ))) + (5 * (tbn ^2 ))) - (10 * (( - 1) to_power n))) + 1) by Lm3;

        then ((((5 * (((2 * (tn * tbn)) + (tn ^2 )) + (tbn ^2 ))) + 1) - (2 * tn)) - (2 * tbn)) < (((((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * (tn ^2 ))) + (5 * (tbn ^2 ))) - ((5 * 2) * (( - 1) to_power n))) + 1) by NEWTON: 7;

        then ((((5 * ((tn + tbn) ^2 )) + 1) - (2 * tn)) - (2 * tbn)) < (((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * (((tn ^2 ) + (tbn ^2 )) - (2 * (( tau * tau_bar ) to_power n))))) + 1) by Lm3;

        then ((((5 * ((tn + tbn) ^2 )) + 1) - (2 * tn)) - (2 * tbn)) < (((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * (((tn ^2 ) + (tbn ^2 )) - (2 * (tn * tbn))))) + 1) by NEWTON: 7;

        then

         A15: (((5 * ((tn + tbn) ^2 )) + 1) - (2 * (tn + tbn))) < (((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * ((tn - tbn) ^2 ))) + 1);



         A16: (((5 * (( Lucas n) ^2 )) + 1) - (2 * ( Lucas n))) >= 0

        proof

          (5 * ( Lucas n)) >= (5 * 4) by A12, XREAL_1: 66;

          then ((5 * ( Lucas n)) - 2) >= (20 - 2) by XREAL_1: 9;

          then (( Lucas n) * ((5 * ( Lucas n)) - 2)) >= (4 * 18) by A12, XREAL_1: 66;

          then ((( Lucas n) * ((5 * ( Lucas n)) - 2)) + 1) >= ((4 * 18) + 1) by XREAL_1: 6;

          hence thesis;

        end;



         A17: (((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) > 0

        proof

          (((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) = (((((2 * (tn * ( tau to_power 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) by Th2

          .= (((((2 * (tn * ( tau to_power 1))) - tn) + (2 * (tbn * (tb to_power 1)))) - tbn) + 1) by Th2

          .= (((((2 * (tn * tau )) - tn) + (2 * (tbn * (tb to_power 1)))) - tbn) + 1)

          .= ((((tn * ( sqrt 5)) + (2 * (tbn * tb))) - tbn) + 1) by FIB_NUM:def 1

          .= (((( sqrt 5) * (tn - tbn)) * 1) + 1) by FIB_NUM:def 2

          .= (((( sqrt 5) * (tn - tbn)) * (( sqrt 5) / ( sqrt 5))) + 1) by A2, XCMPLX_1: 60

          .= (((( sqrt 5) * (tn - tbn)) * (( sqrt 5) * (1 / ( sqrt 5)))) + 1) by XCMPLX_1: 99

          .= (((( sqrt 5) * ((tn - tbn) * (1 / ( sqrt 5)))) * ( sqrt 5)) + 1)

          .= (((( sqrt 5) * ((tn - tbn) / ( sqrt 5))) * ( sqrt 5)) + 1) by XCMPLX_1: 99

          .= (((( sqrt 5) * ( Fib n)) * ( sqrt 5)) + 1) by FIB_NUM: 7

          .= (((( sqrt 5) ^2 ) * ( Fib n)) + 1)

          .= ((5 * ( Fib n)) + 1) by SQUARE_1:def 2;

          hence thesis;

        end;

        (((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + (5 * ((tn - tbn) ^2 ))) + 1) = (((((2 * ( sqrt 5)) * tn) - ((2 * ( sqrt 5)) * tbn)) + ((( sqrt 5) ^2 ) * ((tn - tbn) ^2 ))) + 1) by SQUARE_1:def 2

        .= (((((((2 * tau ) * tn) - (1 * tn)) + ((2 * tb) * tbn)) - (1 * tbn)) + 1) ^2 ) by FIB_NUM:def 1, FIB_NUM:def 2

        .= (((((((2 * ( tau to_power 1)) * tn) - (1 * tn)) + ((2 * tb) * tbn)) - (1 * tbn)) + 1) ^2 )

        .= ((((((2 * (( tau to_power 1) * tn)) - (1 * tn)) + ((2 * (tb to_power 1)) * tbn)) - (1 * tbn)) + 1) ^2 )

        .= ((((((2 * ( tau to_power (n + 1))) - tn) + (2 * ((tb to_power 1) * tbn))) - tbn) + 1) ^2 ) by Th2

        .= ((((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) ^2 ) by Th2;

        then (((5 * (( Lucas n) ^2 )) + 1) - (2 * (tn + tbn))) < ((((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) ^2 ) by A15, FIB_NUM3: 21;

        then (((5 * (( Lucas n) ^2 )) + 1) - (2 * ( Lucas n))) < ((((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) ^2 ) by FIB_NUM3: 21;

        then ( sqrt (((5 * (( Lucas n) ^2 )) + 1) - (2 * ( Lucas n)))) < ( sqrt ((((((2 * ( tau to_power (n + 1))) - tn) + (2 * ( tau_bar to_power (n + 1)))) - tbn) + 1) ^2 )) by A16, SQUARE_1: 27;

        then ( sqrt (((5 * (( Lucas n) ^2 )) + 1) - (2 * ( Lucas n)))) < ((((2 * (( tau to_power (n + 1)) + ( tau_bar to_power (n + 1)))) - tn) - tbn) + 1) by A17, SQUARE_1: 22;

        then ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1)) < ((((2 * ( Lucas (n + 1))) - tn) - tbn) + 1) by FIB_NUM3: 21;

        then (1 + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) < (((((2 * ( Lucas (n + 1))) + 1) - tn) - tbn) + 1) by XREAL_1: 6;

        then (((((tn + tbn) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - tn) - tbn) < ((((2 * ( Lucas (n + 1))) + 2) - tn) - tbn);

        then ((((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - tn) - tbn) < ((((2 * ( Lucas (n + 1))) + 2) - tn) - tbn) by FIB_NUM3: 21;

        then (((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - tn) < (((2 * ( Lucas (n + 1))) + 2) - tn) by XREAL_1: 9;

        then ((((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - 2) + 2) < ((2 * ( Lucas (n + 1))) + 2) by XREAL_1: 9;

        then (((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - 2) < (2 * ( Lucas (n + 1))) by XREAL_1: 6;

        then ((((( Lucas n) + 1) + ( sqrt (((5 * (( Lucas n) ^2 )) - (2 * ( Lucas n))) + 1))) - 2) / 2) < ((2 * ( Lucas (n + 1))) / 2) by XREAL_1: 74;

        hence thesis;

      end;

      hence thesis by A3, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:38

    for n be Nat st n > 2 holds ( Lucas n) = [\((1 / tau ) * (( Lucas (n + 1)) + (1 / 2)))/]

    proof

      let n be Nat;

      assume

       A1: n > 2;

      then

       A2: n > 1 by XXREAL_0: 2;



       A3: ( sqrt 5) > 0 by SQUARE_1: 25;

      set tbn = ( tau_bar to_power n);



       A4: ((1 / tau ) * (( Lucas (n + 1)) + (1 / 2))) >= ( Lucas n)

      proof

        tbn <= (1 / (2 * ( sqrt 5)))

        proof

          per cases ;

            suppose

             A5: n is even;

            n >= (2 + 1) by A1, NAT_1: 13;

            then n = 3 or n > 3 by XXREAL_0: 1;

            then n = 3 or n >= (3 + 1) by NAT_1: 8;

            then

             A6: tbn <= ( tau_bar to_power 4) by Th11, A5, POLYFORM: 6;



             A7: ( tau_bar to_power (3 + 1)) = (( tau_bar to_power 3) * ( tau_bar to_power 1)) by Th2

            .= ((2 - ( sqrt 5)) * tau_bar ) by Lm8

            .= ((((2 - (2 * ( sqrt 5))) - ( sqrt 5)) + (( sqrt 5) ^2 )) / 2) by FIB_NUM:def 2

            .= (((2 - (3 * ( sqrt 5))) + 5) / 2) by SQUARE_1:def 2

            .= ((7 - (3 * ( sqrt 5))) / 2);

            ( sqrt 5) <= ( sqrt ((16 / 7) ^2 )) by SQUARE_1: 26;

            then ( sqrt 5) <= (16 / 7) by SQUARE_1:def 2;

            then (7 * ( sqrt 5)) <= ((16 / 7) * 7) by XREAL_1: 64;

            then ((7 * ( sqrt 5)) - (3 * 5)) <= (16 - (3 * 5)) by XREAL_1: 9;

            then ((7 * ( sqrt 5)) - (3 * (( sqrt 5) ^2 ))) <= 1 by SQUARE_1:def 2;

            then (((7 - (3 * ( sqrt 5))) * ( sqrt 5)) / ( sqrt 5)) <= (1 / ( sqrt 5)) by A3, XREAL_1: 72;

            then (7 - (3 * ( sqrt 5))) <= (1 / ( sqrt 5)) by A3, XCMPLX_1: 89;

            then ((7 - (3 * ( sqrt 5))) / 2) <= ((1 / ( sqrt 5)) / 2) by XREAL_1: 72;

            then ( tau_bar to_power 4) <= (1 / (2 * ( sqrt 5))) by A7, XCMPLX_1: 78;

            hence thesis by A6, XXREAL_0: 2;

          end;

            suppose n is odd;

            then tbn < 0 by Th7;

            hence thesis by A3;

          end;

        end;

        then (tbn * ( sqrt 5)) <= ((1 / (2 * ( sqrt 5))) * ( sqrt 5)) by A3, XREAL_1: 64;

        then (tbn * ( sqrt 5)) <= (1 / 2) by A3, XCMPLX_1: 92;

        then ( - (tbn * ( sqrt 5))) >= ( - (1 / 2)) by XREAL_1: 24;

        then ((( tau_bar * tbn) - ( tau * tbn)) + ((1 / 2) + ( tau * tbn))) >= (( - (1 / 2)) + ((1 / 2) + ( tau * tbn))) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1: 6;

        then ((( tau_bar * tbn) + (1 / 2)) / tau ) >= ((tbn * tau ) / tau ) by XREAL_1: 72;

        then ((( tau_bar * tbn) + (1 / 2)) / tau ) >= tbn by XCMPLX_1: 89;

        then (((( tau_bar * tbn) + (1 / 2)) / tau ) + (( tau to_power (n + 1)) / tau )) >= (tbn + (( tau to_power (n + 1)) / tau )) by XREAL_1: 6;

        then (((( tau_bar * tbn) + (1 / 2)) + ( tau to_power (n + 1))) / tau ) >= (tbn + (( tau to_power (n + 1)) / tau )) by XCMPLX_1: 62;

        then ((((( tau_bar to_power 1) * tbn) + (1 / 2)) + ( tau to_power (n + 1))) / tau ) >= (tbn + (( tau to_power (n + 1)) / tau ));

        then ((((( tau_bar to_power 1) * tbn) + ( tau to_power (n + 1))) + (1 / 2)) / tau ) >= (tbn + ((( tau to_power n) * ( tau to_power 1)) / tau )) by Th2;

        then (((( tau_bar to_power (1 + n)) + ( tau to_power (n + 1))) + (1 / 2)) / tau ) >= (tbn + ((( tau to_power n) * ( tau to_power 1)) / tau )) by Th2;

        then ((( Lucas (n + 1)) + (1 / 2)) / tau ) >= (tbn + ((( tau to_power n) * ( tau to_power 1)) / tau )) by FIB_NUM3: 21;

        then ((( Lucas (n + 1)) + (1 / 2)) / tau ) >= (tbn + ((( tau to_power n) * tau ) / tau ));

        then ((( Lucas (n + 1)) + (1 / 2)) / tau ) >= (tbn + ( tau to_power n)) by XCMPLX_1: 89;

        then ((( Lucas (n + 1)) + (1 / 2)) / tau ) >= ( Lucas n) by FIB_NUM3: 21;

        hence thesis by XCMPLX_1: 99;

      end;

      (((1 / tau ) * (( Lucas (n + 1)) + (1 / 2))) - 1) < ( Lucas n)

      proof

        tbn > ( - (1 / 2)) by Th14, A2;

        then ( - tbn) < ( - ( - (1 / 2))) by XREAL_1: 24;

        then (( - tbn) * ( sqrt 5)) < ((1 / 2) * ( sqrt 5)) by A3, XREAL_1: 68;

        then (((tbn * tau_bar ) - (tbn * tau )) + ((tbn * tau ) + (1 / 2))) < (( tau - (1 / 2)) + ((tbn * tau ) + (1 / 2))) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1: 6;

        then (((tbn * tau_bar ) + (1 / 2)) - tau ) < (((( tau - (1 / 2)) + (tbn * tau )) + (1 / 2)) - tau ) by XREAL_1: 9;

        then ((((tbn * tau_bar ) + (1 / 2)) - tau ) / tau ) < ((tbn * tau ) / tau ) by XREAL_1: 74;

        then ((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) - ( tau / tau )) < ((tbn * tau ) / tau ) by XCMPLX_1: 124;

        then ((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) - ( tau / tau )) < tbn by XCMPLX_1: 89;

        then ((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) - 1) < tbn by XCMPLX_1: 60;

        then (((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) - 1) + ( tau to_power n)) < (tbn + ( tau to_power n)) by XREAL_1: 6;

        then (((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) + (( tau to_power n) * 1)) - 1) < ( Lucas n) by FIB_NUM3: 21;

        then (((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) + (( tau to_power n) * ( tau / tau ))) - 1) < ( Lucas n) by XCMPLX_1: 60;

        then (((((tbn * tau_bar ) / tau ) + ((1 / 2) / tau )) + ((( tau to_power n) * tau ) / tau )) - 1) < ( Lucas n) by XCMPLX_1: 74;

        then (((((tbn * tau_bar ) + (1 / 2)) + (( tau to_power n) * tau )) / tau ) - 1) < ( Lucas n) by XCMPLX_1: 63;

        then (((((tbn * ( tau_bar to_power 1)) + (1 / 2)) + (( tau to_power n) * tau )) / tau ) - 1) < ( Lucas n);

        then (((((tbn * ( tau_bar to_power 1)) + (1 / 2)) + (( tau to_power n) * ( tau to_power 1))) / tau ) - 1) < ( Lucas n);

        then ((((( tau_bar to_power (n + 1)) + (1 / 2)) + (( tau to_power n) * ( tau to_power 1))) / tau ) - 1) < ( Lucas n) by Th2;

        then ((((( tau_bar to_power (n + 1)) + (1 / 2)) + ( tau to_power (n + 1))) / tau ) - 1) < ( Lucas n) by Th2;

        then ((((( tau_bar to_power (n + 1)) + ( tau to_power (n + 1))) + (1 / 2)) / tau ) - 1) < ( Lucas n);

        then (((( Lucas (n + 1)) + (1 / 2)) / tau ) - 1) < ( Lucas n) by FIB_NUM3: 21;

        hence thesis by XCMPLX_1: 99;

      end;

      hence thesis by A4, INT_1:def 6;

    end;

    theorem :: FIB_NUM4:39

    for n,k be Nat st n >= 4 & k >= 1 & n > k & n is odd holds ( Lucas (n + k)) = [\((( tau to_power k) * ( Lucas n)) + 1)/]

    proof

      let n,k be Nat;

      assume

       A1: n >= 4 & k >= 1 & n > k & n is odd;

      set tb = tau_bar ;

      set tk = ( tau to_power k);

      set tn = ( tau to_power n);

      set tbn = ( tau_bar to_power n);



       A2: ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1: 27;



       A3: ((( tau to_power k) * ( Lucas n)) + 1) >= ( Lucas (n + k))

      proof

        ((tk * tbn) + 1) >= (tb to_power (n + k))

        proof

          consider m be Nat such that

           A4: n = (k + m) by A1, NAT_1: 10;



           A5: m is non zero Nat by A1, A4;

          then

           A6: m >= 1 by NAT_1: 14;



           A7: (((((1 - ( sqrt 5)) to_power m) * (( - 1) to_power k)) / (2 to_power m)) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)))

          proof

            per cases ;

              suppose

               A8: k is even;

              then

               A9: m is odd by A1, A4;



               A10: (2 to_power m) > 0 by POWER: 34;



               A11: (((((1 - ( sqrt 5)) to_power m) * (( - 1) to_power k)) / (2 to_power m)) + 1) = (((((1 - ( sqrt 5)) to_power m) * 1) / (2 to_power m)) + 1) by A8, FIB_NUM2: 3

              .= (((( - (( - 1) + ( sqrt 5))) to_power m) / (2 to_power m)) + ((2 to_power m) / (2 to_power m))) by A10, XCMPLX_1: 60

              .= ((((( - 1) * (( sqrt 5) - 1)) to_power m) + (2 to_power m)) / (2 to_power m)) by XCMPLX_1: 62

              .= ((((( - 1) to_power m) * ((( sqrt 5) - 1) to_power m)) + (2 to_power m)) / (2 to_power m)) by NEWTON: 7

              .= (((2 to_power m) + (( - 1) * ((( sqrt 5) - 1) to_power m))) / (2 to_power m)) by A9, FIB_NUM2: 2

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



               A12: ( sqrt (3 ^2 )) > ( sqrt 5) & ( sqrt 5) > ( sqrt 1) by SQUARE_1: 27;

              then 3 > ( sqrt 5) & ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1:def 2;

              then (3 - 1) > (( sqrt 5) - 1) & (( sqrt 5) - 1) > (1 - 1) by XREAL_1: 9;

              then (2 to_power m) > ((( sqrt 5) - 1) to_power m) by A5, POWER: 37;

              then

               A13: ((2 to_power m) - ((( sqrt 5) - 1) to_power m)) > (((( sqrt 5) - 1) to_power m) - ((( sqrt 5) - 1) to_power m)) by XREAL_1: 9;



               A14: (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) = (((( - 1) * (( - 1) + ( sqrt 5))) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)))

              .= (((( - 1) to_power ((2 * k) + m)) * ((( - 1) + ( sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m))) by NEWTON: 7

              .= ((( - 1) * ((( - 1) + ( sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m))) by A9, FIB_NUM2: 2

              .= (( - 1) * (((( - 1) + ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)))) by XCMPLX_1: 74;

              (( sqrt 5) - 1) > (1 - 1) by A12, SQUARE_1: 18, XREAL_1: 9;

              then ((( - 1) + ( sqrt 5)) to_power ((2 * k) + m)) > 0 by POWER: 34;

              then (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) <= 0 by A14;

              hence thesis by A13, A11;

            end;

              suppose

               A15: k is odd;

              then

               A16: m is even by A1, A4;



               A17: (2 to_power m) > 0 by POWER: 34;



               A18: (2 to_power (2 * k)) > 0 by POWER: 34;

              m > 1 by A16, A6, POLYFORM: 4, XXREAL_0: 1;

              then

               A19: (m - 1) is non zero Nat by NAT_1: 20;



               A20: (((((1 - ( sqrt 5)) to_power m) * (( - 1) to_power k)) / (2 to_power m)) + 1) = (((((1 - ( sqrt 5)) to_power m) * ( - 1)) / (2 to_power m)) + 1) by A15, FIB_NUM2: 2

              .= (((((1 - ( sqrt 5)) to_power m) * ( - 1)) / (2 to_power m)) + ((2 to_power m) / (2 to_power m))) by A17, XCMPLX_1: 60

              .= (((((( - 1) * (( - 1) + ( sqrt 5))) to_power m) * ( - 1)) + (2 to_power m)) / (2 to_power m)) by XCMPLX_1: 62

              .= (((((( - 1) to_power m) * ((( - 1) + ( sqrt 5)) to_power m)) * ( - 1)) + (2 to_power m)) / (2 to_power m)) by NEWTON: 7

              .= ((((1 * ((( - 1) + ( sqrt 5)) to_power m)) * ( - 1)) + (2 to_power m)) / (2 to_power m)) by A16, FIB_NUM2: 3

              .= (((( - ((( - 1) + ( sqrt 5)) to_power m)) + (2 to_power m)) * (2 to_power (2 * k))) / ((2 to_power m) * (2 to_power (2 * k)))) by A18, XCMPLX_1: 91

              .= ((( - (((( - 1) + ( sqrt 5)) to_power m) * (2 to_power (2 * k)))) + ((2 to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k)))) by Th2

              .= ((( - (((( - 1) + ( sqrt 5)) to_power m) * (2 to_power (2 * k)))) + (2 to_power (m + (2 * k)))) / (2 to_power (m + (2 * k)))) by Th2

              .= (((2 to_power (m + (2 * k))) - (((( - 1) + ( sqrt 5)) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))));



               A21: (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) = (((( - 1) * (( - 1) + ( sqrt 5))) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)))

              .= (((( - 1) to_power ((2 * k) + m)) * ((( - 1) + ( sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m))) by NEWTON: 7

              .= ((1 * ((( - 1) + ( sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m))) by A16, FIB_NUM2: 3

              .= (((( sqrt 5) - 1) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)));

              ((2 to_power m) - ((( sqrt 5) - 1) to_power m)) >= ((( sqrt 5) - 1) to_power m)

              proof

                defpred P[ Nat] means ((2 to_power ($1 + 1)) - ((( sqrt 5) - 1) to_power ($1 + 1))) >= ((( sqrt 5) - 1) to_power ($1 + 1));



                 A22: ((2 to_power (1 + 1)) - ((( sqrt 5) - 1) to_power (1 + 1))) = ((2 ^2 ) - ((( sqrt 5) - 1) to_power 2)) by POWER: 46

                .= (4 - ((( sqrt 5) - 1) ^2 )) by POWER: 46

                .= (4 - (((( sqrt 5) ^2 ) - ((2 * ( sqrt 5)) * 1)) + (1 ^2 )))

                .= (4 - ((5 - (2 * ( sqrt 5))) + 1)) by SQUARE_1:def 2

                .= ((2 * ( sqrt 5)) - 2);



                 A23: ((( sqrt 5) - 1) to_power (1 + 1)) = ((( sqrt 5) - 1) ^2 ) by POWER: 46

                .= (((( sqrt 5) ^2 ) - ((2 * ( sqrt 5)) * 1)) + (1 ^2 ))

                .= ((5 - (2 * ( sqrt 5))) + 1) by SQUARE_1:def 2

                .= (6 - (2 * ( sqrt 5)));

                ( sqrt 5) >= ( sqrt (2 ^2 )) by SQUARE_1: 27;

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

                then (( sqrt 5) * 4) >= (2 * 4) by XREAL_1: 64;

                then (((( sqrt 5) * 2) + (( sqrt 5) * 2)) - 2) >= ((6 + 2) - 2) by XREAL_1: 9;

                then ((((( sqrt 5) * 2) + (( sqrt 5) * 2)) - 2) - (2 * ( sqrt 5))) >= (6 - (2 * ( sqrt 5))) by XREAL_1: 9;

                then

                 A24: P[1] by A22, A23;



                 A25: for k be non zero Nat st P[k] holds P[(k + 1)]

                proof

                  let k be non zero Nat;



                   A26: (( sqrt 5) - 1) > (1 - 1) by A2, XREAL_1: 9;

                  assume P[k];

                  then (((2 to_power (k + 1)) - ((( sqrt 5) - 1) to_power (k + 1))) + ((( sqrt 5) - 1) to_power (k + 1))) >= (((( sqrt 5) - 1) to_power (k + 1)) + ((( sqrt 5) - 1) to_power (k + 1))) by XREAL_1: 6;

                  then ((2 to_power (k + 1)) * (( sqrt 5) - 1)) >= ((2 * ((( sqrt 5) - 1) to_power (k + 1))) * (( sqrt 5) - 1)) by A26, XREAL_1: 64;

                  then ((2 to_power (k + 1)) * (( sqrt 5) - 1)) >= (2 * (((( sqrt 5) - 1) to_power (k + 1)) * (( sqrt 5) - 1)));

                  then ((2 to_power (k + 1)) * (( sqrt 5) - 1)) >= (2 * (((( sqrt 5) - 1) to_power (k + 1)) * ((( sqrt 5) - 1) to_power 1)));

                  then

                   A27: ((2 to_power (k + 1)) * (( sqrt 5) - 1)) >= (2 * ((( sqrt 5) - 1) to_power ((k + 1) + 1))) by Th2, A26;

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

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

                  then (3 - 1) >= (( sqrt 5) - 1) by XREAL_1: 9;

                  then (2 * (2 to_power (k + 1))) >= ((( sqrt 5) - 1) * (2 to_power (k + 1))) by XREAL_1: 64;

                  then ((2 to_power 1) * (2 to_power (k + 1))) >= ((( sqrt 5) - 1) * (2 to_power (k + 1)));

                  then (2 to_power ((1 + k) + 1)) >= ((( sqrt 5) - 1) * (2 to_power (k + 1))) by Th2;

                  then (2 to_power ((1 + k) + 1)) >= (2 * ((( sqrt 5) - 1) to_power ((k + 1) + 1))) by A27, XXREAL_0: 2;

                  then ((2 to_power ((1 + k) + 1)) - ((( sqrt 5) - 1) to_power ((k + 1) + 1))) >= ((2 * ((( sqrt 5) - 1) to_power ((k + 1) + 1))) - ((( sqrt 5) - 1) to_power ((k + 1) + 1))) by XREAL_1: 9;

                  hence thesis;

                end;

                for k be non zero Nat holds P[k] from NAT_1:sch 10( A24, A25);

                then ((2 to_power ((m - 1) + 1)) - ((( sqrt 5) - 1) to_power ((m - 1) + 1))) >= ((( sqrt 5) - 1) to_power ((m - 1) + 1)) by A19;

                hence thesis;

              end;

              then (((2 to_power m) - ((( sqrt 5) - 1) to_power m)) * (2 to_power (2 * k))) >= (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) by XREAL_1: 64;

              then (((2 to_power m) * (2 to_power (2 * k))) - (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) >= (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)));

              then ((2 to_power (m + (2 * k))) - (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) >= (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) by Th2;

              then (((2 to_power (m + (2 * k))) - (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k)))) >= ((((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k)))) by XREAL_1: 72;

              then

               A28: ((((2 to_power m) * (2 to_power (2 * k))) - (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k)))) >= ((((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k)))) by Th2;



               A29: (( sqrt 5) - 1) > (1 - 1) by A2, XREAL_1: 9;

              ( sqrt (3 ^2 )) > ( sqrt 5) & ( sqrt 5) > ( sqrt 1) by SQUARE_1: 27;

              then 3 > ( sqrt 5) & ( sqrt 5) > 1 by SQUARE_1: 18, SQUARE_1:def 2;

              then

               A30: (3 - 1) > (( sqrt 5) - 1) & (( sqrt 5) - 1) > (1 - 1) by XREAL_1: 9;

              then

               A31: ((( sqrt 5) - 1) to_power m) > 0 by POWER: 34;

              (2 to_power (2 * k)) >= ((( sqrt 5) - 1) to_power (2 * k)) by A30, A1, POWER: 37;

              then ((2 to_power (2 * k)) * ((( sqrt 5) - 1) to_power m)) >= (((( sqrt 5) - 1) to_power (2 * k)) * ((( sqrt 5) - 1) to_power m)) by A31, XREAL_1: 64;

              then (((2 to_power (2 * k)) * ((( sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m))) >= ((((( sqrt 5) - 1) to_power (2 * k)) * ((( sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m))) by XREAL_1: 72;

              then ((((2 to_power m) - ((( sqrt 5) - 1) to_power m)) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k)))) >= ((((( sqrt 5) - 1) to_power (2 * k)) * ((( sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m))) by A28, XXREAL_0: 2;

              then ((((2 to_power m) * (2 to_power (2 * k))) - (((( sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k)))) >= (((( sqrt 5) - 1) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by Th2, A29;

              hence thesis by A20, A21, Th2;

            end;

          end;

          (( sqrt 5) - 1) > (1 - 1) by A2, XREAL_1: 9;

          then

           A32: ( - (( sqrt 5) - 1)) < 0 ;

          (((1 + ( sqrt 5)) * (1 - ( sqrt 5))) / (2 to_power 2)) = (((1 + ( sqrt 5)) * (1 - ( sqrt 5))) / (2 ^2 )) by POWER: 46

          .= (((1 ^2 ) - (( sqrt 5) ^2 )) / 4)

          .= ((1 - 5) / 4) by SQUARE_1:def 2

          .= ( - 1);



          then (( - 1) to_power k) = ((((1 + ( sqrt 5)) * (1 - ( sqrt 5))) to_power k) / ((2 to_power 2) to_power k)) by Th1

          .= ((((1 + ( sqrt 5)) * (1 - ( sqrt 5))) to_power k) / (2 to_power (2 * k))) by NEWTON: 9;

          then ((((((1 - ( sqrt 5)) to_power m) * (((1 + ( sqrt 5)) * (1 - ( sqrt 5))) to_power k)) / (2 to_power (2 * k))) / (2 to_power m)) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by A7, XCMPLX_1: 74;

          then (((((1 - ( sqrt 5)) to_power m) * (((1 + ( sqrt 5)) * (1 - ( sqrt 5))) to_power k)) / ((2 to_power (2 * k)) * (2 to_power m))) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by XCMPLX_1: 78;

          then (((((1 - ( sqrt 5)) to_power m) * (((1 + ( sqrt 5)) * (1 - ( sqrt 5))) to_power k)) / (2 to_power ((2 * k) + m))) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by Th2;

          then (((((1 - ( sqrt 5)) to_power m) * (((1 + ( sqrt 5)) to_power k) * ((1 - ( sqrt 5)) to_power k))) / (2 to_power ((2 * k) + m))) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by NEWTON: 7;

          then ((((((1 - ( sqrt 5)) to_power m) * ((1 - ( sqrt 5)) to_power k)) * ((1 + ( sqrt 5)) to_power k)) / (2 to_power ((2 * k) + m))) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)));

          then (((((1 - ( sqrt 5)) to_power (m + k)) * ((1 + ( sqrt 5)) to_power k)) / (2 to_power ((k + k) + m))) + 1) >= (((1 - ( sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by Th2, A32;

          then (((((1 - ( sqrt 5)) to_power n) * ((1 + ( sqrt 5)) to_power k)) / (2 to_power (k + n))) + 1) >= (((1 - ( sqrt 5)) / 2) to_power ((k + k) + m)) by A4, Th1;

          then (((((1 - ( sqrt 5)) to_power n) * ((1 + ( sqrt 5)) to_power k)) / ((2 to_power n) * (2 to_power k))) + 1) >= (tb to_power (k + n)) by Th2, A4, FIB_NUM:def 2;

          then (((((1 - ( sqrt 5)) to_power n) / (2 to_power n)) * (((1 + ( sqrt 5)) to_power k) / (2 to_power k))) + 1) >= (tb to_power (k + n)) by XCMPLX_1: 76;

          then (((((1 - ( sqrt 5)) / 2) to_power n) * (((1 + ( sqrt 5)) to_power k) / (2 to_power k))) + 1) >= (tb to_power (k + n)) by Th1;

          hence thesis by Th1, FIB_NUM:def 1, FIB_NUM:def 2;

        end;

        then (((tk * tbn) + 1) + ( tau to_power (n + k))) >= ((tb to_power (n + k)) + ( tau to_power (n + k))) by XREAL_1: 6;

        then ((( tau to_power (n + k)) + (tk * tbn)) + 1) >= (( tau to_power (n + k)) + (tb to_power (n + k)));

        then (((tk * tn) + (tk * tbn)) + 1) >= (( tau to_power (n + k)) + (tb to_power (n + k))) by Th2;

        then ((tk * (tn + tbn)) + 1) >= ( Lucas (n + k)) by FIB_NUM3: 21;

        hence thesis by FIB_NUM3: 21;

      end;

      (((( tau to_power k) * ( Lucas n)) + 1) - 1) < ( Lucas (n + k))

      proof

        defpred P[ Nat] means (( tau to_power $1) * ( Lucas n)) < ( Lucas (n + $1));

        tbn < 0 by Th7, A1;

        then ((tbn * tau ) - (tbn * tb)) < 0 ;

        then ((tbn * tau ) - (tbn * (tb to_power 1))) < 0 ;

        then ((tbn * tau ) - (tb to_power (n + 1))) < 0 by Th2;

        then (((tbn * tau ) - (tb to_power (n + 1))) + (( tau to_power (n + 1)) + (tb to_power (n + 1)))) < ( 0 + (( tau to_power (n + 1)) + (tb to_power (n + 1)))) by XREAL_1: 6;

        then ((tbn * tau ) + ( tau to_power (n + 1))) < ( Lucas (n + 1)) by FIB_NUM3: 21;

        then ((tbn * tau ) + (tn * ( tau to_power 1))) < ( Lucas (n + 1)) by Th2;

        then ((tbn * tau ) + (tn * tau )) < ( Lucas (n + 1));

        then ((tbn + tn) * tau ) < ( Lucas (n + 1));

        then (( Lucas n) * tau ) < ( Lucas (n + 1)) by FIB_NUM3: 21;

        then

         A33: P[1];



         A34: for m be non zero Nat st P[m] holds P[(m + 1)]

        proof

          let m be non zero Nat;

          assume P[m];



           A35: ((1 - ( sqrt 5)) to_power (m + 1)) < ((1 + ( sqrt 5)) to_power (m + 1))

          proof

            reconsider s = (m + 1) as Element of NAT by ORDINAL1:def 12;

            ((1 - ( sqrt 5)) to_power s) <= |.((1 - ( sqrt 5)) to_power s).| by ABSVALUE: 4;

            then

             A36: ((1 - ( sqrt 5)) to_power s) <= ( |.(1 - ( sqrt 5)).| to_power s) by SERIES_1: 2;

            ( sqrt 5) > ( sqrt 1) by SQUARE_1: 27;

            then ( - ( sqrt 5)) < ( - 1) by SQUARE_1: 18, XREAL_1: 24;

            then

             A37: (( - ( sqrt 5)) + 1) < (( - 1) + 1) by XREAL_1: 6;

            then

             A38: |.(1 - ( sqrt 5)).| = ( - (1 - ( sqrt 5))) by ABSVALUE:def 1;

            ( - (1 - ( sqrt 5))) = (( - 1) + ( sqrt 5));

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

            then ( |.(1 - ( sqrt 5)).| to_power s) < ((1 + ( sqrt 5)) to_power s) by A38, A37, POWER: 37;

            hence thesis by A36, XXREAL_0: 2;

          end;

          (2 to_power (m + 1)) > 0 by POWER: 34;

          then (((1 - ( sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1))) < (((1 + ( sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1))) by A35, XREAL_1: 74;

          then (((1 - ( sqrt 5)) / 2) to_power (m + 1)) < (((1 + ( sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1))) by Th1;

          then (tb to_power (m + 1)) < ( tau to_power (m + 1)) & tbn < 0 by A1, Th7, Th1, FIB_NUM:def 1, FIB_NUM:def 2;

          then ((tb to_power (m + 1)) * tbn) > (( tau to_power (m + 1)) * tbn) by XREAL_1: 69;

          then (((tb to_power (m + 1)) * tbn) + ( tau to_power ((n + m) + 1))) > ((( tau to_power (m + 1)) * tbn) + ( tau to_power ((n + m) + 1))) by XREAL_1: 6;

          then ((tb to_power ((m + 1) + n)) + ( tau to_power ((n + m) + 1))) > ((( tau to_power (m + 1)) * tbn) + ( tau to_power ((n + m) + 1))) by Th2;

          then ((tb to_power ((m + 1) + n)) + ( tau to_power ((n + m) + 1))) > ((( tau to_power (m + 1)) * tbn) + (tn * ( tau to_power (m + 1)))) by Th2;

          then ( Lucas ((n + m) + 1)) > (( tau to_power (m + 1)) * (tbn + tn)) by FIB_NUM3: 21;

          hence thesis by FIB_NUM3: 21;

        end;

        for m be non zero Nat holds P[m] from NAT_1:sch 10( A33, A34);

        hence thesis by A1;

      end;

      hence thesis by A3, INT_1:def 6;

    end;