let a, b be Element of INT ; :: thesis: ( |.a.| > |.b.| & b > 1 implies ex A, B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded ) )

assume ASKARI: ( |.a.| > |.b.| & b > 1 ) ; :: thesis: ex A, B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

consider A, B being sequence of NAT such that

L1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Nat : B . i = 0 } ) ) by NTALGO_1:def 1;

consider n being Element of NAT such that

CC1: ( n = min* { i where i is Nat : B . i = 0 } & ALGO_GCD (a,b) = A . n ) by L1;

Lm5: for a, b being Element of INT

for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

then n in { i where i is Nat : B . i = 0 } by NAT_1:def 1, CC1;

then ex i being Nat st

( n = i & B . i = 0 ) ;

then LNNZ: n <> 0 by ASKARI, L1;

then NIZ: n - 1 is Nat by NAT_1:20;

LX1: B . (n - 1) <> 0

B . i > 0

B . (i + 1) <= (B . i) - 1_{1}[ Nat] means ( $1 <= n implies B . $1 <= (B . 0) - $1 );

A6: S_{1}[ 0 ]
;

A7: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A6, A7);

LC0P: n <= B . 0

.= B . (n - 1) by L1, NIZ ;

then ASTS: 0 + 1 <= A . n by INT_1:7, LX1;

LKA1: for j being Nat st j < n holds

A . (j + 1) < A . j

(A . (i + 2)) + (A . (i + 1)) <= A . i

Fib (i + 2) <= A . (n - i)

n - 1 < n - 0 by XREAL_1:15;

then G1P: Fib (m + 2) <= A . (n - m) by LEMM1;

G2P: A . 1 = A . (0 + 1)

.= |.b.| by L1 ;

0 + 1 <= n by INT_1:7, LNNZ;

then HYY1: 1 < n + 1 by NAT_1:13;

CLAME: n <= 5 * [/(log (10,|.b.|))\]

set nb = |.b.|;

LC2P: C . |.b.| = |.b.| to_power 1 by ASYMPT_1:def 3, ASKARI;

LC1P: seq_n^ 1 in Big_Oh (seq_n^ 1) by ASYMPT_0:10;

take A ; :: thesis: ex B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take B ; :: thesis: ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take C ; :: thesis: ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take n ; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

thus ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded ) by L1, LC1P, LC2P, CC1, NTALGO_1:2, CLAME, G2P, G1P, LC0P; :: thesis: verum

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded ) )

assume ASKARI: ( |.a.| > |.b.| & b > 1 ) ; :: thesis: ex A, B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

consider A, B being sequence of NAT such that

L1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Nat : B . i = 0 } ) ) by NTALGO_1:def 1;

consider n being Element of NAT such that

CC1: ( n = min* { i where i is Nat : B . i = 0 } & ALGO_GCD (a,b) = A . n ) by L1;

Lm5: for a, b being Element of INT

for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

proof

KL11:
{ i where i is Nat : B . i = 0 } is non empty Subset of NAT
by L1, Lm5;
let a, b be Element of INT ; :: thesis: for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Nat : B . i = 0 } is non empty Subset of NAT )

assume A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: { i where i is Nat : B . i = 0 } is non empty Subset of NAT

A2: for x being object st x in { i where i is Nat : B . i = 0 } holds

x in NAT

A11: B . m0 = 0 ;

m0 in { i where i is Nat : B . i = 0 } by A11;

hence { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A2, TARSKI:def 3; :: thesis: verum

end;( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Nat : B . i = 0 } is non empty Subset of NAT )

assume A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: { i where i is Nat : B . i = 0 } is non empty Subset of NAT

A2: for x being object st x in { i where i is Nat : B . i = 0 } holds

x in NAT

proof

ex m0 being Nat st B . m0 = 0
let x be object ; :: thesis: ( x in { i where i is Nat : B . i = 0 } implies x in NAT )

assume x in { i where i is Nat : B . i = 0 } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & B . i = 0 ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume x in { i where i is Nat : B . i = 0 } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & B . i = 0 ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

proof

