:: FIB_NUM semantic presentation

begin


theorem Th1: :: FIB_NUM:1
for m, n being Element of NAT holds m gcd n = m gcd (n + m)
proof
let m, n be Element of NAT ; ::_thesis: m gcd n = m gcd (n + m)
set a = m gcd n;
set b = m gcd (n + m);
A1: m gcd n divides m by NAT_D:def_5;
A2: m gcd (n + m) divides m by NAT_D:def_5;
 m gcd (n + m) divides n + m by NAT_D:def_5;
then  m gcd (n + m) divides n by A2, NAT_D:10;
then A3: m gcd (n + m) divides m gcd n by A2, NAT_D:def_5;
 m gcd n divides n by NAT_D:def_5;
then  m gcd n divides n + m by A1, NAT_D:8;
then  m gcd n divides m gcd (n + m) by A1, NAT_D:def_5;
hence  m gcd n = m gcd (n + m) by A3, NAT_D:5; ::_thesis: verum
end;

theorem Th2: :: FIB_NUM:2
for k, m, n being Element of NAT st k gcd m = 1 holds
k gcd (m * n) = k gcd n
proof
defpred S1[ Nat] means  for m, n being Element of NAT st $1 gcd m = 1 holds
$1 gcd (m * n) = $1 gcd n;
A1: for k being Nat st ( for a being Nat st a < k holds
S1[a] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for a being Nat st a < k holds
S1[a] ) implies S1[k] )
assume A2: for a being Nat st a < k holds
S1[a] ; ::_thesis: S1[k]
percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
supposeA3: k = 0 ; ::_thesis: S1[k]
let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )
assume  k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n
then  1 = m by A3, NEWTON:52;
hence  k gcd (m * n) = k gcd n ; ::_thesis: verum
end;
supposeA4: k = 1 ; ::_thesis: S1[k]
let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )
assume  k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n
 k gcd (m * n) = 1 by A4, NEWTON:51;
hence  k gcd (m * n) = k gcd n by A4, NEWTON:51; ::_thesis: verum
end;
supposeA5: k > 1 ; ::_thesis: S1[k]
let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n )
set b = k gcd (m * n);
assume A6: k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n
thus  k gcd (m * n) = k gcd n ::_thesis: verum
proof
percases ( k gcd (m * n) = 0 or k gcd (m * n) = 1 or k gcd (m * n) > 1 ) by NAT_1:25;
suppose k gcd (m * n) = 0 ; ::_thesis: k gcd (m * n) = k gcd n
then  0 divides k by NAT_D:def_5;
then  k = 0 by INT_2:3;
hence  k gcd (m * n) = k gcd n by A5; ::_thesis: verum
end;
supposeA7: k gcd (m * n) = 1 ; ::_thesis: k gcd (m * n) = k gcd n
set c = k gcd n;
A8: k gcd n divides k by NAT_D:def_5;
A9: n divides m * n by NAT_D:def_3;
 k gcd n divides n by NAT_D:def_5;
then  k gcd n divides m * n by A9, NAT_D:4;
then  k gcd n divides 1 by A7, A8, NAT_D:def_5;
hence  k gcd (m * n) = k gcd n by A7, WSIERP_1:15; ::_thesis: verum
end;
suppose k gcd (m * n) > 1 ; ::_thesis: k gcd (m * n) = k gcd n
then  k gcd (m * n) >= 1 + 1 by NAT_1:13;
then consider p being Element of NAT  such that
A10: p is prime and
A11: p divides k gcd (m * n) by INT_2:31;
 k gcd (m * n) divides k by NAT_D:def_5;
then A12: p divides k by A11, NAT_D:4;
then consider s being Nat such that
A13: k = p * s by NAT_D:def_3;
A14: not p divides m
proof
assume  p divides m ; ::_thesis: contradiction
then  p divides 1 by A6, A12, NAT_D:def_5;
then  p = 1 by WSIERP_1:15;
hence  contradiction by A10, INT_2:def_4; ::_thesis: verum
end;
 k gcd (m * n) divides m * n by NAT_D:def_5;
then  p divides m * n by A11, NAT_D:4;
then  p divides n by A10, A14, NEWTON:80;
then consider r being Nat such that
A15: n = p * r by NAT_D:def_3;
reconsider s = s as Element of NAT by ORDINAL1:def_12;
A16: s + 1 > s by XREAL_1:29;
 p > 1 by A10, INT_2:def_4;
then  p >= 1 + 1 by NAT_1:13;
then A17: s * p >= s * (1 + 1) by NAT_1:4;
 s <> 0 by A5, A13;
then  s + s > s by NAT_1:3, XREAL_1:29;
then  s + s >= s + 1 by NAT_1:13;
then  k >= s + 1 by A13, A17, XXREAL_0:2;
then A18: s < k by A16, XXREAL_0:2;
A19: s gcd m = 1
proof
set c = s gcd m;
A20: s gcd m divides s by NAT_D:def_5;
A21: s gcd m divides m by NAT_D:def_5;
 s divides k by A13, NAT_D:def_3;
