:: FIB_NUM3 semantic presentation

begin


theorem :: FIB_NUM3:1
for a being real number
for n being Element of NAT st a to_power n = 0 holds
a = 0
proof
let a be real number ; ::_thesis: for n being Element of NAT st a to_power n = 0 holds
a = 0
let n be Element of NAT ; ::_thesis: ( a to_power n = 0 implies a = 0 )
assume  a to_power n = 0 ; ::_thesis: a = 0
then A1: a |^ n = 0 by POWER:41;
assume  a <> 0 ; ::_thesis: contradiction
hence  contradiction by A1, PREPOWER:5; ::_thesis: verum
end;

theorem Th2: :: FIB_NUM3:2
for a being non negative real number holds (sqrt a) * (sqrt a) = a
proof
let a be non negative real number ; ::_thesis: (sqrt a) * (sqrt a) = a
a = sqrt (a ^2) by SQUARE_1:22
.= (sqrt a) * (sqrt a) by SQUARE_1:29 ;
hence  (sqrt a) * (sqrt a) = a ; ::_thesis: verum
end;

theorem Th3: :: FIB_NUM3:3
for a being real number holds a to_power 2 = (- a) to_power 2
proof
let a be real number ; ::_thesis: a to_power 2 = (- a) to_power 2
 2 = 1 * 2 ;
then  2 is even by ABIAN:def_2;
hence  a to_power 2 = (- a) to_power 2 by POWER:47; ::_thesis: verum
end;