then consider m0 being Nat such that
assume A3:
for m0 being Nat holds not B . m0 = 0
; :: thesis: contradiction

A4: for i being Nat holds B . (i + 1) <= (B . i) - 1_{1}[ Nat] means B . $1 <= (B . 0) - $1;

A6: S_{1}[ 0 ]
;

A7: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A6, A7);

then B . (B . 0) <= (B . 0) - (B . 0) ;

hence contradiction by A3, NAT_1:14; :: thesis: verum

end;A4: for i being Nat holds B . (i + 1) <= (B . i) - 1

proof

defpred S
let i be Nat; :: thesis: B . (i + 1) <= (B . i) - 1

A5: B . i <> 0 by A3;

B . (i + 1) = (A . i) mod (B . i) by A1;

then (B . (i + 1)) + 1 <= B . i by NAT_1:13, A5, INT_1:58;

then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;

hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum

end;A5: B . i <> 0 by A3;

B . (i + 1) = (A . i) mod (B . i) by A1;

then (B . (i + 1)) + 1 <= B . i by NAT_1:13, A5, INT_1:58;

then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;

hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum

A6: S

A7: for i being Nat st S

S

proof

A10:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A8: S_{1}[i]
; :: thesis: S_{1}[i + 1]

A9: B . (i + 1) <= (B . i) - 1 by A4;

(B . i) - 1 <= ((B . 0) - i) - 1 by A8, XREAL_1:9;

hence S_{1}[i + 1]
by A9, XXREAL_0:2; :: thesis: verum

end;assume A8: S

A9: B . (i + 1) <= (B . i) - 1 by A4;

(B . i) - 1 <= ((B . 0) - i) - 1 by A8, XREAL_1:9;

hence S

then B . (B . 0) <= (B . 0) - (B . 0) ;

hence contradiction by A3, NAT_1:14; :: thesis: verum

A11: B . m0 = 0 ;

m0 in { i where i is Nat : B . i = 0 } by A11;