then  s gcd m divides k by A20, NAT_D:4;
then  s gcd m divides 1 by A6, A21, NAT_D:def_5;
hence  s gcd m = 1 by WSIERP_1:15; ::_thesis: verum
end;
reconsider r = r as Element of NAT by ORDINAL1:def_12;
A22: k gcd n = p * (s gcd r) by A13, A15, PYTHTRIP:8;
k gcd (m * n) = (p * s) gcd (p * (m * r)) by A13, A15
.= p * (s gcd (m * r)) by PYTHTRIP:8 ;
hence  k gcd (m * n) = k gcd n by A2, A18, A19, A22; ::_thesis: verum
end;
end;
end;
end;
end;
end;
 for k being Nat holds S1[k] from NAT_1:sch_4(A1);
hence  for k, m, n being Element of NAT st k gcd m = 1 holds
k gcd (m * n) = k gcd n ; ::_thesis: verum
end;

theorem Th3: :: FIB_NUM:3
for s being real number st s > 0 holds
ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s )
proof
let s be real number ; ::_thesis: ( s > 0 implies ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s ) )
consider n being Element of NAT  such that
A1: n > 1 / s by SEQ_4:3;
A2: 1 / (1 / s) = 1 / (s ")
.= s ;
assume  s > 0 ; ::_thesis: ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s )
then A3: 1 / s > 0 by XREAL_1:139;
take  n ; ::_thesis: ( n > 0 & 0 < 1 / n & 1 / n <= s )
 n > 0 by A3, A1, XXREAL_0:2;
hence  ( n > 0 & 0 < 1 / n & 1 / n <= s ) by A3, A1, A2, XREAL_1:85, XREAL_1:139; ::_thesis: verum
end;

scheme :: FIB_NUM:sch 1
FibInd{ P1[ set ] } :
 for k being Nat holds P1[k]
provided
A1: P1[ 0 ] and
A2: P1[1] and
A3: for k being Nat st P1[k] & P1[k + 1] holds
P1[k + 2]
proof
let k be Nat; ::_thesis: P1[k]
defpred S1[ Nat] means ( P1[$1] & P1[$1 + 1] );
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A5: k + 2 = (k + 1) + 1 ;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A3, A5; ::_thesis: verum
end;
A6: S1[ 0 ] by A1, A2;
 for k being Nat holds S1[k] from NAT_1:sch_2(A6, A4);
hence  P1[k] ; ::_thesis: verum
end;

scheme :: FIB_NUM:sch 2
BinInd{ P1[ Nat, Nat] } :
 for m, n being Element of NAT holds P1[m,n]
provided
A1: for m, n being Element of NAT st P1[m,n] holds
P1[n,m] and
A2: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds
P1[m,n] ) holds
for m being Element of NAT st m <= k holds
P1[k,m]
proof
defpred S1[ Nat] means  for m, n being Element of NAT st m <= $1 & n <= $1 holds
P1[m,n];
A3: for k being Nat st ( for r being Nat st r < k holds
S1[r] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for r being Nat st r < k holds
S1[r] ) implies S1[k] )
assume A4: for r being Nat st r < k holds
S1[r] ; ::_thesis: S1[k]
let m, n be Element of NAT ; ::_thesis: ( m <= k & n <= k implies P1[m,n] )
assume that
A5: m <= k and
A6: n <= k ; ::_thesis: P1[m,n]
set s = max (m,n);
A7: max (m,n) <= k by A5, A6, XXREAL_0:28;
percases ( max (m,n) < k or max (m,n) = k ) by A7, XXREAL_0:1;
suppose max (m,n) < k ; ::_thesis: P1[m,n]
then  ( m <= max (m,n) & n <= max (m,n) implies P1[m,n] ) by A4;
hence  P1[m,n] by XXREAL_0:25; ::_thesis: verum
end;
supposeA8: max (m,n) = k ; ::_thesis: P1[m,n]
A9: for m, n being Element of NAT st m < k & n < k holds
P1[m,n]
proof
let m, n be Element of NAT ; ::_thesis: ( m < k & n < k implies P1[m,n] )
assume that
A10: m < k and
A11: n < k ; ::_thesis: P1[m,n]
set s = max (m,n);
A12: m <= max (m,n) by XXREAL_0:25;
A13: n <= max (m,n) by XXREAL_0:25;
 max (m,n) < k by A10, A11, XXREAL_0:16;
hence  P1[m,n] by A4, A12, A13; ::_thesis: verum
end;
thus  P1[m,n] ::_thesis: verum
proof
percases ( k = m or k = n ) by A8, XXREAL_0:16;
suppose k = m ; ::_thesis: P1[m,n]
hence  P1[m,n] by A2, A6, A9; ::_thesis: verum
end;
suppose k = n ; ::_thesis: P1[m,n]
then  P1[n,m] by A2, A5, A9;
hence  P1[m,n] by A1; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A14: for k being Nat holds S1[k] from NAT_1:sch_4(A3);
let m, n be Element of NAT ; ::_thesis: P1[m,n]
set k = max (m,n);
 ( m <= max (m,n) & n <= max (m,n) implies P1[m,n] ) by A14;
hence  P1[m,n] by XXREAL_0:30; ::_thesis: verum
end;

 (0 + 1) + 1 = 2
;

then Lm1:  Fib 2 = 1
by PRE_FF:1;

Lm2:  (1 + 1) + 1 = 3
;

Lm3:  for k being Nat holds Fib (k + 1) >= k
proof
defpred S1[ Nat] means  Fib ($1 + 1) >= $1;
 (0 + 1) + 1 = 2 ;
