:: FIB_NUM2 semantic presentation

begin


theorem :: FIB_NUM2:1
for n being non empty Element of NAT holds (n -' 1) + 2 = n + 1
proof
let n be non empty Element of NAT ; ::_thesis: (n -' 1) + 2 = n + 1
 n >= 1 by NAT_2:19;
then (n -' 1) + 2 = (n + 2) -' 1 by NAT_D:38
.= (n + 2) - 1 by NAT_D:37 ;
hence  (n -' 1) + 2 = n + 1 ; ::_thesis: verum
end;

theorem Th2: :: FIB_NUM2:2
for n being odd Integer holds (- 1) to_power n = - 1
proof
let n be odd Integer; ::_thesis: (- 1) to_power n = - 1
(- 1) to_power n = - (1 to_power n) by POWER:48
.= - 1 by POWER:26 ;
hence  (- 1) to_power n = - 1 ; ::_thesis: verum
end;

theorem Th3: :: FIB_NUM2:3
for n being even Integer holds (- 1) to_power n = 1
proof
let n be even Integer; ::_thesis: (- 1) to_power n = 1
 (- 1) to_power n = 1 to_power n by POWER:47;
hence  (- 1) to_power n = 1 by POWER:26; ::_thesis: verum
end;

theorem Th4: :: FIB_NUM2:4
for m being non empty real number
for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
proof
let m be non empty real number ; ::_thesis: for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
let n be Integer; ::_thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
percases ( n is odd or n is even ) ;
supposeA1: n is odd ; ::_thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
then (- m) to_power n = - (m to_power n) by POWER:48
.= (- 1) * (m to_power n)
.= ((- 1) to_power n) * (m to_power n) by A1, Th2 ;
hence  ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; ::_thesis: verum
end;
supposeA2: n is even ; ::_thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
then (- m) to_power n = 1 * (m to_power n) by POWER:47
.= ((- 1) to_power n) * (m to_power n) by A2, Th3 ;
hence  ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; ::_thesis: verum
end;
end;
end;

theorem Th5: :: FIB_NUM2:5
for k, m being Nat
for a being real number holds a to_power (k + m) = (a to_power k) * (a to_power m)
proof
let k, m be Nat; ::_thesis: for a being real number holds a to_power (k + m) = (a to_power k) * (a to_power m)
let a be real number ; ::_thesis: a to_power (k + m) = (a to_power k) * (a to_power m)
thus a to_power (k + m) = a |^ (k + m) by POWER:41
.= (a |^ k) * (a |^ m) by NEWTON:8
.= (a to_power k) * (a |^ m) by POWER:41
.= (a to_power k) * (a to_power m) by POWER:41 ; ::_thesis: verum
end;

theorem Th6: :: FIB_NUM2:6
for n being Nat
for k being non empty real number
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)
proof
let n be Nat; ::_thesis: for k being non empty real number
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)
let k be non empty real number ; ::_thesis: for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)
let m be odd Integer; ::_thesis: (k to_power m) to_power n = k to_power (m * n)
k to_power (m * n) = k #Z (m * n) by POWER:def_2
.= (k #Z m) #Z n by PREPOWER:45
.= (k to_power m) #Z n by POWER:def_2
.= (k to_power m) to_power n by POWER:def_2 ;
hence  (k to_power m) to_power n = k to_power (m * n) ; ::_thesis: verum
end;

theorem Th7: :: FIB_NUM2:7
for n being Nat holds ((- 1) to_power (- n)) ^2 = 1
proof
let n be Nat; ::_thesis: ((- 1) to_power (- n)) ^2 = 1
((- 1) to_power (- n)) ^2 = ((- 1) #Z (- n)) ^2 by POWER:def_2
.= (1 / ((- 1) #Z n)) ^2 by PREPOWER:41
.= (1 / ((- 1) #Z n)) to_power 2 by POWER:46
.= (1 / ((- 1) #Z n)) |^ 2 by POWER:41
.= 1 / (((- 1) #Z n) |^ 2) by PREPOWER:7
.= 1 / (((- 1) #Z n) #Z 2) by PREPOWER:36
.= 1 / ((- 1) #Z (n * 2)) by PREPOWER:45
.= 1 / ((- 1) |^ (2 * n)) by PREPOWER:36
.= 1 / (1 |^ (2 * n)) by WSIERP_1:2
.= 1 / ((1 |^ 2) |^ n) by NEWTON:9
.= 1 / (1 |^ n) by NEWTON:10
.= 1 / 1 by NEWTON:10 ;
hence  ((- 1) to_power (- n)) ^2 = 1 ; ::_thesis: verum
end;

theorem Th8: :: FIB_NUM2:8
for k, m being Nat
for a being non empty real number holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)
proof
let k, m be Nat; ::_thesis: for a being non empty real number holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)
set K = - k;
set M = - m;
let a be non empty real number ; ::_thesis: (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)
(a to_power (- k)) * (a to_power (- m)) = (a #Z (- k)) * (a to_power (- m)) by POWER:def_2
.= (a #Z (- k)) * (a #Z (- m)) by POWER:def_2
.= a #Z ((- k) + (- m)) by PREPOWER:44
.= a to_power ((- k) - m) by POWER:def_2 ;
hence  (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m) ; ::_thesis: verum
end;

theorem Th9: :: FIB_NUM2:9
for n being Nat holds (- 1) to_power (- (2 * n)) = 1
proof
let n be Nat; ::_thesis: (- 1) to_power (- (2 * n)) = 1
(- 1) to_power (- (2 * n)) = (- 1) #Z ((- 1) * (2 * n)) by POWER:def_2
.= ((- 1) #Z (- 1)) #Z (2 * n) by PREPOWER:45
.= (1 / ((- 1) #Z 1)) #Z (2 * n) by PREPOWER:41
.= (1 / (- 1)) #Z (2 * n) by PREPOWER:35
.= (- 1) |^ (2 * n) by PREPOWER:36
.= 1 |^ (2 * n) by WSIERP_1:2
.= (1 |^ 2) |^ n by NEWTON:9
.= 1 |^ n by NEWTON:10
.= 1 by NEWTON:10 ;
hence  (- 1) to_power (- (2 * n)) = 1 ; ::_thesis: verum
end;

theorem Th10: :: FIB_NUM2:10
for k being Nat
for a being non empty real number holds (a to_power k) * (a to_power (- k)) = 1
proof
let k be Nat; ::_thesis: for a being non empty real number holds (a to_power k) * (a to_power (- k)) = 1
let a be non empty real number ; ::_thesis: (a to_power k) * (a to_power (- k)) = 1
(a to_power k) * (a to_power (- k)) = (a #Z k) * (a to_power (- k)) by POWER:def_2
.= (a #Z k) * (a #Z (- k)) by POWER:def_2
.= a #Z (k + (- k)) by PREPOWER:44
.= 1 by PREPOWER:34 ;
hence  (a to_power k) * (a to_power (- k)) = 1 ; ::_thesis: verum
end;

registration
let n be odd Integer;
cluster - n ->  odd ;
coherence
 not - n is even
proof
 - 1 = (2 * (- 1)) + 1 ;
then reconsider e = - 1 as odd Integer ;
 e * n is odd ;
hence  not - n is even ; ::_thesis: verum
end;
end;

registration
let n be even Integer;
cluster - n ->  even ;
coherence
 - n is even
proof
reconsider e = - 1 as Integer ;
 e * n is even ;
hence  - n is even ; ::_thesis: verum
end;
end;

theorem Th11: :: FIB_NUM2:11
for n being Nat holds (- 1) to_power (- n) = (- 1) to_power n
proof
let n be Nat; ::_thesis: (- 1) to_power (- n) = (- 1) to_power n
percases ( n is odd or n is even ) ;
suppose n is odd ; ::_thesis: (- 1) to_power (- n) = (- 1) to_power n
then reconsider n = n as odd Integer ;
(- 1) to_power (- n) = - 1 by Th2
.= (- 1) to_power n by Th2 ;
hence  (- 1) to_power (- n) = (- 1) to_power n ; ::_thesis: verum
end;
suppose n is even ; ::_thesis: (- 1) to_power (- n) = (- 1) to_power n
then reconsider n = n as even Integer ;
(- 1) to_power (- n) = 1 by Th3
.= (- 1) to_power n by Th3 ;
hence  (- 1) to_power (- n) = (- 1) to_power n ; ::_thesis: verum
end;
end;
end;

theorem Th12: :: FIB_NUM2:12
for n being Nat
for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
proof
let n be Nat; ::_thesis: for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
let k, m, m1, n1 be Element of NAT ; ::_thesis: ( k divides m & k divides n implies k divides (m * m1) + (n * n1) )
assume  ( k divides m & k divides n ) ; ::_thesis: k divides (m * m1) + (n * n1)
then  ( k divides m * m1 & k divides n * n1 ) by NAT_D:9;
hence  k divides (m * m1) + (n * n1) by NAT_D:8; ::_thesis: verum
end;

registration
cluster non empty finite with_non-empty_elements natural-membered for set ;
existence
 ex b1 being set st
( b1 is finite & not b1 is empty & b1 is natural-membered & b1 is with_non-empty_elements )
proof
take X = {1}; ::_thesis: ( X is finite & not X is empty & X is natural-membered & X is with_non-empty_elements )
thus  ( X is finite & not X is empty ) ; ::_thesis: ( X is natural-membered & X is with_non-empty_elements )
thus  X is natural-membered ; ::_thesis: X is with_non-empty_elements
thus  X is with_non-empty_elements ; ::_thesis: verum
end;
end;

registration
let f be Function of NAT,NAT;
let A be finite with_non-empty_elements natural-membered set ;
clusterf | A ->  FinSubsequence-like ;
coherence
 f | A is FinSubsequence-like
proof
percases ( not A is empty or A is empty ) ;
suppose not A is empty ; ::_thesis: f | A is FinSubsequence-like
then reconsider A9 = A as non empty finite with_non-empty_elements natural-membered set ;
reconsider k = max A9 as Element of NAT by ORDINAL1:def_12;
A1: dom (f | A) c= A by RELAT_1:58;
 dom (f | A) c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f | A) or x in Seg k )
assume A2: x in dom (f | A) ; ::_thesis: x in Seg k
then reconsider x9 = x as Nat by A1;
reconsider x9 = x9 as Element of NAT by ORDINAL1:def_12;
 ( 1 <= x9 & x9 <= k ) by A1, A2, NAT_1:14, XXREAL_2:def_8;
hence  x in Seg k ; ::_thesis: verum
end;
hence  f | A is FinSubsequence-like by FINSEQ_1:def_12; ::_thesis: verum
end;
suppose A is empty ; ::_thesis: f | A is FinSubsequence-like
hence  f | A is FinSubsequence-like ; ::_thesis: verum
end;
end;
end;
end;

theorem :: FIB_NUM2:13
for p being FinSubsequence holds rng (Seq p) c= rng p by RELAT_1:26;

definition
let f be Function of NAT,NAT;
let A be finite with_non-empty_elements natural-membered set ;
func Prefix (f,A) ->  FinSequence of NAT  equals :: FIB_NUM2:def 1
 Seq (f | A);
coherence
 Seq (f | A) is FinSequence of NAT
proof
 rng (Seq (f | A)) c= NAT by RELAT_1:def_19;
hence  Seq (f | A) is FinSequence of NAT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines Prefix FIB_NUM2:def_1_:_
 for f being Function of NAT,NAT
for A being finite with_non-empty_elements natural-membered set holds Prefix (f,A) = Seq (f | A);

theorem Th14: :: FIB_NUM2:14
for m, n being Nat
for k being Element of NAT st k <> 0 & k + m <= n holds
m < n
proof
let m, n be Nat; ::_thesis: for k being Element of NAT st k <> 0 & k + m <= n holds
m < n
let k be Element of NAT ; ::_thesis: ( k <> 0 & k + m <= n implies m < n )
assume A1: k <> 0 ; ::_thesis: ( not k + m <= n or m < n )
assume A2: k + m <= n ; ::_thesis: m < n
percases ( k + m < n or k + m = n ) by A2, XXREAL_0:1;
suppose k + m < n ; ::_thesis: m < n
hence  m < n by NAT_1:12; ::_thesis: verum
end;
supposeA3: k + m = n ; ::_thesis: m < n
assume  not m < n ; ::_thesis: contradiction
then  m + k >= n + k by XREAL_1:7;
then  n - n >= (n + k) - n by A3, XREAL_1:9;
hence  contradiction by A1; ::_thesis: verum
end;
end;
end;

registration
cluster omega  ->  bounded_below ;
coherence
 NAT is bounded_below ;
end;

theorem Th15: :: FIB_NUM2:15
for i, j being Nat
for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence
proof
let i, j be Nat; ::_thesis: for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence
let x, y be set ; ::_thesis: ( 0 < i & i < j implies {[i,x],[j,y]} is FinSubsequence )
assume that
A1: 0 < i and
A2: i < j ; ::_thesis: {[i,x],[j,y]} is FinSubsequence
reconsider X = {[i,x],[j,y]} as Function by A2, GRFUNC_1:8;
A3: 0 + 1 <= i by A1, NAT_1:13;
now__::_thesis:_for_x_being_set_st_x_in_{i,j}_holds_
x_in_Seg_j
let x be set ; ::_thesis: ( x in {i,j} implies x in Seg j )
assume  x in {i,j} ; ::_thesis: x in Seg j
then A4: ( x = i or x = j ) by TARSKI:def_2;
 i in NAT by ORDINAL1:def_12;
hence  x in Seg j by A2, A3, A4, FINSEQ_1:3; ::_thesis: verum
end;
then  ( dom X = {i,j} & {i,j} c= Seg j ) by RELAT_1:10, TARSKI:def_3;
hence  {[i,x],[j,y]} is FinSubsequence by FINSEQ_1:def_12; ::_thesis: verum
end;

theorem Th16: :: FIB_NUM2:16
for i, j being Nat
for x, y being set
for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
proof
let i, j be Nat; ::_thesis: for x, y being set
for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
let x, y be set ; ::_thesis: for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
let q be FinSubsequence; ::_thesis: ( i < j & q = {[i,x],[j,y]} implies Seq q = <*x,y*> )
assume that
A1: i < j and
A2: q = {[i,x],[j,y]} ; ::_thesis: Seq q = <*x,y*>
A3: q = (i,j) --> (x,y) by A1, A2, FUNCT_4:67;
 [i,x] in q by A2, TARSKI:def_2;
then A4: i in dom q by XTUPLE_0:def_12;
 [j,y] in q by A2, TARSKI:def_2;
then A5: j in dom q by XTUPLE_0:def_12;
A6: dom q = {i,j} by A2, RELAT_1:10;
 ex k being Nat st dom q c= Seg k by FINSEQ_1:def_12;
then  i >= 0 + 1 by A4, FINSEQ_1:1;
then  Seq q = q * <*i,j*> by A1, A6, FINSEQ_3:45
.= <*(q . i),(q . j)*> by A4, A5, FINSEQ_2:125
.= <*x,(q . j)*> by A1, A3, FUNCT_4:63
.= <*x,y*> by A3, FUNCT_4:63 ;
hence  Seq q = <*x,y*> ; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster Seg n ->  with_non-empty_elements ;
coherence
 Seg n is with_non-empty_elements
proof
 not 0 in Seg n by FINSEQ_1:1;
hence  Seg n is with_non-empty_elements by SETFAM_1:def_8; ::_thesis: verum
end;
end;

registration
let A be with_non-empty_elements set ;
cluster  ->  with_non-empty_elements for Element of bool A;
coherence
 for b1 being Subset of A holds b1 is with_non-empty_elements
proof
let L be Subset of A; ::_thesis: L is with_non-empty_elements
 not 0 in L ;
hence  L is with_non-empty_elements by SETFAM_1:def_8; ::_thesis: verum
end;
end;

registration
let A be with_non-empty_elements set ;
let B be set ;
clusterA /\ B ->  with_non-empty_elements ;
coherence
 A /\ B is with_non-empty_elements
proof
reconsider AB = A /\ B as Subset of A by XBOOLE_1:17;
 AB is with_non-empty_elements ;
hence  A /\ B is with_non-empty_elements ; ::_thesis: verum
end;
clusterB /\ A ->  with_non-empty_elements ;
coherence
 B /\ A is with_non-empty_elements ;
end;

theorem Th17: :: FIB_NUM2:17
for k being Element of NAT
for a being set st k >= 1 holds
{[k,a]} is FinSubsequence
proof
let k be Element of NAT ; ::_thesis: for a being set st k >= 1 holds
{[k,a]} is FinSubsequence
let a be set ; ::_thesis: ( k >= 1 implies {[k,a]} is FinSubsequence )
reconsider H = {[k,a]} as Function ;
A1: dom H = {k} by RELAT_1:9;
assume A2: k >= 1 ; ::_thesis: {[k,a]} is FinSubsequence
 dom H c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom H or x in Seg k )
assume  x in dom H ; ::_thesis: x in Seg k
then  x = k by A1, TARSKI:def_1;
hence  x in Seg k by A2; ::_thesis: verum
end;
hence  {[k,a]} is FinSubsequence by FINSEQ_1:def_12; ::_thesis: verum
end;

theorem Th18: :: FIB_NUM2:18
for i being Element of NAT
for y being set
for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
proof
let i be Element of NAT ; ::_thesis: for y being set
for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
let y be set ; ::_thesis: for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
let f be FinSubsequence; ::_thesis: ( f = {[1,y]} implies i Shift f = {[(1 + i),y]} )
set g = i Shift f;
assume A1: f = {[1,y]} ; ::_thesis: i Shift f = {[(1 + i),y]}
then  card f = 1 by CARD_2:42;
then  card (i Shift f) = 1 by PNPROC_1:54;
then A2: ex x being set st i Shift f = {x} by CARD_2:42;
A3: dom f = {1} by A1, RELAT_1:9;
 dom (i Shift f) = {(1 + i)}
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(1 + i)} c= dom (i Shift f)
let x be set ; ::_thesis: ( x in dom (i Shift f) implies x in {(1 + i)} )
assume  x in dom (i Shift f) ; ::_thesis: x in {(1 + i)}
then  x in  {  (i + o) where o is Element of NAT : o in dom f  }  by PNPROC_1:def_14;
then consider w being Element of NAT  such that
A4: i + w = x and
A5: w in dom f ;
 w = 1 by A3, A5, TARSKI:def_1;
hence  x in {(1 + i)} by A4, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(1 + i)} or x in dom (i Shift f) )
assume  x in {(1 + i)} ; ::_thesis: x in dom (i Shift f)
then A6: x = 1 + i by TARSKI:def_1;
 1 in dom f by A3, TARSKI:def_1;
then  x in  {  (i + o) where o is Element of NAT : o in dom f  }  by A6;
hence  x in dom (i Shift f) by PNPROC_1:def_14; ::_thesis: verum
end;
then A7: 1 + i in dom (i Shift f) by TARSKI:def_1;
 1 in dom f by A3, TARSKI:def_1;
then (i Shift f) . (1 + i) = f . 1 by PNPROC_1:def_14
.= y by A1, GRFUNC_1:6 ;
then  [(1 + i),y] in i Shift f by A7, FUNCT_1:def_2;
hence  i Shift f = {[(1 + i),y]} by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem Th19: :: FIB_NUM2:19
for q being FinSubsequence
for k, n being Element of NAT st dom q c= Seg k & n > k holds
ex p being FinSequence st
( q c= p & dom p = Seg n )
proof
let q be FinSubsequence; ::_thesis: for k, n being Element of NAT st dom q c= Seg k & n > k holds
ex p being FinSequence st
( q c= p & dom p = Seg n )
let k, n be Element of NAT ; ::_thesis: ( dom q c= Seg k & n > k implies ex p being FinSequence st
( q c= p & dom p = Seg n ) )
assume that
A1: dom q c= Seg k and
A2: n > k ; ::_thesis: ex p being FinSequence st
( q c= p & dom p = Seg n )
reconsider IK = id (Seg n) as Function ;
set IS = IK +* q;
A3: Seg k c= Seg n by A2, FINSEQ_1:5;
A4: dom (IK +* q) = (dom IK) \/ (dom q) by FUNCT_4:def_1
.= (Seg n) \/ (dom q) by RELAT_1:45
.= Seg n by A1, A3, XBOOLE_1:1, XBOOLE_1:12 ;
then reconsider IS = IK +* q as FinSequence by FINSEQ_1:def_2;
 q c= IS by FUNCT_4:25;
hence  ex p being FinSequence st
( q c= p & dom p = Seg n ) by A4; ::_thesis: verum
end;

theorem Th20: :: FIB_NUM2:20
for q being FinSubsequence ex p being FinSequence st q c= p
proof
let q be FinSubsequence; ::_thesis: ex p being FinSequence st q c= p
consider k being Nat such that
A1: dom q c= Seg k by FINSEQ_1:def_12;
reconsider IK = id (Seg k) as Function ;
set IS = IK +* q;
dom (IK +* q) = (dom IK) \/ (dom q) by FUNCT_4:def_1
.= (Seg k) \/ (dom q) by RELAT_1:45
.= Seg k by A1, XBOOLE_1:12 ;
then reconsider IS = IK +* q as FinSequence by FINSEQ_1:def_2;
 q c= IS by FUNCT_4:25;
hence  ex p being FinSequence st q c= p ; ::_thesis: verum
end;

begin

scheme :: FIB_NUM2:sch 1
FibInd1{ P1[ set ] } :
 for k being non empty Nat holds P1[k]
provided
A1: P1[1] and
A2: P1[2] and
A3: for k being non empty Nat st P1[k] & P1[k + 1] holds
P1[k + 2]
proof
let k be non empty Nat; ::_thesis: P1[k]
defpred S1[ Nat] means ( P1[$1] & P1[$1 + 1] );
A4: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty 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[1] by A1, A2;
 for k being non empty Nat holds S1[k] from NAT_1:sch_10(A6, A4);
hence  P1[k] ; ::_thesis: verum
end;

scheme :: FIB_NUM2:sch 2
FibInd2{ P1[ set ] } :
 for k being non trivial Nat holds P1[k]
provided
A1: P1[2] and
A2: P1[3] and
A3: for k being non trivial Nat st P1[k] & P1[k + 1] holds
P1[k + 2]
proof
defpred S1[ Nat] means ( P1[$1 + 1] & P1[$1 + 2] );
A4: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
 k + 1 <> 0 + 1 ;
then A5: k + 1 is non trivial Nat by NAT_2:def_1;
assume A6: S1[k] ; ::_thesis: S1[k + 1]
then  P1[(k + 1) + 1] ;
hence  S1[k + 1] by A3, A5, A6; ::_thesis: verum
end;
let k be non trivial Nat; ::_thesis: P1[k]
 k <> 1 by NAT_2:def_1;
then A7: k > 1 by NAT_2:19;
then  k - 1 > 1 - 1 by XREAL_1:9;
then A8: k - 1 > 0 ;
A9: S1[1] by A1, A2;
A10: for k being non empty Nat holds S1[k] from NAT_1:sch_10(A9, A4);
 (k -' 1) + 1 = k by A7, XREAL_1:235;
hence  P1[k] by A10, A8; ::_thesis: verum
end;

theorem Th21: :: FIB_NUM2:21
Fib 2 = 1
proof
Fib 2 = Fib ((0 + 1) + 1)
.= 1 by PRE_FF:1 ;
hence  Fib 2 = 1 ; ::_thesis: verum
end;

theorem Th22: :: FIB_NUM2:22
Fib 3 = 2
proof
Fib 3 = Fib ((1 + 1) + 1)
.= 2 by Th21, PRE_FF:1 ;
hence  Fib 3 = 2 ; ::_thesis: verum
end;

theorem Th23: :: FIB_NUM2:23
Fib 4 = 3
proof
Fib 4 = Fib ((2 + 1) + 1)
.= 3 by Th21, Th22, PRE_FF:1 ;
hence  Fib 4 = 3 ; ::_thesis: verum
end;

theorem Th24: :: FIB_NUM2:24
for n being Nat holds Fib (n + 2) = (Fib n) + (Fib (n + 1))
proof
defpred S1[ Nat] means  Fib ($1 + 2) = (Fib $1) + (Fib ($1 + 1));
let n be Nat; ::_thesis: Fib (n + 2) = (Fib n) + (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  S1[k] ; ::_thesis: ( not S1[k + 1] or S1[k + 2] )
assume  S1[k + 1] ; ::_thesis: S1[k + 2]
Fib ((k + 2) + 2) = Fib (((k + 2) + 1) + 1)
.= (Fib (k + 2)) + (Fib ((k + 2) + 1)) by PRE_FF:1 ;
hence  S1[k + 2] ; ::_thesis: verum
end;
Fib (0 + 2) = Fib ((0 + 1) + 1)
.= (Fib 0) + (Fib 1) by PRE_FF:1 ;
then A2: S1[ 0 ] ;
A3: S1[1] by PRE_FF:1;
 for n being Nat holds S1[n] from FIB_NUM:sch_1(A2, A3, A1);
hence  Fib (n + 2) = (Fib n) + (Fib (n + 1)) ; ::_thesis: verum
end;

theorem Th25: :: FIB_NUM2:25
for n being Nat holds Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))
proof
let n be Nat; ::_thesis: Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))
Fib (n + 3) = Fib ((n + 1) + 2)
.= (Fib ((n + 1) + 1)) + (Fib (n + 1)) by Th24
.= (Fib (n + 2)) + (Fib (n + 1)) ;
hence  Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1)) ; ::_thesis: verum
end;

theorem Th26: :: FIB_NUM2:26
for n being Nat holds Fib (n + 4) = (Fib (n + 2)) + (Fib (n + 3))
proof
let n be Nat; ::_thesis: Fib (n + 4) = (Fib (n + 2)) + (Fib (n + 3))
Fib (n + 4) = Fib (((n + 2) + 1) + 1)
.= (Fib (n + 2)) + (Fib ((n + 2) + 1)) by PRE_FF:1 ;
hence  Fib (n + 4) = (Fib (n + 2)) + (Fib (n + 3)) ; ::_thesis: verum
end;

theorem Th27: :: FIB_NUM2:27
for n being Nat holds Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))
proof
let n be Nat; ::_thesis: Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))
Fib (n + 5) = Fib (((n + 3) + 1) + 1)
.= (Fib (n + 3)) + (Fib ((n + 3) + 1)) by PRE_FF:1 ;
hence  Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4)) ; ::_thesis: verum
end;

Lm1:  for k being Nat holds Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))
proof
let k be Nat; ::_thesis: Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))
Fib ((2 * (k + 2)) + 1) = (Fib (((2 * k) + 2) + 1)) + (Fib ((((2 * k) + 2) + 1) + 1)) by PRE_FF:1
.= (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4)) ;
hence  Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4)) ; ::_thesis: verum
end;