hence { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A2, TARSKI:def 3; :: thesis: verum

then n in { i where i is Nat : B . i = 0 } by NAT_1:def 1, CC1;

then ex i being Nat st

( n = i & B . i = 0 ) ;

then LNNZ: n <> 0 by ASKARI, L1;

then NIZ: n - 1 is Nat by NAT_1:20;

LX1: B . (n - 1) <> 0

proof

B11:
for i being Nat st i < n holds
assume
B . (n - 1) = 0
; :: thesis: contradiction

then n - 1 in { i where i is Nat : B . i = 0 } by NIZ;

then n <= n - 1 by CC1, NAT_1:def 1, KL11;

then n < (n - 1) + 1 by XREAL_1:145;

hence contradiction ; :: thesis: verum

end;then n - 1 in { i where i is Nat : B . i = 0 } by NIZ;

then n <= n - 1 by CC1, NAT_1:def 1, KL11;

then n < (n - 1) + 1 by XREAL_1:145;

hence contradiction ; :: thesis: verum

B . i > 0

proof

A4:
for i being Nat st i < n holds
let i be Nat; :: thesis: ( i < n implies B . i > 0 )

assume WHHO: i < n ; :: thesis: B . i > 0

assume 0 >= B . i ; :: thesis: contradiction

then B . i = 0 ;

then i in { i where i is Nat : B . i = 0 } ;

hence contradiction by WHHO, CC1, NAT_1:def 1, KL11; :: thesis: verum

end;assume WHHO: i < n ; :: thesis: B . i > 0

assume 0 >= B . i ; :: thesis: contradiction

then B . i = 0 ;

then i in { i where i is Nat : B . i = 0 } ;

hence contradiction by WHHO, CC1, NAT_1:def 1, KL11; :: thesis: verum

B . (i + 1) <= (B . i) - 1

proof

defpred S
let i be Nat; :: thesis: ( i < n implies B . (i + 1) <= (B . i) - 1 )

assume i < n ; :: thesis: B . (i + 1) <= (B . i) - 1

then A5: B . i <> 0 by B11;

B . (i + 1) = (A . i) mod (B . i) by L1;

then (B . (i + 1)) + 1 <= B . i by NAT_1:13, A5, INT_1:58;

then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;

hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum

end;assume i < n ; :: thesis: B . (i + 1) <= (B . i) - 1

then A5: B . i <> 0 by B11;

B . (i + 1) = (A . i) mod (B . i) by L1;

then (B . (i + 1)) + 1 <= B . i by NAT_1:13, A5, INT_1:58;

then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;

hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum

A6: S

A7: for i being Nat st S

S

proof

A70:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A8: S_{1}[i]
; :: thesis: S_{1}[i + 1]

assume B8: i + 1 <= n ; :: thesis: B . (i + 1) <= (B . 0) - (i + 1)

then i < n by XXREAL_0:2, NAT_1:16;

then A9: B . (i + 1) <= (B . i) - 1 by A4;

(B . i) - 1 <= ((B . 0) - i) - 1 by A8, B8, XXREAL_0:2, NAT_1:16, XREAL_1:9;

hence B . (i + 1) <= (B . 0) - (i + 1) by A9, XXREAL_0:2; :: thesis: verum

end;assume A8: S

assume B8: i + 1 <= n ; :: thesis: B . (i + 1) <= (B . 0) - (i + 1)

then i < n by XXREAL_0:2, NAT_1:16;

then A9: B . (i + 1) <= (B . i) - 1 by A4;

(B . i) - 1 <= ((B . 0) - i) - 1 by A8, B8, XXREAL_0:2, NAT_1:16, XREAL_1:9;

hence B . (i + 1) <= (B . 0) - (i + 1) by A9, XXREAL_0:2; :: thesis: verum

LC0P: n <= B . 0

proof

A . n =
A . ((n - 1) + 1)
assume H1P:
n > B . 0
; :: thesis: contradiction

H2: B . n <= (B . 0) - n by A70;

(B . 0) - n < n - n by H1P, XREAL_1:9;

hence contradiction by H2; :: thesis: verum

end;H2: B . n <= (B . 0) - n by A70;

(B . 0) - n < n - n by H1P, XREAL_1:9;

hence contradiction by H2; :: thesis: verum

.= B . (n - 1) by L1, NIZ ;

then ASTS: 0 + 1 <= A . n by INT_1:7, LX1;

LKA1: for j being Nat st j < n holds

A . (j + 1) < A . j

proof

ZM:
( 1 < n implies Fib 3 <= A . (n - 1) )
let j be Nat; :: thesis: ( j < n implies A . (j + 1) < A . j )

assume CCC1: j < n ; :: thesis: A . (j + 1) < A . j

end;assume CCC1: j < n ; :: thesis: A . (j + 1) < A . j

now :: thesis: ( ( 0 < j & A . (j + 1) < A . j ) or ( j = 0 & A . (j + 1) < A . j ) )end;

hence
A . (j + 1) < A . j
; :: thesis: verumper cases
( 0 < j or j = 0 )
;

end;

case
0 < j
; :: thesis: A . (j + 1) < A . j

then
0 + 1 <= j
by INT_1:7;

then j - 1 in NAT by INT_1:5;

then reconsider k = j - 1 as Nat ;

AME1: ( A . (k + 1) = B . k & A . ((k + 1) + 1) = B . (k + 1) ) by L1;

j - 1 < n by CCC1, XREAL_1:51;

then B . (k + 1) <= (B . k) - 1 by A4;

then (B . (k + 1)) + 1 <= ((B . k) - 1) + 1 by XREAL_1:6;

hence A . (j + 1) < A . j by AME1, NAT_1:13; :: thesis: verum

end;then j - 1 in NAT by INT_1:5;

then reconsider k = j - 1 as Nat ;

AME1: ( A . (k + 1) = B . k & A . ((k + 1) + 1) = B . (k + 1) ) by L1;

j - 1 < n by CCC1, XREAL_1:51;

then B . (k + 1) <= (B . k) - 1 by A4;

then (B . (k + 1)) + 1 <= ((B . k) - 1) + 1 by XREAL_1:6;

hence A . (j + 1) < A . j by AME1, NAT_1:13; :: thesis: verum

proof

TRMT:
for i being Nat st 0 < i & i < n holds
assume
1 < n
; :: thesis: Fib 3 <= A . (n - 1)

then 1 - 1 < n - 1 by XREAL_1:9;

then PZ1: ( 0 < n - 1 & n - 1 is Nat ) by LNNZ, NAT_1:20;

n - 1 < n - 0 by XREAL_1:15;

then A . ((n - 1) + 1) < A . (n - 1) by LKA1, PZ1;

then 1 < A . (n - 1) by ASTS, XXREAL_0:2;

then 1 + 1 <= A . (n - 1) by INT_1:7;

hence Fib 3 <= A . (n - 1) by FIB_NUM2:22; :: thesis: verum

end;then 1 - 1 < n - 1 by XREAL_1:9;

then PZ1: ( 0 < n - 1 & n - 1 is Nat ) by LNNZ, NAT_1:20;

n - 1 < n - 0 by XREAL_1:15;

then A . ((n - 1) + 1) < A . (n - 1) by LKA1, PZ1;

then 1 < A . (n - 1) by ASTS, XXREAL_0:2;

then 1 + 1 <= A . (n - 1) by INT_1:7;

hence Fib 3 <= A . (n - 1) by FIB_NUM2:22; :: thesis: verum

(A . (i + 2)) + (A . (i + 1)) <= A . i

proof

LEMM1:
for i being Nat st i < n holds
let i be Nat; :: thesis: ( 0 < i & i < n implies (A . (i + 2)) + (A . (i + 1)) <= A . i )

assume LP11: ( 0 < i & i < n ) ; :: thesis: (A . (i + 2)) + (A . (i + 1)) <= A . i

then B . (i + 1) <= (B . i) - 1 by A4;

then LK1: B . (i + 1) <= (A . (i + 1)) - 1 by L1;

LX: A . (i + 1) <= A . i by LP11, LKA1;

(A . i) mod (B . i) <= (A . (i + 1)) - 1 by L1, LK1;

then (A . i) mod (A . (i + 1)) <= (A . (i + 1)) - 1 by L1;

then CLL1: ((A . i) mod (A . (i + 1))) + 0 < ((A . (i + 1)) - 1) + 1 by XREAL_1:8;

then (A . i) div (A . (i + 1)) >= 1 by NAT_2:13, LX;

then LCP: (A . (i + 2)) + (A . (i + 1)) <= (A . (i + 2)) + (((A . i) div (A . (i + 1))) * (A . (i + 1))) by XREAL_1:6, XREAL_1:151;

A . (i + 2) = A . ((i + 1) + 1)

.= B . (i + 1) by L1

.= (A . i) mod (B . i) by L1

.= (A . i) mod (A . (i + 1)) by L1

.= (A . i) - (((A . i) div (A . (i + 1))) * (A . (i + 1))) by INT_1:def 10, CLL1 ;

hence (A . (i + 2)) + (A . (i + 1)) <= A . i by LCP; :: thesis: verum

end;assume LP11: ( 0 < i & i < n ) ; :: thesis: (A . (i + 2)) + (A . (i + 1)) <= A . i

then B . (i + 1) <= (B . i) - 1 by A4;

then LK1: B . (i + 1) <= (A . (i + 1)) - 1 by L1;

LX: A . (i + 1) <= A . i by LP11, LKA1;

(A . i) mod (B . i) <= (A . (i + 1)) - 1 by L1, LK1;

then (A . i) mod (A . (i + 1)) <= (A . (i + 1)) - 1 by L1;

then CLL1: ((A . i) mod (A . (i + 1))) + 0 < ((A . (i + 1)) - 1) + 1 by XREAL_1:8;

then (A . i) div (A . (i + 1)) >= 1 by NAT_2:13, LX;

then LCP: (A . (i + 2)) + (A . (i + 1)) <= (A . (i + 2)) + (((A . i) div (A . (i + 1))) * (A . (i + 1))) by XREAL_1:6, XREAL_1:151;

A . (i + 2) = A . ((i + 1) + 1)

.= B . (i + 1) by L1

.= (A . i) mod (B . i) by L1

.= (A . i) mod (A . (i + 1)) by L1

.= (A . i) - (((A . i) div (A . (i + 1))) * (A . (i + 1))) by INT_1:def 10, CLL1 ;

hence (A . (i + 2)) + (A . (i + 1)) <= A . i by LCP; :: thesis: verum

Fib (i + 2) <= A . (n - i)

proof

reconsider m = n - 1 as Nat by LNNZ, NAT_1:20;
defpred S_{2}[ Nat] means ( $1 < n implies Fib ($1 + 2) <= A . (n - $1) );

0 + 1 <= n by INT_1:7, LNNZ;

then HYY1: 1 < n + 1 by NAT_1:13;

S_{2}[i] ) holds

