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: 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;
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 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;
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 A8, XREAL_1:9;
hence S1[i + 1] by A9, XXREAL_0:2; :: thesis: verum
end;
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 A2, TARSKI:def 3; :: thesis: verum
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: 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;
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 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;
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 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;
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 H1P, XREAL_1:9;
hence contradiction by H2; :: thesis: verum
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: ( 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 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;
case j = 0 ; :: thesis: A . (j + 1) < A . j
hence A . (j + 1) < A . j by L1, ASKARI; :: 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 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;
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 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;
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 INT_1:7, LNNZ;
then HYY1: 1 < n + 1 by NAT_1:13;
LLLCT: now :: thesis: ( ( n = 1 & S2[1] ) or ( 1 < n & S2[1] ) )
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 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: ( 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 XREAL_1:231, A2;
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 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 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 NAT_1:sch 9(A1);
 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[1] ) or ( 2 <= i & ( i <= n implies S2[i] ) ) )
per cases ( i = 0 or i = 1 or 2 <= i ) by LLP1, NAT_1:25;
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 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: ( ( n = 1 & n <= 5 * [/(log (10,|.b.|))\] ) or ( 1 < n & n <= 5 * [/(log (10,|.b.|))\] ) )
per cases ( n = 1 or 1 < n ) by HYY1, NAT_1:22;
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;
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 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