then A1: S1[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]
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: S1[k + 2]
hence  S1[k + 2] by Lm1, Lm2, PRE_FF:1; ::_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: Fib ((k + 2) + 1) = (Fib ((k + 1) + 1)) + (Fib (k + 1)) by PRE_FF:1;
A7: k + (k + 1) <= (Fib (k + 1)) + (k + 1) by A3, XREAL_1:6;
 (Fib (k + 1)) + (k + 1) <= (Fib ((k + 1) + 1)) + (Fib (k + 1)) by A4, XREAL_1:6;
then  k + (k + 1) <= Fib ((k + 2) + 1) by A6, A7, XXREAL_0:2;
hence  S1[k + 2] by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A8: S1[ 0 ] by PRE_FF:1;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A8, A1, A2); ::_thesis: verum
end;

Lm4:  for m being Element of NAT holds Fib (m + 1) >= Fib m
proof
defpred S1[ Element of NAT ] means  Fib ($1 + 1) >= Fib $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: Fib k >= 0 by NAT_1:2;
 Fib ((k + 1) + 1) = (Fib (k + 1)) + (Fib k) by PRE_FF:1;
then  Fib ((k + 1) + 1) >= (Fib (k + 1)) + 0 by A2, XREAL_1:6;
hence  ( S1[k] implies S1[k + 1] ) ; ::_thesis: verum
end;
A3: S1[ 0 ] by PRE_FF:1;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

Lm5:  for m, n being Element of NAT st m >= n holds
Fib m >= Fib n
proof
A1: for k, n being Element of NAT holds Fib (n + k) >= Fib n
proof
defpred S1[ Element of NAT ] means  for n being Element of NAT holds Fib (n + $1) >= Fib n;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
let n be Element of NAT ; ::_thesis: Fib (n + (k + 1)) >= Fib n
 n + (k + 1) = (n + k) + 1 ;
then A4: Fib (n + (k + 1)) >= Fib (n + k) by Lm4;
 Fib (n + k) >= Fib n by A3;
hence  Fib (n + (k + 1)) >= Fib n by A4, XXREAL_0:2; ::_thesis: verum
end;
let k, n be Element of NAT ; ::_thesis: Fib (n + k) >= Fib n
A5: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2);
hence  Fib (n + k) >= Fib n ; ::_thesis: verum
end;
let m, n be Element of NAT ; ::_thesis: ( m >= n implies Fib m >= Fib n )
assume  m >= n ; ::_thesis: Fib m >= Fib n
then consider k being Nat such that
A6: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 m = n + k by A6;
hence  Fib m >= Fib n by A1; ::_thesis: verum
end;

Lm6:  for m being Element of NAT holds Fib (m + 1) <> 0
proof
let m be Element of NAT ; ::_thesis: Fib (m + 1) <> 0
percases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; ::_thesis: Fib (m + 1) <> 0
hence  Fib (m + 1) <> 0 by PRE_FF:1; ::_thesis: verum
end;
suppose m <> 0 ; ::_thesis: Fib (m + 1) <> 0
hence  Fib (m + 1) <> 0 by Lm3, NAT_1:3; ::_thesis: verum
end;
end;
end;

theorem Th4: :: FIB_NUM:4
for m, n being Nat holds Fib (m + (n + 1)) = ((Fib n) * (Fib m)) + ((Fib (n + 1)) * (Fib (m + 1)))
proof
defpred S1[ Nat] means  for n being Nat holds Fib ($1 + (n + 1)) = ((Fib n) * (Fib $1)) + ((Fib (n + 1)) * (Fib ($1 + 1)));
A1: S1[ 0 ] by PRE_FF:1;
A2: 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
A3: S1[k] and
A4: S1[k + 1] ; ::_thesis: S1[k + 2]
thus  S1[k + 2] ::_thesis: verum
proof
let n be Nat; ::_thesis: Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1)))
A5: Fib (((k + 1) + 1) + (n + 1)) = Fib (((k + (n + 1)) + 1) + 1)
.= (Fib (k + (n + 1))) + (Fib ((k + 1) + (n + 1))) by PRE_FF:1 ;
set a = (Fib n) * (Fib k);
set b = (Fib (n + 1)) * (Fib (k + 1));
set c = (Fib n) * (Fib (k + 1));
set d = (Fib (n + 1)) * (Fib ((k + 1) + 1));
A6: (((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1)))) + (((Fib n) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) = (((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1)))) + (((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) ;
A7: ((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1))) = (Fib (n + 1)) * ((Fib (k + 1)) + (Fib ((k + 1) + 1)))
.= (Fib (n + 1)) * (Fib (((k + 1) + 1) + 1)) by PRE_FF:1 ;
A8: ((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1))) = (Fib n) * ((Fib k) + (Fib (k + 1)))
.= (Fib n) * (Fib ((k + 1) + 1)) by PRE_FF:1 ;
 Fib (k + (n + 1)) = ((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1))) by A3;
hence  Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1))) by A4, A5, A6, A8, A7; ::_thesis: verum
end;
end;
A9: S1[1] by Lm1, PRE_FF:1;
thus  for k being Nat holds S1[k] from FIB_NUM:sch_1(A1, A9, A2); ::_thesis: verum
end;

