:: 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;