fib_num2.miz

    begin

    reserve n,k,r,m,i,j for Nat;

    theorem :: FIB_NUM2:1

    for n be non zero Element of NAT holds ((n -' 1) + 2) = (n + 1)

    proof

      let n be non zero Element of NAT ;

      n >= 1 by NAT_2: 19;



      then ((n -' 1) + 2) = ((n + 2) -' 1) by NAT_D: 38

      .= ((n + 2) - 1) by NAT_D: 37;

      hence thesis;

    end;

    theorem :: FIB_NUM2:2



     Th2: for n be odd Integer holds (( - 1) to_power n) = ( - 1)

    proof

      let n be odd Integer;

      (( - 1) to_power n) = ( - (1 to_power n)) by POWER: 48

      .= ( - 1) by POWER: 26;

      hence thesis;

    end;

    theorem :: FIB_NUM2:3



     Th3: for n be even Integer holds (( - 1) to_power n) = 1

    proof

      let n be even Integer;

      (( - 1) to_power n) = (1 to_power n) by POWER: 47;

      hence thesis by POWER: 26;

    end;

    theorem :: FIB_NUM2:4



     Th4: for m be non zero Real, n be Integer holds ((( - 1) * m) to_power n) = ((( - 1) to_power n) * (m to_power n))

    proof

      let m be non zero Real, n be Integer;

      per cases ;

        suppose

         A1: n is odd;



        then (( - m) to_power n) = ( - (m to_power n)) by POWER: 48

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

        .= ((( - 1) to_power n) * (m to_power n)) by A1, Th2;

        hence thesis;

      end;

        suppose

         A2: n is even;



        then (( - m) to_power n) = (1 * (m to_power n)) by POWER: 47

        .= ((( - 1) to_power n) * (m to_power n)) by A2, Th3;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM2:5



     Th5: for a be Real holds (a to_power (k + m)) = ((a to_power k) * (a to_power m))

    proof

      let a be Real;



      thus (a to_power (k + m)) = (a |^ (k + m)) by POWER: 41

      .= ((a |^ k) * (a |^ m)) by NEWTON: 8

      .= ((a to_power k) * (a |^ m)) by POWER: 41

      .= ((a to_power k) * (a to_power m)) by POWER: 41;

    end;

    theorem :: FIB_NUM2:6



     Th6: for k be non zero Real, m be odd Integer holds ((k to_power m) to_power n) = (k to_power (m * n))

    proof

      let k be non zero Real, m be odd Integer;

      (k to_power (m * n)) = (k #Z (m * n)) by POWER:def 2

      .= ((k #Z m) #Z n) by PREPOWER: 45

      .= ((k to_power m) #Z n) by POWER:def 2

      .= ((k to_power m) to_power n) by POWER:def 2;

      hence thesis;

    end;

    theorem :: FIB_NUM2:7



     Th7: ((( - 1) to_power ( - n)) ^2 ) = 1

    proof

      ((( - 1) to_power ( - n)) ^2 ) = ((( - 1) #Z ( - n)) ^2 ) by POWER:def 2

      .= ((1 / (( - 1) #Z n)) ^2 ) by PREPOWER: 41

      .= ((1 / (( - 1) #Z n)) to_power 2) by POWER: 46

      .= ((1 / (( - 1) #Z n)) |^ 2) by POWER: 41

      .= (1 / ((( - 1) #Z n) |^ 2)) by PREPOWER: 7

      .= (1 / ((( - 1) #Z n) #Z 2)) by PREPOWER: 36

      .= (1 / (( - 1) #Z (n * 2))) by PREPOWER: 45

      .= (1 / (( - 1) |^ (2 * n))) by PREPOWER: 36

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

      .= (1 / ((1 |^ 2) |^ n))

      .= (1 / (1 |^ n))

      .= (1 / 1);

      hence thesis;

    end;

    theorem :: FIB_NUM2:8



     Th8: for a be non zero Real holds ((a to_power ( - k)) * (a to_power ( - m))) = (a to_power (( - k) - m))

    proof

      set K = ( - k);

      set M = ( - m);

      let a be non zero Real;

      ((a to_power ( - k)) * (a to_power ( - m))) = ((a #Z ( - k)) * (a to_power ( - m))) by POWER:def 2

      .= ((a #Z K) * (a #Z M)) by POWER:def 2

      .= (a #Z (K + M)) by PREPOWER: 44

      .= (a to_power (( - k) - m)) by POWER:def 2;

      hence thesis;

    end;

    theorem :: FIB_NUM2:9



     Th9: (( - 1) to_power ( - (2 * n))) = 1

    proof

      (( - 1) to_power ( - (2 * n))) = (( - 1) #Z (( - 1) * (2 * n))) by POWER:def 2

      .= ((( - 1) #Z ( - 1)) #Z (2 * n)) by PREPOWER: 45

      .= ((1 / (( - 1) #Z 1)) #Z (2 * n)) by PREPOWER: 41

      .= ((1 / ( - 1)) #Z (2 * n)) by PREPOWER: 35

      .= (( - 1) |^ (2 * n)) by PREPOWER: 36

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

      .= ((1 |^ 2) |^ n)

      .= (1 |^ n)

      .= 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:10



     Th10: for a be non zero Real holds ((a to_power k) * (a to_power ( - k))) = 1

    proof

      let a be non zero Real;

      ((a to_power k) * (a to_power ( - k))) = ((a #Z k) * (a to_power ( - k))) by POWER:def 2

      .= ((a #Z k) * (a #Z ( - k))) by POWER:def 2

      .= (a #Z (k + ( - k))) by PREPOWER: 44

      .= 1 by PREPOWER: 34;

      hence thesis;

    end;

    registration

      let n be odd Integer;

      cluster ( - n) -> odd;

      coherence

      proof

        ( - 1) = ((2 * ( - 1)) + 1);

        then

        reconsider e = ( - 1) as odd Integer;

        (e * n) is odd;

        hence thesis;

      end;

    end

    registration

      let n be even Integer;

      cluster ( - n) -> even;

      coherence

      proof

        reconsider e = ( - 1) as Integer;

        (e * n) is even;

        hence thesis;

      end;

    end

    theorem :: FIB_NUM2:11



     Th11: (( - 1) to_power ( - n)) = (( - 1) to_power n)

    proof

      per cases ;

        suppose n is odd;

        then

        reconsider n as odd Integer;

        (( - 1) to_power ( - n)) = ( - 1) by Th2

        .= (( - 1) to_power n) by Th2;

        hence thesis;

      end;

        suppose n is even;

        then

        reconsider n as even Integer;

        (( - 1) to_power ( - n)) = 1 by Th3

        .= (( - 1) to_power n) by Th3;

        hence thesis;

      end;

    end;

    theorem :: FIB_NUM2:12



     Th12: for k,m,m1,n1 be Element of NAT st k divides m & k divides n holds k divides ((m * m1) + (n * n1))

    proof

      let k,m,m1,n1 be Element of NAT ;

      assume k divides m & k divides n;

      then k divides (m * m1) & k divides (n * n1) by NAT_D: 9;

      hence thesis by NAT_D: 8;

    end;

    registration

      cluster finite non empty natural-membered with_non-empty_elements for set;

      existence

      proof

        take X = {1};

        thus X is finite non empty;

        thus X is natural-membered;

        thus thesis;

      end;

    end

    registration

      let f be sequence of NAT ;

      let A be finite natural-membered with_non-empty_elements set;

      cluster (f | A) -> FinSubsequence-like;

      coherence

      proof

        per cases ;

          suppose A is non empty;

          then

          reconsider A9 = A as non empty finite natural-membered with_non-empty_elements set;

          reconsider k = ( max A9) as Element of NAT by ORDINAL1:def 12;



           A1: ( dom (f | A)) c= A by RELAT_1: 58;

          ( dom (f | A)) c= ( Seg k)

          proof

            let x be object;

            assume

             A2: x in ( dom (f | A));

            then

            reconsider x9 = x as Nat by A1;

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

            1 <= x9 & x9 <= k by A1, A2, NAT_1: 14, XXREAL_2:def 8;

            hence thesis;

          end;

          hence thesis;

        end;

          suppose A is empty;

          hence thesis;

        end;

      end;

    end

    theorem :: FIB_NUM2:13

    for p be FinSubsequence holds ( rng ( Seq p)) c= ( rng p) by RELAT_1: 26;

    definition

      let f be sequence of NAT ;

      let A be finite with_non-empty_elements natural-membered set;

      :: FIB_NUM2:def1

      func Prefix (f,A) -> FinSequence of NAT equals ( Seq (f | A));

      coherence

      proof

        ( rng ( Seq (f | A))) c= NAT by RELAT_1:def 19;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: FIB_NUM2:14



     Th14: for k be Element of NAT st k <> 0 holds (k + m) <= n implies m < n

    proof

      let k be Element of NAT ;

      assume

       A1: k <> 0 ;

      assume

       A2: (k + m) <= n;

      per cases by A2, XXREAL_0: 1;

        suppose (k + m) < n;

        hence thesis by NAT_1: 12;

      end;

        suppose

         A3: (k + m) = n;

        assume not m < n;

        then (m + k) >= (n + k) by XREAL_1: 7;

        then (n - n) >= ((n + k) - n) by A3, XREAL_1: 9;

        hence contradiction by A1;

      end;

    end;

    registration

      cluster NAT -> bounded_below;

      coherence ;

    end

    theorem :: FIB_NUM2:15



     Th15: for x,y be set st 0 < i & i < j holds { [i, x], [j, y]} is FinSubsequence

    proof

      let x,y be set;

      assume that

       A1: 0 < i and

       A2: i < j;

      reconsider X = { [i, x], [j, y]} as Function by A2, GRFUNC_1: 8;



       A3: ( 0 + 1) <= i by A1, NAT_1: 13;

      now

        let x be object;

        assume x in {i, j};

        then

         A4: x = i or x = j by TARSKI:def 2;

        thus x in ( Seg j) by A2, A3, A4, FINSEQ_1: 3;

      end;

      then ( dom X) = {i, j} & {i, j} c= ( Seg j) by RELAT_1: 10;

      hence thesis by FINSEQ_1:def 12;

    end;

    theorem :: FIB_NUM2:16



     Th16: for x,y be set, q be FinSubsequence st i < j & q = { [i, x], [j, y]} holds ( Seq q) = <*x, y*>

    proof

      let x,y be set, q be FinSubsequence;

      assume that

       A1: i < j and

       A2: q = { [i, x], [j, y]};



       A3: q = ((i,j) --> (x,y)) by A1, A2, FUNCT_4: 67;

       [i, x] in q by A2, TARSKI:def 2;

      then

       A4: i in ( dom q) by XTUPLE_0:def 12;

       [j, y] in q by A2, TARSKI:def 2;

      then

       A5: j in ( dom q) by XTUPLE_0:def 12;



       A6: ( dom q) = {i, j} by A2, RELAT_1: 10;

      ex k be Nat st ( dom q) c= ( Seg k) by FINSEQ_1:def 12;

      then i >= ( 0 + 1) by A4, FINSEQ_1: 1;



      then ( Seq q) = (q * <*i, j*>) by A1, A6, FINSEQ_3: 45

      .= <*(q . i), (q . j)*> by A4, A5, FINSEQ_2: 125

      .= <*x, (q . j)*> by A1, A3, FUNCT_4: 63

      .= <*x, y*> by A3, FUNCT_4: 63;

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster ( Seg n) -> with_non-empty_elements;

      coherence

      proof

         not 0 in ( Seg n) by FINSEQ_1: 1;

        hence thesis by SETFAM_1:def 8;

      end;

    end

    registration

      let A be with_non-empty_elements set;

      cluster -> with_non-empty_elements for Subset of A;

      coherence

      proof

        let L be Subset of A;

         not 0 in L;

        hence thesis by SETFAM_1:def 8;

      end;

    end

    registration

      let A be with_non-empty_elements set;

      let B be set;

      cluster (A /\ B) -> with_non-empty_elements;

      coherence

      proof

        reconsider AB = (A /\ B) as Subset of A by XBOOLE_1: 17;

        AB is with_non-empty_elements;

        hence thesis;

      end;

      cluster (B /\ A) -> with_non-empty_elements;

      coherence ;

    end

    theorem :: FIB_NUM2:17



     Th17: for k be Element of NAT , a be set st k >= 1 holds { [k, a]} is FinSubsequence

    proof

      let k be Element of NAT , a be set;

      reconsider H = { [k, a]} as Function;



       A1: ( dom H) = {k} by RELAT_1: 9;

      assume

       A2: k >= 1;

      ( dom H) c= ( Seg k)

      proof

        let x be object;

        assume x in ( dom H);

        then x = k by A1, TARSKI:def 1;

        hence thesis by A2;

      end;

      hence thesis by FINSEQ_1:def 12;

    end;

    theorem :: FIB_NUM2:18



     Th18: for i be Element of NAT , y be set, f be FinSubsequence st f = { [1, y]} holds ( Shift (f,i)) = { [(1 + i), y]}

    proof

      let i be Element of NAT , y be set, f be FinSubsequence;

      set g = ( Shift (f,i));

      assume

       A1: f = { [1, y]};

      then ( card f) = 1 by CARD_2: 42;

      then ( card ( Shift (f,i))) = 1 by VALUED_1: 42;

      then

       A2: ex x be object st ( Shift (f,i)) = {x} by CARD_2: 42;



       A3: ( dom f) = {1} by A1, RELAT_1: 9;

      ( dom g) = {(1 + i)}

      proof

        hereby

          let x be object;

          assume x in ( dom g);

          then x in { (o + i) where o be Nat : o in ( dom f) } by VALUED_1:def 12;

          then

          consider w be Nat such that

           A4: (w + i) = x and

           A5: w in ( dom f);

          w = 1 by A3, A5, TARSKI:def 1;

          hence x in {(1 + i)} by A4, TARSKI:def 1;

        end;

        let x be object;

        assume x in {(1 + i)};

        then

         A6: x = (1 + i) by TARSKI:def 1;

        1 in ( dom f) by A3, TARSKI:def 1;

        then x in { (o + i) where o be Nat : o in ( dom f) } by A6;

        hence thesis by VALUED_1:def 12;

      end;

      then

       A7: (1 + i) in ( dom g) by TARSKI:def 1;

      1 in ( dom f) by A3, TARSKI:def 1;



      then (g . (1 + i)) = (f . 1) by VALUED_1:def 12

      .= y by A1, GRFUNC_1: 6;

      then [(1 + i), y] in g by A7, FUNCT_1:def 2;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: FIB_NUM2:19



     Th19: for q be FinSubsequence, k,n be Element of NAT st ( dom q) c= ( Seg k) & n > k holds ex p be FinSequence st q c= p & ( dom p) = ( Seg n)

    proof

      let q be FinSubsequence, k,n be Element of NAT ;

      assume that

       A1: ( dom q) c= ( Seg k) and

       A2: n > k;

      reconsider IK = ( id ( Seg n)) as Function;

      set IS = (IK +* q);



       A3: ( Seg k) c= ( Seg n) by A2, FINSEQ_1: 5;



       A4: ( dom IS) = (( dom IK) \/ ( dom q)) by FUNCT_4:def 1

      .= (( Seg n) \/ ( dom q))

      .= ( Seg n) by A1, A3, XBOOLE_1: 1, XBOOLE_1: 12;

      then

      reconsider IS as FinSequence by FINSEQ_1:def 2;

      q c= IS by FUNCT_4: 25;

      hence thesis by A4;

    end;

    theorem :: FIB_NUM2:20



     Th20: for q be FinSubsequence holds ex p be FinSequence st q c= p

    proof

      let q be FinSubsequence;

      consider k be Nat such that

       A1: ( dom q) c= ( Seg k) by FINSEQ_1:def 12;

      reconsider IK = ( id ( Seg k)) as Function;

      set IS = (IK +* q);

      ( dom IS) = (( dom IK) \/ ( dom q)) by FUNCT_4:def 1

      .= (( Seg k) \/ ( dom q))

      .= ( Seg k) by A1, XBOOLE_1: 12;

      then

      reconsider IS as FinSequence by FINSEQ_1:def 2;

      q c= IS by FUNCT_4: 25;

      hence thesis;

    end;

    begin

    scheme :: FIB_NUM2:sch1

    FibInd1 { P[ set] } :

for k be non zero Nat holds P[k]

      provided

       A1: P[1]

       and

       A2: P[2]

       and

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

      let k be non zero Nat;

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



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

      proof

        let k be non zero Nat;



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

        assume Q[k];

        hence thesis by A3, A5;

      end;



       A6: Q[1] by A1, A2;

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

      hence thesis;

    end;

    scheme :: FIB_NUM2:sch2

    FibInd2 { P[ set] } :

for k be non trivial Nat holds P[k]

      provided

       A1: P[2]

       and

       A2: P[3]

       and

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

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



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

      proof

        let k be non zero Nat;

        (k + 1) <> ( 0 + 1);

        then

         A5: (k + 1) is non trivial Nat by NAT_2:def 1;

        assume

         A6: Q[k];

        then P[((k + 1) + 1)];

        hence thesis by A3, A5, A6;

      end;

      let k be non trivial Nat;

      k <> 1 by NAT_2:def 1;

      then

       A7: k > 1 by NAT_2: 19;

      then (k - 1) > (1 - 1) by XREAL_1: 9;

      then

       A8: (k - 1) > 0 ;



       A9: Q[1] by A1, A2;



       A10: for k be non zero Nat holds Q[k] from NAT_1:sch 10( A9, A4);

      ((k -' 1) + 1) = k by A7, XREAL_1: 235;

      hence thesis by A10, A8;

    end;

    theorem :: FIB_NUM2:21



     Th21: ( Fib 2) = 1

    proof

      ( Fib 2) = ( Fib (( 0 + 1) + 1))

      .= 1 by PRE_FF: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:22



     Th22: ( Fib 3) = 2

    proof

      ( Fib 3) = ( Fib ((1 + 1) + 1))

      .= 2 by Th21, PRE_FF: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:23



     Th23: ( Fib 4) = 3

    proof

      ( Fib 4) = ( Fib ((2 + 1) + 1))

      .= 3 by Th21, Th22, PRE_FF: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:24



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

    proof

      defpred P[ Nat] means ( Fib ($1 + 2)) = (( Fib $1) + ( 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 P[k];

        assume P[(k + 1)];

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

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

        hence thesis;

      end;

      ( Fib ( 0 + 2)) = ( Fib (( 0 + 1) + 1))

      .= (( Fib 0 ) + ( Fib 1)) by PRE_FF: 1;

      then

       A2: P[ 0 ];



       A3: P[1] by PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:25



     Th25: for n be Nat holds ( Fib (n + 3)) = (( Fib (n + 2)) + ( Fib (n + 1)))

    proof

      let n be Nat;

      ( Fib (n + 3)) = ( Fib ((n + 1) + 2))

      .= (( Fib ((n + 1) + 1)) + ( Fib (n + 1))) by Th24

      .= (( Fib (n + 2)) + ( Fib (n + 1)));

      hence thesis;

    end;

    theorem :: FIB_NUM2:26



     Th26: ( Fib (n + 4)) = (( Fib (n + 2)) + ( Fib (n + 3)))

    proof

      ( Fib (n + 4)) = ( Fib (((n + 2) + 1) + 1))

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:27



     Th27: ( Fib (n + 5)) = (( Fib (n + 3)) + ( Fib (n + 4)))

    proof

      ( Fib (n + 5)) = ( Fib (((n + 3) + 1) + 1))

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

      hence thesis;

    end;



     Lm1: for k be Nat holds ( Fib ((2 * (k + 2)) + 1)) = (( Fib ((2 * k) + 3)) + ( Fib ((2 * k) + 4)))

    proof

      let k be Nat;

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

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:28



     Th28: ( Fib (n + 2)) = (( Fib (n + 3)) - ( Fib (n + 1)))

    proof

      ( Fib (n + 3)) = ( Fib (((n + 1) + 1) + 1))

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:29



     Th29: for n be Nat holds ( Fib (n + 1)) = (( Fib (n + 2)) - ( Fib n))

    proof

      let n be Nat;

      (( Fib (n + 2)) - ( Fib n)) = (( Fib ((n + 1) + 1)) - ( Fib n))

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

      .= ( Fib (n + 1));

      hence thesis;

    end;

    theorem :: FIB_NUM2:30



     Th30: ( Fib n) = (( Fib (n + 2)) - ( Fib (n + 1)))

    proof

      (( Fib (n + 2)) - ( Fib (n + 1))) = ((( Fib n) + ( Fib (n + 1))) - ( Fib (n + 1))) by Th24

      .= ( Fib n);

      hence thesis;

    end;

    begin

    theorem :: FIB_NUM2:31



     Th31: ((( Fib n) * ( Fib (n + 2))) - (( Fib (n + 1)) ^2 )) = (( - 1) |^ (n + 1))

    proof

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



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

      proof

        let k be Nat;



         A2: (( Fib (k + 2)) - ( Fib (k + 1))) = ((( Fib (k + 1)) + ( Fib k)) - ( Fib (k + 1))) by Th24

        .= ( Fib k);



         A3: (( Fib (k + 3)) - ( Fib (k + 1))) = ((( Fib (k + 2)) + ( Fib (k + 1))) - ( Fib (k + 1))) by Th25

        .= ( Fib (k + 2));

        assume P[k];



        then (( - 1) |^ ((k + 1) + 1)) = (( - 1) * ((( Fib k) * ( Fib (k + 2))) - (( Fib (k + 1)) ^2 ))) by NEWTON: 6

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

        hence thesis;

      end;



       A4: P[ 0 ] by PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:32

    for n be non zero Element of NAT holds ((( Fib (n -' 1)) * ( Fib (n + 1))) - (( Fib n) ^2 )) = (( - 1) |^ n)

    proof

      let n be non zero Element of NAT ;

      set a = (n -' 1);



       A1: n >= 1 by NAT_2: 19;

      then n = (a + 1) by XREAL_1: 235;



      then ((( Fib (n -' 1)) * ( Fib (n + 1))) - (( Fib n) ^2 )) = ((( Fib a) * ( Fib (a + 2))) - (( Fib (a + 1)) ^2 ))

      .= (( - 1) |^ ((n -' 1) + 1)) by Th31

      .= (( - 1) |^ n) by A1, XREAL_1: 235;

      hence thesis;

    end;

    theorem :: FIB_NUM2:33



     Th33: tau > 0

    proof

      ( sqrt 5) > 0 by SQUARE_1: 25;

      hence thesis by FIB_NUM:def 1;

    end;

    theorem :: FIB_NUM2:34



     Th34: tau_bar = (( - tau ) to_power ( - 1))

    proof



       A1: (1 - ( sqrt 5)) <> 0 by SQUARE_1: 20, SQUARE_1: 27;

      (( - tau ) to_power ( - 1)) = (((( - 1) - ( sqrt 5)) / 2) #Z ( - 1)) by FIB_NUM:def 1, POWER:def 2

      .= (1 / (((( - 1) - ( sqrt 5)) / 2) #Z 1)) by PREPOWER: 41

      .= (1 / ((( - 1) - ( sqrt 5)) / 2)) by PREPOWER: 35

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

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

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

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

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

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

      .= tau_bar by FIB_NUM:def 2;

      hence thesis;

    end;

    theorem :: FIB_NUM2:35



     Th35: (( - tau ) to_power (( - 1) * n)) = ((( - tau ) to_power ( - 1)) to_power n)

    proof

      (( - tau ) to_power (( - 1) * n)) = (( - tau ) #Z (( - 1) * n)) by POWER:def 2

      .= ((( - tau ) #Z ( - 1)) #Z n) by PREPOWER: 45

      .= ((1 / (( - tau ) #Z 1)) #Z n) by PREPOWER: 41

      .= ((1 / ( - tau )) #Z n) by PREPOWER: 35

      .= ((1 / ( - tau )) to_power n) by POWER:def 2

      .= (((1 / ( - tau )) to_power 1) to_power n) by POWER: 25

      .= (((1 / ( - tau )) #Z 1) to_power n) by POWER:def 2

      .= ((1 / (( - tau ) #Z 1)) to_power n) by PREPOWER: 42

      .= ((( - tau ) #Z ( - 1)) to_power n) by PREPOWER: 41;

      hence thesis by POWER:def 2;

    end;

    theorem :: FIB_NUM2:36



     Th36: ( - (1 / tau )) = tau_bar

    proof



       A1: (1 - ( sqrt 5)) <> 0 by SQUARE_1: 20, SQUARE_1: 27;

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

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

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

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

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

      hence thesis by FIB_NUM:def 2;

    end;

    theorem :: FIB_NUM2:37



     Th37: (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + (( tau to_power ( - r)) ^2 )) = ((( tau to_power r) - ( tau_bar to_power r)) ^2 )

    proof

      (( - 1) / tau ) < 0 by Th33;

      then ( - (1 / tau )) < 0 by XCMPLX_1: 187;

      then

       A1: (1 / tau ) > ( - 0 qua Nat);

      ((( tau to_power r) - ( tau_bar to_power r)) ^2 ) = (((( tau to_power r) ^2 ) - ((2 * ( tau to_power r)) * (( - (1 / tau )) to_power r))) + ((( - (1 / tau )) to_power r) ^2 )) by Th36

      .= (((( tau to_power r) ^2 ) - ((2 * ( tau to_power r)) * ((( - 1) * (1 / tau )) #Z r))) + ((( - (1 / tau )) to_power r) ^2 )) by POWER:def 2

      .= (((( tau to_power r) ^2 ) - ((2 * ( tau to_power r)) * ((( - 1) #Z r) * ((1 / tau ) #Z r)))) + ((( - (1 / tau )) to_power r) ^2 )) by PREPOWER: 40

      .= (((( tau to_power r) ^2 ) - ((2 * ( tau to_power r)) * (((1 / tau ) |^ r) * (( - 1) #Z r)))) + ((( - (1 / tau )) to_power r) ^2 )) by PREPOWER: 36

      .= (((( tau to_power r) ^2 ) - ((2 * ( tau |^ r)) * (((1 / tau ) |^ r) * (( - 1) #Z r)))) + ((( - (1 / tau )) to_power r) ^2 )) by POWER: 41

      .= (((( tau to_power r) ^2 ) - ((2 * (( tau |^ r) * ((1 / tau ) |^ r))) * (( - 1) #Z r))) + ((( - (1 / tau )) to_power r) ^2 ))

      .= (((( tau to_power r) ^2 ) - ((2 * (( tau * (1 / tau )) |^ r)) * (( - 1) #Z r))) + ((( - (1 / tau )) to_power r) ^2 )) by NEWTON: 7

      .= (((( tau to_power r) ^2 ) - ((2 * (1 |^ r)) * (( - 1) #Z r))) + ((( - (1 / tau )) to_power r) ^2 )) by Th33, XCMPLX_1: 106

      .= (((( tau to_power r) ^2 ) - ((2 * 1) * (( - 1) #Z r))) + ((( - (1 / tau )) to_power r) ^2 ))

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((( - (1 / tau )) to_power r) ^2 )) by POWER:def 2

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((( - (1 / tau )) #Z r) ^2 )) by POWER:def 2

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((( - (1 / tau )) * ( - (1 / tau ))) #Z r)) by PREPOWER: 40

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((( - (1 / tau )) ^2 ) |^ r)) by PREPOWER: 36

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + (((1 / tau ) ^2 ) to_power r)) by POWER: 41

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + (((1 / tau ) to_power r) ^2 )) by A1, POWER: 30

      .= (((( tau to_power r) ^2 ) - (2 * (( - 1) to_power r))) + (( tau to_power ( - r)) ^2 )) by Th33, POWER: 32;

      hence thesis;

    end;

    theorem :: FIB_NUM2:38

    for n,r be non zero Element of NAT st r <= n holds ((( Fib n) ^2 ) - (( Fib (n + r)) * ( Fib (n -' r)))) = ((( - 1) |^ (n -' r)) * (( Fib r) ^2 ))

    proof

      set T = tau ;

      set S = (1 / ( sqrt 5));

      reconsider T as non zero Real by Th33;

      let n,r be non zero Element of NAT such that

       A1: r <= n;

      set Y = (n -' r);

      set X = (n + r);



       A2: (X + Y) = ((r + n) + (n - r)) by A1, XREAL_1: 233

      .= (((r + n) + n) - r)

      .= ((r + (2 * n)) -' r) by NAT_1: 12, XREAL_1: 233

      .= ((r -' r) + (2 * n)) by NAT_D: 38

      .= ( 0 + (2 * n)) by XREAL_1: 232

      .= (2 * n);



       A3: (X - Y) = ((n + r) - (n - r)) by A1, XREAL_1: 233

      .= (2 * r);

      set tyu = (T to_power ( - Y));

      set txu = (T to_power ( - X));

      set tnu = (T to_power ( - n));

      set ty = (T to_power Y);

      set tx = (T to_power X);

      set tn = (T to_power n);



       A4: ( - T) <> 0 & ( - 1) = ((2 * ( - 1)) + 1);

      ((( Fib n) ^2 ) - (( Fib X) * ( Fib Y))) = ((((tn - ( tau_bar to_power n)) / ( sqrt 5)) ^2 ) - (( Fib X) * ( Fib Y))) by FIB_NUM: 7

      .= ((((tn - ( tau_bar to_power n)) / ( sqrt 5)) ^2 ) - (((tx - ( tau_bar to_power X)) / ( sqrt 5)) * ( Fib Y))) by FIB_NUM: 7

      .= ((((tn - ( tau_bar to_power n)) / ( sqrt 5)) ^2 ) - (((tx - ( tau_bar to_power X)) / ( sqrt 5)) * ((ty - ( tau_bar to_power Y)) / ( sqrt 5)))) by FIB_NUM: 7

      .= ((((tn - ( tau_bar to_power n)) * S) ^2 ) - (((tx - ( tau_bar to_power X)) / ( sqrt 5)) * ((ty - ( tau_bar to_power Y)) / ( sqrt 5)))) by XCMPLX_1: 99

      .= ((((tn - ( tau_bar to_power n)) * S) ^2 ) - (((tx - ( tau_bar to_power X)) * S) * ((ty - ( tau_bar to_power Y)) / ( sqrt 5)))) by XCMPLX_1: 99

      .= ((((tn - ( tau_bar to_power n)) * S) ^2 ) - (((tx - ( tau_bar to_power X)) * S) * ((ty - ( tau_bar to_power Y)) * S))) by XCMPLX_1: 99

      .= ((S ^2 ) * ((((tn ^2 ) - ((2 * tn) * ((( - T) to_power ( - 1)) to_power n))) + (((( - T) to_power ( - 1)) to_power n) ^2 )) - ((tx - ((( - T) to_power ( - 1)) to_power X)) * (ty - ((( - T) to_power ( - 1)) to_power Y))))) by Th34

      .= ((S ^2 ) * ((((tn ^2 ) - ((2 * tn) * (( - T) to_power (( - 1) * n)))) + (((( - T) to_power ( - 1)) to_power n) ^2 )) - ((tx - ((( - T) to_power ( - 1)) to_power X)) * (ty - ((( - T) to_power ( - 1)) to_power Y))))) by A4, Th6

      .= ((S ^2 ) * ((((tn ^2 ) - ((2 * tn) * (( - T) to_power ( - n)))) + ((( - T) to_power (( - 1) * n)) ^2 )) - ((tx - ((( - T) to_power ( - 1)) to_power X)) * (ty - ((( - T) to_power ( - 1)) to_power Y))))) by A4, Th6

      .= ((S ^2 ) * ((((tn ^2 ) - ((2 * tn) * (( - T) to_power ( - n)))) + ((( - T) to_power ( - n)) ^2 )) - ((tx - (( - T) to_power (( - 1) * X))) * (ty - ((( - T) to_power ( - 1)) to_power Y))))) by Th35

      .= ((S ^2 ) * ((((tn ^2 ) - ((2 * tn) * (( - T) to_power ( - n)))) + ((( - T) to_power ( - n)) ^2 )) - ((tx - (( - T) to_power ( - X))) * (ty - (( - T) to_power (( - 1) * Y)))))) by Th35

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) * T) to_power ( - n)))) + (((( - 1) * T) to_power ( - n)) ^2 )) - (tx * ty)) + (tx * ((( - 1) * T) to_power ( - Y)))) + (((( - 1) * T) to_power ( - X)) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) * T) to_power ( - Y)))))

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) * T) to_power ( - n)))) + (((( - 1) * T) to_power ( - n)) ^2 )) - (tx * ty)) + (tx * ((( - 1) * T) to_power ( - Y)))) + (((( - 1) * T) to_power ( - X)) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) to_power ( - n)) * tnu))) + (((( - 1) * T) to_power ( - n)) ^2 )) - (tx * ty)) + (tx * ((( - 1) * T) to_power ( - Y)))) + (((( - 1) * T) to_power ( - X)) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) to_power ( - n)) * tnu))) + (((( - 1) to_power ( - n)) * tnu) ^2 )) - (tx * ty)) + (tx * ((( - 1) * T) to_power ( - Y)))) + (((( - 1) * T) to_power ( - X)) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) to_power ( - n)) * tnu))) + (((( - 1) to_power ( - n)) * tnu) ^2 )) - (tx * ty)) + (tx * ((( - 1) to_power ( - Y)) * tyu))) + (((( - 1) * T) to_power ( - X)) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) to_power ( - n)) * tnu))) + (((( - 1) to_power ( - n)) * tnu) ^2 )) - (tx * ty)) + (tx * ((( - 1) to_power ( - Y)) * tyu))) + (((( - 1) to_power ( - X)) * txu) * ty)) - (((( - 1) * T) to_power ( - X)) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * tn) * ((( - 1) to_power ( - n)) * tnu))) + (((( - 1) to_power ( - n)) * tnu) ^2 )) - (tx * ty)) + (tx * ((( - 1) to_power ( - Y)) * tyu))) + (((( - 1) to_power ( - X)) * txu) * ty)) - (((( - 1) to_power ( - X)) * txu) * ((( - 1) to_power ( - Y)) * tyu)))) by Th4

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * (tn * tnu)) * (( - 1) to_power ( - n)))) + (((( - 1) to_power ( - n)) ^2 ) * (tnu ^2 ))) - (tx * ty)) + ((tx * (( - 1) to_power ( - Y))) * tyu)) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * txu) * (( - 1) to_power ( - Y))) * tyu)))

      .= ((S ^2 ) * (((((((tn ^2 ) - ((2 * 1) * (( - 1) to_power ( - n)))) + (((( - 1) to_power ( - n)) ^2 ) * (tnu ^2 ))) - (tx * ty)) + ((tx * (( - 1) to_power ( - Y))) * tyu)) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * txu) * (( - 1) to_power ( - Y))) * tyu))) by Th10

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (1 * (tnu ^2 ))) - (tx * ty)) + ((tx * tyu) * (( - 1) to_power ( - Y)))) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * txu) * tyu))) by Th7

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (tx * ty)) + ((tx * (1 / ty)) * (( - 1) to_power ( - Y)))) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * txu) * tyu))) by Th33, POWER: 28

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (tx * ty)) + ((tx / ty) * (( - 1) to_power ( - Y)))) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * txu) * tyu))) by XCMPLX_1: 99

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (tx * ty)) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + (((( - 1) to_power ( - X)) * txu) * ty)) - ((((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * txu) * tyu))) by Th33, POWER: 29

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (X + Y))) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (ty * txu))) - (((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * (txu * tyu)))) by Th33, POWER: 27

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (X + Y))) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (ty * (1 / tx)))) - (((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * (txu * tyu)))) by Th33, POWER: 28

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (X + Y))) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (ty / tx))) - (((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * (txu * tyu)))) by XCMPLX_1: 99

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (X + Y))) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power (Y - X)))) - (((( - 1) to_power ( - X)) * (( - 1) to_power ( - Y))) * (txu * tyu)))) by Th33, POWER: 29

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (X + Y))) + ((T to_power (X - Y)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power (Y - X)))) - ((( - 1) to_power (( - X) - Y)) * (txu * tyu)))) by Th8

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - ((( - 1) to_power ( - (2 * n))) * (T to_power ( - (2 * n)))))) by A2, Th8

      .= ((S ^2 ) * (((((((tn ^2 ) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - (1 * (T to_power ( - (2 * n)))))) by Th9

      .= ((S ^2 ) * (((((((tn to_power 2) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - (1 * (T to_power ( - (2 * n)))))) by POWER: 46

      .= ((S ^2 ) * (((((((T to_power (2 * n)) - (2 * (( - 1) to_power ( - n)))) + (tnu ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - (T to_power ( - (2 * n))))) by Th33, POWER: 33

      .= ((S ^2 ) * (((((((T to_power (2 * n)) - (2 * (( - 1) to_power n))) + (tnu ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * (( - 1) to_power ( - Y)))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - (T to_power ( - (2 * n))))) by Th11

      .= ((S ^2 ) * (((((((T to_power (2 * n)) - (T to_power (2 * n))) - (2 * (( - 1) to_power n))) + (tnu ^2 )) + ((T to_power (2 * r)) * (( - 1) to_power Y))) + ((( - 1) to_power ( - X)) * (T to_power ( - (2 * r))))) - (T to_power ( - (2 * n))))) by Th11

      .= ((S ^2 ) * ((((( - (2 * (( - 1) to_power n))) + (tnu ^2 )) + ((T to_power (2 * r)) * (( - 1) to_power Y))) + ((( - 1) to_power X) * (T to_power ( - (2 * r))))) - (T to_power (2 * ( - n))))) by Th11

      .= ((S ^2 ) * ((((( - (2 * (( - 1) to_power n))) + (tnu ^2 )) + ((T to_power (2 * r)) * (( - 1) to_power Y))) + ((( - 1) to_power X) * (T to_power ( - (2 * r))))) - ((T to_power ( - n)) to_power 2))) by Th33, POWER: 33

      .= ((S ^2 ) * ((((( - (2 * (( - 1) to_power n))) + ((T to_power (2 * r)) * (( - 1) to_power Y))) + ((( - 1) to_power X) * (T to_power ( - (2 * r))))) + (tnu ^2 )) - (tnu ^2 ))) by POWER: 46

      .= ((S ^2 ) * ((( - (2 * (( - 1) to_power ((n -' r) + r)))) + ((( - 1) to_power Y) * (T to_power (2 * r)))) + ((( - 1) to_power ((2 * r) + Y)) * (T to_power ( - (2 * r)))))) by A3

      .= ((S ^2 ) * ((( - (2 * ((( - 1) to_power r) * (( - 1) to_power (n -' r))))) + ((( - 1) to_power Y) * (T to_power (2 * r)))) + ((( - 1) to_power ((2 * r) + Y)) * (T to_power ( - (2 * r)))))) by Th5

      .= ((S ^2 ) * ((( - (2 * ((( - 1) to_power r) * (( - 1) to_power (n -' r))))) + ((( - 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((( - 1) to_power (2 * r)) * (( - 1) to_power (n -' r))) * (T to_power ( - (2 * r)))))) by Th5

      .= (((S ^2 ) * ((( - (2 * (( - 1) to_power r))) + (T to_power (2 * r))) + ((T to_power ( - (2 * r))) * (( - 1) to_power (2 * r))))) * (( - 1) to_power (n -' r)))

      .= (((S ^2 ) * ((( - (2 * (( - 1) to_power r))) + (T to_power (2 * r))) + ((T to_power ( - (2 * r))) * 1))) * (( - 1) to_power (n -' r))) by Th3

      .= (((S ^2 ) * (((T to_power (2 * r)) - (2 * (( - 1) to_power r))) + (T to_power (2 * ( - r))))) * (( - 1) to_power (n -' r)))

      .= (((S ^2 ) * ((((T to_power r) to_power 2) - (2 * (( - 1) to_power r))) + (T to_power (( - r) * 2)))) * (( - 1) to_power (n -' r))) by Th33, POWER: 33

      .= (((S ^2 ) * ((((T to_power r) ^2 ) - (2 * (( - 1) to_power r))) + (T to_power (( - r) * 2)))) * (( - 1) to_power (n -' r))) by POWER: 46

      .= ((( - 1) to_power (n -' r)) * ((S ^2 ) * ((((T to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((T to_power ( - r)) to_power 2)))) by Th33, POWER: 33

      .= ((( - 1) to_power (n -' r)) * ((S ^2 ) * ((((T to_power r) ^2 ) - (2 * (( - 1) to_power r))) + ((T to_power ( - r)) ^2 )))) by POWER: 46

      .= ((( - 1) to_power (n -' r)) * ((S ^2 ) * ((( tau to_power r) - ( tau_bar to_power r)) ^2 ))) by Th37

      .= ((( - 1) to_power (n -' r)) * (((( tau to_power r) - ( tau_bar to_power r)) * S) ^2 ))

      .= ((( - 1) to_power (n -' r)) * (((( tau to_power r) - ( tau_bar to_power r)) / ( sqrt 5)) ^2 )) by XCMPLX_1: 99

      .= ((( - 1) |^ (n -' r)) * ((((T to_power r) - ( tau_bar to_power r)) / ( sqrt 5)) ^2 )) by POWER: 41

      .= ((( - 1) |^ (n -' r)) * (( Fib r) ^2 )) by FIB_NUM: 7;

      hence thesis;

    end;

    theorem :: FIB_NUM2:39

    ((( Fib n) ^2 ) + (( Fib (n + 1)) ^2 )) = ( Fib ((2 * n) + 1))

    proof

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



       A1: P[ 0 ] 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];

        assume

         A4: P[(k + 1)];

        ( Fib ((2 * (k + 2)) + 1)) = (( Fib ((2 * k) + 3)) + ( Fib ((2 * k) + 4))) by Lm1

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

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

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

        .= (((2 * (( Fib (k + 1)) ^2 )) + (2 * (( Fib (k + 2)) ^2 ))) + ((( Fib (k + 2)) - ( Fib k)) * (( Fib (k + 2)) + ( Fib k)))) by A3, A4

        .= (((2 * (( Fib (k + 1)) ^2 )) + (2 * (( Fib (k + 2)) ^2 ))) + (( Fib (k + 1)) * (( Fib (k + 2)) + ( Fib k)))) by Th29

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

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

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

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

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

        .= ((( Fib (k + 3)) ^2 ) + (( Fib (k + 2)) ^2 )) by Th25;

        hence thesis;

      end;



       A5: P[1] by Th21, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:40



     Th40: for k be non zero Element of NAT holds ( Fib (n + k)) = ((( Fib k) * ( Fib (n + 1))) + (( Fib (k -' 1)) * ( Fib n)))

    proof

      defpred P[ Nat] means ( Fib (n + $1)) = ((( Fib $1) * ( Fib (n + 1))) + (( Fib ($1 -' 1)) * ( Fib n)));

      ((( Fib 1) * ( Fib (n + 1))) + (( Fib (1 -' 1)) * ( Fib n))) = ((1 * ( Fib (n + 1))) + ( 0 * ( Fib n))) by PRE_FF: 1, XREAL_1: 232

      .= ( Fib (n + 1));

      then

       A1: P[1];



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

      proof

        let m be non zero Nat;



         A3: m >= 1 by NAT_2: 19;

        set F2 = (( Fib (m + 2)) * ( Fib (n + 1)));

        set F1 = (( Fib (n + 1)) * ( Fib (m + 2)));

        set k = (m -' 1);

        assume

         A4: P[m] & P[(m + 1)];

        ( Fib (n + (m + 2))) = ( Fib ((n + m) + 2))

        .= (( Fib (n + m)) + ( Fib ((n + m) + 1))) by Th24

        .= (((( Fib m) * ( Fib (n + 1))) + (( Fib k) * ( Fib n))) + ((( Fib (m + 1)) * ( Fib (n + 1))) + (( Fib (m + (1 -' 1))) * ( Fib n)))) by A4, NAT_D: 38

        .= (((( Fib m) * ( Fib (n + 1))) + (( Fib k) * ( Fib n))) + ((( Fib (m + 1)) * ( Fib (n + 1))) + (( Fib (m + 0 qua Nat)) * ( Fib n)))) by XREAL_1: 232

        .= ((( Fib (n + 1)) * (( Fib m) + ( Fib (m + 1)))) + (( Fib n) * (( Fib k) + ( Fib m))))

        .= (F1 + (( Fib n) * (( Fib k) + ( Fib m)))) by Th24

        .= (F1 + (( Fib n) * (( Fib k) + ( Fib (k + 1))))) by A3, XREAL_1: 235

        .= (F2 + (( Fib n) * ( Fib ((m -' 1) + 2)))) by Th24

        .= (F2 + (( Fib ((m + 2) -' 1)) * ( Fib n))) by A3, NAT_D: 38;

        hence thesis;

      end;

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

      then

       A5: P[2] by Th21, Th24, PRE_FF: 1;

      for k be non zero Nat holds P[k] from FibInd1( A1, A5, A2);

      hence thesis;

    end;

    theorem :: FIB_NUM2:41



     Th41: for n be non zero Element of NAT holds ( Fib n) divides ( Fib (n * k))

    proof

      let n be non zero Element of NAT ;

      defpred P[ Nat] means ( Fib n) divides ( Fib (n * $1));



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

      proof

        let k be Nat;

        assume

         A2: P[k];

        ( Fib (n * (k + 1))) = ( Fib ((n * k) + n))

        .= ((( Fib n) * ( Fib ((n * k) + 1))) + (( Fib (n * k)) * ( Fib (n -' 1)))) by Th40;

        hence thesis by A2, Th12;

      end;



       A3: P[ 0 ] by NAT_D: 6, PRE_FF: 1;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:42



     Th42: for k be non zero Element of NAT holds k divides n implies ( Fib k) divides ( Fib n)

    proof

      let k be non zero Element of NAT ;

      assume k divides n;

      then ex m be Nat st n = (k * m) by NAT_D:def 3;

      hence thesis by Th41;

    end;

    theorem :: FIB_NUM2:43



     Th43: ( Fib n) <= ( Fib (n + 1))

    proof

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



       A1: P[ 0 ] 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];

        assume P[(k + 1)];

        then (( Fib k) + ( Fib (k + 1))) <= (( Fib (k + 1)) + ( Fib (k + 2))) by A3, XREAL_1: 7;

        then ( Fib (k + 2)) <= (( Fib (k + 1)) + ( Fib (k + 2))) by Th24;

        then ( Fib (k + 2)) <= ( Fib (k + 3)) by Th25;

        hence thesis;

      end;



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

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:44



     Th44: for n be Nat st n > 1 holds ( Fib n) < ( Fib (n + 1))

    proof

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

      let n be Nat;

      assume n > 1;

      then

       A1: n is non trivial by NAT_2:def 1;



       A2: P[3] by Th22, Th23;



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

      proof

        let k be non trivial Nat;

        assume

         A4: P[k];

        assume P[(k + 1)];

        then (( Fib k) + ( Fib (k + 1))) < (( Fib (k + 1)) + ( Fib (k + 2))) by A4, XREAL_1: 8;

        then ( Fib (k + 2)) < (( Fib (k + 1)) + ( Fib (k + 2))) by Th24;

        then ( Fib (k + 2)) < ( Fib (k + 3)) by Th25;

        hence thesis;

      end;



       A5: P[2] by Th21, Th22;

      for n be non trivial Nat holds P[n] from FibInd2( A5, A2, A3);

      hence thesis by A1;

    end;

    theorem :: FIB_NUM2:45

    for m, n st m >= n holds ( Fib m) >= ( Fib n)

    proof

      let m, n;

      assume m >= n;

      then

      consider k be Nat such that

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

      for k,n be Nat holds ( Fib (n + k)) >= ( Fib n)

      proof

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



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

        proof

          let k;

          assume

           A3: P[k];

          let n;

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

          then

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

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

          hence thesis by A4, XXREAL_0: 2;

        end;

        let k;

        let n;



         A5: P[ 0 ];

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

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: FIB_NUM2:46



     Th46: for k be Nat st k > 1 holds k < n implies ( Fib k) < ( Fib n)

    proof

      let k be Nat such that

       A1: k > 1;

      assume

       A2: k < n;

      then

      consider m be Nat such that

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

      reconsider k as non zero Element of NAT by A1, ORDINAL1:def 12;

      reconsider m as non zero Element of NAT by A2, A3, ORDINAL1:def 12;

      for k,m be non zero Element of NAT st k > 1 holds ( Fib k) < ( Fib (k + m))

      proof

        let k,m be non zero Element of NAT such that

         A4: k > 1;

        defpred P[ Nat] means ( Fib k) < ( Fib (k + $1));



         A5: for r be non zero Nat st P[r] holds P[(r + 1)]

        proof

          let r be non zero Nat;

          (k + r) > ( 0 + 1) by A4, XREAL_1: 8;

          then

           A6: ( Fib (k + r)) < ( Fib ((k + r) + 1)) by Th44;

          assume P[r];

          hence thesis by A6, XXREAL_0: 2;

        end;



         A7: P[1] by A4, Th44;

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

        hence thesis;

      end;

      then ( Fib k) < ( Fib (k + m)) by A1;

      hence thesis by A3;

    end;

    theorem :: FIB_NUM2:47



     Th47: ( Fib k) = 1 iff k = 1 or k = 2

    proof

      ( Fib k) = 1 implies k = 1 or k = 2

      proof

        assume

         A1: ( Fib k) = 1;

        assume that

         A2: not k = 1 and

         A3: not k = 2;



         A4: k < 2 or k > 2 by A3, XXREAL_0: 1;

        k = 0 or k > 1 by A2, NAT_2: 19;

        hence contradiction by A1, A4, Th21, Th46, PRE_FF: 1;

      end;

      hence thesis by Th21, PRE_FF: 1;

    end;

    theorem :: FIB_NUM2:48



     Th48: for k,n be Element of NAT st n > 1 & k <> 0 & k <> 1 holds ( Fib k) = ( Fib n) iff k = n

    proof

      let k,n be Element of NAT such that

       A1: n > 1 and

       A2: k <> 0 & k <> 1;

      k is non trivial by A2, NAT_2:def 1;

      then k >= (1 + 1) by NAT_2: 29;

      then

       A3: k > 1 by NAT_1: 13;

      ( Fib k) = ( Fib n) implies k = n

      proof

        assume

         A4: ( Fib k) = ( Fib n);

        assume

         A5: k <> n;

        per cases by A5, XXREAL_0: 1;

          suppose k > n;

          hence contradiction by A1, A4, Th46;

        end;

          suppose k < n;

          hence contradiction by A3, A4, Th46;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIB_NUM2:49



     Th49: for n be Element of NAT st n > 1 & n <> 4 holds n is non prime implies ex k be non zero Element of NAT st k <> 1 & k <> 2 & k <> n & k divides n

    proof

      let n be Element of NAT such that

       A1: n > 1 and

       A2: n <> 4;

      assume

       A3: n is non prime;

      per cases by A3, INT_2:def 4;

        suppose n <= 1;

        hence thesis by A1;

      end;

        suppose not for k be Nat holds k divides n implies k = 1 or k = n;

        then

        consider k be Nat such that

         A4: k divides n and

         A5: k <> 1 & k <> n;

        consider m be Nat such that

         A6: n = (k * m) by A4, NAT_D:def 3;



         A7: m divides n & m is non zero Element of NAT by A1, A6, NAT_D:def 3, ORDINAL1:def 12;



         A8: k is non zero Element of NAT by A1, A4, INT_2: 3, ORDINAL1:def 12;



         A9: k <> 2 or m <> 2 by A2, A6;

        m <> 1 & m <> n by A1, A5, A6, XCMPLX_1: 7;

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

      end;

    end;

    theorem :: FIB_NUM2:50

    for n be Element of NAT st n > 1 & n <> 4 holds ( Fib n) is prime implies n is prime

    proof

      let n be Element of NAT such that

       A1: n > 1 and

       A2: n <> 4;

      assume

       A3: ( Fib n) is prime;

      assume not n is prime;

      then

      consider k be non zero Element of NAT such that

       A4: k <> 1 and

       A5: k <> 2 and

       A6: k <> n and

       A7: k divides n by A1, A2, Th49;



       A8: ( Fib k) <> ( Fib n) by A1, A4, A6, Th48;

      ( Fib k) <> 1 & ( Fib k) divides ( Fib n) by A4, A5, A7, Th42, Th47;

      hence contradiction by A3, A8, INT_2:def 4;

    end;

    begin

    definition

      :: FIB_NUM2:def2

      func FIB -> sequence of NAT means

      : Def2: for k be Element of NAT holds (it . k) = ( Fib k);

      existence

      proof

        ex f be sequence of NAT st for x be Element of NAT holds (f . x) = ( Fib x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof



         A1: for f1,f2 be sequence of NAT st (for x be Element of NAT holds (f1 . x) = ( Fib x)) & (for x be Element of NAT holds (f2 . x) = ( Fib x)) holds f1 = f2 from BINOP_2:sch 1;

        let f1,f2 be sequence of NAT ;

        assume (for k be Element of NAT holds (f1 . k) = ( Fib k)) & for k be Element of NAT holds (f2 . k) = ( Fib k);

        hence thesis by A1;

      end;

    end

    definition

      :: FIB_NUM2:def3

      func EvenNAT -> Subset of NAT equals the set of all (2 * k) where k be Nat;

      coherence

      proof

         the set of all (2 * k) where k be Nat c= NAT

        proof

          let x be object;

          assume x in the set of all (2 * k) where k be Nat;

          then ex k be Nat st x = (2 * k);

          hence thesis by ORDINAL1:def 12;

        end;

        hence thesis;

      end;

      :: FIB_NUM2:def4

      func OddNAT -> Subset of NAT equals the set of all ((2 * k) + 1) where k be Element of NAT ;

      coherence

      proof

        defpred P[ set] means not contradiction;

        deffunc F( Element of NAT ) = ((2 * $1) + 1);

        { F(k) where k be Element of NAT : P[k] } is Subset of NAT from DOMAIN_1:sch 8;

        hence thesis;

      end;

    end

    theorem :: FIB_NUM2:51



     Th51: for k be Nat holds (2 * k) in EvenNAT & not ((2 * k) + 1) in EvenNAT

    proof

      let k be Nat;

      thus (2 * k) in EvenNAT ;

      assume ((2 * k) + 1) in EvenNAT ;

      then ex p be Nat st ((2 * k) + 1) = (2 * p);

      hence thesis;

    end;

    theorem :: FIB_NUM2:52



     Th52: for k be Element of NAT holds ((2 * k) + 1) in OddNAT & not (2 * k) in OddNAT

    proof

      let k be Element of NAT ;

      thus ((2 * k) + 1) in OddNAT ;

      assume (2 * k) in OddNAT ;

      then ex p be Element of NAT st (2 * k) = ((2 * p) + 1);

      hence thesis;

    end;

    definition

      let n be Nat;

      :: FIB_NUM2:def5

      func EvenFibs (n) -> FinSequence of NAT equals ( Prefix ( FIB ,( EvenNAT /\ ( Seg n))));

      coherence ;

      :: FIB_NUM2:def6

      func OddFibs (n) -> FinSequence of NAT equals ( Prefix ( FIB ,( OddNAT /\ ( Seg n))));

      coherence ;

    end

    theorem :: FIB_NUM2:53



     Th53: ( EvenFibs 0 ) = {} ;

    theorem :: FIB_NUM2:54

    ( Seq ( FIB | {2})) = <*1*>

    proof

      reconsider H = { [2, ( FIB . 2)]} as Function;



       A1: ( dom H) = {2} by RELAT_1: 9;

      ( dom H) c= ( Seg 2)

      proof

        let x be object;

        assume x in ( dom H);

        then x = 2 by A1, TARSKI:def 1;

        hence thesis;

      end;

      then

      reconsider H as FinSubsequence by FINSEQ_1:def 12;

      2 in NAT ;

      then 2 in ( dom FIB ) by FUNCT_2:def 1;



      then ( Seq ( FIB | {2})) = ( Seq H) by GRFUNC_1: 28

      .= <*( FIB . 2)*> by FINSEQ_3: 157

      .= <*1*> by Def2, Th21;

      hence thesis;

    end;

    theorem :: FIB_NUM2:55



     Th55: ( EvenFibs 2) = <*1*>

    proof

      now

        let x be object;

        assume

         A1: x in ( EvenNAT /\ {1, 2});

        then

         A2: x in EvenNAT by XBOOLE_0:def 4;



         A3: x in {1, 2} by A1, XBOOLE_0:def 4;

        per cases by A3, TARSKI:def 2;

          suppose x = 1;

          then x = ( 0 + 1);

          then

           A4: x = ((2 * 0 qua Nat) + 1);

          ex k be Nat st x = (2 * k) by A2;

          hence x in {2} by A4;

        end;

          suppose x = (2 * 1);

          hence x in {2} by TARSKI:def 1;

        end;

      end;

      then

       A5: ( EvenNAT /\ {1, 2}) c= {2};

      set q = { [2, ( FIB . 2)]};

      reconsider q as FinSubsequence by Th17;

      2 in NAT ;

      then

       A6: 2 in ( dom FIB ) by FUNCT_2:def 1;

      now

        let x be object;

        assume x in {2};

        then x = (2 * 1) by TARSKI:def 1;

        then x in EvenNAT & x in {1, 2} by TARSKI:def 2;

        hence x in ( EvenNAT /\ {1, 2}) by XBOOLE_0:def 4;

      end;

      then {2} c= ( EvenNAT /\ {1, 2});

      then ( EvenNAT /\ {1, 2}) = {2} by A5;



      then ( EvenFibs 2) = ( Seq q) by A6, FINSEQ_1: 2, GRFUNC_1: 28

      .= <*( FIB . 2)*> by FINSEQ_3: 157

      .= <*1*> by Def2, Th21;

      hence thesis;

    end;

    theorem :: FIB_NUM2:56

    ( EvenFibs 4) = <*1, 3*>

    proof

      now

        let x be object;

        assume

         A1: x in ( EvenNAT /\ {1, 2, 3, 4});

        then

         A2: x in EvenNAT by XBOOLE_0:def 4;



         A3: x in {1, 2, 3, 4} by A1, XBOOLE_0:def 4;

        per cases by A3, ENUMSET1:def 2;

          suppose x = ((2 * 0 qua Nat) + 1);

          hence x in {2, 4} by A2, Th51;

        end;

          suppose x = (2 * 1);

          hence x in {2, 4} by TARSKI:def 2;

        end;

          suppose x = ((2 * 1) + 1);

          hence x in {2, 4} by A2, Th51;

        end;

          suppose x = (2 * 2);

          hence x in {2, 4} by TARSKI:def 2;

        end;

      end;

      then

       A4: ( EvenNAT /\ {1, 2, 3, 4}) c= {2, 4};

      set q = { [2, ( FIB . 2)], [4, ( FIB . 4)]};

      4 in NAT ;

      then

       A5: 4 in ( dom FIB ) by FUNCT_2:def 1;

      reconsider q as FinSubsequence by Th15;

      2 in NAT ;

      then

       A6: 2 in ( dom FIB ) by FUNCT_2:def 1;



       A7: ( FIB | ( {2} \/ {4})) = (( FIB | {2}) \/ ( FIB | {4})) by RELAT_1: 78

      .= ( { [2, ( FIB . 2)]} \/ ( FIB | {4})) by A6, GRFUNC_1: 28

      .= ( { [2, ( FIB . 2)]} \/ { [4, ( FIB . 4)]}) by A5, GRFUNC_1: 28

      .= q by ENUMSET1: 1;

      now

        let x be object;

        assume

         A8: x in {2, 4};

        then x = (2 * 1) or x = (2 * 2) by TARSKI:def 2;

        then

         A9: x in EvenNAT ;

        x = 2 or x = 4 by A8, TARSKI:def 2;

        then x in {1, 2, 3, 4} by ENUMSET1:def 2;

        hence x in ( EvenNAT /\ {1, 2, 3, 4}) by A9, XBOOLE_0:def 4;

      end;

      then {2, 4} c= ( EvenNAT /\ {1, 2, 3, 4});

      then ( EvenNAT /\ {1, 2, 3, 4}) = {2, 4} by A4;



      then ( EvenFibs 4) = ( Seq q) by A7, ENUMSET1: 1, FINSEQ_3: 2

      .= <*( FIB . 2), ( FIB . 4)*> by Th16

      .= <*( Fib 2), ( FIB . 4)*> by Def2

      .= <*1, 3*> by Def2, Th21, Th23;

      hence thesis;

    end;

    theorem :: FIB_NUM2:57



     Th57: for k be Nat holds (( EvenNAT /\ ( Seg ((2 * k) + 2))) \/ {((2 * k) + 4)}) = ( EvenNAT /\ ( Seg ((2 * k) + 4)))

    proof

      let k be Nat;

      ((2 * k) + 4) = (2 * (k + 2));

      then

       A1: ((2 * k) + 4) in EvenNAT ;

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

      then

       A2: {((2 * k) + 3)} misses EvenNAT by Th51, ZFMISC_1: 50;

      ( EvenNAT /\ ( Seg ((2 * k) + 4))) = ( EvenNAT /\ ( Seg (((2 * k) + 3) + 1)))

      .= ( EvenNAT /\ (( Seg ((2 * k) + 3)) \/ {((2 * k) + 4)})) by FINSEQ_1: 9

      .= (( EvenNAT /\ ( Seg ((2 * k) + 3))) \/ ( EvenNAT /\ {((2 * k) + 4)})) by XBOOLE_1: 23

      .= (( EvenNAT /\ ( Seg (((2 * k) + 2) + 1))) \/ {((2 * k) + 4)}) by A1, ZFMISC_1: 46

      .= (( EvenNAT /\ (( Seg ((2 * k) + 2)) \/ {((2 * k) + 3)})) \/ {((2 * k) + 4)}) by FINSEQ_1: 9

      .= ((( EvenNAT /\ ( Seg ((2 * k) + 2))) \/ ( EvenNAT /\ {((2 * k) + 3)})) \/ {((2 * k) + 4)}) by XBOOLE_1: 23

      .= ((( EvenNAT /\ ( Seg ((2 * k) + 2))) \/ {} ) \/ {((2 * k) + 4)}) by A2

      .= (( EvenNAT /\ ( Seg ((2 * k) + 2))) \/ {((2 * k) + 4)});

      hence thesis;

    end;

    theorem :: FIB_NUM2:58



     Th58: for k be Nat holds (( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 2)))) \/ { [((2 * k) + 4), ( FIB . ((2 * k) + 4))]}) = ( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 4))))

    proof

      let k be Nat;



       A1: ( dom FIB ) = NAT by FUNCT_2:def 1;

      ( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 4)))) = ( FIB | (( EvenNAT /\ ( Seg ((2 * k) + 2))) \/ {((2 * k) + 4)})) by Th57

      .= (( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 2)))) \/ ( FIB | {((2 * k) + 4)})) by RELAT_1: 78

      .= (( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 2)))) \/ { [((2 * k) + 4), ( FIB . ((2 * k) + 4))]}) by A1, GRFUNC_1: 28;

      hence thesis;

    end;

    theorem :: FIB_NUM2:59



     Th59: for n be Element of NAT holds ( EvenFibs ((2 * n) + 2)) = (( EvenFibs (2 * n)) ^ <*( Fib ((2 * n) + 2))*>)

    proof

      defpred P[ Nat] means ( EvenFibs ((2 * $1) + 2)) = (( EvenFibs (2 * $1)) ^ <*( Fib ((2 * $1) + 2))*>);

      let n be Element of NAT ;



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

      proof

        let k be Nat;

        reconsider ARR = { [1, ( FIB . ((2 * k) + 4))]} as FinSubsequence by Th17;

        assume P[k];

        set LEFTk = ( EvenFibs ((2 * (k + 1)) + 2));

        set RIGHTk = (( EvenFibs (2 * (k + 1))) ^ <*( Fib ((2 * (k + 1)) + 2))*>);

        reconsider RS = ( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 2)))) as FinSubsequence;

        set RR = ( Shift (ARR,((2 * k) + 3)));



         A2: ((2 * k) + 3) > ((2 * k) + 2) by XREAL_1: 6;

        ( dom RS) c= ( EvenNAT /\ ( Seg ((2 * k) + 2))) & ( EvenNAT /\ ( Seg ((2 * k) + 2))) c= ( Seg ((2 * k) + 2)) by RELAT_1: 58, XBOOLE_1: 17;

        then

        consider p1 be FinSequence such that

         A3: RS c= p1 and

         A4: ( dom p1) = ( Seg ((2 * k) + 3)) by A2, Th19, XBOOLE_1: 1;



         A5: ex p2 be FinSequence st ARR c= p2 by Th20;

        (1 + ((2 * k) + 3)) = ((2 * k) + 4);

        then

         A6: RR = { [((2 * k) + 4), ( FIB . ((2 * k) + 4))]} by Th18;

        ( len p1) = ((2 * k) + 3) by A4, FINSEQ_1:def 3;

        then

        consider RSR be FinSubsequence such that

         A7: RSR = (RS \/ RR) and

         A8: (( Seq RS) ^ ( Seq ARR)) = ( Seq RSR) by A3, A5, VALUED_1: 64;

        RIGHTk = (( Seq ( FIB | ( EvenNAT /\ ( Seg ((2 * k) + 2))))) ^ <*( FIB . ((2 * k) + 4))*>) by Def2

        .= ( Seq RSR) by A8, FINSEQ_3: 157

        .= LEFTk by A7, A6, Th58;

        hence thesis;

      end;



       A9: P[ 0 ] by Th21, Th53, Th55, FINSEQ_1: 34;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:60



     Th60: ( OddFibs 1) = <*1*>

    proof

      now

        let x be object;

        assume

         A1: x in {1};

        then x = ((2 * 0 qua Nat) + 1) by TARSKI:def 1;

        then x in OddNAT ;

        hence x in ( OddNAT /\ {1}) by A1, XBOOLE_0:def 4;

      end;

      then

       A2: {1} c= ( OddNAT /\ {1});

      1 in NAT ;

      then

       A3: 1 in ( dom FIB ) by FUNCT_2:def 1;

      for x be object st x in ( OddNAT /\ {1}) holds x in {1} by XBOOLE_0:def 4;

      then ( OddNAT /\ {1}) c= {1};

      then ( OddNAT /\ {1}) = {1} by A2;



      then ( OddFibs 1) = <*( FIB . 1)*> by A3, FINSEQ_1: 2, FINSEQ_3: 157, GRFUNC_1: 28

      .= <*1*> by Def2, PRE_FF: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:61



     Th61: ( OddFibs 3) = <*1, 2*>

    proof

      now

        let x be object;

        assume

         A1: x in ( OddNAT /\ {1, 2, 3});

        then

         A2: x in OddNAT by XBOOLE_0:def 4;



         A3: x in {1, 2, 3} by A1, XBOOLE_0:def 4;

        per cases by A3, ENUMSET1:def 1;

          suppose x = ((2 * 0 qua Nat) + 1);

          hence x in {1, 3} by TARSKI:def 2;

        end;

          suppose x = (2 * 1);

          hence x in {1, 3} by A2, Th52;

        end;

          suppose x = ((2 * 1) + 1);

          hence x in {1, 3} by TARSKI:def 2;

        end;

      end;

      then

       A4: ( OddNAT /\ {1, 2, 3}) c= {1, 3};

      set q = { [1, ( FIB . 1)], [3, ( FIB . 3)]};

      3 in NAT ;

      then

       A5: 3 in ( dom FIB ) by FUNCT_2:def 1;

      reconsider q as FinSubsequence by Th15;

      1 in NAT ;

      then

       A6: 1 in ( dom FIB ) by FUNCT_2:def 1;



       A7: ( FIB | ( {1} \/ {3})) = (( FIB | {1}) \/ ( FIB | {3})) by RELAT_1: 78

      .= ( { [1, ( FIB . 1)]} \/ ( FIB | {3})) by A6, GRFUNC_1: 28

      .= ( { [1, ( FIB . 1)]} \/ { [3, ( FIB . 3)]}) by A5, GRFUNC_1: 28

      .= q by ENUMSET1: 1;

      now

        let x be object;

        assume

         A8: x in {1, 3};

        then x = ((2 * 0 qua Nat) + 1) or x = ((2 * 1) + 1) by TARSKI:def 2;

        then

         A9: x in OddNAT ;

        x = 1 or x = 3 by A8, TARSKI:def 2;

        then x in {1, 2, 3} by ENUMSET1:def 1;

        hence x in ( OddNAT /\ {1, 2, 3}) by A9, XBOOLE_0:def 4;

      end;

      then {1, 3} c= ( OddNAT /\ {1, 2, 3});

      then ( OddNAT /\ {1, 2, 3}) = {1, 3} by A4;



      then ( OddFibs 3) = ( Seq ( FIB | ( {1} \/ {3}))) by ENUMSET1: 1, FINSEQ_3: 1

      .= <*( FIB . 1), ( FIB . 3)*> by A7, Th16

      .= <*( Fib 1), ( FIB . 3)*> by Def2

      .= <*1, 2*> by Def2, Th22, PRE_FF: 1;

      hence thesis;

    end;

    theorem :: FIB_NUM2:62



     Th62: for k be Nat holds (( OddNAT /\ ( Seg ((2 * k) + 3))) \/ {((2 * k) + 5)}) = ( OddNAT /\ ( Seg ((2 * k) + 5)))

    proof

      let k be Nat;

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

      then

       A1: ((2 * k) + 5) in OddNAT ;

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

      then

       A2: {((2 * k) + 4)} misses OddNAT by Th52, ZFMISC_1: 50;

      ( OddNAT /\ ( Seg ((2 * k) + 5))) = ( OddNAT /\ ( Seg (((2 * k) + 4) + 1)))

      .= ( OddNAT /\ (( Seg ((2 * k) + 4)) \/ {((2 * k) + 5)})) by FINSEQ_1: 9

      .= (( OddNAT /\ ( Seg (((2 * k) + 3) + 1))) \/ ( OddNAT /\ {((2 * k) + 5)})) by XBOOLE_1: 23

      .= (( OddNAT /\ (( Seg ((2 * k) + 3)) \/ {((2 * k) + 4)})) \/ ( OddNAT /\ {((2 * k) + 5)})) by FINSEQ_1: 9

      .= ((( OddNAT /\ ( Seg ((2 * k) + 3))) \/ ( OddNAT /\ {((2 * k) + 4)})) \/ ( OddNAT /\ {((2 * k) + 5)})) by XBOOLE_1: 23

      .= ((( OddNAT /\ ( Seg ((2 * k) + 3))) \/ {} ) \/ ( OddNAT /\ {((2 * k) + 5)})) by A2

      .= (( OddNAT /\ ( Seg ((2 * k) + 3))) \/ {((2 * k) + 5)}) by A1, ZFMISC_1: 46;

      hence thesis;

    end;

    theorem :: FIB_NUM2:63



     Th63: for k be Nat holds (( FIB | ( OddNAT /\ ( Seg ((2 * k) + 3)))) \/ { [((2 * k) + 5), ( FIB . ((2 * k) + 5))]}) = ( FIB | ( OddNAT /\ ( Seg ((2 * k) + 5))))

    proof

      let k be Nat;



       A1: ( dom FIB ) = NAT by FUNCT_2:def 1;

      ( FIB | ( OddNAT /\ ( Seg ((2 * k) + 5)))) = ( FIB | (( OddNAT /\ ( Seg ((2 * k) + 3))) \/ {((2 * k) + 5)})) by Th62

      .= (( FIB | ( OddNAT /\ ( Seg ((2 * k) + 3)))) \/ ( FIB | {((2 * k) + 5)})) by RELAT_1: 78

      .= (( FIB | ( OddNAT /\ ( Seg ((2 * k) + 3)))) \/ { [((2 * k) + 5), ( FIB . ((2 * k) + 5))]}) by A1, GRFUNC_1: 28;

      hence thesis;

    end;

    theorem :: FIB_NUM2:64



     Th64: for n be Nat holds ( OddFibs ((2 * n) + 3)) = (( OddFibs ((2 * n) + 1)) ^ <*( Fib ((2 * n) + 3))*>)

    proof

      defpred P[ Nat] means ( OddFibs ((2 * $1) + 3)) = (( OddFibs ((2 * $1) + 1)) ^ <*( Fib ((2 * $1) + 3))*>);

      let n be Nat;



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

      proof

        let k be Nat;

        reconsider ARR = { [1, ( FIB . ((2 * k) + 5))]} as FinSubsequence by Th17;

        assume P[k];

        set LEFTk = ( OddFibs ((2 * (k + 1)) + 3));

        set RIGHTk = (( OddFibs ((2 * (k + 1)) + 1)) ^ <*( Fib ((2 * (k + 1)) + 3))*>);

        reconsider RS = ( FIB | ( OddNAT /\ ( Seg ((2 * k) + 3)))) as FinSubsequence;

        set RR = ( Shift (ARR,((2 * k) + 4)));



         A2: ((2 * k) + 4) > ((2 * k) + 3) by XREAL_1: 6;

        ( dom RS) c= ( OddNAT /\ ( Seg ((2 * k) + 3))) & ( OddNAT /\ ( Seg ((2 * k) + 3))) c= ( Seg ((2 * k) + 3)) by RELAT_1: 58, XBOOLE_1: 17;

        then

        consider p1 be FinSequence such that

         A3: RS c= p1 and

         A4: ( dom p1) = ( Seg ((2 * k) + 4)) by A2, Th19, XBOOLE_1: 1;



         A5: ex p2 be FinSequence st ARR c= p2 by Th20;

        (1 + ((2 * k) + 4)) = ((2 * k) + 5);

        then

         A6: RR = { [((2 * k) + 5), ( FIB . ((2 * k) + 5))]} by Th18;

        ( len p1) = ((2 * k) + 4) by A4, FINSEQ_1:def 3;

        then

        consider RSR be FinSubsequence such that

         A7: RSR = (RS \/ RR) and

         A8: (( Seq RS) ^ ( Seq ARR)) = ( Seq RSR) by A3, A5, VALUED_1: 64;

        RIGHTk = (( Seq ( FIB | ( OddNAT /\ ( Seg ((2 * k) + 3))))) ^ <*( FIB . ((2 * k) + 5))*>) by Def2

        .= ( Seq RSR) by A8, FINSEQ_3: 157

        .= LEFTk by A7, A6, Th63;

        hence thesis;

      end;



       A9: P[ 0 ] by Th22, Th60, Th61;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:65

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

    proof

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

      let n be Element of NAT ;



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

      proof

        let k be Nat;

        reconsider EE = ( EvenFibs (2 * (k + 1))) as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

        assume

         A2: P[k];

        ( Sum ( EvenFibs ((2 * (k + 1)) + 2))) = ( Sum (( EvenFibs (2 * (k + 1))) qua FinSequence of NAT ^ <*( Fib ((2 * (k + 1)) + 2))*>)) by Th59

        .= (( Sum EE) + ( Fib ((2 * (k + 1)) + 2))) by RVSUM_1: 74

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

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

        hence thesis;

      end;



       A3: P[ 0 ] by Th22, Th55, RVSUM_1: 73;

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

      hence thesis;

    end;

    theorem :: FIB_NUM2:66

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

    proof

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

      let n be Nat;



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

      proof

        let k be Nat;

        reconsider EE = ( OddFibs ((2 * k) + 1)) as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

        assume

         A2: P[k];

        ( Sum ( OddFibs ((2 * (k + 1)) + 1))) = ( Sum (( OddFibs ((2 * k) + 1)) ^ <*( Fib ((2 * k) + 3)) qua Element of NAT *>)) by Th64

        .= (( Sum EE) + ( Fib ((2 * k) + 3))) by RVSUM_1: 74

        .= ( Fib ((2 * k) + 4)) by A2, Th26;

        hence thesis;

      end;



       A3: P[ 0 ] by Th21, Th60, RVSUM_1: 73;

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

      hence thesis;

    end;

    begin

    theorem :: FIB_NUM2:67



     Th67: for n be Element of NAT holds (( Fib n),( Fib (n + 1))) are_coprime

    proof

      let n be Element of NAT ;



       A1: (n,(n + 1)) are_coprime by PEPIN: 1;

      (( Fib n) gcd ( Fib (n + 1))) = ( Fib (n gcd (n + 1))) by FIB_NUM: 5

      .= 1 by A1, INT_2:def 3, PRE_FF: 1;

      hence thesis by INT_2:def 3;

    end;

    theorem :: FIB_NUM2:68



     Th68: for n be non zero Nat, m be Nat st m <> 1 holds m divides ( Fib n) implies not m divides ( Fib (n -' 1))

    proof

      let n be non zero Nat;

      let m be Nat;

      assume

       A1: m <> 1;

      assume

       A2: m divides ( Fib n);

      n >= 1 by NAT_2: 19;

      then n = ((n -' 1) + 1) by XREAL_1: 235;

      then (( Fib (n -' 1)),( Fib n)) are_coprime by Th67;

      then

       A3: (( Fib (n -' 1)) gcd ( Fib n)) = 1 by INT_2:def 3;

      assume m divides ( Fib (n -' 1));

      then m divides 1 by A2, A3, NAT_D:def 5;

      hence contradiction by A1, WSIERP_1: 15;

    end;

    ::$Notion-Name

    theorem :: FIB_NUM2:69

    for n be non zero Nat holds m is prime & n is prime & m divides ( Fib n) implies for r be Nat st r < n & r <> 0 holds not m divides ( Fib r)

    proof

      let n be non zero Nat;

      assume

       A1: m is prime;

      defpred R[ Element of NAT ] means $1 < n & $1 <> 0 & m divides ( Fib $1);

      assume

       A2: n is prime;

      reconsider C = { x where x be Element of NAT : R[x] } as Subset of NAT from DOMAIN_1:sch 7;

      assume

       A3: m divides ( Fib n);

      assume

       A4: not for r be Nat st (r < n & r <> 0 ) holds not m divides ( Fib r);

      C is non empty Subset of NAT

      proof

        consider r be Nat such that

         A5: r < n & r <> 0 & m divides ( Fib r) by A4;

        r in NAT by ORDINAL1:def 12;

        then r in C by A5;

        hence thesis;

      end;

      then

      reconsider C as non empty Subset of NAT ;

      reconsider r = ( min C) as Nat by TARSKI: 1;

      defpred P[ Nat] means (m divides ( Fib (n -' (r * ($1 + 1)))) & r <= (n / ($1 + 2)));

      r in C by XXREAL_2:def 7;

      then

       A6: ex r9 be Element of NAT st r9 = r & R[r9];

      then

       A7: (n -' r) < n by NAT_2: 9;

      m <> 1 by A1, INT_2:def 4;

      then

       A8: not m divides ( Fib (r -' 1)) by A6, Th68;



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

      proof

        let k be Nat;



         A10: m divides (( Fib r) * ( Fib ((n -' ((k + 2) * r)) + 1))) by A6, NAT_D: 9;



         A11: (n - (r * (k + 2))) <> 0

        proof

          assume

           A12: (n - (r * (k + 2))) = 0 ;

          then

           A13: r divides n & (k + 2) divides n by NAT_D:def 3;

          per cases by A2, A13, INT_2:def 4;

            suppose r = 1 & (k + 2) = n;

            then m = 1 by A6, PRE_FF: 1, WSIERP_1: 15;

            hence contradiction by A1, INT_2:def 4;

          end;

            suppose r = 1 & (k + 2) = 1;

            hence contradiction by A2, A12, INT_2:def 4;

          end;

            suppose r = n & (k + 2) = n;

            hence contradiction by A6;

          end;

            suppose r = n & (k + 2) = 1;

            hence contradiction by A6;

          end;

        end;

        ( - r) < ( - 0 qua Nat) by A6;

        then (( - r) * (k + 2)) < ( 0 * (k + 2));

        then (( - (r * (k + 2))) + n) < ( 0 qua Nat + n) by XREAL_1: 6;

        then

         A14: (n -' ((k + 2) * r)) < n by A11, XREAL_0:def 2;

        assume

         A15: P[k];

        then

         A16: (r * (k + 2)) <= ((n / (k + 2)) * (k + 2)) by XREAL_1: 64;

        then

         A17: (r * (k + 2)) <= n by XCMPLX_1: 87;

        then

         A18: (n - (r * (k + 2))) >= ((r * (k + 2)) - (r * (k + 2))) by XREAL_1: 9;

        then

         A19: (n -' ((k + 2) * r)) <> 0 by A11, XREAL_0:def 2;

        (r + (r * (k + 1))) <= n by A16, XCMPLX_1: 87;

        then (r * (k + 1)) < n by A6, Th14;

        then

         A20: (((k + 1) * r) - ((k + 1) * r)) < (n - ((k + 1) * r)) by XREAL_1: 9;

        ((n - ((k + 1) * r)) - r) > 0 by A11, A18;

        then ((n -' ((k + 1) * r)) - r) > 0 by A20, XREAL_0:def 2;



        then

         A21: ((n -' ((k + 1) * r)) -' r) = ((n -' ((k + 1) * r)) - r) by XREAL_0:def 2

        .= ((n - ((k + 1) * r)) - r) by A20, XREAL_0:def 2

        .= (n -' ((k + 2) * r)) by A18, XREAL_0:def 2;

        (n - (r * (k + 1))) >= ((r + (r * (k + 1))) - (r * (k + 1))) by A17, XREAL_1: 9;

        then r <= (n -' (r * (k + 1))) by XREAL_0:def 2;



        then ( Fib (n -' ((k + 1) * r))) = ( Fib ((n -' ((k + 2) * r)) + r)) by A21, XREAL_1: 235

        .= ((( Fib r) * ( Fib ((n -' ((k + 2) * r)) + 1))) + (( Fib (r -' 1)) * ( Fib (n -' ((k + 2) * r))))) by A6, Th40;

        then

         A22: m divides (( Fib (r -' 1)) * ( Fib (n -' ((k + 2) * r)))) by A15, A10, NAT_D: 10;

        then m divides ( Fib (n -' ((k + 2) * r))) by A1, A8, NEWTON: 80;

        then (n -' ((k + 2) * r)) in C by A19, A14;

        then (n -' ((k + 2) * r)) >= r by XXREAL_2:def 7;

        then n >= (r + ((k + 2) * r)) by A17, NAT_D: 54;

        then (n * (1 / ((1 + k) + 2))) >= ((r * ((1 + k) + 2)) * (1 / ((1 + k) + 2))) by XREAL_1: 64;

        then (n * (1 / ((1 + k) + 2))) >= ((r * ((1 + k) + 2)) / ((1 + k) + 2)) by XCMPLX_1: 99;

        then (n / ((1 + k) + 2)) >= ((r * ((1 + k) + 2)) / ((1 + k) + 2)) by XCMPLX_1: 99;

        hence thesis by A1, A8, A22, NEWTON: 80, XCMPLX_1: 89;

      end;

      (r - r) < (n - r) by A6, XREAL_1: 9;

      then

       A23: (n -' r) <> 0 by XREAL_0:def 2;



       A24: m divides (( Fib r) * ( Fib ((n -' r) + 1))) by A6, NAT_D: 9;

      ( Fib n) = ( Fib ((n -' r) + r)) by A6, XREAL_1: 235

      .= ((( Fib r) * ( Fib ((n -' r) + 1))) + (( Fib (r -' 1)) * ( Fib (n -' r)))) by A6, Th40;

      then

       A25: m divides (( Fib (r -' 1)) * ( Fib (n -' r))) by A3, A24, NAT_D: 10;

      then m divides ( Fib (n -' r)) by A1, A8, NEWTON: 80;

      then (n -' r) in C by A7, A23;

      then (n -' r) >= r by XXREAL_2:def 7;

      then n >= (r + r) by A6, NAT_D: 54;

      then (n / 2) >= ((2 * r) / 2) by XREAL_1: 72;

      then

       A26: P[ 0 ] by A1, A8, A25, NEWTON: 80;

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

      then (n / (n + 2)) < 1 & r <= (n / (n + 2)) by XREAL_1: 29, XREAL_1: 191;

      then r < (1 + 0 ) by XXREAL_0: 2;

      hence contradiction by A6, NAT_1: 13;

    end;

    begin

    theorem :: FIB_NUM2:70

    for n be non zero Element of NAT holds {(( Fib n) * ( Fib (n + 3))), ((2 * ( Fib (n + 1))) * ( Fib (n + 2))), ((( Fib (n + 1)) ^2 ) + (( Fib (n + 2)) ^2 ))} is Pythagorean_triple

    proof

      let n be non zero Element of NAT ;

      (((( Fib n) * ( Fib (n + 3))) ^2 ) + (((2 * ( Fib (n + 1))) * ( Fib (n + 2))) ^2 )) = (((( Fib n) ^2 ) * (( Fib (n + 3)) ^2 )) + (((2 * 2) * (( Fib (n + 1)) ^2 )) * (( Fib (n + 2)) ^2 )))

      .= (((( Fib n) ^2 ) * ((( Fib (n + 2)) + ( Fib (n + 1))) ^2 )) + ((4 * (( Fib (n + 1)) ^2 )) * (( Fib (n + 2)) ^2 ))) by Th25

      .= ((((( Fib (n + 2)) - ( Fib (n + 1))) ^2 ) * ((( Fib (n + 2)) + ( Fib (n + 1))) ^2 )) + ((4 * (( Fib (n + 1)) ^2 )) * (( Fib (n + 2)) ^2 ))) by Th30

      .= (((( Fib (n + 1)) ^2 ) + (( Fib (n + 2)) ^2 )) ^2 );

      hence thesis by PYTHTRIP:def 4;

    end;