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
proof
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
proof
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:
then ex i being Nat st
( x = i & B . i = 0 ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum
end;
ex m0 being Nat st B . m0 = 0
proof
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
proof
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 ;
then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;
hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum
end;
defpred S1[ Nat] means B . \$1 <= (B . 0) - \$1;
A6: S1[ 0 ] ;
A7: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A8: S1[i] ; :: thesis: S1[i + 1]
A9: B . (i + 1) <= (B . i) - 1 by A4;
(B . i) - 1 <= ((B . 0) - i) - 1 by ;
hence S1[i + 1] by ; :: thesis: verum
end;
A10: for i being Nat holds S1[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;
then consider m0 being Nat such that
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 ; :: thesis: verum
end;
KL11: { i where i is Nat : B . i = 0 } is non empty Subset of NAT by ;
then n in { i where i is Nat : B . i = 0 } by ;
then ex i being Nat st
( n = i & B . i = 0 ) ;
then LNNZ: n <> 0 by ;
then NIZ: n - 1 is Nat by NAT_1:20;
LX1: B . (n - 1) <> 0
proof
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 ;
then n < (n - 1) + 1 by XREAL_1:145;
hence contradiction ; :: thesis: verum
end;
B11: for i being Nat st i < n holds
B . i > 0
proof
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;
A4: for i being Nat st i < n holds
B . (i + 1) <= (B . i) - 1
proof
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 ;
then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;
hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum
end;
defpred S1[ Nat] means ( \$1 <= n implies B . \$1 <= (B . 0) - \$1 );
A6: S1[ 0 ] ;
A7: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A8: S1[i] ; :: thesis: S1[i + 1]
assume B8: i + 1 <= n ; :: thesis: B . (i + 1) <= (B . 0) - (i + 1)
then i < n by ;
then A9: B . (i + 1) <= (B . i) - 1 by A4;
(B . i) - 1 <= ((B . 0) - i) - 1 by ;
hence B . (i + 1) <= (B . 0) - (i + 1) by ; :: thesis: verum
end;
A70: for i being Nat holds S1[i] from NAT_1:sch 2(A6, A7);
LC0P: n <= B . 0
proof
assume H1P: n > B . 0 ; :: thesis: contradiction
H2: B . n <= (B . 0) - n by A70;
(B . 0) - n < n - n by ;
hence contradiction by H2; :: thesis: verum
end;
A . n = A . ((n - 1) + 1)
.= B . (n - 1) by ;
then ASTS: 0 + 1 <= A . n by ;
LKA1: for j being Nat st j < n holds
A . (j + 1) < A . j
proof
let j be Nat; :: thesis: ( j < n implies A . (j + 1) < A . j )
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 ) )
per cases ( 0 < j or j = 0 ) ;
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 ;
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 ; :: thesis: verum
end;
case j = 0 ; :: thesis: A . (j + 1) < A . j
hence A . (j + 1) < A . j by ; :: thesis: verum
end;
end;
end;
hence A . (j + 1) < A . j ; :: thesis: verum
end;
ZM: ( 1 < n implies Fib 3 <= A . (n - 1) )
proof
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 ;
n - 1 < n - 0 by XREAL_1:15;
then A . ((n - 1) + 1) < A . (n - 1) by ;
then 1 < A . (n - 1) by ;
then 1 + 1 <= A . (n - 1) by INT_1:7;
hence Fib 3 <= A . (n - 1) by FIB_NUM2:22; :: thesis: verum
end;
TRMT: for i being Nat st 0 < i & i < n holds
(A . (i + 2)) + (A . (i + 1)) <= A . i
proof
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 ;
(A . i) mod (B . i) <= (A . (i + 1)) - 1 by ;
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 ;
then LCP: (A . (i + 2)) + (A . (i + 1)) <= (A . (i + 2)) + (((A . i) div (A . (i + 1))) * (A . (i + 1))) by ;
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 ;
hence (A . (i + 2)) + (A . (i + 1)) <= A . i by LCP; :: thesis: verum
end;
LEMM1: for i being Nat st i < n holds
Fib (i + 2) <= A . (n - i)
proof
defpred S2[ Nat] means ( \$1 < n implies Fib (\$1 + 2) <= A . (n - \$1) );
0 + 1 <= n by ;
then HYY1: 1 < n + 1 by NAT_1:13;
LLLCT: now :: thesis: ( ( n = 1 & S2 ) or ( 1 < n & S2 ) )
per cases ( n = 1 or 1 < n ) by ;
end;
end;
A1: for k being Nat st k >= 2 & ( for i being Nat st i >= 2 & i < k holds
S2[i] ) holds
S2[k]
proof
let k be Nat; :: thesis: ( k >= 2 & ( for i being Nat st i >= 2 & i < k holds
S2[i] ) implies S2[k] )

assume A2: k >= 2 ; :: thesis: ( ex i being Nat st
( i >= 2 & i < k & not S2[i] ) or S2[k] )

