let f be INT -valued non-zero Polynomial of F_Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 H₁( Real) -> object = |.(a - $1).|;
set DIF = { H₁(b) where b is Element of F_Real : b in (Roots f) \ {a} } ;
A12: (Roots f) \ {a} is finite ;
A13: { H₁(b) where b is Element of F_Real : b in (Roots f) \ {a} } is finite from FRAENKEL:sch 21(A12);
{ H₁(b) where b is Element of F_Real : b in (Roots f) \ {a} } c= REAL then reconsider DIF = { H₁(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 ; :: thesis: for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
let p be Integer; :: thesis: for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
let q be positive Nat; :: thesis: |.(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)) ; :: thesis: 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 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;