gcd_1.miz



    begin

    reserve X,Y for set;

    registration

      cluster commutative right_unital -> left_unital for non empty multLoopStr;

      coherence

      proof

        let R be non empty multLoopStr such that

         A1: R is commutative and

         A2: R is right_unital;

        let x be Element of R;

        

        thus (( 1. R) * x) = (x * ( 1. R)) by A1, GROUP_1:def 12

        .= x by A2;

      end;

    end

    registration

      cluster commutative right-distributive -> distributive for non empty doubleLoopStr;

      coherence

      proof

        let R be non empty doubleLoopStr such that

         A1: R is commutative and

         A2: R is right-distributive;

        let x,y,z be Element of R;

        thus (x * (y + z)) = ((x * y) + (x * z)) by A2;

        

        thus ((y + z) * x) = (x * (y + z)) by A1, GROUP_1:def 12

        .= ((x * y) + (x * z)) by A2

        .= ((y * x) + (x * z)) by A1, GROUP_1:def 12

        .= ((y * x) + (z * x)) by A1, GROUP_1:def 12;

      end;

      cluster commutative left-distributive -> distributive for non empty doubleLoopStr;

      coherence

      proof

        let R be non empty doubleLoopStr such that

         A3: R is commutative and

         A4: R is left-distributive;

        let x,y,z be Element of R;

        

        thus (x * (y + z)) = ((y + z) * x) by A3, GROUP_1:def 12

        .= ((y * x) + (z * x)) by A4

        .= ((x * y) + (z * x)) by A3, GROUP_1:def 12

        .= ((x * y) + (x * z)) by A3, GROUP_1:def 12;

        thus thesis by A4;

      end;

    end

    registration

      cluster -> well-unital for Ring;

      coherence ;

    end

    registration

      cluster F_Real -> domRing-like;

      coherence

      proof

        set D = F_Real ;

        hereby

          let x,y be Element of F_Real ;

          

           A1: ( 0. D) = ( In ( 0 , REAL )) by STRUCT_0:def 6;

          assume (x * y) = ( 0. D) & x <> ( 0. D);

          hence y = ( 0. D) by A1, XCMPLX_1: 6;

        end;

      end;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable associative commutative domRing-like distributive well-unital non degenerated almost_left_invertible for non empty doubleLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    reserve R for domRing-like commutative Ring;

    reserve c for Element of R;

    theorem :: GCD_1:1

    

     Th1: for R be domRing-like commutative Ring holds for a,b,c be Element of R holds a <> ( 0. R) implies ((a * b) = (a * c) implies b = c) & ((b * a) = (c * a) implies b = c)

    proof

      let R be domRing-like commutative Ring;

      let a,b,c be Element of R;

      assume

       A1: a <> ( 0. R);

      now

        assume (a * b) = (a * c);

        

        then ( 0. R) = ((a * b) + ( - (a * c))) by RLVECT_1:def 10

        .= ((a * b) + (a * ( - c))) by VECTSP_1: 8

        .= (a * (b + ( - c))) by VECTSP_1:def 2

        .= (a * (b - c)) by RLVECT_1:def 11;

        then (b - c) = ( 0. R) by A1, VECTSP_2:def 1;

        

        then c = ((b - c) + c) by RLVECT_1: 4

        .= ((b + ( - c)) + c) by RLVECT_1:def 11

        .= (b + (c + ( - c))) by RLVECT_1:def 3

        .= (b + ( 0. R)) by RLVECT_1:def 10

        .= b by RLVECT_1: 4;

        hence b = c;

      end;

      hence thesis;

    end;

    definition

      let R be non empty multMagma;

      let x,y be Element of R;

      :: GCD_1:def1

      pred x divides y means ex z be Element of R st y = (x * z);

    end

    definition

      let R be right_unital non empty multLoopStr;

      let x,y be Element of R;

      :: original: divides

      redefine

      pred x divides y;

      reflexivity

      proof

        let A be Element of R;

        (A * ( 1. R)) = A;

        hence thesis;

      end;

    end

    definition

      let R be non empty multLoopStr;

      let x be Element of R;

      :: GCD_1:def2

      attr x is unital means x divides ( 1. R);

    end

    definition

      let R be non empty multLoopStr;

      let x,y be Element of R;

      :: GCD_1:def3

      pred x is_associated_to y means x divides y & y divides x;

      symmetry ;

    end

    notation

      let R be non empty multLoopStr;

      let x,y be Element of R;

      antonym x is_not_associated_to y for x is_associated_to y;

    end

    definition

      let R be well-unital non empty multLoopStr;

      let x,y be Element of R;

      :: original: is_associated_to

      redefine

      pred x is_associated_to y;

      reflexivity

      proof

        let a be Element of R;

        thus a divides a & a divides a;

      end;

    end

    definition

      let R be domRing-like commutative Ring;

      let x,y be Element of R;

      assume

       A1: y divides x;

      assume

       A2: y <> ( 0. R);

      :: GCD_1:def4

      func x / y -> Element of R means

      : Def4: (it * y) = x;

      existence

      proof

        ex z be Element of R st x = (y * z) by A1;

        hence thesis;

      end;

      uniqueness by A2, Th1;

    end

    theorem :: GCD_1:2

    

     Th2: for R be associative non empty multLoopStr holds for a,b,c be Element of R holds a divides b & b divides c implies a divides c

    proof

      let R be associative non empty multLoopStr;

      let A,B,C be Element of R;

      now

        assume that

         A1: A divides B and

         A2: B divides C;

        consider D be Element of R such that

         A3: (A * D) = B by A1;

        consider E be Element of R such that

         A4: (B * E) = C by A2;

        (A * (D * E)) = C by A3, A4, GROUP_1:def 3;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:3

    

     Th3: for R be commutative associative non empty multLoopStr holds for a,b,c,d be Element of R holds (b divides a & d divides c) implies (b * d) divides (a * c)

    proof

      let R be commutative associative non empty multLoopStr;

      let a,b,c,d be Element of R;

      assume that

       A1: b divides a and

       A2: d divides c;

      consider x be Element of R such that

       A3: (b * x) = a by A1;

      consider y be Element of R such that

       A4: (d * y) = c by A2;

      ((b * d) * (y * x)) = (((b * d) * y) * x) by GROUP_1:def 3

      .= ((b * c) * x) by A4, GROUP_1:def 3

      .= (a * c) by A3, GROUP_1:def 3;

      hence thesis;

    end;

    theorem :: GCD_1:4

    

     Th4: for R be associative non empty multLoopStr holds for a,b,c be Element of R holds a is_associated_to b & b is_associated_to c implies a is_associated_to c by Th2;

    theorem :: GCD_1:5

    

     Th5: for R be associative non empty multLoopStr holds for a,b,c be Element of R holds a divides b implies (c * a) divides (c * b)

    proof

      let R be associative non empty multLoopStr;

      let A,B,C be Element of R;

      assume A divides B;

      then

      consider D be Element of R such that

       A1: (A * D) = B;

      ((C * A) * D) = (C * B) by A1, GROUP_1:def 3;

      hence thesis;

    end;

    theorem :: GCD_1:6

    for R be non empty multLoopStr holds for a,b be Element of R holds a divides (a * b) & (R is commutative implies b divides (a * b))

    proof

      let R be non empty multLoopStr;

      let a,b be Element of R;

      thus a divides (a * b);

      assume

       A1: R is commutative;

      take a;

      thus thesis by A1, GROUP_1:def 12;

    end;

    theorem :: GCD_1:7

    

     Th7: for R be associative non empty multLoopStr holds for a,b,c be Element of R holds a divides b implies a divides (b * c)

    proof

      let R be associative non empty multLoopStr;

      let a,b,c be Element of R;

      assume a divides b;

      then

      consider d be Element of R such that

       A1: (a * d) = b;

      (a * (d * c)) = (b * c) by A1, GROUP_1:def 3;

      hence thesis;

    end;

    theorem :: GCD_1:8

    

     Th8: for a,b be Element of R holds b divides a & b <> ( 0. R) implies ((a / b) = ( 0. R) iff a = ( 0. R))

    proof

      let a,b be Element of R;

      assume that

       A1: b divides a and

       A2: b <> ( 0. R);

      hereby

        assume (a / b) = ( 0. R);

        

        then a = (( 0. R) * b) by A1, A2, Def4

        .= ( 0. R);

        hence a = ( 0. R);

      end;

      assume a = ( 0. R);

      then ( 0. R) = ((a / b) * b) by A1, A2, Def4;

      hence thesis by A2, VECTSP_2:def 1;

    end;

    theorem :: GCD_1:9

    

     Th9: for a be Element of R holds a <> ( 0. R) implies (a / a) = ( 1. R)

    proof

      let A be Element of R;

      assume

       A1: A <> ( 0. R);

      

      then ((A / A) * A) = A by Def4

      .= (( 1. R) * A);

      hence thesis by A1, Th1;

    end;

    theorem :: GCD_1:10

    

     Th10: for R be non degenerated domRing-like commutative Ring holds for a be Element of R holds (a / ( 1. R)) = a

    proof

      let R be non degenerated domRing-like commutative Ring;

      let a be Element of R;

      set A = (a / ( 1. R));

      (( 1. R) * a) = a;

      then

       A1: ( 1. R) <> ( 0. R) & ( 1. R) divides a;

      A = (A * ( 1. R))

      .= a by A1, Def4;

      hence thesis;

    end;

    theorem :: GCD_1:11

    

     Th11: for a,b,c be Element of R holds c <> ( 0. R) implies (c divides (a * b) & c divides a implies ((a * b) / c) = ((a / c) * b)) & (c divides (a * b) & c divides b implies ((a * b) / c) = (a * (b / c)))

    proof

      let A,B,C be Element of R;

      assume

       A1: C <> ( 0. R);

       A2:

      now

        set A2 = (B / C);

        set A1 = ((A * B) / C);

        assume C divides (A * B) & C divides B;

        then (A1 * C) = (A * B) & (A2 * C) = B by A1, Def4;

        then (A1 * C) = ((A * A2) * C) by GROUP_1:def 3;

        hence C divides (A * B) & C divides B implies ((A * B) / C) = (A * (B / C)) by A1, Th1;

      end;

      now

        set A2 = (A / C);

        set A1 = ((A * B) / C);

        assume C divides (A * B) & C divides A;

        then (A1 * C) = (A * B) & (A2 * C) = A by A1, Def4;

        then (A1 * C) = ((A2 * B) * C) by GROUP_1:def 3;

        hence C divides (A * B) & C divides A implies ((A * B) / C) = ((A / C) * B) by A1, Th1;

      end;

      hence thesis by A2;

    end;

    theorem :: GCD_1:12

    

     Th12: for a,b,c be Element of R holds c <> ( 0. R) & c divides a & c divides b & c divides (a + b) implies ((a / c) + (b / c)) = ((a + b) / c)

    proof

      let a,b,c be Element of R;

      assume

       A1: c <> ( 0. R);

      set e = (b / c);

      set d = (a / c);

      assume that

       A2: c divides a & c divides b and

       A3: c divides (a + b);

      (d * c) = a & (e * c) = b by A1, A2, Def4;

      then (a + b) = ((d + e) * c) by VECTSP_1:def 3;

      

      then ((a + b) / c) = ((d + e) * (c / c)) by A1, A3, Th11

      .= ((d + e) * ( 1. R)) by A1, Th9

      .= (d + e);

      hence thesis;

    end;

    theorem :: GCD_1:13

    for a,b,c be Element of R holds c <> ( 0. R) & c divides a & c divides b implies ((a / c) = (b / c) iff a = b)

    proof

      let a,b,c be Element of R;

      assume

       A1: c <> ( 0. R);

      assume that

       A2: c divides a and

       A3: c divides b;

      now

        assume (a / c) = (b / c);

        consider e be Element of R such that

         A4: e = (b / c);

        (e * c) = b by A1, A3, A4, Def4;

        hence (a / c) = (b / c) implies a = b by A1, A2, A4, Def4;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:14

    

     Th14: for a,b,c,d be Element of R holds b <> ( 0. R) & d <> ( 0. R) & b divides a & d divides c implies ((a / b) * (c / d)) = ((a * c) / (b * d))

    proof

      let a,b,c,d be Element of R;

      assume that

       A1: b <> ( 0. R) & d <> ( 0. R) and

       A2: b divides a & d divides c;

      

       A3: (b * d) divides (a * c) by A2, Th3;

      set z = ((a * c) / (b * d));

      set y = (c / d);

      set x = (a / b);

      

       A4: (b * d) <> ( 0. R) by A1, VECTSP_2:def 1;

      (x * b) = a & (y * d) = c by A1, A2, Def4;

      

      then (z * (b * d)) = ((x * b) * (y * d)) by A3, A4, Def4

      .= (x * (b * (y * d))) by GROUP_1:def 3

      .= (x * (y * (b * d))) by GROUP_1:def 3

      .= ((x * y) * (b * d)) by GROUP_1:def 3;

      hence thesis by A4, Th1;

    end;

    theorem :: GCD_1:15

    

     Th15: for a,b,c be Element of R holds a <> ( 0. R) & (a * b) divides (a * c) implies b divides c

    proof

      let A,B,C be Element of R;

      assume that

       A1: A <> ( 0. R) and

       A2: (A * B) divides (A * C);

      consider D be Element of R such that

       A3: ((A * B) * D) = (A * C) by A2;

      A divides (A * C);

      then

       A4: ((A * C) / A) = ((A / A) * C) by A1, Th11;

      A divides (A * (B * D));

      then

       A5: ((A * (B * D)) / A) = ((A / A) * (B * D)) by A1, Th11;

      

       A6: (A * (B * D)) = (A * C) by A3, GROUP_1:def 3;

      (B * D) = (( 1. R) * (B * D))

      .= ((A / A) * C) by A1, A6, A5, A4, Th9

      .= (( 1. R) * C) by A1, Th9

      .= C;

      hence thesis;

    end;

    theorem :: GCD_1:16

    for a be Element of R holds a is_associated_to ( 0. R) implies a = ( 0. R)

    proof

      let A be Element of R;

      assume A is_associated_to ( 0. R);

      then ( 0. R) divides A;

      then ex D be Element of R st (( 0. R) * D) = A;

      hence thesis;

    end;

    theorem :: GCD_1:17

    

     Th17: for a,b be Element of R holds a <> ( 0. R) & (a * b) = a implies b = ( 1. R)

    proof

      let A,B be Element of R;

      assume that

       A1: A <> ( 0. R) and

       A2: (A * B) = A;

      set A1 = (A / A);

      A1 = ( 1. R) & ((A * B) / A) = ((A / A) * B) by A1, A2, Th9, Th11;

      hence thesis by A2;

    end;

    theorem :: GCD_1:18

    

     Th18: for a,b be Element of R holds a is_associated_to b iff ex c st c is unital & (a * c) = b

    proof

      

       A1: for a,b be Element of R holds a is_associated_to b implies ex c be Element of R st c is unital & (a * c) = b

      proof

        let A,B be Element of R;

        assume

         A2: A is_associated_to B;

        then A divides B;

        then

        consider C be Element of R such that

         A3: B = (A * C);

        B divides A by A2;

        then

        consider D be Element of R such that

         A4: A = (B * D);

        now

          per cases ;

            case

             A5: A <> ( 0. R);

            A = (A * (C * D)) by A3, A4, GROUP_1:def 3;

            then (C * D) = ( 1. R) by A5, Th17;

            then C divides ( 1. R);

            then C is unital;

            hence thesis by A3;

          end;

            case

             A6: A = ( 0. R);

            ( 1. R) divides ( 1. R);

            then

             A7: ( 1. R) is unital;

            B = ( 0. R) by A3, A6;

            then B = (A * ( 1. R)) by A6;

            hence thesis by A7;

          end;

        end;

        hence thesis;

      end;

      for a,b be Element of R holds (ex c be Element of R st (c is unital & (a * c) = b)) implies a is_associated_to b

      proof

        let A,B be Element of R;

        (ex c st (c is unital & (A * c) = B)) implies A is_associated_to B

        proof

          now

            assume ex c st c is unital & (A * c) = B;

            then

            consider C be Element of R such that

             A8: C is unital and

             A9: (A * C) = B;

            C divides ( 1. R) by A8;

            then

            consider D be Element of R such that

             A10: (C * D) = ( 1. R);

            A = (A * (C * D)) by A10

            .= (B * D) by A9, GROUP_1:def 3;

            then

             A11: B divides A;

            A divides B by A9;

            hence thesis by A11;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: GCD_1:19

    

     Th19: for a,b,c be Element of R holds c <> ( 0. R) & (c * a) is_associated_to (c * b) implies a is_associated_to b by Th15;

    begin

    definition

      let R be non empty multLoopStr;

      let a be Element of R;

      :: GCD_1:def5

      func Class a -> Subset of R means

      : Def5: for b be Element of R holds b in it iff b is_associated_to a;

      existence

      proof

        set M = { b where b be Element of R : b is_associated_to a };

        now

          let B be object;

          now

            assume B in M;

            then ex B9 be Element of R st B = B9 & B9 is_associated_to a;

            hence B in M implies B in the carrier of R;

          end;

          hence B in M implies B in the carrier of R;

        end;

        then

         A1: M c= the carrier of R by TARSKI:def 3;

        now

          let A be Element of R;

          A in M implies A is_associated_to a

          proof

            assume A in M;

            then ex A9 be Element of R st A = A9 & A9 is_associated_to a;

            hence thesis;

          end;

          hence A in M iff A is_associated_to a;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ Element of R] means $1 is_associated_to a;

        let X1,X2 be Subset of R such that

         A2: for y be Element of R holds y in X1 iff P[y] and

         A3: for y be Element of R holds y in X2 iff P[y];

        thus X1 = X2 from SUBSET_1:sch 2( A2, A3);

      end;

    end

    registration

      let R be well-unital non empty multLoopStr;

      let a be Element of R;

      cluster ( Class a) -> non empty;

      coherence

      proof

        a is_associated_to a;

        hence thesis by Def5;

      end;

    end

    theorem :: GCD_1:20

    

     Th20: for R be associative non empty multLoopStr holds for a,b be Element of R holds ( Class a) meets ( Class b) implies ( Class a) = ( Class b)

    proof

      let R be associative non empty multLoopStr;

      let a,b be Element of R;

      assume (( Class a) /\ ( Class b)) <> {} ;

      then ( Class a) meets ( Class b);

      then

      consider Z be object such that

       A1: Z in ( Class a) and

       A2: Z in ( Class b) by XBOOLE_0: 3;

      reconsider Z as Element of R by A1;

      

       A3: Z is_associated_to b by A2, Def5;

      

       A4: Z is_associated_to a by A1, Def5;

      

       A5: for c be Element of R holds c in ( Class b) implies c in ( Class a)

      proof

        let c be Element of R;

        assume c in ( Class b);

        then c is_associated_to b by Def5;

        then Z is_associated_to c by A3, Th4;

        then a is_associated_to c by A4, Th4;

        hence thesis by Def5;

      end;

      for c be Element of R holds c in ( Class a) implies c in ( Class b)

      proof

        let c be Element of R;

        assume c in ( Class a);

        then c is_associated_to a by Def5;

        then Z is_associated_to c by A4, Th4;

        then b is_associated_to c by A3, Th4;

        hence thesis by Def5;

      end;

      hence thesis by A5, SUBSET_1: 3;

    end;

    definition

      let R be non empty multLoopStr;

      :: GCD_1:def6

      func Classes R -> Subset-Family of R means

      : Def6: for A be Subset of R holds A in it iff ex a be Element of R st A = ( Class a);

      existence

      proof

        defpred P[ set] means ex a be Element of R st $1 = ( Class a);

        ex F be Subset-Family of R st for A be Subset of R holds A in F iff P[A] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ set] means ex a be Element of R st $1 = ( Class a);

        let F1,F2 be Subset-Family of R;

        assume

         A1: for A be Subset of R holds A in F1 iff P[A];

        assume

         A2: for A be Subset of R holds A in F2 iff P[A];

        thus thesis from SUBSET_1:sch 4( A1, A2);

      end;

    end

    registration

      let R be non empty multLoopStr;

      cluster ( Classes R) -> non empty;

      coherence

      proof

        ( Class ( 1. R)) in ( Classes R) by Def6;

        hence thesis;

      end;

    end

    theorem :: GCD_1:21

    

     Th21: for R be well-unital non empty multLoopStr holds for X be Subset of R holds X in ( Classes R) implies X is non empty

    proof

      let R be well-unital non empty multLoopStr;

      let X be Subset of R;

      assume X in ( Classes R);

      then ex a be Element of R st X = ( Class a) by Def6;

      hence thesis;

    end;

    definition

      let R be associative well-unital non empty multLoopStr;

      :: GCD_1:def7

      mode Am of R -> non empty Subset of R means

      : Def7: (for a be Element of R holds ex z be Element of it st z is_associated_to a) & for x,y be Element of it holds x <> y implies x is_not_associated_to y;

      existence

      proof

        now

          let R be associative well-unital non empty multLoopStr;

          reconsider M = ( Classes R) as non empty set;

          

           A1: for X st X in M holds X <> {}

          proof

            let X be set;

            assume X in M;

            then ex A be Element of R st X = ( Class A) by Def6;

            hence thesis;

          end;

          for X, Y st X in M & Y in M & X <> Y holds X misses Y

          proof

            let X,Y be set such that

             A2: X in M & Y in M and

             A3: X <> Y;

            assume

             A4: X meets Y;

            (ex A be Element of R st X = ( Class A)) & ex B be Element of R st Y = ( Class B) by A2, Def6;

            hence contradiction by A3, A4, Th20;

          end;

          then

          consider AmpS9 be set such that

           A5: for X st X in M holds ex x be object st (AmpS9 /\ X) = {x} by A1, WELLORD2: 18;

          AmpS9 is non empty

          proof

            ( Class ( 1. R)) in M by Def6;

            then ex x be object st (AmpS9 /\ ( Class ( 1. R))) = {x} by A5;

            hence thesis;

          end;

          then

          reconsider AmpS9 as non empty set;

          set AmpS = { x where x be Element of AmpS9 : ex X be non empty Subset of R st X in M & (AmpS9 /\ X) = {x} };

          

           A6: AmpS is non empty Subset of R

          proof

            AmpS is non empty

            proof

              

               A7: ( Class ( 1. R)) in M by Def6;

              then

              consider x be object such that

               A8: (AmpS9 /\ ( Class ( 1. R))) = {x} by A5;

              x in {x} by TARSKI:def 1;

              then x in AmpS9 by A8, XBOOLE_0:def 4;

              then x in AmpS by A7, A8;

              hence thesis;

            end;

            then

            reconsider AmpS as non empty set;

            now

              let A be object;

              now

                assume A in AmpS;

                then

                consider x be Element of AmpS9 such that

                 A9: A = x & ex X be non empty Subset of R st X in M & (AmpS9 /\ X) = {x};

                x in {x} by TARSKI:def 1;

                hence A in AmpS implies A in the carrier of R by A9;

              end;

              hence A in AmpS implies A in the carrier of R;

            end;

            hence thesis by TARSKI:def 3;

          end;

          

           A10: for X be Element of M holds ex z be Element of AmpS st (AmpS /\ X) = {z}

          proof

            let X be Element of M;

            consider x be object such that

             A11: (AmpS9 /\ X) = {x} by A5;

            X in ( Classes R);

            then

             A12: X is non empty Subset of R by Th21;

            

             A13: x in {x} by TARSKI:def 1;

            then x in AmpS9 by A11, XBOOLE_0:def 4;

            then

             A14: x in AmpS by A11, A12;

            

             A15: x in X by A11, A13, XBOOLE_0:def 4;

            now

              let y be object;

               A16:

              now

                assume

                 A17: y in (AmpS /\ X);

                then y in AmpS by XBOOLE_0:def 4;

                then

                 A18: ex zz be Element of AmpS9 st y = zz & ex X be non empty Subset of R st X in M & (AmpS9 /\ X) = {zz};

                y in X by A17, XBOOLE_0:def 4;

                hence y in (AmpS /\ X) implies y in {x} by A11, A18, XBOOLE_0:def 4;

              end;

              now

                assume y in {x};

                then y = x by TARSKI:def 1;

                hence y in {x} implies y in (AmpS /\ X) by A15, A14, XBOOLE_0:def 4;

              end;

              hence y in {x} iff y in (AmpS /\ X) by A16;

            end;

            then (AmpS /\ X) = {x} by TARSKI: 2;

            hence thesis by A14;

          end;

          reconsider AmpS as non empty Subset of R by A6;

          

           A19: for x,y be Element of AmpS holds x <> y implies x is_not_associated_to y

          proof

            let x,y be Element of AmpS;

            assume

             A20: x <> y;

            x is_associated_to x;

            then x in ( Class x) by Def5;

            then

             A21: x in (AmpS /\ ( Class x)) by XBOOLE_0:def 4;

            ( Class x) in M by Def6;

            then

            consider z be Element of AmpS such that

             A22: (AmpS /\ ( Class x)) = {z} by A10;

            assume x is_associated_to y;

            then y in ( Class x) by Def5;

            then y in (AmpS /\ ( Class x)) by XBOOLE_0:def 4;

            then y = z by A22, TARSKI:def 1;

            hence thesis by A20, A21, A22, TARSKI:def 1;

          end;

          for a be Element of R holds ex z be Element of AmpS st z is_associated_to a

          proof

            let a be Element of R;

            reconsider N = ( Class a) as Element of M by Def6;

            consider z be Element of AmpS such that

             A23: (AmpS /\ N) = {z} by A10;

            z in {z} by TARSKI:def 1;

            then z in ( Class a) by A23, XBOOLE_0:def 4;

            then z is_associated_to a by Def5;

            hence thesis;

          end;

          hence ex s be non empty Subset of R st (for a be Element of R holds ex z be Element of s st z is_associated_to a) & for x,y be Element of s holds x <> y implies x is_not_associated_to y by A19;

        end;

        hence thesis;

      end;

    end

    definition

      let R be associative well-unital non empty multLoopStr;

      :: GCD_1:def8

      mode AmpleSet of R -> non empty Subset of R means

      : Def8: it is Am of R & ( 1. R) in it ;

      existence

      proof

        now

          let A be Am of R;

          consider x be Element of A such that

           A1: x is_associated_to ( 1. R) by Def7;

          set A9 = ({ z where z be Element of A : z <> x } \/ {( 1. R)});

          ( 1. R) in {( 1. R)} by TARSKI:def 1;

          then

           A2: ( 1. R) in A9 by XBOOLE_0:def 3;

          reconsider A9 as non empty set;

          

           A3: for x be Element of A9 holds x = ( 1. R) or x in A

          proof

            let y be Element of A9;

            per cases by XBOOLE_0:def 3;

              suppose y in { z where z be Element of A : z <> x };

              then ex zz be Element of A st y = zz & zz <> x;

              hence thesis;

            end;

              suppose y in {( 1. R)};

              hence thesis by TARSKI:def 1;

            end;

          end;

          now

            let x be object;

            now

              assume

               A4: x in A9;

              x in the carrier of R

              proof

                now

                  per cases by A3, A4;

                    case x = ( 1. R);

                    hence thesis;

                  end;

                    case x in A;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              hence x in A9 implies x in the carrier of R;

            end;

            hence x in A9 implies x in the carrier of R;

          end;

          then

          reconsider A9 as non empty Subset of R by TARSKI:def 3;

          

           A5: for z,y be Element of A9 holds z <> y implies z is_not_associated_to y

          proof

            let z,y be Element of A9;

            assume

             A6: z <> y;

            now

              per cases ;

                case z = ( 1. R) & y = ( 1. R);

                hence thesis by A6;

              end;

                case

                 A7: z = ( 1. R) & y <> ( 1. R);

                assume z is_associated_to y;

                 not y in {( 1. R)} by A7, TARSKI:def 1;

                then y in { zz where zz be Element of A : zz <> x } by XBOOLE_0:def 3;

                then ex zz be Element of A st y = zz & zz <> x;

                hence thesis by A1, A7, Def7, Th4;

              end;

                case

                 A8: z <> ( 1. R) & y = ( 1. R);

                assume z is_associated_to y;

                 not z in {( 1. R)} by A8, TARSKI:def 1;

                then z in { zz where zz be Element of A : zz <> x } by XBOOLE_0:def 3;

                then ex zz be Element of A st z = zz & zz <> x;

                hence thesis by A1, A8, Def7, Th4;

              end;

                case z <> ( 1. R) & y <> ( 1. R);

                then z in A & y in A by A3;

                hence thesis by A6, Def7;

              end;

            end;

            hence thesis;

          end;

          for a be Element of R holds ex z be Element of A9 st z is_associated_to a

          proof

            let a be Element of R;

            now

              per cases ;

                case a is_associated_to ( 1. R);

                hence thesis by A2;

              end;

                case

                 A9: a is_not_associated_to ( 1. R);

                consider z be Element of A such that

                 A10: z is_associated_to a by Def7;

                z <> x by A1, A9, A10, Th4;

                then z in { zz where zz be Element of A : zz <> x };

                then z in A9 by XBOOLE_0:def 3;

                hence thesis by A10;

              end;

            end;

            hence thesis;

          end;

          then A9 is Am of R by A5, Def7;

          hence thesis by A2;

        end;

        hence thesis;

      end;

    end

    theorem :: GCD_1:22

    

     Th22: for R be associative well-unital non empty multLoopStr holds for Amp be AmpleSet of R holds (( 1. R) in Amp) & (for a be Element of R holds ex z be Element of Amp st z is_associated_to a) & (for x,y be Element of Amp holds x <> y implies x is_not_associated_to y)

    proof

      let R be associative well-unital non empty multLoopStr;

      let Amp be AmpleSet of R;

      Amp is Am of R by Def8;

      hence thesis by Def7, Def8;

    end;

    theorem :: GCD_1:23

    for R be associative well-unital non empty multLoopStr holds for Amp be AmpleSet of R holds for x,y be Element of Amp holds x is_associated_to y implies x = y by Th22;

    theorem :: GCD_1:24

    

     Th24: for Amp be AmpleSet of R holds ( 0. R) is Element of Amp

    proof

      let Amp be AmpleSet of R;

      consider A be Element of Amp such that

       A1: A is_associated_to ( 0. R) by Th22;

      ( 0. R) divides A by A1;

      then ex D be Element of R st (( 0. R) * D) = A;

      hence thesis;

    end;

    definition

      let R be associative well-unital non empty multLoopStr;

      let Amp be AmpleSet of R;

      let x be Element of R;

      :: GCD_1:def9

      func NF (x,Amp) -> Element of R means

      : Def9: it in Amp & it is_associated_to x;

      existence

      proof

        now

          let Amp be AmpleSet of R;

          let x be Element of R;

          ex z be Element of Amp st z is_associated_to x by Th22;

          hence ex zz be Element of R st zz in Amp & zz is_associated_to x;

        end;

        hence thesis;

      end;

      uniqueness by Th4, Th22;

    end

    theorem :: GCD_1:25

    

     Th25: for Amp be AmpleSet of R holds ( NF (( 0. R),Amp)) = ( 0. R) & ( NF (( 1. R),Amp)) = ( 1. R)

    proof

      let Amp be AmpleSet of R;

      ( 1. R) in Amp & ( 0. R) is Element of Amp by Def8, Th24;

      hence thesis by Def9;

    end;

    theorem :: GCD_1:26

    for Amp be AmpleSet of R holds for a be Element of R holds a in Amp iff a = ( NF (a,Amp)) by Def9;

    definition

      let R be associative well-unital non empty multLoopStr;

      let Amp be AmpleSet of R;

      :: GCD_1:def10

      attr Amp is multiplicative means for x,y be Element of Amp holds (x * y) in Amp;

    end

    theorem :: GCD_1:27

    

     Th27: for Amp be AmpleSet of R holds Amp is multiplicative implies for x,y be Element of Amp holds y divides x & y <> ( 0. R) implies (x / y) in Amp

    proof

      let Amp be AmpleSet of R;

      assume

       A1: Amp is multiplicative;

      let x,y be Element of Amp;

      assume that

       A2: y divides x and

       A3: y <> ( 0. R);

      now

        per cases ;

          case

           A4: x <> ( 0. R);

          set d = (x / y);

          consider d9 be Element of Amp such that

           A5: d9 is_associated_to d by Th22;

          consider u be Element of R such that

           A6: u is unital and

           A7: (d * u) = d9 by A5, Th18;

          x = (y * d) by A2, A3, Def4;

          then

           A8: (u * x) = (y * d9) by A7, GROUP_1:def 3;

          

           A9: x is_associated_to (u * x)

          proof

            u divides ( 1. R) by A6;

            then

            consider e be Element of R such that

             A10: (u * e) = ( 1. R);

            

             A11: x divides (u * x);

            ((u * x) * e) = ((e * u) * x) by GROUP_1:def 3

            .= x by A10;

            then (u * x) divides x;

            hence thesis by A11;

          end;

          

           A12: (y * d9) in Amp by A1;

          (( 1. R) * x) = x

          .= (u * x) by A8, A12, A9, Th22;

          then u = ( 1. R) by A4, Th1;

          then d9 = d by A7;

          hence thesis;

        end;

          case

           A13: x = ( 0. R);

          set d = (x / y);

          x = (y * d) by A2, A3, Def4;

          then

           A14: d = ( 0. R) by A3, A13, VECTSP_2:def 1;

          ( 0. R) is Element of Amp by Th24;

          hence thesis by A14;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let R be non empty multLoopStr;

      :: GCD_1:def11

      attr R is gcd-like means

      : Def11: for x,y be Element of R holds ex z be Element of R st z divides x & z divides y & for zz be Element of R st zz divides x & zz divides y holds zz divides z;

    end

     Lm1:

    now

      let F be Field;

      let x,y be Element of F;

      now

        per cases ;

          case

           A1: x <> ( 0. F) & y <> ( 0. F);

          

           A2: for zz be Element of F st zz divides x & zz divides y holds zz divides ( 1_ F)

          proof

            let zz be Element of F;

            assume that

             A3: zz divides x and zz divides y;

            now

              per cases ;

                case zz <> ( 0. F);

                then ex zz9 be Element of F st (zz9 * zz) = ( 1_ F) by VECTSP_1:def 9;

                hence thesis;

              end;

                case

                 A4: zz = ( 0. F);

                assume zz divides x;

                then ex d be Element of F st (zz * d) = x;

                hence thesis by A1, A4;

              end;

            end;

            hence thesis by A3;

          end;

          y = (( 1_ F) * y);

          then

           A5: ( 1_ F) divides y;

          x = (( 1_ F) * x);

          then ( 1_ F) divides x;

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

        end;

          case

           A6: x = ( 0. F);

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

          then

           A7: y divides ( 0. F);

          for z be Element of F st z divides ( 0. F) & z divides y holds z divides y;

          hence ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by A6, A7;

        end;

          case

           A8: y = ( 0. F);

          (x * ( 0. F)) = ( 0. F);

          then

           A9: x divides ( 0. F);

          for z be Element of F st z divides x & z divides ( 0. F) holds z divides x;

          hence ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by A8, A9;

        end;

      end;

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

    end;

    registration

      cluster gcd-like for domRing;

      existence

      proof

        set F = the strict Field;

        reconsider F as comRing;

        reconsider F as domRing by VECTSP_2: 1;

        for x,y be Element of F holds ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by Lm1;

        then F is gcd-like;

        hence thesis;

      end;

    end

    registration

      cluster gcd-like associative commutative well-unital for non empty multLoopStr;

      existence

      proof

        set F = the strict Field;

        for x,y be Element of F holds ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by Lm1;

        then F is gcd-like;

        hence thesis;

      end;

    end

    registration

      cluster gcd-like associative commutative well-unital for non empty multLoopStr_0;

      existence

      proof

        set F = the strict Field;

        for x,y be Element of F holds ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by Lm1;

        then F is gcd-like;

        hence thesis;

      end;

    end

    registration

      cluster -> gcd-like for almost_left_invertible add-associative right_zeroed right_complementable left_unital well-unital left-distributive right-distributive commutative non empty doubleLoopStr;

      coherence

      proof

        let F be almost_left_invertible add-associative right_zeroed right_complementable left_unital well-unital left-distributive right-distributive commutative non empty doubleLoopStr;

        let x,y be Element of F;

        now

          per cases ;

            case

             A1: x <> ( 0. F) & y <> ( 0. F);

            

             A2: for zz be Element of F st zz divides x & zz divides y holds zz divides ( 1_ F)

            proof

              let zz be Element of F;

              assume that

               A3: zz divides x and zz divides y;

              now

                per cases ;

                  case zz <> ( 0. F);

                  then ex zz9 be Element of F st (zz9 * zz) = ( 1_ F) by VECTSP_1:def 9;

                  hence thesis;

                end;

                  case

                   A4: zz = ( 0. F);

                  assume zz divides x;

                  then ex d be Element of F st (zz * d) = x;

                  hence thesis by A1, A4;

                end;

              end;

              hence thesis by A3;

            end;

            y = (( 1_ F) * y);

            then

             A5: ( 1_ F) divides y;

            x = (( 1_ F) * x);

            then ( 1_ F) divides x;

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

          end;

            case

             A6: x = ( 0. F);

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

            then

             A7: y divides ( 0. F);

            for z be Element of F st z divides ( 0. F) & z divides y holds z divides y;

            hence ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by A6, A7;

          end;

            case

             A8: y = ( 0. F);

            (x * ( 0. F)) = ( 0. F);

            then

             A9: x divides ( 0. F);

            for z be Element of F st z divides x & z divides ( 0. F) holds z divides x;

            hence ex z be Element of F st z divides x & z divides y & for zz be Element of F st zz divides x & zz divides y holds zz divides z by A8, A9;

          end;

        end;

        hence thesis;

      end;

    end

    registration

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

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    definition

      mode gcdDomain is gcd-like domRing-like non degenerated commutative Ring;

    end

    definition

      let R be gcd-like associative well-unital non empty multLoopStr;

      let Amp be AmpleSet of R;

      let x,y be Element of R;

      :: GCD_1:def12

      func gcd (x,y,Amp) -> Element of R means

      : Def12: it in Amp & it divides x & it divides y & for z be Element of R st z divides x & z divides y holds z divides it ;

      existence

      proof

        consider u be Element of R such that

         A1: u divides x & u divides y and

         A2: for zz be Element of R st zz divides x & zz divides y holds zz divides u by Def11;

        consider z be Element of Amp such that

         A3: z is_associated_to u by Th22;

        

         A4: for zz be Element of R st zz divides x & zz divides y holds zz divides z

        proof

          let zz be Element of R;

          assume zz divides x & zz divides y;

          then

           A5: zz divides u by A2;

          u divides z by A3;

          hence thesis by A5, Th2;

        end;

        z divides u by A3;

        then z divides x & z divides y by A1, Th2;

        hence thesis by A4;

      end;

      uniqueness

      proof

        now

          let z1 be Element of R such that

           A6: z1 in Amp and

           A7: z1 divides x & z1 divides y & for z be Element of R st z divides x & z divides y holds z divides z1;

          let z2 be Element of R such that

           A8: z2 in Amp and

           A9: z2 divides x & z2 divides y & for z be Element of R st z divides x & z divides y holds z divides z2;

          z1 divides z2 & z2 divides z1 by A7, A9;

          then z1 is_associated_to z2;

          hence z1 = z2 by A6, A8, Th22;

        end;

        hence thesis;

      end;

    end

    reserve R for gcdDomain;

    theorem :: GCD_1:28

    

     Th28: for Amp be AmpleSet of R holds for a,b,c be Element of R holds c divides ( gcd (a,b,Amp)) implies c divides a & c divides b

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      assume C divides ( gcd (A,B,Amp));

      then

      consider D be Element of R such that

       A1: (C * D) = ( gcd (A,B,Amp));

      ( gcd (A,B,Amp)) divides A by Def12;

      then

      consider E be Element of R such that

       A2: (( gcd (A,B,Amp)) * E) = A;

      

       A3: (C * (D * E)) = A by A1, A2, GROUP_1:def 3;

      ( gcd (A,B,Amp)) divides B by Def12;

      then

      consider E be Element of R such that

       A4: (( gcd (A,B,Amp)) * E) = B;

      (C * (D * E)) = B by A1, A4, GROUP_1:def 3;

      hence thesis by A3;

    end;

    theorem :: GCD_1:29

    

     Th29: for Amp be AmpleSet of R holds for a,b be Element of R holds ( gcd (a,b,Amp)) = ( gcd (b,a,Amp))

    proof

      let Amp be AmpleSet of R;

      let A,B be Element of R;

      set D = ( gcd (A,B,Amp));

      

       A1: D divides A & for z be Element of R st z divides B & z divides A holds z divides D by Def12;

      D in Amp & D divides B by Def12;

      hence thesis by A1, Def12;

    end;

    theorem :: GCD_1:30

    

     Th30: for Amp be AmpleSet of R holds for a be Element of R holds ( gcd (a,( 0. R),Amp)) = ( NF (a,Amp)) & ( gcd (( 0. R),a,Amp)) = ( NF (a,Amp))

    proof

      let Amp be AmpleSet of R;

      let A be Element of R;

      

       A1: ( NF (A,Amp)) in Amp by Def9;

      (( NF (A,Amp)) * ( 0. R)) = ( 0. R);

      then

       A2: ( NF (A,Amp)) divides ( 0. R);

      

       A3: ( NF (A,Amp)) is_associated_to A by Def9;

      

       A4: for z be Element of R st z divides A & z divides ( 0. R) holds z divides ( NF (A,Amp)) by A3, Th2;

      ( NF (A,Amp)) divides A by A3;

      then ( gcd (A,( 0. R),Amp)) = ( NF (A,Amp)) by A2, A4, A1, Def12;

      hence thesis by Th29;

    end;

    theorem :: GCD_1:31

    

     Th31: for Amp be AmpleSet of R holds ( gcd (( 0. R),( 0. R),Amp)) = ( 0. R)

    proof

      let Amp be AmpleSet of R;

      ( gcd (( 0. R),( 0. R),Amp)) = ( NF (( 0. R),Amp)) by Th30;

      hence thesis by Th25;

    end;

    theorem :: GCD_1:32

    

     Th32: for Amp be AmpleSet of R holds for a be Element of R holds ( gcd (a,( 1. R),Amp)) = ( 1. R) & ( gcd (( 1. R),a,Amp)) = ( 1. R)

    proof

      let Amp be AmpleSet of R;

      let A be Element of R;

      (( 1. R) * A) = A;

      then

       A1: ( 1. R) divides A;

      ( 1. R) in Amp & for z be Element of R st z divides A & z divides ( 1. R) holds z divides ( 1. R) by Def8;

      then ( gcd (A,( 1. R),Amp)) = ( 1. R) by A1, Def12;

      hence thesis by Th29;

    end;

    theorem :: GCD_1:33

    

     Th33: for Amp be AmpleSet of R holds for a,b be Element of R holds ( gcd (a,b,Amp)) = ( 0. R) iff a = ( 0. R) & b = ( 0. R)

    proof

      let Amp be AmpleSet of R;

      let A,B be Element of R;

       A1:

      now

        assume

         A2: ( gcd (A,B,Amp)) = ( 0. R);

        then ( 0. R) divides B by Def12;

        then

         A3: ex E be Element of R st (( 0. R) * E) = B;

        ( 0. R) divides A by A2, Def12;

        then ex D be Element of R st (( 0. R) * D) = A;

        hence ( gcd (A,B,Amp)) = ( 0. R) implies A = ( 0. R) & B = ( 0. R) by A3;

      end;

      A = ( 0. R) & B = ( 0. R) implies ( gcd (A,B,Amp)) = ( 0. R)

      proof

        assume that

         A4: A = ( 0. R) and

         A5: B = ( 0. R);

        ( gcd (A,B,Amp)) = ( NF (A,Amp)) by A5, Th30;

        hence thesis by A4, Th25;

      end;

      hence thesis by A1;

    end;

    theorem :: GCD_1:34

    

     Th34: for Amp be AmpleSet of R holds for a,b,c be Element of R holds b is_associated_to c implies ( gcd (a,b,Amp)) is_associated_to ( gcd (a,c,Amp)) & ( gcd (b,a,Amp)) is_associated_to ( gcd (c,a,Amp))

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      

       A1: ( gcd (A,B,Amp)) divides B by Def12;

      

       A2: ( gcd (A,B,Amp)) divides A by Def12;

      

       A3: ( gcd (A,C,Amp)) divides A by Def12;

      

       A4: ( gcd (A,C,Amp)) divides C by Def12;

      

       A5: ( gcd (A,B,Amp)) = ( gcd (B,A,Amp)) by Th29;

      assume

       A6: B is_associated_to C;

      then C divides B;

      then ( gcd (A,C,Amp)) divides B by A4, Th2;

      then

       A7: ( gcd (A,C,Amp)) divides ( gcd (A,B,Amp)) by A3, Def12;

      B divides C by A6;

      then ( gcd (A,B,Amp)) divides C by A1, Th2;

      then ( gcd (A,B,Amp)) divides ( gcd (A,C,Amp)) by A2, Def12;

      then ( gcd (A,B,Amp)) is_associated_to ( gcd (A,C,Amp)) by A7;

      hence thesis by A5, Th29;

    end;

    theorem :: GCD_1:35

    

     Th35: for Amp be AmpleSet of R holds for a,b,c be Element of R holds ( gcd (( gcd (a,b,Amp)),c,Amp)) = ( gcd (a,( gcd (b,c,Amp)),Amp))

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      set D = ( gcd (( gcd (A,B,Amp)),C,Amp));

      set E = ( gcd (A,( gcd (B,C,Amp)),Amp));

      

       A1: D divides C by Def12;

      

       A2: E divides A by Def12;

      

       A3: E divides ( gcd (B,C,Amp)) by Def12;

      then

       A4: E divides C by Th28;

      E divides B by A3, Th28;

      then E divides ( gcd (A,B,Amp)) by A2, Def12;

      then

       A5: E divides D by A4, Def12;

      

       A6: D is Element of Amp & E is Element of Amp by Def12;

      

       A7: D divides ( gcd (A,B,Amp)) by Def12;

      then

       A8: D divides A by Th28;

      D divides B by A7, Th28;

      then D divides ( gcd (B,C,Amp)) by A1, Def12;

      then D divides E by A8, Def12;

      then D is_associated_to E by A5;

      hence thesis by A6, Th22;

    end;

    theorem :: GCD_1:36

    

     Th36: for Amp be AmpleSet of R holds for a,b,c be Element of R holds ( gcd ((a * c),(b * c),Amp)) is_associated_to (c * ( gcd (a,b,Amp)))

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      now

        per cases ;

          case

           A1: C <> ( 0. R);

          set D = ( gcd (A,B,Amp));

          now

            per cases ;

              case

               A2: D <> ( 0. R);

              set E = ( gcd ((A * C),(B * C),Amp));

              

               A3: E divides (B * C) by Def12;

              D divides B by Def12;

              then

               A4: (C * D) divides (B * C) by Th5;

              D divides A by Def12;

              then (C * D) divides (A * C) by Th5;

              then (C * D) divides ( gcd ((A * C),(B * C),Amp)) by A4, Def12;

              then

              consider F be Element of R such that

               A5: E = ((C * D) * F);

              

               A6: E divides (A * C) by Def12;

              (D * F) divides A & (D * F) divides B

              proof

                consider G be Element of R such that

                 A7: (((C * D) * F) * G) = (A * C) by A5, A6;

                ((C * (D * F)) * G) = (C * A) by A7, GROUP_1:def 3;

                then

                 A8: (C * (D * F)) divides (C * A);

                consider G be Element of R such that

                 A9: (((C * D) * F) * G) = (B * C) by A5, A3;

                ((C * (D * F)) * G) = (C * B) by A9, GROUP_1:def 3;

                then (C * (D * F)) divides (C * B);

                hence thesis by A1, A8, Th15;

              end;

              then

               A10: (D * F) divides D by Def12;

              D = (D * ( 1. R));

              then F divides ( 1. R) by A2, A10, Th15;

              then F is unital;

              hence thesis by A5, Th18;

            end;

              case

               A11: D = ( 0. R);

              then

               A12: (C * ( gcd (A,B,Amp))) = ( 0. R);

              A = ( 0. R) & B = ( 0. R) by A11, Th33;

              

              then ( gcd ((A * C),(B * C),Amp)) = ( gcd (( 0. R),(( 0. R) * C),Amp))

              .= ( gcd (( 0. R),( 0. R),Amp))

              .= (C * ( gcd (A,B,Amp))) by A12, Th31;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          case

           A13: C = ( 0. R);

          then (A * C) = ( 0. R) & (B * C) = ( 0. R);

          

          then ( gcd ((A * C),(B * C),Amp)) = ( 0. R) by Th31

          .= (C * ( gcd (A,B,Amp))) by A13;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:37

    

     Th37: for Amp be AmpleSet of R holds for a,b,c be Element of R holds ( gcd (a,b,Amp)) = ( 1. R) implies ( gcd (a,(b * c),Amp)) = ( gcd (a,c,Amp))

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      assume ( gcd (A,B,Amp)) = ( 1. R);

      then

       A1: (C * ( gcd (A,B,Amp))) = C;

      ( gcd ((A * C),(B * C),Amp)) is_associated_to (C * ( gcd (A,B,Amp))) by Th36;

      then ( gcd (A,C,Amp)) is_associated_to ( gcd (A,( gcd ((A * C),(B * C),Amp)),Amp)) by A1, Th34;

      then

       A2: ( gcd (A,C,Amp)) is_associated_to ( gcd (( gcd (A,(A * C),Amp)),(B * C),Amp)) by Th35;

      

       A3: (A * ( gcd (( 1. R),C,Amp))) = (A * ( 1. R)) by Th32

      .= A;

      ( gcd ((A * ( 1. R)),(A * C),Amp)) is_associated_to (A * ( gcd (( 1. R),C,Amp))) by Th36;

      then ( gcd (A,(A * C),Amp)) is_associated_to A by A3;

      then

       A4: ( gcd (( gcd (A,(A * C),Amp)),(B * C),Amp)) is_associated_to ( gcd (A,(B * C),Amp)) by Th34;

      ( gcd (A,(B * C),Amp)) is Element of Amp & ( gcd (A,C,Amp)) is Element of Amp by Def12;

      hence thesis by A2, A4, Th4, Th22;

    end;

    theorem :: GCD_1:38

    

     Th38: for Amp be AmpleSet of R holds for a,b,c be Element of R holds c = ( gcd (a,b,Amp)) & c <> ( 0. R) implies ( gcd ((a / c),(b / c),Amp)) = ( 1. R)

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      assume that

       A1: C = ( gcd (A,B,Amp)) and

       A2: C <> ( 0. R);

      set A1 = (A / C);

      C divides A by A1, Def12;

      then

       A3: (A1 * C) = A by A2, Def4;

      set B1 = (B / C);

      

       A4: ( gcd ((A1 * C),(B1 * C),Amp)) is_associated_to (C * ( gcd (A1,B1,Amp))) by Th36;

      

       A5: ( gcd (A1,B1,Amp)) is Element of Amp & ( 1. R) is Element of Amp by Def8, Def12;

      C divides B by A1, Def12;

      then ( gcd (A,B,Amp)) = ( gcd ((A1 * C),(B1 * C),Amp)) by A2, A3, Def4;

      then (C * ( 1. R)) is_associated_to (C * ( gcd (A1,B1,Amp))) by A1, A4;

      hence thesis by A2, A5, Th19, Th22;

    end;

    theorem :: GCD_1:39

    

     Th39: for Amp be AmpleSet of R holds for a,b,c be Element of R holds ( gcd ((a + (b * c)),c,Amp)) = ( gcd (a,c,Amp))

    proof

      let Amp be AmpleSet of R;

      let A,B,C be Element of R;

      set D = ( gcd (A,C,Amp));

      D divides A by Def12;

      then

      consider E be Element of R such that

       A1: (D * E) = A;

      

       A2: D divides C by Def12;

      then

      consider F be Element of R such that

       A3: (D * F) = C;

      

       A4: for z be Element of R st z divides (A + (B * C)) & z divides C holds z divides D

      proof

        let Z be Element of R;

        assume that

         A5: Z divides (A + (B * C)) and

         A6: Z divides C;

        consider X be Element of R such that

         A7: (Z * X) = C by A6;

        consider Y be Element of R such that

         A8: (Z * Y) = (A + (B * C)) by A5;

        (Z * (Y + ( - (B * X)))) = ((Z * Y) + (Z * ( - (B * X)))) by VECTSP_1:def 2

        .= ((Z * Y) + ( - (Z * (X * B)))) by VECTSP_1: 8

        .= ((A + (B * C)) + ( - (C * B))) by A7, A8, GROUP_1:def 3

        .= (A + ((B * C) + ( - (C * B)))) by RLVECT_1:def 3

        .= (A + ( 0. R)) by RLVECT_1:def 10

        .= A by RLVECT_1: 4;

        then Z divides A;

        hence thesis by A6, Def12;

      end;

      (D * (E + (F * B))) = ((D * E) + (D * (F * B))) by VECTSP_1:def 2

      .= (A + (B * C)) by A1, A3, GROUP_1:def 3;

      then

       A9: D divides (A + (B * C));

      D is Element of Amp by Def12;

      hence thesis by A2, A9, A4, Def12;

    end;

    begin

    ::$Notion-Name

    theorem :: GCD_1:40

    

     Th40: for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds ( gcd (r1,r2,Amp)) = ( 1. R) & ( gcd (s1,s2,Amp)) = ( 1. R) & r2 <> ( 0. R) implies ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),(r2 * (s2 / ( gcd (r2,s2,Amp)))),Amp)) = ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: ( gcd (r1,r2,Amp)) = ( 1. R) and

       A2: ( gcd (s1,s2,Amp)) = ( 1. R) and

       A3: r2 <> ( 0. R);

      set d = ( gcd (r2,s2,Amp));

      set r = (r2 / d);

      set s = (s2 / d);

      

       A4: d <> ( 0. R) by A3, Th33;

      then

       A5: ( gcd (r,s,Amp)) = ( 1. R) by Th38;

      

       A6: d divides s2 by Def12;

      ( gcd (s,s1,Amp)) = ( 1. R)

      proof

        ( gcd (s,s1,Amp)) divides s by Def12;

        then

        consider e be Element of R such that

         A7: (( gcd (s,s1,Amp)) * e) = s;

        (( gcd (s,s1,Amp)) * (e * d)) = (s * d) by A7, GROUP_1:def 3

        .= s2 by A6, A4, Def4;

        then

         A8: ( gcd (s,s1,Amp)) divides s2;

        

         A9: ( gcd (s,s1,Amp)) is Element of Amp & ( 1. R) is Element of Amp by Def8, Def12;

        (( 1. R) * ( gcd (s,s1,Amp))) = ( gcd (s,s1,Amp));

        then

         A10: ( 1. R) divides ( gcd (s,s1,Amp));

        ( gcd (s,s1,Amp)) divides s1 by Def12;

        then ( gcd (s,s1,Amp)) divides ( gcd (s1,s2,Amp)) by A8, Def12;

        then ( gcd (s,s1,Amp)) is_associated_to ( 1. R) by A2, A10;

        hence thesis by A9, Th22;

      end;

      then

       A11: ( gcd (s,(s1 * r),Amp)) = ( gcd (s,r,Amp)) by Th37;

      ( gcd (((r1 * s) + (s1 * r)),s,Amp)) = ( gcd ((s1 * r),s,Amp)) by Th39;

      

      then

       A12: ( gcd (((r1 * s) + (s1 * r)),s,Amp)) = ( gcd (s,(s1 * r),Amp)) by Th29

      .= ( 1. R) by A11, A5, Th29;

      

       A13: d divides (d * r2);

      

       A14: d divides r2 by Def12;

      ( gcd (r,r1,Amp)) = ( 1. R)

      proof

        ( gcd (r,r1,Amp)) divides r by Def12;

        then

        consider e be Element of R such that

         A15: (( gcd (r,r1,Amp)) * e) = r;

        (( gcd (r,r1,Amp)) * (e * d)) = (r * d) by A15, GROUP_1:def 3

        .= r2 by A14, A4, Def4;

        then

         A16: ( gcd (r,r1,Amp)) divides r2;

        

         A17: ( gcd (r,r1,Amp)) is Element of Amp & ( 1. R) is Element of Amp by Def8, Def12;

        (( 1. R) * ( gcd (r,r1,Amp))) = ( gcd (r,r1,Amp));

        then

         A18: ( 1. R) divides ( gcd (r,r1,Amp));

        ( gcd (r,r1,Amp)) divides r1 by Def12;

        then ( gcd (r,r1,Amp)) divides ( gcd (r1,r2,Amp)) by A16, Def12;

        then ( gcd (r,r1,Amp)) is_associated_to ( 1. R) by A1, A18;

        hence thesis by A17, Th22;

      end;

      then

       A19: ( gcd (r,(r1 * s),Amp)) = ( gcd (r,s,Amp)) by Th37;

      

       A20: ( gcd (((r1 * s) + (s1 * r)),r,Amp)) = ( gcd ((r1 * s),r,Amp)) by Th39;

      ( gcd (r,s,Amp)) = ( 1. R) by A4, Th38;

      then

       A21: ( gcd (((r1 * s) + (s1 * r)),(d * r),Amp)) = ( gcd (((r1 * s) + (s1 * r)),d,Amp)) by A20, A19, Th29, Th37;

      (r2 * s) = ((( 1. R) * r2) * s)

      .= (((d / d) * r2) * s) by A4, Th9

      .= (((d * r2) / d) * s) by A4, A13, Th11

      .= (s * (d * r)) by A14, A4, A13, Th11;

      hence thesis by A12, A21, Th37;

    end;

    ::$Notion-Name

    theorem :: GCD_1:41

    

     Th41: for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds ( gcd (r1,r2,Amp)) = ( 1. R) & ( gcd (s1,s2,Amp)) = ( 1. R) & r2 <> ( 0. R) & s2 <> ( 0. R) implies ( gcd (((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp)))),((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp)))),Amp)) = ( 1. R)

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: ( gcd (r1,r2,Amp)) = ( 1. R) and

       A2: ( gcd (s1,s2,Amp)) = ( 1. R) and

       A3: r2 <> ( 0. R) and

       A4: s2 <> ( 0. R);

      set d1 = ( gcd (r1,s2,Amp));

      

       A5: d1 <> ( 0. R) by A4, Th33;

      set d2 = ( gcd (s1,r2,Amp));

      set s19 = (s1 / d2);

      set r29 = (r2 / d2);

      

       A6: d2 <> ( 0. R) by A3, Th33;

      then

       A7: ( gcd (s19,r29,Amp)) = ( 1. R) by Th38;

      set r19 = (r1 / d1);

      

       A8: ( gcd (r19,r29,Amp)) divides r29 by Def12;

      d2 divides r2 by Def12;

      then (r29 * d2) = r2 by A6, Def4;

      then r29 divides r2;

      then

       A9: ( gcd (r19,r29,Amp)) divides r2 by A8, Th2;

      

       A10: ( gcd (r19,r29,Amp)) is Element of Amp & ( 1. R) is Element of Amp by Def8, Def12;

      d1 divides r1 by Def12;

      then (r19 * d1) = r1 by A5, Def4;

      then

       A11: r19 divides r1;

      (( 1. R) * ( gcd (r19,r29,Amp))) = ( gcd (r19,r29,Amp));

      then

       A12: ( 1. R) divides ( gcd (r19,r29,Amp));

      ( gcd (r19,r29,Amp)) divides r19 by Def12;

      then ( gcd (r19,r29,Amp)) divides r1 by A11, Th2;

      then ( gcd (r19,r29,Amp)) divides ( gcd (r1,r2,Amp)) by A9, Def12;

      then ( gcd (r19,r29,Amp)) is_associated_to ( 1. R) by A1, A12;

      then ( gcd (r19,r29,Amp)) = ( 1. R) by A10, Th22;

      then

       A13: ( gcd (r29,r19,Amp)) = ( 1. R) by Th29;

      set s29 = (s2 / d1);

      

       A14: ( gcd (s19,s29,Amp)) divides s29 by Def12;

      d1 divides s2 by Def12;

      then (s29 * d1) = s2 by A5, Def4;

      then s29 divides s2;

      then

       A15: ( gcd (s19,s29,Amp)) divides s2 by A14, Th2;

      

       A16: ( gcd (s19,s29,Amp)) is Element of Amp & ( 1. R) is Element of Amp by Def8, Def12;

      d2 divides s1 by Def12;

      then (s19 * d2) = s1 by A6, Def4;

      then

       A17: s19 divides s1;

      (( 1. R) * ( gcd (s19,s29,Amp))) = ( gcd (s19,s29,Amp));

      then

       A18: ( 1. R) divides ( gcd (s19,s29,Amp));

      ( gcd (s19,s29,Amp)) divides s19 by Def12;

      then ( gcd (s19,s29,Amp)) divides s1 by A17, Th2;

      then ( gcd (s19,s29,Amp)) divides ( gcd (s1,s2,Amp)) by A15, Def12;

      then ( gcd (s19,s29,Amp)) is_associated_to ( 1. R) by A2, A18;

      then

       A19: ( gcd (s19,s29,Amp)) = ( 1. R) by A16, Th22;

      

       A20: ( gcd (s29,r19,Amp)) = ( gcd ((r1 / d1),(s2 / d1),Amp)) by Th29

      .= ( 1. R) by A5, Th38;

      ( gcd ((r19 * s19),r29,Amp)) = ( gcd (r29,(r19 * s19),Amp)) by Th29

      .= ( gcd (r29,s19,Amp)) by A13, Th37

      .= ( 1. R) by A7, Th29;

      

      then ( gcd ((r19 * s19),(r29 * s29),Amp)) = ( gcd ((r19 * s19),s29,Amp)) by Th37

      .= ( gcd (s29,(r19 * s19),Amp)) by Th29

      .= ( gcd (s29,s19,Amp)) by A20, Th37

      .= ( 1. R) by A19, Th29;

      hence thesis;

    end;

    begin

    definition

      let R be gcd-like associative well-unital non empty multLoopStr;

      let Amp be AmpleSet of R;

      let x,y be Element of R;

      :: GCD_1:def13

      pred x,y are_canonical_wrt Amp means ( gcd (x,y,Amp)) = ( 1. R);

    end

    theorem :: GCD_1:42

    

     Th42: for Amp,Amp9 be AmpleSet of R holds for x,y be Element of R st (x,y) are_canonical_wrt Amp holds (x,y) are_canonical_wrt Amp9

    proof

      let Amp,Amp9 be AmpleSet of R;

      let x,y be Element of R;

      (( 1. R) * x) = x;

      then

       A1: ( 1. R) divides x;

      (( 1. R) * y) = y;

      then

       A2: ( 1. R) divides y;

      assume (x,y) are_canonical_wrt Amp;

      then ( gcd (x,y,Amp)) = ( 1. R);

      then

       A3: for z be Element of R st z divides x & z divides y holds z divides ( 1. R) by Def12;

      ( 1. R) in Amp9 by Def8;

      then ( gcd (x,y,Amp9)) = ( 1. R) by A3, A1, A2, Def12;

      hence thesis;

    end;

    definition

      let R be gcd-like associative well-unital non empty multLoopStr;

      let x,y be Element of R;

      :: GCD_1:def14

      pred x,y are_co-prime means ex Amp be AmpleSet of R st ( gcd (x,y,Amp)) = ( 1. R);

    end

    definition

      let R be gcdDomain;

      let x,y be Element of R;

      :: original: are_co-prime

      redefine

      pred x,y are_co-prime ;

      symmetry

      proof

        let x,y be Element of R;

        given Amp be AmpleSet of R such that

         A1: ( gcd (x,y,Amp)) = ( 1. R);

        ( gcd (y,x,Amp)) = ( 1. R) by A1, Th29;

        hence thesis;

      end;

    end

    theorem :: GCD_1:43

    

     Th43: for Amp be AmpleSet of R holds for x,y be Element of R holds (x,y) are_co-prime implies ( gcd (x,y,Amp)) = ( 1. R)

    proof

      let Amp be AmpleSet of R;

      let x,y be Element of R;

      assume (x,y) are_co-prime ;

      then

      consider Amp9 be AmpleSet of R such that

       A1: ( gcd (x,y,Amp9)) = ( 1. R);

      (x,y) are_canonical_wrt Amp9 by A1;

      then (x,y) are_canonical_wrt Amp by Th42;

      hence thesis;

    end;

    definition

      let R be gcd-like associative well-unital non empty multLoopStr_0;

      let Amp be AmpleSet of R;

      let x,y be Element of R;

      :: GCD_1:def15

      pred x,y are_normalized_wrt Amp means ( gcd (x,y,Amp)) = ( 1. R) & y in Amp & y <> ( 0. R);

    end

    definition

      let R be gcdDomain;

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: (r1,r2) are_co-prime and

       A2: (s1,s2) are_co-prime and

       A3: r2 = ( NF (r2,Amp)) and

       A4: s2 = ( NF (s2,Amp));

      :: GCD_1:def16

      func add1 (r1,r2,s1,s2,Amp) -> Element of R equals

      : Def16: s1 if r1 = ( 0. R),