S_{2}[k]

S_{2}[k]
from NAT_1:sch 9(A1);

for i being Nat st i <= n holds

S_{2}[i]

Fib (i + 2) <= A . (n - i) ; :: thesis: verum

end;0 + 1 <= n by INT_1:7, LNNZ;

then HYY1: 1 < n + 1 by NAT_1:13;

LLLCT: now :: thesis: ( ( n = 1 & S_{2}[1] ) or ( 1 < n & S_{2}[1] ) )end;

A1:
for k being Nat st k >= 2 & ( for i being Nat st i >= 2 & i < k holds S

S

proof

A10:
for k being Nat st k >= 2 holds
let k be Nat; :: thesis: ( k >= 2 & ( for i being Nat st i >= 2 & i < k holds

S_{2}[i] ) implies S_{2}[k] )

assume A2: k >= 2 ; :: thesis: ( ex i being Nat st

( i >= 2 & i < k & not S_{2}[i] ) or S_{2}[k] )

assume A3: for i being Nat st i >= 2 & i < k holds

S_{2}[i]
; :: thesis: S_{2}[k]

AU4: for i being Nat st i < k holds

S_{2}[i]

then reconsider x = k - 1 as Nat ;

k - 2 in NAT by A2, INT_1:5;

then reconsider y = k - 2 as Nat ;

LLZZ: ( x < k & y < k ) by XREAL_1:44;

LLZ: ( S_{2}[x] & S_{2}[y] )
by AU4, XREAL_1:44;

_{2}[k]
; :: thesis: verum

end;S

assume A2: k >= 2 ; :: thesis: ( ex i being Nat st

( i >= 2 & i < k & not S

assume A3: for i being Nat st i >= 2 & i < k holds

S

AU4: for i being Nat st i < k holds

S

proof

k - 1 in NAT
by INT_1:5, A2, XXREAL_0:2;
let i be Nat; :: thesis: ( i < k implies S_{2}[i] )

assume NNNH: i < k ; :: thesis: S_{2}[i]

_{2}[i]
; :: thesis: verum

end;assume NNNH: i < k ; :: thesis: S

now :: thesis: ( ( i = 0 & S_{2}[i] ) or ( i = 1 & S_{2}[i] ) or ( 2 <= i & S_{2}[i] ) )end;

hence
Sthen reconsider x = k - 1 as Nat ;

k - 2 in NAT by A2, INT_1:5;

then reconsider y = k - 2 as Nat ;

LLZZ: ( x < k & y < k ) by XREAL_1:44;

LLZ: ( S

now :: thesis: ( ( k < n & S_{2}[k] ) or ( n <= k & S_{2}[k] ) )end;

hence
Sper cases
( k < n or n <= k )
;

end;

case LLAQ:
k < n
; :: thesis: S_{2}[k]

then
n - k in NAT
by INT_1:5;

then reconsider z = n - k as Nat ;

ZEE: z < n by XREAL_1:231, A2;

_{2}[k]
; :: thesis: verum

end;then reconsider z = n - k as Nat ;

ZEE: z < n by XREAL_1:231, A2;

now :: thesis: ( ( z = 0 & S_{2}[k] ) or ( 0 < z & S_{2}[k] ) )end;

hence
Sper cases
( z = 0 or 0 < z )
;

end;

case
0 < z
; :: thesis: S_{2}[k]

then SDD:
(A . (z + 2)) + (A . (z + 1)) <= A . z
by TRMT, ZEE;

LYY: (Fib (x + 2)) + (Fib (y + 2)) <= (A . (z + 2)) + (A . (z + 1)) by XREAL_1:7, LLAQ, LLZ, LLZZ, XXREAL_0:2;

(Fib (x + 2)) + (Fib (y + 2)) = Fib (((y + 2) + 1) + 1) by PRE_FF:1

.= Fib (k + 2) ;

hence S_{2}[k]
by SDD, XXREAL_0:2, LYY; :: thesis: verum

end;LYY: (Fib (x + 2)) + (Fib (y + 2)) <= (A . (z + 2)) + (A . (z + 1)) by XREAL_1:7, LLAQ, LLZ, LLZZ, XXREAL_0:2;

(Fib (x + 2)) + (Fib (y + 2)) = Fib (((y + 2) + 1) + 1) by PRE_FF:1

.= Fib (k + 2) ;

hence S

S

for i being Nat st i <= n holds

S

proof

hence
for i being Nat st i < n holds
let i be Nat; :: thesis: ( i <= n implies S_{2}[i] )

( i < 1 + 1 or 2 <= i ) ;

then LLP1: ( i <= 1 or 2 <= i ) by INT_1:7;

_{2}[i] )
; :: thesis: verum

end;( i < 1 + 1 or 2 <= i ) ;

then LLP1: ( i <= 1 or 2 <= i ) by INT_1:7;

now :: thesis: ( ( i = 0 & S_{2}[ 0 ] ) or ( i = 1 & S_{2}[1] ) or ( 2 <= i & ( i <= n implies S_{2}[i] ) ) )

hence
( i <= n implies Send;

Fib (i + 2) <= A . (n - i) ; :: thesis: verum

n - 1 < n - 0 by XREAL_1:15;

then G1P: Fib (m + 2) <= A . (n - m) by LEMM1;

G2P: A . 1 = A . (0 + 1)

.= |.b.| by L1 ;

0 + 1 <= n by INT_1:7, LNNZ;

then HYY1: 1 < n + 1 by NAT_1:13;

CLAME: n <= 5 * [/(log (10,|.b.|))\]

proof

end;

reconsider C = seq_n^ 1 as Real_Sequence ;now :: thesis: ( ( n = 1 & n <= 5 * [/(log (10,|.b.|))\] ) or ( 1 < n & n <= 5 * [/(log (10,|.b.|))\] ) )end;

hence
n <= 5 * [/(log (10,|.b.|))\]
; :: thesis: verumper cases
( n = 1 or 1 < n )
by HYY1, NAT_1:22;

end;

case TKK:
n = 1
; :: thesis: n <= 5 * [/(log (10,|.b.|))\]

b <= |.b.|
by ABSVALUE:4;

then 1 < |.b.| by XXREAL_0:2, ASKARI;

then log (10,1) < log (10,|.b.|) by POWER:57;

then 0 < log (10,|.b.|) by POWER:51;

then 0 < [/(log (10,|.b.|))\] by INT_1:def 7;

then 0 + 1 <= 5 * [/(log (10,|.b.|))\] by INT_1:7;

hence n <= 5 * [/(log (10,|.b.|))\] by TKK; :: thesis: verum

end;then 1 < |.b.| by XXREAL_0:2, ASKARI;

then log (10,1) < log (10,|.b.|) by POWER:57;

then 0 < log (10,|.b.|) by POWER:51;

then 0 < [/(log (10,|.b.|))\] by INT_1:def 7;

then 0 + 1 <= 5 * [/(log (10,|.b.|))\] by INT_1:7;

hence n <= 5 * [/(log (10,|.b.|))\] by TKK; :: thesis: verum

case GF:
1 < n
; :: thesis: n <= 5 * [/(log (10,|.b.|))\]

then
1 + 1 <= n
by INT_1:7;

then 2 + 1 <= n + 1 by XREAL_1:6;

then tau to_power ((n + 1) - 2) < Fib (n + 1) by LTAUPOW;

then GCV: tau to_power (n - 1) < |.b.| by XXREAL_0:2, G2P, G1P;

1 - 1 < n - 1 by XREAL_1:9, GF;

then 0 < tau to_power (n - 1) by THTU, POWER:35;

then log (tau,(tau to_power (n - 1))) <= log (tau,|.b.|) by ASYMPT_2:7, GCV, THTU;

then (n - 1) * (log (tau,tau)) <= log (tau,|.b.|) by POWER:55, THTU;

then (n - 1) * 1 <= log (tau,|.b.|) by POWER:52, THTU;

then FAW: n - 1 <= (log (tau,10)) * (log (10,|.b.|)) by POWER:56, THTU, ASKARI;

b <= |.b.| by ABSVALUE:4;

then 1 < |.b.| by XXREAL_0:2, ASKARI;

then log (10,1) < log (10,|.b.|) by POWER:57;

then 0 < log (10,|.b.|) by POWER:51;

then (log (tau,10)) * (log (10,|.b.|)) < 5 * (log (10,|.b.|)) by XREAL_1:68, THTU3;

then MB3: n - 1 < 5 * (log (10,|.b.|)) by FAW, XXREAL_0:2;

log (10,|.b.|) <= [/(log (10,|.b.|))\] by INT_1:def 7;

then 5 * (log (10,|.b.|)) <= 5 * [/(log (10,|.b.|))\] by XREAL_1:64;

then n - 1 < 5 * [/(log (10,|.b.|))\] by XXREAL_0:2, MB3;

then (n - 1) + 1 <= 5 * [/(log (10,|.b.|))\] by INT_1:7;

hence n <= 5 * [/(log (10,|.b.|))\] ; :: thesis: verum

end;then 2 + 1 <= n + 1 by XREAL_1:6;

then tau to_power ((n + 1) - 2) < Fib (n + 1) by LTAUPOW;

then GCV: tau to_power (n - 1) < |.b.| by XXREAL_0:2, G2P, G1P;

1 - 1 < n - 1 by XREAL_1:9, GF;

then 0 < tau to_power (n - 1) by THTU, POWER:35;

then log (tau,(tau to_power (n - 1))) <= log (tau,|.b.|) by ASYMPT_2:7, GCV, THTU;

then (n - 1) * (log (tau,tau)) <= log (tau,|.b.|) by POWER:55, THTU;

then (n - 1) * 1 <= log (tau,|.b.|) by POWER:52, THTU;

then FAW: n - 1 <= (log (tau,10)) * (log (10,|.b.|)) by POWER:56, THTU, ASKARI;

b <= |.b.| by ABSVALUE:4;

then 1 < |.b.| by XXREAL_0:2, ASKARI;

then log (10,1) < log (10,|.b.|) by POWER:57;

then 0 < log (10,|.b.|) by POWER:51;

then (log (tau,10)) * (log (10,|.b.|)) < 5 * (log (10,|.b.|)) by XREAL_1:68, THTU3;

then MB3: n - 1 < 5 * (log (10,|.b.|)) by FAW, XXREAL_0:2;

log (10,|.b.|) <= [/(log (10,|.b.|))\] by INT_1:def 7;

then 5 * (log (10,|.b.|)) <= 5 * [/(log (10,|.b.|))\] by XREAL_1:64;

then n - 1 < 5 * [/(log (10,|.b.|))\] by XXREAL_0:2, MB3;

then (n - 1) + 1 <= 5 * [/(log (10,|.b.|))\] by INT_1:7;

hence n <= 5 * [/(log (10,|.b.|))\] ; :: thesis: verum

set nb = |.b.|;

LC2P: C . |.b.| = |.b.| to_power 1 by ASYMPT_1:def 3, ASKARI;

LC1P: seq_n^ 1 in Big_Oh (seq_n^ 1) by ASYMPT_0:10;

take A ; :: thesis: ex B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take B ; :: thesis: ex C being Real_Sequence ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take C ; :: thesis: ex n being Element of NAT st

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

take n ; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )

thus ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded ) by L1, LC1P, LC2P, CC1, NTALGO_1:2, CLAME, G2P, G1P, LC0P; :: thesis: verum