Lm7:  for n being Element of NAT holds (Fib n) gcd (Fib (n + 1)) = 1
proof
defpred S1[ Element of NAT ] means (Fib $1) gcd (Fib ($1 + 1)) = 1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(Fib (k + 1)) gcd (Fib ((k + 1) + 1)) = (Fib (k + 1)) gcd ((Fib (k + 1)) + (Fib k)) by PRE_FF:1
.= 1 by A2, Th1 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by NEWTON:52, PRE_FF:1;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

theorem :: FIB_NUM:5
for m, n being Element of NAT holds (Fib m) gcd (Fib n) = Fib (m gcd n)
proof
defpred S1[ Element of NAT , Element of NAT ] means (Fib $1) gcd (Fib $2) = Fib ($1 gcd $2);
A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ) holds
for m being Element of NAT st m <= k holds
S1[k,m]
proof
let k be Element of NAT ; ::_thesis: ( ( for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ) implies for m being Element of NAT st m <= k holds
S1[k,m] )
assume A2: for m, n being Element of NAT st m < k & n < k holds
S1[m,n] ; ::_thesis: for m being Element of NAT st m <= k holds
S1[k,m]
let m be Element of NAT ; ::_thesis: ( m <= k implies S1[k,m] )
assume A3: m <= k ; ::_thesis: S1[k,m]
percases ( m = k or m < k ) by A3, XXREAL_0:1;
supposeA4: m = k ; ::_thesis: S1[k,m]
hence (Fib k) gcd (Fib m) = Fib k by NAT_D:32
.= Fib (k gcd m) by A4, NAT_D:32 ;
::_thesis: verum
end;
supposeA5: m < k ; ::_thesis: S1[k,m]
A6: not m < 0 by NAT_1:2;
thus  S1[k,m] ::_thesis: verum
proof
percases ( m = 0 or m > 0 ) by A6, XXREAL_0:1;
supposeA7: m = 0 ; ::_thesis: S1[k,m]
then  (Fib k) gcd (Fib m) = Fib k by NEWTON:52, PRE_FF:1;
hence  S1[k,m] by A7, NEWTON:52; ::_thesis: verum
end;
supposeA8: m > 0 ; ::_thesis: S1[k,m]
thus  S1[k,m] ::_thesis: verum
proof
consider r being Nat such that
A9: k = m + r by A3, NAT_1:10;
reconsider r = r as Element of NAT by ORDINAL1:def_12;
A10: r <= k by A9, NAT_1:11;
 r <> 0 by A5, A9;
then consider rr being Nat such that
A11: r = rr + 1 by NAT_1:6;
reconsider rr = rr as Element of NAT by ORDINAL1:def_12;
 Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A9, A11, Th4;
then A12: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by A11, EULER_1:8;
 (Fib m) gcd (Fib (m + 1)) = 1 by Lm7;
then A13: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by A12, Th2;
 r <> k by A8, A9;
then A14: r < k by A10, XXREAL_0:1;
 k gcd m = m gcd r by A9, Th1;
hence  S1[k,m] by A2, A5, A13, A14; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A15: for m, n being Element of NAT st S1[m,n] holds
S1[n,m] ;
thus  for m, n being Element of NAT holds S1[m,n] from FIB_NUM:sch_2(A15, A1); ::_thesis: verum
end;

begin


theorem Th6: :: FIB_NUM:6
for x, a, b, c being real number st a <> 0 & delta (a,b,c) >= 0 holds
( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )
proof
let x, a, b, c be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 implies ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) )
set lh = ((a * (x ^2)) + (b * x)) + c;
set r1 = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a);
set r2 = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a);
assume that
A1: a <> 0 and
A2: delta (a,b,c) >= 0 ; ::_thesis: ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )
 ((a * (x ^2)) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) by A1, A2, QUIN_1:16;
hence  ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) by A1, A2, QUIN_1:15; ::_thesis: verum
end;

definition
func tau  ->  real number  equals :: FIB_NUM:def 1
(1 + (sqrt 5)) / 2;
correctness
coherence
(1 + (sqrt 5)) / 2 is real number ;
;
end;

:: deftheorem  defines tau FIB_NUM:def_1_:_
 tau = (1 + (sqrt 5)) / 2;

definition
func tau_bar  ->  real number  equals :: FIB_NUM:def 2
(1 - (sqrt 5)) / 2;
correctness
coherence
(1 - (sqrt 5)) / 2 is real number ;
;
end;

:: deftheorem  defines tau_bar FIB_NUM:def_2_:_
 tau_bar = (1 - (sqrt 5)) / 2;

Lm8:  ( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 )
proof
A1: delta (1,(- 1),(- 1)) = ((- 1) ^2) - ((4 * 1) * (- 1)) by QUIN_1:def_1
.= 5 ;
then A2: ((- (- 1)) - (sqrt (delta (1,(- 1),(- 1))))) / (2 * 1) = tau_bar ;
A3: for x being real number st ( x = tau or x = tau_bar ) holds
x ^2 = x + 1
proof
let x be real number ; ::_thesis: ( ( x = tau or x = tau_bar ) implies x ^2 = x + 1 )
assume  ( x = tau or x = tau_bar ) ; ::_thesis: x ^2 = x + 1
then  ((1 * (x ^2)) + ((- 1) * x)) + (- 1) = 0 by A1, A2, Th6;
hence  x ^2 = x + 1 ; ::_thesis: verum
end;
hence  tau ^2 = tau + 1 ; ::_thesis: tau_bar ^2 = tau_bar + 1
thus  tau_bar ^2 = tau_bar + 1 by A3; ::_thesis: verum
end;

