fib_num3.miz



    begin

    reserve a,b,n for Element of NAT ;

    theorem :: FIB_NUM3:1

    for a be Real, n be Element of NAT st (a to_power n) = 0 holds a = 0

    proof

      let a be Real, n be Element of NAT ;

      assume (a to_power n) = 0 ;

      then

       A1: (a |^ n) = 0 by POWER: 41;

      assume a <> 0 ;

      hence thesis by A1, PREPOWER: 5;

    end;

    theorem :: FIB_NUM3:2

    

     Th2: for a be non negative Real holds (( sqrt a) * ( sqrt a)) = a

    proof

      let a be non negative Real;

      a = ( sqrt (a ^2 )) by SQUARE_1: 22

      .= (( sqrt a) * ( sqrt a)) by SQUARE_1: 29;

      hence thesis;

    end;

    theorem :: FIB_NUM3:3

    

     Th3: for a be Real holds (a to_power 2) = (( - a) to_power 2)

    proof

      let a be Real;

      2 = (1 * 2);

      then 2 is even by ABIAN:def 2;

      hence thesis by POWER: 47;

    end;

    theorem :: FIB_NUM3:4

    

     Th4: for k be non zero Nat holds ((k -' 1) + 2) = ((k + 2) -' 1)

    proof

      let k be non zero Nat;

      k >= 1 by NAT_2: 19;

      hence thesis by NAT_D: 38;

    end;

    theorem :: FIB_NUM3:5

    

     Th5: ((a + b) |^ 2) = ((((a * a) + (a * b)) + (a * b)) + (b * b))

    proof

      ((a + b) |^ 2) = ((a + b) * (a + b)) by WSIERP_1: 1

      .= ((((a * a) + (a * b)) + (b * a)) + (b * b));

      hence thesis;

    end;

    theorem :: FIB_NUM3:6

    

     Th6: for a be non zero Real holds ((a to_power n) to_power 2) = (a to_power (2 * n))

    proof

      let a be non zero Real;

      ((a to_power n) to_power 2) = ((a to_power n) to_power (1 + 1))

      .= (((a to_power n) to_power 1) * ((a to_power n) to_power 1)) by FIB_NUM2: 5

      .= ((a to_power n) * ((a to_power n) to_power 1)) by POWER: 25

      .= ((a to_power n) * (a to_power n)) by POWER: 25

      .= (a to_power (n + n)) by FIB_NUM2: 5

      .= (a to_power (2 * n));

      hence thesis;

    end;

    theorem :: FIB_NUM3:7

    

     Th7: for a,b be Real holds ((a + b) * (a - b)) = ((a to_power 2) - (b to_power 2))

    proof

      let a,b be Real;

      ((a + b) * (a - b)) = ((a ^2 ) - (b ^2 ))

      .= ((a to_power 2) - (b ^2 )) by POWER: 46

      .= ((a to_power 2) - (b to_power 2)) by POWER: 46;

      hence thesis;

    end;

    theorem :: FIB_NUM3:8

    

     Th8: for a,b be non zero Real holds ((a * b) to_power n) = ((a to_power n) * (b to_power n))

    proof

      let a,b be non zero Real;

      

       A1: (b #Z n) = (b to_power n) by POWER: 43;

      ((a * b) #Z n) = ((a * b) to_power n) & (a #Z n) = (a to_power n) by POWER: 43;

      hence thesis by A1, PREPOWER: 40;

    end;

    registration

      cluster tau -> positive;

      coherence by FIB_NUM2: 33;

      cluster tau_bar -> negative;

      coherence by FIB_NUM2: 36;

    end

    theorem :: FIB_NUM3:9

    

     Th9: for n be Nat holds (( tau to_power n) + ( tau to_power (n + 1))) = ( tau to_power (n + 2))

    proof

      defpred P[ Nat] means (( tau to_power $1) + ( tau to_power ($1 + 1))) = ( tau to_power ($1 + 2));

      let n be Nat;

      

       A1: (( tau to_power 0 ) + ( tau to_power ( 0 + 1))) = (1 + ( tau to_power 1)) by POWER: 24

      .= (1 + ((1 + ( sqrt 5)) / 2)) by FIB_NUM:def 1, POWER: 25

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

      .= ((((1 + ( sqrt 5)) + ( sqrt 5)) + ( sqrt (5 ^2 ))) / 4) by SQUARE_1: 22

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

      .= ( tau * tau ) by FIB_NUM:def 1

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

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

      .= ( tau to_power (1 + 1)) by POWER: 27

      .= ( tau to_power ( 0 + 2));

      

       A2: (1 + tau ) = (1 + ( tau to_power 1)) by POWER: 25

      .= ( tau to_power ( 0 + 2)) by A1, POWER: 24;

      

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

      proof

        let k be Nat;

        assume that P[k] and P[(k + 1)];

        (( tau to_power (k + 2)) + ( tau to_power ((k + 2) + 1))) = (( tau to_power (k + 2)) + (( tau to_power (k + 2)) * ( tau to_power 1))) by POWER: 27

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

        .= (( tau to_power (k + 2)) * ( tau to_power 2)) by A2, POWER: 25

        .= ( tau to_power ((k + 2) + 2)) by POWER: 27;

        hence thesis;

      end;

      (( tau to_power 1) + ( tau to_power (1 + 1))) = ( tau + ( tau to_power (1 + 1))) by POWER: 25

      .= ( tau + (( tau to_power 1) * ( tau to_power 1))) by POWER: 27

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

      .= ( tau + ( tau * tau )) by POWER: 25

      .= ( tau * (1 + tau ))

      .= (( tau to_power 1) * ( tau to_power 2)) by A2, POWER: 25

      .= ( tau to_power (1 + 2)) by POWER: 27;

      then

       A4: P[1];

      

       A5: P[ 0 ] by A1;

      for k be Nat holds P[k] from FIB_NUM:sch 1( A5, A4, A3);

      hence thesis;

    end;

    theorem :: FIB_NUM3:10

    

     Th10: for n be Nat holds (( tau_bar to_power n) + ( tau_bar to_power (n + 1))) = ( tau_bar to_power (n + 2))

    proof

      defpred P[ Nat] means (( tau_bar to_power $1) + ( tau_bar to_power ($1 + 1))) = ( tau_bar to_power ($1 + 2));

      let n be Nat;

      

       A1: (( tau_bar to_power 0 ) + ( tau_bar to_power ( 0 + 1))) = (1 + ( tau_bar to_power 1)) by POWER: 24

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

      .= ((((1 - ( sqrt 5)) - ( sqrt 5)) + 5) / 4)

      .= ((((1 - ( sqrt 5)) - ( sqrt 5)) + ( sqrt (5 ^2 ))) / 4) by SQUARE_1: 22

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

      .= ( tau_bar * tau_bar ) by FIB_NUM:def 2

      .= (( tau_bar to_power 1) * tau_bar ) by POWER: 25

      .= (( tau_bar to_power 1) * ( tau_bar to_power 1)) by POWER: 25

      .= ( tau_bar to_power (1 + 1)) by FIB_NUM2: 5

      .= ( tau_bar to_power ( 0 + 2));

      

       A2: ( tau_bar + 1) = ( tau_bar + ( tau_bar to_power 0 )) by POWER: 24

      .= ( tau_bar to_power 2) by A1, POWER: 25;

      

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

      proof

        let k be Nat;

        assume that P[k] and P[(k + 1)];

        (( tau_bar to_power (k + 2)) + ( tau_bar to_power ((k + 2) + 1))) = (( tau_bar to_power (k + 2)) + (( tau_bar to_power (k + 2)) * ( tau_bar to_power 1))) by FIB_NUM2: 5

        .= (( tau_bar to_power (k + 2)) * (1 + ( tau_bar to_power 1)))

        .= (( tau_bar to_power (k + 2)) * ( tau_bar to_power 2)) by A2, POWER: 25

        .= ( tau_bar to_power ((k + 2) + 2)) by FIB_NUM2: 5;

        hence thesis;

      end;

      (( tau_bar to_power 1) + ( tau_bar to_power (1 + 1))) = ( tau_bar + ( tau_bar to_power (1 + 1))) by POWER: 25

      .= ( tau_bar + (( tau_bar to_power 1) * ( tau_bar to_power 1))) by FIB_NUM2: 5

      .= ( tau_bar + (( tau_bar to_power 1) * tau_bar )) by POWER: 25

      .= ( tau_bar + ( tau_bar * tau_bar )) by POWER: 25

      .= ( tau_bar * (1 + tau_bar ))

      .= (( tau_bar to_power 1) * ( tau_bar to_power 2)) by A2, POWER: 25

      .= ( tau_bar to_power (1 + 2)) by FIB_NUM2: 5;

      then

       A4: P[1];

      

       A5: P[ 0 ] by A1;

      for k be Nat holds P[k] from FIB_NUM:sch 1( A5, A4, A3);

      hence thesis;

    end;

    begin

    deffunc F( set, Element of [: NAT , NAT :]) = [($2 `2 ), (($2 `1 ) + ($2 `2 ))];

    definition

      :: FIB_NUM3:def1

      func Lucas -> sequence of [: NAT , NAT :] means

      : Def1: (it . 0 ) = [2, 1] & for n be Nat holds (it . (n + 1)) = [((it . n) `2 ), (((it . n) `1 ) + ((it . n) `2 ))];

      existence

      proof

        consider L be sequence of [: NAT , NAT :] such that

         A1: (L . 0 ) = [2, 1] & for n be Nat holds (L . (n + 1)) = F(n,.) from NAT_1:sch 12;

        take L;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let L1,L2 be sequence of [: NAT , NAT :] such that

         A3: (L1 . 0 ) = [2, 1] and

         A4: for n be Nat holds (L1 . (n + 1)) = F(n,.) and

         A6: (L2 . 0 ) = [2, 1] and

         A7: for n be Nat holds (L2 . (n + 1)) = F(n,.);

        thus L1 = L2 from NAT_1:sch 16( A3, A4, A6, A7);

      end;

    end

    definition

      let n be Nat;

      ::$Notion-Name

      :: FIB_NUM3:def2

      func Lucas (n) -> Element of NAT equals (( Lucas . n) `1 );

      coherence ;

    end

    theorem :: FIB_NUM3:11

    

     Th11: ( Lucas 0 ) = 2 & ( Lucas 1) = 1 & for n be Nat holds ( Lucas ((n + 1) + 1)) = (( Lucas n) + ( Lucas (n + 1)))

    proof

      set L = Lucas ;

      

       A1: (L . 0 ) = [2, 1] by Def1;

      

      thus ( Lucas 0 ) = ( [2, 1] `1 ) by Def1

      .= 2;

      

      thus ( Lucas 1) = ((L . ( 0 + 1)) `1 )

      .= ( [((L . 0 ) `2 ), (((L . 0 ) `1 ) + ((L . 0 ) `2 ))] `1 ) by Def1

      .= 1 by A1;

      let n be Nat;

      

       A3: ((L . (n + 1)) `1 ) = ( [((L . n) `2 ), (((L . n) `1 ) + ((L . n) `2 ))] `1 ) by Def1

      .= ((L . n) `2 );

      

      thus ( Lucas ((n + 1) + 1)) = ( [((L . (n + 1)) `2 ), (((L . (n + 1)) `1 ) + ((L . (n + 1)) `2 ))] `1 ) by Def1

      .= ( [((L . n) `2 ), (((L . n) `1 ) + ((L . n) `2 ))] `2 ) by Def1

      .= (( Lucas n) + ( Lucas (n + 1))) by A3;

    end;

    theorem :: FIB_NUM3:12

    

     Th12: for n be Nat holds ( Lucas (n + 2)) = (( Lucas n) + ( Lucas (n + 1)))

    proof

      let n be Nat;

      

      thus ( Lucas (n + 2)) = ( Lucas ((n + 1) + 1))

      .= (( Lucas n) + ( Lucas (n + 1))) by Th11;

    end;

    theorem :: FIB_NUM3:13

    

     Th13: for n be Nat holds (( Lucas (n + 1)) + ( Lucas (n + 2))) = ( Lucas (n + 3))

    proof

      let n be Nat;

      (( Lucas (n + 1)) + ( Lucas (n + 2))) = ( Lucas (((n + 1) + 1) + 1)) by Th11

      .= ( Lucas (n + 3));

      hence thesis;

    end;

    theorem :: FIB_NUM3:14

    

     Th14: ( Lucas 2) = 3

    proof

      ( Lucas 2) = ( Lucas (( 0 + 1) + 1))

      .= (2 + 1) by Th11

      .= 3;

      hence thesis;

    end;

    theorem :: FIB_NUM3:15

    

     Th15: ( Lucas 3) = 4

    proof

      ( Lucas 3) = ( Lucas ((1 + 1) + 1))

      .= (3 + 1) by Th11, Th14

      .= 4;

      hence thesis;

    end;

    theorem :: FIB_NUM3:16

    

     Th16: ( Lucas 4) = 7

    proof

      ( Lucas 4) = ( Lucas (((1 + 1) + 1) + 1))

      .= (4 + 3) by Th11, Th14, Th15

      .= 7;

      hence thesis;

    end;

    theorem :: FIB_NUM3:17

    

     Th17: for k be Nat holds ( Lucas k) >= k

    proof

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

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        per cases ;

          suppose k = 0 ;

          hence thesis by Th14;

        end;

          suppose k <> 0 ;

          then

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

          

           A6: (k + (k + 1)) <= (( Lucas k) + (k + 1)) by A3, XREAL_1: 6;

          ( Lucas ((k + 1) + 1)) = (( Lucas (k + 1)) + ( Lucas k)) & (( Lucas k) + (k + 1)) <= (( Lucas (k + 1)) + ( Lucas k)) by A4, Th11, XREAL_1: 6;

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

          hence thesis by A5, XXREAL_0: 2;

        end;

      end;

      

       A7: P[1] by Th11;

      thus for k be Nat holds P[k] from FIB_NUM:sch 1( A1, A7, A2);

    end;

    theorem :: FIB_NUM3:18

    for m be non zero Element of NAT holds ( Lucas (m + 1)) >= ( Lucas m)

    proof

      let m be non zero Element of NAT ;

      thus ( Lucas (m + 1)) >= ( Lucas m)

      proof

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

        

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

        proof

          let k be non zero Nat;

          assume that P[k] and P[(k + 1)];

          (( Lucas (k + 2)) + ( Lucas (k + 1))) = ( Lucas (k + 3)) by Th13;

          hence P[(k + 2)] by NAT_1: 12;

        end;

        

         A2: P[2] by Th14, Th15;

        

         A3: P[1] by Th11, Th14;

        for k be non zero Nat holds P[k] from FIB_NUM2:sch 1( A3, A2, A1);

        hence thesis;

      end;

    end;

    registration

      let n be Element of NAT ;

      cluster ( Lucas n) -> positive;

      coherence

      proof

        per cases ;

          suppose n = 0 ;

          hence thesis by Th11;

        end;

          suppose n <> 0 ;

          hence thesis by Th17;

        end;

      end;

    end

    theorem :: FIB_NUM3:19

    for n be Element of NAT holds (2 * ( Lucas (n + 2))) = (( Lucas n) + ( Lucas (n + 3)))

    proof

      let n be Element of NAT ;

      

       A1: (( Lucas (n + 1)) + ( Lucas (n + 2))) = ( Lucas (n + 3)) by Th13;

      

      thus (2 * ( Lucas (n + 2))) = (( Lucas (n + 2)) + ( Lucas (n + 2)))

      .= ((( Lucas (n + 1)) + ( Lucas n)) + ( Lucas (n + 2))) by Th12

      .= (( Lucas n) + ( Lucas (n + 3))) by A1;

    end;

    theorem :: FIB_NUM3:20

    for n be Nat holds ( Lucas (n + 1)) = (( Fib n) + ( Fib (n + 2)))

    proof

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

      

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

      proof

        let k be Nat;

        assume

         A2: P[k] & P[(k + 1)];

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

        then

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

        ( Lucas ((k + 2) + 1)) = (( Lucas (k + 1)) + ( Lucas ((k + 1) + 1))) by Th11

        .= (((( Fib k) + ( Fib (k + 1))) + ( Fib (k + 2))) + ( Fib ((k + 1) + 2))) by A2

        .= ((( Fib ((k + 1) + 1)) + ( Fib (k + 2))) + ( Fib ((k + 1) + 2))) by PRE_FF: 1

        .= (( Fib (k + 2)) + ( Fib ((k + 2) + 2))) by A3;

        hence thesis;

      end;

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

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

      then

       A4: P[1] by Th14, PRE_FF: 1;

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

      then

       A5: P[ 0 ] by Th11, PRE_FF: 1;

      thus for k be Nat holds P[k] from FIB_NUM:sch 1( A5, A4, A1);

    end;

    theorem :: FIB_NUM3:21

    

     Th21: for n be Nat holds ( Lucas n) = (( tau to_power n) + ( tau_bar to_power n))

    proof

      defpred P[ Nat] means ( Lucas $1) = (( tau to_power $1) + ( tau_bar to_power $1));

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

      

      then (( tau to_power 0 ) + ( tau_bar to_power 0 )) = (1 + 1) by POWER: 24

      .= 2;

      then

       A1: P[ 0 ] by Th11;

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        ( Lucas (k + 2)) = ((( tau to_power k) + ( tau_bar to_power k)) + ( Lucas (k + 1))) by A3, Th12

        .= (((( tau to_power k) + ( tau to_power (k + 1))) + ( tau_bar to_power k)) + ( tau_bar to_power (k + 1))) by A4

        .= ((( tau to_power (k + 2)) + ( tau_bar to_power k)) + ( tau_bar to_power (k + 1))) by Th9

        .= (( tau to_power (k + 2)) + (( tau_bar to_power k) + ( tau_bar to_power (k + 1))))

        .= (( tau to_power (k + 2)) + ( tau_bar to_power (k + 2))) by Th10;

        hence thesis;

      end;

      ( tau_bar to_power 1) = tau_bar & ( tau to_power 1) = tau by POWER: 25;

      then

       A5: P[1] by Th11, FIB_NUM:def 1, FIB_NUM:def 2;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:22

    for n be Nat holds ((2 * ( Lucas n)) + ( Lucas (n + 1))) = (5 * ( Fib (n + 1)))

    proof

      defpred P[ Nat] means ((2 * ( Lucas $1)) + ( Lucas ($1 + 1))) = (5 * ( Fib ($1 + 1)));

      

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

      proof

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        ((2 * ( Lucas (k + 2))) + ( Lucas ((k + 2) + 1))) = ((2 * ( Lucas (k + 2))) + ( Lucas (k + (2 + 1))))

        .= ((2 * ( Lucas (k + 2))) + (( Lucas (k + 1)) + ( Lucas (k + 2)))) by Th13

        .= (((2 * ( Lucas (k + 2))) + ( Lucas (k + 1))) + ( Lucas (k + 2)))

        .= (((2 * ( Lucas (k + 2))) + ( Lucas (k + 1))) + (( Lucas k) + ( Lucas (k + 1)))) by Th12

        .= ((( Lucas (k + 2)) + ((2 * ( Lucas (k + 1))) + ( Lucas (k + 2)))) + ( Lucas k))

        .= (((( Lucas k) + ( Lucas (k + 1))) + (5 * ( Fib (k + 2)))) + ( Lucas k)) by A3, Th12

        .= ((5 * ( Fib (k + 1))) + (5 * ( Fib (k + 2)))) by A2

        .= (5 * (( Fib (k + 1)) + ( Fib (k + (1 + 1)))))

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

        .= (5 * ( Fib ((k + 2) + 1)));

        hence thesis;

      end;

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

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

      then

       A4: P[1] by Th11, Th14;

      

       A5: P[ 0 ] by Th11, PRE_FF: 1;

      thus for k be Nat holds P[k] from FIB_NUM:sch 1( A5, A4, A1);

    end;

    theorem :: FIB_NUM3:23

    

     Th23: for n be Nat holds (( Lucas (n + 3)) - (2 * ( Lucas n))) = (5 * ( Fib n))

    proof

      defpred P[ Nat] means (( Lucas ($1 + 3)) - (2 * ( Lucas $1))) = (5 * ( Fib $1));

      

       A1: P[1] by Th11, Th16, PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        (( Lucas ((k + 2) + 3)) - (2 * ( Lucas (k + 2)))) = (( Lucas (((((k + 1) + 1) + 1) + 1) + 1)) - (2 * ( Lucas (k + 2))))

        .= ((( Lucas (k + 3)) + ( Lucas (k + 4))) - (2 * ( Lucas (k + 2)))) by Th11;

        

        then (( Lucas ((k + 2) + 3)) - (2 * ( Lucas (k + 2)))) = ((( Lucas (k + 3)) + ( Lucas (k + 4))) - (2 * (( Lucas k) + ( Lucas (k + 1))))) by Th12

        .= ((( Lucas (k + 4)) - (2 * ( Lucas (k + 1)))) + (5 * ( Fib k))) by A3

        .= ((5 * ( Fib k)) + (5 * ( Fib (k + 1)))) by A4

        .= (5 * (( Fib k) + ( Fib (k + 1))))

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

        .= (5 * ( Fib (k + 2)));

        hence thesis;

      end;

      

       A5: P[ 0 ] by Th11, Th15, PRE_FF: 1;

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

    end;

    theorem :: FIB_NUM3:24

    for n be Nat holds (( Lucas n) + ( Fib n)) = (2 * ( Fib (n + 1)))

    proof

      defpred P[ Nat] means (( Lucas $1) + ( Fib $1)) = (2 * ( Fib ($1 + 1)));

      let n be Nat;

      

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

      proof

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        (( Lucas (k + 2)) + ( Fib (k + 2))) = ((( Lucas k) + ( Lucas (k + 1))) + ( Fib (k + 2))) by Th12

        .= ((( Lucas k) + ( Lucas (k + 1))) + (( Fib k) + ( Fib (k + 1)))) by FIB_NUM2: 24

        .= ((2 * ( Fib (k + 1))) + (2 * ( Fib ((k + 1) + 1)))) by A2, A3

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

        .= (2 * ( Fib (k + 3))) by FIB_NUM2: 25

        .= (2 * ( Fib ((k + 2) + 1)));

        hence thesis;

      end;

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

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

      then

       A4: P[1] by Th11, PRE_FF: 1;

      

       A5: P[ 0 ] by Th11, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:25

    for n be Nat holds ((3 * ( Fib n)) + ( Lucas n)) = (2 * ( Fib (n + 2)))

    proof

      defpred P[ Nat] means ((3 * ( Fib $1)) + ( Lucas $1)) = (2 * ( Fib ($1 + 2)));

      let n be Nat;

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

      then

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

      

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

      proof

        let k be Nat;

        assume

         A3: P[k] & P[(k + 1)];

        ((3 * ( Fib (k + 2))) + ( Lucas (k + 2))) = ((3 * (( Fib k) + ( Fib (k + 1)))) + ( Lucas (k + 2))) by FIB_NUM2: 24

        .= (((3 * ( Fib k)) + (3 * ( Fib (k + 1)))) + (( Lucas k) + ( Lucas (k + 1)))) by Th12

        .= ((2 * ( Fib (k + 2))) + (2 * ( Fib ((k + 1) + 2)))) by A3

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

        .= (2 * ( Fib ((k + 2) + 2))) by FIB_NUM2: 24;

        hence thesis;

      end;

      ((( 0 + 1) + 1) + 1) = 3;

      then ( Fib 3) = 2 by A1, PRE_FF: 1;

      then

       A4: P[1] by Th11, PRE_FF: 1;

      

       A5: P[ 0 ] by A1, Th11, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:26

    for n,m be Element of NAT holds (2 * ( Lucas (n + m))) = ((( Lucas n) * ( Lucas m)) + ((5 * ( Fib n)) * ( Fib m)))

    proof

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

       A1:

      now

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        thus P[(k + 2)]

        proof

          let n;

          

           A4: (2 * ( Lucas (n + (k + 1)))) = ((( Lucas n) * ( Lucas (k + 1))) + ((5 * ( Fib n)) * ( Fib (k + 1)))) by A3;

          (2 * ( Lucas (n + (k + 2)))) = (2 * ( Lucas ((n + k) + 2)))

          .= (2 * (( Lucas (n + k)) + ( Lucas ((n + k) + 1)))) by Th12

          .= ((2 * ( Lucas (n + k))) + (2 * ( Lucas ((n + k) + 1))))

          .= (((( Lucas n) * ( Lucas k)) + ((5 * ( Fib n)) * ( Fib k))) + (2 * ( Lucas (n + (k + 1))))) by A2

          .= ((( Lucas n) * (( Lucas k) + ( Lucas (k + 1)))) + ((5 * ( Fib n)) * (( Fib k) + ( Fib (k + 1))))) by A4

          .= ((( Lucas n) * ( Lucas (k + 2))) + ((5 * ( Fib n)) * (( Fib k) + ( Fib (k + 1))))) by Th12

          .= ((( Lucas n) * ( Lucas (k + 2))) + ((5 * ( Fib n)) * ( Fib (k + 2)))) by FIB_NUM2: 24;

          hence thesis;

        end;

      end;

      

       A5: P[1]

      proof

        let n be Element of NAT ;

        (2 * ( Lucas (n + 1))) = (((( Lucas (n + 1)) + ( Lucas n)) + ( Lucas (n + 1))) - ( Lucas n))

        .= ((( Lucas (n + 1)) + ( Lucas (n + 2))) - ( Lucas n)) by Th12

        .= (( Lucas (n + 3)) - ( Lucas n)) by Th13

        .= (( Lucas n) + (( Lucas (n + 3)) - (2 * ( Lucas n))))

        .= ((( Lucas n) * ( Lucas 1)) + ((5 * ( Fib n)) * ( Fib 1))) by Th11, Th23, PRE_FF: 1;

        hence thesis;

      end;

      

       A6: P[ 0 ] by Th11, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:27

    for n be Element of NAT holds (( Lucas (n + 3)) * ( Lucas n)) = ((( Lucas (n + 2)) |^ 2) - (( Lucas (n + 1)) |^ 2))

    proof

      defpred P[ Nat] means (( Lucas ($1 + 3)) * ( Lucas $1)) = ((( Lucas ($1 + 2)) |^ 2) - (( Lucas ($1 + 1)) |^ 2));

      

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

      proof

        let k be Nat;

        assume that P[k] and P[(k + 1)];

        (( Lucas ((k + 2) + 3)) * ( Lucas (k + 2))) = (( Lucas ((k + 3) + 2)) * ( Lucas (k + 2)))

        .= ((( Lucas (k + 3)) + ( Lucas ((k + 3) + 1))) * ( Lucas (k + 2))) by Th12

        .= ((( Lucas (k + 3)) + ( Lucas ((k + 2) + 2))) * ( Lucas (k + 2)))

        .= ((( Lucas (k + 3)) + (( Lucas (k + 2)) + ( Lucas ((k + 2) + 1)))) * ( Lucas (k + 2))) by Th12

        .= (((( Lucas (k + 2)) + ( Lucas (k + 3))) * (( Lucas (k + 2)) + ( Lucas ((k + 2) + 1)))) - (( Lucas (k + 3)) * ( Lucas (k + 3))))

        .= (((( Lucas (k + 2)) + ( Lucas (k + 3))) * ( Lucas ((k + 2) + 2))) - (( Lucas (k + 3)) * ( Lucas (k + 3)))) by Th12

        .= (((( Lucas (k + 2)) + ( Lucas ((k + 2) + 1))) * ( Lucas (k + 4))) - (( Lucas (k + 3)) * ( Lucas (k + 3))))

        .= ((( Lucas ((k + 2) + 2)) * ( Lucas (k + 4))) - (( Lucas (k + 3)) * ( Lucas (k + 3)))) by Th12

        .= ((( Lucas (k + 4)) * ( Lucas (k + 4))) - (( Lucas (k + 3)) |^ 2)) by WSIERP_1: 1

        .= ((( Lucas ((k + 2) + 2)) |^ 2) - (( Lucas ((k + 2) + 1)) |^ 2)) by WSIERP_1: 1;

        hence thesis;

      end;

      (( Lucas (1 + 3)) * ( Lucas 1)) = ((4 * 4) - (3 * 3)) by Th11, Th16

      .= ((4 * 4) - (3 |^ 2)) by WSIERP_1: 1

      .= ((( Lucas (1 + 2)) |^ 2) - (( Lucas (1 + 1)) |^ 2)) by Th14, Th15, WSIERP_1: 1;

      then

       A2: P[1];

      ((( Lucas ( 0 + 2)) |^ 2) - (( Lucas ( 0 + 1)) |^ 2)) = ((3 * 3) - (( Lucas 1) |^ 2)) by Th14, WSIERP_1: 1

      .= (9 - (1 * 1)) by Th11, WSIERP_1: 1

      .= (( Lucas ( 0 + 3)) * ( Lucas 0 )) by Th11, Th15;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:28

    

     Th28: for n be Nat holds ( Fib (2 * n)) = (( Fib n) * ( Lucas n))

    proof

      let n be Nat;

      

       A1: n in NAT by ORDINAL1:def 12;

      (( Fib n) * ( Lucas n)) = (((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5)) * ( Lucas n)) by FIB_NUM: 7

      .= (((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5)) * (( tau to_power n) + ( tau_bar to_power n))) by Th21

      .= (((( tau to_power n) + ( tau_bar to_power n)) * (( tau to_power n) - ( tau_bar to_power n))) / ( sqrt 5)) by XCMPLX_1: 74

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

      .= (((( tau to_power n) to_power 2) - ( tau_bar to_power (2 * n))) / ( sqrt 5)) by A1, Th6

      .= ((( tau to_power (2 * n)) - ( tau_bar to_power (2 * n))) / ( sqrt 5)) by POWER: 33

      .= ( Fib (2 * n)) by FIB_NUM: 7;

      hence thesis;

    end;

    theorem :: FIB_NUM3:29

    for n be Element of NAT holds (2 * ( Fib ((2 * n) + 1))) = ((( Lucas (n + 1)) * ( Fib n)) + (( Lucas n) * ( Fib (n + 1))))

    proof

      defpred P[ Nat] means (2 * ( Fib ((2 * $1) + 1))) = ((( Lucas ($1 + 1)) * ( Fib $1)) + (( Lucas $1) * ( Fib ($1 + 1))));

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

      then

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

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        set f2 = ( Fib (k + 2));

        set f1 = ( Fib (k + 1));

        set f = ( Fib k);

        set l2 = ( Lucas (k + 2));

        set l1 = ( Lucas (k + 1));

        set l = ( Lucas k);

        

         A5: (2 * ( Fib (2 * k))) = (2 * (( Fib ((2 * k) + 2)) - ( Fib ((2 * k) + 1)))) by FIB_NUM2: 30

        .= (2 * (( Fib (((2 * k) + 1) + 1)) - ( Fib ((2 * k) + 1))))

        .= (2 * ((( Fib (((2 * k) + 1) + 2)) - ( Fib ((2 * k) + 1))) - ( Fib ((2 * k) + 1)))) by FIB_NUM2: 29

        .= ((2 * ( Fib ((2 * k) + 3))) - (2 * (2 * ( Fib ((2 * k) + 1)))))

        .= (((l2 * f1) + (l1 * f2)) - (2 * ((( Lucas (k + 1)) * ( Fib k)) + (( Lucas k) * ( Fib (k + 1)))))) by A3, A4

        .= ((((l2 * f1) + (l1 * f2)) - ((2 * l1) * f)) - ((2 * l) * f1))

        .= (((((l + l1) * f1) + (l1 * f2)) - ((2 * l1) * f)) - ((2 * l) * f1)) by Th12

        .= (((((l * f1) + (l1 * f1)) + (l1 * (f + f1))) - ((2 * l1) * f)) - ((2 * l) * f1)) by FIB_NUM2: 24

        .= ((((2 * l1) * f1) - (l * f1)) - (l1 * f));

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

        .= (2 * (( Fib ((2 * k) + 3)) + ( Fib (((2 * k) + 3) + 1)))) by FIB_NUM2: 24

        .= (2 * (( Fib ((2 * k) + 3)) + ( Fib (((2 * k) + 2) + 2))))

        .= (2 * (( Fib ((2 * k) + 3)) + (( Fib ((2 * k) + 2)) + ( Fib (((2 * k) + 2) + 1))))) by FIB_NUM2: 24

        .= (2 * ((( Fib ((2 * k) + 3)) + ( Fib (((2 * k) + 1) + 1))) + ( Fib ((2 * k) + 3))))

        .= (2 * ((( Fib ((2 * k) + 3)) + (( Fib (((2 * k) + 1) + 2)) - ( Fib ((2 * k) + 1)))) + ( Fib ((2 * k) + 3)))) by FIB_NUM2: 29

        .= ((3 * (2 * ( Fib ((2 * k) + 3)))) - (2 * ( Fib ((2 * k) + 1))))

        .= ((3 * ((( Lucas (k + 2)) * ( Fib (k + 1))) + (( Lucas (k + 1)) * ( Fib (k + 2))))) - (2 * ( Fib ((2 * k) + 1)))) by A4

        .= (((((3 * l2) * f1) + ((3 * l1) * f2)) - (l1 * f)) - (l * f1)) by A3

        .= (((((3 * (l + l1)) * f1) + ((3 * l1) * f2)) - (l1 * f)) - (l * f1)) by Th12

        .= ((((((3 * l) + (3 * l1)) * f1) + ((3 * l1) * (f + f1))) - (l1 * f)) - (l * f1)) by FIB_NUM2: 24

        .= (((((3 * l) * f1) + ((4 * l1) * f1)) + ((3 * l1) * f)) + ((((2 * l1) * f1) - (l * f1)) - (l1 * f)))

        .= (((((3 * l) * f1) + ((4 * l1) * f1)) + ((3 * l1) * f)) + (2 * (l * f))) by A5, Th28

        .= (((((((l * f1) + (l1 * f1)) + (l1 * (f + f1))) + ((2 * l) * f)) + ((2 * l) * f1)) + ((2 * l1) * f)) + ((2 * l1) * f1))

        .= (((((((l + l1) * f1) + (l1 * f2)) + ((2 * l) * f)) + ((2 * l) * f1)) + ((2 * l1) * f)) + ((2 * l1) * f1)) by FIB_NUM2: 24

        .= ((((((l2 * f1) + (l1 * f2)) + ((2 * l) * f)) + ((2 * l) * f1)) + ((2 * l1) * f)) + ((2 * l1) * f1)) by Th12

        .= (((( Lucas (k + 2)) * ( Fib (k + 1))) + (( Lucas (k + 1)) * ( Fib (k + 2)))) + (2 * ((((l * f) + (l * f1)) + (l1 * f)) + (l1 * f1))))

        .= ((2 * ( Fib ((2 * k) + 3))) + (2 * ((((l * f) + (l * f1)) + (l1 * f)) + (l1 * f1)))) by A4

        .= (2 * (( Fib ((2 * k) + 3)) + ((( Lucas k) + ( Lucas (k + 1))) * (( Fib k) + ( Fib (k + 1))))))

        .= (2 * (( Fib ((2 * k) + 3)) + ((( Lucas k) + ( Lucas (k + 1))) * ( Fib (k + 2))))) by FIB_NUM2: 24

        .= (2 * (( Fib ((2 * k) + 3)) + (( Lucas (k + 2)) * ( Fib (k + 2))))) by Th12

        .= (((2 * ( Fib ((2 * k) + 3))) + (( Lucas (k + 2)) * ( Fib (k + 2)))) + (( Lucas (k + 2)) * ( Fib (k + 2))))

        .= ((((( Lucas (k + 1)) * ( Fib (k + 2))) + (( Lucas (k + 2)) * ( Fib (k + 1)))) + (( Lucas (k + 2)) * ( Fib (k + 2)))) + (( Lucas (k + 2)) * ( Fib (k + 2)))) by A4

        .= (((( Lucas (k + 1)) + ( Lucas (k + 2))) * ( Fib (k + 2))) + (( Lucas (k + 2)) * (( Fib (k + 1)) + ( Fib (k + 2)))))

        .= (((( Lucas (k + 1)) + ( Lucas ((k + 1) + 1))) * ( Fib (k + 2))) + (( Lucas (k + 2)) * ( Fib ((k + 1) + 2)))) by FIB_NUM2: 24

        .= ((( Lucas ((k + 2) + 1)) * ( Fib (k + 2))) + (( Lucas (k + 2)) * ( Fib ((k + 2) + 1)))) by Th12;

        hence thesis;

      end;

      ((1 + 1) + 1) = 3;

      

      then (2 * ( Fib ((2 * 1) + 1))) = (2 * 2) by A1, PRE_FF: 1

      .= ((( Lucas (1 + 1)) * ( Fib 1)) + (( Lucas 1) * ( Fib (1 + 1)))) by A1, Th11, Th14, PRE_FF: 1;

      then

       A6: P[1];

      

       A7: P[ 0 ] by Th11, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:30

    for n be Element of NAT holds ((5 * (( Fib n) |^ 2)) - (( Lucas n) |^ 2)) = (4 * (( - 1) to_power (n + 1)))

    proof

      let n be Element of NAT ;

      set a = ( tau to_power n);

      set b = ( tau_bar to_power n);

      

       A1: (( Fib n) |^ 2) = (( Fib n) * ( Fib n)) by WSIERP_1: 1

      .= (((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5)) * ( Fib n)) by FIB_NUM: 7

      .= (((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5)) * ((( tau to_power n) - ( tau_bar to_power n)) / ( sqrt 5))) by FIB_NUM: 7

      .= (((a - b) * (a - b)) / (( sqrt 5) * ( sqrt 5))) by XCMPLX_1: 76

      .= ((((a * a) - ((2 * a) * b)) + (b * b)) / 5) by Th2;

      

       A2: (a * b) = (( tau * tau_bar ) to_power n) by Th8

      .= ((((1 * 1) - (( sqrt 5) * ( sqrt 5))) / 4) to_power n) by FIB_NUM:def 1, FIB_NUM:def 2

      .= (((1 - 5) / 4) to_power n) by Th2

      .= (( - 1) to_power n);

      (( Lucas n) |^ 2) = (( Lucas n) * ( Lucas n)) by WSIERP_1: 1

      .= ((( tau to_power n) + ( tau_bar to_power n)) * ( Lucas n)) by Th21

      .= ((( tau to_power n) + ( tau_bar to_power n)) * (( tau to_power n) + ( tau_bar to_power n))) by Th21

      .= (((a * a) + ((2 * a) * b)) + (b * b));

      

      then ((5 * (( Fib n) |^ 2)) - (( Lucas n) |^ 2)) = ((4 * ( - 1)) * (( - 1) to_power n)) by A1, A2

      .= ((4 * (( - 1) to_power 1)) * (( - 1) to_power n)) by POWER: 25

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

      .= (4 * (( - 1) to_power (n + 1))) by FIB_NUM2: 5;

      hence thesis;

    end;

    theorem :: FIB_NUM3:31

    for n be Element of NAT holds ( Fib ((2 * n) + 1)) = ((( Fib (n + 1)) * ( Lucas (n + 1))) - (( Fib n) * ( Lucas n)))

    proof

      let n be Element of NAT ;

      ((( Fib (n + 1)) * ( Lucas (n + 1))) - (( Fib n) * ( Lucas n))) = (( Fib (2 * (n + 1))) - (( Fib n) * ( Lucas n))) by Th28

      .= (( Fib ((2 * n) + 2)) - ( Fib (2 * n))) by Th28

      .= ( Fib ((2 * n) + 1)) by FIB_NUM2: 29;

      hence thesis;

    end;

    begin

    definition

      let a,b be Nat;

      :: original: [

      redefine

      func [a,b] -> Element of [: NAT , NAT :] ;

      coherence

      proof

        reconsider a, b as Element of NAT by ORDINAL1:def 12;

         [a, b] is Element of [: NAT , NAT :];

        hence thesis;

      end;

    end

    definition

      let a,b be Nat;

      deffunc F( set, Element of [: NAT , NAT :]) = [($2 `2 ), (($2 `1 ) + ($2 `2 ))];

      :: FIB_NUM3:def3

      func GenFib (a,b) -> sequence of [: NAT , NAT :] means

      : Def2: (it . 0 ) = [a, b] & for n be Nat holds (it . (n + 1)) = [((it . n) `2 ), (((it . n) `1 ) + ((it . n) `2 ))];

      existence

      proof

        consider L be sequence of [: NAT , NAT :] such that

         A1: (L . 0 ) = [a, b] & for n be Nat holds (L . (n + 1)) = F(n,.) from NAT_1:sch 12;

        take L;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let L1,L2 be sequence of [: NAT , NAT :] such that

         A3: (L1 . 0 ) = [a, b] and

         A4: for n be Nat holds (L1 . (n + 1)) = F(n,.) and

         A6: (L2 . 0 ) = [a, b] and

         A7: for n be Nat holds (L2 . (n + 1)) = F(n,.);

        thus L1 = L2 from NAT_1:sch 16( A3, A4, A6, A7);

      end;

    end

    definition

      let a,b,n be Nat;

      :: FIB_NUM3:def4

      func GenFib (a,b,n) -> Element of NAT equals ((( GenFib (a,b)) . n) `1 );

      coherence ;

    end

    theorem :: FIB_NUM3:32

    

     Th32: for a,b be Nat holds ( GenFib (a,b, 0 )) = a & ( GenFib (a,b,1)) = b & for n be Nat holds ( GenFib (a,b,((n + 1) + 1))) = (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1))))

    proof

      deffunc F( set, Element of [: NAT , NAT :]) = [($2 `2 ), (($2 `1 ) + ($2 `2 ))];

      let a,b be Nat;

      consider L be sequence of [: NAT , NAT :] such that

       A1: (L . 0 ) = [a, b] and

       A2: for n be Nat holds (L . (n + 1)) = F(n,.) from NAT_1:sch 12;

      

      thus ( GenFib (a,b, 0 )) = ( [a, b] `1 ) by Def2

      .= a;

      

      thus ( GenFib (a,b,1)) = ((L . ( 0 + 1)) `1 ) by A1, A2, Def2

      .= ( [((L . 0 ) `2 ), (((L . 0 ) `1 ) + ((L . 0 ) `2 ))] `1 ) by A2

      .= b by A1;

      let n be Nat;

      

       A3: ((L . (n + 1)) `1 ) = ( [((L . n) `2 ), (((L . n) `1 ) + ((L . n) `2 ))] `1 ) by A2

      .= ((L . n) `2 );

      ( GenFib (a,b,((n + 1) + 1))) = ((L . ((n + 1) + 1)) `1 ) by A1, A2, Def2

      .= ( [((L . (n + 1)) `2 ), (((L . (n + 1)) `1 ) + ((L . (n + 1)) `2 ))] `1 ) by A2

      .= ( [((L . n) `2 ), (((L . n) `1 ) + ((L . n) `2 ))] `2 ) by A2

      .= (( GenFib (a,b,n)) + ((L . (n + 1)) `1 )) by A1, A2, A3, Def2

      .= (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1)))) by A1, A2, Def2;

      hence thesis;

    end;

    theorem :: FIB_NUM3:33

    

     Th33: for k be Nat holds ((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) |^ 2) = (((( GenFib (a,b,(k + 1))) |^ 2) + ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,((k + 1) + 1))))) + (( GenFib (a,b,((k + 1) + 1))) |^ 2))

    proof

      let k be Nat;

      set a1 = ( GenFib (a,b,(k + 1)));

      set b1 = ( GenFib (a,b,((k + 1) + 1)));

      ((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) |^ 2) = ((((a1 * a1) + (a1 * b1)) + (b1 * a1)) + (b1 * b1)) by Th5

      .= (((a1 * a1) + (2 * (a1 * b1))) + (b1 * b1))

      .= (((a1 |^ 2) + ((2 * a1) * b1)) + (b1 * b1)) by WSIERP_1: 1

      .= (((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2)) by WSIERP_1: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM3:34

    

     Th34: for a,b,n be Nat holds (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1)))) = ( GenFib (a,b,(n + 2)))

    proof

      let a,b,n be Nat;

      (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1)))) = ( GenFib (a,b,((n + 1) + 1))) by Th32

      .= ( GenFib (a,b,(n + 2)));

      hence thesis;

    end;

    theorem :: FIB_NUM3:35

    

     Th35: for a,b,n be Nat holds (( GenFib (a,b,(n + 1))) + ( GenFib (a,b,(n + 2)))) = ( GenFib (a,b,(n + 3)))

    proof

      let a,b,n be Nat;

      (( GenFib (a,b,(n + 1))) + ( GenFib (a,b,(n + 2)))) = ( GenFib (a,b,(((n + 1) + 1) + 1))) by Th32

      .= ( GenFib (a,b,(n + 3)));

      hence thesis;

    end;

    theorem :: FIB_NUM3:36

    

     Th36: for a,b,n be Element of NAT holds (( GenFib (a,b,(n + 2))) + ( GenFib (a,b,(n + 3)))) = ( GenFib (a,b,(n + 4)))

    proof

      let a,b,n be Element of NAT ;

      (( GenFib (a,b,(n + 2))) + ( GenFib (a,b,(n + 3)))) = ( GenFib (a,b,((((n + 1) + 1) + 1) + 1))) by Th32

      .= ( GenFib (a,b,(n + 4)));

      hence thesis;

    end;

    theorem :: FIB_NUM3:37

    for n be Element of NAT holds ( GenFib ( 0 ,1,n)) = ( Fib n)

    proof

      defpred P[ Nat] means ( GenFib ( 0 ,1,$1)) = ( Fib $1);

      

       A1: P[1] by Th32, PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume P[k] & P[(k + 1)];

        

        then ( GenFib ( 0 ,1,(k + 2))) = (( Fib k) + ( Fib (k + 1))) by Th34

        .= ( Fib (k + 2)) by FIB_NUM2: 24;

        hence thesis;

      end;

      

       A3: P[ 0 ] by Th32, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:38

    

     Th38: for n be Element of NAT holds ( GenFib (2,1,n)) = ( Lucas n)

    proof

      defpred P[ Nat] means ( GenFib (2,1,$1)) = ( Lucas $1);

      

       A1: P[1] by Th11, Th32;

      

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

      proof

        let k be Nat;

        assume P[k] & P[(k + 1)];

        

        then ( GenFib (2,1,(k + 2))) = (( Lucas k) + ( Lucas (k + 1))) by Th34

        .= ( Lucas (k + 2)) by Th12;

        hence thesis;

      end;

      

       A3: P[ 0 ] by Th11, Th32;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:39

    

     Th39: for a,b,n be Element of NAT holds (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 3)))) = (2 * ( GenFib (a,b,(n + 2))))

    proof

      let a,b,n be Element of NAT ;

      (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 3)))) = (( GenFib (a,b,n)) + (( GenFib (a,b,(n + 1))) + ( GenFib (a,b,(n + 2))))) by Th35

      .= ((( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1)))) + ( GenFib (a,b,(n + 2))))

      .= (( GenFib (a,b,(n + 2))) + ( GenFib (a,b,(n + 2)))) by Th34

      .= (2 * ( GenFib (a,b,(n + 2))));

      hence thesis;

    end;

    theorem :: FIB_NUM3:40

    for a,b,n be Element of NAT holds (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 4)))) = (3 * ( GenFib (a,b,(n + 2))))

    proof

      let a,b,n be Element of NAT ;

      (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 4)))) = (( GenFib (a,b,n)) + (( GenFib (a,b,(n + 2))) + ( GenFib (a,b,(n + 3))))) by Th36

      .= ((( GenFib (a,b,n)) + ( GenFib (a,b,(n + 2)))) + ( GenFib (a,b,(n + 3))))

      .= ((( GenFib (a,b,n)) + ( GenFib (a,b,(n + 2)))) + (( GenFib (a,b,(n + 1))) + ( GenFib (a,b,(n + 2))))) by Th35

      .= (((( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1)))) + ( GenFib (a,b,(n + 2)))) + ( GenFib (a,b,(n + 2))))

      .= ((( GenFib (a,b,(n + 2))) + ( GenFib (a,b,(n + 2)))) + ( GenFib (a,b,(n + 2)))) by Th34

      .= (3 * ( GenFib (a,b,(n + 2))));

      hence thesis;

    end;

    theorem :: FIB_NUM3:41

    for a,b,n be Element of NAT holds (( GenFib (a,b,(n + 3))) - ( GenFib (a,b,n))) = (2 * ( GenFib (a,b,(n + 1))))

    proof

      let a,b,n be Element of NAT ;

      (( GenFib (a,b,(n + 3))) - ( GenFib (a,b,n))) = ((( GenFib (a,b,(n + 1))) + ( GenFib (a,b,(n + 2)))) - ( GenFib (a,b,n))) by Th35

      .= ((( GenFib (a,b,(n + 1))) + (( GenFib (a,b,n)) + ( GenFib (a,b,(n + 1))))) - ( GenFib (a,b,n))) by Th34

      .= (2 * ( GenFib (a,b,(n + 1))));

      hence thesis;

    end;

    theorem :: FIB_NUM3:42

    for a,b,n be non zero Element of NAT holds ( GenFib (a,b,n)) = ((( GenFib (a,b, 0 )) * ( Fib (n -' 1))) + (( GenFib (a,b,1)) * ( Fib n)))

    proof

      let a,b,n be non zero Element of NAT ;

      thus ( GenFib (a,b,n)) = ((( GenFib (a,b, 0 )) * ( Fib (n -' 1))) + (( GenFib (a,b,1)) * ( Fib n)))

      proof

        defpred P[ Nat] means ( GenFib (a,b,$1)) = ((( GenFib (a,b, 0 )) * ( Fib ($1 -' 1))) + (( GenFib (a,b,1)) * ( Fib $1)));

        ( GenFib (a,b,1)) = ((( GenFib (a,b, 0 )) * ( Fib 0 )) + (( GenFib (a,b,1)) * ( Fib 1))) by PRE_FF: 1

        .= ((( GenFib (a,b, 0 )) * ( Fib (1 -' 1))) + (( GenFib (a,b,1)) * ( Fib 1))) by XREAL_1: 232;

        then

         A1: P[1];

        

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

        proof

          let k be non zero Nat;

          assume that

           A3: P[k] and

           A4: P[(k + 1)];

          1 <= k by NAT_2: 19;

          

          then

           A5: (( Fib (k -' 1)) + ( Fib ((k + 1) -' 1))) = (( Fib (k -' 1)) + ( Fib ((k -' 1) + 1))) by NAT_D: 38

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

          .= ( Fib ((k -' 1) + 2))

          .= ( Fib ((k + 2) -' 1)) by Th4;

          ( GenFib (a,b,(k + 2))) = (((( GenFib (a,b, 0 )) * ( Fib (k -' 1))) + (( GenFib (a,b,1)) * ( Fib k))) + ( GenFib (a,b,(k + 1)))) by A3, Th34

          .= (((a * ( Fib (k -' 1))) + (( GenFib (a,b,1)) * ( Fib k))) + ( GenFib (a,b,(k + 1)))) by Th32

          .= (((a * ( Fib (k -' 1))) + (b * ( Fib k))) + ( GenFib (a,b,(k + 1)))) by Th32

          .= ((((a * ( Fib (k -' 1))) + (b * ( Fib k))) + (( GenFib (a,b, 0 )) * ( Fib ((k + 1) -' 1)))) + (( GenFib (a,b,1)) * ( Fib (k + 1)))) by A4

          .= ((((a * ( Fib (k -' 1))) + (b * ( Fib k))) + (a * ( Fib ((k + 1) -' 1)))) + (( GenFib (a,b,1)) * ( Fib (k + 1)))) by Th32

          .= ((((a * ( Fib (k -' 1))) + (b * ( Fib k))) + (a * ( Fib ((k + 1) -' 1)))) + (b * ( Fib (k + 1)))) by Th32

          .= ((a * (( Fib (k -' 1)) + ( Fib ((k + 1) -' 1)))) + (b * (( Fib k) + ( Fib (k + 1)))))

          .= ((a * ( Fib ((k + 2) -' 1))) + (b * ( Fib (k + 2)))) by A5, FIB_NUM2: 24

          .= ((a * ( Fib ((k + 2) -' 1))) + (( GenFib (a,b,1)) * ( Fib (k + 2)))) by Th32

          .= ((( GenFib (a,b, 0 )) * ( Fib ((k + 2) -' 1))) + (( GenFib (a,b,1)) * ( Fib (k + 2)))) by Th32;

          hence thesis;

        end;

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

        then

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

        ( GenFib (a,b,2)) = ( GenFib (a,b,( 0 + 2)))

        .= ((( GenFib (a,b, 0 )) * ( Fib (1 + 0 ))) + (( GenFib (a,b,1)) * ( Fib 2))) by A6, Th34, PRE_FF: 1

        .= ((( GenFib (a,b, 0 )) * ( Fib (1 + (1 -' 1)))) + (( GenFib (a,b,1)) * ( Fib 2))) by XREAL_1: 232

        .= ((( GenFib (a,b, 0 )) * ( Fib ((1 + 1) -' 1))) + (( GenFib (a,b,1)) * ( Fib 2))) by NAT_D: 38

        .= ((( GenFib (a,b, 0 )) * ( Fib (2 -' 1))) + (( GenFib (a,b,1)) * ( Fib 2)));

        then

         A7: P[2];

        for k be non zero Nat holds P[k] from FIB_NUM2:sch 1( A1, A7, A2);

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM3:43

    for n,m be Nat holds ((( Fib m) * ( Lucas n)) + (( Lucas m) * ( Fib n))) = ( GenFib (( Fib 0 ),( Lucas 0 ),(n + m)))

    proof

      let n,m be Nat;

      defpred P[ Nat] means ((( Fib $1) * ( Lucas n)) + (( Lucas $1) * ( Fib n))) = ( GenFib (( Fib 0 ),( Lucas 0 ),(n + $1)));

      (2 * ( Fib n)) = ( GenFib ( 0 ,2,n))

      proof

        defpred R[ Nat] means (2 * ( Fib $1)) = ( GenFib ( 0 ,2,$1));

        

         A1: R[1] by Th32, PRE_FF: 1;

        

         A2: for i be Nat st R[i] & R[(i + 1)] holds R[(i + 2)]

        proof

          let i be Nat;

          assume

           A3: R[i] & R[(i + 1)];

          (2 * ( Fib (i + 2))) = (2 * (( Fib i) + ( Fib (i + 1)))) by FIB_NUM2: 24

          .= ((2 * ( Fib i)) + (2 * ( Fib (i + 1))))

          .= ( GenFib ( 0 ,2,(i + 2))) by A3, Th34;

          hence thesis;

        end;

        

         A4: R[ 0 ] by Th32, PRE_FF: 1;

        for i be Nat holds R[i] from FIB_NUM:sch 1( A4, A1, A2);

        hence thesis;

      end;

      then

       A5: P[ 0 ] by Th11, PRE_FF: 1;

      (( Lucas n) + ( Fib n)) = ( GenFib ( 0 ,2,(n + 1)))

      proof

        defpred Q[ Nat] means (( Lucas $1) + ( Fib $1)) = ( GenFib ( 0 ,2,($1 + 1)));

        

         A6: for j be Nat st Q[j] & Q[(j + 1)] holds Q[(j + 2)]

        proof

          let j be Nat;

          assume

           A7: Q[j] & Q[(j + 1)];

          (( Lucas (j + 2)) + ( Fib (j + 2))) = ((( Lucas j) + ( Lucas (j + 1))) + ( Fib (j + 2))) by Th12

          .= ((( Lucas j) + ( Lucas (j + 1))) + (( Fib j) + ( Fib (j + 1)))) by FIB_NUM2: 24

          .= (( GenFib ( 0 ,2,(j + 1))) + ( GenFib ( 0 ,2,(j + 2)))) by A7

          .= ( GenFib ( 0 ,2,(j + 3))) by Th35

          .= ( GenFib ( 0 ,2,((j + 2) + 1)));

          hence thesis;

        end;

        (( Lucas 1) + ( Fib 1)) = ( 0 + ( GenFib ( 0 ,2,1))) by Th11, Th32, PRE_FF: 1

        .= (( GenFib ( 0 ,2,( 0 + 0 ))) + ( GenFib ( 0 ,2,( 0 + 1)))) by Th32

        .= ( GenFib ( 0 ,2,( 0 + 2))) by Th34

        .= ( GenFib ( 0 ,2,(1 + 1)));

        then

         A8: Q[1];

        

         A9: Q[ 0 ] by Th11, Th32, PRE_FF: 1;

        for j be Nat holds Q[j] from FIB_NUM:sch 1( A9, A8, A6);

        hence thesis;

      end;

      then

       A10: P[1] by Th11, PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume

         A12: P[k] & P[(k + 1)];

        ((( Fib (k + 2)) * ( Lucas n)) + (( Lucas (k + 2)) * ( Fib n))) = (((( Fib k) + ( Fib (k + 1))) * ( Lucas n)) + (( Lucas (k + 2)) * ( Fib n))) by FIB_NUM2: 24

        .= (((( Fib k) * ( Lucas n)) + (( Fib (k + 1)) * ( Lucas n))) + ((( Lucas k) + ( Lucas (k + 1))) * ( Fib n))) by Th12

        .= (( GenFib ( 0 ,2,(n + k))) + ( GenFib ( 0 ,2,((n + k) + 1)))) by A12, Th11, PRE_FF: 1

        .= ( GenFib ( 0 ,2,((n + k) + 2))) by Th34

        .= ( GenFib (( Fib 0 ),( Lucas 0 ),(n + (k + 2)))) by Th11, PRE_FF: 1;

        hence thesis;

      end;

      for k be Nat holds P[k] from FIB_NUM:sch 1( A5, A10, A11);

      hence thesis;

    end;

    theorem :: FIB_NUM3:44

    for n be Element of NAT holds (( Lucas n) + ( Lucas (n + 3))) = (2 * ( Lucas (n + 2)))

    proof

      let n be Element of NAT ;

      

       A1: (2 * ( GenFib (2,1,(n + 2)))) = (2 * ( Lucas (n + 2))) by Th38;

      ( GenFib (2,1,n)) = ( Lucas n) & ( GenFib (2,1,(n + 3))) = ( Lucas (n + 3)) by Th38;

      hence thesis by A1, Th39;

    end;

    theorem :: FIB_NUM3:45

    for a,n be Element of NAT holds ( GenFib (a,a,n)) = ((( GenFib (a,a, 0 )) / 2) * (( Fib n) + ( Lucas n)))

    proof

      let a,b be Element of NAT ;

      defpred P[ Nat] means ( GenFib (a,a,$1)) = ((( GenFib (a,a, 0 )) / 2) * (( Fib $1) + ( Lucas $1)));

      

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

      proof

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        ( GenFib (a,a,(k + 2))) = (((( GenFib (a,a, 0 )) / 2) * (( Fib k) + ( Lucas k))) + ( GenFib (a,a,(k + 1)))) by A2, Th34

        .= ((( GenFib (a,a, 0 )) / 2) * ((( Fib k) + ( Fib (k + 1))) + (( Lucas k) + ( Lucas (k + 1))))) by A3

        .= ((( GenFib (a,a, 0 )) / 2) * (( Fib (k + 2)) + (( Lucas k) + ( Lucas (k + 1))))) by FIB_NUM2: 24

        .= ((( GenFib (a,a, 0 )) / 2) * (( Fib (k + 2)) + ( Lucas (k + 2)))) by Th12;

        hence thesis;

      end;

      ( GenFib (a,a,1)) = a by Th32;

      then

       A4: P[1] by Th11, Th32, PRE_FF: 1;

      

       A5: P[ 0 ] by Th11, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:46

    for a,b,n be Element of NAT holds ( GenFib (b,(a + b),n)) = ( GenFib (a,b,(n + 1)))

    proof

      let a,b,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib (b,(a + b),$1)) = ( GenFib (a,b,($1 + 1)));

      

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

      proof

        let k be Nat;

        assume P[k] & P[(k + 1)];

        

        then ( GenFib (b,(a + b),(k + 2))) = (( GenFib (a,b,(k + 1))) + ( GenFib (a,b,(k + 2)))) by Th34

        .= ( GenFib (a,b,(k + 3))) by Th35

        .= ( GenFib (a,b,((k + 2) + 1)));

        hence thesis;

      end;

      ( GenFib (b,(a + b), 0 )) = b by Th32

      .= ( GenFib (a,b,( 0 + 1))) by Th32;

      then

       A2: P[ 0 ];

      ( GenFib (b,(a + b),1)) = (a + b) by Th32

      .= (a + ( GenFib (a,b,1))) by Th32

      .= (( GenFib (a,b, 0 )) + ( GenFib (a,b,( 0 + 1)))) by Th32

      .= ( GenFib (a,b,( 0 + 2))) by Th34

      .= ( GenFib (a,b,(1 + 1)));

      then

       A3: P[1];

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:47

    for a,b,n be Element of NAT holds ((( GenFib (a,b,(n + 2))) * ( GenFib (a,b,n))) - (( GenFib (a,b,(n + 1))) |^ 2)) = ((( - 1) to_power n) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3)))))

    proof

      let a,b,n be Element of NAT ;

      defpred P[ Nat] means ((( GenFib (a,b,($1 + 2))) * ( GenFib (a,b,$1))) - (( GenFib (a,b,($1 + 1))) |^ 2)) = ((( - 1) to_power $1) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3)))));

      

       A1: ( GenFib (a,b,2)) = ( GenFib (a,b,( 0 + 2)))

      .= (( GenFib (a,b, 0 )) + ( GenFib (a,b,( 0 + 1)))) by Th34

      .= (a + ( GenFib (a,b,1))) by Th32

      .= (a + b) by Th32;

      

       A2: ( GenFib (a,b,3)) = ( GenFib (a,b,(1 + 2)))

      .= (( GenFib (a,b,1)) + ( GenFib (a,b,(1 + 1)))) by Th32

      .= (b + (a + b)) by A1, Th32

      .= ((2 * b) + a);

      

      then ((( GenFib (a,b,(1 + 2))) * ( GenFib (a,b,1))) - (( GenFib (a,b,(1 + 1))) |^ 2)) = ((((2 * b) + a) * b) - ((a + b) |^ 2)) by A1, Th32

      .= ((((2 * b) * b) + (a * b)) - ((a + b) * (a + b))) by WSIERP_1: 1

      .= (( - 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a))))

      .= ((( - 1) to_power 1) * (((a + b) * (a + b)) - (b * ((2 * b) + a)))) by POWER: 25

      .= ((( - 1) to_power 1) * (((a + b) |^ 2) - (b * ( GenFib (a,b,3))))) by A2, WSIERP_1: 1

      .= ((( - 1) to_power 1) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by A1, Th32;

      then

       A3: P[1];

      

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

      proof

        let k be Nat;

        assume that

         A5: P[k] and

         A6: P[(k + 1)];

        set d = (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,k)));

        

         A7: ((( - 1) to_power (k + 1)) + (( - 1) to_power k)) = (((( - 1) to_power k) * (( - 1) to_power 1)) + (( - 1) to_power k)) by FIB_NUM2: 5

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

        .= 0 ;

        (( GenFib (a,b,2)) |^ 2) = (( GenFib (a,b,( 0 + 2))) |^ 2)

        .= ((( GenFib (a,b, 0 )) + ( GenFib (a,b,( 0 + 1)))) |^ 2) by Th34

        .= ((a + ( GenFib (a,b,1))) |^ 2) by Th32

        .= ((a + b) |^ 2) by Th32;

        

        then

         A8: ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3)))) = (((a + b) |^ 2) - (b * ( GenFib (a,b,(1 + 2))))) by Th32

        .= (((a + b) |^ 2) - (b * (( GenFib (a,b,1)) + ( GenFib (a,b,(1 + 1)))))) by Th34

        .= (((a + b) |^ 2) - (b * (b + ( GenFib (a,b,( 0 + 2)))))) by Th32

        .= (((a + b) |^ 2) - (b * (b + (( GenFib (a,b, 0 )) + ( GenFib (a,b,( 0 + 1))))))) by Th34

        .= (((a + b) |^ 2) - (b * (b + (a + ( GenFib (a,b,1)))))) by Th32

        .= (((a + b) |^ 2) - (b * (b + (a + b)))) by Th32

        .= (((((a + b) |^ 2) - (b * b)) - (b * a)) - (b * b))

        .= (((((((a * a) + (a * b)) + (b * a)) + (b * b)) - (b * b)) - (b * a)) - (b * b)) by Th5

        .= (((a * a) + (a * b)) - (b * b));

        then (d - (( GenFib (a,b,(k + 1))) |^ 2)) = ((( - 1) to_power k) * (((a * a) + (a * b)) - (b * b))) by A5;

        

        then

         A9: (((( - 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + (d - (( GenFib (a,b,(k + 1))) |^ 2))) = (((( - 1) to_power (k + 1)) + (( - 1) to_power k)) * (((a * a) + (a * b)) - (b * b)))

        .= ((((a * a) + (a * b)) - (b * b)) * 0 ) by A7;

        set c = (( GenFib (a,b,((k + 2) + 1))) * ( GenFib (a,b,(k + 1))));

        

         A10: (c - (( GenFib (a,b,((k + 1) + 1))) |^ 2)) = ((( - 1) to_power (k + 1)) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by A6;

        

         A11: ((c + d) - ((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) |^ 2)) = ((c + d) - (((( GenFib (a,b,(k + 1))) |^ 2) + ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,((k + 1) + 1))))) + (( GenFib (a,b,((k + 1) + 1))) |^ 2))) by Th33

        .= (((((( - 1) to_power (k + 1)) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) + d) - (( GenFib (a,b,(k + 1))) |^ 2)) - ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,((k + 1) + 1))))) by A10

        .= (((((( - 1) to_power (k + 1)) * (((a * a) + (a * b)) - (b * b))) + d) - (( GenFib (a,b,(k + 1))) |^ 2)) - ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,((k + 1) + 1))))) by A8

        .= ( - ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,((k + 1) + 1))))) by A9;

        ((( GenFib (a,b,((k + 2) + 2))) * ( GenFib (a,b,(k + 2)))) - (( GenFib (a,b,((k + 2) + 1))) |^ 2)) = (((( GenFib (a,b,(k + 2))) + ( GenFib (a,b,((k + 2) + 1)))) * ( GenFib (a,b,(k + 2)))) - (( GenFib (a,b,((k + 2) + 1))) |^ 2)) by Th34

        .= (((( GenFib (a,b,((k + 2) + 1))) + ( GenFib (a,b,(k + 2)))) * (( GenFib (a,b,k)) + ( GenFib (a,b,(k + 1))))) - (( GenFib (a,b,((k + 1) + 2))) |^ 2)) by Th34

        .= (((((( GenFib (a,b,((k + 2) + 1))) * ( GenFib (a,b,k))) + c) + d) + (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,(k + 1))))) - ((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) |^ 2)) by Th32

        .= (((( GenFib (a,b,((k + 2) + 1))) * ( GenFib (a,b,k))) + (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,(k + 1))))) + ((c + d) - ((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) |^ 2)))

        .= (((( GenFib (a,b,((k + 2) + 1))) * ( GenFib (a,b,k))) + (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,(k + 1))))) + ( - ((2 * ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,(k + 2)))))) by A11

        .= ((( GenFib (a,b,((k + 1) + 2))) * ( GenFib (a,b,k))) - (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,(k + 1)))))

        .= (((( GenFib (a,b,(k + 1))) + ( GenFib (a,b,((k + 1) + 1)))) * ( GenFib (a,b,k))) - (( GenFib (a,b,(k + 2))) * ( GenFib (a,b,(k + 1))))) by Th34

        .= (((( GenFib (a,b,(k + 1))) * ( GenFib (a,b,k))) + d) - ((( GenFib (a,b,k)) + ( GenFib (a,b,(k + 1)))) * ( GenFib (a,b,(k + 1))))) by Th34

        .= (d - (( GenFib (a,b,(k + 1))) * ( GenFib (a,b,(k + 1)))))

        .= (((( - 1) to_power k) * 1) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by A5, WSIERP_1: 1

        .= (((( - 1) to_power k) * (1 to_power 2)) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by POWER: 26

        .= (((( - 1) to_power k) * (( - 1) to_power 2)) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by Th3

        .= ((( - 1) to_power (k + 2)) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by FIB_NUM2: 5;

        hence thesis;

      end;

      ((( GenFib (a,b,( 0 + 2))) * ( GenFib (a,b, 0 ))) - (( GenFib (a,b,( 0 + 1))) |^ 2)) = ((( GenFib (a,b,2)) * a) - (( GenFib (a,b,1)) |^ 2)) by Th32

      .= (((a + b) * a) - (b |^ 2)) by A1, Th32

      .= (((a * a) + (b * a)) - (b * b)) by WSIERP_1: 1

      .= (((a + b) * (a + b)) - (b * ((2 * b) + a)))

      .= (1 * ((( GenFib (a,b,2)) |^ 2) - (b * ( GenFib (a,b,3))))) by A1, A2, WSIERP_1: 1

      .= ((( - 1) to_power 0 ) * ((( GenFib (a,b,2)) |^ 2) - (b * ( GenFib (a,b,3))))) by POWER: 24

      .= ((( - 1) to_power 0 ) * ((( GenFib (a,b,2)) |^ 2) - (( GenFib (a,b,1)) * ( GenFib (a,b,3))))) by Th32;

      then

       A12: P[ 0 ];

      for k be Nat holds P[k] from FIB_NUM:sch 1( A12, A3, A4);

      hence thesis;

    end;

    theorem :: FIB_NUM3:48

    for a,b,k,n be Element of NAT holds ( GenFib (( GenFib (a,b,k)),( GenFib (a,b,(k + 1))),n)) = ( GenFib (a,b,(n + k)))

    proof

      let a,b,k,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib (( GenFib (a,b,k)),( GenFib (a,b,(k + 1))),$1)) = ( GenFib (a,b,($1 + k)));

      

       A1: P[1] by Th32;

      

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

      proof

        let i be Nat;

        assume P[i] & P[(i + 1)];

        

        then ( GenFib (( GenFib (a,b,k)),( GenFib (a,b,(k + 1))),(i + 2))) = (( GenFib (a,b,(i + k))) + ( GenFib (a,b,((i + k) + 1)))) by Th34

        .= ( GenFib (a,b,((i + k) + 2))) by Th34

        .= ( GenFib (a,b,((i + 2) + k)));

        hence thesis;

      end;

      

       A3: P[ 0 ] by Th32;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:49

    

     Th49: for a,b,n be Element of NAT holds ( GenFib (a,b,(n + 1))) = ((a * ( Fib n)) + (b * ( Fib (n + 1))))

    proof

      let a,b,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib (a,b,($1 + 1))) = ((a * ( Fib $1)) + (b * ( Fib ($1 + 1))));

      

       A1: ( Fib 2) = ( Fib ( 0 + 2))

      .= ( 0 + 1) by FIB_NUM2: 24, PRE_FF: 1;

      ( GenFib (a,b,2)) = ( GenFib (a,b,( 0 + 2)))

      .= (( GenFib (a,b, 0 )) + ( GenFib (a,b,( 0 + 1)))) by Th34

      .= (a + ( GenFib (a,b,1))) by Th32

      .= (a + b) by Th32;

      then

       A2: P[1] by A1, PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume that

         A4: P[k] and

         A5: P[(k + 1)];

        ( GenFib (a,b,((k + 2) + 1))) = ( GenFib (a,b,((k + 1) + 2)))

        .= (((a * ( Fib k)) + (b * ( Fib (k + 1)))) + ( GenFib (a,b,((k + 1) + 1)))) by A4, Th34

        .= ((a * (( Fib k) + ( Fib (k + 1)))) + (b * (( Fib (k + 1)) + ( Fib ((k + 1) + 1))))) by A5

        .= ((a * ( Fib (k + 2))) + (b * (( Fib (k + 1)) + ( Fib ((k + 1) + 1))))) by FIB_NUM2: 24

        .= ((a * ( Fib (k + 2))) + (b * ( Fib ((k + 1) + 2)))) by FIB_NUM2: 24

        .= ((a * ( Fib (k + 2))) + (b * ( Fib ((k + 2) + 1))));

        hence thesis;

      end;

      

       A6: P[ 0 ] by Th32, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:50

    for b,n be Element of NAT holds ( GenFib ( 0 ,b,n)) = (b * ( Fib n))

    proof

      let b,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib ( 0 ,b,$1)) = (b * ( Fib $1));

      

       A1: P[1] by Th32, PRE_FF: 1;

      

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

      proof

        let k be Nat;

        assume that

         A3: P[k] and

         A4: P[(k + 1)];

        ( GenFib ( 0 ,b,(k + 2))) = ((b * ( Fib k)) + ( GenFib ( 0 ,b,(k + 1)))) by A3, Th34

        .= (b * (( Fib k) + ( Fib (k + 1)))) by A4

        .= (b * ( Fib (k + 2))) by FIB_NUM2: 24;

        hence thesis;

      end;

      

       A5: P[ 0 ] by Th32, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:51

    for a,n be Element of NAT holds ( GenFib (a, 0 ,(n + 1))) = (a * ( Fib n))

    proof

      let a,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib (a, 0 ,($1 + 1))) = (a * ( Fib $1));

      

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

      proof

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        ( GenFib (a, 0 ,((k + 2) + 1))) = ( GenFib (a, 0 ,((k + 1) + 2)))

        .= ((a * ( Fib k)) + ( GenFib (a, 0 ,((k + 1) + 1)))) by A2, Th34

        .= (a * (( Fib k) + ( Fib (k + 1)))) by A3

        .= (a * ( Fib (k + 2))) by FIB_NUM2: 24;

        hence thesis;

      end;

      ( GenFib (a, 0 ,2)) = ( GenFib (a, 0 ,( 0 + 2)))

      .= (( GenFib (a, 0 , 0 )) + ( GenFib (a, 0 ,( 0 + 1)))) by Th34

      .= (a + ( GenFib (a, 0 ,1))) by Th32

      .= (a + 0 ) by Th32;

      then

       A4: P[1] by PRE_FF: 1;

      

       A5: P[ 0 ] by Th32, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:52

    for a,b,c,d,n be Element of NAT holds (( GenFib (a,b,n)) + ( GenFib (c,d,n))) = ( GenFib ((a + c),(b + d),n))

    proof

      let a,b,c,d,n be Element of NAT ;

      defpred P[ Nat] means (( GenFib (a,b,$1)) + ( GenFib (c,d,$1))) = ( GenFib ((a + c),(b + d),$1));

      

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

      proof

        let k be Nat;

        assume that

         A2: P[k] and

         A3: P[(k + 1)];

        (( GenFib (a,b,(k + 2))) + ( GenFib (c,d,(k + 2)))) = ((( GenFib (a,b,k)) + ( GenFib (a,b,(k + 1)))) + ( GenFib (c,d,(k + 2)))) by Th34

        .= ((( GenFib (a,b,k)) + ( GenFib (a,b,(k + 1)))) + (( GenFib (c,d,k)) + ( GenFib (c,d,(k + 1))))) by Th34

        .= (( GenFib ((a + c),(b + d),k)) + (( GenFib (a,b,(k + 1))) + ( GenFib (c,d,(k + 1))))) by A2

        .= ( GenFib ((a + c),(b + d),(k + 2))) by A3, Th34;

        hence thesis;

      end;

      (( GenFib (a,b,1)) + ( GenFib (c,d,1))) = (b + ( GenFib (c,d,1))) by Th32

      .= (b + d) by Th32

      .= ( GenFib ((a + c),(b + d),1)) by Th32;

      then

       A4: P[1];

      (( GenFib (a,b, 0 )) + ( GenFib (c,d, 0 ))) = (a + ( GenFib (c,d, 0 ))) by Th32

      .= (a + c) by Th32

      .= ( GenFib ((a + c),(b + d), 0 )) by Th32;

      then

       A5: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:53

    for a,b,k,n be Element of NAT holds ( GenFib ((k * a),(k * b),n)) = (k * ( GenFib (a,b,n)))

    proof

      let a,b,k,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib ((k * a),(k * b),$1)) = (k * ( GenFib (a,b,$1)));

      

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

      proof

        let i be Nat;

        assume that

         A2: P[i] and

         A3: P[(i + 1)];

        ( GenFib ((k * a),(k * b),(i + 2))) = ((k * ( GenFib (a,b,i))) + ( GenFib ((k * a),(k * b),(i + 1)))) by A2, Th34

        .= (k * (( GenFib (a,b,i)) + ( GenFib (a,b,(i + 1))))) by A3

        .= (k * ( GenFib (a,b,(i + 2)))) by Th34;

        hence thesis;

      end;

      ( GenFib ((k * a),(k * b),1)) = (k * b) by Th32

      .= (k * ( GenFib (a,b,1))) by Th32;

      then

       A4: P[1];

      ( GenFib ((k * a),(k * b), 0 )) = (k * a) by Th32

      .= (k * ( GenFib (a,b, 0 ))) by Th32;

      then

       A5: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:54

    for a,b,n be Element of NAT holds ( GenFib (a,b,n)) = (((((a * ( - tau_bar )) + b) * ( tau to_power n)) + (((a * tau ) - b) * ( tau_bar to_power n))) / ( sqrt 5))

    proof

      let a,b,n be Element of NAT ;

      defpred P[ Nat] means ( GenFib (a,b,$1)) = (((((a * ( - tau_bar )) + b) * ( tau to_power $1)) + (((a * tau ) - b) * ( tau_bar to_power $1))) / ( sqrt 5));

      (((((a * ( - tau_bar )) + b) * ( tau to_power 1)) + (((a * tau ) - b) * ( tau_bar to_power 1))) / ( sqrt 5)) = (((((a * ( - tau_bar )) + b) * tau ) + (((a * tau ) - b) * ( tau_bar to_power 1))) / ( sqrt 5)) by POWER: 25

      .= (((((a * ( - tau_bar )) + b) * tau ) + (((a * tau ) - b) * tau_bar )) / ( sqrt 5)) by POWER: 25

      .= ((b * ( tau - tau_bar )) / ( sqrt 5))

      .= b by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1: 89

      .= ( GenFib (a,b,1)) by Th32;

      then

       A1: P[1];

      

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

      proof

        let k be Nat;

        set c = ( tau to_power k);

        set d = ( tau_bar to_power k);

        

         A3: ( tau to_power (k + 1)) = (( tau to_power k) * ( tau to_power 1)) by POWER: 27

        .= (c * tau ) by POWER: 25;

        set g = ((((a * ( - tau_bar )) + b) * c) + (((a * tau ) - b) * d));

        

         A4: ( tau_bar to_power (k + 1)) = (( tau_bar to_power k) * ( tau_bar to_power 1)) by FIB_NUM2: 5

        .= (d * tau_bar ) by POWER: 25;

        (( sqrt 5) * ( sqrt 5)) = 5 by Th2;

        

        then

         A5: (1 + tau ) = (((1 + ( sqrt 5)) * (1 + ( sqrt 5))) / (2 * 2)) by FIB_NUM:def 1

        .= ( tau * tau ) by FIB_NUM:def 1

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

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

        .= ( tau to_power (1 + 1)) by POWER: 27;

        

         A6: (1 + tau_bar ) = ((((1 - ( sqrt 5)) - ( sqrt 5)) + 5) / 4) by FIB_NUM:def 2

        .= ((((1 - (1 * ( sqrt 5))) - (( sqrt 5) * 1)) + (( sqrt 5) * ( sqrt 5))) / 4) by Th2

        .= ( tau_bar * tau_bar ) by FIB_NUM:def 2

        .= (( tau_bar to_power 1) * tau_bar ) by POWER: 25

        .= (( tau_bar to_power 1) * ( tau_bar to_power 1)) by POWER: 25

        .= ( tau_bar to_power (1 + 1)) by FIB_NUM2: 5

        .= ( tau_bar to_power 2);

        set h = (((((a * ( - tau_bar )) + b) * c) * tau ) + ((((a * tau ) - b) * d) * tau_bar ));

        

         A7: ( tau to_power (k + 2)) = (c * ( tau to_power 2)) & ( tau_bar to_power (k + 2)) = (d * ( tau_bar to_power 2)) by FIB_NUM2: 5;

        assume P[k] & P[(k + 1)];

        

        then ( GenFib (a,b,(k + 2))) = ((g / ( sqrt 5)) + (h / ( sqrt 5))) by A3, A4, Th34

        .= ((g + h) / ( sqrt 5)) by XCMPLX_1: 62

        .= (((((a * ( - tau_bar )) + b) * ( tau to_power (k + 2))) + (((a * tau ) - b) * ( tau_bar to_power (k + 2)))) / ( sqrt 5)) by A7, A5, A6;

        hence thesis;

      end;

      (((((a * ( - tau_bar )) + b) * ( tau to_power 0 )) + (((a * tau ) - b) * ( tau_bar to_power 0 ))) / ( sqrt 5)) = (((((a * ( - tau_bar )) + b) * 1) + (((a * tau ) - b) * ( tau_bar to_power 0 ))) / ( sqrt 5)) by POWER: 24

      .= ((((a * ( - tau_bar )) + b) + (((a * tau ) - b) * 1)) / ( sqrt 5)) by POWER: 24

      .= ((a * ( tau - tau_bar )) / ( sqrt 5))

      .= a by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1: 89

      .= ( GenFib (a,b, 0 )) by Th32;

      then

       A8: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FIB_NUM3:55

    for a,n be Element of NAT holds ( GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1))) = (((2 * a) + 1) * ( Fib (n + 2)))

    proof

      let a,n be Element of NAT ;

      ( GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1))) = ((((2 * a) + 1) * ( Fib n)) + (((2 * a) + 1) * ( Fib (n + 1)))) by Th49

      .= (((2 * a) + 1) * (( Fib n) + ( Fib (n + 1))))

      .= (((2 * a) + 1) * ( Fib (n + 2))) by FIB_NUM2: 24;

      hence thesis;

    end;