let a, b be Element of INT ; ( |.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 )
; 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
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
B11:
for i being Nat st i < n holds
B . i > 0
A4:
for i being Nat st i < n holds
B . (i + 1) <= (B . i) - 1
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]
A70:
for i being Nat holds S1[i]
from NAT_1:sch 2(A6, A7);
LC0P:
n <= B . 0
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;
( j < n implies A . (j + 1) < A . j )
assume CCC1:
j < n
;
A . (j + 1) < A . j
now ( ( 0 < j & A . (j + 1) < A . j ) or ( j = 0 & A . (j + 1) < A . j ) )end;
hence
A . (j + 1) < A . j
;
verum
end;
ZM:
( 1 < n implies Fib 3 <= A . (n - 1) )
TRMT:
for i being Nat st 0 < i & i < n holds
(A . (i + 2)) + (A . (i + 1)) <= A . i
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 ( ( 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;
( k >= 2 & ( for i being Nat st i >= 2 & i < k holds
S2[i] ) implies S2[k] )
assume A2:
k >= 2
;
( 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]
;
S2[k]
AU4:
for
i being
Nat st
i < k holds
S2[
i]
proof
let i be
Nat;
( i < k implies S2[i] )
assume NNNH:
i < k
;
S2[i]
now ( ( i = 0 & S2[i] ) or ( i = 1 & S2[i] ) or ( 2 <= i & S2[i] ) )end;
hence
S2[
i]
;
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 ( ( k < n & S2[k] ) or ( n <= k & S2[k] ) )end;
hence
S2[
k]
;
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;
( i <= n implies S2[i] )
(
i < 1
+ 1 or 2
<= i )
;
then LLP1:
(
i <= 1 or 2
<= i )
by INT_1:7;
now ( ( i = 0 & S2[ 0 ] ) or ( i = 1 & S2[1] ) or ( 2 <= i & ( i <= n implies S2[i] ) ) )end;
hence
(
i <= n implies
S2[
i] )
;
verum
end;
hence
for
i being
Nat st
i < n holds
Fib (i + 2) <= A . (n - i)
;
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 ( ( 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
;
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.|))\]
;
verum end; end; end;
hence
n <= 5
* [/(log (10,|.b.|))\]
;
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
; 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
; 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
; 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
; ( 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; verum