r1 if s1 = ( 0. R),

((r1 * s2) + (r2 * s1)) if ( gcd (r2,s2,Amp)) = ( 1. R),

( 0. R) if ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R)

      otherwise (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)));

      coherence ;

      consistency

      proof

        

         A5: ( gcd (s1,s2,Amp)) = ( 1. R) by A2, Th43;

        

         A6: s1 = ( 0. R) & ( gcd (r2,s2,Amp)) = ( 1. R) implies for z be Element of R holds z = r1 iff z = ((r1 * s2) + (r2 * s1))

        proof

          assume that

           A7: s1 = ( 0. R) and ( gcd (r2,s2,Amp)) = ( 1. R);

          

           A8: s2 = ( 1. R) by A4, A5, A7, Th30;

          let z be Element of R;

          ((r1 * s2) + (r2 * s1)) = ((r1 * s2) + ( 0. R)) by A7

          .= (r1 * ( 1. R)) by A8, RLVECT_1: 4

          .= r1;

          hence thesis;

        end;

        

         A9: s1 = ( 0. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = r1 iff z = ( 0. R)

        proof

          

           A10: ( 1. R) <> ( 0. R);

          assume that

           A11: s1 = ( 0. R) and

           A12: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          let z be Element of R;

          

           A13: s2 = ( 1. R) by A4, A5, A11, Th30;

          then

           A14: ( gcd (r2,s2,Amp)) = ( 1. R) by Th32;

          ( 0. R) = ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + ( 0. R)) by A11, A12

          .= (r1 * (( 1. R) / ( gcd (r2,s2,Amp)))) by A13, RLVECT_1: 4

          .= (r1 * ( 1. R)) by A14, A10, Th9

          .= r1;

          hence thesis;

        end;

        

         A15: ( gcd (r1,r2,Amp)) = ( 1. R) by A1, Th43;

        

         A16: r1 = ( 0. R) & ( gcd (r2,s2,Amp)) = ( 1. R) implies for z be Element of R holds z = s1 iff z = ((r1 * s2) + (r2 * s1))

        proof

          assume that

           A17: r1 = ( 0. R) and ( gcd (r2,s2,Amp)) = ( 1. R);

          

           A18: r2 = ( 1. R) by A3, A15, A17, Th30;

          let z be Element of R;

          ((r1 * s2) + (r2 * s1)) = (( 0. R) + (r2 * s1)) by A17

          .= (( 1. R) * s1) by A18, RLVECT_1: 4

          .= s1;

          hence thesis;

        end;

        

         A19: r1 = ( 0. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = s1 iff z = ( 0. R)

        proof

          

           A20: ( 1. R) <> ( 0. R);

          assume that

           A21: r1 = ( 0. R) and

           A22: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          let z be Element of R;

          

           A23: r2 = ( 1. R) by A3, A15, A21, Th30;

          then

           A24: ( gcd (r2,s2,Amp)) = ( 1. R) by Th32;

          ( 0. R) = (( 0. R) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) by A21, A22

          .= (s1 * (( 1. R) / ( gcd (r2,s2,Amp)))) by A23, RLVECT_1: 4

          .= (s1 * ( 1. R)) by A24, A20, Th9

          .= s1;

          hence thesis;

        end;

        ( gcd (r2,s2,Amp)) = ( 1. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = ((r1 * s2) + (r2 * s1)) iff z = ( 0. R)

        proof

          assume

           A25: ( gcd (r2,s2,Amp)) = ( 1. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          let z be Element of R;

          ( 0. R) = ((r1 * s2) + (s1 * (r2 / ( 1. R)))) by A25, Th10

          .= ((r1 * s2) + (s1 * r2)) by Th10;

          hence thesis;

        end;

        hence thesis by A16, A19, A6, A9;

      end;

    end

    definition

      let R be gcdDomain;

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: (r1,r2) are_co-prime and

       A2: (s1,s2) are_co-prime and

       A3: r2 = ( NF (r2,Amp)) and

       A4: s2 = ( NF (s2,Amp));

      :: GCD_1:def17

      func add2 (r1,r2,s1,s2,Amp) -> Element of R equals

      : Def17: s2 if r1 = ( 0. R),

r2 if s1 = ( 0. R),

(r2 * s2) if ( gcd (r2,s2,Amp)) = ( 1. R),

( 1. R) if ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R)

      otherwise ((r2 * (s2 / ( gcd (r2,s2,Amp)))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)));

      coherence ;

      consistency

      proof

        

         A5: ( gcd (r2,s2,Amp)) = ( 1. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = (r2 * s2) iff z = ( 1. R)

        proof

          assume that

           A6: ( gcd (r2,s2,Amp)) = ( 1. R) and

           A7: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          

           A8: ( 0. R) = ((r1 * s2) + (s1 * (r2 / ( 1. R)))) by A6, A7, Th10

          .= ((r1 * s2) + (s1 * r2)) by Th10;

          then

           A9: (r1 * s2) = ( - (s1 * r2)) by RLVECT_1: 6;

          

           A10: (s1 * r2) = ( - (r1 * s2)) by A8, RLVECT_1: 6;

          ( gcd (s2,s1,Amp)) = ( 1. R) by A2, Th43;

          

          then ( gcd (s2,(s1 * r2),Amp)) = ( gcd (s2,r2,Amp)) by Th37

          .= ( 1. R) by A6, Th29;

          

          then ( 1. R) = ( gcd ((( 1. R) * s2),( - (r1 * s2)),Amp)) by A10

          .= ( gcd ((( 1. R) * s2),(( - r1) * s2),Amp)) by VECTSP_1: 8;

          then

           A11: ( 1. R) is_associated_to (s2 * ( gcd (( 1. R),( - r1),Amp))) by Th36;

          let z be Element of R;

          

           A12: ( 1. R) in Amp by Th22;

          ( gcd (r2,r1,Amp)) = ( 1. R) by A1, Th43;

          then ( gcd (r2,(r1 * s2),Amp)) = ( 1. R) by A6, Th37;

          

          then ( 1. R) = ( gcd ((( 1. R) * r2),( - (s1 * r2)),Amp)) by A9

          .= ( gcd ((( 1. R) * r2),(( - s1) * r2),Amp)) by VECTSP_1: 8;

          then

           A13: ( 1. R) is_associated_to (r2 * ( gcd (( 1. R),( - s1),Amp))) by Th36;

          (s2 * ( gcd (( 1. R),( - r1),Amp))) = (s2 * ( 1. R)) by Th32

          .= s2;

          then

           A14: s2 = ( 1. R) by A4, A12, A11, Def9;

          (r2 * ( gcd (( 1. R),( - s1),Amp))) = (r2 * ( 1. R)) by Th32

          .= r2;

          then r2 = ( 1. R) by A3, A13, A12, Def9;

          hence thesis by A14;

        end;

        

         A15: ( gcd (r1,r2,Amp)) = ( 1. R) by A1, Th43;

        

         A16: r1 = ( 0. R) & ( gcd (r2,s2,Amp)) = ( 1. R) implies for z be Element of R holds z = s2 iff z = (r2 * s2)

        proof

          assume that

           A17: r1 = ( 0. R) and ( gcd (r2,s2,Amp)) = ( 1. R);

          let z be Element of R;

          r2 = ( 1. R) by A3, A15, A17, Th30;

          hence thesis;

        end;

        

         A18: ( gcd (s1,s2,Amp)) = ( 1. R) by A2, Th43;

        

         A19: s1 = ( 0. R) & ( gcd (r2,s2,Amp)) = ( 1. R) implies for z be Element of R holds z = r2 iff z = (r2 * s2)

        proof

          assume that

           A20: s1 = ( 0. R) and ( gcd (r2,s2,Amp)) = ( 1. R);

          let z be Element of R;

          s2 = ( 1. R) by A4, A18, A20, Th30;

          hence thesis;

        end;

        

         A21: s1 = ( 0. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = r2 iff z = ( 1. R)

        proof

          

           A22: ( 1. R) <> ( 0. R);

          assume that

           A23: s1 = ( 0. R) and

           A24: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          let z be Element of R;

          

           A25: s2 = ( 1. R) by A4, A18, A23, Th30;

          then

           A26: ( gcd (r2,s2,Amp)) = ( 1. R) by Th32;

          ( 0. R) = ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + ( 0. R)) by A23, A24

          .= (r1 * (( 1. R) / ( gcd (r2,s2,Amp)))) by A25, RLVECT_1: 4

          .= (r1 * ( 1. R)) by A26, A22, Th9

          .= r1;

          hence thesis by A3, A15, Th30;

        end;

        

         A27: r1 = ( 0. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R) implies for z be Element of R holds z = s2 iff z = ( 1. R)

        proof

          

           A28: ( 1. R) <> ( 0. R);

          assume that

           A29: r1 = ( 0. R) and

           A30: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          let z be Element of R;

          

           A31: r2 = ( 1. R) by A3, A15, A29, Th30;

          then

           A32: ( gcd (r2,s2,Amp)) = ( 1. R) by Th32;

          ( 0. R) = (( 0. R) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) by A29, A30

          .= (s1 * (( 1. R) / ( gcd (r2,s2,Amp)))) by A31, RLVECT_1: 4

          .= (s1 * ( 1. R)) by A32, A28, Th9

          .= s1;

          hence thesis by A4, A18, Th30;

        end;

        r1 = ( 0. R) & s1 = ( 0. R) implies for z be Element of R holds z = s2 iff z = r2

        proof

          assume that

           A33: r1 = ( 0. R) and

           A34: s1 = ( 0. R);

          let z be Element of R;

          r2 = ( 1. R) by A3, A15, A33, Th30;

          hence thesis by A4, A18, A34, Th30;

        end;

        hence thesis by A16, A27, A19, A21, A5;

      end;

    end

    theorem :: GCD_1:44

    for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds Amp is multiplicative & (r1,r2) are_normalized_wrt Amp & (s1,s2) are_normalized_wrt Amp implies (( add1 (r1,r2,s1,s2,Amp)),( add2 (r1,r2,s1,s2,Amp))) are_normalized_wrt Amp

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: Amp is multiplicative and

       A2: (r1,r2) are_normalized_wrt Amp and

       A3: (s1,s2) are_normalized_wrt Amp;

      

       A4: r2 <> ( 0. R) by A2;

      r2 in Amp by A2;

      then

       A5: r2 = ( NF (r2,Amp)) by Def9;

      s2 in Amp by A3;

      then

       A6: s2 = ( NF (s2,Amp)) by Def9;

      

       A7: ( gcd (r1,r2,Amp)) = ( 1. R) by A2;

      then

       A8: (r1,r2) are_co-prime ;

      

       A9: ( gcd (s1,s2,Amp)) = ( 1. R) by A3;

      then

       A10: (s1,s2) are_co-prime ;

      

       A11: s2 <> ( 0. R) by A3;

      now

        per cases ;

          case

           A12: r1 = ( 0. R);

          then ( add2 (r1,r2,s1,s2,Amp)) = s2 by A5, A6, A8, A10, Def17;

          hence thesis by A3, A5, A6, A8, A10, A12, Def16;

        end;

          case

           A13: s1 = ( 0. R);

          then ( add2 (r1,r2,s1,s2,Amp)) = r2 by A5, A6, A8, A10, Def17;

          hence thesis by A2, A5, A6, A8, A10, A13, Def16;

        end;

          case

           A14: ( gcd (r2,s2,Amp)) = ( 1. R);

          then

           A15: ( add2 (r1,r2,s1,s2,Amp)) = (r2 * s2) by A5, A6, A8, A10, Def17;

          ( add1 (r1,r2,s1,s2,Amp)) = ((r1 * s2) + (r2 * s1)) by A5, A6, A8, A10, A14, Def16;

          

          then

           A16: ( gcd (( add1 (r1,r2,s1,s2,Amp)),( add2 (r1,r2,s1,s2,Amp)),Amp)) = ( gcd (((r1 * (s2 / ( 1. R))) + (s1 * r2)),(r2 * s2),Amp)) by A15, Th10

          .= ( gcd (((r1 * (s2 / ( 1. R))) + (s1 * (r2 / ( 1. R)))),(r2 * s2),Amp)) by Th10

          .= ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),(r2 * (s2 / ( gcd (r2,s2,Amp)))),Amp)) by A14, Th10

          .= ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) by A4, A7, A9, Th40

          .= ( 1. R) by A14, Th32;

          reconsider r2, s2 as Element of Amp by A2, A3;

          (r2 * s2) in Amp & (r2 * s2) <> ( 0. R) by A1, A4, A11, VECTSP_2:def 1;

          hence thesis by A15, A16;

        end;

          case

           A17: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          

           A18: ( 1. R) in Amp & ( 1. R) <> ( 0. R) by Th22;

          

           A19: ( add2 (r1,r2,s1,s2,Amp)) = ( 1. R) by A5, A6, A8, A10, A17, Def17;

          then ( gcd (( add1 (r1,r2,s1,s2,Amp)),( add2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by Th32;

          hence thesis by A19, A18;

        end;

          case r1 <> ( 0. R) & s1 <> ( 0. R) & ( gcd (r2,s2,Amp)) <> ( 1. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) <> ( 0. R);

          then

           A20: ( add1 (r1,r2,s1,s2,Amp)) = (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))) & ( add2 (r1,r2,s1,s2,Amp)) = ((r2 * (s2 / ( gcd (r2,s2,Amp)))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))) by A5, A6, A8, A10, Def16, Def17;

          ( gcd (r2,s2,Amp)) <> ( 0. R) by A4, Th33;

          then

           A21: ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) <> ( 0. R) by Th33;

          ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),(r2 * (s2 / ( gcd (r2,s2,Amp)))),Amp)) = ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) by A4, A7, A9, Th40;

          then

           A22: ( gcd ((((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))),((r2 * (s2 / ( gcd (r2,s2,Amp)))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))),Amp)) = ( 1. R) by A21, Th38;

          reconsider r2, s2 as Element of Amp by A2, A3;

          

           A23: ( gcd (r2,s2,Amp)) divides s2 by Def12;

          reconsider z2 = ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) as Element of Amp by Def12;

          

           A24: ( gcd (r2,s2,Amp)) <> ( 0. R) by A4, Th33;

          then

           A25: z2 <> ( 0. R) by Th33;

          ( gcd (r2,s2,Amp)) in Amp by Def12;

          then

          reconsider z3 = (s2 / ( gcd (r2,s2,Amp))) as Element of Amp by A1, A23, A24, Th27;

          (r2 * z3) in Amp by A1;

          then

          reconsider z1 = (r2 * (s2 / ( gcd (r2,s2,Amp)))) as Element of Amp;

          

           A26: (r2 * s2) <> ( 0. R) by A4, A11, VECTSP_2:def 1;

          

           A27: ( gcd (r2,s2,Amp)) divides (r2 * s2) by A23, Th7;

          then z1 = ((r2 * s2) / ( gcd (r2,s2,Amp))) by A23, A24, Th11;

          then

           A28: z1 <> ( 0. R) by A24, A26, A27, Th8;

          z2 divides ( gcd (r2,s2,Amp)) & ( gcd (r2,s2,Amp)) divides r2 by Def12;

          then

           A29: z2 divides r2 by Th2;

          then z2 divides z1 by Th7;

          then

           A30: (z1 / z2) <> ( 0. R) by A25, A28, Th8;

          (z1 / z2) in Amp by A1, A29, A25, Th7, Th27;

          hence thesis by A20, A22, A30;

        end;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:45

    for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds (r1,r2) are_normalized_wrt Amp & (s1,s2) are_normalized_wrt Amp implies (( add1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) = (( add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)))

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: (r1,r2) are_normalized_wrt Amp and

       A2: (s1,s2) are_normalized_wrt Amp;

      ( gcd (r1,r2,Amp)) = ( 1. R) by A1;

      then

       A3: (r1,r2) are_co-prime ;

      s2 in Amp by A2;

      then

       A4: s2 = ( NF (s2,Amp)) by Def9;

      ( gcd (s1,s2,Amp)) = ( 1. R) by A2;

      then

       A5: (s1,s2) are_co-prime ;

      r2 in Amp by A1;

      then

       A6: r2 = ( NF (r2,Amp)) by Def9;

      

       A7: r2 <> ( 0. R) by A1;

      now

        per cases ;

          case

           A8: r1 = ( 0. R);

          then

           A9: ( add1 (r1,r2,s1,s2,Amp)) = s1 by A3, A5, A6, A4, Def16;

          ( add2 (r1,r2,s1,s2,Amp)) = s2 by A3, A5, A6, A4, A8, Def17;

          

          then (( add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))) = (s2 * (( 0. R) + (s1 * r2))) by A8

          .= (s2 * (s1 * r2)) by RLVECT_1: 4

          .= (( add1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) by A9, GROUP_1:def 3;

          hence thesis;

        end;

          case

           A10: s1 = ( 0. R);

          then

           A11: ( add1 (r1,r2,s1,s2,Amp)) = r1 by A3, A5, A6, A4, Def16;

          ( add2 (r1,r2,s1,s2,Amp)) = r2 by A3, A5, A6, A4, A10, Def17;

          

          then (( add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))) = (r2 * ((r1 * s2) + ( 0. R))) by A10

          .= (r2 * (r1 * s2)) by RLVECT_1: 4

          .= (( add1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) by A11, GROUP_1:def 3;

          hence thesis;

        end;

          case

           A12: ( gcd (r2,s2,Amp)) = ( 1. R);

          then ( add2 (r1,r2,s1,s2,Amp)) = (r2 * s2) by A3, A5, A6, A4, Def17;

          hence thesis by A3, A5, A6, A4, A12, Def16;

        end;

          case

           A13: ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) = ( 0. R);

          

           A14: ((r1 * s2) + (s1 * r2)) = ( 0. R)

          proof

            

             A15: ( gcd (r2,s2,Amp)) divides r2 by Def12;

            then

             A16: ( gcd (r2,s2,Amp)) divides (s1 * r2) by Th7;

            

             A17: ( gcd (r2,s2,Amp)) divides s2 by Def12;

            then

            consider f be Element of R such that

             A18: (( gcd (r2,s2,Amp)) * f) = s2;

            

             A19: ( gcd (r2,s2,Amp)) <> ( 0. R) by A7, Th33;

            consider e be Element of R such that

             A20: (( gcd (r2,s2,Amp)) * e) = r2 by A15;

            (( gcd (r2,s2,Amp)) * ((e * s1) + (f * r1))) = ((( gcd (r2,s2,Amp)) * (e * s1)) + (( gcd (r2,s2,Amp)) * (f * r1))) by VECTSP_1:def 2

            .= (((( gcd (r2,s2,Amp)) * e) * s1) + (( gcd (r2,s2,Amp)) * (f * r1))) by GROUP_1:def 3

            .= ((r1 * s2) + (s1 * r2)) by A20, A18, GROUP_1:def 3;

            then

             A21: ( gcd (r2,s2,Amp)) divides ((r1 * s2) + (s1 * r2));

            

             A22: ( gcd (r2,s2,Amp)) divides (r1 * s2) by A17, Th7;

            

            then ( 0. R) = (((r1 * s2) / ( gcd (r2,s2,Amp))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) by A13, A19, A17, Th11

            .= (((r1 * s2) / ( gcd (r2,s2,Amp))) + ((s1 * r2) / ( gcd (r2,s2,Amp)))) by A19, A15, A16, Th11;

            then

             A23: ( 0. R) = (((r1 * s2) + (s1 * r2)) / ( gcd (r2,s2,Amp))) by A19, A22, A16, A21, Th12;

            ( 0. R) = (( 0. R) * ( gcd (r2,s2,Amp)))

            .= ((r1 * s2) + (s1 * r2)) by A19, A21, A23, Def4;

            hence thesis;

          end;

          ( add1 (r1,r2,s1,s2,Amp)) = ( 0. R) by A3, A5, A6, A4, A13, Def16;

          

          then (( add1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) = ( 0. R)

          .= (( add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))) by A14;

          hence thesis;

        end;

          case

           A24: r1 <> ( 0. R) & s1 <> ( 0. R) & ( gcd (r2,s2,Amp)) <> ( 1. R) & ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) <> ( 0. R);

          

           A25: ( gcd (r2,s2,Amp)) divides s2 by Def12;

          then

           A26: ( gcd (r2,s2,Amp)) divides (r1 * s2) by Th7;

          then

           A27: ( gcd (r2,s2,Amp)) divides ((r1 * s2) * r2) by Th7;

          then

           A28: ( gcd (r2,s2,Amp)) divides (((r1 * s2) * r2) * s2) by Th7;

          

           A29: ( add1 (r1,r2,s1,s2,Amp)) = (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))) by A3, A5, A6, A4, A24, Def16;

          

           A30: ( gcd (r2,s2,Amp)) divides r2 by Def12;

          then

           A31: ( gcd (r2,s2,Amp)) divides (s1 * r2) by Th7;

          ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides ( gcd (r2,s2,Amp)) by Def12;

          then ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides r2 by A30, Th2;

          then

           A32: ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides (r2 * (s2 / ( gcd (r2,s2,Amp)))) by Th7;

          then

           A33: ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides ((r2 * (s2 / ( gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2))) by Th7;

          

           A34: ( gcd (r2,s2,Amp)) divides ((s1 * r2) * r2) by A30, Th7;

          then

           A35: ( gcd (r2,s2,Amp)) divides (((s1 * r2) * r2) * s2) by Th7;

          

           A36: ( gcd (r2,s2,Amp)) divides (r2 * s2) by A30, Th7;

          then

           A37: ( gcd (r2,s2,Amp)) divides ((r2 * s2) * r1) by Th7;

          then

           A38: ( gcd (r2,s2,Amp)) divides (((r2 * s2) * r1) * s2) by Th7;

          

           A39: ( gcd (r2,s2,Amp)) divides ((r2 * s2) * s1) by A36, Th7;

          then

           A40: ( gcd (r2,s2,Amp)) divides (((r2 * s2) * s1) * r2) by Th7;

          

           A41: ( add2 (r1,r2,s1,s2,Amp)) = ((r2 * (s2 / ( gcd (r2,s2,Amp)))) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))) by A3, A5, A6, A4, A24, Def17;

          

           A42: ( gcd (r2,s2,Amp)) <> ( 0. R) by A7, Th33;

          then

           A43: ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) <> ( 0. R) by Th33;

          

           A44: ((r2 * (s2 / ( gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2))) = (((r2 * (s2 / ( gcd (r2,s2,Amp)))) * (r1 * s2)) + ((r2 * (s2 / ( gcd (r2,s2,Amp)))) * (s1 * r2))) by VECTSP_1:def 2

          .= ((((r2 * (s2 / ( gcd (r2,s2,Amp)))) * r1) * s2) + ((r2 * (s2 / ( gcd (r2,s2,Amp)))) * (s1 * r2))) by GROUP_1:def 3

          .= ((((r2 * (s2 / ( gcd (r2,s2,Amp)))) * r1) * s2) + (((r2 * (s2 / ( gcd (r2,s2,Amp)))) * s1) * r2)) by GROUP_1:def 3

          .= (((((r2 * s2) / ( gcd (r2,s2,Amp))) * r1) * s2) + (((r2 * (s2 / ( gcd (r2,s2,Amp)))) * s1) * r2)) by A42, A25, A36, Th11

          .= (((((r2 * s2) / ( gcd (r2,s2,Amp))) * r1) * s2) + ((((r2 * s2) / ( gcd (r2,s2,Amp))) * s1) * r2)) by A42, A25, A36, Th11

          .= (((((r2 * s2) * r1) / ( gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) / ( gcd (r2,s2,Amp))) * s1) * r2)) by A42, A36, A37, Th11

          .= (((((r2 * s2) * r1) / ( gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) * s1) / ( gcd (r2,s2,Amp))) * r2)) by A42, A36, A39, Th11

          .= (((((r2 * s2) * r1) * s2) / ( gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) / ( gcd (r2,s2,Amp))) * r2)) by A42, A37, A38, Th11

          .= ((((r1 * (s2 * r2)) * s2) / ( gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / ( gcd (r2,s2,Amp)))) by A42, A39, A40, Th11

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / ( gcd (r2,s2,Amp)))) by GROUP_1:def 3

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((s1 * ((r2 * s2) * r2)) / ( gcd (r2,s2,Amp)))) by GROUP_1:def 3

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((s1 * ((r2 * r2) * s2)) / ( gcd (r2,s2,Amp)))) by GROUP_1:def 3

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + (((s1 * (r2 * r2)) * s2) / ( gcd (r2,s2,Amp)))) by GROUP_1:def 3

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / ( gcd (r2,s2,Amp)))) by GROUP_1:def 3;

          

           A45: (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) * (r2 * s2)) = (((r1 * (s2 / ( gcd (r2,s2,Amp)))) * (r2 * s2)) + ((s1 * (r2 / ( gcd (r2,s2,Amp)))) * (r2 * s2))) by VECTSP_1:def 7

          .= ((((r1 * s2) / ( gcd (r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2 / ( gcd (r2,s2,Amp)))) * (r2 * s2))) by A42, A25, A26, Th11

          .= ((((r1 * s2) / ( gcd (r2,s2,Amp))) * (r2 * s2)) + (((s1 * r2) / ( gcd (r2,s2,Amp))) * (r2 * s2))) by A42, A30, A31, Th11

          .= (((((r1 * s2) / ( gcd (r2,s2,Amp))) * r2) * s2) + (((s1 * r2) / ( gcd (r2,s2,Amp))) * (r2 * s2))) by GROUP_1:def 3

          .= (((((r1 * s2) / ( gcd (r2,s2,Amp))) * r2) * s2) + ((((s1 * r2) / ( gcd (r2,s2,Amp))) * r2) * s2)) by GROUP_1:def 3

          .= (((((r1 * s2) * r2) / ( gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) / ( gcd (r2,s2,Amp))) * r2) * s2)) by A42, A26, A27, Th11

          .= (((((r1 * s2) * r2) / ( gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) * r2) / ( gcd (r2,s2,Amp))) * s2)) by A42, A31, A34, Th11

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) / ( gcd (r2,s2,Amp))) * s2)) by A42, A27, A28, Th11

          .= (((((r1 * s2) * r2) * s2) / ( gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / ( gcd (r2,s2,Amp)))) by A42, A34, A35, Th11;

          

           A46: ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides ((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) by Def12;

          then ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp)) divides (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) * (r2 * s2)) by Th7;

          

          then (( add1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) = ((((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))) * (r2 * s2)) / ( gcd (((r1 * (s2 / ( gcd (r2,s2,Amp)))) + (s1 * (r2 / ( gcd (r2,s2,Amp))))),( gcd (r2,s2,Amp)),Amp))) by A29, A43, A46, Th11

          .= (( add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))) by A41, A45, A44, A43, A32, A33, Th11;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    definition

      let R be gcdDomain;

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      :: GCD_1:def18

      func mult1 (r1,r2,s1,s2,Amp) -> Element of R equals

      : Def18: ( 0. R) if r1 = ( 0. R) or s1 = ( 0. R),