assume A3: for i being Nat st i >= 2 & i < k holds
S2[i] ; :: thesis: S2[k]
AU4: for i being Nat st i < k holds
S2[i]
proof
let i be Nat; :: thesis: ( i < k implies S2[i] )
assume NNNH: i < k ; :: thesis: S2[i]
now :: thesis: ( ( i = 0 & S2[i] ) or ( i = 1 & S2[i] ) or ( 2 <= i & S2[i] ) )end;
hence S2[i] ; :: thesis: verum
end;
k - 1 in NAT by ;
then reconsider x = k - 1 as Nat ;
k - 2 in NAT by ;
then reconsider y = k - 2 as Nat ;
LLZZ: ( x < k & y < k ) by XREAL_1:44;
LLZ: ( S2[x] & S2[y] ) by AU4, XREAL_1:44;
now :: thesis: ( ( k < n & S2[k] ) or ( n <= k & S2[k] ) )
per cases ( k < n or n <= k ) ;
case LLAQ: k < n ; :: thesis: S2[k]
then n - k in NAT by INT_1:5;
then reconsider z = n - k as Nat ;
ZEE: z < n by ;
now :: thesis: ( ( z = 0 & S2[k] ) or ( 0 < z & S2[k] ) )
per cases ( z = 0 or 0 < z ) ;
case 0 < z ; :: thesis: S2[k]
then SDD: (A . (z + 2)) + (A . (z + 1)) <= A . z by ;
LYY: (Fib (x + 2)) + (Fib (y + 2)) <= (A . (z + 2)) + (A . (z + 1)) by ;
(Fib (x + 2)) + (Fib (y + 2)) = Fib (((y + 2) + 1) + 1) by PRE_FF:1
.= Fib (k + 2) ;
hence S2[k] by SDD, XXREAL_0:2, LYY; :: thesis: verum
end;
end;
end;
hence S2[k] ; :: thesis: verum
end;
end;
end;
hence S2[k] ; :: thesis: verum
end;
A10: for k being Nat st k >= 2 holds
S2[k] from for i being Nat st i <= n holds
S2[i]
proof
let i be Nat; :: thesis: ( i <= n implies S2[i] )
( i < 1 + 1 or 2 <= i ) ;
then LLP1: ( i <= 1 or 2 <= i ) by INT_1:7;
now :: thesis: ( ( i = 0 & S2[ 0 ] ) or ( i = 1 & S2 ) or ( 2 <= i & ( i <= n implies S2[i] ) ) )
per cases ( i = 0 or i = 1 or 2 <= i ) by ;
case i = 0 ; :: thesis: S2[ 0 ]
thus S2[ 0 ] by ; :: thesis: verum
end;
case 2 <= i ; :: thesis: ( i <= n implies S2[i] )
hence ( i <= n implies S2[i] ) by A10; :: thesis: verum
end;
end;
end;
hence ( i <= n implies S2[i] ) ; :: thesis: verum
end;
hence for i being Nat st i < n holds
Fib (i + 2) <= A . (n - i) ; :: thesis: verum
end;
reconsider m = n - 1 as Nat by ;
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 ;
then HYY1: 1 < n + 1 by NAT_1:13;
CLAME: n <= 5 * [/(log (10,|.b.|))\]
proof
now :: thesis: ( ( n = 1 & n <= 5 * [/(log (10,|.b.|))\] ) or ( 1 < n & n <= 5 * [/(log (10,|.b.|))\] ) )
per cases ( n = 1 or 1 < n ) by ;
case TKK: n = 1 ; :: thesis: n <= 5 * [/(log (10,|.b.|))\]
b <= |.b.| by ABSVALUE:4;
then 1 < |.b.| by ;
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;
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 ;
1 - 1 < n - 1 by ;
then 0 < tau to_power (n - 1) by ;
then log (tau,(tau to_power (n - 1))) <= log (tau,|.b.|) by ;
then (n - 1) * (log (tau,tau)) <= log (tau,|.b.|) by ;
then (n - 1) * 1 <= log (tau,|.b.|) by ;
then FAW: n - 1 <= (log (tau,10)) * (log (10,|.b.|)) by ;
b <= |.b.| by ABSVALUE:4;
then 1 < |.b.| by ;
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 ;
then MB3: n - 1 < 5 * (log (10,|.b.|)) by ;
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 ;
then (n - 1) + 1 <= 5 * [/(log (10,|.b.|))\] by INT_1:7;
hence n <= 5 * [/(log (10,|.b.|))\] ; :: thesis: verum
end;
end;
end;
hence n <= 5 * [/(log (10,|.b.|))\] ; :: thesis: verum
end;
reconsider C = seq_n^ 1 as Real_Sequence ;
set nb = |.b.|;
LC2P: C . |.b.| = |.b.| to_power 1 by ;
LC1P: seq_n^ 1 in Big_Oh () 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 ; :: thesis: verum