Lm9:  2 < sqrt 5
by SQUARE_1:20, SQUARE_1:27;

Lm10:  sqrt 5 <> 0
by SQUARE_1:20, SQUARE_1:27;

Lm11:  sqrt 5 < 3
proof
 3 ^2 = 9 ;
then  sqrt 9 = 3 by SQUARE_1:22;
hence  sqrt 5 < 3 by SQUARE_1:27; ::_thesis: verum
end;

 1 < tau
proof
 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27;
then  1 < sqrt 5 by XXREAL_0:2;
then  1 + 1 < 1 + (sqrt 5) by XREAL_1:8;
then  2 / 2 < (1 + (sqrt 5)) / 2 by XREAL_1:74;
hence  1 < tau ; ::_thesis: verum
end;

then Lm12:  0 < tau
by XXREAL_0:2;

Lm13:  tau_bar < 0
proof
 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27;
then  not 0 + (sqrt 5) <= 1 by XXREAL_0:2;
then  0 * 2 > (1 - (sqrt 5)) / 1 by XREAL_1:19;
then  (1 - (sqrt 5)) / 2 < 0 * 1 by XREAL_1:113;
hence  tau_bar < 0 ; ::_thesis: verum
end;

Lm14:  abs tau_bar < 1
proof
 (sqrt 5) - 1 < 3 - 1 by Lm11, XREAL_1:9;
then A1: ((sqrt 5) - 1) / 2 < 2 / 2 by XREAL_1:74;
abs tau_bar = - ((1 - (sqrt 5)) / 2) by Lm13, ABSVALUE:def_1
.= ((sqrt 5) - 1) / 2 ;
hence  abs tau_bar < 1 by A1; ::_thesis: verum
end;

theorem Th7: :: FIB_NUM:7
for n being Nat holds Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)
proof
defpred S1[ Nat] means  Fib $1 = ((tau to_power $1) - (tau_bar to_power $1)) / (sqrt 5);
A1: tau_bar to_power 1 = tau_bar by POWER:25;
 tau_bar to_power 0 = 1 by POWER:24;
then ((tau to_power 0) - (tau_bar to_power 0)) / (sqrt 5) = (1 - 1) / (sqrt 5) by POWER:24
.= 0 ;
then A2: S1[ 0 ] by 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]
set a = tau to_power k;
set a1 = tau_bar to_power k;
set b = tau to_power (k + 1);
set b1 = tau_bar to_power (k + 1);
set c = tau to_power (k + 2);
set c1 = tau_bar to_power (k + 2);
A6: tau_bar to_power (k + 2) = tau_bar |^ (k + 2) by POWER:41
.= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:8
.= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:6
.= (tau_bar |^ k) * (tau_bar + 1) by Lm8, NEWTON:5
.= ((tau_bar |^ k) * tau_bar) + ((tau_bar |^ k) * 1)
.= (tau_bar |^ (k + 1)) + ((tau_bar |^ k) * 1) by NEWTON:6
.= (tau_bar to_power (k + 1)) + (tau_bar |^ k) by POWER:41
.= (tau_bar to_power k) + (tau_bar to_power (k + 1)) by POWER:41 ;
A7: tau to_power (k + 2) = (tau to_power 2) * (tau to_power k) by Lm12, POWER:27
.= (tau to_power k) * (tau + 1) by Lm8, POWER:46
.= ((tau to_power k) * tau) + ((tau to_power k) * 1)
.= ((tau to_power k) * (tau to_power 1)) + (tau to_power k) by POWER:25
.= (tau to_power k) + (tau to_power (k + 1)) by Lm12, POWER:27 ;
Fib (k + 2) = Fib ((k + 1) + 1)
.= (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) + (((tau to_power (k + 1)) - (tau_bar to_power (k + 1))) / (sqrt 5)) by A4, A5, PRE_FF:1
.= ((tau to_power (k + 2)) - (tau_bar to_power (k + 2))) / (sqrt 5) by A7, A6 ;
hence  S1[k + 2] ; ::_thesis: verum
end;
 tau - tau_bar = sqrt 5 ;
then ((tau to_power 1) - (tau_bar to_power 1)) / (sqrt 5) = (sqrt 5) / (sqrt 5) by A1, POWER:25
.= Fib 1 by Lm10, PRE_FF:1, XCMPLX_1:60 ;
then A8: S1[1] ;
thus  for n being Nat holds S1[n] from FIB_NUM:sch_1(A2, A8, A3); ::_thesis: verum
end;

Lm15:  for n being Element of NAT
for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
proof
let n be Element of NAT ; ::_thesis: for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
let x be real number ; ::_thesis: ( abs x <= 1 implies abs (x |^ n) <= 1 )
defpred S1[ Element of NAT ] means  abs (x |^ $1) <= 1;
assume A1: abs x <= 1 ; ::_thesis: abs (x |^ n) <= 1
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: abs (x |^ (k + 1)) = abs ((x |^ k) * x) by NEWTON:6
.= (abs (x |^ k)) * (abs x) by COMPLEX1:65 ;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A1, A3, COMPLEX1:46, XREAL_1:160; ::_thesis: verum
end;
abs (x |^ 0) = abs 1 by NEWTON:4
.= 1 by ABSVALUE:def_1 ;
then A4: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2);
hence  abs (x |^ n) <= 1 ; ::_thesis: verum
end;

