int_3.miz



    begin

    definition

      :: original: multint

      redefine

      :: INT_3:def1

      func multint means

      : Def1: for a,b be Element of INT holds (it . (a,b)) = ( multreal . (a,b));

      compatibility

      proof

        let b be BinOp of INT ;

        hereby

          assume

           A1: b = multint ;

          let i1,i2 be Element of INT ;

          

          thus (b . (i1,i2)) = (i1 * i2) by A1, BINOP_2:def 22

          .= ( multreal . (i1,i2)) by BINOP_2:def 11;

        end;

        assume

         A2: for i1,i2 be Element of INT holds (b . (i1,i2)) = ( multreal . (i1,i2));

        now

          let i1,i2 be Element of INT ;

          

          thus (b . (i1,i2)) = ( multreal . (i1,i2)) by A2

          .= (i1 * i2) by BINOP_2:def 11

          .= ( multint . (i1,i2)) by BINOP_2:def 22;

        end;

        hence b = multint by BINOP_1: 2;

      end;

    end

    definition

      :: original: compint

      redefine

      :: INT_3:def2

      func compint means for a be Element of INT holds (it . a) = ( compreal . a);

      compatibility

      proof

        let b be UnOp of INT ;

        hereby

          assume

           A1: b = compint ;

          let i be Element of INT ;

          

          thus (b . i) = ( - i) by A1, BINOP_2:def 19

          .= ( compreal . i) by BINOP_2:def 7;

        end;

        assume

         A2: for i be Element of INT holds (b . i) = ( compreal . i);

        now

          let i be Element of INT ;

          

          thus (b . i) = ( compreal . i) by A2

          .= ( - i) by BINOP_2:def 7

          .= ( compint . i) by BINOP_2:def 19;

        end;

        hence b = compint by FUNCT_2: 63;

      end;

    end

    definition

      :: INT_3:def3

      func INT.Ring -> doubleLoopStr equals doubleLoopStr (# INT , addint , multint , ( In (1, INT )), ( In ( 0 , INT )) #);

      coherence ;

    end

    registration

      cluster INT.Ring -> strict non empty;

      coherence ;

    end

    registration

      cluster the carrier of INT.Ring -> integer-membered;

      coherence ;

    end

    registration

      let a,b be Element of INT.Ring , c,d be Integer;

      identify c * d with a * b when a = c, b = d;

      compatibility

      proof

        assume

         A1: a = c & b = d;

        ( multint . (a,b)) = ( multreal . (a,b)) by Def1

        .= (c * d) by A1, BINOP_2:def 11;

        hence thesis;

      end;

      identify c + d with a + b when a = c, b = d;

      compatibility

      proof

        assume

         A2: a = c & b = d;

        ( addint . (a,b)) = ( addreal . (a,b)) by GR_CY_1:def 1

        .= (c + d) by A2, BINOP_2:def 9;

        hence thesis;

      end;

    end

    set M = INT.Ring ;

    registration

      cluster INT.Ring -> well-unital;

      coherence ;

    end

    registration

      cluster INT.Ring -> Abelian add-associative right_zeroed right_complementable distributive commutative associative domRing-like non degenerated;

      coherence

      proof

        thus for a,b be Element of M holds (a + b) = (b + a);

        thus for a,b,c be Element of M holds ((a + b) + c) = (a + (b + c));

        thus for a be Element of M holds (a + ( 0. M)) = a;

        thus M is right_complementable

        proof

          let a be Element of M;

          reconsider a9 = a as Integer;

          reconsider v = ( - a9) as Element of M by INT_1:def 2;

          take v;

          thus thesis;

        end;

        thus for a,b,c be Element of M holds (a * (b + c)) = ((a * b) + (a * c)) & ((b + c) * a) = ((b * a) + (c * a));

        thus for x,y be Element of M holds (x * y) = (y * x);

        thus for a,b,c be Element of M holds ((a * b) * c) = (a * (b * c));

        thus for a,b be Element of M st (a * b) = ( 0. M) holds a = ( 0. M) or b = ( 0. M) by XCMPLX_1: 6;

        thus ( 0. M) <> ( 1. M);

      end;

    end

    registration

      let a be Element of INT.Ring , b be Integer;

      identify - b with - a when a = b;

      compatibility

      proof

        reconsider b9 = ( - b) as Element of M by INT_1:def 2;

        assume b = a;

        then (b9 + a) = ( 0. M);

        hence thesis by RLVECT_1: 6;

      end;

    end

    definition

      ::$Canceled

      let a be Element of INT.Ring ;

      :: original: |.

      redefine

      func |.a.| -> Element of INT.Ring ;

      coherence

      proof

         |.a.| in INT by INT_1:def 2;

        hence thesis;

      end;

    end

    definition

      :: INT_3:def5

      func absint -> Function of INT.Ring , NAT means

      : Def5: for a be Element of INT.Ring holds (it . a) = ( absreal . a);

      existence

      proof

        ( dom absreal ) = REAL by FUNCT_2:def 1;

        then

         A1: ( dom ( absreal | INT )) = the carrier of INT.Ring by NUMBERS: 15, RELAT_1: 62;

        for y be object holds y in ( rng ( absreal | INT )) implies y in NAT

        proof

          let y be object;

          assume y in ( rng ( absreal | INT ));

          then

          consider x be object such that

           A2: [x, y] in ( absreal | INT ) by XTUPLE_0:def 13;

          

           A3: (( absreal | INT ) . x) = y by A2, FUNCT_1: 1;

          

           A4: x in ( dom ( absreal | INT )) by A2, XTUPLE_0:def 12;

          then

          reconsider x as Integer by A1;

          

           A5: (( absreal | INT ) . x) = ( absreal . x) by A1, A4, FUNCT_1: 49;

          now

            per cases ;

              case

               A6: 0 <= x;

              (( absreal | INT ) . x) = |.x.| by A5, EUCLID:def 2

              .= x by A6, ABSVALUE:def 1;

              hence (( absreal | INT ) . x) is Element of NAT by A6, INT_1: 3;

            end;

              case

               A7: not 0 <= x;

              (( absreal | INT ) . x) = |.x.| by A5, EUCLID:def 2

              .= ( - x) by A7, ABSVALUE:def 1;

              hence (( absreal | INT ) . x) is Element of NAT by A7, INT_1: 3;

            end;

          end;

          hence thesis by A3;

        end;

        then ( rng ( absreal | INT )) c= NAT by TARSKI:def 3;

        then

        reconsider f = ( absreal | INT ) as Function of INT.Ring , NAT by A1, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        thus thesis by FUNCT_1: 49;

      end;

      uniqueness

      proof

        deffunc F( Element of INT.Ring ) = ( absreal . $1);

        thus for f1,f2 be Function of INT.Ring , NAT st (for x be Element of INT.Ring holds (f1 . x) = F(x)) & (for x be Element of INT.Ring holds (f2 . x) = F(x)) holds f1 = f2 from BINOP_2:sch 1;

      end;

    end

    theorem :: INT_3:1

    

     Th1: for a be Element of INT.Ring holds ( absint . a) = |.a.|

    proof

      let a be Element of INT.Ring ;

      reconsider a9 = a as Integer;

      ( absint . a) = ( absreal . a9) by Def5

      .= |.a9.| by EUCLID:def 2;

      hence thesis;

    end;

    

     Lm1: for a be Integer holds a = 0 or ( absreal . a) >= 1

    proof

      let a be Integer;

      assume

       A1: a <> 0 ;

      per cases ;

        suppose 0 <= a;

        then

        reconsider a as Element of NAT by INT_1: 3;

        

         A2: ( absreal . a) = |.a.| by EUCLID:def 2

        .= a by ABSVALUE:def 1;

        ( 0 + 1) < (a + 1) by A1, XREAL_1: 6;

        hence thesis by A2, NAT_1: 13;

      end;

        suppose

         A3: a < 0 ;

        then a <= ( - 1) by INT_1: 8;

        then

         A4: ( - ( - 1)) <= ( - a) by XREAL_1: 24;

        ( absreal . a) = |.a.| by EUCLID:def 2

        .= ( - a) by A3, ABSVALUE:def 1;

        hence thesis by A4;

      end;

    end;

    

     Lm2: for a,b be Element of INT.Ring st b <> ( 0. INT.Ring ) holds for b9 be Integer st b9 = b holds 0 <= b9 implies ex q,r be Element of INT.Ring st a = ((q * b) + r) & (r = ( 0. INT.Ring ) or ( absint . r) < ( absint . b))

    proof

      let a,b be Element of M;

      assume

       A1: b <> ( 0. M);

      reconsider a9 = a as Integer;

      let b9 be Integer;

      assume

       A2: b9 = b;

      defpred P[ Nat] means ex s be Integer st $1 = (a9 - (s * b9));

      assume

       A3: 0 <= b9;

      

       A4: ex k be Nat st P[k]

      proof

        now

          per cases ;

            case 0 <= a9;

            then

            reconsider a9 as Element of NAT by INT_1: 3;

            (a9 - ( 0 * b9)) = a9;

            hence thesis;

          end;

            case

             A5: a9 < 0 ;

            (1 + 0 ) <= b9 by A1, A2, A3, INT_1: 7;

            then (1 - 1) <= (b9 - 1) by XREAL_1: 9;

            then

            reconsider m = (b9 - 1) as Element of NAT by INT_1: 3;

            reconsider n = ( - a9) as Element of NAT by A5, INT_1: 3;

            (a9 - (a9 * b9)) = (( - a9) * (b9 - 1)) & (n * m) is Element of NAT by ORDINAL1:def 12;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A4);

      then

      consider k9 be Nat such that

       A6: ex s be Integer st k9 = (a9 - (s * b9)) & for n be Nat st ex s9 be Integer st n = (a9 - (s9 * b9)) holds k9 <= n;

      consider l9 be Integer such that

       A7: k9 = (a9 - (l9 * b9)) by A6;

      reconsider k = k9, l = l9 as Element of M by INT_1:def 2;

      

       A8: k9 = 0 or k9 < b9

      proof

        assume k9 <> 0 ;

        assume b9 <= k9;

        then

        reconsider k = (k9 - b9) as Element of NAT by INT_1: 5;

        

         A9: k9 > k

        proof

          reconsider b9 as Element of NAT by A3, INT_1: 3;

          assume k9 <= k;

          then

          consider x be Nat such that

           A10: k = (k9 + x) by NAT_1: 10;

          ( - x) = b9 by A10;

          hence contradiction by A1, A2;

        end;

        (k9 - b9) = (a9 - ((l9 + 1) * b9)) by A7;

        hence thesis by A6, A9;

      end;

      

       A11: k = ( 0. M) or ( absint . k) < ( absint . b)

      proof

        reconsider b9 as Element of NAT by A3, INT_1: 3;

        assume

         A12: k <> ( 0. M);

        

         A13: ( absint . k) = ( absreal . k) by Def5

        .= |.k9.| by EUCLID:def 2

        .= k9 by ABSVALUE:def 1;

        ( absint . b) = ( absreal . b9) by A2, Def5

        .= |.b9.| by EUCLID:def 2

        .= b9 by ABSVALUE:def 1;

        hence thesis by A8, A12, A13;

      end;

      (k + (l * b)) = a by A2, A7;

      hence thesis by A11;

    end;

    theorem :: INT_3:2

    for a,b,q1,q2,r1,r2 be Element of INT.Ring st b <> ( 0. INT.Ring ) & a = ((q1 * b) + r1) & ( 0. INT.Ring ) <= r1 & r1 < |.b.| & a = ((q2 * b) + r2) & ( 0. INT.Ring ) <= r2 & r2 < |.b.| holds q1 = q2 & r1 = r2

    proof

      let a,b,q1,q2,r1,r2 be Element of INT.Ring ;

      assume that

       A1: b <> ( 0. INT.Ring ) and

       A2: a = ((q1 * b) + r1) and

       A3: ( 0. INT.Ring ) <= r1 and

       A4: r1 < |.b.| and

       A5: a = ((q2 * b) + r2) and

       A6: ( 0. INT.Ring ) <= r2 and

       A7: r2 < |.b.|;

      reconsider r29 = r2, r19 = r1, q29 = q2, q19 = q1, b9 = b as Integer;

      now

        per cases ;

          case

           A8: 0 <= (r19 - r29);

          

           A9: ((q29 - q19) * b9) = (r19 - r29) by A2, A5;

          now

            per cases ;

              case 0 = (r19 - r29);

              then (q29 - q19) = 0 or b9 = 0 by A9, XCMPLX_1: 6;

              hence q1 = q2 by A1;

            end;

              case 0 <> (r19 - r29);

              then

               A10: 0 <> (q29 - q19) by A9;

              

               A11: (( absreal . (q29 - q19)) * ( absreal . b9)) >= ( absreal . b9)

              proof

                reconsider e = (q2 + ( - q1)) as Element of M;

                reconsider d9 = (q29 - q19) as Integer;

                ( absreal . b9) = ( absint . b) by Def5;

                then

                reconsider c = ( absreal . b9) as Element of NAT ;

                ( absreal . d9) = ( absint . e) by Def5;

                then

                reconsider d = ( absreal . d9) as Element of NAT ;

                (d * c) >= (1 * c) by A10, Lm1, NAT_1: 4;

                hence thesis;

              end;

              

               A12: (r19 + ( - r29)) <= (r19 + 0 ) by A6, XREAL_1: 6;

              

               A13: |.b.| = ( absint . b) by Th1

              .= ( absreal . b) by Def5;

              (r19 - r29) = |.((q29 - q19) * b9).| by A2, A5, A8, ABSVALUE:def 1

              .= ( |.(q29 - q19).| * |.b9.|) by COMPLEX1: 65

              .= (( absreal . (q29 - q19)) * |.b9.|) by EUCLID:def 2

              .= (( absreal . (q29 - q19)) * ( absreal . b9)) by EUCLID:def 2;

              hence q1 = q2 by A4, A11, A12, A13, XXREAL_0: 2;

            end;

          end;

          hence q1 = q2;

        end;

          case

           A14: (r19 - r29) < 0 ;

          ( - (r19 - r29)) = (r29 - r19) & ((q19 - q29) * b9) = (r29 - r19) by A2, A5;

          then

           A15: 0 <> (q19 - q29) by A14, XREAL_1: 58;

          

           A16: (( absreal . (q19 - q29)) * ( absreal . b9)) >= ( absreal . b9)

          proof

            reconsider e = (q1 + ( - q2)) as Element of M;

            reconsider d9 = (q19 - q29) as Integer;

            ( absreal . b9) = ( absint . b) by Def5;

            then

            reconsider c = ( absreal . b9) as Element of NAT ;

            ( absreal . d9) = ( absint . e) by Def5;

            then

            reconsider d = ( absreal . d9) as Element of NAT ;

            (d * c) >= (1 * c) by A15, Lm1, NAT_1: 4;

            hence thesis;

          end;

          

           A17: |.b.| = ( absint . b) by Th1

          .= ( absreal . b) by Def5;

          ( - (r19 - r29)) > 0 by A14, XREAL_1: 58;

          

          then

           A18: (r29 - r19) = |.((q19 - q29) * b9).| by A2, A5, ABSVALUE:def 1

          .= ( |.(q19 - q29).| * |.b9.|) by COMPLEX1: 65

          .= (( absreal . (q19 - q29)) * |.b9.|) by EUCLID:def 2

          .= (( absreal . (q19 - q29)) * ( absreal . b9)) by EUCLID:def 2;

          (r29 + ( - r19)) <= (r29 + 0 ) by A3, XREAL_1: 6;

          hence q1 = q2 by A7, A16, A17, A18, XXREAL_0: 2;

        end;

      end;

      hence thesis by A2, A5;

    end;

    definition

      ::$Canceled

      let a,b be Element of INT.Ring ;

      :: original: div

      redefine

      func a div b -> Element of INT.Ring ;

      coherence by INT_1:def 2;

      :: original: mod

      redefine

      func a mod b -> Element of INT.Ring ;

      coherence by INT_1:def 2;

    end

    theorem :: INT_3:3

    for a,b be Element of INT.Ring st b <> ( 0. INT.Ring ) holds a = (((a div b) * b) + (a mod b)) by INT_1: 59;

    begin

    definition

      let I be non empty doubleLoopStr;

      :: INT_3:def8

      attr I is Euclidian means

      : Def8: ex f be Function of I, NAT st for a,b be Element of I st b <> ( 0. I) holds ex q,r be Element of I st a = ((q * b) + r) & (r = ( 0. I) or (f . r) < (f . b));

    end

    registration

      cluster INT.Ring -> Euclidian;

      coherence

      proof

        take absint ;

        let a,b be Element of M;

        reconsider b9 = b as Integer;

        assume

         A1: b <> ( 0. M);

        now

          per cases ;

            case 0 <= b9;

            hence thesis by A1, Lm2;

          end;

            case

             A2: b9 < 0 ;

            reconsider c = ( - b9) as Element of M by INT_1:def 2;

             0 < ( - b9) by A2, XREAL_1: 58;

            then

            consider q,r be Element of M such that

             A3: a = ((q * c) + r) and

             A4: r = ( 0. M) or ( absint . r) < ( absint . c) by Lm2;

            

             A5: r = ( 0. M) or ( absint . r) < ( absint . b)

            proof

              assume

               A6: r <> ( 0. M);

              ( absint . c) = ( absreal . c) by Def5

              .= |.( - b9).| by EUCLID:def 2

              .= ( - b9) by A2, ABSVALUE:def 1

              .= |.b9.| by A2, ABSVALUE:def 1

              .= ( absreal . b9) by EUCLID:def 2

              .= ( absint . b) by Def5;

              hence thesis by A4, A6;

            end;

            reconsider t = ( - q) as Element of M;

            ((t * b) + r) = a by A3;

            hence ex q,r be Element of M st a = ((q * b) + r) & (r = ( 0. M) or ( absint . r) < ( absint . b)) by A5;

          end;

        end;

        hence thesis;

      end;

    end

    

     Lm4: for F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr holds for f be Function of F, NAT holds for a,b be Element of F st b <> ( 0. F) holds ex q,r be Element of F st a = ((q * b) + r) & (r = ( 0. F) or (f . r) < (f . b))

    proof

      let F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr;

      let f be Function of F, NAT ;

      now

        let a,b be Element of F;

        assume

         A1: b <> ( 0. F);

        ex q,r be Element of F st a = ((q * b) + r) & (r = ( 0. F) or (f . r) < (f . b))

        proof

          consider x be Element of F such that

           A2: (x * b) = ( 1. F) by A1, VECTSP_1:def 9;

          (((a * x) * b) + ( 0. F)) = ((a * ( 1. F)) + ( 0. F)) by A2, GROUP_1:def 3

          .= (a + ( 0. F))

          .= a by RLVECT_1:def 4;

          hence thesis;

        end;

        hence b <> ( 0. F) implies ex q,r be Element of F st a = ((q * b) + r) & (r = ( 0. F) or (f . r) < (f . b));

      end;

      hence thesis;

    end;

    registration

      cluster strict Euclidian domRing-like non degenerated distributive commutative for Ring;

      existence

      proof

        take INT.Ring ;

        thus thesis;

      end;

    end

    definition

      mode EuclidianRing is Euclidian domRing-like non degenerated distributive commutative Ring;

    end

    definition

      let E be Euclidian non empty doubleLoopStr;

      :: INT_3:def9

      mode DegreeFunction of E -> Function of E, NAT means

      : Def9: for a,b be Element of E st b <> ( 0. E) holds ex q,r be Element of E st a = ((q * b) + r) & (r = ( 0. E) or (it . r) < (it . b));

      existence by Def8;

    end

    theorem :: INT_3:4

    

     Th4: for E be EuclidianRing holds E is gcdDomain

    proof

      let E be EuclidianRing;

      set d = the DegreeFunction of E;

      now

        let x,y be Element of E;

        now

          per cases ;

            case

             A1: x = ( 0. E);

            (y * ( 0. E)) = ( 0. E);

            then

             A2: y divides ( 0. E) by GCD_1:def 1;

            for zz be Element of E st zz divides x & zz divides y holds zz divides y;

            hence ex z be Element of E st z divides x & z divides y & for zz be Element of E st zz divides x & zz divides y holds zz divides z by A1, A2;

          end;

            case

             A3: x <> ( 0. E);

            set M = { z where z be Element of E : ex s,t be Element of E st z = ((s * x) + (t * y)) };

            defpred P[ Nat] means ex z be Element of E st (z in M & z <> ( 0. E) & $1 = (d . z));

            ((( 1. E) * x) + (( 0. E) * y)) = (( 1. E) * x) by RLVECT_1:def 4

            .= x;

            then

             A4: x in M;

            ex k be Element of NAT st k = (d . x);

            then

             A5: ex k be Nat st P[k] by A3, A4;

            ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A5);

            then

            consider k be Nat such that

             A6: P[k] & for n be Nat st P[n] holds k <= n;

            consider g be Element of E such that

             A7: g in M and

             A8: g <> ( 0. E) and

             A9: k = (d . g) & for n be Nat st (ex z be Element of E st z in M & z <> ( 0. E) & n = (d . z)) holds k <= n by A6;

            set G = { z where z be Element of E : ex r be Element of E st z = (r * g) };

            

             A10: for z be object holds z in M implies z in G

            proof

              let z be object;

              assume z in M;

              then

              consider z2 be Element of E such that

               A11: z = z2 and

               A12: ex s,t be Element of E st z2 = ((s * x) + (t * y));

              consider u,v be Element of E such that

               A13: z2 = ((u * x) + (v * y)) by A12;

              reconsider z as Element of E by A11;

              consider q,r be Element of E such that

               A14: z = ((q * g) + r) and

               A15: r = ( 0. E) or (d . r) < (d . g) by A8, Def9;

              r in M

              proof

                consider z1 be Element of E such that

                 A16: g = z1 and

                 A17: ex s,t be Element of E st z1 = ((s * x) + (t * y)) by A7;

                consider s,t be Element of E such that

                 A18: z1 = ((s * x) + (t * y)) by A17;

                (z + ( - (q * g))) = (r + ((q * g) + ( - (q * g)))) by A14, RLVECT_1:def 3

                .= (r + ( 0. E)) by RLVECT_1:def 10

                .= r by RLVECT_1:def 4;

                

                then r = (z + ( - ((q * (s * x)) + (q * (t * y))))) by A16, A18, VECTSP_1:def 7

                .= (z + (( - (q * (s * x))) + ( - (q * (t * y))))) by RLVECT_1: 31

                .= ((((u * x) + (v * y)) + ( - (q * (s * x)))) + ( - (q * (t * y)))) by A11, A13, RLVECT_1:def 3

                .= ((((u * x) + ( - (q * (s * x)))) + (v * y)) + ( - (q * (t * y)))) by RLVECT_1:def 3

                .= (((u * x) + ( - (q * (s * x)))) + ((v * y) + ( - (q * (t * y))))) by RLVECT_1:def 3

                .= (((u * x) + (( - q) * (s * x))) + ((v * y) + ( - (q * (t * y))))) by GCD_1: 48

                .= (((u * x) + (( - q) * (s * x))) + ((v * y) + (( - q) * (t * y)))) by GCD_1: 48

                .= (((u * x) + ((( - q) * s) * x)) + ((v * y) + (( - q) * (t * y)))) by GROUP_1:def 3

                .= (((u * x) + ((( - q) * s) * x)) + ((v * y) + ((( - q) * t) * y))) by GROUP_1:def 3

                .= (((u + (( - q) * s)) * x) + ((v * y) + ((( - q) * t) * y))) by VECTSP_1:def 7

                .= (((u + (( - q) * s)) * x) + ((v + (( - q) * t)) * y)) by VECTSP_1:def 7;

                hence thesis;

              end;

              then r = ( 0. E) by A9, A15;

              then z = (q * g) by A14, RLVECT_1:def 4;

              hence thesis;

            end;

            

             A19: for z be Element of E holds z divides x & z divides y implies z divides g

            proof

              let z be Element of E;

              assume that

               A20: z divides x and

               A21: z divides y;

              consider u be Element of E such that

               A22: x = (z * u) by A20, GCD_1:def 1;

              consider zz be Element of E such that

               A23: g = zz and

               A24: ex s,t be Element of E st zz = ((s * x) + (t * y)) by A7;

              consider s,t be Element of E such that

               A25: zz = ((s * x) + (t * y)) by A24;

              consider v be Element of E such that

               A26: y = (z * v) by A21, GCD_1:def 1;

              g = (((s * u) * z) + (t * (v * z))) by A22, A26, A23, A25, GROUP_1:def 3

              .= (((s * u) * z) + ((t * v) * z)) by GROUP_1:def 3

              .= (((s * u) + (t * v)) * z) by VECTSP_1:def 7;

              hence thesis by GCD_1:def 1;

            end;

            ((( 0. E) * x) + (( 1. E) * y)) = (( 1. E) * y) by RLVECT_1: 4

            .= y;

            then

             A27: y in M;

            for z be object holds z in G implies z in M

            proof

              let z be object;

              assume z in G;

              then

              consider z2 be Element of E such that

               A28: z = z2 and

               A29: ex s be Element of E st z2 = (s * g);

              reconsider z as Element of E by A28;

              consider u be Element of E such that

               A30: z2 = (u * g) by A29;

              consider z1 be Element of E such that

               A31: g = z1 and

               A32: ex s,t be Element of E st z1 = ((s * x) + (t * y)) by A7;

              consider s,t be Element of E such that

               A33: z1 = ((s * x) + (t * y)) by A32;

              z = ((u * (s * x)) + (u * (t * y))) by A28, A30, A31, A33, VECTSP_1:def 2

              .= (((u * s) * x) + (u * (t * y))) by GROUP_1:def 3

              .= (((u * s) * x) + ((u * t) * y)) by GROUP_1:def 3;

              hence thesis;

            end;

            then

             A34: M = G by A10, TARSKI: 2;

            g divides x & g divides y

            proof

              (ex zz be Element of E st x = zz & ex r be Element of E st zz = (r * g)) & ex zzz be Element of E st y = zzz & ex r be Element of E st zzz = (r * g) by A4, A27, A34;

              hence thesis by GCD_1:def 1;

            end;

            hence ex z be Element of E st z divides x & z divides y & for zz be Element of E st zz divides x & zz divides y holds zz divides z by A19;

          end;

        end;

        hence ex z be Element of E st z divides x & z divides y & for zz be Element of E st zz divides x & zz divides y holds zz divides z;

      end;

      hence thesis by GCD_1:def 11;

    end;

    registration

      cluster Euclidian -> gcd-like for domRing-like Abelian add-associative right_zeroed right_complementable associative commutative well-unital right-distributive non degenerated doubleLoopStr;

      coherence by Th4;

    end

    definition

      :: original: absint

      redefine

      func absint -> DegreeFunction of INT.Ring ;

      coherence

      proof

        let a,b be Element of M;

        assume

         A1: b <> ( 0. M);

        per cases ;

          suppose 0 <= b;

          hence thesis by A1, Lm2;

        end;

          suppose

           A2: b < 0 ;

          reconsider c = ( - b) as Element of M;

           0 < ( - b) by A2, XREAL_1: 58;

          then

          consider q,r be Element of M such that

           A3: a = ((q * c) + r) and

           A4: r = ( 0. M) or ( absint . r) < ( absint . c) by Lm2;

          

           A5: r = ( 0. M) or ( absint . r) < ( absint . b)

          proof

            assume

             A6: r <> ( 0. M);

            ( absint . c) = ( absreal . c) by Def5

            .= |.( - b).| by EUCLID:def 2

            .= ( - b) by A2, ABSVALUE:def 1

            .= |.b.| by A2, ABSVALUE:def 1

            .= ( absreal . b) by EUCLID:def 2

            .= ( absint . b) by Def5;

            hence thesis by A4, A6;

          end;

          reconsider t = ( - q) as Element of M;

          ((t * b) + r) = a by A3;

          hence thesis by A5;

        end;

      end;

    end

    theorem :: INT_3:5

    

     Th5: for F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr holds F is Euclidian

    proof

      let F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr;

      set f = the Function of F, NAT ;

      for a,b be Element of F st b <> ( 0. F) holds ex q,r be Element of F st a = ((q * b) + r) & (r = ( 0. F) or (f . r) < (f . b)) by Lm4;

      hence thesis;

    end;

    registration

      cluster commutative associative well-unital almost_left_invertible right_zeroed -> Euclidian for non empty doubleLoopStr;

      coherence by Th5;

    end

    theorem :: INT_3:6

    for F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr holds for f be Function of F, NAT holds f is DegreeFunction of F

    proof

      let F be commutative associative well-unital almost_left_invertible right_zeroed non empty doubleLoopStr;

      let f be Function of F, NAT ;

      for a,b be Element of F st b <> ( 0. F) holds ex q,r be Element of F st a = ((q * b) + r) & (r = ( 0. F) or (f . r) < (f . b)) by Lm4;

      hence thesis by Def9;

    end;

    begin

    definition

      let n be natural Number;

      :: INT_3:def10

      func multint (n) -> BinOp of ( Segm n) means

      : Def10: for k,l be Element of ( Segm n) holds (it . (k,l)) = ((k * l) mod n);

      existence

      proof

        reconsider n as non zero Nat by A1, TARSKI: 1;

        defpred P[ Element of ( Segm n), Element of ( Segm n), set] means $3 = (($1 * $2) mod n);

        

         A2: for k,l be Element of ( Segm n) holds ex c be Element of ( Segm n) st P[k, l, c]

        proof

          let k,l be Element of ( Segm n);

          reconsider k9 = k, l9 = l as Element of NAT ;

          ((k9 * l9) mod n) < n by NAT_D: 1;

          then

          reconsider c = ((k9 * l9) mod n) as Element of ( Segm n) by NAT_1: 44;

          take c;

          thus thesis;

        end;

        ex c be BinOp of ( Segm n) st for k,l be Element of ( Segm n) holds P[k, l, (c . (k,l))] from BINOP_1:sch 3( A2);

        hence thesis;

      end;

      uniqueness

      proof

        reconsider n as non zero natural Number by A1;

        deffunc O( Element of ( Segm n), Element of ( Segm n)) = (($1 * $2) mod n);

        for o1,o2 be BinOp of ( Segm n) st (for a,b be Element of ( Segm n) holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of ( Segm n) holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

        hence thesis;

      end;

    end

    definition

      let n be natural Number;

      :: INT_3:def11

      func compint (n) -> UnOp of ( Segm n) means

      : Def11: for k be Element of ( Segm n) holds (it . k) = ((n - k) mod n);

      existence

      proof

        reconsider n as non zero Nat by A1, TARSKI: 1;

        set f = { [k, ((n - k) mod n)] where k be Element of NAT : k < n };

        

         A2: for x be object st x in f holds ex y,z be object st x = [y, z]

        proof

          let x be object;

          assume x in f;

          then ex k be Element of NAT st x = [k, ((n - k) mod n)] & k < n;

          hence thesis;

        end;

        for x,y1,y2 be object st [x, y1] in f & [x, y2] in f holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume that

           A3: [x, y1] in f and

           A4: [x, y2] in f;

          consider k be Element of NAT such that

           A5: [x, y1] = [k, ((n - k) mod n)] and k < n by A3;

          

           A6: y1 = ((n - k) mod n) by A5, XTUPLE_0: 1;

          consider k9 be Element of NAT such that

           A7: [x, y2] = [k9, ((n - k9) mod n)] and k9 < n by A4;

          

           A8: y2 = ((n - k9) mod n) by A7, XTUPLE_0: 1;

          k = x by A5, XTUPLE_0: 1

          .= k9 by A7, XTUPLE_0: 1;

          hence thesis by A6, A8;

        end;

        then

        reconsider f as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;

        

         A9: for x be object holds x in ( Segm n) implies x in ( dom f)

        proof

          let x be object;

          assume

           A10: x in ( Segm n);

          then

          reconsider x as Element of NAT ;

          x < n by A10, NAT_1: 44;

          then [x, ((n - x) mod n)] in f;

          hence thesis by XTUPLE_0:def 12;

        end;

        for x be object holds x in ( dom f) implies x in ( Segm n)

        proof

          let x be object;

          assume x in ( dom f);

          then

          consider y be object such that

           A11: [x, y] in f by XTUPLE_0:def 12;

          consider k be Element of NAT such that

           A12: [x, y] = [k, ((n - k) mod n)] and

           A13: k < n by A11;

          x = k by A12, XTUPLE_0: 1;

          hence thesis by A13, NAT_1: 44;

        end;

        then

         A14: ( dom f) = ( Segm n) by A9, TARSKI: 2;

        for y be object holds y in ( rng f) implies y in ( Segm n)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A15: [x, y] in f by XTUPLE_0:def 13;

          consider k be Element of NAT such that

           A16: [x, y] = [k, ((n - k) mod n)] and

           A17: k < n by A15;

          (k - k) < (n - k) by A17, XREAL_1: 9;

          then

          reconsider z = (n - k) as Element of NAT by INT_1: 3;

          

           A18: (z mod n) < n by NAT_D: 1;

          y = ((n - k) mod n) by A16, XTUPLE_0: 1;

          hence thesis by A18, NAT_1: 44;

        end;

        then ( rng f) c= ( Segm n) by TARSKI:def 3;

        then

        reconsider f as UnOp of ( Segm n) by A14, FUNCT_2:def 1, RELSET_1: 4;

        for k be Element of ( Segm n) holds (f . k) = ((n - k) mod n)

        proof

          let k be Element of ( Segm n);

          reconsider k as Element of NAT ;

          

           A0: ((n - k) mod n) is set by TARSKI: 1;

          k < n by NAT_1: 44;

          then [k, ((n - k) mod n)] in f;

          hence thesis by A14, A0, FUNCT_1:def 2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        reconsider n as non zero Nat by A1, TARSKI: 1;

        deffunc F( Element of ( Segm n)) = ((n - $1) mod n);

        for f1,f2 be UnOp of ( Segm n) st (for a be Element of ( Segm n) holds (f1 . a) = F(a)) & (for a be Element of ( Segm n) holds (f2 . a) = F(a)) holds f1 = f2 from LMOD_7:sch 2;

        hence thesis;

      end;

    end

    theorem :: INT_3:7

    

     Th7: for n be Nat st n > 0 holds for a,b be Element of ( Segm n) holds ((a + b) < n iff (( addint n) . (a,b)) = (a + b)) & ((a + b) >= n iff (( addint n) . (a,b)) = ((a + b) - n))

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      let a,b be Element of ( Segm n);

      reconsider n as non zero Nat by A1;

      consider c be Element of NAT such that

       A2: c = ((a + b) mod n);

      consider t be Nat such that

       A3: (a + b) = ((n * t) + c) & c < n or c = 0 & n = 0 by A2, NAT_D:def 2;

       A4:

      now

        assume

         A5: (a + b) >= n;

        t = 1

        proof

          now

            per cases ;

              case t = 0 ;

              hence thesis by A3, A5;

            end;

              case

               A6: t <> 0 ;

              t < 2

              proof

                a < n & b < n by NAT_1: 44;

                then

                 A7: ((n * t) + c) >= (n * t) & (a + b) < ((n * 1) + (n * 1)) by NAT_1: 11, XREAL_1: 8;

                assume t >= 2;

                then (n * t) >= (n * 2) by XREAL_1: 64;

                hence thesis by A3, A7, XXREAL_0: 2;

              end;

              then t < (1 + 1);

              then

               A8: t <= 1 by NAT_1: 13;

              (1 + 0 ) <= t by A6, INT_1: 7;

              hence thesis by A8, XXREAL_0: 1;

            end;

          end;

          hence thesis;

        end;

        hence (( addint n) . (a,b)) = ((a + b) - n) by A2, A3, GR_CY_1:def 4;

      end;

      

       A9: (( addint n) . (a,b)) = ((a + b) - n) implies (a + b) >= n

      proof

        assume (( addint n) . (a,b)) = ((a + b) - n);

        then

         A10: ((a + b) mod n) = ((a + b) - n) by GR_CY_1:def 4;

        consider t be Nat such that

         A11: (a + b) = ((n * t) + ((a + b) mod n)) and ((a + b) mod n) < n by NAT_D:def 2;

        assume

         A12: (a + b) < n;

        t = 0

        proof

          assume t <> 0 ;

          then (1 + 0 ) <= t by INT_1: 7;

          then

           A13: (1 * n) <= (t * n) by XREAL_1: 64;

          (t * n) <= ((t * n) + ((a + b) mod n)) by NAT_1: 11;

          hence thesis by A12, A11, A13, XXREAL_0: 2;

        end;

        hence thesis by A10, A11;

      end;

       A14:

      now

        assume

         A15: (a + b) < n;

        t = 0

        proof

          assume t <> 0 ;

          then (1 + 0 ) <= t by INT_1: 7;

          then

           A16: (1 * n) <= (t * n) by XREAL_1: 64;

          (n * t) <= ((n * t) + c) by NAT_1: 11;

          hence thesis by A3, A15, A16, XXREAL_0: 2;

        end;

        hence (( addint n) . (a,b)) = (a + b) by A2, A3, GR_CY_1:def 4;

      end;

      (( addint n) . (a,b)) = (a + b) implies (a + b) < n

      proof

        assume (( addint n) . (a,b)) = (a + b);

        then ((a + b) mod n) = (a + b) by GR_CY_1:def 4;

        hence thesis by NAT_D: 1;

      end;

      hence thesis by A14, A9, A4;

    end;

    

     Lm5: for a,b be Nat st b <> 0 holds ex k be Element of NAT st (k * b) <= a & a < ((k + 1) * b)

    proof

      let a,b be Nat;

      set k9 = (a div b);

      assume b <> 0 ;

      then

       A1: ex t be Nat st a = ((b * k9) + t) & t < b by NAT_D:def 1;

      ((k9 + 1) * b) = ((k9 * b) + b);

      then ((k9 + 1) * b) > a by A1, XREAL_1: 6;

      hence thesis by A1, NAT_1: 11;

    end;

    theorem :: INT_3:8

    

     Th8: for n be Nat st n > 0 holds for a,b be Element of ( Segm n) holds for k be Nat holds (k * n) <= (a * b) & (a * b) < ((k + 1) * n) iff (( multint n) . (a,b)) = ((a * b) - (k * n))

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      let a,b be Element of ( Segm n);

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

      let k be Nat;

       A2:

      now

        assume that

         A3: (k * n) <= (a * b) and

         A4: (a * b) < ((k + 1) * n);

        consider c be Element of NAT such that

         A5: c = ((a * b) mod n);

        consider t be Nat such that

         A6: (a * b) = ((n * t) + c) & c < n or c = 0 & n = 0 by A5, NAT_D:def 2;

        now

          consider q be Nat such that

           A7: (a * b) = ((k * n) + q) by A3, NAT_1: 10;

          t = k

          proof

            now

              per cases ;

                case t <= k;

                then

                consider r be Nat such that

                 A8: (t + r) = k by NAT_1: 10;

                

                 A9: ((n * t) + c) = ((t * n) + ((r * n) + q)) by A1, A6, A7, A8;

                now

                  per cases ;

                    case t = k;

                    hence thesis;

                  end;

                    case

                     A10: t <> k;

                    r >= 1

                    proof

                      assume

                       A11: r < 1;

                      r = 0

                      proof

                        assume r <> 0 ;

                        then (1 + 0 ) <= r by INT_1: 7;

                        hence thesis by A11;

                      end;

                      hence thesis by A8, A10;

                    end;

                    then (r * n) >= (1 * n) by NAT_1: 4;

                    then

                     A12: ((r * n) + q) >= ((1 * n) + q) by XREAL_1: 6;

                    ((1 * n) + q) >= n by NAT_1: 11;

                    hence thesis by A1, A6, A9, A12, XXREAL_0: 2;

                  end;

                end;

                hence thesis;

              end;

                case t > k;

                then t >= (k + 1) by INT_1: 7;

                then

                 A13: (n * t) >= (n * (k + 1)) by NAT_1: 4;

                ((n * t) + c) >= (n * t) by NAT_1: 11;

                hence thesis by A4, A6, A13, XXREAL_0: 2;

              end;

            end;

            hence thesis;

          end;

          hence (( multint n) . (a,b)) = ((a * b) - (k * n)) by A1, A5, A6, Def10;

        end;

        hence (( multint n) . (a,b)) = ((a * b) - (k * n));

      end;

      now

        assume (( multint n) . (a,b)) = ((a * b) - (k * n));

        then ((a * b) mod n) = ((a * b) - (k * n)) by A1, Def10;

        then

         A14: (((a * b) - (k * n)) + (k * n)) >= ( 0 + (k * n)) & ex t be Nat st (a * b) = ((n * t) + ((a * b) - (n * k))) & ((a * b) - (n * k)) < n by A1, NAT_D:def 2, XREAL_1: 6;

        ((k + 1) * n) = ((k * n) + n);

        hence (k * n) <= (a * b) & (a * b) < ((k + 1) * n) by A14, XREAL_1: 6;

      end;

      hence thesis by A2;

    end;

    theorem :: INT_3:9

    for n be Nat st n > 0 holds for a be Element of ( Segm n) holds (a = 0 iff (( compint n) . a) = 0 ) & (a <> 0 iff (( compint n) . a) = (n - a))

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      let a be Element of ( Segm n);

      reconsider n as non zero Nat by A1;

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

      

       A2: a < n by NAT_1: 44;

      then (a - a) < (n - a) by XREAL_1: 9;

      then

      reconsider b = (n - a) as Element of NAT by INT_1: 3;

      consider c be Element of NAT such that

       A3: c = (b mod n);

      

       A4: (( compint n) . a) = 0 implies a = 0

      proof

        (a - a) < (n - a) by A2, XREAL_1: 9;

        then

        reconsider a9 = (n - a) as Element of NAT by INT_1: 3;

        assume

         A5: (( compint n) . a) = 0 ;

        n <= (n + a) by NAT_1: 11;

        then

         A6: (n - a) <= ((n + a) - a) by XREAL_1: 9;

        consider t be Nat such that

         A7: a9 = ((n * t) + (a9 mod n)) and (a9 mod n) < n by NAT_D:def 2;

        assume a <> 0 ;

        then (n - a) <> n;

        then

         A8: (n - a) < n by A6, XXREAL_0: 1;

        t = 0

        proof

          assume t <> 0 ;

          then (1 + 0 ) <= t by INT_1: 7;

          then

           A9: (1 * n) <= (t * n) by XREAL_1: 64;

          (t * n) <= ((t * n) + (a9 mod n)) by NAT_1: 11;

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

        end;

        then a9 = 0 by A5, A7, Def11;

        hence thesis by NAT_1: 44;

      end;

      consider t be Nat such that

       A10: b = ((n * t) + c) & c < n or c = 0 & n = 0 by A3, NAT_D:def 2;

      

       A11: (n - a) <= n

      proof

        assume (n - a) > n;

        then ((n - a) + a) > (n + a) by XREAL_1: 6;

        hence thesis by NAT_1: 11;

      end;

       A12:

      now

        assume

         A13: a = 0 ;

        

         A14: t = 1

        proof

          now

            per cases ;

              case t = 0 ;

              hence thesis by A10, A13;

            end;

              case

               A15: t <> 0 ;

              t < 2

              proof

                assume t >= 2;

                then

                 A16: (n * t) >= (n * 2) by XREAL_1: 64;

                

                 A17: n <= ((n * 1) + (n * 1)) by NAT_1: 11;

                ((n * t) + c) >= (n * t) by NAT_1: 11;

                then (n - a) >= (n * 2) by A10, A16, XXREAL_0: 2;

                then (n * 1) = (2 * n) by A13, A17, XXREAL_0: 1;

                hence thesis by A1;

              end;

              then t < (1 + 1);

              then

               A18: t <= 1 by NAT_1: 13;

              (1 + 0 ) <= t by A15, INT_1: 7;

              hence thesis by A18, XXREAL_0: 1;

            end;

          end;

          hence thesis;

        end;

        c = 0

        proof

          assume c <> 0 ;

          then (n + c) > (n + 0 ) by XREAL_1: 6;

          hence thesis by A10, A11, A14;

        end;

        hence (( compint n) . a) = 0 by A3, Def11;

      end;

      now

        assume

         A19: a <> 0 ;

        

         A20: (n - a) < n

        proof

          assume (n - a) >= n;

          then (n - a) = n by A11, XXREAL_0: 1;

          hence thesis by A19;

        end;

        t = 0

        proof

          assume t <> 0 ;

          then (1 + 0 ) <= t by INT_1: 7;

          then

           A21: (1 * n) <= (t * n) by XREAL_1: 64;

          (n * t) <= ((n * t) + c) by NAT_1: 11;

          hence thesis by A10, A20, A21, XXREAL_0: 2;

        end;

        hence (( compint n) . a) = (n - a) by A3, A10, Def11;

      end;

      hence thesis by A12, A4;

    end;

    definition

      let n be natural Number;

      :: INT_3:def12

      func INT.Ring (n) -> doubleLoopStr equals doubleLoopStr (# ( Segm n), ( addint n), ( multint n), ( In (1,( Segm n))), ( In ( 0 ,( Segm n))) #);

      coherence ;

    end

    registration

      let n be non zero Nat;

      cluster ( INT.Ring n) -> strict non empty;

      coherence ;

    end

    theorem :: INT_3:10

    

     Th10: ( INT.Ring 1) is degenerated & ( INT.Ring 1) is Ring & ( INT.Ring 1) is almost_left_invertible unital distributive commutative

    proof

      set n = 1, R = ( INT.Ring n);

      

       A1: for x be Element of R st x <> ( 0. R) holds ex y be Element of R st (y * x) = ( 1. R)

      proof

        let x be Element of R;

        assume x <> ( 0. R);

        then x <> 0 by SUBSET_1:def 8;

        hence thesis by CARD_1: 49, TARSKI:def 1;

      end;

      

       A2: for a,b be Element of R holds (a + b) = (b + a)

      proof

        let a,b be Element of R;

        

        thus (a + b) = 0 by CARD_1: 49, TARSKI:def 1

        .= (b + a) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A3: for a be Element of R holds (a + ( 0. R)) = a

      proof

        let a be Element of R;

        a = 0 by CARD_1: 49, TARSKI:def 1;

        hence thesis by CARD_1: 49, TARSKI:def 1;

      end;

      

       A4: for a,b,c be Element of R holds ((a * b) * c) = (a * (b * c))

      proof

        let a,b,c be Element of R;

        

        thus ((a * b) * c) = 0 by CARD_1: 49, TARSKI:def 1

        .= (a * (b * c)) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A5: for a be Element of R holds (a + ( - a)) = ( 0. R)

      proof

        let a be Element of R;

        

        thus (a + ( - a)) = 0 by CARD_1: 49, TARSKI:def 1

        .= ( 0. R) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A6: R is right_complementable

      proof

        let v be Element of R;

        take ( - v);

        thus thesis by A5;

      end;

      

       A7: for a,b,c be Element of R holds ((a + b) + c) = (a + (b + c))

      proof

        let a,b,c be Element of R;

        

        thus ((a + b) + c) = 0 by CARD_1: 49, TARSKI:def 1

        .= (a + (b + c)) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A8: for a be Element of R holds (( 1. R) * a) = a & (a * ( 1. R)) = a

      proof

        let a be Element of R;

        

         A9: (a * ( 1. R)) = 0 by CARD_1: 49, TARSKI:def 1

        .= a by CARD_1: 49, TARSKI:def 1;

        (( 1. R) * a) = 0 by CARD_1: 49, TARSKI:def 1

        .= a by CARD_1: 49, TARSKI:def 1;

        hence thesis by A9;

      end;

      

       A10: R is well-unital by A8;

      

       A11: for a,b be Element of R holds (a * b) = (b * a)

      proof

        let a,b be Element of R;

        

        thus (a * b) = 0 by CARD_1: 49, TARSKI:def 1

        .= (b * a) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A12: for a,b,c be Element of R holds (a * (b + c)) = ((a * b) + (a * c))

      proof

        let a,b,c be Element of R;

        

        thus (a * (b + c)) = 0 by CARD_1: 49, TARSKI:def 1

        .= ((a * b) + (a * c)) by CARD_1: 49, TARSKI:def 1;

      end;

      

       A13: for a,b,c be Element of R holds ((b + c) * a) = ((b * a) + (c * a))

      proof

        let a,b,c be Element of R;

        

        thus ((b + c) * a) = 0 by CARD_1: 49, TARSKI:def 1

        .= ((b * a) + (c * a)) by CARD_1: 49, TARSKI:def 1;

      end;

      ( 0. R) = 0 by CARD_1: 49, TARSKI:def 1

      .= ( 1. R) by CARD_1: 49, TARSKI:def 1;

      hence thesis by A1, A2, A11, A7, A4, A3, A13, A12, A6, A10, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 7;

    end;

    registration

      cluster strict degenerated unital distributive almost_left_invertible commutative for Ring;

      existence by Th10;

    end

     Lm6:

    now

      let a,n be Nat;

      assume a in ( Segm n);

      then a < n by NAT_1: 44;

      then

       A1: (n - a) is Element of NAT by INT_1: 5;

      assume a > 0 ;

      then (n - a) < (n - 0 ) by XREAL_1: 15;

      hence (n - a) in ( Segm n) by A1, NAT_1: 44;

    end;

    

     Lm7: for n be Nat st 1 < n holds ( 1. ( INT.Ring n)) = 1 by NAT_1: 44, SUBSET_1:def 8;

    theorem :: INT_3:11

    

     Th11: for n be Nat st n > 1 holds ( INT.Ring n) is non degenerated & ( INT.Ring n) is well-unital distributive commutative Ring

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then

      reconsider n as non zero Nat;

      set F = ( INT.Ring n);

      

       A2: ( 1. F) = 1 by A1, Lm7;

      

       A3: for a be Element of F holds (( 1. F) * a) = a & (a * ( 1. F)) = a

      proof

        let a be Element of F;

        reconsider a9 = a as Element of ( Segm n);

        

         A4: (1 * a9) < (( 0 + 1) * n) & 1 is Element of ( Segm n) by A1, NAT_1: 44;

        

        then

         A5: (( multint n) . (a,1)) = (a9 - ( 0 * n)) by Th8

        .= a9;

        (( multint n) . (1,a)) = (a9 - ( 0 * n)) by A4, Th8

        .= a9;

        hence thesis by A1, A5, Lm7;

      end;

      

       A6: F is well-unital by A3;

      

       A7: for a,b be Element of F holds (a + b) = (b + a)

      proof

        let a,b be Element of F;

        reconsider a9 = a as Element of ( Segm n);

        reconsider b9 = b as Element of ( Segm n);

        now

          per cases ;

            case

             A8: (a9 + b9) < n;

            

            hence (( addint n) . (a,b)) = (a9 + b9) by Th7

            .= (( addint n) . (b,a)) by A8, Th7;

          end;

            case

             A9: (a9 + b9) >= n;

            

            hence (( addint n) . (a,b)) = ((a9 + b9) - n) by Th7

            .= (( addint n) . (b,a)) by A9, Th7;

          end;

        end;

        hence thesis;

      end;

      

       A10: for a,b,c be Element of F holds ((a * b) * c) = (a * (b * c))

      proof

        let a,b,c be Element of F;

        reconsider a9 = a, b9 = b, c9 = c as Element of ( Segm n);

        reconsider aa = a9 as Element of NAT ;

        reconsider aa as Integer;

        reconsider bb = b9 as Element of NAT ;

        reconsider bb as Integer;

        reconsider cc = c9 as Element of NAT ;

        reconsider cc as Integer;

        

         A11: cc < n by NAT_1: 44;

        aa < n by NAT_1: 44;

        

        then

         A12: ((a9 * ((b9 * c9) mod n)) mod n) = (((aa mod n) * ((bb * cc) mod n)) mod n) by NAT_D: 63

        .= ((aa * (bb * cc)) mod n) by NAT_D: 67

        .= (((aa * bb) * cc) mod n)

        .= ((((aa * bb) mod n) * (cc mod n)) mod n) by NAT_D: 67

        .= ((((a9 * b9) mod n) * c9) mod n) by A11, NAT_D: 63;

        ((aa * bb) mod n) < n by NAT_D: 62;

        then

         A13: ((a9 * b9) mod n) is Element of ( Segm n) by NAT_1: 44;

        ((bb * cc) mod n) < n by NAT_D: 62;

        then

         A14: ((b9 * c9) mod n) is Element of ( Segm n) by NAT_1: 44;

        

         A15: (a * (b * c)) = (( multint n) . (a9,((b9 * c9) mod n))) by Def10

        .= ((a9 * ((b9 * c9) mod n)) mod n) by A14, Def10;

        ((a * b) * c) = (( multint n) . (((a9 * b9) mod n),c9)) by Def10

        .= ((((a9 * b9) mod n) * c9) mod n) by A13, Def10;

        hence thesis by A15, A12;

      end;

      

       A16: for a,b be Element of F holds (a * b) = (b * a)

      proof

        let a,b be Element of F;

        reconsider a9 = a as Element of ( Segm n);

        reconsider b9 = b as Element of ( Segm n);

        consider k be Element of NAT such that

         A17: (k * n) <= (a9 * b9) & (a9 * b9) < ((k + 1) * n) by Lm5;

        (( multint n) . (a9,b9)) = ((a9 * b9) - (k * n)) by A17, Th8

        .= (( multint n) . (b9,a9)) by A17, Th8;

        hence thesis;

      end;

      

       A18: for a,b,c be Element of F holds ((a + b) + c) = (a + (b + c))

      proof

        let a,b,c be Element of F;

        reconsider a9 = a, b9 = b, c9 = c as Element of ( Segm n);

        reconsider aa = a9 as Element of NAT ;

        reconsider aa as Integer;

        reconsider bb = b9 as Element of NAT ;

        reconsider bb as Integer;

        reconsider cc = c9 as Element of NAT ;

        reconsider cc as Integer;

        

         A19: cc < n by NAT_1: 44;

        aa < n by NAT_1: 44;

        

        then

         A20: ((a9 + ((b9 + c9) mod n)) mod n) = (((aa mod n) + ((bb + cc) mod n)) mod n) by NAT_D: 63

        .= ((aa + (bb + cc)) mod n) by NAT_D: 66

        .= (((aa + bb) + cc) mod n)

        .= ((((aa + bb) mod n) + (cc mod n)) mod n) by NAT_D: 66

        .= ((((a9 + b9) mod n) + c9) mod n) by A19, NAT_D: 63;

        ((aa + bb) mod n) < n by NAT_D: 62;

        then

         A21: ((a9 + b9) mod n) is Element of ( Segm n) by NAT_1: 44;

        ((bb + cc) mod n) < n by NAT_D: 62;

        then

         A22: ((b9 + c9) mod n) is Element of ( Segm n) by NAT_1: 44;

        

         A23: (a + (b + c)) = (( addint n) . (a9,((b9 + c9) mod n))) by GR_CY_1:def 4

        .= ((a9 + ((b9 + c9) mod n)) mod n) by A22, GR_CY_1:def 4;

        ((a + b) + c) = (( addint n) . (((a9 + b9) mod n),c9)) by GR_CY_1:def 4

        .= ((((a9 + b9) mod n) + c9) mod n) by A21, GR_CY_1:def 4;

        hence thesis by A23, A20;

      end;

       0 in ( Segm n) by NAT_1: 44;

      then

       A24: ( 0. F) = 0 by SUBSET_1:def 8;

      

       A25: for a be Element of F holds (a + ( 0. F)) = a

      proof

        let a be Element of F;

        reconsider a9 = a as Element of ( Segm n);

        (a9 + 0 ) < n by NAT_1: 44;

        hence thesis by A24, Th7;

      end;

      

       A26: F is right_complementable

      proof

        let a be Element of F;

        reconsider a9 = a as Element of ( Segm n);

        reconsider a9 as Element of NAT ;

        per cases ;

          suppose

           A27: a9 = 0 ;

          take ( 0. F);

          thus thesis by A24, A25, A27;

        end;

          suppose a9 <> 0 ;

          then

          reconsider b = (n - a9) as Element of ( Segm n) by Lm6;

          reconsider v = b as Element of F;

          take v;

          

          thus (a + v) = ((a9 + b) mod n) by GR_CY_1:def 4

          .= ( 0. F) by A24, NAT_D: 25;

        end;

      end;

      

       A28: for a,b,c be Element of F holds ((b + c) * a) = ((b * a) + (c * a))

      proof

        let a,b,c be Element of F;

        reconsider a9 = a, b9 = b, c9 = c as Element of ( Segm n);

        reconsider aa = a9 as Element of NAT ;

        reconsider aa as Integer;

        reconsider bb = b9 as Element of NAT ;

        reconsider bb as Integer;

        reconsider cc = c9 as Element of NAT ;

        reconsider cc as Integer;

        

         A29: aa < n by NAT_1: 44;

        

         A30: ((((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n) = (((bb * aa) + (cc * aa)) mod n) by NAT_D: 66

        .= (((bb + cc) * aa) mod n)

        .= ((((bb + cc) mod n) * (aa mod n)) mod n) by NAT_D: 67

        .= ((((b9 + c9) mod n) * a9) mod n) by A29, NAT_D: 63;

        ((bb + cc) mod n) < n by NAT_D: 62;

        then

         A31: ((b9 + c9) mod n) is Element of ( Segm n) by NAT_1: 44;

        ((cc * aa) mod n) < n by NAT_D: 62;

        then

         A32: ((c9 * a9) mod n) is Element of ( Segm n) by NAT_1: 44;

        ((bb * aa) mod n) < n by NAT_D: 62;

        then

         A33: ((b9 * a9) mod n) is Element of ( Segm n) by NAT_1: 44;

        

         A34: ((b + c) * a) = (( multint n) . (((b9 + c9) mod n),a9)) by GR_CY_1:def 4

        .= ((((b9 + c9) mod n) * a9) mod n) by A31, Def10;

        ((b * a) + (c * a)) = (( addint n) . ((( multint n) . (b,a)),((c9 * a9) mod n))) by Def10

        .= (( addint n) . (((b9 * a9) mod n),((c9 * a9) mod n))) by Def10

        .= ((((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n) by A33, A32, GR_CY_1:def 4;

        hence thesis by A34, A30;

      end;

      for a,b,c be Element of F holds (a * (b + c)) = ((a * b) + (a * c))

      proof

        let a,b,c be Element of F;

        

        thus (a * (b + c)) = ((b + c) * a) by A16

        .= ((b * a) + (c * a)) by A28

        .= ((a * b) + (c * a)) by A16

        .= ((a * b) + (a * c)) by A16;

      end;

      then

      reconsider F as commutative Ring by A7, A16, A18, A10, A25, A28, A26, A6, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 7;

      F is non degenerated by A24, A2;

      hence thesis;

    end;

    theorem :: INT_3:12

    

     Th12: for p be Nat st p > 1 holds ( INT.Ring p) is add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr iff p is Prime

    proof

      let p be Nat;

      assume

       A1: p > 1;

      then

      reconsider p as non zero Nat;

      reconsider P = ( INT.Ring p) as Ring by A1, Th11;

      reconsider p as non zero Element of NAT by ORDINAL1:def 12;

       A2:

      now

        assume

         A3: ( INT.Ring p) is add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

        for n be Nat holds n divides p implies n = 1 or n = p

        proof

          let n be Nat;

          assume n divides p;

          then

          consider k be Nat such that

           A4: p = (n * k) by NAT_D:def 3;

          

           A5: n <= p

          proof

            assume

             A6: n > p;

            now

              per cases ;

                case k = 0 ;

                hence thesis by A4;

              end;

                case

                 A7: k <> 0 ;

                then k >= (1 + 0 ) by INT_1: 7;

                then (k * p) >= (1 * p) by XREAL_1: 64;

                hence thesis by A4, A6, A7, XREAL_1: 68;

              end;

            end;

            hence thesis;

          end;

          

           A8: k <= p

          proof

            assume

             A9: k > p;

            now

              per cases ;

                case n = 0 ;

                hence thesis by A4;

              end;

                case

                 A10: n <> 0 ;

                then n >= (1 + 0 ) by INT_1: 7;

                then (n * p) >= (1 * p) by XREAL_1: 64;

                hence thesis by A4, A9, A10, XREAL_1: 68;

              end;

            end;

            hence thesis;

          end;

          now

            per cases ;

              case k = p;

              then (1 * p) = (p * n) by A4;

              hence thesis by XCMPLX_1: 5;

            end;

              case k <> p;

              then

               A11: k < p by A8, XXREAL_0: 1;

              now

                per cases ;

                  case n = p;

                  then (1 * p) = (k * p) by A4;

                  then k = 1 by XCMPLX_1: 5;

                  hence thesis by A4;

                end;

                  case n <> p;

                  then n < p by A5, XXREAL_0: 1;

                  then

                  reconsider n2 = n as Element of ( Segm p) by NAT_1: 44;

                   0 in ( Segm p) by NAT_1: 44;

                  then

                   A12: 0 = ( 0. ( INT.Ring p)) by SUBSET_1:def 8;

                  k <> 0 by A4;

                  then

                   A13: k <> ( 0. ( INT.Ring p)) by A12;

                  reconsider k2 = k as Element of ( Segm p) by A11, NAT_1: 44;

                  reconsider n9 = n2 as Element of ( INT.Ring p);

                  reconsider k9 = k2 as Element of ( INT.Ring p);

                  n <> 0 by A4;

                  then

                   A14: n <> ( 0. ( INT.Ring p)) by A12;

                  (n9 * k9) = ((n2 * k2) mod p) by Def10

                  .= ( 0. ( INT.Ring p)) by A12, A4, INT_1: 62;

                  hence contradiction by A3, A14, A13, VECTSP_1: 12;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence p is Prime by A1, INT_2:def 4;

      end;

      now

        assume

         A15: p is Prime;

        for a be Element of P st a <> ( 0. P) holds ex b be Element of P st (b * a) = ( 1. P)

        proof

          reconsider e = 1 as Integer;

          let a be Element of P;

          reconsider a9 = a as Element of ( Segm p);

          reconsider a9 as Element of NAT ;

          reconsider a2 = a9 as Integer;

          (1 * p) = p;

          then

           A16: 1 divides p by NAT_D:def 3;

          assume

           A17: a <> ( 0. P);

          

           A18: for m be Nat st m divides a9 & m divides p holds m divides 1

          proof

            let m be Nat;

            assume that

             A19: m divides a9 and

             A20: m divides p;

            consider k be Nat such that

             A21: a9 = (m * k) by A19, NAT_D:def 3;

            m <= a9

            proof

              assume

               A22: m > a9;

              now

                per cases ;

                  case k = 0 ;

                  hence thesis by A17, A21, SUBSET_1:def 8;

                end;

                  case

                   A23: k <> 0 ;

                  then k >= (1 + 0 ) by INT_1: 7;

                  then (k * a9) >= (1 * a9) by XREAL_1: 64;

                  hence thesis by A21, A22, A23, XREAL_1: 68;

                end;

              end;

              hence thesis;

            end;

            then m <> p by NAT_1: 44;

            hence thesis by A15, A20, INT_2:def 4;

          end;

          (1 * a9) = a9;

          then 1 divides a9 by NAT_D:def 3;

          then (a9 gcd p) = 1 by A16, A18, NAT_D:def 5;

          then

          consider s,t be Integer such that

           A24: 1 = ((s * a9) + (t * p)) by NAT_D: 68;

          (s mod p) >= 0 by NAT_D: 62;

          then

           A25: (s mod p) is Element of NAT by INT_1: 3;

          (s mod p) < p by NAT_D: 62;

          then

          reconsider b9 = (s mod p) as Element of ( Segm p) by A25, NAT_1: 44;

          reconsider b = b9 as Element of P;

          (b * a) = ((a9 * b9) mod p) by Def10

          .= (((a2 mod p) * ((s mod p) mod p)) mod p) by NAT_D: 67

          .= (((a2 mod p) * (s mod p)) mod p) by NAT_D: 65

          .= ((a2 * s) mod p) by NAT_D: 67

          .= (e mod p) by A24, NAT_D: 61

          .= e by A1, NAT_D: 63

          .= ( 1. P) by A1, Lm7;

          hence thesis;

        end;

        hence ( INT.Ring p) is add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr by A1, Th11, VECTSP_1:def 9;

      end;

      hence thesis by A2;

    end;

    registration

      cluster -> non zero for Prime;

      coherence

      proof

        let k be Prime;

        assume k is zero;

        then k in ( SetPrimenumber 2) by NEWTON:def 7;

        hence contradiction;

      end;

    end

    registration

      let p be Prime;

      cluster ( INT.Ring p) -> add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated;

      coherence

      proof

        p > 1 by INT_2:def 4;

        hence thesis by Th12;

      end;

    end

    theorem :: INT_3:13

    ( 1. INT.Ring ) = 1;

    theorem :: INT_3:14

    for n be Nat st 1 < n holds ( 1. ( INT.Ring n)) = 1 by Lm7;

    begin

    registration

      cluster INT.Ring -> infinite;

      coherence ;

    end

    registration

      cluster strict infinite for Ring;

      existence

      proof

        take INT.Ring ;

        thus thesis;

      end;

    end