theorem Th28: :: FIB_NUM2:28
for n being Nat holds Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1))
proof
let n be Nat; ::_thesis: Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1))
Fib (n + 3) = Fib (((n + 1) + 1) + 1)
.= (Fib (n + 1)) + (Fib (n + 2)) by PRE_FF:1 ;
hence  Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1)) ; ::_thesis: verum
end;

theorem Th29: :: FIB_NUM2:29
for n being Nat holds Fib (n + 1) = (Fib (n + 2)) - (Fib n)
proof
let n be Nat; ::_thesis: Fib (n + 1) = (Fib (n + 2)) - (Fib n)
(Fib (n + 2)) - (Fib n) = (Fib ((n + 1) + 1)) - (Fib n)
.= ((Fib n) + (Fib (n + 1))) - (Fib n) by PRE_FF:1
.= Fib (n + 1) ;
hence  Fib (n + 1) = (Fib (n + 2)) - (Fib n) ; ::_thesis: verum
end;

theorem Th30: :: FIB_NUM2:30
for n being Nat holds Fib n = (Fib (n + 2)) - (Fib (n + 1))
proof
let n be Nat; ::_thesis: Fib n = (Fib (n + 2)) - (Fib (n + 1))
(Fib (n + 2)) - (Fib (n + 1)) = ((Fib n) + (Fib (n + 1))) - (Fib (n + 1)) by Th24
.= Fib n ;
hence  Fib n = (Fib (n + 2)) - (Fib (n + 1)) ; ::_thesis: verum
end;