theorem Th4: :: FIB_NUM3:4
for k being non empty Nat holds (k -' 1) + 2 = (k + 2) -' 1
proof
let k be non empty Nat; ::_thesis: (k -' 1) + 2 = (k + 2) -' 1
 k >= 1 by NAT_2:19;
hence  (k -' 1) + 2 = (k + 2) -' 1 by NAT_D:38; ::_thesis: verum
end;

theorem Th5: :: FIB_NUM3:5
for a, b being Element of NAT holds (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b)
proof
let a, b be Element of NAT ; ::_thesis: (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b)
(a + b) |^ 2 = (a + b) * (a + b) by WSIERP_1:1
.= (((a * a) + (a * b)) + (b * a)) + (b * b) ;
hence  (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b) ; ::_thesis: verum
end;

theorem Th6: :: FIB_NUM3:6
for n being Element of NAT
for a being non empty real number holds (a to_power n) to_power 2 = a to_power (2 * n)
proof
let n be Element of NAT ; ::_thesis: for a being non empty real number holds (a to_power n) to_power 2 = a to_power (2 * n)
let a be non empty real number ; ::_thesis: (a to_power n) to_power 2 = a to_power (2 * n)
(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  (a to_power n) to_power 2 = a to_power (2 * n) ; ::_thesis: verum
end;

theorem Th7: :: FIB_NUM3:7
for a, b being real number holds (a + b) * (a - b) = (a to_power 2) - (b to_power 2)
proof
let a, b be real number ; ::_thesis: (a + b) * (a - b) = (a to_power 2) - (b to_power 2)
(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  (a + b) * (a - b) = (a to_power 2) - (b to_power 2) ; ::_thesis: verum
end;

theorem Th8: :: FIB_NUM3:8
for n being Element of NAT
for a, b being non empty real number holds (a * b) to_power n = (a to_power n) * (b to_power n)
proof
let n be Element of NAT ; ::_thesis: for a, b being non empty real number holds (a * b) to_power n = (a to_power n) * (b to_power n)
let a, b be non empty real number ; ::_thesis: (a * b) to_power n = (a to_power n) * (b to_power n)
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  (a * b) to_power n = (a to_power n) * (b to_power n) by A1, PREPOWER:40; ::_thesis: verum
end;

registration
cluster tau  ->  positive ;
coherence
 tau is positive by FIB_NUM2:33;
cluster tau_bar  ->  negative ;
coherence
 tau_bar is negative by FIB_NUM2:36;
end;

theorem Th9: :: FIB_NUM3:9
for n being Nat holds (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2)
proof
defpred S1[ Nat] means (tau to_power $1) + (tau to_power ($1 + 1)) = tau to_power ($1 + 2);
let n be Nat; ::_thesis: (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2)
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 being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
 S1[k] and
 S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
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: S1[1] ;
A5: S1[ 0 ] by A1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A3);
hence  (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2) ; ::_thesis: verum
end;

theorem Th10: :: FIB_NUM3:10
for n being Nat holds (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2)
proof
defpred S1[ Nat] means (tau_bar to_power $1) + (tau_bar to_power ($1 + 1)) = tau_bar to_power ($1 + 2);
let n be Nat; ::_thesis: (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2)
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 being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
 S1[k] and
 S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
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: S1[1] ;
A5: S1[ 0 ] by A1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A3);
hence  (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2) ; ::_thesis: verum
end;

begin

definition
let n be Nat;
func Lucas n ->  Element of NAT  means :Def1: :: FIB_NUM3:def 1
 ex L being Function of NAT,[:NAT,NAT:] st
( it = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );
existence
 ex b1 being Element of NAT ex L being Function of NAT,[:NAT,NAT:] st
( b1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of K33(NAT,NAT) = [($2 `2),(($2 `1) + ($2 `2))];
consider L being Function of NAT,[:NAT,NAT:] such that
A1: ( L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = H1(n,L . n) ) ) from NAT_1:sch_12();
take  (L . n) `1 ; ::_thesis: ex L being Function of NAT,[:NAT,NAT:] st
( (L . n) `1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
take  L ; ::_thesis: ( (L . n) `1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
thus  ( (L . n) `1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex L being Function of NAT,[:NAT,NAT:] st
( b1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being Function of NAT,[:NAT,NAT:] st
( b2 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) holds
b1 = b2
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of K33(NAT,NAT) = [($2 `2),(($2 `1) + ($2 `2))];
let it1, it2 be Element of NAT ; ::_thesis: ( ex L being Function of NAT,[:NAT,NAT:] st
( it1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being Function of NAT,[:NAT,NAT:] st
( it2 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) implies it1 = it2 )
given L1 being Function of NAT,[:NAT,NAT:] such that A2: it1 = (L1 . n) `1 and
A3: L1 . 0 = [2,1] and
A4: for n being Nat holds L1 . (n + 1) = H1(n,L1 . n) ; ::_thesis: ( for L being Function of NAT,[:NAT,NAT:] holds
( not it2 = (L . n) `1 or not L . 0 = [2,1] or ex n being Nat st not L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) or it1 = it2 )
given L2 being Function of NAT,[:NAT,NAT:] such that A5: it2 = (L2 . n) `1 and
A6: L2 . 0 = [2,1] and
A7: for n being Nat holds L2 . (n + 1) = H1(n,L2 . n) ; ::_thesis: it1 = it2
 L1 = L2 from NAT_1:sch_16(A3, A4, A6, A7);
hence  it1 = it2 by A2, A5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Lucas FIB_NUM3:def_1_:_
 for n being Nat
for b2 being Element of NAT holds
( b2 = Lucas n iff ex L being Function of NAT,[:NAT,NAT:] st
( b2 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) );

theorem Th11: :: FIB_NUM3:11
( Lucas 0 = 2 & Lucas 1 = 1 & ( for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1)) ) )
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of K33(NAT,NAT) = [($2 `2),(($2 `1) + ($2 `2))];
consider L being Function of NAT,[:NAT,NAT:] such that
A1: L . 0 = [2,1] and
A2: for n being Nat holds L . (n + 1) = H1(n,L . n) from NAT_1:sch_12();
thus  Lucas 0 = [2,1] `1 by A1, A2, Def1
.= 2 by MCART_1:7 ; ::_thesis: ( Lucas 1 = 1 & ( for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1)) ) )
thus  Lucas 1 = (L . (0 + 1)) `1 by A1, A2, Def1
.= [((L . 0) `2),(((L . 0) `1) + ((L . 0) `2))] `1 by A2
.= [2,1] `2 by A1, MCART_1:7
.= 1 by MCART_1:7 ; ::_thesis: for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
let n be Nat; ::_thesis: Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
A3: (L . (n + 1)) `1 = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `1 by A2
.= (L . n) `2 by MCART_1:7 ;
thus  Lucas ((n + 1) + 1) = (L . ((n + 1) + 1)) `1 by A1, A2, Def1
.= [((L . (n + 1)) `2),(((L . (n + 1)) `1) + ((L . (n + 1)) `2))] `1 by A2
.= (L . (n + 1)) `2 by MCART_1:7
.= [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `2 by A2
.= ((L . n) `1) + ((L . (n + 1)) `1) by A3, MCART_1:7
.= (Lucas n) + ((L . (n + 1)) `1) by A1, A2, Def1
.= (Lucas n) + (Lucas (n + 1)) by A1, A2, Def1 ; ::_thesis: verum
end;

theorem Th12: :: FIB_NUM3:12
for n being Nat holds Lucas (n + 2) = (Lucas n) + (Lucas (n + 1))
proof
let n be Nat; ::_thesis: Lucas (n + 2) = (Lucas n) + (Lucas (n + 1))
thus  Lucas (n + 2) = Lucas ((n + 1) + 1)
.= (Lucas n) + (Lucas (n + 1)) by Th11 ; ::_thesis: verum
end;

theorem Th13: :: FIB_NUM3:13
for n being Nat holds (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3)
proof
let n be Nat; ::_thesis: (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3)
(Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (((n + 1) + 1) + 1) by Th11
.= Lucas (n + 3) ;
hence  (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3) ; ::_thesis: verum
end;

theorem Th14: :: FIB_NUM3:14
Lucas 2 = 3
proof
Lucas 2 = Lucas ((0 + 1) + 1)
.= 2 + 1 by Th11
.= 3 ;
hence  Lucas 2 = 3 ; ::_thesis: verum
end;

theorem Th15: :: FIB_NUM3:15
Lucas 3 = 4
proof
Lucas 3 = Lucas ((1 + 1) + 1)
.= 3 + 1 by Th11, Th14
.= 4 ;
hence  Lucas 3 = 4 ; ::_thesis: verum
end;

theorem Th16: :: FIB_NUM3:16
Lucas 4 = 7
proof
Lucas 4 = Lucas (((1 + 1) + 1) + 1)
.= 4 + 3 by Th11, Th14, Th15
.= 7 ;
hence  Lucas 4 = 7 ; ::_thesis: verum
end;

theorem Th17: :: FIB_NUM3:17
for k being Nat holds Lucas k >= k
proof
defpred S1[ Nat] means  Lucas $1 >= $1;
A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: S1[k + 2]
hence  S1[k + 2] by Th14; ::_thesis: verum
end;
suppose k <> 0 ; ::_thesis: S1[k + 2]
then  1 <= k by NAT_1:14;
then A5: 1 + (k + 1) <= k + (k + 1) by XREAL_1:6;
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  S1[k + 2] by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A7: S1[1] by Th11;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A1, A7, A2); ::_thesis: verum
end;

theorem :: FIB_NUM3:18
for m being non empty Element of NAT holds Lucas (m + 1) >= Lucas m
proof
let m be non empty Element of NAT ; ::_thesis: Lucas (m + 1) >= Lucas m
thus  Lucas (m + 1) >= Lucas m ::_thesis: verum
proof
defpred S1[ Nat] means  Lucas ($1 + 1) >= Lucas $1;
A1: for k being non empty Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non empty Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
 S1[k] and
 S1[k + 1] ; ::_thesis: S1[k + 2]
 (Lucas (k + 2)) + (Lucas (k + 1)) = Lucas (k + 3) by Th13;
hence  S1[k + 2] by NAT_1:12; ::_thesis: verum
end;
A2: S1[2] by Th14, Th15;
A3: S1[1] by Th11, Th14;
 for k being non empty Nat holds S1[k] from FIB_NUM2:sch_1(A3, A2, A1);
hence  Lucas (m + 1) >= Lucas m ; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
cluster Lucas n ->  positive ;
coherence
 Lucas n is positive
proof
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: Lucas n is positive
hence  Lucas n is positive by Th11; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: Lucas n is positive
hence  Lucas n is positive by Th17; ::_thesis: verum
end;
end;
end;
end;

theorem :: FIB_NUM3:19
for n being Element of NAT holds 2 * (Lucas (n + 2)) = (Lucas n) + (Lucas (n + 3))
proof
let n be Element of NAT ; ::_thesis: 2 * (Lucas (n + 2)) = (Lucas n) + (Lucas (n + 3))
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 ; ::_thesis: verum
end;

theorem :: FIB_NUM3:20
for n being Nat holds Lucas (n + 1) = (Fib n) + (Fib (n + 2))
proof
defpred S1[ Nat] means  Lucas ($1 + 1) = (Fib $1) + (Fib ($1 + 2));
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A2: ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
 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  S1[k + 2] ; ::_thesis: verum
end;
 (0 + 1) + 1 = 2 ;
then  Fib 2 = 1 by PRE_FF:1;
then A4: S1[1] by Th14, PRE_FF:1;
 (0 + 1) + 1 = 2 ;
then A5: S1[ 0 ] by Th11, PRE_FF:1;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1); ::_thesis: verum
end;

theorem Th21: :: FIB_NUM3:21
for n being Nat holds Lucas n = (tau to_power n) + (tau_bar to_power n)
proof
defpred S1[ 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: S1[ 0 ] by Th11;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
end;
 ( tau_bar to_power 1 = tau_bar & tau to_power 1 = tau ) by POWER:25;
then A5: S1[1] by Th11, FIB_NUM:def_1, FIB_NUM:def_2;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A1, A5, A2);
hence  for n being Nat holds Lucas n = (tau to_power n) + (tau_bar to_power n) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:22
for n being Nat holds (2 * (Lucas n)) + (Lucas (n + 1)) = 5 * (Fib (n + 1))
proof
defpred S1[ Nat] means (2 * (Lucas $1)) + (Lucas ($1 + 1)) = 5 * (Fib ($1 + 1));
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
end;
 (0 + 1) + 1 = 2 ;
then  Fib 2 = 1 by PRE_FF:1;
then A4: S1[1] by Th11, Th14;
A5: S1[ 0 ] by Th11, PRE_FF:1;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1); ::_thesis: verum
end;

theorem Th23: :: FIB_NUM3:23
for n being Nat holds (Lucas (n + 3)) - (2 * (Lucas n)) = 5 * (Fib n)
proof
defpred S1[ Nat] means (Lucas ($1 + 3)) - (2 * (Lucas $1)) = 5 * (Fib $1);
A1: S1[1] by Th11, Th16, PRE_FF:1;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
end;
A5: S1[ 0 ] by Th11, Th15, PRE_FF:1;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A1, A2); ::_thesis: verum
end;