(r1 * s1) if r2 = ( 1. R) & s2 = ( 1. R),

((r1 * s1) / ( gcd (r1,s2,Amp))) if s2 <> ( 0. R) & r2 = ( 1. R),

((r1 * s1) / ( gcd (s1,r2,Amp))) if r2 <> ( 0. R) & s2 = ( 1. R)

      otherwise ((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp))));

      coherence ;

      consistency

      proof

        

         A1: (r1 = ( 0. R) or s1 = ( 0. R)) & r2 <> ( 0. R) & s2 = ( 1. R) implies for z be Element of R holds z = ( 0. R) iff z = ((r1 * s1) / ( gcd (s1,r2,Amp)))

        proof

          set d = ((r1 * s1) / ( gcd (s1,r2,Amp)));

          assume that

           A2: r1 = ( 0. R) or s1 = ( 0. R) and

           A3: r2 <> ( 0. R) and s2 = ( 1. R);

          

           A4: ( gcd (s1,r2,Amp)) <> ( 0. R) by A3, Th33;

          let z be Element of R;

          

           A5: (r1 * s1) = ( 0. R)

          proof

            now

              per cases by A2;

                case r1 = ( 0. R);

                hence thesis;

              end;

                case s1 = ( 0. R);

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          ( gcd (s1,r2,Amp)) divides s1 by Def12;

          then ( gcd (s1,r2,Amp)) divides (r1 * s1) by Th7;

          then (d * ( gcd (s1,r2,Amp))) = ( 0. R) by A5, A4, Def4;

          hence thesis by A4, VECTSP_2:def 1;

        end;

        

         A6: (r1 = ( 0. R) or s1 = ( 0. R)) & s2 <> ( 0. R) & r2 = ( 1. R) implies for z be Element of R holds z = ( 0. R) iff z = ((r1 * s1) / ( gcd (r1,s2,Amp)))

        proof

          set d = ((r1 * s1) / ( gcd (r1,s2,Amp)));

          assume that

           A7: r1 = ( 0. R) or s1 = ( 0. R) and

           A8: s2 <> ( 0. R) and r2 = ( 1. R);

          

           A9: ( gcd (r1,s2,Amp)) <> ( 0. R) by A8, Th33;

          let z be Element of R;

          

           A10: (r1 * s1) = ( 0. R)

          proof

            now

              per cases by A7;

                case r1 = ( 0. R);

                hence thesis;

              end;

                case s1 = ( 0. R);

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          ( gcd (r1,s2,Amp)) divides r1 by Def12;

          then ( gcd (r1,s2,Amp)) divides (r1 * s1) by Th7;

          then (d * ( gcd (r1,s2,Amp))) = ( 0. R) by A10, A9, Def4;

          hence thesis by A9, VECTSP_2:def 1;

        end;

        

         A11: r2 = ( 1. R) & s2 = ( 1. R) & r2 <> ( 0. R) & s2 = ( 1. R) implies for z be Element of R holds z = (r1 * s1) iff z = ((r1 * s1) / ( gcd (s1,r2,Amp)))

        proof

          assume that

           A12: r2 = ( 1. R) and s2 = ( 1. R) and r2 <> ( 0. R) and s2 = ( 1. R);

          ( gcd (s1,r2,Amp)) = ( 1. R) by A12, Th32;

          hence thesis by Th10;

        end;

        r2 = ( 1. R) & s2 = ( 1. R) & s2 <> ( 0. R) & r2 = ( 1. R) implies for z be Element of R holds z = (r1 * s1) iff z = ((r1 * s1) / ( gcd (r1,s2,Amp)))

        proof

          assume that r2 = ( 1. R) and

           A13: s2 = ( 1. R) and s2 <> ( 0. R) and r2 = ( 1. R);

          ( gcd (r1,s2,Amp)) = ( 1. R) by A13, Th32;

          hence thesis by Th10;

        end;

        hence thesis by A6, A1, A11;

      end;

    end

    definition

      let R be gcdDomain;

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: (r1,r2) are_co-prime and

       A2: (s1,s2) are_co-prime and

       A3: r2 = ( NF (r2,Amp)) and

       A4: s2 = ( NF (s2,Amp));

      :: GCD_1:def19

      func mult2 (r1,r2,s1,s2,Amp) -> Element of R equals

      : Def19: ( 1. R) if r1 = ( 0. R) or s1 = ( 0. R),