Lm16:  for n being Element of NAT holds abs ((tau_bar to_power n) / (sqrt 5)) < 1
proof
let n be Element of NAT ; ::_thesis: abs ((tau_bar to_power n) / (sqrt 5)) < 1
set y = tau_bar to_power n;
set z = sqrt 5;
A1: abs (tau_bar to_power n) = abs (tau_bar |^ n) by POWER:41;
A2: abs ((tau_bar to_power n) / (sqrt 5)) = abs ((tau_bar to_power n) * ((sqrt 5) "))
.= (abs (tau_bar to_power n)) * (abs ((sqrt 5) ")) by COMPLEX1:65 ;
A3: 1 / (sqrt 5) < 1 / 2 by Lm9, XREAL_1:88;
 sqrt 5 > 0 by Lm9, XXREAL_0:2;
then A4: (sqrt 5) " > 0 by XREAL_1:122;
then  abs ((sqrt 5) ") = (sqrt 5) " by ABSVALUE:def_1;
then A5: abs ((sqrt 5) ") < 1 by A3, XXREAL_0:2;
 abs ((sqrt 5) ") >= 0 by A4, ABSVALUE:def_1;
hence  abs ((tau_bar to_power n) / (sqrt 5)) < 1 by A1, A2, A5, Lm14, Lm15, XREAL_1:162; ::_thesis: verum
end;

theorem :: FIB_NUM:8
for n being Element of NAT holds abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1
proof
let n be Element of NAT ; ::_thesis: abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1
set k = Fib n;
set x = tau to_power n;
set y = tau_bar to_power n;
set z = sqrt 5;
Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7
.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) ;
then  abs (- ((Fib n) - ((tau to_power n) / (sqrt 5)))) < 1 by Lm16;
hence  abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1 by COMPLEX1:52; ::_thesis: verum
end;


theorem Th9: :: FIB_NUM:9
for f, g, h being Real_Sequence st g is non-zero holds
(f /" g) (#) (g /" h) = f /" h
proof
let f, g, h be Real_Sequence; ::_thesis: ( g is non-zero implies (f /" g) (#) (g /" h) = f /" h )
set f3 = f /" g;
set g3 = g /" h;
set h3 = f /" h;
assume A1: g is non-zero ; ::_thesis: (f /" g) (#) (g /" h) = f /" h
 for n being Element of NAT holds ((f /" g) (#) (g /" h)) . n = (f /" h) . n
proof
let n be Element of NAT ; ::_thesis: ((f /" g) (#) (g /" h)) . n = (f /" h) . n
set a = f . n;
set b = (g . n) " ;
set c = g . n;
set d = (h . n) " ;
A2: (g /" h) . n = (g . n) * ((h ") . n) by SEQ_1:8
.= (g . n) * ((h . n) ") by VALUED_1:10 ;
A3: (f /" h) . n = (f . n) * ((h ") . n) by SEQ_1:8
.= (f . n) * ((h . n) ") by VALUED_1:10 ;
A4: g . n <> 0 by A1, SEQ_1:5;
A5: ((g . n) ") * (g . n) = (1 / (g . n)) * (g . n)
.= 1 by A4, XCMPLX_1:106 ;
(f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8
.= (f . n) * ((g . n) ") by VALUED_1:10 ;
then ((f /" g) (#) (g /" h)) . n = ((f . n) * ((g . n) ")) * ((g . n) * ((h . n) ")) by A2, SEQ_1:8
.= ((((g . n) ") * (g . n)) * (f . n)) * ((h . n) ")
.= (f /" h) . n by A3, A5 ;
hence  ((f /" g) (#) (g /" h)) . n = (f /" h) . n ; ::_thesis: verum
end;
hence  (f /" g) (#) (g /" h) = f /" h by FUNCT_2:63; ::_thesis: verum
end;

theorem Th10: :: FIB_NUM:10
for f, g being Real_Sequence
for n being Element of NAT holds
( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )
proof
let f, g be Real_Sequence; ::_thesis: for n being Element of NAT holds
( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )
let n be Element of NAT ; ::_thesis: ( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )
A1: (f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8
.= (f . n) * ((g . n) ") by VALUED_1:10 ;
hence  (f /" g) . n = (f . n) / (g . n) ; ::_thesis: (f /" g) . n = (f . n) * ((g . n) ")
thus  (f /" g) . n = (f . n) * ((g . n) ") by A1; ::_thesis: verum
end;

theorem :: FIB_NUM:11
for F being Real_Sequence st ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) holds
( F is convergent & lim F = tau )
proof
deffunc H1( Element of NAT ) ->  Element of COMPLEX = (tau to_power $1) / (sqrt 5);
let F be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) implies ( F is convergent & lim F = tau ) )
consider f being Real_Sequence such that
A1: for n being Element of NAT holds f . n = Fib n from SEQ_1:sch_1();
set f2 = f ^\ 2;
set f1 = f ^\ 1;
A2: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:48
.= f ^\ 2 ;
A3: for n being Element of NAT holds (f ^\ 2) . n <> 0
proof
let n be Element of NAT ; ::_thesis: (f ^\ 2) . n <> 0
(f ^\ 2) . n = f . (n + 2) by NAT_1:def_3
.= Fib ((n + 1) + 1) by A1 ;
hence  (f ^\ 2) . n <> 0 by Lm3, NAT_1:5; ::_thesis: verum
end;
A4: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = 1
proof
let n be Nat; ::_thesis: ((f ^\ 2) /" (f ^\ 2)) . n = 1
A5: n in NAT by ORDINAL1:def_12;
then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) ") by Th10
.= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n))
.= 1 by A3, A5, XCMPLX_1:106 ;
hence  ((f ^\ 2) /" (f ^\ 2)) . n = 1 ; ::_thesis: verum
end;
then A6: (f ^\ 2) /" (f ^\ 2) is constant by VALUED_0:def_18;
A7: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:20;
then A8: f /" f is convergent by A6, SEQ_4:21;
 ((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A4;
then  lim ((f ^\ 2) /" (f ^\ 2)) = 1 by A6, SEQ_4:25;
then A9: lim (f /" f) = 1 by A6, A7, SEQ_4:22;
 ex g being Real_Sequence st
for n being Element of NAT holds g . n = H1(n) from SEQ_1:sch_1();
then consider g being Real_Sequence such that
A10: for n being Element of NAT holds g . n = H1(n) ;
set g1 = g ^\ 1;
A11: for n being Element of NAT holds g . n <> 0
proof
let n be Element of NAT ; ::_thesis: g . n <> 0
A12: (sqrt 5) " <> 0 by SQUARE_1:20, SQUARE_1:27, XCMPLX_1:202;
A13: tau |^ n <> 0 by Lm12, PREPOWER:5;
g . n = (tau to_power n) / (sqrt 5) by A10
.= (tau to_power n) * ((sqrt 5) ")
.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;
hence  g . n <> 0 by A13, A12, XCMPLX_1:6; ::_thesis: verum
end;
then A14: g is non-zero by SEQ_1:5;
then A15: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by Th9;
set g2 = (g ^\ 1) ^\ 1;
 for n being Element of NAT holds (f ^\ 1) . n <> 0
proof
let n be Element of NAT ; ::_thesis: (f ^\ 1) . n <> 0
(f ^\ 1) . n = f . (n + 1) by NAT_1:def_3
.= Fib (n + 1) by A1 ;
hence  (f ^\ 1) . n <> 0 by Lm6; ::_thesis: verum
end;
then A16: f ^\ 1 is non-zero by SEQ_1:5;
 for n being Element of NAT holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
proof
let n be Element of NAT ; ::_thesis: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
A17: ((g ^\ 1) ^\ 1) . n <> 0 by A14, SEQ_1:5;
A18: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) ") by Th10;
 ((f ^\ 2) . n) " <> 0 by A16, A2, SEQ_1:5, XCMPLX_1:202;
hence  (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by A17, A18, XCMPLX_1:6; ::_thesis: verum
end;
then A19: ((g ^\ 1) ^\ 1) /" (f ^\ 2) is non-zero by SEQ_1:5;
 (g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:48;
then A20: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by SEQM_3:20;
A21: for n being Element of NAT holds (f ^\ 1) . n = Fib (n + 1)
proof
let n be Element of NAT ; ::_thesis: (f ^\ 1) . n = Fib (n + 1)
(f ^\ 1) . n = f . (n + 1) by NAT_1:def_3
.= Fib (n + 1) by A1 ;
hence  (f ^\ 1) . n = Fib (n + 1) ; ::_thesis: verum
end;
assume A22: for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ; ::_thesis: ( F is convergent & lim F = tau )
 for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n
proof
let n be Element of NAT ; ::_thesis: F . n = ((f ^\ 1) /" f) . n
((f ^\ 1) /" f) . n = ((f ^\ 1) . n) / (f . n) by Th10
.= (Fib (n + 1)) / (f . n) by A21
.= (Fib (n + 1)) / (Fib n) by A1 ;
hence  F . n = ((f ^\ 1) /" f) . n by A22; ::_thesis: verum
end;
then  F = (f ^\ 1) /" f by FUNCT_2:63;
then A23: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by A2, SEQM_3:20;
A24: ((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:20;
A25: for n being Nat holds ((g ^\ 1) /" g) . n = tau
proof
let n be Nat; ::_thesis: ((g ^\ 1) /" g) . n = tau
A26: n in NAT by ORDINAL1:def_12;
then A27: g . n = (tau to_power n) / (sqrt 5) by A10
.= (tau to_power n) * ((sqrt 5) ")
.= (tau |^ n) * ((sqrt 5) ") by POWER:41 ;
A28: g . n <> 0 by A11, A26;
(g ^\ 1) . n = g . (n + 1) by NAT_1:def_3
.= (tau to_power (n + 1)) / (sqrt 5) by A10
.= (tau to_power (n + 1)) * ((sqrt 5) ")
.= (tau |^ (n + 1)) * ((sqrt 5) ") by POWER:41
.= (tau * (tau |^ n)) * ((sqrt 5) ") by NEWTON:6
.= tau * (g . n) by A27 ;
then ((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) ") by A26, Th10
.= tau * ((g . n) * ((g . n) "))
.= tau * 1 by A28, XCMPLX_0:def_7
.= tau ;
hence  ((g ^\ 1) /" g) . n = tau ; ::_thesis: verum
end;
 tau in REAL by XREAL_0:def_1;
then A29: (g ^\ 1) /" g is constant by A25, VALUED_0:def_18;
A30: for x being real number st 0 < x holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f ") . m) - 0) < x
proof
let x be real number ; ::_thesis: ( 0 < x implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f ") . m) - 0) < x )
assume  0 < x ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f ") . m) - 0) < x
then consider k being Element of NAT  such that
A31: k > 0 and
 0 < 1 / k and
A32: 1 / k <= x by Th3;
 for m being Element of NAT st k + 2 <= m holds
abs (((f ") . m) - 0) < x
proof
let m be Element of NAT ; ::_thesis: ( k + 2 <= m implies abs (((f ") . m) - 0) < x )
 k + 2 = (k + 1) + 1 ;
then A33: Fib (k + 2) >= k + 1 by Lm3;
assume  k + 2 <= m ; ::_thesis: abs (((f ") . m) - 0) < x
then  Fib (k + 2) <= Fib m by Lm5;
then  k + 1 <= Fib m by A33, XXREAL_0:2;
then A34: k + 1 <= f . m by A1;
then  0 < f . m by NAT_1:5, XXREAL_0:2;
then A35: 0 <= (f . m) " by XREAL_1:122;
 k + 0 < k + 1 by XREAL_1:6;
then A36: 1 / (k + 1) < 1 / k by A31, XREAL_1:88;
A37: abs (((f ") . m) - 0) = abs ((f . m) ") by VALUED_1:10
.= (f . m) " by A35, ABSVALUE:def_1
.= 1 / (f . m) ;
 1 / (f . m) <= 1 / (k + 1) by A34, NAT_1:5, XREAL_1:85;
then  1 / (f . m) < 1 / k by A36, XXREAL_0:2;
hence  abs (((f ") . m) - 0) < x by A32, A37, XXREAL_0:2; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f ") . m) - 0) < x ; ::_thesis: verum
end;
then A38: f " is convergent by SEQ_2:def_6;
then A39: lim (f ") = 0 by A30, SEQ_2:def_7;
deffunc H2( Element of NAT ) ->  Element of COMPLEX = (tau_bar to_power $1) / (sqrt 5);
 ex h being Real_Sequence st
for n being Element of NAT holds h . n = H2(n) from SEQ_1:sch_1();
then consider h being Real_Sequence such that
A40: for n being Element of NAT holds h . n = H2(n) ;
A41: for n being Element of NAT holds f . n = (g . n) - (h . n)
proof
let n be Element of NAT ; ::_thesis: f . n = (g . n) - (h . n)
f . n = Fib n by A1
.= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7
.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))
.= (g . n) - ((tau_bar to_power n) / (sqrt 5)) by A10
.= (g . n) - (h . n) by A40 ;
hence  f . n = (g . n) - (h . n) ; ::_thesis: verum
end;
 for n being Element of NAT holds g . n = (f . n) + (h . n)
proof
let n be Element of NAT ; ::_thesis: g . n = (f . n) + (h . n)
 f . n = (g . n) - (h . n) by A41;
hence  g . n = (f . n) + (h . n) ; ::_thesis: verum
end;
then  g = f + h by SEQ_1:7;
then A42: g /" f = (f /" f) + (h /" f) by SEQ_1:49;
 for n being Element of NAT holds abs (h . n) < 1
proof
let n be Element of NAT ; ::_thesis: abs (h . n) < 1
 h . n = (tau_bar to_power n) / (sqrt 5) by A40;
hence  abs (h . n) < 1 by Lm16; ::_thesis: verum
end;
then A43: h is bounded by SEQ_2:3;
 f " is convergent by A30, SEQ_2:def_6;
then A44: h /" f is convergent by A43, A39, SEQ_2:25;
then A45: g /" f is convergent by A8, A42, SEQ_2:5;
 ((g ^\ 1) /" g) . 0 = tau by A25;
then  lim ((g ^\ 1) /" g) = tau by A29, SEQ_4:25;
then A46: lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau by A29, A24, SEQ_4:20;
A47: (g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:20;
 lim (h /" f) = 0 by A43, A38, A39, SEQ_2:26;
then A48: lim (g /" f) = 1 + 0 by A44, A8, A9, A42, SEQ_2:6
.= 1 ;
then A49: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by A45, A20, SEQ_4:20;
then  (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by A45, A20, A19, SEQ_2:21;
then A50: (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:40;
A51: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by A14, Th9;
then A52: (f ^\ 2) /" (g ^\ 1) is convergent by A29, A50, A24, SEQ_2:14;
then A53: (f ^\ 2) /" (f ^\ 1) is convergent by A45, A47, A15, SEQ_2:14;
hence  F is convergent by A23, SEQ_4:21; ::_thesis: lim F = tau
lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") = 1 " by A45, A20, A49, A19, SEQ_2:22
.= 1 ;
then  lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:40;
then A54: lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by A29, A51, A50, A24, A46, SEQ_2:15
.= tau ;
 lim ((g ^\ 1) /" (f ^\ 1)) = 1 by A45, A48, A47, SEQ_4:20;
then  lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by A45, A54, A52, A47, A15, SEQ_2:15;
hence  lim F = tau by A53, A23, SEQ_4:22; ::_thesis: verum
end;