theorem :: FIB_NUM3:24
for n being Nat holds (Lucas n) + (Fib n) = 2 * (Fib (n + 1))
proof
defpred S1[ Nat] means (Lucas $1) + (Fib $1) = 2 * (Fib ($1 + 1));
let n be Nat; ::_thesis: (Lucas n) + (Fib n) = 2 * (Fib (n + 1))
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
(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))) + ((Lucas (k + 1)) + (Fib (k + 1))) by A2
.= (2 * (Fib (k + 1))) + (2 * (Fib ((k + 1) + 1))) by A3
.= 2 * ((Fib (k + 1)) + (Fib (k + 2)))
.= 2 * (Fib (k + 3)) by FIB_NUM2:25
.= 2 * (Fib ((k + 2) + 1)) ;
hence  S1[k + 2] ; ::_thesis: verum
end;
 (0 + 1) + 1 = 2 ;
then  Fib 2 = 1 by PRE_FF:1;
then A4: S1[1] by Th11, PRE_FF:1;
A5: S1[ 0 ] by Th11, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1);
hence  (Lucas n) + (Fib n) = 2 * (Fib (n + 1)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:25
for n being Nat holds (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))
proof
defpred S1[ Nat] means (3 * (Fib $1)) + (Lucas $1) = 2 * (Fib ($1 + 2));
let n be Nat; ::_thesis: (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))
 (0 + 1) + 1 = 2 ;