begin

theorem Th31: :: FIB_NUM2:31
for n being Nat holds ((Fib n) * (Fib (n + 2))) - ((Fib (n + 1)) ^2) = (- 1) |^ (n + 1)
proof
let n be Nat; ::_thesis: ((Fib n) * (Fib (n + 2))) - ((Fib (n + 1)) ^2) = (- 1) |^ (n + 1)
defpred S1[ Nat] means ((Fib $1) * (Fib ($1 + 2))) - ((Fib ($1 + 1)) ^2) = (- 1) |^ ($1 + 1);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: (Fib (k + 2)) - (Fib (k + 1)) = ((Fib (k + 1)) + (Fib k)) - (Fib (k + 1)) by Th24
.= Fib k ;
A3: (Fib (k + 3)) - (Fib (k + 1)) = ((Fib (k + 2)) + (Fib (k + 1))) - (Fib (k + 1)) by Th25
.= Fib (k + 2) ;
assume  S1[k] ; ::_thesis: S1[k + 1]
then (- 1) |^ ((k + 1) + 1) = (- 1) * (((Fib k) * (Fib (k + 2))) - ((Fib (k + 1)) ^2)) by NEWTON:6
.= ((Fib (k + 1)) * (Fib ((k + 1) + 2))) - ((Fib ((k + 1) + 1)) ^2) by A2, A3 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A4: S1[ 0 ] by NEWTON:5, PRE_FF:1;
 for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence  ((Fib n) * (Fib (n + 2))) - ((Fib (n + 1)) ^2) = (- 1) |^ (n + 1) ; ::_thesis: verum
end;

