niven.miz



    begin

    reserve r,t for Real;

    reserve i for Integer;

    reserve k,n for Nat;

    reserve p for Polynomial of F_Real ;

    reserve e for Element of F_Real ;

    reserve L for non empty ZeroStr;

    reserve z,z0,z1,z2 for Element of L;

    

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

    

     Lm2: (3 -' 1) = (3 - 1) by XREAL_0:def 2;

    theorem :: NIVEN:1

    

     Th1: for a,b,c,d be Complex st b <> 0 & (a / b) = (c / d) holds a = ((b * c) / d)

    proof

      let a,b,c,d be Complex;

      assume that

       A1: b <> 0 and

       A2: (a / b) = (c / d);

      

      thus a = (b * (a / b)) by A1, XCMPLX_1: 87

      .= ((b * c) / d) by A2, XCMPLX_1: 74;

    end;

    theorem :: NIVEN:2

    

     Th2: for a,b be Real st |.a.| = b holds a = b or a = ( - b)

    proof

      let a be Real;

       |.a.| = a or |.a.| = ( - a) by COMPLEX1: 71;

      hence thesis;

    end;

    theorem :: NIVEN:3

    

     Th3: |.i.| <= 2 implies i = ( - 2) or i = ( - 1) or i = 0 or i = 1 or i = 2

    proof

      assume |.i.| <= 2;

      then |.i.| = 0 or ... or |.i.| = 2;

      hence thesis by ABSVALUE: 2, Th2;

    end;

    theorem :: NIVEN:4

    

     Th4: n <> 0 implies i divides (i |^ n)

    proof

      assume n <> 0 ;

      then

      consider b be Nat such that

       A1: n = (b + 1) by NAT_1: 6;

      reconsider b as Element of NAT by ORDINAL1:def 12;

      (i |^ 1) divides (i |^ (b + 1)) by NAT_1: 12, NEWTON03: 16;

      hence thesis by A1;

    end;

    theorem :: NIVEN:5

    

     Th16: t > 0 implies ex i st (t * i) <= r <= (t * (i + 1))

    proof

      assume

       A0: t > 0 ;

      defpred P[ Integer] means (t * $1) <= r;

      

       g: ex i1 be Integer st P[i1]

      proof

        take i1 = [\(r / t)/];

        i1 <= (r / t) by INT_1:def 6;

        then (i1 * t) <= ((r / t) * t) by A0, XREAL_1: 64;

        then (t * i1) <= (r / (t / t)) by XCMPLX_1: 82;

        hence (t * i1) <= r by A0, XCMPLX_1: 51;

      end;

      set F = [/(r / t)\];

      

       f: for i1 be Integer st P[i1] holds i1 <= F

      proof

        let i1 be Integer;

        assume P[i1];

        then ((i1 * t) / t) <= (r / t) by A0, XREAL_1: 72;

        then (i1 * (t / t)) <= (r / t);

        then (i1 * 1) <= (r / t) & (r / t) <= [/(r / t)\] by A0, XCMPLX_1: 60, INT_1:def 7;

        hence i1 <= F by XXREAL_0: 2;

      end;

      consider i such that

       i: P[i] & for i1 be Integer st P[i1] holds i1 <= i from INT_1:sch 6( f, g);

      take i;

      thus (t * i) <= r by i;

      (i + 1) > (i + 0 ) by XREAL_1: 6;

      hence r <= (t * (i + 1)) by i;

    end;

    theorem :: NIVEN:6

    

     Th49: for p be FinSequence of F_Real holds for q be real-valued FinSequence st p = q holds ( Sum p) = ( Sum q)

    proof

      defpred P[ FinSequence] means for p be FinSequence of F_Real holds for q be real-valued FinSequence st p = q & p = $1 holds ( Sum p) = ( Sum q);

      

       A1: P[ {} ]

      proof

        let p be FinSequence of F_Real ;

        let q be real-valued FinSequence;

        assume

         A2: p = q & p = {} ;

        then p = ( <*> the carrier of F_Real ) & q = ( <*> REAL );

        

        hence ( Sum p) = ( 0. F_Real ) by RLVECT_1: 43

        .= ( Sum q) by A2, RVSUM_1: 72;

      end;

      

       A3: for f be FinSequence, x be object st P[f] holds P[(f ^ <*x*>)]

      proof

        let f be FinSequence, x be object;

        assume

         A4: P[f];

        thus P[(f ^ <*x*>)]

        proof

          let p1 be FinSequence of F_Real ;

          let q1 be real-valued FinSequence;

          assume

           A5: p1 = q1 & p1 = (f ^ <*x*>);

          reconsider fp = f as FinSequence of F_Real by A5, FINSEQ_1: 36;

          ( rng fp) c= REAL ;

          then

          reconsider fq = f as real-valued FinSequence;

           <*x*> is FinSequence of F_Real by A5, FINSEQ_1: 36;

          then ( rng <*x*>) c= the carrier of F_Real by FINSEQ_1:def 4;

          then {x} c= the carrier of F_Real by FINSEQ_1: 38;

          then

          reconsider xp = x as Element of F_Real by ZFMISC_1: 31;

          reconsider xq = xp as Real;

          

          thus ( Sum p1) = (( Sum fp) + ( Sum <*xp*>)) by A5, RLVECT_1: 41

          .= (( Sum fp) + xp) by RLVECT_1: 44

          .= (( Sum fq) + xq) by A4

          .= ( Sum q1) by A5, RVSUM_1: 74;

        end;

      end;

      let p be FinSequence of F_Real ;

      let q be real-valued FinSequence;

      for f be FinSequence holds P[f] from FINSEQ_1:sch 3( A1, A3);

      hence thesis;

    end;

    theorem :: NIVEN:7

    

     Th48: for i be Nat, r be Element of F_Real holds (( power F_Real ) . (r,i)) = (r |^ i)

    proof

      let i be Nat;

      let r be Element of F_Real ;

      defpred P[ Nat] means (( power F_Real ) . (r,$1)) = (r |^ $1);

      (( power F_Real ) . (r, 0 )) = ( 1_ F_Real ) by GROUP_1:def 7

      .= (r |^ 0 ) by NEWTON: 4;

      then

       A1: P[ 0 ];

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        (( power F_Real ) . (r,(n + 1))) = ((( power F_Real ) . (r,n)) * r) by GROUP_1:def 7

        .= (r |^ (n + 1)) by A3, NEWTON: 6;

        hence P[(n + 1)];

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      hence (( power F_Real ) . (r,i)) = (r |^ i);

    end;

    theorem :: NIVEN:8

    

     Th5: ( sin ((5 * PI ) / 6)) = (1 / 2)

    proof

      ((5 * PI ) / 6) = ( PI - ( PI / 6));

      hence thesis by EUCLID10: 1, EUCLID10: 17;

    end;

    theorem :: NIVEN:9

    ( sin (((5 * PI ) / 6) + ((2 * PI ) * i))) = (1 / 2) by COMPLEX2: 8, Th5;

    theorem :: NIVEN:10

    

     Th7: ( sin ((7 * PI ) / 6)) = ( - (1 / 2))

    proof

      ((7 * PI ) / 6) = ( PI + ( PI / 6));

      hence thesis by EUCLID10: 17, SIN_COS: 79;

    end;

    theorem :: NIVEN:11

    ( sin (((7 * PI ) / 6) + ((2 * PI ) * i))) = ( - (1 / 2)) by COMPLEX2: 8, Th7;

    theorem :: NIVEN:12

    

     Th9: ( sin ((11 * PI ) / 6)) = ( - (1 / 2))

    proof

      ((11 * PI ) / 6) = ((2 * PI ) - ( PI / 6));

      hence thesis by EUCLID10: 3, EUCLID10: 17;

    end;

    theorem :: NIVEN:13

    ( sin (((11 * PI ) / 6) + ((2 * PI ) * i))) = ( - (1 / 2)) by COMPLEX2: 8, Th9;

    theorem :: NIVEN:14

    

     Th11: ( cos ((4 * PI ) / 3)) = ( - (1 / 2))

    proof

      ((4 * PI ) / 3) = ( PI + ( PI / 3));

      hence thesis by EUCLID10: 14, SIN_COS: 79;

    end;

    theorem :: NIVEN:15

    ( cos (((4 * PI ) / 3) + ((2 * PI ) * i))) = ( - (1 / 2)) by COMPLEX2: 9, Th11;

    theorem :: NIVEN:16

    

     Th13: ( cos ((5 * PI ) / 3)) = (1 / 2)

    proof

      ((5 * PI ) / 3) = ( PI + ((2 * PI ) / 3));

      

      hence ( cos ((5 * PI ) / 3)) = ( - ( cos ((2 * PI ) / 3))) by SIN_COS: 79

      .= (1 / 2) by EUCLID10: 23;

    end;

    theorem :: NIVEN:17

    ( cos (((5 * PI ) / 3) + ((2 * PI ) * i))) = (1 / 2) by COMPLEX2: 9, Th13;

    theorem :: NIVEN:18

    

     Th15: 0 <= r <= ( PI / 2) & ( cos r) = (1 / 2) implies r = ( PI / 3)

    proof

      set X = [. 0 , ( PI / 2).];

      set f = ( cos | X);

      assume that

       A1: 0 <= r and

       A2: r <= ( PI / 2);

      

       A3: r in X by A1, A2, XXREAL_1: 1;

      assume

       A4: ( cos r) = (1 / 2);

      

       A5: ( dom cos ) = REAL by FUNCT_2:def 1;

      

       A6: ( PI / 3) <= ( PI / 2) by XREAL_1: 76;

      then

       A7: ( PI / 3) in X by XXREAL_1: 1;

      

       A8: ( dom f) = X by A5, RELAT_1: 62;

      

      then (f . r) = ( cos ( PI / 3)) by A1, A2, A4, EUCLID10: 14, XXREAL_1: 1, FUNCT_1: 47

      .= (f . ( PI / 3)) by A6, A8, XXREAL_1: 1, FUNCT_1: 47;

      hence thesis by A3, A7, A8, FUNCT_1:def 4;

    end;

    theorem :: NIVEN:19

    

     Th17: for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for p be sequence of L holds (( 0_. L) *' p) = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      let p be sequence of L;

      now

        let i be Element of NAT ;

        consider r be FinSequence of L such that ( len r) = (i + 1) and

         A1: ((( 0_. L) *' p) . i) = ( Sum r) and

         A2: for k be Element of NAT st k in ( dom r) holds (r . k) = ((( 0_. L) . (k -' 1)) * (p . ((i + 1) -' k))) by POLYNOM3:def 9;

        now

          let k be Element of NAT ;

          assume k in ( dom r);

          

          hence (r . k) = ((( 0_. L) . (k -' 1)) * (p . ((i + 1) -' k))) by A2

          .= (( 0. L) * (p . ((i + 1) -' k))) by FUNCOP_1: 7

          .= ( 0. L);

        end;

        

        hence ((( 0_. L) *' p) . i) = ( 0. L) by A1, POLYNOM3: 1

        .= (( 0_. L) . i) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2:def 8;

    end;

    registration

      let L, z, n;

      cluster (( 0_. L) +* (n,z)) -> finite-Support;

      coherence

      proof

        let s be sequence of L such that

         A1: s = (( 0_. L) +* (n,z));

        take (n + 1);

        let i be Nat;

        assume (n + 1) <= i;

        then n < i by NAT_1: 13;

        

        hence (s . i) = (( 0_. L) . i) by A1, FUNCT_7: 32

        .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

      end;

    end

    theorem :: NIVEN:20

    

     Th18: z <> ( 0. L) implies for p be Polynomial of L st p = (( 0_. L) +* (n,z)) holds ( len p) = (n + 1)

    proof

      assume

       A1: z <> ( 0. L);

      let p be Polynomial of L;

      assume

       A2: p = (( 0_. L) +* (n,z));

      

       A3: (n + 1) is_at_least_length_of p

      proof

        let i be Nat such that

         A4: i >= (n + 1);

        i > n by A4, NAT_1: 13;

        

        hence (p . i) = (( 0_. L) . i) by A2, FUNCT_7: 32

        .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

      end;

      for m be Nat st m is_at_least_length_of p holds (n + 1) <= m

      proof

        let m be Nat;

        assume

         A5: m is_at_least_length_of p;

        assume

         A6: (n + 1) > m;

        ( dom ( 0_. L)) = NAT by FUNCOP_1: 13;

        then (p . n) = z by A2, ORDINAL1:def 12, FUNCT_7: 31;

        hence contradiction by A1, A5, A6, NAT_1: 13;

      end;

      hence thesis by A3, ALGSEQ_1:def 3;

    end;

    theorem :: NIVEN:21

    z <> ( 0. L) implies for p be Polynomial of L st p = (( 0_. L) +* (n,z)) holds ( deg p) = n

    proof

      assume

       A1: z <> ( 0. L);

      let p be Polynomial of L;

      assume p = (( 0_. L) +* (n,z));

      

      hence ( deg p) = ((n + 1) - 1) by A1, Th18

      .= n;

    end;

    registration

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

      coherence ;

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

      coherence ;

    end

    registration

      cluster integer for Element of F_Real ;

      existence ;

    end

    theorem :: NIVEN:22

    

     Th20: ( rng <%z%>) = {z, ( 0. L)}

    proof

      set p = <%z%>;

      

       A1: (p . 0 ) = z by ALGSEQ_1:def 5;

      

       A2: ( dom p) = NAT by FUNCT_2:def 1;

      thus ( rng p) c= {z, ( 0. L)}

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A3: x in ( dom p) and

         A4: (p . x) = y by FUNCT_1:def 3;

        reconsider x as Element of NAT by A3;

        per cases ;

          suppose x = 0 ;

          hence thesis by A4, A1, TARSKI:def 2;

        end;

          suppose x <> 0 ;

          then (p . x) = ( 0. L) by POLYNOM5: 32, NAT_1: 14;

          hence thesis by A4, TARSKI:def 2;

        end;

      end;

      let y be object;

      assume y in {z, ( 0. L)};

      per cases by TARSKI:def 2;

        suppose y = z;

        hence thesis by A1, A2, FUNCT_1:def 3;

      end;

        suppose

         A5: y = ( 0. L);

        (p . 1) = ( 0. L) by POLYNOM5: 32;

        hence thesis by A2, A5, FUNCT_1:def 3;

      end;

    end;

    definition

      let L, z0, z1, z2;

      :: NIVEN:def1

      func <%z0,z1,z2%> -> sequence of L equals (((( 0_. L) +* ( 0 ,z0)) +* (1,z1)) +* (2,z2));

      coherence ;

    end

    theorem :: NIVEN:23

    

     Th21: ( <%z0, z1, z2%> . 0 ) = z0

    proof

      

       A1: ( dom ( 0_. L)) = NAT by FUNCOP_1: 13;

      

      thus ( <%z0, z1, z2%> . 0 ) = (((( 0_. L) +* ( 0 ,z0)) +* (1,z1)) . 0 ) by FUNCT_7: 32

      .= ((( 0_. L) +* ( 0 ,z0)) . 0 ) by FUNCT_7: 32

      .= z0 by A1, FUNCT_7: 31;

    end;

    theorem :: NIVEN:24

    

     Th22: ( <%z0, z1, z2%> . 1) = z1

    proof

      

       A1: ( dom (( 0_. L) +* ( 0 ,z0))) = ( dom ( 0_. L)) by FUNCT_7: 30

      .= NAT by FUNCOP_1: 13;

      

      thus ( <%z0, z1, z2%> . 1) = (((( 0_. L) +* ( 0 ,z0)) +* (1,z1)) . 1) by FUNCT_7: 32

      .= z1 by A1, FUNCT_7: 31;

    end;

    theorem :: NIVEN:25

    

     Th23: ( <%z0, z1, z2%> . 2) = z2

    proof

      ( dom ((( 0_. L) +* ( 0 ,z0)) +* (1,z1))) = ( dom (( 0_. L) +* ( 0 ,z0))) by FUNCT_7: 30

      .= ( dom ( 0_. L)) by FUNCT_7: 30

      .= NAT by FUNCOP_1: 13;

      hence ( <%z0, z1, z2%> . 2) = z2 by FUNCT_7: 31;

    end;

    theorem :: NIVEN:26

    

     Th24: 3 <= n implies ( <%z0, z1, z2%> . n) = ( 0. L)

    proof

      assume

       A1: 3 <= n;

      then

       A2: n <> 0 & n <> 1 & n <> 2;

      

      hence ( <%z0, z1, z2%> . n) = (((( 0_. L) +* ( 0 ,z0)) +* (1,z1)) . n) by FUNCT_7: 32

      .= ((( 0_. L) +* ( 0 ,z0)) . n) by A2, FUNCT_7: 32

      .= (( 0_. L) . n) by A1, FUNCT_7: 32

      .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

    end;

    registration

      let L, z0, z1, z2;

      cluster <%z0, z1, z2%> -> finite-Support;

      coherence

      proof

        take 3;

        thus thesis by Th24;

      end;

    end

    theorem :: NIVEN:27

    

     Th25: ( len <%z0, z1, z2%>) <= 3

    proof

      3 is_at_least_length_of <%z0, z1, z2%> by Th24;

      hence thesis by ALGSEQ_1:def 3;

    end;

    theorem :: NIVEN:28

    

     Th26: z2 <> ( 0. L) implies ( len <%z0, z1, z2%>) = 3

    proof

      assume z2 <> ( 0. L);

      then ( <%z0, z1, z2%> . 2) <> ( 0. L) by Th23;

      then

       A1: for n be Nat st n is_at_least_length_of <%z0, z1, z2%> holds (2 + 1) <= n by NAT_1: 13;

      3 is_at_least_length_of <%z0, z1, z2%> by Th24;

      hence thesis by A1, ALGSEQ_1:def 3;

    end;

    theorem :: NIVEN:29

    

     Th27: for L be right_zeroed non empty addLoopStr holds for z0,z1 be Element of L holds ( <%z0%> + <%z1%>) = <%(z0 + z1)%>

    proof

      let L be right_zeroed non empty addLoopStr;

      let z0,z1 be Element of L;

      set p = <%z0%>;

      set q = <%z1%>;

      set r = <%(z0 + z1)%>;

      let n be Element of NAT ;

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (q . n) = z1 & (r . n) = (z0 + z1) by POLYNOM5: 32;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n > 0 ;

        then n >= ( 0 + 1) by NAT_1: 13;

        then

         A1: (p . n) = ( 0. L) & (q . n) = ( 0. L) & (r . n) = ( 0. L) by POLYNOM5: 32;

        (( 0. L) + ( 0. L)) = ( 0. L) by RLVECT_1:def 4;

        hence thesis by A1, NORMSP_1:def 2;

      end;

    end;

    theorem :: NIVEN:30

    

     Th28: for L be right_zeroed non empty addLoopStr holds for z0,z1,z2,z3 be Element of L holds ( <%z0, z1%> + <%z2, z3%>) = <%(z0 + z2), (z1 + z3)%>

    proof

      let L be right_zeroed non empty addLoopStr;

      let z0,z1,z2,z3 be Element of L;

      set p = <%z0, z1%>;

      set q = <%z2, z3%>;

      set r = <%(z0 + z2), (z1 + z3)%>;

      let n be Element of NAT ;

      (n = 0 or ... or n = 1) or n > 1;

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (q . n) = z2 & (r . n) = (z0 + z2) by POLYNOM5: 38;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n = 1;

        then (p . n) = z1 & (q . n) = z3 & (r . n) = (z1 + z3) by POLYNOM5: 38;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n > 1;

        then n >= (1 + 1) by NAT_1: 13;

        then

         A1: (p . n) = ( 0. L) & (q . n) = ( 0. L) & (r . n) = ( 0. L) by POLYNOM5: 38;

        (( 0. L) + ( 0. L)) = ( 0. L) by RLVECT_1:def 4;

        hence thesis by A1, NORMSP_1:def 2;

      end;

    end;

    theorem :: NIVEN:31

    

     Th29: for L be right_zeroed non empty addLoopStr holds for z0,z1,z2,z3,z4,z5 be Element of L holds ( <%z0, z1, z2%> + <%z3, z4, z5%>) = <%(z0 + z3), (z1 + z4), (z2 + z5)%>

    proof

      let L be right_zeroed non empty addLoopStr;

      let z0,z1,z2,z3,z4,z5 be Element of L;

      set p = <%z0, z1, z2%>;

      set q = <%z3, z4, z5%>;

      set r = <%(z0 + z3), (z1 + z4), (z2 + z5)%>;

      let n be Element of NAT ;

      (n = 0 or ... or n = 2) or n > 2;

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (q . n) = z3 & (r . n) = (z0 + z3) by Th21;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n = 1;

        then (p . n) = z1 & (q . n) = z4 & (r . n) = (z1 + z4) by Th22;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n = 2;

        then (p . n) = z2 & (q . n) = z5 & (r . n) = (z2 + z5) by Th23;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose n > 2;

        then n >= (2 + 1) by NAT_1: 13;

        then

         A1: (p . n) = ( 0. L) & (q . n) = ( 0. L) & (r . n) = ( 0. L) by Th24;

        (( 0. L) + ( 0. L)) = ( 0. L) by RLVECT_1:def 4;

        hence thesis by A1, NORMSP_1:def 2;

      end;

    end;

    theorem :: NIVEN:32

    

     Th30: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0 be Element of L holds ( - <%z0%>) = <%( - z0)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0 be Element of L;

      set p = <%z0%>;

      set r = <%( - z0)%>;

      let n be Element of NAT ;

      

       A1: ( dom ( - p)) = NAT by FUNCT_2:def 1;

      

       A2: (( - p) . n) = (( - p) /. n)

      .= ( - (p /. n)) by A1, VFUNCT_1:def 5

      .= ( - (p . n));

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (r . n) = ( - z0) by POLYNOM5: 32;

        hence thesis by A2;

      end;

        suppose n > 0 ;

        then n >= ( 0 + 1) by NAT_1: 13;

        then (p . n) = ( 0. L) & (r . n) = ( 0. L) by POLYNOM5: 32;

        hence thesis by A2;

      end;

    end;

    theorem :: NIVEN:33

    

     Th31: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0,z1 be Element of L holds ( - <%z0, z1%>) = <%( - z0), ( - z1)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0,z1 be Element of L;

      set p = <%z0, z1%>;

      set r = <%( - z0), ( - z1)%>;

      let n be Element of NAT ;

      

       A1: ( dom ( - p)) = NAT by FUNCT_2:def 1;

      

       A2: (( - p) . n) = (( - p) /. n)

      .= ( - (p /. n)) by A1, VFUNCT_1:def 5

      .= ( - (p . n));

      (n = 0 or ... or n = 1) or n > 1;

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (r . n) = ( - z0) by POLYNOM5: 38;

        hence thesis by A2;

      end;

        suppose n = 1;

        then (p . n) = z1 & (r . n) = ( - z1) by POLYNOM5: 38;

        hence thesis by A2;

      end;

        suppose n > 1;

        then n >= (1 + 1) by NAT_1: 13;

        then (p . n) = ( 0. L) & (r . n) = ( 0. L) by POLYNOM5: 38;

        hence thesis by A2;

      end;

    end;

    theorem :: NIVEN:34

    

     Th32: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0,z1,z2 be Element of L holds ( - <%z0, z1, z2%>) = <%( - z0), ( - z1), ( - z2)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0,z1,z2 be Element of L;

      set p = <%z0, z1, z2%>;

      set r = <%( - z0), ( - z1), ( - z2)%>;

      let n be Element of NAT ;

      

       A1: ( dom ( - p)) = NAT by FUNCT_2:def 1;

      

       A2: (( - p) . n) = (( - p) /. n)

      .= ( - (p /. n)) by A1, VFUNCT_1:def 5

      .= ( - (p . n));

      (n = 0 or ... or n = 2) or n > 2;

      per cases ;

        suppose n = 0 ;

        then (p . n) = z0 & (r . n) = ( - z0) by Th21;

        hence thesis by A2;

      end;

        suppose n = 1;

        then (p . n) = z1 & (r . n) = ( - z1) by Th22;

        hence thesis by A2;

      end;

        suppose n = 2;

        then (p . n) = z2 & (r . n) = ( - z2) by Th23;

        hence thesis by A2;

      end;

        suppose n > 2;

        then n >= (2 + 1) by NAT_1: 13;

        then (p . n) = ( 0. L) & (r . n) = ( 0. L) by Th24;

        hence thesis by A2;

      end;

    end;

    theorem :: NIVEN:35

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0,z1 be Element of L holds ( <%z0%> - <%z1%>) = <%(z0 - z1)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0,z1 be Element of L;

      

      thus ( <%z0%> - <%z1%>) = ( <%z0%> + <%( - z1)%>) by Th30

      .= <%(z0 - z1)%> by Th27;

    end;

    theorem :: NIVEN:36

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0,z1,z2,z3 be Element of L holds ( <%z0, z1%> - <%z2, z3%>) = <%(z0 - z2), (z1 - z3)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0,z1,z2,z3 be Element of L;

      

      thus ( <%z0, z1%> - <%z2, z3%>) = ( <%z0, z1%> + <%( - z2), ( - z3)%>) by Th31

      .= <%(z0 - z2), (z1 - z3)%> by Th28;

    end;

    theorem :: NIVEN:37

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for z0,z1,z2,z3,z4,z5 be Element of L holds ( <%z0, z1, z2%> - <%z3, z4, z5%>) = <%(z0 - z3), (z1 - z4), (z2 - z5)%>

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let z0,z1,z2,z3,z4,z5 be Element of L;

      

      thus ( <%z0, z1, z2%> - <%z3, z4, z5%>) = ( <%z0, z1, z2%> + <%( - z3), ( - z4), ( - z5)%>) by Th32

      .= <%(z0 - z3), (z1 - z4), (z2 - z5)%> by Th29;

    end;

    theorem :: NIVEN:38

    

     Th36: for L be add-associative right_zeroed right_complementable left-distributive unital associative non empty doubleLoopStr holds for z0,z1,z2,x be Element of L holds ( eval ( <%z0, z1, z2%>,x)) = ((z0 + (z1 * x)) + ((z2 * x) * x))

    proof

      let L be add-associative right_zeroed right_complementable left-distributive unital associative non empty doubleLoopStr;

      let z0,z1,z2,x be Element of L;

      consider F be FinSequence of L such that

       A1: ( eval ( <%z0, z1, z2%>,x)) = ( Sum F) and

       A2: ( len F) = ( len <%z0, z1, z2%>) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( <%z0, z1, z2%> . (n -' 1)) * (( power L) . (x,(n -' 1)))) by POLYNOM4:def 2;

       A4:

      now

        assume 1 in ( dom F);

        

        hence (F . 1) = (( <%z0, z1, z2%> . (1 -' 1)) * (( power L) . (x,(1 -' 1)))) by A3

        .= (( <%z0, z1, z2%> . 0 ) * (( power L) . (x,(1 -' 1)))) by XREAL_1: 232

        .= (( <%z0, z1, z2%> . 0 ) * (( power L) . (x, 0 ))) by XREAL_1: 232

        .= (z0 * (( power L) . (x, 0 ))) by Th21

        .= (z0 * ( 1_ L)) by GROUP_1:def 7

        .= z0 by GROUP_1:def 4;

      end;

       A5:

      now

        assume 2 in ( dom F);

        

        hence (F . 2) = (( <%z0, z1, z2%> . (2 -' 1)) * (( power L) . (x,(2 -' 1)))) by A3

        .= (z1 * (( power L) . (x,1))) by Lm1, Th22

        .= (z1 * x) by GROUP_1: 50;

      end;

      ( len F) = 0 or ... or ( len F) = 3 by A2, Th25;

      per cases ;

        suppose ( len F) = 0 ;

        then

         A6: <%z0, z1, z2%> = ( 0_. L) by A2, POLYNOM4: 5;

        

        hence ( eval ( <%z0, z1, z2%>,x)) = ( 0. L) by POLYNOM4: 17

        .= (( 0_. L) . 0 ) by FUNCOP_1: 7

        .= ((z0 + ( 0. L)) + ( 0. L)) by A6, Th21

        .= ((z0 + ((( 0_. L) . 1) * x)) + ((( 0. L) * x) * x)) by FUNCOP_1: 7

        .= ((z0 + ((( 0_. L) . 1) * x)) + (((( 0_. L) . 2) * x) * x)) by FUNCOP_1: 7

        .= ((z0 + (z1 * x)) + (((( 0_. L) . 2) * x) * x)) by A6, Th22

        .= ((z0 + (z1 * x)) + ((z2 * x) * x)) by A6, Th23;

      end;

        suppose

         A7: ( len F) = 1;

        then ( 0 + 1) in ( Seg ( len F)) by FINSEQ_1: 1;

        then F = <*z0*> by A4, A7, FINSEQ_1:def 3, FINSEQ_1: 40;

        

        hence ( eval ( <%z0, z1, z2%>,x)) = z0 by A1, RLVECT_1: 44

        .= ((z0 + (( 0. L) * x)) + ((( <%z0, z1, z2%> . 2) * x) * x)) by A2, A7, ALGSEQ_1: 8

        .= ((z0 + (( <%z0, z1, z2%> . 1) * x)) + ((( <%z0, z1, z2%> . 2) * x) * x)) by A2, A7, ALGSEQ_1: 8

        .= ((z0 + (z1 * x)) + ((( <%z0, z1, z2%> . 2) * x) * x)) by Th22

        .= ((z0 + (z1 * x)) + ((z2 * x) * x)) by Th23;

      end;

        suppose

         A8: ( len F) = 2;

        F = <*z0, (z1 * x)*> by A4, A5, A8, FINSEQ_1: 44, FINSEQ_3: 25;

        

        hence ( eval ( <%z0, z1, z2%>,x)) = ((z0 + (z1 * x)) + ((( 0. L) * x) * x)) by A1, RLVECT_1: 45

        .= ((z0 + (z1 * x)) + ((( <%z0, z1, z2%> . 2) * x) * x)) by A2, A8, ALGSEQ_1: 8

        .= ((z0 + (z1 * x)) + ((z2 * x) * x)) by Th23;

      end;

        suppose

         A9: ( len F) = 3;

        (F . 3) = (( <%z0, z1, z2%> . (3 -' 1)) * (( power L) . (x,(3 -' 1)))) by A3, A9, FINSEQ_3: 25

        .= (z2 * (( power L) . (x,2))) by Lm2, Th23

        .= (z2 * (x * x)) by GROUP_1: 51

        .= ((z2 * x) * x) by GROUP_1:def 3;

        then F = <*z0, (z1 * x), ((z2 * x) * x)*> by A4, A5, A9, FINSEQ_1: 45, FINSEQ_3: 25;

        hence thesis by A1, RLVECT_1: 46;

      end;

    end;

    registration

      let a be integer Element of F_Real ;

      cluster <%a%> -> INT -valued;

      coherence

      proof

        ( rng <%a%>) c= {a, ( 0. F_Real )} by Th20;

        hence ( rng <%a%>) c= INT by INT_1:def 2;

      end;

    end

    registration

      let a,b be integer Element of F_Real ;

      cluster <%a, b%> -> INT -valued;

      coherence

      proof

        reconsider a1 = a, b1 = b as Element of INT by INT_1:def 2;

         <%a, b%> = ((( 0_. F_Real ) +* ( 0 ,a1)) +* (1,b1));

        hence thesis;

      end;

    end

    registration

      let a,b,c be integer Element of F_Real ;

      cluster <%a, b, c%> -> INT -valued;

      coherence

      proof

        reconsider a1 = a, b1 = b, c1 = c as Element of INT by INT_1:def 2;

         <%a, b, c%> = (((( 0_. F_Real ) +* ( 0 ,a1)) +* (1,b1)) +* (2,c1));

        hence thesis;

      end;

    end

    registration

      cluster monic INT -valued for Polynomial of F_Real ;

      existence

      proof

        take ( 1_. F_Real );

        thus thesis;

      end;

    end

    registration

      cluster INT -valued for FinSequence of F_Real ;

      existence

      proof

        take ( <*> the carrier of F_Real );

        thus thesis;

      end;

    end

    registration

      let F be INT -valued FinSequence of F_Real ;

      cluster ( Sum F) -> integer;

      coherence

      proof

        consider f be sequence of F_Real such that

         A1: ( Sum F) = (f . ( len F)) and

         A2: (f . 0 ) = ( 0. F_Real ) and

         A3: for j be Nat, v be Element of F_Real st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Nat] means $1 <= ( len F) implies (f . $1) is integer;

        

         A4: P[ 0 ] by A2;

        

         A5: P[k] implies P[(k + 1)]

        proof

          assume that

           A6: P[k] and

           A7: (k + 1) <= ( len F);

          reconsider v = (F . (k + 1)) as Element of F_Real by XREAL_0:def 1;

          

           A8: (k + 0 ) < (k + 1) by XREAL_1: 8;

          then k < ( len F) by A7, XXREAL_0: 2;

          then (f . (k + 1)) = ((f . k) + v) by A3;

          hence thesis by A6, A8, A7, XXREAL_0: 2;

        end;

         P[k] from NAT_1:sch 2( A4, A5);

        hence thesis by A1;

      end;

    end

    registration

      let f be INT -valued sequence of F_Real ;

      cluster ( - f) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng ( - f));

        then

        consider x be object such that

         A1: x in ( dom ( - f)) and

         A2: (( - f) . x) = y by FUNCT_1:def 3;

        reconsider x as Element of NAT by A1;

        (( - f) . x) = (( - f) /. x)

        .= ( - (f /. x)) by A1, VFUNCT_1:def 5

        .= ( - (f . x));

        hence thesis by A2, INT_1:def 2;

      end;

      let g be INT -valued sequence of F_Real ;

      cluster (f + g) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f + g));

        then

        consider x be object such that

         A3: x in ( dom (f + g)) and

         A4: ((f + g) . x) = y by FUNCT_1:def 3;

        reconsider x as Element of NAT by A3;

        ((f + g) . x) = ((f . x) + (g . x)) by NORMSP_1:def 2;

        hence thesis by A4, INT_1:def 2;

      end;

      cluster (f - g) -> INT -valued;

      coherence ;

      cluster (f *' g) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f *' g));

        then

        consider x be object such that

         A5: x in ( dom (f *' g)) and

         A6: ((f *' g) . x) = y by FUNCT_1:def 3;

        reconsider x as Element of NAT by A5;

        consider r be FinSequence of F_Real such that ( len r) = (x + 1) and

         A7: ((f *' g) . x) = ( Sum r) and

         A8: for k be Element of NAT st k in ( dom r) holds (r . k) = ((f . (k -' 1)) * (g . ((x + 1) -' k))) by POLYNOM3:def 9;

        r is INT -valued

        proof

          let y be object;

          assume y in ( rng r);

          then

          consider a be object such that

           A9: a in ( dom r) and

           A10: (r . a) = y by FUNCT_1:def 3;

          reconsider a as Element of NAT by A9;

          (r . a) = ((f . (a -' 1)) * (g . ((x + 1) -' a))) by A8, A9;

          hence y in INT by A10, INT_1:def 2;

        end;

        hence thesis by A6, A7, INT_1:def 2;

      end;

    end

    theorem :: NIVEN:39

    

     Th37: for L be non degenerated non empty doubleLoopStr, z be Element of L holds ( LC <%z, ( 1. L)%>) = ( 1. L)

    proof

      let L be non degenerated non empty doubleLoopStr;

      let z be Element of L;

      ( len <%z, ( 1. L)%>) = 2 by POLYNOM5: 40;

      hence thesis by Lm1, POLYNOM5: 38;

    end;

    registration

      let L be non degenerated non empty doubleLoopStr;

      let z be Element of L;

      cluster <%z, ( 1. L)%> -> monic;

      coherence by Th37;

    end

    theorem :: NIVEN:40

    

     Th38: for L be non degenerated non empty doubleLoopStr, z1,z2 be Element of L holds ( LC <%z1, z2, ( 1. L)%>) = ( 1. L)

    proof

      let L be non degenerated non empty doubleLoopStr;

      let z1,z2 be Element of L;

      ( len <%z1, z2, ( 1. L)%>) = 3 by Th26;

      hence thesis by Lm2, Th23;

    end;

    registration

      let L be non degenerated non empty doubleLoopStr;

      let z1,z2 be Element of L;

      cluster <%z1, z2, ( 1. L)%> -> monic;

      coherence by Th38;

    end

    registration

      let p be INT -valued Polynomial of F_Real ;

      cluster ( LC p) -> integer;

      coherence ;

    end

    theorem :: NIVEN:41

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L holds ( deg ( - p)) = ( deg p) by POLYNOM4: 8;

    theorem :: NIVEN:42

    

     Th40: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p,q be Polynomial of L st ( deg p) > ( deg q) holds ( deg (p + q)) = ( deg p)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p,q be Polynomial of L;

      assume

       A1: ( deg p) > ( deg q);

      then ( deg (p + q)) = ( max (( deg p),( deg q))) by HURWITZ: 21;

      hence thesis by A1, XXREAL_0:def 10;

    end;

    theorem :: NIVEN:43

    

     Th41: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p,q be Polynomial of L st ( deg p) > ( deg q) holds ( deg (p - q)) = ( deg p)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p,q be Polynomial of L;

      assume

       A1: ( deg p) > ( deg q);

      

       A2: ( deg q) = ( deg ( - q)) by POLYNOM4: 8;

      then ( deg (p + ( - q))) = ( max (( deg p),( deg ( - q)))) by A1, HURWITZ: 21;

      hence thesis by A1, A2, XXREAL_0:def 10;

    end;

    theorem :: NIVEN:44

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p,q be Polynomial of L st ( deg p) < ( deg q) holds ( deg (p - q)) = ( deg q)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p,q be Polynomial of L;

      assume

       A1: ( deg p) < ( deg q);

      ( deg ( - q)) = ( deg q) by POLYNOM4: 8;

      then ( deg (p + ( - q))) = ( max (( deg p),( deg q))) by A1, HURWITZ: 21;

      hence thesis by A1, XXREAL_0:def 10;

    end;

    theorem :: NIVEN:45

    for L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr holds for p be Polynomial of L holds ( LC p) = ( - ( LC ( - p)))

    proof

      let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr;

      let p be Polynomial of L;

      

       A1: ( len p) = ( len ( - p)) by POLYNOM4: 8;

      

       A2: ( dom ( - p)) = NAT by FUNCT_2:def 1;

      

      thus ( LC p) = ( - ( - (p /. (( len p) -' 1))))

      .= ( - (( - p) /. (( len ( - p)) -' 1))) by A1, A2, VFUNCT_1:def 5

      .= ( - ( LC ( - p)));

    end;

    

     lemmul: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for p,q be Polynomial of L st p <> ( 0_. L) & q <> ( 0_. L) holds ((p *' q) . (((( len p) + ( len q)) - 1) -' 1)) = ((p . (( len p) -' 1)) * (q . (( len q) -' 1)))

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

      let p,q be Polynomial of L;

      assume p <> ( 0_. L) & q <> ( 0_. L);

      then

       B: ( len p) >= 1 & ( len q) >= 1 by NAT_1: 14, POLYNOM4: 5;

      then (( len p) + ( len q)) >= (1 + 1) by XREAL_1: 7;

      then

       A: ((( len p) + ( len q)) - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

      reconsider j = ((( len p) + ( len q)) - 1) as Element of NAT by B, INT_1: 3;

      set i = (j -' 1);

      consider r be FinSequence of the carrier of L such that

       M: ( len r) = (i + 1) & ((p *' q) . i) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by POLYNOM3:def 9;

      

       A7: (j - 1) = i by A, XREAL_0:def 2;

      reconsider x = (( len q) - 1) as Element of NAT by B, INT_1: 3;

      

       A3: j = (( len p) + x);

      then j >= ( len p) by NAT_1: 11;

      then

       A1: ( len p) in ( dom r) by A7, M, B, FINSEQ_3: 25;

      

       A2: ((i + 1) -' ( len p)) = (((((( len p) + ( len q)) - 1) - 1) + 1) - ( len p)) by A3, A7, XREAL_0:def 2

      .= (((( len p) - ( len p)) + ( len q)) - 1)

      .= (( len q) -' 1) by B, XREAL_0:def 2;

      now

        let k be Element of NAT ;

        assume

         E: k in ( dom r) & k <> ( len p);

        per cases by E, XXREAL_0: 1;

          suppose

           E1: k > ( len p);

          then

          reconsider k1 = (k - 1) as Element of NAT by INT_1: 3;

          

           E2: (k1 + 1) > ( len p) by E1;

          (k -' 1) = (k - 1) by E1, XREAL_0:def 2;

          then (p . (k -' 1)) = ( 0. L) by E2, ALGSEQ_1: 8, NAT_1: 13;

          then (r . k) = (( 0. L) * (q . ((i + 1) -' k))) by E, M;

          hence (r /. k) = ( 0. L) by E, PARTFUN1:def 6;

        end;

          suppose k < ( len p);

          then (k + 1) <= ( len p) by INT_1: 7;

          then ((k + 1) - k) <= (( len p) - k) by XREAL_1: 9;

          then ((( len p) - k) + ( len q)) >= (1 + ( len q)) by XREAL_1: 6;

          then

           E2: (((( len p) - k) + ( len q)) - 1) >= ((( len q) + 1) - 1) by XREAL_1: 9;

          ((i + 1) - k) = (((((( len p) + ( len q)) - 1) - 1) + 1) - k) by A, XREAL_0:def 2;

          then ((i + 1) -' k) = (((( len p) + ( len q)) - 1) - k) by E2, XREAL_0:def 2;

          then (q . ((i + 1) -' k)) = ( 0. L) by E2, ALGSEQ_1: 8;

          then (r . k) = ((p . (k -' 1)) * ( 0. L)) by E, M;

          hence (r /. k) = ( 0. L) by E, PARTFUN1:def 6;

        end;

      end;

      

      then ( Sum r) = (r /. ( len p)) by A1, POLYNOM2: 3

      .= (r . ( len p)) by A1, PARTFUN1:def 6

      .= ((p . (( len p) -' 1)) * (q . ((i + 1) -' ( len p)))) by A1, M;

      hence thesis by M, A2;

    end;

    theorem :: NIVEN:46

    

     Th44: for L be add-associative right_zeroed right_complementable distributive associative well-unital domRing-like non degenerated doubleLoopStr holds for p,q be Polynomial of L holds ( LC (p *' q)) = (( LC p) * ( LC q))

    proof

      let L be add-associative right_zeroed right_complementable distributive associative well-unital domRing-like non degenerated doubleLoopStr;

      let p,q be Polynomial of L;

      per cases ;

        suppose

         AS: p <> ( 0_. L) & q <> ( 0_. L);

        ( len (p *' q)) = (( deg (p *' q)) + 1)

        .= ((( deg p) + ( deg q)) + 1) by AS, HURWITZ: 23

        .= (((( len p) - 1) + (( len q) - 1)) + 1);

        

        hence ( LC (p *' q)) = ((p *' q) . (((( len p) + ( len q)) - 1) -' 1))

        .= (( LC p) * ( LC q)) by AS, lemmul;

      end;

        suppose

         A30: p is zero;

        then (p *' q) = ( 0_. L) by Th17;

        

        hence ( LC (p *' q)) = (( 0. L) * ( LC q)) by FUNCOP_1: 7

        .= (( LC p) * ( LC q)) by A30, FUNCOP_1: 7;

      end;

        suppose

         A31: q is zero;

        then (p *' q) = ( 0_. L) by POLYNOM3: 34;

        

        hence ( LC (p *' q)) = (( LC p) * ( 0. L)) by FUNCOP_1: 7

        .= (( LC p) * ( LC q)) by A31, FUNCOP_1: 7;

      end;

    end;

     Lm3:

    now

      let L be non degenerated doubleLoopStr;

      let p be monic Polynomial of L;

      let q be Polynomial of L;

      assume

       A1: ( deg p) > ( deg q);

      p <> ( 0_. L);

      then 0 <> ( len p) by POLYNOM4: 5;

      then

       A2: (( len p) - 1) = (( len p) -' 1) by XREAL_0:def 2;

      ( len q) <= (( len p) - 1) by A1, INT_1: 52;

      hence (q . (( len p) -' 1)) = ( 0. L) by A2, ALGSEQ_1: 8;

    end;

    theorem :: NIVEN:47

    for L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr holds for p be monic Polynomial of L holds for q be Polynomial of L st ( deg p) > ( deg q) holds (p + q) is monic

    proof

      let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr;

      let p be monic Polynomial of L;

      let q be Polynomial of L;

      assume

       A1: ( deg p) > ( deg q);

      then

       A2: (q . (( len p) -' 1)) = ( 0. L) by Lm3;

      ( deg (p + q)) = ( deg p) by A1, Th40;

      

      hence ( LC (p + q)) = ((p . (( len p) -' 1)) + (q . (( len p) -' 1))) by NORMSP_1:def 2

      .= ( LC p) by A2

      .= ( 1. L) by RATFUNC1:def 7;

    end;

    theorem :: NIVEN:48

    

     Th46: for L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr holds for p be monic Polynomial of L holds for q be Polynomial of L st ( deg p) > ( deg q) holds (p - q) is monic

    proof

      let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr;

      let p be monic Polynomial of L;

      let q be Polynomial of L;

      assume

       A1: ( deg p) > ( deg q);

      then

       A2: (q . (( len p) -' 1)) = ( 0. L) by Lm3;

      ( deg (p - q)) = ( deg p) by A1, Th41;

      

      hence ( LC (p - q)) = ((p . (( len p) -' 1)) - (q . (( len p) -' 1))) by NORMSP_1:def 3

      .= ( LC p) by A2

      .= ( 1. L) by RATFUNC1:def 7;

    end;

    registration

      let L be add-associative right_zeroed right_complementable associative well-unital almost_left_invertible distributive non degenerated doubleLoopStr;

      let p,q be monic Polynomial of L;

      cluster (p *' q) -> monic;

      coherence

      proof

        ( LC p) = ( 1. L) & ( LC q) = ( 1. L) by RATFUNC1:def 7;

        

        hence ( 1. L) = (( LC p) * ( LC q))

        .= ( LC (p *' q)) by Th44;

      end;

    end

    theorem :: NIVEN:49

    

     Th47: for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for z1,z2 be Element of L holds for p be Polynomial of L st ( eval (p,z1)) = z2 holds ( eval ((p - <%z2%>),z1)) = ( 0. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr;

      let z1,z2 be Element of L;

      let p be Polynomial of L such that

       A1: ( eval (p,z1)) = z2;

      

      thus ( eval ((p - <%z2%>),z1)) = (( eval (p,z1)) - ( eval ( <%z2%>,z1))) by POLYNOM4: 21

      .= (z2 - z2) by A1, POLYNOM5: 37

      .= ( 0. L) by RLVECT_1: 15;

    end;

    ::$Notion-Name

    theorem :: NIVEN:50

    

     Th50: for p be INT -valued Polynomial of F_Real holds for e be Element of F_Real st e is_a_root_of p holds for k,l be Integer st l <> 0 & e = (k / l) & (k,l) are_coprime holds k divides (p . 0 ) & l divides ( LC p)

    proof

      let p be INT -valued Polynomial of F_Real ;

      let e be Element of F_Real such that

       A1: e is_a_root_of p;

      let k,l be Integer such that

       A2: l <> 0 & e = (k / l) & (k,l) are_coprime ;

      consider F be FinSequence of F_Real such that

       A3: ( 0. F_Real ) = ( Sum F) & ( len F) = ( len p) & for n be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (( power F_Real ) . (e,(n -' 1)))) by A1, POLYNOM4:def 2;

      per cases ;

        suppose ( len F) = 0 ;

        then

         A4: p = <%( 0. F_Real )%> by A3, ALGSEQ_1: 14;

        then (p . 0 ) = ( 0. F_Real ) by ALGSEQ_1: 16;

        hence k divides (p . 0 ) by INT_2: 12;

        p = ( 0_. F_Real ) by A4, POLYNOM5: 34;

        then ( LC p) = ( 0. F_Real ) by FUNCOP_1: 7;

        hence l divides ( LC p) by INT_2: 12;

      end;

        suppose

         A5: ( len F) > 0 ;

        set n = ( len p);

        

         A6: n >= 1 by A5, A3, NAT_1: 14;

        reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20, A5, A3;

        

         A7: (n -' 1) = n1 by A5, A3, NAT_1: 14, XREAL_1: 233;

        

         A8: (l |^ (n -' 1)) <> 0 by A2, CARD_4: 3;

        reconsider k1 = k, l1 = l as Element of F_Real by XREAL_0:def 1;

        set ln = (( power F_Real ) . (l1,n1));

        set G = (ln * F);

        reconsider FF = F as Element of (( len F) -tuples_on the carrier of F_Real ) by FINSEQ_2: 92;

        set GG = (ln * FF);

        

         A9: ( len GG) = ( len F) by FINSEQ_2: 132;

        then

         A10: ( dom G) = ( dom F) by FINSEQ_3: 29;

        

         A11: ( Sum G) = (ln * ( Sum F)) by FVSUM_1: 73;

        ( rng G) c= INT

        proof

          let o be object;

          assume o in ( rng G);

          then

          consider b be object such that

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

          reconsider b as Element of NAT by A12;

          b in ( Seg n) by A12, A9, A3, FINSEQ_1:def 3;

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

          then (b -' 1) = (b - 1) & (b - 1) <= n1 by XREAL_1: 233, XREAL_1: 9;

          then

          consider c be Nat such that

           A13: n1 = ((b -' 1) + c) by NAT_1: 10;

          ( rng F) c= the carrier of F_Real ;

          then

          reconsider a9 = (F . b) as Element of F_Real by A12, A10, FUNCT_1: 3;

          

           A14: (l |^ (b -' 1)) <> 0 by A2, CARD_4: 3;

          b in ( dom (ln * F)) & a9 = (F . b) implies ((ln * F) . b) = (ln * a9) by FVSUM_1: 50;

          

          then (G . b) = (ln * ((p . (b -' 1)) * (( power F_Real ) . (e,(b -' 1))))) by A3, A12, A10

          .= ((p . (b -' 1)) * ((( power F_Real ) . (l1,n1)) * (( power F_Real ) . (e,(b -' 1)))))

          .= ((p . (b -' 1)) * ((l1 |^ n1) * (( power F_Real ) . (e,(b -' 1))))) by Th48

          .= ((p . (b -' 1)) * ((l1 |^ n1) * ((k / l) |^ (b -' 1)))) by A2, Th48

          .= ((p . (b -' 1)) * ((l |^ n1) * ((k |^ (b -' 1)) / (l |^ (b -' 1))))) by PREPOWER: 8

          .= (((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ n1) / (l |^ (b -' 1))))

          .= (((p . (b -' 1)) * (k |^ (b -' 1))) * (((l |^ c) * (l |^ (b -' 1))) / (l |^ (b -' 1)))) by A13, NEWTON: 8

          .= (((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ c) * ((l |^ (b -' 1)) / (l |^ (b -' 1)))))

          .= (((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ c) * 1)) by XCMPLX_1: 60, A14

          .= (((p . (b -' 1)) * (k |^ (b -' 1))) * (l |^ c));

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

        end;

        then

        reconsider G1 = G as non empty INT -valued FinSequence by A9, A5, RELAT_1:def 19;

        

         A15: 1 in ( dom G) by A9, A6, A3, FINSEQ_3: 25;

        

         A16: ( Sum G1) = ( Sum G) by Th49;

        

         A17: ( Sum G1) = 0 by A3, A11, Th49;

        reconsider Gn0 = (G1 /^ 1) as INT -valued FinSequence;

        G = ( <*(G /. 1)*> ^ Gn0) by FINSEQ_5: 29;

        then (( Sum Gn0) + (G /. 1)) = 0 by RVSUM_1: 76, A16, A11, A3;

        then (( Sum Gn0) + (G . 1)) = 0 by A15, PARTFUN1:def 6;

        then

         A18: ( Sum Gn0) = ( - (G1 . 1));

        ( rng F) c= the carrier of F_Real ;

        then

        reconsider a9 = (F . 1) as Element of F_Real by A15, A10, FUNCT_1: 3;

        

         A19: (G1 . 1) = (ln * a9) by FVSUM_1: 50, A15

        .= (ln * ((p . (1 -' 1)) * (( power F_Real ) . (e,(1 -' 1))))) by A6, A3, FINSEQ_3: 25

        .= (((p . (1 -' 1)) * ln) * (( power F_Real ) . (e,(1 -' 1))))

        .= (((p . (1 -' 1)) * ln) * (( power F_Real ) . (e, 0 ))) by XREAL_1: 232

        .= (((p . 0 ) * ln) * (( power F_Real ) . (e, 0 ))) by XREAL_1: 232

        .= (((p . 0 ) * ln) * ( 1_ F_Real )) by GROUP_1:def 7

        .= ((p . 0 ) * (l |^ n1)) by Th48;

        for i be Nat st i in ( dom Gn0) holds k divides (Gn0 . i)

        proof

          let i be Nat;

          assume

           A20: i in ( dom Gn0);

          then

           A21: (1 + i) in ( dom G1) by FINSEQ_5: 26;

          ( rng F) c= the carrier of F_Real ;

          then

          reconsider a9 = (F . (1 + i)) as Element of F_Real by A21, A10, FUNCT_1: 3;

          

           A22: (l |^ i) <> 0 by A2, CARD_4: 3;

          

           A23: 1 <= i <= ( len Gn0) by A20, FINSEQ_3: 25;

          (i + 1) in ( Seg n) by A3, A21, A9, FINSEQ_1:def 3;

          then (i + 1) <= n by FINSEQ_1: 1;

          then ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

          then

          consider d be Nat such that

           A24: n1 = (i + d) by NAT_1: 10;

          (Gn0 . i) = ((G /^ 1) /. i) by A20, PARTFUN1:def 6

          .= (G /. (1 + i)) by FINSEQ_5: 27, A20

          .= (G . (1 + i)) by A21, PARTFUN1:def 6

          .= (ln * a9) by FVSUM_1: 50, A21

          .= (ln * ((p . ((1 + i) -' 1)) * (( power F_Real ) . (e,((1 + i) -' 1))))) by A3, A21, A10

          .= (ln * ((p . i) * (( power F_Real ) . (e,((1 + i) -' 1))))) by NAT_D: 34

          .= (ln * ((p . i) * (( power F_Real ) . (e,i)))) by NAT_D: 34

          .= ((p . i) * ((( power F_Real ) . (l1,n1)) * (( power F_Real ) . (e,i))))

          .= ((p . i) * ((l1 |^ n1) * (( power F_Real ) . (e,i)))) by Th48

          .= ((p . i) * ((l1 |^ n1) * (e |^ i))) by Th48

          .= ((p . i) * ((l |^ n1) * ((k |^ i) / (l |^ i)))) by A2, PREPOWER: 8

          .= (((p . i) * (k |^ i)) * ((l |^ (d + i)) / (l |^ i))) by A24

          .= (((p . i) * (k |^ i)) * (((l |^ d) * (l |^ i)) / (l |^ i))) by NEWTON: 8

          .= (((p . i) * (k |^ i)) * ((l |^ d) * ((l |^ i) / (l |^ i))))

          .= (((p . i) * (k |^ i)) * ((l |^ d) * 1)) by XCMPLX_1: 60, A22

          .= (((p . i) * (l |^ d)) * (k |^ i));

          hence k divides (Gn0 . i) by A23, Th4, INT_2: 2;

        end;

        then k divides (G1 . 1) by A18, NEWTON04: 80, INT_2: 10;

        hence k divides (p . 0 ) by A19, A2, WSIERP_1: 10, INT_2: 25;

        reconsider Gn1 = (G1 | ( Seg n1)) as INT -valued FinSequence by FINSEQ_1: 15;

        

         A25: ( len GG) = ( len F) by FINSEQ_2: 132;

        then

         A26: ( len G1) = (n1 + 1) by A3;

        G1 = (Gn1 ^ <*(G1 . (n1 + 1))*>) by A25, A3, FINSEQ_3: 55;

        then (( Sum Gn1) + (G1 . (n1 + 1))) = 0 by RVSUM_1: 74, A17;

        

        then

         A27: ( Sum Gn1) = ( - (G1 . (n1 + 1)))

        .= ( - (G1 . n));

        

         A28: n in ( dom F) by FINSEQ_3: 25, A6, A3;

        ( rng F) c= the carrier of F_Real ;

        then

        reconsider a9 = (F . n) as Element of F_Real by A28, FUNCT_1: 3;

        n in ( dom G1) by A25, A3, FINSEQ_3: 25, A6;

        

        then

         A29: (G1 . n) = (ln * a9) by FVSUM_1: 50

        .= (ln * ((p . (n -' 1)) * (( power F_Real ) . (e,(n -' 1))))) by A6, A3, FINSEQ_3: 25

        .= ((p . (n -' 1)) * ((( power F_Real ) . (l1,n1)) * (( power F_Real ) . (e,(n -' 1)))))

        .= ((p . (n -' 1)) * ((l1 |^ n1) * (( power F_Real ) . (e,(n -' 1))))) by Th48

        .= ((p . (n -' 1)) * ((l1 |^ n1) * (e |^ (n -' 1)))) by Th48

        .= ((p . (n -' 1)) * ((l |^ n1) * ((k |^ (n -' 1)) / (l |^ (n -' 1))))) by A2, PREPOWER: 8

        .= (((p . (n -' 1)) * (k |^ (n -' 1))) * ((l |^ (n -' 1)) / (l |^ (n -' 1)))) by A7

        .= (((p . (n -' 1)) * (k |^ (n -' 1))) * 1) by A8, XCMPLX_1: 60

        .= (( LC p) * (k |^ (n -' 1)));

        for i be Nat st i in ( dom Gn1) holds l divides (Gn1 . i)

        proof

          let i be Nat;

          assume

           A30: i in ( dom Gn1);

          then i in ( Seg n1) by A26, FINSEQ_3: 54;

          then

           A31: 1 <= i <= n1 & (i -' 1) <= i by FINSEQ_1: 1, NAT_D: 35;

          then

          consider d be Nat such that

           A32: n1 = ((i -' 1) + d) by XXREAL_0: 2, NAT_1: 10;

          (i - i) <= ((n - 1) - i) by A31, XREAL_1: 9;

          then

           A33: ( 0 + 1) <= (((n - i) - 1) + 1) by XREAL_1: 6;

          

           A34: (n - 1) = ((i - 1) + d) by A32, A31, XREAL_1: 233;

          

           A35: (Gn1 . i) = (G1 . i) by A30, FUNCT_1: 47;

          

           A36: ( dom Gn1) c= ( dom G1) by RELAT_1: 60;

          ( rng F) c= the carrier of F_Real ;

          then

          reconsider a9 = (F . i) as Element of F_Real by A36, A10, A30, FUNCT_1: 3;

          

           A37: (l |^ (i -' 1)) <> 0 by A2, CARD_4: 3;

          (G1 . i) = (ln * a9) by A36, A30, FVSUM_1: 50

          .= (ln * ((p . (i -' 1)) * (( power F_Real ) . (e,(i -' 1))))) by A3, A36, A30, A10

          .= ((p . (i -' 1)) * ((( power F_Real ) . (l1,n1)) * (( power F_Real ) . (e,(i -' 1)))))

          .= ((p . (i -' 1)) * ((l1 |^ n1) * (( power F_Real ) . (e,(i -' 1))))) by Th48

          .= ((p . (i -' 1)) * ((l1 |^ n1) * (e |^ (i -' 1)))) by Th48

          .= ((p . (i -' 1)) * ((l |^ n1) * ((k |^ (i -' 1)) / (l |^ (i -' 1))))) by A2, PREPOWER: 8

          .= (((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ n1) / (l |^ (i -' 1))))

          .= (((p . (i -' 1)) * (k |^ (i -' 1))) * (((l |^ d) * (l |^ (i -' 1))) / (l |^ (i -' 1)))) by A32, NEWTON: 8

          .= (((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ d) * ((l |^ (i -' 1)) / (l |^ (i -' 1)))))

          .= (((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ d) * 1)) by XCMPLX_1: 60, A37

          .= (((p . (i -' 1)) * (k |^ (i -' 1))) * (l |^ d));

          hence l divides (Gn1 . i) by A35, A34, A33, Th4, INT_2: 2;

        end;

        then l divides (G1 . n) by A27, NEWTON04: 80, INT_2: 10;

        hence l divides ( LC p) by A29, A2, WSIERP_1: 10, INT_2: 25;

      end;

    end;

    ::$Notion-Name

    theorem :: NIVEN:51

    

     Th51: for p be monic INT -valued Polynomial of F_Real holds for e be rational Element of F_Real st e is_a_root_of p holds e is integer

    proof

      let p be monic INT -valued Polynomial of F_Real ;

      let e be rational Element of F_Real ;

      assume

       A1: e is_a_root_of p;

      set k = ( numerator e);

      set n = ( denominator e);

      

       A2: e = (k / n) by RAT_1: 15;

      

       A3: (k,n) are_coprime by WSIERP_1: 22;

      p is monic;

      then n = 1 or n = ( - 1) by A1, A2, A3, Th50, INT_2: 13;

      hence thesis by A2;

    end;

    theorem :: NIVEN:52

    

     Th52: 1 <= n & e = (2 * ( cos t)) implies ex p be monic INT -valued Polynomial of F_Real st ( eval (p,e)) = (2 * ( cos (n * t))) & ( deg p) = n & (n = 1 implies p = <%( 0. F_Real ), ( 1. F_Real )%>) & (n = 2 implies ex r be Element of F_Real st r = ( - 2) & p = <%r, ( 0. F_Real ), ( 1. F_Real )%>)

    proof

      assume that

       A1: 1 <= n and

       A2: e = (2 * ( cos t));

      defpred P[ Nat] means 1 <= $1 implies ex p be monic INT -valued Polynomial of F_Real st ( eval (p,e)) = (2 * ( cos ($1 * t))) & ( deg p) = $1 & ($1 = 1 implies p = <%( 0. F_Real ), ( 1. F_Real )%>) & ($1 = 2 implies ex r be Element of F_Real st r = ( - 2) & p = <%r, ( 0. F_Real ), ( 1. F_Real )%>);

      

       A3: P[1]

      proof

        assume 1 <= 1;

        reconsider p = <%( 0. F_Real ), ( 1. F_Real )%> as monic INT -valued Polynomial of F_Real ;

        take p;

        thus ( eval (p,e)) = (2 * ( cos (1 * t))) by A2, POLYNOM5: 48;

        ( len p) = 2 by POLYNOM5: 40;

        hence ( deg p) = 1;

        thus thesis;

      end;

      

       A4: P[2]

      proof

        assume 1 <= 2;

        reconsider r = ( - 2) as Element of F_Real by XREAL_0:def 1;

        reconsider p = <%r, ( 0. F_Real ), ( 1. F_Real )%> as monic INT -valued Polynomial of F_Real ;

        take p;

        ( cos (2 * t)) = ((2 * (( cos t) ^2 )) - 1) by SIN_COS5: 7;

        

        hence (2 * ( cos (2 * t))) = ((r + (( 0. F_Real ) * e)) + ((( 1. F_Real ) * e) * e)) by A2

        .= ( eval (p,e)) by Th36;

        ( len p) = 3 by Th26;

        hence ( deg p) = 2;

        thus thesis;

      end;

      

       A5: for k be non zero Nat st P[k] & P[(k + 1)] holds P[(k + 2)]

      proof

        let k be non zero Nat such that

         A6: P[k] and

         A7: P[(k + 1)] and 1 <= (k + 2);

        per cases ;

          suppose (k + 2) = 1;

          then k = ( - 1);

          hence thesis;

        end;

          suppose (k + 2) = 2;

          hence thesis;

        end;

          suppose

           A8: (k + 2) <> 1 & (k + 2) <> 2;

          

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

          then

          consider p2 be monic INT -valued Polynomial of F_Real such that

           A10: ( eval (p2,e)) = (2 * ( cos (k * t))) and

           A11: ( deg p2) = k by A6;

          consider p1 be monic INT -valued Polynomial of F_Real such that

           A12: ( eval (p1,e)) = (2 * ( cos ((k + 1) * t))) and

           A13: ( deg p1) = (k + 1) by A7, A9, NAT_1: 13;

          set f = <%( 0. F_Real ), ( 1. F_Real )%>;

          set p = ((f *' p1) - p2);

          p1 is non-zero;

          then

           A14: ( len (f *' p1)) = (( len p1) + 1) by UPROOTS: 38;

          then

           A15: ( deg (f *' p1)) > ( deg p2) by A11, A13, XREAL_1: 8;

          then

          reconsider p as monic INT -valued Polynomial of F_Real by Th46;

          take p;

          

           A16: ( eval ((f *' p1),e)) = (( eval (f,e)) * ( eval (p1,e))) by POLYNOM4: 24;

          (( cos ((k + 2) * t)) + ( cos (k * t))) = (2 * (( cos ((((k + 2) * t) + (k * t)) / 2)) * ( cos ((((k + 2) * t) - (k * t)) / 2)))) by SIN_COS4: 17

          .= (( cos t) * (2 * ( cos ((k * t) + t))));

          then (((2 * ( cos t)) * (2 * ( cos ((k * t) + t)))) - (2 * ( cos (k * t)))) = (2 * ( cos ((k + 2) * t)));

          

          hence (2 * ( cos ((k + 2) * t))) = (( eval ((f *' p1),e)) - ( eval (p2,e))) by A2, A10, A12, A16, POLYNOM5: 48

          .= ( eval (p,e)) by POLYNOM4: 21;

          thus ( deg p) = (k + 2) by A13, A14, A15, Th41;

          thus thesis by A8;

        end;

      end;

      for k be non zero Nat holds P[k] from FIB_NUM2:sch 1( A3, A4, A5);

      hence thesis by A1;

    end;

    theorem :: NIVEN:53

    

     Th53: 0 <= r <= ( PI / 2) & (r / PI ) is rational & ( cos r) is rational implies r in { 0 , ( PI / 3), ( PI / 2)}

    proof

      assume that

       A1: 0 <= r and

       A2: r <= ( PI / 2) and

       A3: (r / PI ) is rational and

       A4: ( cos r) is rational;

      consider k be Integer, n be Nat such that

       A5: n <> 0 and

       A6: ((r / PI ) / 2) = (k / n) by A3, RAT_1: 8;

      set e = (2 * ( cos r));

      reconsider c = e as Element of F_Real by XREAL_0:def 1;

      consider p be monic INT -valued Polynomial of F_Real such that

       A7: ( eval (p,c)) = (2 * ( cos (n * r))) and

       A8: ( deg p) = n and (n = 1 implies p = <%( 0. F_Real ), ( 1. F_Real )%>) & (n = 2 implies ex a be Element of F_Real st a = ( - 2) & p = <%a, ( 0. F_Real ), ( 1. F_Real )%>) by A5, NAT_1: 14, Th52;

      

       A9: (n * (((2 * PI ) * k) / n)) = ((2 * PI ) * k) by A5, XCMPLX_1: 87;

      

       A10: ( cos (((2 * PI ) * k) + 0 )) = 1 by SIN_COS: 31, COMPLEX2: 9;

      reconsider r2 = 2 as Element of F_Real by XREAL_0:def 1;

      ((r / PI ) / 2) = (r / (2 * PI )) by XCMPLX_1: 78;

      then r = (((2 * PI ) * k) / n) by A6, Th1;

      then

       A11: c is_a_root_of (p - <%r2%>) by A7, A9, A10, Th47;

      (( len <%r2%>) - 1) <= (1 - 1) by XREAL_1: 9, ALGSEQ_1:def 5;

      then ( deg p) > ( deg <%r2%>) by A5, A8;

      then (p - <%r2%>) is monic by Th46;

      then

       A12: e is integer by A4, A11, Th51;

      ( PI / 2) < (2 * PI ) by XREAL_1: 68;

      then

       A13: r < (2 * PI ) by A2, XXREAL_0: 2;

      

       A14: r in [.( - ( PI / 2)), ( PI / 2).] by A1, A2, XXREAL_1: 1;

      ( cos . r) in [.( - 1), 1.] by COMPTRIG: 27;

      then ( - 1) <= ( cos r) <= 1 by XXREAL_1: 1;

      then (2 * ( - 1)) <= e <= (2 * 1) by XREAL_1: 64;

      then ( - 2) <= e <= 2;

      then |.e.| <= 2 by ABSVALUE: 5;

      then e = ( - 2) or e = ( - 1) or e = 0 or e = 1 or e = 2 by A12, Th3;

      then ( cos r) = ( - 1) or ( cos r) = ( - (1 / 2)) or ( cos r) = 0 or ( cos r) = (1 / 2) or ( cos r) = 1;

      then r = ( PI / 2) or r = ((3 / 2) * PI ) or r = ( PI / 3) or r = 0 by A1, A2, A13, A14, Th15, COMPTRIG: 12, COMPTRIG: 18, COMPTRIG: 61;

      hence thesis by A2, XREAL_1: 68, ENUMSET1:def 1;

    end;

    theorem :: NIVEN:54

    ((2 * PI ) * i) <= r <= (( PI / 2) + ((2 * PI ) * i)) & (r / PI ) is rational & ( cos r) is rational implies r in {((2 * PI ) * i), (( PI / 3) + ((2 * PI ) * i)), (( PI / 2) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume a <= r <= (( PI / 2) + a);

      then

       A1: (a - a) <= R <= ((( PI / 2) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( cos r) = ( cos R) by COMPLEX2: 9;

      then R in { 0 , ( PI / 3), ( PI / 2)} by A1, A2, A3, Th53;

      then R = 0 or R = ( PI / 3) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:55

    

     Th55: ( PI / 2) <= r <= PI & (r / PI ) is rational & ( cos r) is rational implies r in {( PI / 2), ((2 * PI ) / 3), PI }

    proof

      set R = ( PI - r);

      assume ( PI / 2) <= r <= PI ;

      then

       A1: ( PI - PI ) <= R <= ( PI - ( PI / 2)) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      

       A3: (R / PI ) = (( PI / PI ) - (r / PI ))

      .= (1 - (r / PI )) by XCMPLX_1: 60;

      ( cos R) = ( - ( cos r)) by EUCLID10: 2;

      then R in { 0 , ( PI / 3), ( PI / 2)} by A1, A2, A3, Th53;

      then R = 0 or R = ( PI / 3) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:56

    (( PI / 2) + ((2 * PI ) * i)) <= r <= ( PI + ((2 * PI ) * i)) & (r / PI ) is rational & ( cos r) is rational implies r in {(( PI / 2) + ((2 * PI ) * i)), (((2 * PI ) / 3) + ((2 * PI ) * i)), ( PI + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume (( PI / 2) + a) <= r <= ( PI + a);

      then

       A1: ((( PI / 2) + a) - a) <= R <= (( PI + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( cos r) = ( cos R) by COMPLEX2: 9;

      then R in {( PI / 2), ((2 * PI ) / 3), PI } by A1, A2, A3, Th55;

      then R = ( PI / 2) or R = ((2 * PI ) / 3) or R = PI by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:57

    

     Th57: PI <= r <= ((3 * PI ) / 2) & (r / PI ) is rational & ( cos r) is rational implies r in { PI , ((4 * PI ) / 3), ((3 * PI ) / 2)}

    proof

      set R = (r - PI );

      assume PI <= r <= ((3 * PI ) / 2);

      then

       A1: ( PI - PI ) <= R <= (((3 * PI ) / 2) - PI ) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      

       A3: (R / PI ) = ((r / PI ) - ( PI / PI ))

      .= ((r / PI ) - 1) by XCMPLX_1: 60;

      ( cos R) = ( cos ( - ( PI - r)))

      .= ( cos ( PI - r)) by SIN_COS: 31

      .= ( - ( cos r)) by EUCLID10: 2;

      then R in { 0 , ( PI / 3), ( PI / 2)} by A1, A2, A3, Th53;

      then R = 0 or R = ( PI / 3) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:58

    ( PI + ((2 * PI ) * i)) <= r <= (((3 * PI ) / 2) + ((2 * PI ) * i)) & (r / PI ) is rational & ( cos r) is rational implies r in {( PI + ((2 * PI ) * i)), (((4 * PI ) / 3) + ((2 * PI ) * i)), (((3 * PI ) / 2) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume ( PI + a) <= r <= (((3 * PI ) / 2) + a);

      then

       A1: (( PI + a) - a) <= R <= ((((3 * PI ) / 2) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( cos r) = ( cos R) by COMPLEX2: 9;

      then R in { PI , ((4 * PI ) / 3), ((3 * PI ) / 2)} by A1, A2, A3, Th57;

      then R = PI or R = ((4 * PI ) / 3) or R = ((3 * PI ) / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:59

    

     Th59: ((3 * PI ) / 2) <= r <= (2 * PI ) & (r / PI ) is rational & ( cos r) is rational implies r in {((3 * PI ) / 2), ((5 * PI ) / 3), (2 * PI )}

    proof

      set R = ((2 * PI ) - r);

      assume ((3 * PI ) / 2) <= r <= (2 * PI );

      then

       A1: ((2 * PI ) - (2 * PI )) <= R <= ((2 * PI ) - ((3 * PI ) / 2)) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      

       A3: (R / PI ) = (((2 * PI ) / PI ) - (r / PI ))

      .= (2 - (r / PI )) by XCMPLX_1: 89;

      ( cos R) = ( cos r) by EUCLID10: 4;

      then R in { 0 , ( PI / 3), ( PI / 2)} by A1, A2, A3, Th53;

      then R = 0 or R = ( PI / 3) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:60

    (((3 * PI ) / 2) + ((2 * PI ) * i)) <= r <= ((2 * PI ) + ((2 * PI ) * i)) & (r / PI ) is rational & ( cos r) is rational implies r in {(((3 * PI ) / 2) + ((2 * PI ) * i)), (((5 * PI ) / 3) + ((2 * PI ) * i)), ((2 * PI ) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume (((3 * PI ) / 2) + a) <= r <= ((2 * PI ) + a);

      then

       A1: ((((3 * PI ) / 2) + a) - a) <= R <= (((2 * PI ) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( cos r) = ( cos R) by COMPLEX2: 9;

      then R in {((3 * PI ) / 2), ((5 * PI ) / 3), (2 * PI )} by A1, A2, A3, Th59;

      then R = ((3 * PI ) / 2) or R = ((5 * PI ) / 3) or R = (2 * PI ) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    

     Lm4: 0 <= r <= (2 * PI ) & (r / PI ) is rational & ( cos r) is rational implies ( cos r) in { 0 , 1, ( - 1), (1 / 2), ( - (1 / 2))}

    proof

      assume

       A1: 0 <= r <= (2 * PI );

      assume

       A2: (r / PI ) is rational & ( cos r) is rational;

      per cases by A1;

        suppose 0 <= r <= ( PI / 2);

        then r in { 0 , ( PI / 3), ( PI / 2)} by A2, Th53;

        then r = 0 or r = ( PI / 3) or r = ( PI / 2) by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, SIN_COS: 31, SIN_COS: 77, EUCLID10: 14;

      end;

        suppose ( PI / 2) <= r <= PI ;

        then r in {( PI / 2), ((2 * PI ) / 3), PI } by A2, Th55;

        then r = ( PI / 2) or r = ((2 * PI ) / 3) or r = PI by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, SIN_COS: 77, EUCLID10: 23;

      end;

        suppose PI <= r <= ((3 * PI ) / 2);

        then r in { PI , ((4 * PI ) / 3), ((3 * PI ) / 2)} by A2, Th57;

        then r = PI or r = ((4 * PI ) / 3) or r = ((3 * PI ) / 2) by ENUMSET1:def 1;

        hence thesis by Th11, ENUMSET1:def 3, SIN_COS: 77;

      end;

        suppose ((3 * PI ) / 2) <= r <= (2 * PI );

        then r in {((3 * PI ) / 2), ((5 * PI ) / 3), (2 * PI )} by A2, Th59;

        then r = ((3 * PI ) / 2) or r = ((5 * PI ) / 3) or r = (2 * PI ) by ENUMSET1:def 1;

        hence thesis by Th13, ENUMSET1:def 3, SIN_COS: 77;

      end;

    end;

    theorem :: NIVEN:61

    (r / PI ) is rational & ( cos r) is rational implies ( cos r) in { 0 , 1, ( - 1), (1 / 2), ( - (1 / 2))}

    proof

      consider i such that

       A0: ((2 * PI ) * i) <= r <= ((2 * PI ) * (i + 1)) by Th16;

      set a = ((2 * PI ) * i);

      set R = (r - a);

      

       A2: (a - a) <= R <= (((2 * PI ) + a) - a) by A0, XREAL_1: 9;

      assume

       A3: (r / PI ) is rational & ( cos r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A4: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( cos r) = ( cos R) by COMPLEX2: 9;

      hence thesis by A2, A3, A4, Lm4;

    end;

    theorem :: NIVEN:62

    

     Th62: 0 <= r <= ( PI / 2) & (r / PI ) is rational & ( sin r) is rational implies r in { 0 , ( PI / 6), ( PI / 2)}

    proof

      set t = (( PI / 2) - r);

      assume 0 <= r;

      then

       A1: t <= (( PI / 2) - 0 ) by XREAL_1: 10;

      assume r <= ( PI / 2);

      then

       A2: (( PI / 2) - ( PI / 2)) <= t by XREAL_1: 10;

      assume

       A3: (r / PI ) is rational & ( sin r) is rational;

      

       A4: (t / PI ) = ((( PI / 2) / PI ) - (r / PI ));

      

       A5: (( PI / 2) / PI ) = (1 / 2) by XCMPLX_1: 203;

      ( cos t) = ((( cos ( PI / 2)) * ( cos r)) + (( sin ( PI / 2)) * ( sin r))) by SIN_COS: 83

      .= ( sin r) by SIN_COS: 77;

      then t in { 0 , ( PI / 3), ( PI / 2)} by A1, A2, A3, A4, A5, Th53;

      then t = 0 or t = ( PI / 3) or t = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:63

    ((2 * PI ) * i) <= r <= (( PI / 2) + ((2 * PI ) * i)) & (r / PI ) is rational & ( sin r) is rational implies r in {((2 * PI ) * i), (( PI / 6) + ((2 * PI ) * i)), (( PI / 2) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume a <= r <= (( PI / 2) + a);

      then

       A1: (a - a) <= R <= ((( PI / 2) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( sin r) = ( sin R) by COMPLEX2: 8;

      then R in { 0 , ( PI / 6), ( PI / 2)} by A1, A2, A3, Th62;

      then R = 0 or R = ( PI / 6) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:64

    

     Th64: ( PI / 2) <= r <= PI & (r / PI ) is rational & ( sin r) is rational implies r in {( PI / 2), ((5 * PI ) / 6), PI }

    proof

      set R = ( PI - r);

      assume ( PI / 2) <= r <= PI ;

      then

       A1: ( PI - PI ) <= R <= ( PI - ( PI / 2)) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      

       A3: (R / PI ) = (( PI / PI ) - (r / PI ))

      .= (1 - (r / PI )) by XCMPLX_1: 60;

      ( sin R) = ( sin r) by EUCLID10: 1;

      then R in { 0 , ( PI / 6), ( PI / 2)} by A1, A2, A3, Th62;

      then R = 0 or R = ( PI / 6) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:65

    (( PI / 2) + ((2 * PI ) * i)) <= r <= ( PI + ((2 * PI ) * i)) & (r / PI ) is rational & ( sin r) is rational implies r in {(( PI / 2) + ((2 * PI ) * i)), (((5 * PI ) / 6) + ((2 * PI ) * i)), ( PI + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume (( PI / 2) + a) <= r <= ( PI + a);

      then

       A1: ((( PI / 2) + a) - a) <= R <= (( PI + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( sin r) = ( sin R) by COMPLEX2: 8;

      then R in {( PI / 2), ((5 * PI ) / 6), PI } by A1, A2, A3, Th64;

      then R = ( PI / 2) or R = ((5 * PI ) / 6) or R = PI by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:66

    

     Th66: PI <= r <= ((3 * PI ) / 2) & (r / PI ) is rational & ( sin r) is rational implies r in { PI , ((7 * PI ) / 6), ((3 * PI ) / 2)}

    proof

      set R = (r - PI );

      assume PI <= r <= ((3 * PI ) / 2);

      then

       A1: ( PI - PI ) <= R <= (((3 * PI ) / 2) - PI ) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      

       A3: (R / PI ) = ((r / PI ) - ( PI / PI ))

      .= ((r / PI ) - 1) by XCMPLX_1: 60;

      ( sin R) = ( sin ( - ( PI - r)))

      .= ( - ( sin ( PI - r))) by SIN_COS: 31

      .= ( - ( sin r)) by EUCLID10: 1;

      then R in { 0 , ( PI / 6), ( PI / 2)} by A1, A2, A3, Th62;

      then R = 0 or R = ( PI / 6) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:67

    ( PI + ((2 * PI ) * i)) <= r <= (((3 * PI ) / 2) + ((2 * PI ) * i)) & (r / PI ) is rational & ( sin r) is rational implies r in {( PI + ((2 * PI ) * i)), (((7 * PI ) / 6) + ((2 * PI ) * i)), (((3 * PI ) / 2) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume ( PI + a) <= r <= (((3 * PI ) / 2) + a);

      then

       A1: (( PI + a) - a) <= R <= ((((3 * PI ) / 2) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( sin r) = ( sin R) by COMPLEX2: 8;

      then R in { PI , ((7 * PI ) / 6), ((3 * PI ) / 2)} by A1, A2, A3, Th66;

      then R = PI or R = ((7 * PI ) / 6) or R = ((3 * PI ) / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:68

    

     Th68: ((3 * PI ) / 2) <= r <= (2 * PI ) & (r / PI ) is rational & ( sin r) is rational implies r in {((3 * PI ) / 2), ((11 * PI ) / 6), (2 * PI )}

    proof

      set R = ((2 * PI ) - r);

      assume ((3 * PI ) / 2) <= r <= (2 * PI );

      then

       A1: ((2 * PI ) - (2 * PI )) <= R <= ((2 * PI ) - ((3 * PI ) / 2)) by XREAL_1: 13;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      

       A3: (R / PI ) = (((2 * PI ) / PI ) - (r / PI ))

      .= (2 - (r / PI )) by XCMPLX_1: 89;

      ( sin R) = ( - ( sin r)) by EUCLID10: 3;

      then R in { 0 , ( PI / 6), ( PI / 2)} by A1, A2, A3, Th62;

      then R = 0 or R = ( PI / 6) or R = ( PI / 2) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: NIVEN:69

    (((3 * PI ) / 2) + ((2 * PI ) * i)) <= r <= ((2 * PI ) + ((2 * PI ) * i)) & (r / PI ) is rational & ( sin r) is rational implies r in {(((3 * PI ) / 2) + ((2 * PI ) * i)), (((11 * PI ) / 6) + ((2 * PI ) * i)), ((2 * PI ) + ((2 * PI ) * i))}

    proof

      set a = ((2 * PI ) * i);

      set R = (r - a);

      assume (((3 * PI ) / 2) + a) <= r <= ((2 * PI ) + a);

      then

       A1: ((((3 * PI ) / 2) + a) - a) <= R <= (((2 * PI ) + a) - a) by XREAL_1: 9;

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A3: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( sin r) = ( sin R) by COMPLEX2: 8;

      then R in {((3 * PI ) / 2), ((11 * PI ) / 6), (2 * PI )} by A1, A2, A3, Th68;

      then R = ((3 * PI ) / 2) or R = ((11 * PI ) / 6) or R = (2 * PI ) by ENUMSET1:def 1;

      hence thesis by ENUMSET1:def 1;

    end;

    

     Lm5: 0 <= r <= (2 * PI ) & (r / PI ) is rational & ( sin r) is rational implies ( sin r) in { 0 , 1, ( - 1), (1 / 2), ( - (1 / 2))}

    proof

      assume

       A1: 0 <= r <= (2 * PI );

      assume

       A2: (r / PI ) is rational & ( sin r) is rational;

      per cases by A1;

        suppose 0 <= r <= ( PI / 2);

        then r in { 0 , ( PI / 6), ( PI / 2)} by A2, Th62;

        then r = 0 or r = ( PI / 6) or r = ( PI / 2) by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, SIN_COS: 31, SIN_COS: 77, EUCLID10: 17;

      end;

        suppose ( PI / 2) <= r <= PI ;

        then r in {( PI / 2), ((5 * PI ) / 6), PI } by A2, Th64;

        then r = ( PI / 2) or r = ((5 * PI ) / 6) or r = PI by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, Th5, SIN_COS: 77;

      end;

        suppose PI <= r <= ((3 * PI ) / 2);

        then r in { PI , ((7 * PI ) / 6), ((3 * PI ) / 2)} by A2, Th66;

        then r = PI or r = ((7 * PI ) / 6) or r = ((3 * PI ) / 2) by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, Th7, SIN_COS: 77;

      end;

        suppose ((3 * PI ) / 2) <= r <= (2 * PI );

        then r in {((3 * PI ) / 2), ((11 * PI ) / 6), (2 * PI )} by A2, Th68;

        then r = ((3 * PI ) / 2) or r = ((11 * PI ) / 6) or r = (2 * PI ) by ENUMSET1:def 1;

        hence thesis by ENUMSET1:def 3, Th9, SIN_COS: 77;

      end;

    end;

    ::$Notion-Name

    theorem :: NIVEN:70

    (r / PI ) is rational & ( sin r) is rational implies ( sin r) in { 0 , 1, ( - 1), (1 / 2), ( - (1 / 2))}

    proof

      consider i such that

       A0: ((2 * PI ) * i) <= r <= ((2 * PI ) * (i + 1)) by Th16;

      set a = ((2 * PI ) * i);

      set R = (r - a);

      

       A2: (a - a) <= R <= (((2 * PI ) + a) - a) by A0, XREAL_1: 9;

      assume

       A3: (r / PI ) is rational & ( sin r) is rational;

      (a / PI ) = (((2 * i) * PI ) / PI )

      .= (2 * i) by XCMPLX_1: 89;

      then

       A4: (R / PI ) = ((r / PI ) - (2 * i));

      R = (((2 * PI ) * ( - i)) + r);

      then ( sin r) = ( sin R) by COMPLEX2: 8;

      hence thesis by A2, A3, A4, Lm5;

    end;