then A1: Fib 2 = 1 by PRE_FF:1;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A3: ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
(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
.= ((3 * (Fib k)) + (Lucas k)) + ((3 * (Fib (k + 1))) + (Lucas (k + 1)))
.= (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  S1[k + 2] ; ::_thesis: verum
end;
 ((0 + 1) + 1) + 1 = 3 ;
then  Fib 3 = 2 by A1, PRE_FF:1;
then A4: S1[1] by Th11, PRE_FF:1;
A5: S1[ 0 ] by A1, Th11, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A2);
hence  (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:26
for n, m being Element of NAT holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m))
proof
defpred S1[ Nat] means  for n being Element of NAT holds 2 * (Lucas (n + $1)) = ((Lucas n) * (Lucas $1)) + ((5 * (Fib n)) * (Fib $1));
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_&_S1[k_+_1]_holds_
S1[k_+_2]
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
thus  S1[k + 2] ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: 2 * (Lucas (n + (k + 2))) = ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2)))
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  2 * (Lucas (n + (k + 2))) = ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) ; ::_thesis: verum
end;
end;
A5: S1[1]
proof
let n be Element of NAT ; ::_thesis: 2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1))
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  2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1)) ; ::_thesis: verum
end;
A6: S1[ 0 ] by Th11, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A6, A5, A1);
hence  for n, m being Element of NAT holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:27
for n being Element of NAT holds (Lucas (n + 3)) * (Lucas n) = ((Lucas (n + 2)) |^ 2) - ((Lucas (n + 1)) |^ 2)
proof
defpred S1[ Nat] means (Lucas ($1 + 3)) * (Lucas $1) = ((Lucas ($1 + 2)) |^ 2) - ((Lucas ($1 + 1)) |^ 2);
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
 S1[k] and
 S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
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: S1[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: S1[ 0 ] ;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A3, A2, A1);
hence  for n being Element of NAT holds (Lucas (n + 3)) * (Lucas n) = ((Lucas (n + 2)) |^ 2) - ((Lucas (n + 1)) |^ 2) ; ::_thesis: verum
end;