theorem :: FIB_NUM2:32
for n being non empty Element of NAT holds ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n
proof
let n be non empty Element of NAT ; ::_thesis: ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n
set a = n -' 1;
A1: n >= 1 by NAT_2:19;
then  n = (n -' 1) + 1 by XREAL_1:235;
then ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = ((Fib (n -' 1)) * (Fib ((n -' 1) + 2))) - ((Fib ((n -' 1) + 1)) ^2)
.= (- 1) |^ ((n -' 1) + 1) by Th31
.= (- 1) |^ n by A1, XREAL_1:235 ;
hence  ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n ; ::_thesis: verum
end;

theorem Th33: :: FIB_NUM2:33
tau > 0
proof
 sqrt 5 > 0 by SQUARE_1:25;
hence  tau > 0 by FIB_NUM:def_1, XREAL_1:139; ::_thesis: verum
end;

theorem Th34: :: FIB_NUM2:34
tau_bar = (- tau) to_power (- 1)
proof
A1: 1 - (sqrt 5) <> 0 by SQUARE_1:20, SQUARE_1:27;
(- tau) to_power (- 1) = (((- 1) - (sqrt 5)) / 2) #Z (- 1) by FIB_NUM:def_1, POWER:def_2
.= 1 / ((((- 1) - (sqrt 5)) / 2) #Z 1) by PREPOWER:41
.= 1 / (((- 1) - (sqrt 5)) / 2) by PREPOWER:35
.= 2 / (- (1 + (sqrt 5))) by XCMPLX_1:57
.= - (2 / (1 + (sqrt 5))) by XCMPLX_1:188
.= (- 2) / (1 + (sqrt 5)) by XCMPLX_1:187
.= ((- 2) * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))) by A1, XCMPLX_1:91
.= ((- 2) * (1 - (sqrt 5))) / ((1 ^2) - ((sqrt 5) ^2))
.= ((- 2) * (1 - (sqrt 5))) / (1 - 5) by SQUARE_1:def_2
.= tau_bar by FIB_NUM:def_2 ;
hence  tau_bar = (- tau) to_power (- 1) ; ::_thesis: verum
end;

theorem Th35: :: FIB_NUM2:35
for n being Nat holds (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n
proof
let n be Nat; ::_thesis: (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n
(- tau) to_power ((- 1) * n) = (- tau) #Z ((- 1) * n) by POWER:def_2
.= ((- tau) #Z (- 1)) #Z n by PREPOWER:45
.= (1 / ((- tau) #Z 1)) #Z n by PREPOWER:41
.= (1 / (- tau)) #Z n by PREPOWER:35
.= (1 / (- tau)) to_power n by POWER:def_2
.= ((1 / (- tau)) to_power 1) to_power n by POWER:25
.= ((1 / (- tau)) #Z 1) to_power n by POWER:def_2
.= (1 / ((- tau) #Z 1)) to_power n by PREPOWER:42
.= ((- tau) #Z (- 1)) to_power n by PREPOWER:41 ;
hence  (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n by POWER:def_2; ::_thesis: verum
end;

theorem Th36: :: FIB_NUM2:36
- (1 / tau) = tau_bar
proof
A1: 1 - (sqrt 5) <> 0 by SQUARE_1:20, SQUARE_1:27;
- (1 / tau) = - (1 * (2 / (1 + (sqrt 5)))) by FIB_NUM:def_1, XCMPLX_1:57
.= - (1 * ((2 * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))))) by A1, XCMPLX_1:91
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - ((sqrt 5) ^2))))
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - 5))) by SQUARE_1:def_2
.= (1 - (sqrt 5)) / 2 ;
hence  - (1 / tau) = tau_bar by FIB_NUM:def_2; ::_thesis: verum
end;

theorem Th37: :: FIB_NUM2:37
for r being Nat holds (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) = ((tau to_power r) - (tau_bar to_power r)) ^2
proof
let r be Nat; ::_thesis: (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) = ((tau to_power r) - (tau_bar to_power r)) ^2
 (- 1) / tau < 0 by Th33, XREAL_1:141;
then  - (1 / tau) < 0 by XCMPLX_1:187;
then A1: 1 / tau > - 0 ;
((tau to_power r) - (tau_bar to_power r)) ^2 = (((tau to_power r) ^2) - ((2 * (tau to_power r)) * ((- (1 / tau)) to_power r))) + (((- (1 / tau)) to_power r) ^2) by Th36
.= (((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((- 1) * (1 / tau)) #Z r))) + (((- (1 / tau)) to_power r) ^2) by POWER:def_2
.= (((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((- 1) #Z r) * ((1 / tau) #Z r)))) + (((- (1 / tau)) to_power r) ^2) by PREPOWER:40
.= (((tau to_power r) ^2) - ((2 * (tau to_power r)) * (((1 / tau) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau)) to_power r) ^2) by PREPOWER:36
.= (((tau to_power r) ^2) - ((2 * (tau |^ r)) * (((1 / tau) |^ r) * ((- 1) #Z r)))) + (((- (1 / tau)) to_power r) ^2) by POWER:41
.= (((tau to_power r) ^2) - ((2 * ((tau |^ r) * ((1 / tau) |^ r))) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2)
.= (((tau to_power r) ^2) - ((2 * ((tau * (1 / tau)) |^ r)) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2) by NEWTON:7
.= (((tau to_power r) ^2) - ((2 * (1 |^ r)) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2) by Th33, XCMPLX_1:106
.= (((tau to_power r) ^2) - ((2 * 1) * ((- 1) #Z r))) + (((- (1 / tau)) to_power r) ^2) by NEWTON:10
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) to_power r) ^2) by POWER:def_2
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) #Z r) ^2) by POWER:def_2
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) * (- (1 / tau))) #Z r) by PREPOWER:40
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((- (1 / tau)) ^2) |^ r) by PREPOWER:36
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((1 / tau) ^2) to_power r) by POWER:41
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + (((1 / tau) to_power r) ^2) by A1, POWER:30
.= (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) by Th33, POWER:32 ;
hence  (((tau to_power r) ^2) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2) = ((tau to_power r) - (tau_bar to_power r)) ^2 ; ::_thesis: verum
end;

theorem :: FIB_NUM2:38
for n, r being non empty Element of NAT st r <= n holds
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)
proof
set T = tau ;
set S = 1 / (sqrt 5);
A1: not - 1 is empty ;
reconsider T = tau as non empty real number by Th33;
let n, r be non empty Element of NAT ; ::_thesis: ( r <= n implies ((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2) )
assume A2: r <= n ; ::_thesis: ((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)
set Y = n -' r;
set X = n + r;
A3: (n + r) + (n -' r) = (r + n) + (n - r) by A2, XREAL_1:233
.= ((r + n) + n) - r
.= (r + (2 * n)) -' r by NAT_1:12, XREAL_1:233
.= (r -' r) + (2 * n) by NAT_D:38
.= 0 + (2 * n) by XREAL_1:232
.= 2 * n ;
A4: (n + r) - (n -' r) = (n + r) - (n - r) by A2, XREAL_1:233
.= 2 * r ;
set tyu = T to_power (- (n -' r));
set txu = T to_power (- (n + r));
set tnu = T to_power (- n);
set ty = T to_power (n -' r);
set tx = T to_power (n + r);
set tn = T to_power n;
A5: ( - T <> 0 & - 1 = (2 * (- 1)) + 1 ) ;
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((Fib (n + r)) * (Fib (n -' r))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (Fib (n -' r))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by XCMPLX_1:99
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by XCMPLX_1:99
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) * (1 / (sqrt 5)))) by XCMPLX_1:99
.= ((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- T) to_power (- 1)) to_power n))) + ((((- T) to_power (- 1)) to_power n) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by Th34
.= ((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power ((- 1) * n)))) + ((((- T) to_power (- 1)) to_power n) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by A5, Th6
.= ((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power ((- 1) * n)) ^2)) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by A5, Th6
.= ((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2)) - (((T to_power (n + r)) - ((- T) to_power ((- 1) * (n + r)))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by Th35
.= ((1 / (sqrt 5)) ^2) * (((((T to_power n) ^2) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2)) - (((T to_power (n + r)) - ((- T) to_power (- (n + r)))) * ((T to_power (n -' r)) - ((- T) to_power ((- 1) * (n -' r)))))) by Th35
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) * T) to_power (- (n -' r)))))
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) * T) to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th4
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * ((T to_power n) * (T to_power (- n)))) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2) * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r)))))
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - ((2 * 1) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2) * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) by Th10
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + (1 * ((T to_power (- n)) ^2))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (T to_power (- (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th7
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (1 / (T to_power (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th33, POWER:28
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) / (T to_power (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by XCMPLX_1:99
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th33, POWER:29
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (T to_power (- (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th33, POWER:27
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (1 / (T to_power (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th33, POWER:28
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) / (T to_power (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by XCMPLX_1:99
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th33, POWER:29
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - (((- 1) to_power ((- (n + r)) - (n -' r))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by A1, Th8
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (((- 1) to_power (- (2 * n))) * (T to_power (- (2 * n))))) by A3, Th8
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) ^2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n))))) by Th9
.= ((1 / (sqrt 5)) ^2) * ((((((((T to_power n) to_power 2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n))))) by POWER:46
.= ((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th33, POWER:33
.= ((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th11
.= ((1 / (sqrt 5)) ^2) * (((((((T to_power (2 * n)) - (T to_power (2 * n))) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th11
.= ((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - (T to_power (2 * (- n)))) by Th11
.= ((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2)) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - ((T to_power (- n)) to_power 2)) by Th33, POWER:33
.= ((1 / (sqrt 5)) ^2) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) + ((T to_power (- n)) ^2)) - ((T to_power (- n)) ^2)) by POWER:46
.= ((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power ((n -' r) + r)))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r))))) by A4
.= ((1 / (sqrt 5)) ^2) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r))))) by Th5
.= ((1 / (sqrt 5)) ^2) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + ((((- 1) to_power (2 * r)) * ((- 1) to_power (n -' r))) * (T to_power (- (2 * r))))) by Th5
.= (((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * ((- 1) to_power (2 * r))))) * ((- 1) to_power (n -' r))
.= (((1 / (sqrt 5)) ^2) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * 1))) * ((- 1) to_power (n -' r)) by Th3
.= (((1 / (sqrt 5)) ^2) * (((T to_power (2 * r)) - (2 * ((- 1) to_power r))) + (T to_power (2 * (- r))))) * ((- 1) to_power (n -' r))
.= (((1 / (sqrt 5)) ^2) * ((((T to_power r) to_power 2) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r)) by Th33, POWER:33
.= (((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r)) by POWER:46
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) to_power 2))) by Th33, POWER:33
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * ((((T to_power r) ^2) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) ^2))) by POWER:46
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2) * (((tau to_power r) - (tau_bar to_power r)) ^2)) by Th37
.= ((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) * (1 / (sqrt 5))) ^2)
.= ((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2) by XCMPLX_1:99
.= ((- 1) |^ (n -' r)) * ((((T to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2) by POWER:41
.= ((- 1) |^ (n -' r)) * ((Fib r) ^2) by FIB_NUM:7 ;
hence  ((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2) ; ::_thesis: verum
end;

theorem :: FIB_NUM2:39
for n being Nat holds ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1)
proof
let n be Nat; ::_thesis: ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1)
defpred S1[ Nat] means ((Fib $1) ^2) + ((Fib ($1 + 1)) ^2) = Fib ((2 * $1) + 1);
A1: S1[ 0 ] 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] ; ::_thesis: ( not S1[k + 1] or S1[k + 2] )
assume A4: S1[k + 1] ; ::_thesis: S1[k + 2]
Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4)) by Lm1
.= (Fib ((2 * k) + 3)) + ((Fib ((2 * k) + 3)) + (Fib ((2 * k) + 2))) by Th26
.= ((Fib ((2 * k) + 3)) + (Fib ((2 * k) + 3))) + (Fib ((2 * k) + 2))
.= (2 * (Fib ((2 * k) + 3))) + ((Fib ((2 * k) + 3)) - (Fib ((2 * k) + 1))) by Th28
.= ((2 * ((Fib (k + 1)) ^2)) + (2 * ((Fib (k + 2)) ^2))) + (((Fib (k + 2)) - (Fib k)) * ((Fib (k + 2)) + (Fib k))) by A3, A4
.= ((2 * ((Fib (k + 1)) ^2)) + (2 * ((Fib (k + 2)) ^2))) + ((Fib (k + 1)) * ((Fib (k + 2)) + (Fib k))) by Th29
.= ((Fib (k + 1)) * ((Fib (k + 1)) + ((Fib (k + 1)) + (Fib k)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + ((Fib (k + 2)) + (Fib (k + 1)))))
.= ((Fib (k + 1)) * ((Fib (k + 1)) + (Fib (k + 2)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + ((Fib (k + 2)) + (Fib (k + 1))))) by Th24
.= ((Fib (k + 1)) * ((Fib (k + 2)) + (Fib (k + 1)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + (Fib (k + 3)))) by Th25
.= ((Fib (k + 1)) * (Fib (k + 3))) + (((Fib (k + 2)) * (Fib (k + 2))) + ((Fib (k + 2)) * (Fib (k + 3)))) by Th25
.= ((Fib (k + 3)) * ((Fib (k + 1)) + (Fib (k + 2)))) + ((Fib (k + 2)) ^2)
.= ((Fib (k + 3)) ^2) + ((Fib (k + 2)) ^2) by Th25 ;
hence  S1[k + 2] ; ::_thesis: verum
end;
A5: S1[1] by Th21, PRE_FF:1;
 for n being Nat holds S1[n] from FIB_NUM:sch_1(A1, A5, A2);
hence  ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1) ; ::_thesis: verum
end;

theorem Th40: :: FIB_NUM2:40
for n being Nat
for k being non empty Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))
proof
let n be Nat; ::_thesis: for k being non empty Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))
defpred S1[ Nat] means  Fib (n + $1) = ((Fib $1) * (Fib (n + 1))) + ((Fib ($1 -' 1)) * (Fib n));
((Fib 1) * (Fib (n + 1))) + ((Fib (1 -' 1)) * (Fib n)) = (1 * (Fib (n + 1))) + (0 * (Fib n)) by PRE_FF:1, XREAL_1:232
.= Fib (n + 1) ;
then A1: S1[1] ;
A2: for m being non empty Nat st S1[m] & S1[m + 1] holds
S1[m + 2]
proof
let m be non empty Nat; ::_thesis: ( S1[m] & S1[m + 1] implies S1[m + 2] )
A3: m >= 1 by NAT_2:19;
set F2 = (Fib (m + 2)) * (Fib (n + 1));
set F1 = (Fib (n + 1)) * (Fib (m + 2));
set k = m -' 1;
assume A4: ( S1[m] & S1[m + 1] ) ; ::_thesis: S1[m + 2]
Fib (n + (m + 2)) = Fib ((n + m) + 2)
.= (Fib (n + m)) + (Fib ((n + m) + 1)) by Th24
.= (((Fib m) * (Fib (n + 1))) + ((Fib (m -' 1)) * (Fib n))) + (((Fib (m + 1)) * (Fib (n + 1))) + ((Fib (m + (1 -' 1))) * (Fib n))) by A4, NAT_D:38
.= (((Fib m) * (Fib (n + 1))) + ((Fib (m -' 1)) * (Fib n))) + (((Fib (m + 1)) * (Fib (n + 1))) + ((Fib (m + 0)) * (Fib n))) by XREAL_1:232
.= ((Fib (n + 1)) * ((Fib m) + (Fib (m + 1)))) + ((Fib n) * ((Fib (m -' 1)) + (Fib m)))
.= ((Fib (n + 1)) * (Fib (m + 2))) + ((Fib n) * ((Fib (m -' 1)) + (Fib m))) by Th24
.= ((Fib (n + 1)) * (Fib (m + 2))) + ((Fib n) * ((Fib (m -' 1)) + (Fib ((m -' 1) + 1)))) by A3, XREAL_1:235
.= ((Fib (m + 2)) * (Fib (n + 1))) + ((Fib n) * (Fib ((m -' 1) + 2))) by Th24
.= ((Fib (m + 2)) * (Fib (n + 1))) + ((Fib ((m + 2) -' 1)) * (Fib n)) by A3, NAT_D:38 ;
hence  S1[m + 2] ; ::_thesis: verum
end;
 2 -' 1 = 2 - 1 by NAT_D:39;
then A5: S1[2] by Th21, Th24, PRE_FF:1;
 for k being non empty Nat holds S1[k] from FIB_NUM2:sch_1(A1, A5, A2);
hence  for k being non empty Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n)) ; ::_thesis: verum
end;

theorem Th41: :: FIB_NUM2:41
for k being Nat
for n being non empty Element of NAT holds Fib n divides Fib (n * k)
proof
let k be Nat; ::_thesis: for n being non empty Element of NAT holds Fib n divides Fib (n * k)
let n be non empty Element of NAT ; ::_thesis: Fib n divides Fib (n * k)
defpred S1[ Nat] means  Fib n divides Fib (n * $1);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
Fib (n * (k + 1)) = Fib ((n * k) + n)
.= ((Fib n) * (Fib ((n * k) + 1))) + ((Fib (n * k)) * (Fib (n -' 1))) by Th40 ;
hence  S1[k + 1] by A2, Th12; ::_thesis: verum
end;
A3: S1[ 0 ] by NAT_D:6, PRE_FF:1;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  Fib n divides Fib (n * k) ; ::_thesis: verum
end;

theorem Th42: :: FIB_NUM2:42
for n being Nat
for k being non empty Element of NAT st k divides n holds
Fib k divides Fib n
proof
let n be Nat; ::_thesis: for k being non empty Element of NAT st k divides n holds
Fib k divides Fib n
let k be non empty Element of NAT ; ::_thesis: ( k divides n implies Fib k divides Fib n )
assume  k divides n ; ::_thesis: Fib k divides Fib n
then  ex m being Nat st n = k * m by NAT_D:def_3;
hence  Fib k divides Fib n by Th41; ::_thesis: verum
end;

theorem Th43: :: FIB_NUM2:43
for n being Nat holds Fib n <= Fib (n + 1)
proof
let n be Nat; ::_thesis: Fib n <= Fib (n + 1)
defpred S1[ Nat] means  Fib $1 <= Fib ($1 + 1);
A1: S1[ 0 ] 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] ; ::_thesis: ( not S1[k + 1] or S1[k + 2] )
assume  S1[k + 1] ; ::_thesis: S1[k + 2]
then  (Fib k) + (Fib (k + 1)) <= (Fib (k + 1)) + (Fib (k + 2)) by A3, XREAL_1:7;
then  Fib (k + 2) <= (Fib (k + 1)) + (Fib (k + 2)) by Th24;
then  Fib (k + 2) <= Fib (k + 3) by Th25;
hence  S1[k + 2] ; ::_thesis: verum
end;
A4: S1[1] by Th21, PRE_FF:1;
 for n being Nat holds S1[n] from FIB_NUM:sch_1(A1, A4, A2);
hence  Fib n <= Fib (n + 1) ; ::_thesis: verum
end;

theorem Th44: :: FIB_NUM2:44
for n being Element of NAT st n > 1 holds
Fib n < Fib (n + 1)
proof
defpred S1[ Nat] means  Fib $1 < Fib ($1 + 1);
let n be Element of NAT ; ::_thesis: ( n > 1 implies Fib n < Fib (n + 1) )
assume  n > 1 ; ::_thesis: Fib n < Fib (n + 1)
then A1: not n is trivial by NAT_2:def_1;
A2: S1[3] by Th22, Th23;
A3: for k being non trivial Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non trivial Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A4: S1[k] ; ::_thesis: ( not S1[k + 1] or S1[k + 2] )
assume  S1[k + 1] ; ::_thesis: S1[k + 2]
then  (Fib k) + (Fib (k + 1)) < (Fib (k + 1)) + (Fib (k + 2)) by A4, XREAL_1:8;
then  Fib (k + 2) < (Fib (k + 1)) + (Fib (k + 2)) by Th24;
then  Fib (k + 2) < Fib (k + 3) by Th25;
hence  S1[k + 2] ; ::_thesis: verum
end;
A5: S1[2] by Th21, Th22;
 for n being non trivial Nat holds S1[n] from FIB_NUM2:sch_2(A5, A2, A3);
hence  Fib n < Fib (n + 1) by A1; ::_thesis: verum
end;

theorem :: FIB_NUM2:45
for m, n being Nat st m >= n holds
Fib m >= Fib n
proof
let m, n be Nat; ::_thesis: ( m >= n implies Fib m >= Fib n )
assume  m >= n ; ::_thesis: Fib m >= Fib n
then consider k being Nat such that
A1: m = n + k by NAT_1:10;
 for k, n being Nat holds Fib (n + k) >= Fib n
proof
defpred S1[ Nat] means  for n being Nat holds Fib (n + $1) >= Fib n;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
let n be Nat; ::_thesis: Fib (n + (k + 1)) >= Fib n
 n + (k + 1) = (n + k) + 1 ;
then A4: Fib (n + (k + 1)) >= Fib (n + k) by Th43;
 Fib (n + k) >= Fib n by A3;
hence  Fib (n + (k + 1)) >= Fib n by A4, XXREAL_0:2; ::_thesis: verum
end;
let k, n be Nat; ::_thesis: Fib (n + k) >= Fib n
A5: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A5, A2);
hence  Fib (n + k) >= Fib n ; ::_thesis: verum
end;
hence  Fib m >= Fib n by A1; ::_thesis: verum
end;

theorem Th46: :: FIB_NUM2:46
for n, k being Nat st k > 1 & k < n holds
Fib k < Fib n
proof
let n, k be Nat; ::_thesis: ( k > 1 & k < n implies Fib k < Fib n )
assume A1: k > 1 ; ::_thesis: ( not k < n or Fib k < Fib n )
assume A2: k < n ; ::_thesis: Fib k < Fib n
then consider m being Nat such that
A3: n = k + m by NAT_1:10;
reconsider k = k as non empty Element of NAT by A1, ORDINAL1:def_12;
reconsider m = m as non empty Element of NAT by A2, A3, ORDINAL1:def_12;
 for k, m being non empty Element of NAT st k > 1 holds
Fib k < Fib (k + m)
proof
let k, m be non empty Element of NAT ; ::_thesis: ( k > 1 implies Fib k < Fib (k + m) )
assume A4: k > 1 ; ::_thesis: Fib k < Fib (k + m)
defpred S1[ Nat] means  Fib k < Fib (k + $1);
A5: for r being non empty Nat st S1[r] holds
S1[r + 1]
proof
let r be non empty Nat; ::_thesis: ( S1[r] implies S1[r + 1] )
 k + r > 0 + 1 by A4, XREAL_1:8;
then A6: Fib (k + r) < Fib ((k + r) + 1) by Th44;
assume  S1[r] ; ::_thesis: S1[r + 1]
hence  S1[r + 1] by A6, XXREAL_0:2; ::_thesis: verum
end;
A7: S1[1] by A4, Th44;
 for k being non empty Nat holds S1[k] from NAT_1:sch_10(A7, A5);
hence  Fib k < Fib (k + m) ; ::_thesis: verum
end;
then  Fib k < Fib (k + m) by A1;
hence  Fib k < Fib n by A3; ::_thesis: verum
end;

theorem Th47: :: FIB_NUM2:47
for k being Nat holds
( Fib k = 1 iff ( k = 1 or k = 2 ) )
proof
let k be Nat; ::_thesis: ( Fib k = 1 iff ( k = 1 or k = 2 ) )
 ( not Fib k = 1 or k = 1 or k = 2 )
proof
assume A1: Fib k = 1 ; ::_thesis: ( k = 1 or k = 2 )
assume that
A2: not k = 1 and
A3: not k = 2 ; ::_thesis: contradiction
A4: ( k < 2 or k > 2 ) by A3, XXREAL_0:1;
 ( k = 0 or k > 1 ) by A2, NAT_2:19;
hence  contradiction by A1, A4, Th21, Th46, PRE_FF:1; ::_thesis: verum
end;
hence  ( Fib k = 1 iff ( k = 1 or k = 2 ) ) by Th21, PRE_FF:1; ::_thesis: verum
end;

theorem Th48: :: FIB_NUM2:48
for k, n being Element of NAT st n > 1 & k <> 0 & k <> 1 holds
( Fib k = Fib n iff k = n )
proof
let k, n be Element of NAT ; ::_thesis: ( n > 1 & k <> 0 & k <> 1 implies ( Fib k = Fib n iff k = n ) )
assume that
A1: n > 1 and
A2: ( k <> 0 & k <> 1 ) ; ::_thesis: ( Fib k = Fib n iff k = n )
 not k is trivial by A2, NAT_2:def_1;
then  k >= 1 + 1 by NAT_2:29;
then A3: k > 1 by NAT_1:13;
 ( Fib k = Fib n implies k = n )
proof
assume A4: Fib k = Fib n ; ::_thesis: k = n
assume A5: k <> n ; ::_thesis: contradiction
percases ( k > n or k < n ) by A5, XXREAL_0:1;
suppose k > n ; ::_thesis: contradiction
hence  contradiction by A1, A4, Th46; ::_thesis: verum
end;
suppose k < n ; ::_thesis: contradiction
hence  contradiction by A3, A4, Th46; ::_thesis: verum
end;
end;
end;
hence  ( Fib k = Fib n iff k = n ) ; ::_thesis: verum
end;

theorem Th49: :: FIB_NUM2:49
for n being Element of NAT st n > 1 & n <> 4 & not n is prime holds
ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )
proof
let n be Element of NAT ; ::_thesis: ( n > 1 & n <> 4 & not n is prime implies ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume that
A1: n > 1 and
A2: n <> 4 ; ::_thesis: ( n is prime or ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume A3: not n is prime ; ::_thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )
percases ( n <= 1 or ex k being Nat st
( k divides n & not k = 1 & not k = n ) ) by A3, INT_2:def_4;
suppose n <= 1 ; ::_thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )
hence  ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) by A1; ::_thesis: verum
end;
suppose ex k being Nat st
( k divides n & not k = 1 & not k = n ) ; ::_thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )
then consider k being Nat such that
A4: k divides n and
A5: ( k <> 1 & k <> n ) ;
consider m being Nat such that
A6: n = k * m by A4, NAT_D:def_3;
A7: ( m divides n & m is non empty Element of NAT ) by A1, A6, NAT_D:def_3, ORDINAL1:def_12;
A8: k is non empty Element of NAT by A1, A4, INT_2:3, ORDINAL1:def_12;
A9: ( k <> 2 or m <> 2 ) by A2, A6;
 ( m <> 1 & m <> n ) by A1, A5, A6, XCMPLX_1:7;
hence  ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) by A4, A5, A8, A7, A9; ::_thesis: verum
end;
end;
end;

theorem :: FIB_NUM2:50
for n being Element of NAT st n > 1 & n <> 4 & Fib n is prime holds
n is prime
proof
let n be Element of NAT ; ::_thesis: ( n > 1 & n <> 4 & Fib n is prime implies n is prime )
assume that
A1: n > 1 and
A2: n <> 4 ; ::_thesis: ( not Fib n is prime or n is prime )
assume A3: Fib n is prime ; ::_thesis: n is prime
assume  not n is prime ; ::_thesis: contradiction
then consider k being non empty Element of NAT  such that
A4: k <> 1 and
A5: k <> 2 and
A6: k <> n and
A7: k divides n by A1, A2, Th49;
A8: Fib k <> Fib n by A1, A4, A6, Th48;
 ( Fib k <> 1 & Fib k divides Fib n ) by A4, A5, A7, Th42, Th47;
hence  contradiction by A3, A8, INT_2:def_4; ::_thesis: verum
end;

begin

definition
func FIB  ->  Function of NAT,NAT means :Def2: :: FIB_NUM2:def 2
 for k being Element of NAT holds it . k = Fib k;
existence
 ex b1 being Function of NAT,NAT st
for k being Element of NAT holds b1 . k = Fib k
proof
 ex f being Function of NAT,NAT st
for x being Element of NAT holds f . x = Fib x from FUNCT_2:sch_4();
hence  ex b1 being Function of NAT,NAT st
for k being Element of NAT holds b1 . k = Fib k ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,NAT st ( for k being Element of NAT holds b1 . k = Fib k ) & ( for k being Element of NAT holds b2 . k = Fib k ) holds
b1 = b2
proof
A1: for f1, f2 being Function of NAT,NAT st ( for x being Element of NAT holds f1 . x = Fib x ) & ( for x being Element of NAT holds f2 . x = Fib x ) holds
f1 = f2 from BINOP_2:sch_1();
let f1, f2 be Function of NAT,NAT; ::_thesis: ( ( for k being Element of NAT holds f1 . k = Fib k ) & ( for k being Element of NAT holds f2 . k = Fib k ) implies f1 = f2 )
assume  ( ( for k being Element of NAT holds f1 . k = Fib k ) & ( for k being Element of NAT holds f2 . k = Fib k ) ) ; ::_thesis: f1 = f2
hence  f1 = f2 by A1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines FIB FIB_NUM2:def_2_:_
 for b1 being Function of NAT,NAT holds
( b1 = FIB iff for k being Element of NAT holds b1 . k = Fib k );

definition
func EvenNAT  ->  Subset of NAT equals :: FIB_NUM2:def 3
 {  (2 * k) where k is Element of NAT : verum  }  ;
coherence
  {  (2 * k) where k is Element of NAT : verum  }  is Subset of NAT
proof
defpred S1[ set ] means verum;
deffunc H1( Element of NAT ) ->  Element of NAT = 2 * $1;
  {  H1(k) where k is Element of NAT : S1[k]  }  is Subset of NAT from DOMAIN_1:sch_8();
hence   {  (2 * k) where k is Element of NAT : verum  }  is Subset of NAT ; ::_thesis: verum
end;
func OddNAT  ->  Subset of NAT equals :: FIB_NUM2:def 4
 {  ((2 * k) + 1) where k is Element of NAT : verum  }  ;
coherence
  {  ((2 * k) + 1) where k is Element of NAT : verum  }  is Subset of NAT
proof
defpred S1[ set ] means verum;
deffunc H1( Element of NAT ) ->  Element of NAT = (2 * $1) + 1;
  {  H1(k) where k is Element of NAT : S1[k]  }  is Subset of NAT from DOMAIN_1:sch_8();
hence   {  ((2 * k) + 1) where k is Element of NAT : verum  }  is Subset of NAT ; ::_thesis: verum
end;
end;

:: deftheorem  defines EvenNAT FIB_NUM2:def_3_:_
 EvenNAT =  {  (2 * k) where k is Element of NAT : verum  }  ;

:: deftheorem  defines OddNAT FIB_NUM2:def_4_:_
 OddNAT =  {  ((2 * k) + 1) where k is Element of NAT : verum  }  ;

theorem Th51: :: FIB_NUM2:51
for k being Element of NAT holds
( 2 * k in EvenNAT & not (2 * k) + 1 in EvenNAT )
proof
let k be Element of NAT ; ::_thesis: ( 2 * k in EvenNAT & not (2 * k) + 1 in EvenNAT )
thus  2 * k in EvenNAT ; ::_thesis: not (2 * k) + 1 in EvenNAT
assume  (2 * k) + 1 in EvenNAT ; ::_thesis: contradiction
then  ex p being Element of NAT st (2 * k) + 1 = 2 * p ;
hence  contradiction ; ::_thesis: verum
end;

theorem Th52: :: FIB_NUM2:52
for k being Element of NAT holds
( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )
proof
let k be Element of NAT ; ::_thesis: ( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )
thus  (2 * k) + 1 in OddNAT ; ::_thesis: not 2 * k in OddNAT
assume  2 * k in OddNAT ; ::_thesis: contradiction
then  ex p being Element of NAT st 2 * k = (2 * p) + 1 ;
hence  contradiction ; ::_thesis: verum
end;

definition
let n be Element of NAT ;
func EvenFibs n ->  FinSequence of NAT  equals :: FIB_NUM2:def 5
 Prefix (FIB,(EvenNAT /\ (Seg n)));
coherence
 Prefix (FIB,(EvenNAT /\ (Seg n))) is FinSequence of NAT ;
func OddFibs n ->  FinSequence of NAT  equals :: FIB_NUM2:def 6
 Prefix (FIB,(OddNAT /\ (Seg n)));
coherence
 Prefix (FIB,(OddNAT /\ (Seg n))) is FinSequence of NAT ;
end;

:: deftheorem  defines EvenFibs FIB_NUM2:def_5_:_
 for n being Element of NAT holds EvenFibs n = Prefix (FIB,(EvenNAT /\ (Seg n)));

:: deftheorem  defines OddFibs FIB_NUM2:def_6_:_
 for n being Element of NAT holds OddFibs n = Prefix (FIB,(OddNAT /\ (Seg n)));

theorem Th53: :: FIB_NUM2:53
EvenFibs 0 = {} ;

theorem :: FIB_NUM2:54
Seq (FIB | {2}) = <*1*>
proof
reconsider H = {[2,(FIB . 2)]} as Function ;
A1: dom H = {2} by RELAT_1:9;
 dom H c= Seg 2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom H or x in Seg 2 )
assume  x in dom H ; ::_thesis: x in Seg 2
then  x = 2 by A1, TARSKI:def_1;
hence  x in Seg 2 ; ::_thesis: verum
end;
then reconsider H = H as FinSubsequence by FINSEQ_1:def_12;
 2 in NAT ;
then  2 in dom FIB by FUNCT_2:def_1;
then  Seq (FIB | {2}) = Seq H by GRFUNC_1:28
.= <*(FIB . 2)*> by PNPROC_1:3
.= <*1*> by Def2, Th21 ;
hence  Seq (FIB | {2}) = <*1*> ; ::_thesis: verum
end;

theorem Th55: :: FIB_NUM2:55
EvenFibs 2 = <*1*>
proof
now__::_thesis:_for_x_being_set_st_x_in_EvenNAT_/\_{1,2}_holds_
x_in_{2}
let x be set ; ::_thesis: ( x in EvenNAT /\ {1,2} implies b1 in {2} )
assume A1: x in EvenNAT /\ {1,2} ; ::_thesis: b1 in {2}
then A2: x in EvenNAT by XBOOLE_0:def_4;
A3: x in {1,2} by A1, XBOOLE_0:def_4;
percases ( x = (2 * 0) + 1 or x = 2 * 1 ) by A3, TARSKI:def_2;
suppose x = (2 * 0) + 1 ; ::_thesis: b1 in {2}
hence  x in {2} by A2, Th51; ::_thesis: verum
end;
suppose x = 2 * 1 ; ::_thesis: b1 in {2}
hence  x in {2} by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then A4: EvenNAT /\ {1,2} c= {2} by TARSKI:def_3;
set q = {[2,(FIB . 2)]};
reconsider q = {[2,(FIB . 2)]} as FinSubsequence by Th17;
 2 in NAT ;
then A5: 2 in dom FIB by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_{2}_holds_
x_in_EvenNAT_/\_{1,2}
let x be set ; ::_thesis: ( x in {2} implies x in EvenNAT /\ {1,2} )
assume  x in {2} ; ::_thesis: x in EvenNAT /\ {1,2}
then  x = 2 * 1 by TARSKI:def_1;
then  ( x in EvenNAT & x in {1,2} ) by TARSKI:def_2;
hence  x in EvenNAT /\ {1,2} by XBOOLE_0:def_4; ::_thesis: verum
end;
then  {2} c= EvenNAT /\ {1,2} by TARSKI:def_3;
then  EvenNAT /\ {1,2} = {2} by A4, XBOOLE_0:def_10;
then  EvenFibs 2 = Seq q by A5, FINSEQ_1:2, GRFUNC_1:28
.= <*(FIB . 2)*> by PNPROC_1:3
.= <*1*> by Def2, Th21 ;
hence  EvenFibs 2 = <*1*> ; ::_thesis: verum
end;

theorem :: FIB_NUM2:56
EvenFibs 4 = <*1,3*>
proof
now__::_thesis:_for_x_being_set_st_x_in_EvenNAT_/\_{1,2,3,4}_holds_
x_in_{2,4}
let x be set ; ::_thesis: ( x in EvenNAT /\ {1,2,3,4} implies b1 in {2,4} )
assume A1: x in EvenNAT /\ {1,2,3,4} ; ::_thesis: b1 in {2,4}
then A2: x in EvenNAT by XBOOLE_0:def_4;
A3: x in {1,2,3,4} by A1, XBOOLE_0:def_4;
percases ( x = (2 * 0) + 1 or x = 2 * 1 or x = (2 * 1) + 1 or x = 2 * 2 ) by A3, ENUMSET1:def_2;
suppose x = (2 * 0) + 1 ; ::_thesis: b1 in {2,4}
hence  x in {2,4} by A2, Th51; ::_thesis: verum
end;
suppose x = 2 * 1 ; ::_thesis: b1 in {2,4}
hence  x in {2,4} by TARSKI:def_2; ::_thesis: verum
end;
suppose x = (2 * 1) + 1 ; ::_thesis: b1 in {2,4}
hence  x in {2,4} by A2, Th51; ::_thesis: verum
end;
suppose x = 2 * 2 ; ::_thesis: b1 in {2,4}
hence  x in {2,4} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
then A4: EvenNAT /\ {1,2,3,4} c= {2,4} by TARSKI:def_3;
set q = {[2,(FIB . 2)],[4,(FIB . 4)]};
 4 in NAT ;
then A5: 4 in dom FIB by FUNCT_2:def_1;
reconsider q = {[2,(FIB . 2)],[4,(FIB . 4)]} as FinSubsequence by Th15;
 2 in NAT ;
then A6: 2 in dom FIB by FUNCT_2:def_1;
A7: FIB | ({2} \/ {4}) = (FIB | {2}) \/ (FIB | {4}) by RELAT_1:78
.= {[2,(FIB . 2)]} \/ (FIB | {4}) by A6, GRFUNC_1:28
.= {[2,(FIB . 2)]} \/ {[4,(FIB . 4)]} by A5, GRFUNC_1:28
.= q by ENUMSET1:1 ;
now__::_thesis:_for_x_being_set_st_x_in_{2,4}_holds_
x_in_EvenNAT_/\_{1,2,3,4}
let x be set ; ::_thesis: ( x in {2,4} implies x in EvenNAT /\ {1,2,3,4} )
assume A8: x in {2,4} ; ::_thesis: x in EvenNAT /\ {1,2,3,4}
then  ( x = 2 * 1 or x = 2 * 2 ) by TARSKI:def_2;
then A9: x in EvenNAT ;
 ( x = 2 or x = 4 ) by A8, TARSKI:def_2;
then  x in {1,2,3,4} by ENUMSET1:def_2;
hence  x in EvenNAT /\ {1,2,3,4} by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
then  {2,4} c= EvenNAT /\ {1,2,3,4} by TARSKI:def_3;
then  EvenNAT /\ {1,2,3,4} = {2,4} by A4, XBOOLE_0:def_10;
then  EvenFibs 4 = Seq q by A7, ENUMSET1:1, FINSEQ_3:2
.= <*(FIB . 2),(FIB . 4)*> by Th16
.= <*(Fib 2),(FIB . 4)*> by Def2
.= <*1,3*> by Def2, Th21, Th23 ;
hence  EvenFibs 4 = <*1,3*> ; ::_thesis: verum
end;

theorem Th57: :: FIB_NUM2:57
for k being Element of NAT holds (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))
proof
let k be Element of NAT ; ::_thesis: (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))
 (2 * k) + 4 = 2 * (k + 2) ;
then A1: (2 * k) + 4 in EvenNAT ;
 (2 * k) + 3 = (2 * (k + 1)) + 1 ;
then A2: {((2 * k) + 3)} misses EvenNAT by Th51, ZFMISC_1:50;
EvenNAT /\ (Seg ((2 * k) + 4)) = EvenNAT /\ (Seg (((2 * k) + 3) + 1))
.= EvenNAT /\ ((Seg ((2 * k) + 3)) \/ {((2 * k) + 4)}) by FINSEQ_1:9
.= (EvenNAT /\ (Seg ((2 * k) + 3))) \/ (EvenNAT /\ {((2 * k) + 4)}) by XBOOLE_1:23
.= (EvenNAT /\ (Seg (((2 * k) + 2) + 1))) \/ {((2 * k) + 4)} by A1, ZFMISC_1:46
.= (EvenNAT /\ ((Seg ((2 * k) + 2)) \/ {((2 * k) + 3)})) \/ {((2 * k) + 4)} by FINSEQ_1:9
.= ((EvenNAT /\ (Seg ((2 * k) + 2))) \/ (EvenNAT /\ {((2 * k) + 3)})) \/ {((2 * k) + 4)} by XBOOLE_1:23
.= ((EvenNAT /\ (Seg ((2 * k) + 2))) \/ {}) \/ {((2 * k) + 4)} by A2, XBOOLE_0:def_7
.= (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} ;
hence  (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4)) ; ::_thesis: verum
end;

theorem Th58: :: FIB_NUM2:58
for k being Element of NAT holds (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * k) + 4)))
proof
let k be Element of NAT ; ::_thesis: (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * k) + 4)))
A1: dom FIB = NAT by FUNCT_2:def_1;
FIB | (EvenNAT /\ (Seg ((2 * k) + 4))) = FIB | ((EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)}) by Th57
.= (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ (FIB | {((2 * k) + 4)}) by RELAT_1:78
.= (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} by A1, GRFUNC_1:28 ;
hence  (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * k) + 4))) ; ::_thesis: verum
end;

theorem Th59: :: FIB_NUM2:59
for n being Element of NAT holds EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
proof
defpred S1[ Element of NAT ] means  EvenFibs ((2 * $1) + 2) = (EvenFibs (2 * $1)) ^ <*(Fib ((2 * $1) + 2))*>;
let n be Element of NAT ; ::_thesis: EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
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] )
reconsider ARR = {[1,(FIB . ((2 * k) + 4))]} as FinSubsequence by Th17;
assume  S1[k] ; ::_thesis: S1[k + 1]
set LEFTk = EvenFibs ((2 * (k + 1)) + 2);
set RIGHTk = (EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*>;
reconsider RS = FIB | (EvenNAT /\ (Seg ((2 * k) + 2))) as FinSubsequence ;
set RR = ((2 * k) + 3) Shift ARR;
A2: (2 * k) + 3 > (2 * k) + 2 by XREAL_1:6;
 ( dom RS c= EvenNAT /\ (Seg ((2 * k) + 2)) & EvenNAT /\ (Seg ((2 * k) + 2)) c= Seg ((2 * k) + 2) ) by RELAT_1:58, XBOOLE_1:17;
then consider p1 being FinSequence such that
A3: RS c= p1 and
A4: dom p1 = Seg ((2 * k) + 3) by A2, Th19, XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th20;
 1 + ((2 * k) + 3) = (2 * k) + 4 ;
then A6: ((2 * k) + 3) Shift ARR = {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} by Th18;
 len p1 = (2 * k) + 3 by A4, FINSEQ_1:def_3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ (((2 * k) + 3) Shift ARR) and
A8: (Seq RS) ^ (Seq ARR) = Seq RSR by A3, A5, PNPROC_1:79;
(EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*> = (Seq (FIB | (EvenNAT /\ (Seg ((2 * k) + 2))))) ^ <*(FIB . ((2 * k) + 4))*> by Def2
.= Seq RSR by A8, PNPROC_1:3
.= EvenFibs ((2 * (k + 1)) + 2) by A7, A6, Th58 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A9: S1[ 0 ] by Th21, Th53, Th55, FINSEQ_1:34;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A1);
hence  EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*> ; ::_thesis: verum
end;

theorem Th60: :: FIB_NUM2:60
OddFibs 1 = <*1*>
proof
now__::_thesis:_for_x_being_set_st_x_in_{1}_holds_
x_in_OddNAT_/\_{1}
let x be set ; ::_thesis: ( x in {1} implies x in OddNAT /\ {1} )
assume A1: x in {1} ; ::_thesis: x in OddNAT /\ {1}
then  x = (2 * 0) + 1 by TARSKI:def_1;
then  x in OddNAT ;
hence  x in OddNAT /\ {1} by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
then A2: {1} c= OddNAT /\ {1} by TARSKI:def_3;
 1 in NAT ;
then A3: 1 in dom FIB by FUNCT_2:def_1;
 for x being set st x in OddNAT /\ {1} holds
x in {1} by XBOOLE_0:def_4;
then  OddNAT /\ {1} c= {1} by TARSKI:def_3;
then  OddNAT /\ {1} = {1} by A2, XBOOLE_0:def_10;
then  OddFibs 1 = <*(FIB . 1)*> by A3, FINSEQ_1:2, GRFUNC_1:28, PNPROC_1:3
.= <*1*> by Def2, PRE_FF:1 ;
hence  OddFibs 1 = <*1*> ; ::_thesis: verum
end;

theorem Th61: :: FIB_NUM2:61
OddFibs 3 = <*1,2*>
proof
now__::_thesis:_for_x_being_set_st_x_in_OddNAT_/\_{1,2,3}_holds_
x_in_{1,3}
let x be set ; ::_thesis: ( x in OddNAT /\ {1,2,3} implies b1 in {1,3} )
assume A1: x in OddNAT /\ {1,2,3} ; ::_thesis: b1 in {1,3}
then A2: x in OddNAT by XBOOLE_0:def_4;
A3: x in {1,2,3} by A1, XBOOLE_0:def_4;
percases ( x = (2 * 0) + 1 or x = 2 * 1 or x = (2 * 1) + 1 ) by A3, ENUMSET1:def_1;
suppose x = (2 * 0) + 1 ; ::_thesis: b1 in {1,3}
hence  x in {1,3} by TARSKI:def_2; ::_thesis: verum
end;
suppose x = 2 * 1 ; ::_thesis: b1 in {1,3}
hence  x in {1,3} by A2, Th52; ::_thesis: verum
end;
suppose x = (2 * 1) + 1 ; ::_thesis: b1 in {1,3}
hence  x in {1,3} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
then A4: OddNAT /\ {1,2,3} c= {1,3} by TARSKI:def_3;
set q = {[1,(FIB . 1)],[3,(FIB . 3)]};
 3 in NAT ;
then A5: 3 in dom FIB by FUNCT_2:def_1;
reconsider q = {[1,(FIB . 1)],[3,(FIB . 3)]} as FinSubsequence by Th15;
 1 in NAT ;
then A6: 1 in dom FIB by FUNCT_2:def_1;
A7: FIB | ({1} \/ {3}) = (FIB | {1}) \/ (FIB | {3}) by RELAT_1:78
.= {[1,(FIB . 1)]} \/ (FIB | {3}) by A6, GRFUNC_1:28
.= {[1,(FIB . 1)]} \/ {[3,(FIB . 3)]} by A5, GRFUNC_1:28
.= q by ENUMSET1:1 ;
now__::_thesis:_for_x_being_set_st_x_in_{1,3}_holds_
x_in_OddNAT_/\_{1,2,3}
let x be set ; ::_thesis: ( x in {1,3} implies x in OddNAT /\ {1,2,3} )
assume A8: x in {1,3} ; ::_thesis: x in OddNAT /\ {1,2,3}
then  ( x = (2 * 0) + 1 or x = (2 * 1) + 1 ) by TARSKI:def_2;
then A9: x in OddNAT ;
 ( x = 1 or x = 3 ) by A8, TARSKI:def_2;
then  x in {1,2,3} by ENUMSET1:def_1;
hence  x in OddNAT /\ {1,2,3} by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
then  {1,3} c= OddNAT /\ {1,2,3} by TARSKI:def_3;
then  OddNAT /\ {1,2,3} = {1,3} by A4, XBOOLE_0:def_10;
then  OddFibs 3 = Seq (FIB | ({1} \/ {3})) by ENUMSET1:1, FINSEQ_3:1
.= <*(FIB . 1),(FIB . 3)*> by A7, Th16
.= <*(Fib 1),(FIB . 3)*> by Def2
.= <*1,2*> by Def2, Th22, PRE_FF:1 ;
hence  OddFibs 3 = <*1,2*> ; ::_thesis: verum
end;

theorem Th62: :: FIB_NUM2:62
for k being Nat holds (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))
proof
let k be Nat; ::_thesis: (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))
 (2 * k) + 5 = (2 * (k + 2)) + 1 ;
then A1: (2 * k) + 5 in OddNAT ;
 (2 * k) + 4 = 2 * ((k + 1) + 1) ;
then A2: {((2 * k) + 4)} misses OddNAT by Th52, ZFMISC_1:50;
OddNAT /\ (Seg ((2 * k) + 5)) = OddNAT /\ (Seg (((2 * k) + 4) + 1))
.= OddNAT /\ ((Seg ((2 * k) + 4)) \/ {((2 * k) + 5)}) by FINSEQ_1:9
.= (OddNAT /\ (Seg (((2 * k) + 3) + 1))) \/ (OddNAT /\ {((2 * k) + 5)}) by XBOOLE_1:23
.= (OddNAT /\ ((Seg ((2 * k) + 3)) \/ {((2 * k) + 4)})) \/ (OddNAT /\ {((2 * k) + 5)}) by FINSEQ_1:9
.= ((OddNAT /\ (Seg ((2 * k) + 3))) \/ (OddNAT /\ {((2 * k) + 4)})) \/ (OddNAT /\ {((2 * k) + 5)}) by XBOOLE_1:23
.= ((OddNAT /\ (Seg ((2 * k) + 3))) \/ {}) \/ (OddNAT /\ {((2 * k) + 5)}) by A2, XBOOLE_0:def_7
.= (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} by A1, ZFMISC_1:46 ;
hence  (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5)) ; ::_thesis: verum
end;

theorem Th63: :: FIB_NUM2:63
for k being Nat holds (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))
proof
let k be Nat; ::_thesis: (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))
A1: dom FIB = NAT by FUNCT_2:def_1;
FIB | (OddNAT /\ (Seg ((2 * k) + 5))) = FIB | ((OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)}) by Th62
.= (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ (FIB | {((2 * k) + 5)}) by RELAT_1:78
.= (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} by A1, GRFUNC_1:28 ;
hence  (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5))) ; ::_thesis: verum
end;

theorem Th64: :: FIB_NUM2:64
for n being Nat holds OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>
proof
defpred S1[ Nat] means  OddFibs ((2 * $1) + 3) = (OddFibs ((2 * $1) + 1)) ^ <*(Fib ((2 * $1) + 3))*>;
let n be Nat; ::_thesis: OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider ARR = {[1,(FIB . ((2 * k) + 5))]} as FinSubsequence by Th17;
assume  S1[k] ; ::_thesis: S1[k + 1]
set LEFTk = OddFibs ((2 * (k + 1)) + 3);
set RIGHTk = (OddFibs ((2 * (k + 1)) + 1)) ^ <*(Fib ((2 * (k + 1)) + 3))*>;
reconsider RS = FIB | (OddNAT /\ (Seg ((2 * k) + 3))) as FinSubsequence ;
set RR = ((2 * k) + 4) Shift ARR;
A2: (2 * k) + 4 > (2 * k) + 3 by XREAL_1:6;
 ( dom RS c= OddNAT /\ (Seg ((2 * k) + 3)) & OddNAT /\ (Seg ((2 * k) + 3)) c= Seg ((2 * k) + 3) ) by RELAT_1:58, XBOOLE_1:17;
then consider p1 being FinSequence such that
A3: RS c= p1 and
A4: dom p1 = Seg ((2 * k) + 4) by A2, Th19, XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th20;
 1 + ((2 * k) + 4) = (2 * k) + 5 ;
then A6: ((2 * k) + 4) Shift ARR = {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} by Th18;
 len p1 = (2 * k) + 4 by A4, FINSEQ_1:def_3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ (((2 * k) + 4) Shift ARR) and
A8: (Seq RS) ^ (Seq ARR) = Seq RSR by A3, A5, PNPROC_1:79;
(OddFibs ((2 * (k + 1)) + 1)) ^ <*(Fib ((2 * (k + 1)) + 3))*> = (Seq (FIB | (OddNAT /\ (Seg ((2 * k) + 3))))) ^ <*(FIB . ((2 * k) + 5))*> by Def2
.= Seq RSR by A8, PNPROC_1:3
.= OddFibs ((2 * (k + 1)) + 3) by A7, A6, Th63 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A9: S1[ 0 ] by Th22, Th60, Th61;
 for k being Nat holds S1[k] from NAT_1:sch_2(A9, A1);
hence  OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*> ; ::_thesis: verum
end;

theorem :: FIB_NUM2:65
for n being Element of NAT holds Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 1
proof
defpred S1[ Nat] means  Sum (EvenFibs ((2 * $1) + 2)) = (Fib ((2 * $1) + 3)) - 1;
let n be Element of NAT ; ::_thesis: Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 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] )
reconsider EE = EvenFibs (2 * (k + 1)) as FinSequence of REAL ;
assume A2: S1[k] ; ::_thesis: S1[k + 1]
Sum (EvenFibs ((2 * (k + 1)) + 2)) = Sum ((EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*>) by Th59
.= (Sum EE) + (Fib ((2 * (k + 1)) + 2)) by RVSUM_1:74
.= ((Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))) - 1 by A2
.= (Fib ((2 * k) + 5)) - 1 by Th27 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th22, Th55, RVSUM_1:73;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 1 ; ::_thesis: verum
end;

theorem :: FIB_NUM2:66
for n being Nat holds Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2)
proof
defpred S1[ Nat] means  Sum (OddFibs ((2 * $1) + 1)) = Fib ((2 * $1) + 2);
let n be Nat; ::_thesis: Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2)
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider EE = OddFibs ((2 * k) + 1) as FinSequence of REAL ;
assume A2: S1[k] ; ::_thesis: S1[k + 1]
Sum (OddFibs ((2 * (k + 1)) + 1)) = Sum ((OddFibs ((2 * k) + 1)) ^ <*(Fib ((2 * k) + 3))*>) by Th64
.= (Sum EE) + (Fib ((2 * k) + 3)) by RVSUM_1:74
.= Fib ((2 * k) + 4) by A2, Th26 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th21, Th60, RVSUM_1:73;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2) ; ::_thesis: verum
end;

begin

theorem Th67: :: FIB_NUM2:67
for n being Element of NAT holds Fib n, Fib (n + 1) are_relative_prime
proof
let n be Element of NAT ; ::_thesis: Fib n, Fib (n + 1) are_relative_prime
A1: n,n + 1 are_relative_prime by PEPIN:1;
(Fib n) gcd (Fib (n + 1)) = Fib (n gcd (n + 1)) by FIB_NUM:5
.= 1 by A1, INT_2:def_3, PRE_FF:1 ;
hence  Fib n, Fib (n + 1) are_relative_prime by INT_2:def_3; ::_thesis: verum
end;

theorem Th68: :: FIB_NUM2:68
for n being non empty Nat
for m being Nat st m <> 1 & m divides Fib n holds
not m divides Fib (n -' 1)
proof
let n be non empty Nat; ::_thesis: for m being Nat st m <> 1 & m divides Fib n holds
not m divides Fib (n -' 1)
let m be Nat; ::_thesis: ( m <> 1 & m divides Fib n implies not m divides Fib (n -' 1) )
assume A1: m <> 1 ; ::_thesis: ( not m divides Fib n or not m divides Fib (n -' 1) )
assume A2: m divides Fib n ; ::_thesis: not m divides Fib (n -' 1)
 n >= 1 by NAT_2:19;
then  n = (n -' 1) + 1 by XREAL_1:235;
then  Fib (n -' 1), Fib n are_relative_prime by Th67;
then A3: (Fib (n -' 1)) gcd (Fib n) = 1 by INT_2:def_3;
assume  m divides Fib (n -' 1) ; ::_thesis: contradiction
then  m divides 1 by A2, A3, NAT_D:def_5;
hence  contradiction by A1, WSIERP_1:15; ::_thesis: verum
end;

theorem :: FIB_NUM2:69
for m being Nat
for n being non empty Nat st m is prime & n is prime & m divides Fib n holds
for r being Nat st r < n & r <> 0 holds
not m divides Fib r
proof
let m be Nat; ::_thesis: for n being non empty Nat st m is prime & n is prime & m divides Fib n holds
for r being Nat st r < n & r <> 0 holds
not m divides Fib r
let n be non empty Nat; ::_thesis: ( m is prime & n is prime & m divides Fib n implies for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
assume A1: m is prime ; ::_thesis: ( not n is prime or not m divides Fib n or for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
defpred S1[ Element of NAT ] means ( $1 < n & $1 <> 0 & m divides Fib $1 );
assume A2: n is prime ; ::_thesis: ( not m divides Fib n or for r being Nat st r < n & r <> 0 holds
not m divides Fib r )
reconsider C =  {  x where x is Element of NAT : S1[x]  }  as Subset of NAT from DOMAIN_1:sch_7();
assume A3: m divides Fib n ; ::_thesis: for r being Nat st r < n & r <> 0 holds
not m divides Fib r
assume A4: ex r being Nat st
( r < n & r <> 0 & m divides Fib r ) ; ::_thesis: contradiction
 C is non empty Subset of NAT
proof
consider r being Nat such that
A5: ( r < n & r <> 0 & m divides Fib r ) by A4;
 r in NAT by ORDINAL1:def_12;
then  r in C by A5;
hence  C is non empty Subset of NAT ; ::_thesis: verum
end;
then reconsider C = C as non empty Subset of NAT ;
set r = min C;
defpred S2[ Nat] means ( m divides Fib (n -' ((min C) * ($1 + 1))) & min C <= n / ($1 + 2) );
 min C in C by XXREAL_2:def_7;
then A6: ex r9 being Element of NAT st
( r9 = min C & S1[r9] ) ;
then A7: n -' (min C) < n by NAT_2:9;
 m <> 1 by A1, INT_2:def_4;
then A8: not m divides Fib ((min C) -' 1) by A6, Th68;
A9: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
A10: m divides (Fib (min C)) * (Fib ((n -' ((k + 2) * (min C))) + 1)) by A6, NAT_D:9;
A11: n - ((min C) * (k + 2)) <> 0
proof
assume A12: n - ((min C) * (k + 2)) = 0 ; ::_thesis: contradiction
then A13: ( min C divides n & k + 2 divides n ) by NAT_D:def_3;
percases ( ( min C = 1 & k + 2 = n ) or ( min C = 1 & k + 2 = 1 ) or ( min C = n & k + 2 = n ) or ( min C = n & k + 2 = 1 ) ) by A2, A13, INT_2:def_4;
suppose ( min C = 1 & k + 2 = n ) ; ::_thesis: contradiction
then  m = 1 by A6, PRE_FF:1, WSIERP_1:15;
hence  contradiction by A1, INT_2:def_4; ::_thesis: verum
end;
suppose ( min C = 1 & k + 2 = 1 ) ; ::_thesis: contradiction
hence  contradiction by A2, A12, INT_2:def_4; ::_thesis: verum
end;
suppose ( min C = n & k + 2 = n ) ; ::_thesis: contradiction
hence  contradiction by A6; ::_thesis: verum
end;
suppose ( min C = n & k + 2 = 1 ) ; ::_thesis: contradiction
hence  contradiction by A6; ::_thesis: verum
end;
end;
end;
 - (min C) < - 0 by A6, XREAL_1:24;
then  (- (min C)) * (k + 2) < 0 * (k + 2) by XREAL_1:68;
then  (- ((min C) * (k + 2))) + n < 0 + n by XREAL_1:6;
then A14: n -' ((k + 2) * (min C)) < n by A11, XREAL_0:def_2;
assume A15: S2[k] ; ::_thesis: S2[k + 1]
then A16: (min C) * (k + 2) <= (n / (k + 2)) * (k + 2) by XREAL_1:64;
then A17: (min C) * (k + 2) <= n by XCMPLX_1:87;
then A18: n - ((min C) * (k + 2)) >= ((min C) * (k + 2)) - ((min C) * (k + 2)) by XREAL_1:9;
then A19: n -' ((k + 2) * (min C)) <> 0 by A11, XREAL_0:def_2;
 (min C) + ((min C) * (k + 1)) <= n by A16, XCMPLX_1:87;
then  (min C) * (k + 1) < n by A6, Th14;
then A20: ((k + 1) * (min C)) - ((k + 1) * (min C)) < n - ((k + 1) * (min C)) by XREAL_1:9;
 (n - ((k + 1) * (min C))) - (min C) > 0 by A11, A18;
then  (n -' ((k + 1) * (min C))) - (min C) > 0 by A20, XREAL_0:def_2;
then A21: (n -' ((k + 1) * (min C))) -' (min C) = (n -' ((k + 1) * (min C))) - (min C) by XREAL_0:def_2
.= (n - ((k + 1) * (min C))) - (min C) by A20, XREAL_0:def_2
.= n -' ((k + 2) * (min C)) by A18, XREAL_0:def_2 ;
 n - ((min C) * (k + 1)) >= ((min C) + ((min C) * (k + 1))) - ((min C) * (k + 1)) by A17, XREAL_1:9;
then  min C <= n -' ((min C) * (k + 1)) by XREAL_0:def_2;
then  Fib (n -' ((k + 1) * (min C))) = Fib ((n -' ((k + 2) * (min C))) + (min C)) by A21, XREAL_1:235
.= ((Fib (min C)) * (Fib ((n -' ((k + 2) * (min C))) + 1))) + ((Fib ((min C) -' 1)) * (Fib (n -' ((k + 2) * (min C))))) by A6, Th40 ;
then A22: m divides (Fib ((min C) -' 1)) * (Fib (n -' ((k + 2) * (min C)))) by A15, A10, NAT_D:10;
then  m divides Fib (n -' ((k + 2) * (min C))) by A1, A8, NEWTON:80;
then  n -' ((k + 2) * (min C)) in C by A19, A14;
then  n -' ((k + 2) * (min C)) >= min C by XXREAL_2:def_7;
then  n >= (min C) + ((k + 2) * (min C)) by A17, NAT_D:54;
then  n * (1 / ((1 + k) + 2)) >= ((min C) * ((1 + k) + 2)) * (1 / ((1 + k) + 2)) by XREAL_1:64;
then  n * (1 / ((1 + k) + 2)) >= ((min C) * ((1 + k) + 2)) / ((1 + k) + 2) by XCMPLX_1:99;
then  n / ((1 + k) + 2) >= ((min C) * ((1 + k) + 2)) / ((1 + k) + 2) by XCMPLX_1:99;
hence  S2[k + 1] by A1, A8, A22, NEWTON:80, XCMPLX_1:89; ::_thesis: verum
end;
 (min C) - (min C) < n - (min C) by A6, XREAL_1:9;
then A23: n -' (min C) <> 0 by XREAL_0:def_2;
A24: m divides (Fib (min C)) * (Fib ((n -' (min C)) + 1)) by A6, NAT_D:9;
Fib n = Fib ((n -' (min C)) + (min C)) by A6, XREAL_1:235
.= ((Fib (min C)) * (Fib ((n -' (min C)) + 1))) + ((Fib ((min C) -' 1)) * (Fib (n -' (min C)))) by A6, Th40 ;
then A25: m divides (Fib ((min C) -' 1)) * (Fib (n -' (min C))) by A3, A24, NAT_D:10;
then  m divides Fib (n -' (min C)) by A1, A8, NEWTON:80;
then  n -' (min C) in C by A7, A23;
then  n -' (min C) >= min C by XXREAL_2:def_7;
then  n >= (min C) + (min C) by A6, NAT_D:54;
then  n / 2 >= (2 * (min C)) / 2 by XREAL_1:72;
then A26: S2[ 0 ] by A1, A8, A25, NEWTON:80;
 for k being Nat holds S2[k] from NAT_1:sch_2(A26, A9);
then  ( n / (n + 2) < 1 & min C <= n / (n + 2) ) by XREAL_1:29, XREAL_1:191;
then  min C < 1 + 0 by XXREAL_0:2;
hence  contradiction by A6, NAT_1:13; ::_thesis: verum
end;

begin

theorem :: FIB_NUM2:70
for n being non empty Element of NAT holds {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2) + ((Fib (n + 2)) ^2))} is Pythagorean_triple
proof
let n be non empty Element of NAT ; ::_thesis: {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2) + ((Fib (n + 2)) ^2))} is Pythagorean_triple
(((Fib n) * (Fib (n + 3))) ^2) + (((2 * (Fib (n + 1))) * (Fib (n + 2))) ^2) = (((Fib n) ^2) * ((Fib (n + 3)) ^2)) + (((2 * 2) * ((Fib (n + 1)) ^2)) * ((Fib (n + 2)) ^2))
.= (((Fib n) ^2) * (((Fib (n + 2)) + (Fib (n + 1))) ^2)) + ((4 * ((Fib (n + 1)) ^2)) * ((Fib (n + 2)) ^2)) by Th25
.= ((((Fib (n + 2)) - (Fib (n + 1))) ^2) * (((Fib (n + 2)) + (Fib (n + 1))) ^2)) + ((4 * ((Fib (n + 1)) ^2)) * ((Fib (n + 2)) ^2)) by Th30
.= (((Fib (n + 1)) ^2) + ((Fib (n + 2)) ^2)) ^2 ;
hence  {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2) + ((Fib (n + 2)) ^2))} is Pythagorean_triple by PYTHTRIP:def_4; ::_thesis: verum
end;