let f be INT -valued non-zero Polynomial of F_Real; for a being irrational Element of F_Real st a is_a_root_of f holds
ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
set n = len f;
let a be irrational Element of F_Real; ( a is_a_root_of f implies ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f)) )
assume A1:
a is_a_root_of f
; ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
set X = [.(a - 1),(a + 1).];
set E = Eval f;
set F = ((Eval f) `|) | [.(a - 1),(a + 1).];
set M1 = sup (rng |.(((Eval f) `|) | [.(a - 1),(a + 1).]).|);
A2:
dom (Eval f) = REAL
by FUNCT_2:def 1;
A3:
Eval f is differentiable
;
A4:
dom ((Eval f) `|) = REAL
by FUNCT_2:def 1;
then A5:
dom (((Eval f) `|) | [.(a - 1),(a + 1).]) = [.(a - 1),(a + 1).]
by RELAT_1:62;
A6:
dom |.(((Eval f) `|) | [.(a - 1),(a + 1).]).| = dom (((Eval f) `|) | [.(a - 1),(a + 1).])
by VALUED_1:def 11;
reconsider F = ((Eval f) `|) | [.(a - 1),(a + 1).] as PartFunc of [.(a - 1),(a + 1).],REAL by RELAT_1:185;
F is bounded
by A4, INTEGRA5:10;
then
rng |.F.| is real-bounded
by INTEGRA1:15;
then reconsider M1 = sup (rng |.(((Eval f) `|) | [.(a - 1),(a + 1).]).|) as Element of REAL by XXREAL_2:16;
set M = M1 + 1;
consider Y being object such that
A7:
Y in rng |.F.|
by XBOOLE_0:def 1;
reconsider Y = Y as Real by A7;
consider A being object such that
A in dom |.F.|
and
A8:
|.F.| . A = Y
by A7, FUNCT_1:def 3;
A9:
|.F.| . A = |.(F . A).|
by VALUED_1:18;
M1 is UpperBound of rng |.F.|
by XXREAL_2:def 3;
then A10:
Y <= M1
by A7, XXREAL_2:def 1;
A11:
M1 + 0 <= M1 + 1
by XREAL_1:6;
set RTS = (Roots f) \ {a};
deffunc H1( Real) -> object = |.(a - $1).|;
set DIF = { H1(b) where b is Element of F_Real : b in (Roots f) \ {a} } ;
A12:
(Roots f) \ {a} is finite
;
A13:
{ H1(b) where b is Element of F_Real : b in (Roots f) \ {a} } is finite
from FRAENKEL:sch 21(A12);
{ H1(b) where b is Element of F_Real : b in (Roots f) \ {a} } c= REAL
then reconsider DIF = { H1(b) where b is Element of F_Real : b in (Roots f) \ {a} } as finite Subset of REAL by A13;
set MIN = {1,(1 / (M1 + 1))} \/ DIF;
{1,(1 / (M1 + 1))} \/ DIF c= REAL
by XREAL_0:def 1;
then reconsider MIN = {1,(1 / (M1 + 1))} \/ DIF as non empty finite Subset of REAL ;
for x being Real st x in MIN holds
x > 0
then
min MIN > 0
by XXREAL_2:def 5;
then consider A being Real such that
A16:
0 < A
and
A17:
A < inf MIN
by XREAL_1:5;
reconsider A = A as positive Real by A16;
take
A
; for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
let p be Integer; for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
let q be positive Nat; |.(a - (p / q)).| > A / (q |^ (len f))
set qn = q |^ (len f);
reconsider qtn = q |^ (len f) as Element of F_Real by XREAL_0:def 1;
assume A18:
|.(a - (p / q)).| <= A / (q |^ (len f))
; contradiction
A19:
|.(a - (p / q)).| = |.((p / q) - a).|
by COMPLEX1:60;
A20:
(Eval f) . a = 0. F_Real
by A1, POLYNOM5:def 13;
reconsider pq = p / q as Element of F_Real by XREAL_0:def 1;
0 + 1 <= q |^ (len f)
by NAT_1:13;
then
A / (q |^ (len f)) <= A / 1
by XREAL_1:118;
then
|.(a - (p / q)).| <= A
by A18, XXREAL_0:2;
then A21:
|.(a - (p / q)).| < inf MIN
by A17, XXREAL_0:2;
then
not |.(a - (p / q)).| in MIN
by XXREAL_2:3;
then
not |.(a - (p / q)).| in DIF
by XBOOLE_0:def 3;
then
not pq in (Roots f) \ {a}
;
then
not p / q in Roots f
by ZFMISC_1:56;
then A22:
not pq is_a_root_of f
by POLYNOM5:def 10;
A23:
( (Eval f) . (p / q) = eval (f,pq) & (Eval f) . a = eval (f,a) )
by POLYNOM5:def 13;
A24:
a + 0 <= a + 1
by XREAL_1:6;
A25:
1 / ((M1 + 1) * (q |^ (len f))) = (1 / (M1 + 1)) * (1 / (q |^ (len f)))
by XCMPLX_1:102;
1 / (M1 + 1) in {1,(1 / (M1 + 1))}
by TARSKI:def 2;
then
1 / (M1 + 1) in MIN
by XBOOLE_0:def 3;
then
inf MIN <= 1 / (M1 + 1)
by XXREAL_2:3;
then
A < 1 / (M1 + 1)
by A17, XXREAL_0:2;
then A26:
A * (1 / (q |^ (len f))) < (1 / (M1 + 1)) * (1 / (q |^ (len f)))
by XREAL_1:68;
1 in {1,(1 / (M1 + 1))}
by TARSKI:def 2;
then
1 in MIN
by XBOOLE_0:def 3;
then
inf MIN <= 1
by XXREAL_2:3;
then A27:
|.(a - (p / q)).| <= 1
by A21, XXREAL_0:2;
consider EF being FinSequence of the carrier of F_Real such that
A28:
( (Eval f) . (p / q) = Sum EF & len EF = len f & ( for n being Element of NAT st n in dom EF holds
EF . n = (f . (n -' 1)) * ((power F_Real) . (pq,(n -' 1))) ) )
by POLYNOM4:def 2, A23;
set G = qtn * EF;
reconsider FF = EF as Element of (len EF) -tuples_on the carrier of F_Real by FINSEQ_2:92;
set GG = qtn * FF;
len (qtn * FF) = len EF
by FINSEQ_2:132;
then A29: dom (qtn * EF) =
Seg (len EF)
by FINSEQ_1:def 3
.=
dom EF
by FINSEQ_1:def 3
;
rng (qtn * EF) c= INT
proof
let o be
object ;
TARSKI:def 3 ( not o in rng (qtn * EF) or o in INT )
assume
o in rng (qtn * EF)
;
o in INT
then consider b being
object such that A30:
(
b in dom (qtn * EF) &
o = (qtn * EF) . b )
by FUNCT_1:def 3;
reconsider b =
b as
Element of
NAT by A30;
b in Seg (len f)
by A30, A29, A28, FINSEQ_1:def 3;
then
( 1
<= b &
b <= len f &
b -' 1
<= b )
by FINSEQ_1:1, NAT_D:35;
then consider c being
Nat such that A31:
len f = (b -' 1) + c
by NAT_1:10, XXREAL_0:2;
rng EF c= the
carrier of
F_Real
;
then reconsider a9 =
EF . b as
Element of
F_Real by A30, A29, FUNCT_1:3;
(
b in dom (qtn * EF) &
a9 = EF . b implies
(qtn * EF) . b = qtn * a9 )
by FVSUM_1:50;
then (qtn * EF) . b =
qtn * ((f . (b -' 1)) * ((power F_Real) . (pq,(b -' 1))))
by A28, A30, A29
.=
(f . (b -' 1)) * ((q |^ (len f)) * ((power F_Real) . (pq,(b -' 1))))
.=
(f . (b -' 1)) * ((q |^ (len f)) * ((p / q) |^ (b -' 1)))
by NIVEN:7
.=
(f . (b -' 1)) * ((q |^ (len f)) * ((p |^ (b -' 1)) / (q |^ (b -' 1))))
by PREPOWER:8
.=
((f . (b -' 1)) * (p |^ (b -' 1))) * ((q |^ (len f)) / (q |^ (b -' 1)))
.=
((f . (b -' 1)) * (p |^ (b -' 1))) * (((q |^ c) * (q |^ (b -' 1))) / (q |^ (b -' 1)))
by A31, NEWTON:8
.=
((f . (b -' 1)) * (p |^ (b -' 1))) * ((q |^ c) * ((q |^ (b -' 1)) / (q |^ (b -' 1))))
.=
((f . (b -' 1)) * (p |^ (b -' 1))) * ((q |^ c) * 1)
by XCMPLX_1:60
.=
((f . (b -' 1)) * (p |^ (b -' 1))) * (q |^ c)
;
hence
o in INT
by INT_1:def 2, A30;
verum
end;
then reconsider G1 = qtn * EF as INT -valued FinSequence by RELAT_1:def 19;
Sum G1 = Sum (qtn * EF)
by NIVEN:6;
then reconsider SG = Sum (qtn * EF) as Integer ;
Sum (qtn * EF) =
qtn * (Sum EF)
by FVSUM_1:73
.=
(q |^ (len f)) * (Sum EF)
;
then
|.SG.| = |.(q |^ (len f)).| * |.(Sum EF).|
by COMPLEX1:65;
then A32:
|.((Eval f) . (p / q)).| >= 1 / (q |^ (len f))
by A28, A22, A23, NAT_1:14, XREAL_1:79;
per cases
( p / q < a or a < p / q )
by XXREAL_0:1;
suppose A33:
p / q < a
;
contradiction
(Eval f) | [.(p / q),a.] is
continuous
;
then consider x0 being
Real such that A34:
x0 in ].(p / q),a.[
and A35:
diff (
(Eval f),
x0)
= (((Eval f) . a) - ((Eval f) . (p / q))) / (a - (p / q))
by A2, A3, A33, FDIFF_1:26, ROLLE:3;
A36:
|.(((Eval f) . a) - ((Eval f) . (p / q))).| = |.((Eval f) . (p / q)).|
by A20, COMPLEX1:52;
A37:
a - (p / q) <> 0
;
then
a - (p / q) = (((Eval f) . a) - ((Eval f) . (p / q))) / (diff ((Eval f),x0))
by A35, A1, A22, A23, XCMPLX_1:54;
then A38:
|.(a - (p / q)).| = |.((Eval f) . (p / q)).| / |.(diff ((Eval f),x0)).|
by A36, COMPLEX1:67;
a - (p / q) <= 1
by A27, ABSVALUE:5;
then
(a - (p / q)) - a <= 1
- a
by XREAL_1:9;
then
- (- (p / q)) >= - (1 - a)
by XREAL_1:24;
then A39:
].(p / q),a.[ c= [.(a - 1),(a + 1).]
by A24, XXREAL_1:37;
then A40:
F . x0 =
((Eval f) `|) . x0
by A34, FUNCT_1:49
.=
diff (
(Eval f),
x0)
by POLYDIFF:10
;
|.F.| . x0 = |.(F . x0).|
by VALUED_1:18;
then
|.(diff ((Eval f),x0)).| in rng |.F.|
by A5, A6, A34, A39, A40, FUNCT_1:def 3;
then
|.(diff ((Eval f),x0)).| <= M1
by XXREAL_2:4;
then
|.(diff ((Eval f),x0)).| <= M1 + 1
by A11, XXREAL_0:2;
then
1
/ |.(diff ((Eval f),x0)).| >= 1
/ (M1 + 1)
by A35, A1, A37, A22, A23, XREAL_1:118;
then
|.((Eval f) . (p / q)).| / |.(diff ((Eval f),x0)).| >= 1
/ ((M1 + 1) * (q |^ (len f)))
by A10, A9, A8, A32, A25, XREAL_1:66;
hence
contradiction
by A18, A38, A25, A26, XXREAL_0:2;
verum end; suppose A41:
a < p / q
;
contradiction
(Eval f) | [.a,(p / q).] is
continuous
;
then consider x0 being
Real such that A42:
x0 in ].a,(p / q).[
and A43:
diff (
(Eval f),
x0)
= (((Eval f) . (p / q)) - ((Eval f) . a)) / ((p / q) - a)
by A2, A3, A41, FDIFF_1:26, ROLLE:3;
A44:
(p / q) - a <> 0
;
then
(p / q) - a = (((Eval f) . (p / q)) - ((Eval f) . a)) / (diff ((Eval f),x0))
by A1, A22, A23, A43, XCMPLX_1:54;
then A45:
|.((p / q) - a).| = |.((Eval f) . (p / q)).| / |.(diff ((Eval f),x0)).|
by A20, COMPLEX1:67;
A46:
a - 1
< a - 0
by XREAL_1:15;
- 1
<= a - (p / q)
by A27, ABSVALUE:5;
then
(- 1) - a <= (a - (p / q)) - a
by XREAL_1:9;
then
- ((- 1) - a) >= - (- (p / q))
by XREAL_1:24;
then A47:
].a,(p / q).[ c= [.(a - 1),(a + 1).]
by A46, XXREAL_1:37;
then A48:
F . x0 =
((Eval f) `|) . x0
by A42, FUNCT_1:49
.=
diff (
(Eval f),
x0)
by POLYDIFF:10
;
|.F.| . x0 = |.(F . x0).|
by VALUED_1:18;
then
|.(diff ((Eval f),x0)).| in rng |.F.|
by A5, A6, A42, A47, A48, FUNCT_1:def 3;
then
|.(diff ((Eval f),x0)).| <= M1
by XXREAL_2:4;
then
|.(diff ((Eval f),x0)).| <= M1 + 1
by A11, XXREAL_0:2;
then
1
/ |.(diff ((Eval f),x0)).| >= 1
/ (M1 + 1)
by A43, A1, A22, A44, A23, XREAL_1:118;
then
|.((Eval f) . (p / q)).| / |.(diff ((Eval f),x0)).| >= 1
/ ((M1 + 1) * (q |^ (len f)))
by A10, A9, A8, A25, A32, XREAL_1:66;
hence
contradiction
by A18, A19, A45, A25, A26, XXREAL_0:2;
verum end;