liouvil2.miz

    begin

    reserve m,n for Nat;

    reserve r for Real;

    reserve c for Element of F_Complex ;

    set FC = F_Complex ;

    set FR = F_Real ;

    set Fq = F_Rat ;

    set IR = INT.Ring ;

    registration

      let f be non empty complex-valued Function;

      cluster |.f.| -> non empty;

      coherence

      proof

        ( dom |.f.|) = ( dom f) by VALUED_1:def 11;

        hence thesis;

      end;

    end

    theorem :: LIOUVIL2:1



     Th2: 2 <= m implies for A be Real holds ex n be positive Nat st A <= (m |^ n)

    proof

      assume 2 <= m;

      then (1 + 1) <= m;

      then

       A1: 1 < m by NAT_1: 13;

      let A be Real;

      reconsider a = |. [/A\].| as Nat by TARSKI: 1;

      reconsider n = (a + 1) as positive Nat;

      A <= [/A\] & [/A\] <= a by ABSVALUE: 4, INT_1:def 7;

      then

       A2: A <= a by XXREAL_0: 2;

      a < n & n <= (m |^ n) by A1, NAT_3: 2, NAT_1: 13;

      then a <= (m |^ n) by XXREAL_0: 2;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: LIOUVIL2:2



     Th3: for A be positive Real holds ex n be positive Nat st (1 / (2 |^ n)) <= A

    proof

      let A be positive Real;

      consider n be positive Nat such that

       A1: (1 / A) <= (2 |^ n) by Th2;

      take n;

      (1 / (1 / A)) >= (1 / (2 |^ n)) by A1, XREAL_1: 118;

      hence thesis;

    end;

    registration

      let r, n;

      cluster [.(r - n), (r + n).] -> right_end;

      coherence

      proof

        (r - n) <= (r + n) by XREAL_1: 6;

        hence thesis by XXREAL_2: 33;

      end;

    end

    registration

      let a,b be Real;

      cluster [.a, b.] -> closed_interval;

      coherence

      proof

        let X be Subset of REAL ;

        assume X = [.a, b.];

        hence ex x,y be Real st X = [.x, y.];

      end;

    end

    registration

      cluster irrational for Element of F_Real ;

      existence

      proof

        reconsider a = the irrational Real as Element of FR by XREAL_0:def 1;

        take a;

        thus thesis;

      end;

    end

    theorem :: LIOUVIL2:3



     Th4: F_Real is Subring of F_Complex by RING_3: 43, RING_3: 48;

    theorem :: LIOUVIL2:4



     Th5: F_Rat is Subring of F_Real by GAUSSINT: 14, RING_3: 43;

    theorem :: LIOUVIL2:5

     INT.Ring is Subring of F_Real by Th5, RING_3: 47, ALGNUM_1: 1;

    theorem :: LIOUVIL2:6



     Th7: for R be Ring, S be Subring of R holds for x be Element of S holds x is Element of R

    proof

      let R be Ring;

      let S be Subring of R;

      let x be Element of S;

      the carrier of S c= the carrier of R by C0SP1:def 3;

      hence x is Element of R;

    end;

    theorem :: LIOUVIL2:7



     Th8: for R be Ring, S be Subring of R holds for f be Polynomial of S holds f is Polynomial of R

    proof

      let R be Ring, S be Subring of R;

      let f be Polynomial of S;

      the carrier of S c= the carrier of R by C0SP1:def 3;

      then

      reconsider f as sequence of R by FUNCT_2: 7;

      f is finite-Support

      proof

        consider n such that

         A1: for i be Nat st i >= n holds (f . i) = ( 0. S) by ALGSEQ_1:def 1;

        take n;

        ( 0. S) = ( 0. R) by C0SP1:def 3;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: LIOUVIL2:8



     Th9: for R be Ring, S be Subring of R holds for f be Polynomial of S holds for g be Polynomial of R st f = g holds ( len f) = ( len g)

    proof

      let R be Ring;

      let S be Subring of R;

      let f be Polynomial of S;

      let g be Polynomial of R;

      assume

       A1: f = g;



       A2: ( len g) is_at_least_length_of f

      proof

        let i be Nat;

        assume i >= ( len g);

        then (g . i) = ( 0. R) by ALGSEQ_1: 8;

        hence (f . i) = ( 0. S) by A1, C0SP1:def 3;

      end;

      for m be Nat st m is_at_least_length_of f holds ( len g) <= m

      proof

        let m be Nat;

        assume

         A3: m is_at_least_length_of f;

        m is_at_least_length_of g

        proof

          let i be Nat;

          assume i >= m;

          then (f . i) = ( 0. S) by A3;

          hence (g . i) = ( 0. R) by A1, C0SP1:def 3;

        end;

        hence ( len g) <= m by ALGSEQ_1:def 3;

      end;

      hence thesis by A2, ALGSEQ_1:def 3;

    end;

    theorem :: LIOUVIL2:9

    for R be Ring, S be Subring of R holds for f be Polynomial of S holds for g be Polynomial of R st f = g holds ( LC f) = ( LC g) by Th9;

    theorem :: LIOUVIL2:10

    for R be non degenerated Ring, S be Subring of R holds for f be Polynomial of S holds for g be monic Polynomial of R st f = g holds f is monic

    proof

      let R be non degenerated Ring;

      let S be Subring of R;

      let f be Polynomial of S;

      let g be monic Polynomial of R;

      assume f = g;



      hence ( LC f) = ( LC g) by Th9

      .= ( 1. R) by RATFUNC1:def 7

      .= ( 1. S) by C0SP1:def 3;

    end;

    registration

      let R be non degenerated Ring;

      cluster -> non degenerated for Subring of R;

      coherence

      proof

        let S be Subring of R;

        ( 0. S) = ( 0. R) & ( 1. S) = ( 1. R) by C0SP1:def 3;

        hence ( 0. S) <> ( 1. S);

      end;

      cluster non degenerated for Subring of R;

      existence

      proof

        take the Subring of R;

        thus thesis;

      end;

    end

    theorem :: LIOUVIL2:11

    for R be non degenerated Ring, S be non degenerated Subring of R holds for f be monic Polynomial of S holds for g be Polynomial of R st f = g holds g is monic

    proof

      let R be non degenerated Ring;

      let S be non degenerated Subring of R;

      let f be monic Polynomial of S;

      let g be Polynomial of R;

      assume f = g;



      hence ( LC g) = ( LC f) by Th9

      .= ( 1. S) by RATFUNC1:def 7

      .= ( 1. R) by C0SP1:def 3;

    end;

    theorem :: LIOUVIL2:12



     Th13: for R be non degenerated Ring, S be Subring of R holds for f be Polynomial of S holds for g be non-zero Polynomial of R st f = g holds f is non-zero

    proof

      let R be non degenerated Ring;

      let S be Subring of R;

      let f be Polynomial of S;

      let g be non-zero Polynomial of R;

      assume f = g;

      then

       A1: ( len f) = ( len g) by Th9;

       0 < ( len g) by UPROOTS: 17;

      hence thesis by A1, UPROOTS: 17;

    end;

    theorem :: LIOUVIL2:13

    for R be non degenerated Ring, S be Subring of R holds for f be non-zero Polynomial of S holds for g be Polynomial of R st f = g holds g is non-zero

    proof

      let R be non degenerated Ring;

      let S be Subring of R;

      let f be non-zero Polynomial of S;

      let g be Polynomial of R;

      assume f = g;

      then

       A1: ( len f) = ( len g) by Th9;

       0 < ( len f) by UPROOTS: 17;

      hence thesis by A1, UPROOTS: 17;

    end;

    theorem :: LIOUVIL2:14



     Th15: for R,T be Ring, S be Subring of R holds for f be Polynomial of S holds for g be Polynomial of R st f = g holds for a be Element of R holds ( Ext_eval (f,( In (a,T)))) = ( Ext_eval (g,( In (a,T))))

    proof

      let R,T be Ring;

      let S be Subring of R;

      let f be Polynomial of S;

      let g be Polynomial of R;

      assume

       A1: f = g;

      let a be Element of R;

      consider F be FinSequence of T such that

       A2: ( Ext_eval (f,( In (a,T)))) = ( Sum F) and

       A3: ( len F) = ( len f) and

       A4: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((f . (n -' 1)),T)) * (( power T) . (( In (a,T)),(n -' 1)))) by ALGNUM_1:def 1;

      consider G be FinSequence of T such that

       A5: ( Ext_eval (g,( In (a,T)))) = ( Sum G) and

       A6: ( len G) = ( len g) and

       A7: for n be Element of NAT st n in ( dom G) holds (G . n) = (( In ((g . (n -' 1)),T)) * (( power T) . (( In (a,T)),(n -' 1)))) by ALGNUM_1:def 1;

      consider Z be sequence of T such that

       A8: ( Sum G) = (Z . ( len G)) and

       A9: (Z . 0 ) = ( 0. T) and

       A10: for j be Nat, v be Element of T st j < ( len G) & v = (G . (j + 1)) holds (Z . (j + 1)) = ((Z . j) + v) by RLVECT_1:def 12;



       A11: ( Sum G) = (Z . ( len F)) by A1, A3, A6, A8, Th9;

      now

        let j be Nat, v be Element of T such that

         A12: j < ( len F) and

         A13: v = (F . (j + 1));



         A14: ( len F) = ( len G) by A1, A3, A6, Th9;



         A15: ( dom F) = ( dom G) by A1, A3, A6, Th9, FINSEQ_3: 29;

        (j + 1) <= ( len F) by A12, NAT_1: 13;

        then

         A16: (j + 1) in ( dom F) by NAT_1: 11, FINSEQ_3: 25;



        then (F . (j + 1)) = (( In ((f . ((j + 1) -' 1)),T)) * (( power T) . (( In (a,T)),((j + 1) -' 1)))) by A4

        .= (G . (j + 1)) by A1, A7, A15, A16;

        hence (Z . (j + 1)) = ((Z . j) + v) by A10, A12, A13, A14;

      end;

      hence thesis by A2, A5, A9, A11, RLVECT_1:def 12;

    end;

    theorem :: LIOUVIL2:15



     Th16: for R be Ring, S be Subring of R holds for f be Polynomial of S holds for r be Element of R, s be Element of S st r = s holds ( Ext_eval (f,r)) = ( Ext_eval (f,s))

    proof

      let R be Ring;

      let S be Subring of R;

      let f be Polynomial of S;

      let r be Element of R;

      let s be Element of S;

      assume

       A1: r = s;

      consider F be FinSequence of R such that

       A2: ( Ext_eval (f,r)) = ( Sum F) and

       A3: ( len F) = ( len f) and

       A4: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((f . (n -' 1)),R)) * (( power R) . (r,(n -' 1)))) by ALGNUM_1:def 1;

      consider G be FinSequence of S such that

       A5: ( Ext_eval (f,s)) = ( Sum G) and

       A6: ( len G) = ( len f) and

       A7: for n be Element of NAT st n in ( dom G) holds (G . n) = (( In ((f . (n -' 1)),S)) * (( power S) . (s,(n -' 1)))) by ALGNUM_1:def 1;

      now

        let n such that

         A8: n in ( dom F);



         A9: ( dom F) = ( dom G) by A3, A6, FINSEQ_3: 29;



         A10: r = ( In (s,R)) by A1;



         A11: ((f . (n -' 1)) * (( power S) . (s,(n -' 1)))) is Element of R by Th7;



        thus (F . n) = (( In ((f . (n -' 1)),R)) * (( power R) . (r,(n -' 1)))) by A4, A8

        .= ( In (((f . (n -' 1)) * (( power S) . (s,(n -' 1)))),R)) by A10, ALGNUM_1: 11

        .= (( In ((f . (n -' 1)),S)) * (( power S) . (s,(n -' 1)))) by A11

        .= (G . n) by A7, A8, A9;

      end;

      then F = G by A3, A6, FINSEQ_2: 9;

      then

       A12: ( In (( Sum G),R)) = ( Sum F) by ALGNUM_1: 10;

      ( Sum G) is Element of R by Th7;

      hence ( Ext_eval (f,r)) = ( Ext_eval (f,s)) by A2, A5, A12;

    end;

    theorem :: LIOUVIL2:16

    for R be Ring, S be Subring of R holds for r be Element of R, s be Element of S st r = s & s is_integral_over S holds r is_integral_over R

    proof

      let R be Ring;

      let S be Subring of R;

      let r be Element of R;

      let s be Element of S;

      assume

       A1: r = s;

      given f be Polynomial of S such that

       A2: ( LC f) = ( 1. S) and

       A3: ( Ext_eval (f,s)) = ( 0. S);

      reconsider f1 = f as Polynomial of R by Th8;

      take f1;

      ( LC f) = ( LC f1) by Th9;

      hence ( LC f1) = ( 1. R) by A2, C0SP1:def 3;

      r = ( In (r,R));



      then ( Ext_eval (f1,r)) = ( Ext_eval (f,r)) by Th15

      .= ( Ext_eval (f,s)) by A1, Th16;

      hence ( Ext_eval (f1,r)) = ( 0. R) by A3, C0SP1:def 3;

    end;

    theorem :: LIOUVIL2:17



     Th18: for R be Ring, S be Subring of R holds for r be Element of R, s be Element of S holds for f be Polynomial of R, g be Polynomial of S st r = s & f = g & r is_a_root_of f holds s is_a_root_of g

    proof

      let R be Ring;

      let S be Subring of R;

      let r be Element of R, s be Element of S;

      let f be Polynomial of R, g be Polynomial of S;

      assume that

       A1: r = s and

       A2: f = g and

       A3: ( eval (f,r)) = ( 0. R);

      consider F be FinSequence of R such that

       A4: ( eval (f,r)) = ( Sum F) and

       A5: ( len F) = ( len f) and

       A6: for n be Element of NAT st n in ( dom F) holds (F . n) = ((f . (n -' 1)) * (( power R) . (r,(n -' 1)))) by POLYNOM4:def 2;



       A7: for n be Element of NAT st n in ( dom F) holds (F . n) = ((g . (n -' 1)) * (( power S) . (s,(n -' 1))))

      proof

        let n be Element of NAT such that

         A8: n in ( dom F);



         A9: ((g . (n -' 1)) * (( power S) . (s,(n -' 1)))) is Element of R by Th7;



        thus (F . n) = ((f . (n -' 1)) * (( power R) . (r,(n -' 1)))) by A6, A8

        .= (( In ((g . (n -' 1)),R)) * (( power R) . (( In (s,R)),(n -' 1)))) by A1, A2

        .= ( In (((g . (n -' 1)) * (( power S) . (s,(n -' 1)))),R)) by ALGNUM_1: 11

        .= ((g . (n -' 1)) * (( power S) . (s,(n -' 1)))) by A9;

      end;

      ( rng F) c= the carrier of S

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider n be object such that

         A10: n in ( dom F) and

         A11: (F . n) = y by FUNCT_1:def 3;

        reconsider n as Element of NAT by A10;

        (F . n) = ((g . (n -' 1)) * (( power S) . (s,(n -' 1)))) by A7, A10;

        hence thesis by A11;

      end;

      then

      reconsider G = F as FinSequence of S by FINSEQ_1:def 4;



       A12: ( len G) = ( len g) by A2, A5, Th9;

      ( Sum G) is Element of R by Th7;



      then ( Sum G) = ( In (( Sum G),R))

      .= ( Sum F) by ALGNUM_1: 10

      .= ( 0. S) by A3, A4, C0SP1:def 3;

      hence ( eval (g,s)) = ( 0. S) by A7, A12, POLYNOM4:def 2;

    end;

    theorem :: LIOUVIL2:18



     Th19: for R be Ring holds R is Subring of R

    proof

      let R be Ring;

      thus the carrier of R c= the carrier of R;

      thus thesis;

    end;



     Lm1: ( 0. FC) = 0 by COMPLFLD:def 1;



     Lm2: ( 1. FC) = 1 by COMPLFLD:def 1;



     Lm3: FC is Subring of FC by Th19;

    registration

      cluster ( 0_. F_Complex ) -> INT -valued;

      coherence by Lm1;

      cluster ( 1_. F_Complex ) -> INT -valued;

      coherence

      proof



         A1: ( rng ( 1_. FC)) c= (( rng ( 0_. FC)) \/ {( 1. FC)}) by FUNCT_7: 100;

        ( 1. FC) = 1 by COMPLFLD:def 1;

        hence ( rng ( 1_. FC)) c= INT by A1, INT_1:def 2;

      end;

    end

    registration

      let L be non degenerated non empty doubleLoopStr;

      cluster monic -> non-zero for Polynomial of L;

      coherence ;

    end

    registration

      cluster monic INT -valued for Polynomial of F_Complex ;

      existence

      proof

        take ( 1_. FC);

        thus thesis;

      end;

      cluster monic RAT -valued for Polynomial of F_Complex ;

      existence

      proof

        take ( 1_. FC);

        thus thesis;

      end;

      cluster monic REAL -valued for Polynomial of F_Complex ;

      existence

      proof

        take ( 1_. FC);

        thus thesis;

      end;

    end

    theorem :: LIOUVIL2:19



     Th20: for f be INT -valued Polynomial of F_Complex holds f is Polynomial of INT.Ring

    proof

      let f be INT -valued Polynomial of FC;

      ( rng f) c= INT by RELAT_1:def 19;

      then

      reconsider f1 = f as sequence of IR by FUNCT_2: 6;

      f1 is finite-Support by Lm1, ALGSEQ_1:def 1;

      hence thesis;

    end;

    theorem :: LIOUVIL2:20



     Th21: for f be RAT -valued Polynomial of F_Complex holds f is Polynomial of F_Rat

    proof

      let f be RAT -valued Polynomial of FC;

      ( rng f) c= RAT by RELAT_1:def 19;

      then

      reconsider f1 = f as sequence of Fq by FUNCT_2: 6;

      f1 is finite-Support by Lm1, ALGSEQ_1:def 1;

      hence thesis;

    end;

    theorem :: LIOUVIL2:21



     Th22: for f be REAL -valued Polynomial of F_Complex holds f is Polynomial of F_Real

    proof

      let f be REAL -valued Polynomial of FC;

      ( rng f) c= REAL ;

      then

      reconsider f1 = f as sequence of FR by FUNCT_2: 6;

      f1 is finite-Support by Lm1, ALGSEQ_1:def 1;

      hence thesis;

    end;

    registration

      let L be non empty ZeroStr;

      cluster non-zero -> non zero for Polynomial of L;

      correctness ;

      cluster zero -> non non-zero for Polynomial of L;

      correctness ;

    end

    theorem :: LIOUVIL2:22



     Th23: for i be Integer holds for f be INT -valued FinSequence st i in ( rng f) holds i divides ( Product f)

    proof

      defpred P[ FinSequence of INT ] means for a be Integer st a in ( rng $1) holds a divides ( Product $1);



       A1: for p be FinSequence of INT , n be Element of INT st P[p] holds P[(p ^ <*n*>)]

      proof

        let p be FinSequence of INT , n be Element of INT such that

         A2: P[p];

        set p1 = (p ^ <*n*>);



         A3: ( rng p1) = (( rng p) \/ ( rng <*n*>)) by FINSEQ_1: 31;



         A4: ( Product p1) = (( Product p) * n) by RVSUM_1: 96;

        let a be Integer such that

         A5: a in ( rng p1);

        per cases by A5, A3, XBOOLE_0:def 3;

          suppose a in ( rng p);

          hence thesis by A2, A4, INT_2: 2;

        end;

          suppose a in ( rng <*n*>);

          then a in {n} by FINSEQ_1: 39;

          then a = n by TARSKI:def 1;

          hence thesis by A4;

        end;

      end;



       A6: P[( <*> INT ) qua FinSequence of INT ];



       A7: for p be FinSequence of INT holds P[p] from FINSEQ_2:sch 2( A6, A1);

      let i be Integer;

      let f be INT -valued FinSequence;

      ( rng f) c= INT by RELAT_1:def 19;

      then

      reconsider g = f as FinSequence of INT by FINSEQ_1:def 4;

       P[g] by A7;

      hence thesis;

    end;

    theorem :: LIOUVIL2:23



     Th24: (ex f be non-zero INT -valued Polynomial of F_Complex st c is_a_root_of f) iff (ex f be monic RAT -valued Polynomial of F_Complex st c is_a_root_of f)

    proof

      thus (ex f be non-zero INT -valued Polynomial of FC st c is_a_root_of f) implies (ex f be monic RAT -valued Polynomial of FC st c is_a_root_of f)

      proof

        given f be non-zero INT -valued Polynomial of FC such that

         A1: c is_a_root_of f;

        f <> ( 0_. FC);

        then

         A2: ( len f) <> 0 by POLYNOM4: 5;

        ( rng ( NormPolynomial f)) c= RAT

        proof

          let o be object;

          assume o in ( rng ( NormPolynomial f));

          then

          consider x be object such that

           A3: x in ( dom ( NormPolynomial f)) & o = (( NormPolynomial f) . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A3;

          reconsider fix = (f . x), fil = (f . (( len f) -' 1)) as Integer;



           A4: (f . (( len f) -' 1)) = ( LC f);

          o = ((f . x) / (f . (( len f) -' 1))) by A3, POLYNOM5:def 11

          .= (fix / fil) by A4, COMPLFLD: 6;

          hence o in RAT by RAT_1:def 1;

        end;

        then

        reconsider g = ( NormPolynomial f) as monic RAT -valued Polynomial of FC by RELAT_1:def 19;

        take g;

        thus c is_a_root_of g by A1, A2, POLYNOM5: 59;

      end;

      given f be monic RAT -valued Polynomial of FC such that

       A5: c is_a_root_of f;

      f <> ( 0_. FC);

      then

       A6: ( len f) <> 0 by POLYNOM4: 5;

      reconsider lf = ( len f) as Element of NAT ;

      deffunc F( Element of NAT ) = ( In (( denominator (f . $1)),FC));

      consider d be Polynomial of FC such that

       A7: ( len d) <= lf & for n be Element of NAT st n < lf holds (d . n) = F(n) from POLYNOM3:sch 2;

      now

        assume

         A8: ( len d) < lf;

        then

        reconsider lf1 = (lf - 1) as Element of NAT by NAT_1: 20;

        ( len d) < (lf1 + 1) by A8;

        then

         A9: ( len d) <= lf1 by NAT_1: 13;

        (d . lf1) = F(lf1) by A7, XREAL_1: 44;

        then (d . lf1) <> ( 0. FC) by COMPLFLD:def 1;

        hence contradiction by A9, ALGSEQ_1: 8;

      end;

      then

       A10: ( len d) = ( len f) by A7, XXREAL_0: 1;

      deffunc G( Nat) = (d . ($1 -' 1));

      consider df be FinSequence such that

       A11: ( len df) = ( len d) & for k be Nat st k in ( dom df) holds (df . k) = G(k) from FINSEQ_1:sch 2;



       A12: ( rng df) c= INT

      proof

        let o be object;

        assume o in ( rng df);

        then

        consider a be object such that

         A13: a in ( dom df) & o = (df . a) by FUNCT_1:def 3;

        reconsider a as Element of NAT by A13;



         A14: 1 <= a & a <= ( len df) by A13, FINSEQ_3: 25;

        then (a -' 1) = (a - 1) by XREAL_0:def 2;

        then

         A15: (a -' 1) < ( len f) by A10, A11, A14, XREAL_1: 231;

        (df . a) = (d . (a -' 1)) by A13, A11

        .= ( In (( denominator (f . (a -' 1))),FC)) by A15, A7

        .= ( denominator (f . (a -' 1)));

        hence o in INT by A13, INT_1:def 2;

      end;

      then

      reconsider df as INT -valued FinSequence by RELAT_1:def 19;

      ( rng df) c= COMPLEX by A12, NUMBERS: 16;

      then ( rng df) c= the carrier of FC by COMPLFLD:def 1;

      then

      reconsider dfc = df as FinSequence of FC by FINSEQ_1:def 4;

      ( Product df) in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider dd = ( Product df) as Element of FC by COMPLFLD:def 1;



       A16: for i be Nat st i in ( dom dfc) holds (dfc . i) <> ( 0. FC)

      proof

        let i be Nat;

        assume

         A17: i in ( dom dfc);

        then

        reconsider a = i as Element of NAT ;



         A18: 1 <= a & a <= ( len df) by A17, FINSEQ_3: 25;

        then (a -' 1) = (a - 1) by XREAL_0:def 2;

        then

         A19: (a -' 1) < ( len f) by A10, A11, A18, XREAL_1: 231;

        (df . a) = (d . (a -' 1)) by A17, A11

        .= ( In (( denominator (f . (a -' 1))),FC)) by A19, A7

        .= ( denominator (f . (a -' 1)));

        hence (dfc . i) <> ( 0. FC) by COMPLFLD:def 1;

      end;



       A20: the multF of FC = multcomplex & the carrier of FC = COMPLEX by COMPLFLD:def 1;

      consider dfo be FinSequence of COMPLEX such that

       A21: dfo = df & ( Product df) = ( multcomplex $$ dfo) by RVSUM_1:def 13;

      ( Product df) = ( Product dfc) by A20, A21, GROUP_4:def 2;

      then

       A22: ( len (dd * f)) > 0 by A16, A6, POLYNOM5: 25, RING_2: 2;

      ( rng (dd * f)) c= INT

      proof

        let o be object;

        assume o in ( rng (dd * f));

        then

        consider a be object such that

         A23: a in ( dom (dd * f)) & o = ((dd * f) . a) by FUNCT_1:def 3;

        reconsider a as Element of NAT by A23;



         A24: o = (dd * (f . a)) by A23, POLYNOM5:def 4

        .= (( Product df) * (f . a));

        per cases ;

          suppose a >= ( len f);

          then (f . a) = ( 0. FC) by ALGSEQ_1: 8;



          then o = (( Product df) * 0 ) by A24, COMPLFLD:def 1

          .= 0 ;

          hence o in INT by INT_1:def 2;

        end;

          suppose

           A25: a < ( len f);

          then

           A26: 1 <= (a + 1) & (a + 1) <= ( len df) by A11, A10, NAT_1: 12, NAT_1: 13;

          then

           A27: (a + 1) in ( dom df) by FINSEQ_3: 25;

          (df . (a + 1)) = (d . ((a + 1) -' 1)) by A11, A26, FINSEQ_3: 25

          .= (d . a) by NAT_D: 34

          .= ( In (( denominator (f . a)),FC)) by A25, A7

          .= ( denominator (f . a));

          then ( denominator (f . a)) in ( rng df) by A27, FUNCT_1:def 3;

          then ( denominator (f . a)) divides ( Product df) by Th23;

          then

          consider j be Integer such that

           A28: ( Product df) = (( denominator (f . a)) * j);

          (f . a) = (( numerator (f . a)) / ( denominator (f . a))) by RAT_1: 15;

          then o = (j * ( numerator (f . a))) by A28, A24, XCMPLX_1: 90;

          hence o in INT by INT_1:def 2;

        end;

      end;

      then

      reconsider g = (dd * f) as non-zero INT -valued Polynomial of FC by RELAT_1:def 19, UPROOTS: 17, A22;

      take g;

      ( eval (g,c)) = (dd * ( 0. FC)) by A5, POLYNOM5: 30;

      hence c is_a_root_of g;

    end;

    theorem :: LIOUVIL2:24



     Th25: c is algebraic iff ex f be monic RAT -valued Polynomial of F_Complex st c is_a_root_of f

    proof

      hereby

        assume c is algebraic;

        then c is_integral_over Fq;

        then

        consider f be Polynomial of Fq such that

         A1: ( LC f) = ( 1. Fq) and

         A2: ( Ext_eval (f,c)) = ( 0. FC);

        reconsider f1 = f as RAT -valued Polynomial of FC by ALGNUM_1: 3, Th8;

        f1 is monic by A1, Th9, Lm2, ALGNUM_1: 3;

        then

        reconsider f1 as monic RAT -valued Polynomial of FC;

        take f1;

        thus c is_a_root_of f1

        proof



          thus ( eval (f1,c)) = ( In (( eval (f1,c)),FC))

          .= ( Ext_eval (f1,( In (c,FC)))) by Lm3, ALGNUM_1: 12

          .= ( 0. FC) by A2, Th15, ALGNUM_1: 3;

        end;

      end;

      given f1 be monic RAT -valued Polynomial of FC such that

       A3: c is_a_root_of f1;

      reconsider f = f1 as Polynomial of Fq by Th21;

      take f;

      ( LC f1) = ( 1. FC) by RATFUNC1:def 7;

      hence ( LC f) = ( 1. Fq) by Th9, Lm2, ALGNUM_1: 3;



      thus ( Ext_eval (f,c)) = ( Ext_eval (f1,( In (c,FC)))) by Th15, ALGNUM_1: 3

      .= ( In (( eval (f1,c)),FC)) by Lm3, ALGNUM_1: 12

      .= ( 0. FC) by A3;

    end;

    theorem :: LIOUVIL2:25



     Th26: c is algebraic iff ex f be non-zero INT -valued Polynomial of F_Complex st c is_a_root_of f

    proof

      hereby

        assume c is algebraic;

        then ex f be monic RAT -valued Polynomial of FC st c is_a_root_of f by Th25;

        hence ex f be non-zero INT -valued Polynomial of FC st c is_a_root_of f by Th24;

      end;

      assume ex f be non-zero INT -valued Polynomial of FC st c is_a_root_of f;

      then ex f be monic RAT -valued Polynomial of FC st c is_a_root_of f by Th24;

      hence thesis by Th25;

    end;

    theorem :: LIOUVIL2:26



     Th27: c is algebraic_integer iff ex f be monic INT -valued Polynomial of F_Complex st c is_a_root_of f

    proof

      hereby

        assume c is algebraic_integer;

        then c is_integral_over IR;

        then

        consider f be Polynomial of IR such that

         A1: ( LC f) = ( 1. IR) and

         A2: ( Ext_eval (f,c)) = ( 0. FC);

        reconsider f1 = f as RAT -valued Polynomial of FC by ALGNUM_1: 4, Th8;

        f1 is monic by A1, Th9, Lm2, ALGNUM_1: 4;

        then

        reconsider f1 as monic INT -valued Polynomial of FC;

        take f1;

        thus c is_a_root_of f1

        proof



          thus ( eval (f1,c)) = ( In (( eval (f1,c)),FC))

          .= ( Ext_eval (f1,( In (c,FC)))) by Lm3, ALGNUM_1: 12

          .= ( 0. FC) by A2, Th15, ALGNUM_1: 4;

        end;

      end;

      given f1 be monic INT -valued Polynomial of FC such that

       A3: c is_a_root_of f1;

      reconsider f = f1 as Polynomial of IR by Th20;

      take f;

      ( LC f1) = ( 1. FC) by RATFUNC1:def 7;

      hence ( LC f) = ( 1. IR) by Th9, Lm2, ALGNUM_1: 4;



      thus ( Ext_eval (f,c)) = ( Ext_eval (f1,( In (c,FC)))) by Th15, ALGNUM_1: 4

      .= ( In (( eval (f1,c)),FC)) by Lm3, ALGNUM_1: 12

      .= ( 0. FC) by A3;

    end;

    registration

      cluster algebraic_integer -> algebraic for Complex;

      coherence

      proof

        let c be Complex;

        assume

         A1: c is algebraic_integer;

        c in COMPLEX by XCMPLX_0:def 2;

        then

        reconsider c as Element of FC by COMPLFLD:def 1;

        ex f be monic INT -valued Polynomial of FC st c is_a_root_of f by A1, Th27;

        hence thesis by Th26;

      end;

      cluster transcendental -> non algebraic_integer for Complex;

      coherence ;

    end

    ::$Notion-Name

    theorem :: LIOUVIL2:27



     Th28: for f be non-zero INT -valued Polynomial of F_Real holds for a be irrational Element of F_Real st a is_a_root_of f holds ex A be positive Real st for p be Integer, q be positive Nat holds |.(a - (p / q)).| > (A / (q |^ ( len f)))

    proof

      let f be non-zero INT -valued Polynomial of FR;

      set n = ( len f);

      let a be irrational Element of FR;

      assume

       A1: a is_a_root_of f;

      set X = [.(a - 1), (a + 1).];

      set E = ( Eval f);

      set F = ((E `| ) | X);

      set M1 = ( sup ( rng |.F.|));



       A2: ( dom E) = REAL by FUNCT_2:def 1;



       A3: E is differentiable;



       A4: ( dom (E `| )) = REAL by FUNCT_2:def 1;

      then

       A5: ( dom F) = X by RELAT_1: 62;



       A6: ( dom |.F.|) = ( dom F) by VALUED_1:def 11;

      reconsider F as PartFunc of X, REAL by RELAT_1: 185;

      F is bounded by A4, INTEGRA5: 10;

      then ( rng |.F.|) is real-bounded by INTEGRA1: 15;

      then

      reconsider M1 as Element of REAL by XXREAL_2: 16;

      set M = (M1 + 1);

      consider Y be object such that

       A7: Y in ( rng |.F.|) by XBOOLE_0:def 1;

      reconsider Y as Real by A7;

      consider A be 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 ) <= M by XREAL_1: 6;

      set RTS = (( Roots f) \ {a});

      deffunc F( Real) = |.(a - $1).|;

      set DIF = { F(b) where b be Element of FR : b in RTS };



       A12: RTS is finite;



       A13: DIF is finite from FRAENKEL:sch 21( A12);

      DIF c= REAL

      proof

        let x be object;

        assume x in DIF;

        then ex b be Element of FR st x = F(b) & b in RTS;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider DIF as finite Subset of REAL by A13;

      set MIN = ( {1, (1 / M)} \/ DIF);

      MIN c= REAL by XREAL_0:def 1;

      then

      reconsider MIN as finite non empty Subset of REAL ;

      for x be Real st x in MIN holds x > 0

      proof

        let x be Real;

        assume x in MIN;

        then x in {1, (1 / M)} or x in DIF by XBOOLE_0:def 3;

        per cases by TARSKI:def 2;

          suppose x = 1 or x = (1 / M);

          hence thesis by A10, A9, A8;

        end;

          suppose ex b be Element of FR st x = F(b) & b in RTS;

          then

          consider b be Element of FR such that

           A14: x = F(b) and

           A15: b in RTS;

          (a - b) <> 0 by A15, ZFMISC_1: 56;

          hence thesis by A14;

        end;

      end;

      then ( min MIN) > 0 by XXREAL_2:def 5;

      then

      consider A be Real such that

       A16: 0 < A and

       A17: A < ( inf MIN) by XREAL_1: 5;

      reconsider A as positive Real by A16;

      take A;

      let p be Integer;

      let q be positive Nat;

      set qn = (q |^ n);

      reconsider qtn = qn as Element of FR by XREAL_0:def 1;

      assume

       A18: |.(a - (p / q)).| <= (A / qn);



       A19: |.(a - (p / q)).| = |.((p / q) - a).| by COMPLEX1: 60;



       A20: (E . a) = ( 0. FR) by A1, POLYNOM5:def 13;

      reconsider pq = (p / q) as Element of FR by XREAL_0:def 1;

      ( 0 + 1) <= qn by NAT_1: 13;

      then (A / qn) <= (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 RTS;

      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: (E . (p / q)) = ( eval (f,pq)) & (E . a) = ( eval (f,a)) by POLYNOM5:def 13;



       A24: (a + 0 ) <= (a + 1) by XREAL_1: 6;



       A25: (1 / (M * qn)) = ((1 / M) * (1 / qn)) by XCMPLX_1: 102;

      (1 / M) in {1, (1 / M)} by TARSKI:def 2;

      then (1 / M) in MIN by XBOOLE_0:def 3;

      then ( inf MIN) <= (1 / M) by XXREAL_2: 3;

      then A < (1 / M) by A17, XXREAL_0: 2;

      then

       A26: (A * (1 / qn)) < ((1 / M) * (1 / qn)) by XREAL_1: 68;

      1 in {1, (1 / M)} 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 be FinSequence of the carrier of FR such that

       A28: (E . (p / q)) = ( Sum EF) & ( len EF) = ( len f) & for n be Element of NAT st n in ( dom EF) holds (EF . n) = ((f . (n -' 1)) * (( power FR) . (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 GG) = ( len EF) by FINSEQ_2: 132;



      then

       A29: ( dom G) = ( Seg ( len EF)) by FINSEQ_1:def 3

      .= ( dom EF) by FINSEQ_1:def 3;

      ( rng G) c= INT

      proof

        let o be object;

        assume o in ( rng G);

        then

        consider b be object such that

         A30: b in ( dom G) & o = (G . b) by FUNCT_1:def 3;

        reconsider b as Element of NAT by A30;

        b in ( Seg n) by A30, A29, A28, FINSEQ_1:def 3;

        then 1 <= b & b <= n & (b -' 1) <= b by FINSEQ_1: 1, NAT_D: 35;

        then

        consider c be Nat such that

         A31: n = ((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 (G . b) = (qtn * ((f . (b -' 1)) * (( power F_Real ) . (pq,(b -' 1))))) by A28, A30, A29

        .= ((f . (b -' 1)) * ((q |^ n) * (( power F_Real ) . (pq,(b -' 1)))))

        .= ((f . (b -' 1)) * ((q |^ n) * ((p / q) |^ (b -' 1)))) by NIVEN: 7

        .= ((f . (b -' 1)) * ((q |^ n) * ((p |^ (b -' 1)) / (q |^ (b -' 1))))) by PREPOWER: 8

        .= (((f . (b -' 1)) * (p |^ (b -' 1))) * ((q |^ n) / (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;

      end;

      then

      reconsider G1 = G as INT -valued FinSequence by RELAT_1:def 19;

      ( Sum G1) = ( Sum G) by NIVEN: 6;

      then

      reconsider SG = ( Sum G) as Integer;

      ( Sum G) = (qtn * ( Sum EF)) by FVSUM_1: 73

      .= (qn * ( Sum EF));

      then |.SG.| = ( |.qn.| * |.( Sum EF).|) by COMPLEX1: 65;

      then

       A32: |.(E . (p / q)).| >= (1 / qn) by A28, A22, A23, NAT_1: 14, XREAL_1: 79;

      per cases by XXREAL_0: 1;

        suppose

         A33: (p / q) < a;

        (E | [.(p / q), a.]) is continuous;

        then

        consider x0 be Real such that

         A34: x0 in ].(p / q), a.[ and

         A35: ( diff (E,x0)) = (((E . a) - (E . (p / q))) / (a - (p / q))) by A2, A3, A33, FDIFF_1: 26, ROLLE: 3;



         A36: |.((E . a) - (E . (p / q))).| = |.(E . (p / q)).| by A20, COMPLEX1: 52;



         A37: (a - (p / q)) <> 0 ;

        then (a - (p / q)) = (((E . a) - (E . (p / q))) / ( diff (E,x0))) by A35, A1, A22, A23, XCMPLX_1: 54;

        then

         A38: |.(a - (p / q)).| = ( |.(E . (p / q)).| / |.( diff (E,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= X by A24, XXREAL_1: 37;



        then

         A40: (F . x0) = ((E `| ) . x0) by A34, FUNCT_1: 49

        .= ( diff (E,x0)) by POLYDIFF: 10;

        ( |.F.| . x0) = |.(F . x0).| by VALUED_1: 18;

        then |.( diff (E,x0)).| in ( rng |.F.|) by A5, A6, A34, A39, A40, FUNCT_1:def 3;

        then |.( diff (E,x0)).| <= M1 by XXREAL_2: 4;

        then |.( diff (E,x0)).| <= M by A11, XXREAL_0: 2;

        then (1 / |.( diff (E,x0)).|) >= (1 / M) by A35, A1, A37, A22, A23, XREAL_1: 118;

        then ( |.(E . (p / q)).| / |.( diff (E,x0)).|) >= (1 / (M * qn)) by A10, A9, A8, A32, A25, XREAL_1: 66;

        hence contradiction by A18, A38, A25, A26, XXREAL_0: 2;

      end;

        suppose

         A41: a < (p / q);

        (E | [.a, (p / q).]) is continuous;

        then

        consider x0 be Real such that

         A42: x0 in ].a, (p / q).[ and

         A43: ( diff (E,x0)) = (((E . (p / q)) - (E . a)) / ((p / q) - a)) by A2, A3, A41, FDIFF_1: 26, ROLLE: 3;



         A44: ((p / q) - a) <> 0 ;

        then ((p / q) - a) = (((E . (p / q)) - (E . a)) / ( diff (E,x0))) by A1, A22, A23, A43, XCMPLX_1: 54;

        then

         A45: |.((p / q) - a).| = ( |.(E . (p / q)).| / |.( diff (E,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= X by A46, XXREAL_1: 37;



        then

         A48: (F . x0) = ((E `| ) . x0) by A42, FUNCT_1: 49

        .= ( diff (E,x0)) by POLYDIFF: 10;

        ( |.F.| . x0) = |.(F . x0).| by VALUED_1: 18;

        then |.( diff (E,x0)).| in ( rng |.F.|) by A5, A6, A42, A47, A48, FUNCT_1:def 3;

        then |.( diff (E,x0)).| <= M1 by XXREAL_2: 4;

        then |.( diff (E,x0)).| <= M by A11, XXREAL_0: 2;

        then (1 / |.( diff (E,x0)).|) >= (1 / M) by A43, A1, A22, A44, A23, XREAL_1: 118;

        then ( |.(E . (p / q)).| / |.( diff (E,x0)).|) >= (1 / (M * qn)) by A10, A9, A8, A25, A32, XREAL_1: 66;

        hence contradiction by A18, A19, A45, A25, A26, XXREAL_0: 2;

      end;

    end;

     Lm4:

    now

      let n;

      let L be Liouville;

      let A be positive Real such that

       A1: for p be Integer, q be positive Nat holds |.(L - (p / q)).| > (A / (q |^ n));

      consider r be positive Nat such that

       A2: (1 / (2 |^ r)) <= A by Th3;

      consider p be Integer, q be Nat such that

       A3: 1 < q and 0 < |.(L - (p / q)).| and

       A4: |.(L - (p / q)).| < (1 / (q |^ (r + n))) by LIOUVIL1:def 5;



       A5: (q |^ (r + n)) = ((q |^ r) * (q |^ n)) by NEWTON: 8;

      (1 + 1) <= q by A3, NAT_1: 13;

      then (2 |^ r) <= (q |^ r) by PREPOWER: 9;

      then

       A6: (1 / (2 |^ r)) >= (1 / (q |^ r)) by XREAL_1: 118;

      (1 / ((q |^ r) * (q |^ n))) = ((1 / (q |^ r)) * (1 / (q |^ n))) by XCMPLX_1: 102;

      then

       A7: (1 / ((q |^ r) * (q |^ n))) <= ((1 / (2 |^ r)) * (1 / (q |^ n))) by A6, XREAL_1: 64;

      ((1 / (2 |^ r)) * (1 / (q |^ n))) <= (A * (1 / (q |^ n))) by A2, XREAL_1: 64;

      then (1 / ((q |^ r) * (q |^ n))) <= (A / (q |^ n)) by A7, XXREAL_0: 2;

      hence contradiction by A1, A3, A4, A5, XXREAL_0: 2;

    end;

    ::$Notion-Name

    registration

      cluster -> transcendental for Liouville;

      coherence

      proof

        let L be Liouville;

        assume L is algebraic;

        then

        consider f be non-zero INT -valued Polynomial of FC such that

         A1: ( In (L,FC)) is_a_root_of f by Th26;

        reconsider g = f as non-zero INT -valued Polynomial of FR by Th4, Th13, Th22;

        L is irrational Element of FR by XREAL_0:def 1;

        then ex A be positive Real st for p be Integer, q be positive Nat holds |.(L - (p / q)).| > (A / (q |^ ( len g))) by A1, Th4, Th18, Th28;

        hence thesis by Lm4;

      end;

    end