theorem Th28: :: FIB_NUM3:28
for n being Nat holds Fib (2 * n) = (Fib n) * (Lucas n)
proof
let n be Nat; ::_thesis: Fib (2 * n) = (Fib n) * (Lucas n)
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  Fib (2 * n) = (Fib n) * (Lucas n) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:29
for n being Element of NAT holds 2 * (Fib ((2 * n) + 1)) = ((Lucas (n + 1)) * (Fib n)) + ((Lucas n) * (Fib (n + 1)))
proof
defpred S1[ 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 being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
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))))
.= (((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - (2 * (((Lucas (k + 1)) * (Fib k)) + ((Lucas k) * (Fib (k + 1))))) by A3, A4
.= ((((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1)))
.= (((((Lucas k) + (Lucas (k + 1))) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1))) by Th12
.= (((((Lucas k) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 1)))) + ((Lucas (k + 1)) * ((Fib k) + (Fib (k + 1))))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1))) by FIB_NUM2:24
.= (((2 * (Lucas (k + 1))) * (Fib (k + 1))) - ((Lucas k) * (Fib (k + 1)))) - ((Lucas (k + 1)) * (Fib k)) ;
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 * (Lucas (k + 2))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * (Fib (k + 2)))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by A3
.= ((((3 * ((Lucas k) + (Lucas (k + 1)))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * (Fib (k + 2)))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by Th12
.= (((((3 * (Lucas k)) + (3 * (Lucas (k + 1)))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * ((Fib k) + (Fib (k + 1))))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by FIB_NUM2:24
.= ((((3 * (Lucas k)) * (Fib (k + 1))) + ((4 * (Lucas (k + 1))) * (Fib (k + 1)))) + ((3 * (Lucas (k + 1))) * (Fib k))) + ((((2 * (Lucas (k + 1))) * (Fib (k + 1))) - ((Lucas k) * (Fib (k + 1)))) - ((Lucas (k + 1)) * (Fib k)))
.= ((((3 * (Lucas k)) * (Fib (k + 1))) + ((4 * (Lucas (k + 1))) * (Fib (k + 1)))) + ((3 * (Lucas (k + 1))) * (Fib k))) + (2 * ((Lucas k) * (Fib k))) by A5, Th28
.= (((((((Lucas k) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 1)))) + ((Lucas (k + 1)) * ((Fib k) + (Fib (k + 1))))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1)))
.= (((((((Lucas k) + (Lucas (k + 1))) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1))) by FIB_NUM2:24
.= ((((((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1))) by Th12
.= (((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + (2 * (((((Lucas k) * (Fib k)) + ((Lucas k) * (Fib (k + 1)))) + ((Lucas (k + 1)) * (Fib k))) + ((Lucas (k + 1)) * (Fib (k + 1)))))
.= (2 * (Fib ((2 * k) + 3))) + (2 * (((((Lucas k) * (Fib k)) + ((Lucas k) * (Fib (k + 1)))) + ((Lucas (k + 1)) * (Fib k))) + ((Lucas (k + 1)) * (Fib (k + 1))))) 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  S1[k + 2] ; ::_thesis: verum
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: S1[1] ;
A7: S1[ 0 ] by Th11, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A7, A6, A2);
hence  for n being Element of NAT holds 2 * (Fib ((2 * n) + 1)) = ((Lucas (n + 1)) * (Fib n)) + ((Lucas n) * (Fib (n + 1))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:30
for n being Element of NAT holds (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))
proof
let n be Element of NAT ; ::_thesis: (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))
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
.= (((tau to_power n) - (tau_bar to_power n)) * ((tau to_power n) - (tau_bar to_power n))) / ((sqrt 5) * (sqrt 5)) by XCMPLX_1:76
.= ((((tau to_power n) * (tau to_power n)) - ((2 * (tau to_power n)) * (tau_bar to_power n))) + ((tau_bar to_power n) * (tau_bar to_power n))) / 5 by Th2 ;
A2: (tau to_power n) * (tau_bar to_power n) = (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
.= (((tau to_power n) * (tau to_power n)) + ((2 * (tau to_power n)) * (tau_bar to_power n))) + ((tau_bar to_power n) * (tau_bar to_power n)) ;
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  (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:31
for n being 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 ; ::_thesis: Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n))
((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  Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n)) ; ::_thesis: verum
end;

begin

definition
let a, b be Nat;
:: original: [
redefine func[a,b] ->  Element of [:NAT,NAT:];
coherence
 [a,b] is Element of [:NAT,NAT:]
proof
reconsider a = a, b = b as Element of NAT by ORDINAL1:def_12;
 [a,b] is Element of [:NAT,NAT:] ;
hence  [a,b] is Element of [:NAT,NAT:] ; ::_thesis: verum
end;
end;

definition
let a, b, n be Nat;
func GenFib (a,b,n) ->  Element of NAT  means :Def2: :: FIB_NUM3:def 2
 ex L being Function of NAT,[:NAT,NAT:] st
( it = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) );
existence
 ex b1 being Element of NAT ex L being Function of NAT,[:NAT,NAT:] st
( b1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
consider L being Function of NAT,[:NAT,NAT:] such that
A1: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = H1(n,L . n) ) ) from NAT_1:sch_12();
take  (L . n) `1 ; ::_thesis: ex L being Function of NAT,[:NAT,NAT:] st
( (L . n) `1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
take  L ; ::_thesis: ( (L . n) `1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )
thus  ( (L . n) `1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex L being Function of NAT,[:NAT,NAT:] st
( b1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being Function of NAT,[:NAT,NAT:] st
( b2 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) holds
b1 = b2
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
let it1, it2 be Element of NAT ; ::_thesis: ( ex L being Function of NAT,[:NAT,NAT:] st
( it1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being Function of NAT,[:NAT,NAT:] st
( it2 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) implies it1 = it2 )
given L1 being Function of NAT,[:NAT,NAT:] such that A2: it1 = (L1 . n) `1 and
A3: L1 . 0 = [a,b] and
A4: for n being Nat holds L1 . (n + 1) = H1(n,L1 . n) ; ::_thesis: ( for L being Function of NAT,[:NAT,NAT:] holds
( not it2 = (L . n) `1 or not L . 0 = [a,b] or ex n being Nat st not L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) or it1 = it2 )
given L2 being Function of NAT,[:NAT,NAT:] such that A5: it2 = (L2 . n) `1 and
A6: L2 . 0 = [a,b] and
A7: for n being Nat holds L2 . (n + 1) = H1(n,L2 . n) ; ::_thesis: it1 = it2
 L1 = L2 from NAT_1:sch_16(A3, A4, A6, A7);
hence  it1 = it2 by A2, A5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines GenFib FIB_NUM3:def_2_:_
 for a, b, n being Nat
for b4 being Element of NAT holds
( b4 = GenFib (a,b,n) iff ex L being Function of NAT,[:NAT,NAT:] st
( b4 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) );

theorem Th32: :: FIB_NUM3:32
for a, b being Nat holds
( GenFib (a,b,0) = a & GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
let a, b be Nat; ::_thesis: ( GenFib (a,b,0) = a & GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )
consider L being Function of NAT,[:NAT,NAT:] such that
A1: L . 0 = [a,b] and
A2: for n being Nat holds L . (n + 1) = H1(n,L . n) from NAT_1:sch_12();
thus  GenFib (a,b,0) = [a,b] `1 by A1, A2, Def2
.= a by MCART_1:7 ; ::_thesis: ( GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )
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
.= [a,b] `2 by A1, MCART_1:7
.= b by MCART_1:7 ; ::_thesis: for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))
let n be Nat; ::_thesis: GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))
A3: (L . (n + 1)) `1 = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `1 by A2
.= (L . n) `2 by MCART_1:7 ;
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 + 1)) `2 by MCART_1:7
.= [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `2 by A2
.= ((L . n) `1) + ((L . (n + 1)) `1) by A3, MCART_1:7
.= (GenFib (a,b,n)) + ((L . (n + 1)) `1) by A1, A2, Def2
.= (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) by A1, A2, Def2 ;
hence  GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ; ::_thesis: verum
end;

theorem Th33: :: FIB_NUM3:33
for a, b being Element of NAT
for k being 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 a, b be Element of NAT ; ::_thesis: for k being 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)
let k be Nat; ::_thesis: ((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)
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 = ((((GenFib (a,b,(k + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 1))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,(k + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1)))) by Th5
.= (((GenFib (a,b,(k + 1))) * (GenFib (a,b,(k + 1)))) + (2 * ((GenFib (a,b,(k + 1))) * (GenFib (a,b,((k + 1) + 1)))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1))))
.= (((GenFib (a,b,(k + 1))) |^ 2) + ((2 * (GenFib (a,b,(k + 1)))) * (GenFib (a,b,((k + 1) + 1))))) + ((GenFib (a,b,((k + 1) + 1))) * (GenFib (a,b,((k + 1) + 1)))) by WSIERP_1:1
.= (((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 WSIERP_1:1 ;
hence  ((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) ; ::_thesis: verum
end;

theorem Th34: :: FIB_NUM3:34
for a, b, n being Nat holds (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2))
proof
let a, b, n be Nat; ::_thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2))
(GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,((n + 1) + 1)) by Th32
.= GenFib (a,b,(n + 2)) ;
hence  (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2)) ; ::_thesis: verum
end;

theorem Th35: :: FIB_NUM3:35
for a, b, n being Nat holds (GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2))) = GenFib (a,b,(n + 3))
proof
let a, b, n be Nat; ::_thesis: (GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2))) = GenFib (a,b,(n + 3))
(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  (GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2))) = GenFib (a,b,(n + 3)) ; ::_thesis: verum
end;

theorem Th36: :: FIB_NUM3:36
for a, b, n being 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 ; ::_thesis: (GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 3))) = GenFib (a,b,(n + 4))
(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  (GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 3))) = GenFib (a,b,(n + 4)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:37
for n being Element of NAT holds GenFib (0,1,n) = Fib n
proof
defpred S1[ Nat] means  GenFib (0,1,$1) = Fib $1;
A1: S1[1] by Th32, PRE_FF:1;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume  ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
then  GenFib (0,1,(k + 2)) = (Fib k) + (Fib (k + 1)) by Th34
.= Fib (k + 2) by FIB_NUM2:24 ;
hence  S1[k + 2] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th32, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A3, A1, A2);
hence  for n being Element of NAT holds GenFib (0,1,n) = Fib n ; ::_thesis: verum
end;

theorem Th38: :: FIB_NUM3:38
for n being Element of NAT holds GenFib (2,1,n) = Lucas n
proof
defpred S1[ Nat] means  GenFib (2,1,$1) = Lucas $1;
A1: S1[1] by Th11, Th32;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume  ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
then  GenFib (2,1,(k + 2)) = (Lucas k) + (Lucas (k + 1)) by Th34
.= Lucas (k + 2) by Th12 ;
hence  S1[k + 2] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th11, Th32;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A3, A1, A2);
hence  for n being Element of NAT holds GenFib (2,1,n) = Lucas n ; ::_thesis: verum
end;

theorem Th39: :: FIB_NUM3:39
for a, b, n being 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 ; ::_thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2)))
(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  (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:40
for a, b, n being 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 ; ::_thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = 3 * (GenFib (a,b,(n + 2)))
(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  (GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = 3 * (GenFib (a,b,(n + 2))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:41
for a, b, n being 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 ; ::_thesis: (GenFib (a,b,(n + 3))) - (GenFib (a,b,n)) = 2 * (GenFib (a,b,(n + 1)))
(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  (GenFib (a,b,(n + 3))) - (GenFib (a,b,n)) = 2 * (GenFib (a,b,(n + 1))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:42
for a, b, n being non empty 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 empty Element of NAT ; ::_thesis: GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))
thus  GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) ::_thesis: verum
proof
defpred S1[ 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: S1[1] ;
A2: for k being non empty Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non empty Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
 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  S1[k + 2] ; ::_thesis: verum
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: S1[2] ;
 for k being non empty Nat holds S1[k] from FIB_NUM2:sch_1(A1, A7, A2);
hence  GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) ; ::_thesis: verum
end;
end;

theorem :: FIB_NUM3:43
for n, m being Nat holds ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib ((Fib 0),(Lucas 0),(n + m))
proof
let n, m be Nat; ::_thesis: ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib ((Fib 0),(Lucas 0),(n + m))
defpred S1[ 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 S2[ Nat] means 2 * (Fib $1) = GenFib (0,2,$1);
A1: S2[1] by Th32, PRE_FF:1;
A2: for i being Nat st S2[i] & S2[i + 1] holds
S2[i + 2]
proof
let i be Nat; ::_thesis: ( S2[i] & S2[i + 1] implies S2[i + 2] )
assume A3: ( S2[i] & S2[i + 1] ) ; ::_thesis: S2[i + 2]
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  S2[i + 2] ; ::_thesis: verum
end;
A4: S2[ 0 ] by Th32, PRE_FF:1;
 for i being Nat holds S2[i] from FIB_NUM:sch_1(A4, A1, A2);
hence  2 * (Fib n) = GenFib (0,2,n) ; ::_thesis: verum
end;
then A5: S1[ 0 ] by Th11, PRE_FF:1;
 (Lucas n) + (Fib n) = GenFib (0,2,(n + 1))
proof
defpred S2[ Nat] means (Lucas $1) + (Fib $1) = GenFib (0,2,($1 + 1));
A6: for j being Nat st S2[j] & S2[j + 1] holds
S2[j + 2]
proof
let j be Nat; ::_thesis: ( S2[j] & S2[j + 1] implies S2[j + 2] )
assume A7: ( S2[j] & S2[j + 1] ) ; ::_thesis: S2[j + 2]
(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  S2[j + 2] ; ::_thesis: verum
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: S2[1] ;
A9: S2[ 0 ] by Th11, Th32, PRE_FF:1;
 for j being Nat holds S2[j] from FIB_NUM:sch_1(A9, A8, A6);
hence  (Lucas n) + (Fib n) = GenFib (0,2,(n + 1)) ; ::_thesis: verum
end;
then A10: S1[1] by Th11, PRE_FF:1;
A11: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A12: ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
((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  S1[k + 2] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A10, A11);
hence  ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib ((Fib 0),(Lucas 0),(n + m)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:44
for n being Element of NAT holds (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))
proof
let n be Element of NAT ; ::_thesis: (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))
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  (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2)) by A1, Th39; ::_thesis: verum
end;

theorem :: FIB_NUM3:45
for a, n being 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 ; ::_thesis: GenFib (a,a,b) = ((GenFib (a,a,0)) / 2) * ((Fib b) + (Lucas b))
defpred S1[ Nat] means  GenFib (a,a,$1) = ((GenFib (a,a,0)) / 2) * ((Fib $1) + (Lucas $1));
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
end;
 GenFib (a,a,1) = a by Th32;
then A4: S1[1] by Th11, Th32, PRE_FF:1;
A5: S1[ 0 ] by Th11, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1);
hence  GenFib (a,a,b) = ((GenFib (a,a,0)) / 2) * ((Fib b) + (Lucas b)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:46
for a, b, n being Element of NAT holds GenFib (b,(a + b),n) = GenFib (a,b,(n + 1))
proof
let a, b, n be Element of NAT ; ::_thesis: GenFib (b,(a + b),n) = GenFib (a,b,(n + 1))
defpred S1[ Nat] means  GenFib (b,(a + b),$1) = GenFib (a,b,($1 + 1));
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume  ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
end;
GenFib (b,(a + b),0) = b by Th32
.= GenFib (a,b,(0 + 1)) by Th32 ;
then A2: S1[ 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: S1[1] ;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A2, A3, A1);
hence  GenFib (b,(a + b),n) = GenFib (a,b,(n + 1)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:47
for a, b, n being 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 ; ::_thesis: ((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))))
defpred S1[ 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: S1[1] ;
A4: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A5: S1[k] and
A6: S1[k + 1] ; ::_thesis: S1[k + 2]
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  ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((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))) + (((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((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: ((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) - ((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: (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((GenFib (a,b,(k + 1))) + (GenFib (a,b,((k + 1) + 1)))) |^ 2) = (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((((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))))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((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))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - ((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))) + ((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1))))) + ((GenFib (a,b,(k + 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)))) |^ 2) by Th32
.= (((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,k))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,(k + 1))))) + ((((GenFib (a,b,((k + 2) + 1))) * (GenFib (a,b,(k + 1)))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((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))) + ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k)))) - (((GenFib (a,b,k)) + (GenFib (a,b,(k + 1)))) * (GenFib (a,b,(k + 1)))) by Th34
.= ((GenFib (a,b,(k + 2))) * (GenFib (a,b,k))) - ((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  S1[k + 2] ; ::_thesis: verum
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: S1[ 0 ] ;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A12, A3, A4);
hence  ((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)))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:48
for a, b, k, n being 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 ; ::_thesis: GenFib ((GenFib (a,b,k)),(GenFib (a,b,(k + 1))),n) = GenFib (a,b,(n + k))
defpred S1[ Nat] means  GenFib ((GenFib (a,b,k)),(GenFib (a,b,(k + 1))),$1) = GenFib (a,b,($1 + k));
A1: S1[1] by Th32;
A2: for i being Nat st S1[i] & S1[i + 1] holds
S1[i + 2]
proof
let i be Nat; ::_thesis: ( S1[i] & S1[i + 1] implies S1[i + 2] )
assume  ( S1[i] & S1[i + 1] ) ; ::_thesis: S1[i + 2]
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  S1[i + 2] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th32;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A3, A1, A2);
hence  GenFib ((GenFib (a,b,k)),(GenFib (a,b,(k + 1))),n) = GenFib (a,b,(n + k)) ; ::_thesis: verum
end;

theorem Th49: :: FIB_NUM3:49
for a, b, n being 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 ; ::_thesis: GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1)))
defpred S1[ 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: S1[1] by A1, PRE_FF:1;
A3: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A4: S1[k] and
A5: S1[k + 1] ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
end;
A6: S1[ 0 ] by Th32, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A6, A2, A3);
hence  GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1))) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:50
for b, n being Element of NAT holds GenFib (0,b,n) = b * (Fib n)
proof
let b, n be Element of NAT ; ::_thesis: GenFib (0,b,n) = b * (Fib n)
defpred S1[ Nat] means  GenFib (0,b,$1) = b * (Fib $1);
A1: S1[1] by Th32, PRE_FF:1;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
end;
A5: S1[ 0 ] by Th32, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A1, A2);
hence  GenFib (0,b,n) = b * (Fib n) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:51
for a, n being Element of NAT holds GenFib (a,0,(n + 1)) = a * (Fib n)
proof
let a, n be Element of NAT ; ::_thesis: GenFib (a,0,(n + 1)) = a * (Fib n)
defpred S1[ Nat] means  GenFib (a,0,($1 + 1)) = a * (Fib $1);
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
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  S1[k + 2] ; ::_thesis: verum
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: S1[1] by PRE_FF:1;
A5: S1[ 0 ] by Th32, PRE_FF:1;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1);
hence  GenFib (a,0,(n + 1)) = a * (Fib n) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:52
for a, b, c, d, n being 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 ; ::_thesis: (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n)
defpred S1[ Nat] means (GenFib (a,b,$1)) + (GenFib (c,d,$1)) = GenFib ((a + c),(b + d),$1);
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; ::_thesis: S1[k + 2]
(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  S1[k + 2] ; ::_thesis: verum
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: S1[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: S1[ 0 ] ;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A5, A4, A1);
hence  (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:53
for a, b, k, n being 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 ; ::_thesis: GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n))
defpred S1[ Nat] means  GenFib ((k * a),(k * b),$1) = k * (GenFib (a,b,$1));
A1: for i being Nat st S1[i] & S1[i + 1] holds
S1[i + 2]
proof
let i be Nat; ::_thesis: ( S1[i] & S1[i + 1] implies S1[i + 2] )
assume that
A2: S1[i] and
A3: S1[i + 1] ; ::_thesis: S1[i + 2]
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  S1[i + 2] ; ::_thesis: verum
end;
GenFib ((k * a),(k * b),1) = k * b by Th32
.= k * (GenFib (a,b,1)) by Th32 ;
then A4: S1[1] ;
GenFib ((k * a),(k * b),0) = k * a by Th32
.= k * (GenFib (a,b,0)) by Th32 ;
then A5: S1[ 0 ] ;
 for i being Nat holds S1[i] from FIB_NUM:sch_1(A5, A4, A1);
hence  GenFib ((k * a),(k * b),n) = k * (GenFib (a,b,n)) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:54
for a, b, n being 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 ; ::_thesis: GenFib (a,b,n) = ((((a * (- tau_bar)) + b) * (tau to_power n)) + (((a * tau) - b) * (tau_bar to_power n))) / (sqrt 5)
defpred S1[ 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: S1[1] ;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
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
.= (tau to_power k) * tau by POWER:25 ;
set g = (((a * (- tau_bar)) + b) * (tau to_power k)) + (((a * tau) - b) * (tau_bar to_power k));
A4: tau_bar to_power (k + 1) = (tau_bar to_power k) * (tau_bar to_power 1) by FIB_NUM2:5
.= (tau_bar to_power k) * 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) * (tau to_power k)) * tau) + ((((a * tau) - b) * (tau_bar to_power k)) * tau_bar);
A7: ( tau to_power (k + 2) = (tau to_power k) * (tau to_power 2) & tau_bar to_power (k + 2) = (tau_bar to_power k) * (tau_bar to_power 2) ) by FIB_NUM2:5;
assume  ( S1[k] & S1[k + 1] ) ; ::_thesis: S1[k + 2]
then  GenFib (a,b,(k + 2)) = (((((a * (- tau_bar)) + b) * (tau to_power k)) + (((a * tau) - b) * (tau_bar to_power k))) / (sqrt 5)) + ((((((a * (- tau_bar)) + b) * (tau to_power k)) * tau) + ((((a * tau) - b) * (tau_bar to_power k)) * tau_bar)) / (sqrt 5)) by A3, A4, Th34
.= (((((a * (- tau_bar)) + b) * (tau to_power k)) + (((a * tau) - b) * (tau_bar to_power k))) + (((((a * (- tau_bar)) + b) * (tau to_power k)) * tau) + ((((a * tau) - b) * (tau_bar to_power k)) * tau_bar))) / (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  S1[k + 2] ; ::_thesis: verum
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: S1[ 0 ] ;
 for k being Nat holds S1[k] from FIB_NUM:sch_1(A8, A1, A2);
hence  GenFib (a,b,n) = ((((a * (- tau_bar)) + b) * (tau to_power n)) + (((a * tau) - b) * (tau_bar to_power n))) / (sqrt 5) ; ::_thesis: verum
end;

theorem :: FIB_NUM3:55
for a, n being 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 ; ::_thesis: GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2))
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  GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2)) ; ::_thesis: verum
end;