( 1. R) if r2 = ( 1. R) & s2 = ( 1. R),

(s2 / ( gcd (r1,s2,Amp))) if s2 <> ( 0. R) & r2 = ( 1. R),

(r2 / ( gcd (s1,r2,Amp))) if r2 <> ( 0. R) & s2 = ( 1. R)

      otherwise ((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp))));

      coherence ;

      consistency

      proof

        

         A5: ( gcd (s1,s2,Amp)) = ( 1. R) by A2, Th43;

        

         A6: (r1 = ( 0. R) or s1 = ( 0. R)) & s2 <> ( 0. R) & r2 = ( 1. R) implies for z be Element of R holds z = ( 1. R) iff z = (s2 / ( gcd (r1,s2,Amp)))

        proof

          assume that

           A7: r1 = ( 0. R) or s1 = ( 0. R) and

           A8: s2 <> ( 0. R) and r2 = ( 1. R);

          now

            per cases by A7;

              case r1 = ( 0. R);

              then ( gcd (r1,s2,Amp)) = s2 by A4, Th30;

              hence thesis by A8, Th9;

            end;

              case

               A9: s1 = ( 0. R);

              

               A10: ( 1. R) <> ( 0. R);

              

               A11: ( 1. R) = s2 by A4, A5, A9, Th30;

              then ( gcd (r1,s2,Amp)) = ( 1. R) by Th32;

              hence thesis by A11, A10, Th9;

            end;

          end;

          hence thesis;

        end;

        

         A12: ( gcd (r1,r2,Amp)) = ( 1. R) by A1, Th43;

        

         A13: (r1 = ( 0. R) or s1 = ( 0. R)) & r2 <> ( 0. R) & s2 = ( 1. R) implies for z be Element of R holds z = ( 1. R) iff z = (r2 / ( gcd (s1,r2,Amp)))

        proof

          assume that

           A14: r1 = ( 0. R) or s1 = ( 0. R) and

           A15: r2 <> ( 0. R) and s2 = ( 1. R);

          now

            per cases by A14;

              case s1 = ( 0. R);

              then ( gcd (s1,r2,Amp)) = r2 by A3, Th30;

              hence thesis by A15, Th9;

            end;

              case

               A16: r1 = ( 0. R);

              

               A17: ( 1. R) <> ( 0. R);

              

               A18: ( 1. R) = r2 by A3, A12, A16, Th30;

              then ( gcd (s1,r2,Amp)) = ( 1. R) by Th32;

              hence thesis by A18, A17, Th9;

            end;

          end;

          hence thesis;

        end;

        

         A19: r2 = ( 1. R) & s2 = ( 1. R) & r2 <> ( 0. R) & s2 = ( 1. R) implies for z be Element of R holds z = ( 1. R) iff z = (r2 / ( gcd (s1,r2,Amp)))

        proof

          assume that

           A20: r2 = ( 1. R) and s2 = ( 1. R) and

           A21: r2 <> ( 0. R) and s2 = ( 1. R);

          ( gcd (s1,r2,Amp)) = ( 1. R) by A20, Th32;

          hence thesis by A20, A21, Th9;

        end;

        r2 = ( 1. R) & s2 = ( 1. R) & s2 <> ( 0. R) & r2 = ( 1. R) implies for z be Element of R holds z = ( 1. R) iff z = (s2 / ( gcd (r1,s2,Amp)))

        proof

          assume that r2 = ( 1. R) and

           A22: s2 = ( 1. R) and

           A23: s2 <> ( 0. R) and r2 = ( 1. R);

          ( gcd (r1,s2,Amp)) = ( 1. R) by A22, Th32;

          hence thesis by A22, A23, Th9;

        end;

        hence thesis by A6, A13, A19;

      end;

    end

    theorem :: GCD_1:46

    for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds Amp is multiplicative & (r1,r2) are_normalized_wrt Amp & (s1,s2) are_normalized_wrt Amp implies (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp))) are_normalized_wrt Amp

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: Amp is multiplicative and

       A2: (r1,r2) are_normalized_wrt Amp and

       A3: (s1,s2) are_normalized_wrt Amp;

      

       A4: ( gcd (r1,r2,Amp)) = ( 1. R) by A2;

      then

       A5: (r1,r2) are_co-prime ;

      s2 in Amp by A3;

      then

       A6: s2 = ( NF (s2,Amp)) by Def9;

      r2 in Amp by A2;

      then

       A7: r2 = ( NF (r2,Amp)) by Def9;

      

       A8: r2 <> ( 0. R) by A2;

      then

       A9: ( gcd (s1,r2,Amp)) <> ( 0. R) by Th33;

      

       A10: ( gcd (s1,s2,Amp)) = ( 1. R) by A3;

      then

       A11: (s1,s2) are_co-prime ;

      

       A12: s2 <> ( 0. R) by A3;

      then

       A13: ( gcd (r1,s2,Amp)) <> ( 0. R) by Th33;

      now

        per cases ;

          case

           A14: r1 = ( 0. R) or s1 = ( 0. R);

          

           A15: ( 1. R) in Amp & ( 1. R) <> ( 0. R) by Th22;

          

           A16: ( mult2 (r1,r2,s1,s2,Amp)) = ( 1. R) by A5, A11, A7, A6, A14, Def19;

          then ( gcd (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by Th32;

          hence thesis by A16, A15;

        end;

          case

           A17: r2 = ( 1. R) & s2 = ( 1. R);

          

           A18: ( 1. R) in Amp & ( 1. R) <> ( 0. R) by Th22;

          

           A19: ( mult2 (r1,r2,s1,s2,Amp)) = ( 1. R) by A5, A11, A7, A17, Def19;

          then ( gcd (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by Th32;

          hence thesis by A19, A18;

        end;

          case

           A20: s2 <> ( 0. R) & r2 = ( 1. R);

          then

           A21: ( gcd (s1,r2,Amp)) = ( 1. R) by Th32;

          then (r2 / ( gcd (s1,r2,Amp))) = ( 1. R) by A20, Th9;

          then

           A22: (s2 / ( gcd (r1,s2,Amp))) = ((s2 / ( gcd (r1,s2,Amp))) * (r2 / ( gcd (s1,r2,Amp))));

          

           A23: ( gcd (r1,s2,Amp)) divides r1 by Def12;

          then ( gcd (r1,s2,Amp)) divides (r1 * s1) by Th7;

          

          then

           A24: ((r1 * s1) / ( gcd (r1,s2,Amp))) = ((r1 / ( gcd (r1,s2,Amp))) * s1) by A13, A23, Th11

          .= ((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp)))) by A21, Th10;

          

           A25: ( mult2 (r1,r2,s1,s2,Amp)) = (s2 / ( gcd (r1,s2,Amp))) by A5, A11, A7, A6, A20, Def19;

          reconsider zz = ( gcd (r1,s2,Amp)) as Element of Amp by Def12;

          

           A26: ( gcd (r1,s2,Amp)) divides s2 & ( gcd (r1,s2,Amp)) <> ( 0. R) by A12, Def12, Th33;

          then

           A27: (s2 / ( gcd (r1,s2,Amp))) <> ( 0. R) by A12, Th8;

          ( mult1 (r1,r2,s1,s2,Amp)) = ((r1 * s1) / ( gcd (r1,s2,Amp))) by A20, Def18;

          then

           A28: ( gcd (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by A4, A10, A8, A12, A25, A24, A22, Th41;

          reconsider s2 as Element of Amp by A3;

          (s2 / zz) in Amp by A1, A26, Th27;

          hence thesis by A25, A28, A27;

        end;

          case

           A29: r2 <> ( 0. R) & s2 = ( 1. R);

          then

           A30: ( gcd (r1,s2,Amp)) = ( 1. R) by Th32;

          then (s2 / ( gcd (r1,s2,Amp))) = ( 1. R) by A29, Th9;

          then

           A31: (r2 / ( gcd (s1,r2,Amp))) = ((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp))));

          

           A32: ( gcd (s1,r2,Amp)) divides s1 by Def12;

          then ( gcd (s1,r2,Amp)) divides (r1 * s1) by Th7;

          

          then

           A33: ((r1 * s1) / ( gcd (s1,r2,Amp))) = (r1 * (s1 / ( gcd (s1,r2,Amp)))) by A9, A32, Th11

          .= ((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp)))) by A30, Th10;

          

           A34: ( mult2 (r1,r2,s1,s2,Amp)) = (r2 / ( gcd (s1,r2,Amp))) by A5, A11, A7, A6, A29, Def19;

          reconsider zz = ( gcd (s1,r2,Amp)) as Element of Amp by Def12;

          

           A35: ( gcd (s1,r2,Amp)) divides r2 & ( gcd (s1,r2,Amp)) <> ( 0. R) by A8, Def12, Th33;

          then

           A36: (r2 / ( gcd (s1,r2,Amp))) <> ( 0. R) by A8, Th8;

          ( mult1 (r1,r2,s1,s2,Amp)) = ((r1 * s1) / ( gcd (s1,r2,Amp))) by A29, Def18;

          then

           A37: ( gcd (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by A4, A10, A8, A12, A34, A33, A31, Th41;

          reconsider r2 as Element of Amp by A2;

          (r2 / zz) in Amp by A1, A35, Th27;

          hence thesis by A34, A37, A36;

        end;

          case

           A38: not (r1 = ( 0. R) or s1 = ( 0. R)) & not (r2 = ( 1. R) & s2 = ( 1. R)) & not (s2 <> ( 0. R) & r2 = ( 1. R)) & not (r2 <> ( 0. R) & s2 = ( 1. R));

          reconsider z2 = ( gcd (s1,r2,Amp)) as Element of Amp by Def12;

          reconsider z1 = ( gcd (r1,s2,Amp)) as Element of Amp by Def12;

          

           A39: ( gcd (r1,s2,Amp)) divides s2 & ( gcd (r1,s2,Amp)) <> ( 0. R) by A12, Def12, Th33;

          then

           A40: (s2 / ( gcd (r1,s2,Amp))) <> ( 0. R) by A12, Th8;

          

           A41: ( mult2 (r1,r2,s1,s2,Amp)) = ((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp)))) by A5, A11, A7, A6, A38, Def19;

          ( mult1 (r1,r2,s1,s2,Amp)) = ((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp)))) by A38, Def18;

          then

           A42: ( gcd (( mult1 (r1,r2,s1,s2,Amp)),( mult2 (r1,r2,s1,s2,Amp)),Amp)) = ( 1. R) by A4, A10, A8, A12, A41, Th41;

          

           A43: ( gcd (s1,r2,Amp)) divides r2 & ( gcd (s1,r2,Amp)) <> ( 0. R) by A8, Def12, Th33;

          then

           A44: (r2 / ( gcd (s1,r2,Amp))) <> ( 0. R) by A8, Th8;

          reconsider s2 as Element of Amp by A3;

          reconsider u = (s2 / z1) as Element of Amp by A1, A39, Th27;

          reconsider r2 as Element of Amp by A2;

          reconsider v = (r2 / z2) as Element of Amp by A1, A43, Th27;

          

           A45: (v * u) <> ( 0. R) by A40, A44, VECTSP_2:def 1;

          (v * u) in Amp by A1;

          hence thesis by A41, A42, A45;

        end;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:47

    for Amp be AmpleSet of R holds for r1,r2,s1,s2 be Element of R holds (r1,r2) are_normalized_wrt Amp & (s1,s2) are_normalized_wrt Amp implies (( mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2)) = (( mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1))

    proof

      let Amp be AmpleSet of R;

      let r1,r2,s1,s2 be Element of R;

      assume that

       A1: (r1,r2) are_normalized_wrt Amp and

       A2: (s1,s2) are_normalized_wrt Amp;

      ( gcd (r1,r2,Amp)) = ( 1. R) by A1;

      then

       A3: (r1,r2) are_co-prime ;

      s2 <> ( 0. R) by A2;

      then

       A4: ( gcd (r1,s2,Amp)) <> ( 0. R) by Th33;

      r2 in Amp by A1;

      then

       A5: r2 = ( NF (r2,Amp)) by Def9;

      ( gcd (s1,s2,Amp)) = ( 1. R) by A2;

      then

       A6: (s1,s2) are_co-prime ;

      r2 <> ( 0. R) by A1;

      then

       A7: ( gcd (s1,r2,Amp)) <> ( 0. R) by Th33;

      s2 in Amp by A2;

      then

       A8: s2 = ( NF (s2,Amp)) by Def9;

      now

        per cases ;

          case

           A9: r1 = ( 0. R) or s1 = ( 0. R);

          then

           A10: ( mult1 (r1,r2,s1,s2,Amp)) = ( 0. R) by Def18;

          now

            per cases by A9;

              case r1 = ( 0. R);

              

              then (( mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)) = (( mult2 (r1,r2,s1,s2,Amp)) * ( 0. R))

              .= ( 0. R);

              hence thesis by A10;

            end;

              case s1 = ( 0. R);

              

              then (( mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)) = (( mult2 (r1,r2,s1,s2,Amp)) * ( 0. R))

              .= ( 0. R);

              hence thesis by A10;

            end;

          end;

          hence thesis;

        end;

          case

           A11: r2 = ( 1. R) & s2 = ( 1. R);

          then ( mult1 (r1,r2,s1,s2,Amp)) = (r1 * s1) & ( mult2 (r1,r2,s1,s2,Amp)) = ( 1. R) by A3, A6, A5, Def18, Def19;

          hence thesis by A11;

        end;

          case

           A12: s2 <> ( 0. R) & r2 = ( 1. R);

          ( gcd (r1,s2,Amp)) divides r1 by Def12;

          then

           A13: ( gcd (r1,s2,Amp)) divides (r1 * s1) by Th7;

          then

           A14: ( gcd (r1,s2,Amp)) divides ((r1 * s1) * s2) by Th7;

          

           A15: (((r1 * s1) / ( gcd (r1,s2,Amp))) * (r2 * s2)) = (((r1 * s1) / ( gcd (r1,s2,Amp))) * s2) by A12

          .= (((r1 * s1) * s2) / ( gcd (r1,s2,Amp))) by A4, A13, A14, Th11;

          

           A16: ( mult2 (r1,r2,s1,s2,Amp)) = (s2 / ( gcd (r1,s2,Amp))) by A3, A6, A5, A8, A12, Def19;

          

           A17: ( gcd (r1,s2,Amp)) divides s2 by Def12;

          then

           A18: ( gcd (r1,s2,Amp)) divides (s2 * r1) by Th7;

          then

           A19: ( gcd (r1,s2,Amp)) divides ((s2 * r1) * s1) by Th7;

          ((s2 / ( gcd (r1,s2,Amp))) * (r1 * s1)) = (((s2 / ( gcd (r1,s2,Amp))) * r1) * s1) by GROUP_1:def 3

          .= (((s2 * r1) / ( gcd (r1,s2,Amp))) * s1) by A4, A17, A18, Th11

          .= (((s2 * r1) * s1) / ( gcd (r1,s2,Amp))) by A4, A18, A19, Th11

          .= (((r1 * s1) * s2) / ( gcd (r1,s2,Amp))) by GROUP_1:def 3;

          hence thesis by A12, A16, A15, Def18;

        end;

          case

           A20: r2 <> ( 0. R) & s2 = ( 1. R);

          ( gcd (s1,r2,Amp)) divides s1 by Def12;

          then

           A21: ( gcd (s1,r2,Amp)) divides (s1 * r1) by Th7;

          then

           A22: ( gcd (s1,r2,Amp)) divides ((s1 * r1) * r2) by Th7;

          

           A23: (((r1 * s1) / ( gcd (s1,r2,Amp))) * (r2 * s2)) = (((r1 * s1) / ( gcd (s1,r2,Amp))) * r2) by A20

          .= (((r1 * s1) * r2) / ( gcd (s1,r2,Amp))) by A7, A21, A22, Th11;

          

           A24: ( mult2 (r1,r2,s1,s2,Amp)) = (r2 / ( gcd (s1,r2,Amp))) by A3, A6, A5, A8, A20, Def19;

          

           A25: ( gcd (s1,r2,Amp)) divides r2 by Def12;

          then

           A26: ( gcd (s1,r2,Amp)) divides (r2 * r1) by Th7;

          then

           A27: ( gcd (s1,r2,Amp)) divides ((r2 * r1) * s1) by Th7;

          ((r2 / ( gcd (s1,r2,Amp))) * (r1 * s1)) = (((r2 / ( gcd (s1,r2,Amp))) * r1) * s1) by GROUP_1:def 3

          .= (((r2 * r1) / ( gcd (s1,r2,Amp))) * s1) by A7, A25, A26, Th11

          .= (((r2 * r1) * s1) / ( gcd (s1,r2,Amp))) by A7, A26, A27, Th11

          .= (((r1 * s1) * r2) / ( gcd (s1,r2,Amp))) by GROUP_1:def 3;

          hence thesis by A20, A24, A23, Def18;

        end;

          case

           A28: not (r1 = ( 0. R) or s1 = ( 0. R)) & not (r2 = ( 1. R) & s2 = ( 1. R)) & not (s2 <> ( 0. R) & r2 = ( 1. R)) & not (r2 <> ( 0. R) & s2 = ( 1. R));

          

           A29: ( gcd (s1,r2,Amp)) divides r2 & ( gcd (r1,s2,Amp)) divides s2 by Def12;

          then

           A30: (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp))) divides (r2 * s2) by Th3;

          then

           A31: (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp))) divides ((r2 * s2) * r1) by Th7;

          then

           A32: (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp))) divides (((r2 * s2) * r1) * s1) by Th7;

          

           A33: ( gcd (r1,s2,Amp)) divides r1 & ( gcd (s1,r2,Amp)) divides s1 by Def12;

          then

           A34: (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp))) divides (r1 * s1) by Th3;

          then

           A35: (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp))) divides ((r1 * s1) * r2) by Th7;

          then

           A36: (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp))) divides (((r1 * s1) * r2) * s2) by Th7;

          

           A37: ( mult2 (r1,r2,s1,s2,Amp)) = ((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp)))) by A3, A6, A5, A8, A28, Def19;

          

           A38: (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp))) <> ( 0. R) by A4, A7, VECTSP_2:def 1;

          

           A39: (((r2 / ( gcd (s1,r2,Amp))) * (s2 / ( gcd (r1,s2,Amp)))) * (r1 * s1)) = (((r2 * s2) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) * (r1 * s1)) by A4, A7, A29, Th14

          .= ((((r2 * s2) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) * r1) * s1) by GROUP_1:def 3

          .= ((((r2 * s2) * r1) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) * s1) by A38, A30, A31, Th11

          .= ((((r2 * s2) * r1) * s1) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) by A38, A31, A32, Th11

          .= ((r1 * ((r2 * s2) * s1)) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) by GROUP_1:def 3

          .= ((r1 * ((s1 * r2) * s2)) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) by GROUP_1:def 3

          .= (((r1 * (s1 * r2)) * s2) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) by GROUP_1:def 3

          .= ((((r1 * s1) * r2) * s2) / (( gcd (s1,r2,Amp)) * ( gcd (r1,s2,Amp)))) by GROUP_1:def 3;

          (((r1 / ( gcd (r1,s2,Amp))) * (s1 / ( gcd (s1,r2,Amp)))) * (r2 * s2)) = (((r1 * s1) / (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp)))) * (r2 * s2)) by A4, A7, A33, Th14

          .= ((((r1 * s1) / (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp)))) * r2) * s2) by GROUP_1:def 3

          .= ((((r1 * s1) * r2) / (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp)))) * s2) by A34, A35, A38, Th11

          .= ((((r1 * s1) * r2) * s2) / (( gcd (r1,s2,Amp)) * ( gcd (s1,r2,Amp)))) by A35, A36, A38, Th11;

          hence thesis by A28, A37, A39, Def18;

        end;

      end;

      hence thesis;

    end;

    theorem :: GCD_1:48

    for F be add-associative right_zeroed right_complementable Abelian distributive non empty doubleLoopStr, x,y be Element of F holds (( - x) * y) = ( - (x * y)) & (x * ( - y)) = ( - (x * y)) by VECTSP_1: 8, VECTSP_1: 9;

    theorem :: GCD_1:49

    for F be almost_left_invertible commutative Ring holds for a,b be Element of F st a <> ( 0. F) & b <> ( 0. F) holds ((a " ) * (b " )) = ((b * a) " )

    proof

      let F be almost_left_invertible commutative Ring;

      let a,b be Element of F such that

       A1: a <> ( 0. F) and

       A2: b <> ( 0. F);

      

       A3: ((b * a) * ((a " ) * (b " ))) = (((b * a) * (a " )) * (b " )) by GROUP_1:def 3

      .= ((b * (a * (a " ))) * (b " )) by GROUP_1:def 3

      .= ((b * ( 1_ F)) * (b " )) by A1, VECTSP_1:def 10

      .= (b * (b " ))

      .= ( 1_ F) by A2, VECTSP_1:def 10;

      (b * a) <> ( 0. F) by A1, A2, VECTSP_1: 12;

      hence thesis by A3, VECTSP_1:def 10;

    end;