let a, b be Element of INT ; :: thesis:
assume ASKARI: ( |.a.| > |.b.| & b > 1 ) ; :: thesis:
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:
let A, B be sequence of NAT; :: thesis:
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:
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:
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:

end;

ex m0 being Nat st B . m0 = 0

proof

assume A3: for m0 being Nat holds not B . m0 = 0 ; :: thesis:
A4: for i being Nat holds B . (i + 1) <= (B . i) - 1

proof

let i be Nat; :: thesis:
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:

end;

defpred S₁[ Nat] means B . $1 <= (B . 0) - $1;
A6: S₁[ 0 ] ;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A8: S₁[i] ; :: thesis:
A9: B . (i + 1) <= (B . i) - 1 by A4;
(B . i) - 1 <= ((B . 0) - i) - 1 by A8, XREAL_1:9;
hence S₁[i + 1] by A9, XXREAL_0:2; :: thesis:

end;

A10: for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A7);
then B . (B . 0) <= (B . 0) - (B . 0) ;
hence contradiction by A3, NAT_1:14; :: thesis:

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 A2, TARSKI:def 3; :: thesis:

end;

KL11: { i where i is Nat : B . i = 0 } is non empty Subset of NAT by L1, Lm5;
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

assume B . (n - 1) = 0 ; :: thesis:
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:

end;

B11: for i being Nat st i < n holds
B . i > 0

proof

let i be Nat; :: thesis:
assume WHHO: i < n ; :: thesis:
assume 0 >= B . i ; :: thesis:
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:

end;

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

proof

let i be Nat; :: thesis:
assume i < n ; :: thesis:
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:

end;

defpred S₁[ Nat] means ( $1 <= n implies B . $1 <= (B . 0) - $1 );
A6: S₁[ 0 ] ;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A8: S₁[i] ; :: thesis:
assume B8: i + 1 <= n ; :: thesis:
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:

end;

A70: for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A7);
LC0P: n <= B . 0

proof

assume H1P: n > B . 0 ; :: thesis:
H2: B . n <= (B . 0) - n by A70;
(B . 0) - n < n - n by H1P, XREAL_1:9;
hence contradiction by H2; :: thesis:

end;

A . n = A . ((n - 1) + 1)
.= 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

let j be Nat; :: thesis:
assume CCC1: j < n ; :: thesis:

now :: thesis:

per cases ;

case 0 < j ; :: thesis:

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:

end;

case j = 0 ; :: thesis:

hence A . (j + 1) < A . j by L1, ASKARI; :: thesis:

end;

end;

end;

hence A . (j + 1) < A . j ; :: thesis:

end;

ZM: ( 1 < n implies Fib 3 <= A . (n - 1) )

proof

assume 1 < n ; :: thesis:
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:

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:
assume LP11: ( 0 < i & i < n ) ; :: thesis:
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:

end;

LEMM1: for i being Nat st i < n holds
Fib (i + 2) <= A . (n - i)

proof

defpred S₂[ 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;

LLLCT: now :: thesis:

per cases by HYY1, NAT_1:22;

case n = 1 ; :: thesis:

hence S₂[1] ; :: thesis:

end;

case 1 < n ; :: thesis:

thus S₂[1] by ZM; :: thesis:

end;

end;

end;

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

proof

let k be Nat; :: thesis:
assume A2: k >= 2 ; :: thesis:
assume A3: for i being Nat st i >= 2 & i < k holds
S₂[i] ; :: thesis:
AU4: for i being Nat st i < k holds
S₂[i]

proof

let i be Nat; :: thesis:
assume NNNH: i < k ; :: thesis:

now :: thesis:

per cases by NAT_1:23;

case i = 0 ; :: thesis:

hence S₂[i] by ASTS, FIB_NUM2:21; :: thesis:

end;

case i = 1 ; :: thesis:

hence S₂[i] by LLLCT; :: thesis:

end;

case 2 <= i ; :: thesis:

hence S₂[i] by A3, NNNH; :: thesis:

end;

end;

end;

hence S₂[i] ; :: thesis:

end;

k - 1 in NAT by INT_1:5, A2, XXREAL_0:2;
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₂[x] & S₂[y] ) by AU4, XREAL_1:44;

now :: thesis:

per cases ;

case LLAQ: k < n ; :: thesis:

then n - k in NAT by INT_1:5;
then reconsider z = n - k as Nat ;
ZEE: z < n by XREAL_1:231, A2;

now :: thesis:

per cases ;

case z = 0 ; :: thesis:

hence S₂[k] ; :: thesis:

end;

case 0 < z ; :: thesis:

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₂[k] by SDD, XXREAL_0:2, LYY; :: thesis:

end;

end;

end;

hence S₂[k] ; :: thesis:

end;

case n <= k ; :: thesis:

hence S₂[k] ; :: thesis:

end;

end;

end;

hence S₂[k] ; :: thesis:

end;

A10: for k being Nat st k >= 2 holds
S₂[k] from NAT_1:sch 9(A1);
for i being Nat st i <= n holds
S₂[i]

proof

let i be Nat; :: thesis:
( i < 1 + 1 or 2 <= i ) ;
then LLP1: ( i <= 1 or 2 <= i ) by INT_1:7;

now :: thesis:

per cases by LLP1, NAT_1:25;

case i = 0 ; :: thesis:

thus S₂[ 0 ] by ASTS, FIB_NUM2:21; :: thesis:

end;

case i = 1 ; :: thesis:

thus S₂[1] by LLLCT; :: thesis:

end;

case 2 <= i ; :: thesis:

hence ( i <= n implies S₂[i] ) by A10; :: thesis:

end;

end;

end;

hence ( i <= n implies S₂[i] ) ; :: thesis:

end;

hence for i being Nat st i < n holds
Fib (i + 2) <= A . (n - i) ; :: thesis:

end;

reconsider m = n - 1 as Nat by LNNZ, NAT_1:20;
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

now :: thesis:

per cases by HYY1, NAT_1:22;

case TKK: n = 1 ; :: thesis:

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:

end;

case GF: 1 < n ; :: thesis:

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:

end;

end;

end;

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

end;

reconsider C = seq_n^ 1 as Real_Sequence ;
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:
take B ; :: thesis:
take C ; :: thesis:
take n ; :: thesis:
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: