int_6.miz



    begin

    

     Lm1: for f be INT -valued FinSequence holds f is FinSequence of INT

    proof

      let f be INT -valued FinSequence;

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

      hence thesis by FINSEQ_1:def 4;

    end;

    registration

      let f be complex-valued FinSequence, n be Nat;

      cluster (f | n) -> complex-valued;

      coherence ;

    end

    registration

      let f be INT -valued FinSequence, n be Nat;

      cluster (f | n) -> INT -valued;

      coherence ;

    end

    registration

      let f be INT -valued FinSequence, n be Nat;

      cluster (f /^ n) -> INT -valued;

      coherence

      proof

        per cases ;

          suppose n > ( len f);

          hence thesis by RFINSEQ:def 1;

        end;

          suppose

           A1: n <= ( len f);

          now

            reconsider f9 = f as FinSequence of INT by Lm1;

            let u be object;

            reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

            

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

            assume u in ( rng (f /^ n));

            then

            consider x be object such that

             A3: x in ( dom (f /^ n)) and

             A4: ((f /^ n) . x) = u by FUNCT_1:def 3;

            reconsider x as Element of NAT by A3;

            (x + n9) in ( dom f9) by A3, FINSEQ_5: 26;

            then

             A5: (f . (x + n)) in ( rng f) by FUNCT_1:def 3;

            ((f /^ n) . x) = (f . (x + n)) by A1, A3, RFINSEQ:def 1;

            hence u in INT by A4, A5, A2;

          end;

          then ( rng (f /^ n)) c= INT by TARSKI:def 3;

          hence thesis by RELAT_1:def 19;

        end;

      end;

    end

    registration

      let i be Integer;

      cluster <*i*> -> INT -valued;

      coherence

      proof

        for u be object st u in {i} holds u in INT by INT_1:def 2;

        then

         A1: {i} c= INT by TARSKI:def 3;

        ( rng <*i*>) = {i} by FINSEQ_1: 39;

        hence thesis by A1, RELAT_1:def 19;

      end;

    end

    registration

      let f,g be INT -valued FinSequence;

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

      coherence

      proof

        now

          let u be object;

          

           A1: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

          assume

           A2: u in ( rng (f ^ g));

          now

            per cases by A2, A1, XBOOLE_0:def 3;

              case

               A3: u in ( rng f);

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

              hence u in INT by A3;

            end;

              case

               A4: u in ( rng g);

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

              hence u in INT by A4;

            end;

          end;

          hence u in INT ;

        end;

        then ( rng (f ^ g)) c= INT by TARSKI:def 3;

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: INT_6:1

    

     Th1: for f1,f2 be complex-valued FinSequence holds ( len (f1 + f2)) = ( min (( len f1),( len f2)))

    proof

      let f1,f2 be complex-valued FinSequence;

      set g = (f1 + f2);

      consider n1 be Nat such that

       A1: ( dom f1) = ( Seg n1) by FINSEQ_1:def 2;

      n1 in NAT by ORDINAL1:def 12;

      then

       A2: ( len f1) = n1 by A1, FINSEQ_1:def 3;

      consider n2 be Nat such that

       A3: ( dom f2) = ( Seg n2) by FINSEQ_1:def 2;

      n2 in NAT by ORDINAL1:def 12;

      then

       A4: ( len f2) = n2 by A3, FINSEQ_1:def 3;

      

       A5: ( dom g) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

      now

        per cases ;

          case

           A6: n1 <= n2;

          then ( dom f1) c= ( dom f2) by A1, A3, FINSEQ_1: 5;

          then

           A7: ( dom g) = ( Seg n1) by A1, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n1 by A6, XXREAL_0:def 9;

          hence thesis by A2, A4, A7, FINSEQ_1:def 3;

        end;

          case

           A8: n2 <= n1;

          then ( dom f2) c= ( dom f1) by A1, A3, FINSEQ_1: 5;

          then

           A9: ( dom g) = ( Seg n2) by A3, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n2 by A8, XXREAL_0:def 9;

          hence thesis by A2, A4, A9, FINSEQ_1:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: INT_6:2

    

     Th2: for f1,f2 be complex-valued FinSequence holds ( len (f1 - f2)) = ( min (( len f1),( len f2)))

    proof

      let f1,f2 be complex-valued FinSequence;

      set g = (f1 - f2);

      consider n1 be Nat such that

       A1: ( dom f1) = ( Seg n1) by FINSEQ_1:def 2;

      n1 in NAT by ORDINAL1:def 12;

      then

       A2: ( len f1) = n1 by A1, FINSEQ_1:def 3;

      consider n2 be Nat such that

       A3: ( dom f2) = ( Seg n2) by FINSEQ_1:def 2;

      n2 in NAT by ORDINAL1:def 12;

      then

       A4: ( len f2) = n2 by A3, FINSEQ_1:def 3;

      

       A5: ( dom g) = (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

      now

        per cases ;

          case

           A6: n1 <= n2;

          then ( dom f1) c= ( dom f2) by A1, A3, FINSEQ_1: 5;

          then

           A7: ( dom g) = ( Seg n1) by A1, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n1 by A6, XXREAL_0:def 9;

          hence thesis by A2, A4, A7, FINSEQ_1:def 3;

        end;

          case

           A8: n2 <= n1;

          then ( dom f2) c= ( dom f1) by A1, A3, FINSEQ_1: 5;

          then

           A9: ( dom g) = ( Seg n2) by A3, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n2 by A8, XXREAL_0:def 9;

          hence thesis by A2, A4, A9, FINSEQ_1:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: INT_6:3

    

     Th3: for f1,f2 be complex-valued FinSequence holds ( len (f1 (#) f2)) = ( min (( len f1),( len f2)))

    proof

      let f1,f2 be complex-valued FinSequence;

      set g = (f1 (#) f2);

      consider n1 be Nat such that

       A1: ( dom f1) = ( Seg n1) by FINSEQ_1:def 2;

      n1 in NAT by ORDINAL1:def 12;

      then

       A2: ( len f1) = n1 by A1, FINSEQ_1:def 3;

      consider n2 be Nat such that

       A3: ( dom f2) = ( Seg n2) by FINSEQ_1:def 2;

      n2 in NAT by ORDINAL1:def 12;

      then

       A4: ( len f2) = n2 by A3, FINSEQ_1:def 3;

      

       A5: ( dom g) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

      now

        per cases ;

          case

           A6: n1 <= n2;

          then ( dom f1) c= ( dom f2) by A1, A3, FINSEQ_1: 5;

          then

           A7: ( dom g) = ( Seg n1) by A1, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n1 by A6, XXREAL_0:def 9;

          hence thesis by A2, A4, A7, FINSEQ_1:def 3;

        end;

          case

           A8: n2 <= n1;

          then ( dom f2) c= ( dom f1) by A1, A3, FINSEQ_1: 5;

          then

           A9: ( dom g) = ( Seg n2) by A3, A5, XBOOLE_1: 28;

          ( min (n1,n2)) = n2 by A8, XXREAL_0:def 9;

          hence thesis by A2, A4, A9, FINSEQ_1:def 3;

        end;

      end;

      hence thesis;

    end;

    

     Lm2: for m1,m2 be complex-valued FinSequence st ( len m1) = ( len m2) holds ( len (m1 + m2)) = ( len m1)

    proof

      let m1,m2 be complex-valued FinSequence;

      assume

       A1: ( len m1) = ( len m2);

      

      thus ( len (m1 + m2)) = ( min (( len m1),( len m2))) by Th1

      .= ( len m1) by A1;

    end;

    

     Lm3: for m1,m2 be complex-valued FinSequence st ( len m1) = ( len m2) holds ( len (m1 - m2)) = ( len m1)

    proof

      let m1,m2 be complex-valued FinSequence;

      assume

       A1: ( len m1) = ( len m2);

      

      thus ( len (m1 - m2)) = ( min (( len m1),( len m2))) by Th2

      .= ( len m1) by A1;

    end;

    

     Lm4: for m1,m2 be complex-valued FinSequence st ( len m1) = ( len m2) holds ( len (m1 (#) m2)) = ( len m1)

    proof

      let m1,m2 be complex-valued FinSequence;

      assume

       A1: ( len m1) = ( len m2);

      

      thus ( len (m1 (#) m2)) = ( min (( len m1),( len m2))) by Th3

      .= ( len m1) by A1;

    end;

    theorem :: INT_6:4

    

     Th4: for m1,m2 be complex-valued FinSequence st ( len m1) = ( len m2) holds for k be Nat st k <= ( len m1) holds ((m1 (#) m2) | k) = ((m1 | k) (#) (m2 | k))

    proof

      let m1,m2 be complex-valued FinSequence;

      assume

       A1: ( len m1) = ( len m2);

      let k9 be Nat;

      set p = ((m1 (#) m2) | k9), q = ((m1 | k9) (#) (m2 | k9));

      assume

       A2: k9 <= ( len m1);

      then

       A3: ( len (m1 | k9)) = k9 by FINSEQ_1: 59;

      reconsider k = k9 as Element of NAT by ORDINAL1:def 12;

      

       A4: k9 <= ( len (m1 (#) m2)) by A1, A2, Lm4;

      then

       A5: ( len p) = k9 by FINSEQ_1: 59;

      

       A6: ( len (m2 | k9)) = k9 by A1, A2, FINSEQ_1: 59;

      then

       A7: ( len q) = k9 by A3, Lm4;

      now

        

         A8: ( len (m1 (#) m2)) = ( len m1) by A1, Lm4;

        let j be Nat;

        assume that

         A9: 1 <= j and

         A10: j <= ( len p);

        

         A11: j in ( Seg k) by A5, A9, A10;

        then

         A12: j in ( dom (m1 | k)) by A3, FINSEQ_1:def 3;

        

         A13: j in ( dom q) by A7, A11, FINSEQ_1:def 3;

        

         A14: j in ( dom (m2 | k)) by A6, A11, FINSEQ_1:def 3;

        j <= ( len m1) by A2, A5, A10, XXREAL_0: 2;

        then j in ( Seg ( len (m1 (#) m2))) by A9, A8;

        then

         A15: j in ( dom (m1 (#) m2)) by FINSEQ_1:def 3;

        j in ( dom p) by A9, A10, FINSEQ_3: 25;

        

        hence (p . j) = ((m1 (#) m2) . j) by FUNCT_1: 47

        .= ((m1 . j) * (m2 . j)) by A15, VALUED_1:def 4

        .= (((m1 | k) . j) * (m2 . j)) by A12, FUNCT_1: 47

        .= (((m1 | k) . j) * ((m2 | k) . j)) by A14, FUNCT_1: 47

        .= (q . j) by A13, VALUED_1:def 4;

      end;

      hence thesis by A4, A7, FINSEQ_1: 59;

    end;

    registration

      let F be INT -valued FinSequence;

      cluster ( Sum F) -> integer;

      coherence

      proof

        set mc = addcomplex ;

        consider f be FinSequence of COMPLEX such that

         A1: f = F and

         A2: ( Sum F) = ( addcomplex $$ f) by RVSUM_1:def 10;

        set g = ( [#] (f,( the_unity_wrt mc)));

        defpred P[ Nat] means (mc $$ (( finSeg $1),( [#] (f,( the_unity_wrt mc))))) is integer;

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          

           A4: (g . (k + 1)) is integer

          proof

            per cases ;

              suppose (k + 1) in ( dom f);

              then (g . (k + 1)) = (f . (k + 1)) by SETWOP_2: 20;

              hence thesis by A1;

            end;

              suppose not (k + 1) in ( dom f);

              hence thesis by BINOP_2: 1, SETWOP_2: 20;

            end;

          end;

          assume P[k];

          then

          reconsider a = (g . (k + 1)), b = (mc $$ (( finSeg k),g)) as Integer by A4;

           not (k + 1) in ( Seg k) by FINSEQ_3: 8;

          

          then (mc $$ ((( finSeg k) \/ {.(k + 1).}),g)) = (mc . ((mc $$ (( finSeg k),g)),(g . (k + 1)))) by SETWOP_2: 2

          .= (b + a) by BINOP_2:def 3;

          hence thesis by FINSEQ_1: 9;

        end;

        ( Seg 0 ) = ( {}. NAT );

        then

         A5: P[ 0 ] by BINOP_2: 1, SETWISEO: 31;

        

         A6: for n be Nat holds P[n] from NAT_1:sch 2( A5, A3);

        consider n be Nat such that

         A7: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

        

         A8: (mc $$ f) = (mc $$ (( findom f),( [#] (f,( the_unity_wrt mc))))) by SETWOP_2:def 2;

        thus thesis by A2, A8, A7, A6;

      end;

      cluster ( Product F) -> integer;

      coherence

      proof

        set mc = multcomplex ;

        consider f be FinSequence of COMPLEX such that

         A9: f = F and

         A10: ( Product F) = ( multcomplex $$ f) by RVSUM_1:def 13;

        set g = ( [#] (f,( the_unity_wrt mc)));

        defpred P[ Nat] means (mc $$ (( finSeg $1),( [#] (f,( the_unity_wrt mc))))) is integer;

        

         A11: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          

           A12: (g . (k + 1)) is integer

          proof

            per cases ;

              suppose (k + 1) in ( dom f);

              then (g . (k + 1)) = (f . (k + 1)) by SETWOP_2: 20;

              hence thesis by A9;

            end;

              suppose not (k + 1) in ( dom f);

              hence thesis by BINOP_2: 6, SETWOP_2: 20;

            end;

          end;

          assume P[k];

          then

          reconsider a = (g . (k + 1)), b = (mc $$ (( finSeg k),g)) as Integer by A12;

           not (k + 1) in ( Seg k) by FINSEQ_3: 8;

          

          then (mc $$ ((( finSeg k) \/ {.(k + 1).}),g)) = (mc . ((mc $$ (( finSeg k),g)),(g . (k + 1)))) by SETWOP_2: 2

          .= (b * a) by BINOP_2:def 5;

          hence thesis by FINSEQ_1: 9;

        end;

        ( Seg 0 ) = ( {}. NAT );

        then

         A13: P[ 0 ] by BINOP_2: 6, SETWISEO: 31;

        

         A14: for n be Nat holds P[n] from NAT_1:sch 2( A13, A11);

        consider n be Nat such that

         A15: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

        

         A16: (mc $$ f) = (mc $$ (( findom f),( [#] (f,( the_unity_wrt mc))))) by SETWOP_2:def 2;

        thus thesis by A10, A16, A15, A14;

      end;

    end

    

     Lm5: for z be INT -valued FinSequence holds z is FinSequence of REAL

    proof

      let f be INT -valued FinSequence;

      ( rng f) c= REAL ;

      hence thesis by FINSEQ_1:def 4;

    end;

    theorem :: INT_6:5

    

     Th5: for f be complex-valued FinSequence, i be Nat st (i + 1) <= ( len f) holds ((f | i) ^ <*(f . (i + 1))*>) = (f | (i + 1))

    proof

      let f be complex-valued FinSequence, i be Nat;

      assume

       A1: (i + 1) <= ( len f);

      set f1 = ((f | i) ^ <*(f . (i + 1))*>), f2 = (f | (i + 1));

      

       A2: i <= (i + 1) by NAT_1: 11;

      reconsider f1 as complex-valued FinSequence;

      

       A3: ( len f1) = (( len (f | i)) + ( len <*(f . (i + 1))*>)) by FINSEQ_1: 22

      .= (( len (f | i)) + 1) by FINSEQ_1: 39

      .= (i + 1) by A1, A2, FINSEQ_1: 59, XXREAL_0: 2

      .= ( len f2) by A1, FINSEQ_1: 59;

      

      then

       A4: ( dom f1) = ( Seg ( len f2)) by FINSEQ_1:def 3

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

      

       A5: i <= ( len f) by A1, A2, XXREAL_0: 2;

      now

        let x9 be object;

        assume

         A6: x9 in ( dom f1);

        then

        reconsider x = x9 as Element of NAT ;

        

         A7: ( dom f1) = ( Seg ( len f1)) by FINSEQ_1:def 3;

        then

         A8: 1 <= x by A6, FINSEQ_1: 1;

        x <= ( len f1) by A6, A7, FINSEQ_1: 1;

        then

         A9: x <= (i + 1) by A1, A3, FINSEQ_1: 59;

        per cases by A9, XXREAL_0: 1;

          suppose

           A10: x = (i + 1);

          then x in ( Seg (i + 1)) by A8;

          then

           A11: x in ( dom f2) by A1, FINSEQ_1: 17;

          ( dom <*(f . (i + 1))*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then

           A12: 1 in ( dom <*(f . (i + 1))*>) by TARSKI:def 1;

          ( len (f | i)) = i by A1, A2, FINSEQ_1: 59, XXREAL_0: 2;

          

          hence (f1 . x9) = ( <*(f . (i + 1))*> . 1) by A10, A12, FINSEQ_1:def 7

          .= (f . (i + 1)) by FINSEQ_1: 40

          .= (f2 . x9) by A10, A11, FUNCT_1: 47;

        end;

          suppose x < (i + 1);

          then

           A13: x <= i by NAT_1: 13;

          1 <= x by A6, A7, FINSEQ_1: 1;

          then x in ( Seg i) by A13;

          then

           A14: x in ( dom (f | i)) by A5, FINSEQ_1: 17;

          

          hence (f1 . x9) = ((f | i) . x) by FINSEQ_1:def 7

          .= (f . x) by A14, FUNCT_1: 47

          .= (f2 . x9) by A4, A6, FUNCT_1: 47;

        end;

      end;

      hence thesis by A4;

    end;

    theorem :: INT_6:6

    

     Th6: for f be complex-valued FinSequence st ex i be Nat st i in ( dom f) & (f . i) = 0 holds ( Product f) = 0

    proof

      defpred P[ Nat] means for f be complex-valued FinSequence st ( len f) = $1 holds (ex i be Nat st i in ( dom f) & (f . i) = 0 ) implies ( Product f) = 0 ;

      let m be complex-valued FinSequence;

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: P[k];

        now

          let f be complex-valued FinSequence;

          set f1 = (f | k);

          assume

           A3: ( len f) = (k + 1);

          then

           A4: ( len f1) = k by FINSEQ_1: 59, NAT_1: 11;

          reconsider f1 as complex-valued FinSequence;

          f = (f1 ^ <*(f . (k + 1))*>) by A3, FINSEQ_3: 55;

          then

           A5: ( Product f) = (( Product f1) * (f . (k + 1))) by RVSUM_1: 96;

          assume

           A6: ex i be Nat st i in ( dom f) & (f . i) = 0 ;

          per cases ;

            suppose (f . (k + 1)) = 0 ;

            hence ( Product f) = 0 by A5;

          end;

            suppose

             A7: (f . (k + 1)) <> 0 ;

            consider j be Nat such that

             A8: j in ( dom f) and

             A9: (f . j) = 0 by A6;

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

            

             A10: j in ( Seg ( len f)) by A8, FINSEQ_1:def 3;

            then j <= (k + 1) by A3, FINSEQ_1: 1;

            then j < (k + 1) by A7, A9, XXREAL_0: 1;

            then

             A11: j <= k by NAT_1: 13;

            1 <= j by A10, FINSEQ_1: 1;

            then j in ( Seg k) by A11;

            then

             A12: j in ( dom f1) by A4, FINSEQ_1:def 3;

            then (f1 . j) = (f . j) by FUNCT_1: 47;

            then ( Product f1) = 0 by A2, A4, A9, A12;

            hence ( Product f) = 0 by A5;

          end;

        end;

        hence thesis;

      end;

      

       A13: P[ 0 ]

      proof

        let f be complex-valued FinSequence;

        assume ( len f) = 0 ;

        then ( Seg ( len f)) = {} ;

        hence thesis by FINSEQ_1:def 3;

      end;

      

       A14: for k be Nat holds P[k] from NAT_1:sch 2( A13, A1);

      

       A15: ex j be Nat st ( len m) = j;

      assume ex i be Nat st i in ( dom m) & (m . i) = 0 ;

      hence thesis by A14, A15;

    end;

    theorem :: INT_6:7

    

     Th7: for n,a,b be Integer holds ((a - b) mod n) = (((a mod n) - (b mod n)) mod n)

    proof

      let n,a,b be Integer;

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ((a - b) mod n) = 0 by INT_1:def 10

        .= (((a mod n) - (b mod n)) mod n) by A1, INT_1:def 10;

      end;

        suppose

         A2: n <> 0 ;

        then

         A3: ((b mod n) + ((b div n) * n)) = ((b - ((b div n) * n)) + ((b div n) * n)) by INT_1:def 10;

        ((a mod n) + ((a div n) * n)) = ((a - ((a div n) * n)) + ((a div n) * n)) by A2, INT_1:def 10;

        then ((a - b) - ((a mod n) - (b mod n))) = (((a div n) - (b div n)) * n) by A3;

        then n divides ((a - b) - ((a mod n) - (b mod n))) by INT_1:def 3;

        then ((a - b),((a mod n) - (b mod n))) are_congruent_mod n by INT_2: 15;

        hence thesis by NAT_D: 64;

      end;

    end;

    theorem :: INT_6:8

    

     Th8: for i,j,k be Integer st i divides j holds (k * i) divides (k * j)

    proof

      let i,j,k be Integer;

      assume i divides j;

      then

      consider z be Integer such that

       A1: (i * z) = j by INT_1:def 3;

      ((i * k) * z) = (j * k) by A1;

      hence thesis by INT_1:def 3;

    end;

    theorem :: INT_6:9

    

     Th9: for m be INT -valued FinSequence, i be Nat st i in ( dom m) & (m . i) <> 0 holds (( Product m) / (m . i)) is Integer

    proof

      let m be INT -valued FinSequence, i9 be Nat;

      reconsider i = i9 as Element of NAT by ORDINAL1:def 12;

      reconsider m2 = (m /^ i) as FinSequence of INT by Lm1;

      reconsider m1 = (m | i) as FinSequence of INT by Lm1;

      reconsider m9 = m as FinSequence of INT by Lm1;

      assume that

       A1: i9 in ( dom m) and

       A2: (m . i9) <> 0 ;

      

       A3: ( dom m) = ( Seg ( len m)) by FINSEQ_1:def 3;

      then 1 <= i by A1, FINSEQ_1: 1;

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

      then

      reconsider j = (i - 1) as Element of NAT by INT_1: 3;

      set f = ((m | j) ^ (m /^ i));

      reconsider f as FinSequence of INT by Lm1;

      

       A4: m9 = (m1 ^ m2) by RFINSEQ: 8;

      (j + 1) <= ( len m) by A1, A3, FINSEQ_1: 1;

      then ((m | j) ^ <*(m . i)*>) = (m | i) by Th5;

      

      then ( Product m) = (( Product ((m | j) ^ <*(m . i)*>)) * ( Product (m /^ i))) by A4, RVSUM_1: 97

      .= ((( Product (m | j)) * ( Product <*(m . i)*>)) * ( Product (m /^ i))) by RVSUM_1: 97

      .= ((( Product (m | j)) * ( Product (m /^ i))) * ( Product <*(m . i)*>))

      .= ((( Product (m | j)) * ( Product (m /^ i))) * (m . i))

      .= (( Product f) * (m . i)) by RVSUM_1: 97;

      then (m . i) divides ( Product m) by INT_1:def 3;

      hence thesis by A2, WSIERP_1: 17;

    end;

    theorem :: INT_6:10

    

     Th10: for m be INT -valued FinSequence, i be Nat st i in ( dom m) holds ex z be Integer st (z * (m . i)) = ( Product m)

    proof

      let m be INT -valued FinSequence, i be Nat;

      assume

       A1: i in ( dom m);

      per cases ;

        suppose

         A2: (m . i) <> 0 ;

        then

        reconsider z = (( Product m) / (m . i)) as Integer by A1, Th9;

        take z;

        

        thus (z * (m . i)) = (( Product m) * (((m . i) " ) * (m . i)))

        .= (( Product m) * 1) by A2, XCMPLX_0:def 7

        .= ( Product m);

      end;

        suppose

         A3: (m . i) = 0 ;

        take 1;

        thus thesis by A1, A3, Th6;

      end;

    end;

    

     Lm6: for m be INT -valued FinSequence, i,j be Nat st i in ( dom m) & j in ( dom m) & j <> i & (m . j) <> 0 holds ex z be Integer st (z * (m . i)) = (( Product m) / (m . j))

    proof

      let m be INT -valued FinSequence, i9,j9 be Nat;

      reconsider m9 = m as FinSequence of INT by Lm1;

      assume that

       A1: i9 in ( dom m) and

       A2: j9 in ( dom m) and

       A3: j9 <> i9 and

       A4: (m . j9) <> 0 ;

      reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;

      

       A5: ( dom m) = ( Seg ( len m)) by FINSEQ_1:def 3;

      then

       A6: j <= ( len m) by A2, FINSEQ_1: 1;

      

       A7: 1 <= j by A2, A5, FINSEQ_1: 1;

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

      then

      reconsider kj = (j - 1) as Element of NAT by INT_1: 3;

      set f = ((m | kj) ^ (m /^ j));

      reconsider f as FinSequence of INT by Lm1;

      (kj + 1) = j;

      then kj <= j by NAT_1: 11;

      then

       A8: ( len (m | kj)) = kj by A6, FINSEQ_1: 59, XXREAL_0: 2;

      

       A9: ( dom m) = ( Seg ( len m)) by FINSEQ_1:def 3;

      then

       A10: 1 <= i by A1, FINSEQ_1: 1;

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

      then

      reconsider ki = (i - 1) as Element of NAT by INT_1: 3;

      

       A11: i <= ( len m) by A1, A9, FINSEQ_1: 1;

      ex l be Element of NAT st l in ( dom f) & (f . l) = (m . i)

      proof

        per cases by A3, XXREAL_0: 1;

          suppose

           A12: i < j;

          

           A13: ( dom (m | kj)) c= ( dom f) by FINSEQ_1: 26;

          i < (kj + 1) by A12;

          then i <= (j - 1) by NAT_1: 13;

          then i in ( Seg kj) by A10;

          then

           A14: i in ( dom (m | kj)) by A8, FINSEQ_1:def 3;

          then ((m | kj) . i) = (m . i) by FUNCT_1: 47;

          then (f . i) = (m . i) by A14, FINSEQ_1:def 7;

          hence thesis by A14, A13;

        end;

          suppose

           A15: i > j;

          then (i - 1) > kj by XREAL_1: 9;

          then

          reconsider a = ((i - 1) - kj) as Element of NAT by INT_1: 5;

          (i - kj) > ((kj + 1) - kj) by A15, XREAL_1: 9;

          then ((i - kj) - 1) > (1 - 1) by XREAL_1: 9;

          then ex g be Nat st a = (g + 1) by NAT_1: 6;

          then

           A16: 1 <= ((i - 1) - kj) by NAT_1: 11;

          

           A17: ( len (m /^ j)) = (( len m) - j) by A6, RFINSEQ:def 1;

          

          then ( len f) = (kj + (( len m) - j)) by A8, FINSEQ_1: 22

          .= (( len m) - 1);

          then

           A18: ki <= ( len f) by A11, XREAL_1: 9;

          (i - j) <= (( len m) - j) by A11, XREAL_1: 9;

          then a in ( Seg ( len (m /^ j))) by A17, A16;

          then

           A19: ((i - 1) - kj) in ( dom (m9 /^ j)) by FINSEQ_1:def 3;

          (ki + 1) > 1 by A7, A15, XXREAL_0: 2;

          then ki >= 1 by NAT_1: 13;

          then ki in ( Seg ( len f)) by A18;

          then

           A20: ki in ( dom f) by FINSEQ_1:def 3;

          reconsider D = INT as set;

          reconsider ww = m9 as FinSequence of D;

          ( len (m | kj)) < (i - 1) by A8, A15, XREAL_1: 9;

          

          then (f . ki) = ((m /^ j) . (ki - kj)) by A8, A18, FINSEQ_1: 24

          .= ((ww /^ j) /. (ki - kj)) by A19, PARTFUN1:def 6

          .= (ww /. (j + a)) by A19, FINSEQ_5: 27

          .= (m . i) by A1, PARTFUN1:def 6;

          hence thesis by A20;

        end;

      end;

      then

      consider l be Element of NAT such that

       A21: l in ( dom f) and

       A22: (f . l) = (m . i);

      l in ( Seg ( len f)) by A21, FINSEQ_1:def 3;

      then 1 <= l by FINSEQ_1: 1;

      then

      reconsider kl = (l - 1) as Element of NAT by INT_1: 5;

      l in ( Seg ( len f)) by A21, FINSEQ_1:def 3;

      then (kl + 1) <= ( len f) by FINSEQ_1: 1;

      then ((f | kl) ^ <*(f . l)*>) = (f | l) by Th5;

      then f = (((f | kl) ^ <*(f . l)*>) ^ (f /^ l)) by RFINSEQ: 8;

      

      then

       A23: ( Product f) = (( Product ((f | kl) ^ <*(f . l)*>)) * ( Product (f /^ l))) by RVSUM_1: 97

      .= ((( Product (f | kl)) * ( Product <*(f . l)*>)) * ( Product (f /^ l))) by RVSUM_1: 97

      .= ((( Product (f | kl)) * ( Product (f /^ l))) * ( Product <*(m . i)*>)) by A22

      .= ((( Product (f | kl)) * ( Product (f /^ l))) * (m . i))

      .= (( Product ((f | kl) ^ (f /^ l))) * (m . i)) by RVSUM_1: 97;

      (kj + 1) <= ( len m) by A2, A5, FINSEQ_1: 1;

      then

       A24: ((m | kj) ^ <*(m . j)*>) = (m | j) by Th5;

      reconsider m2 = (m /^ j) as FinSequence of INT by Lm1;

      reconsider m1 = (m | j) as FinSequence of INT by Lm1;

      m9 = (m1 ^ m2) by RFINSEQ: 8;

      

      then ( Product m) = (( Product ((m | kj) ^ <*(m . j)*>)) * ( Product (m /^ j))) by A24, RVSUM_1: 97

      .= ((( Product (m | kj)) * ( Product <*(m . j)*>)) * ( Product (m /^ j))) by RVSUM_1: 97

      .= ((( Product (m | kj)) * ( Product (m /^ j))) * ( Product <*(m . j)*>))

      .= ((( Product (m | kj)) * ( Product (m /^ j))) * (m . j))

      .= (( Product f) * (m . j)) by RVSUM_1: 97;

      

      then (( Product m) / (m . j)) = (( Product f) * ((m . j) * ((m . j) " )))

      .= (( Product f) * 1) by A4, XCMPLX_0:def 7;

      hence thesis by A23;

    end;

    theorem :: INT_6:11

    for m be INT -valued FinSequence, i,j be Nat st i in ( dom m) & j in ( dom m) & j <> i & (m . j) <> 0 holds (( Product m) / ((m . i) * (m . j))) is Integer

    proof

      let m be INT -valued FinSequence, i9,j9 be Nat;

      assume that

       A1: i9 in ( dom m) and

       A2: j9 in ( dom m) and

       A3: j9 <> i9 and

       A4: (m . j9) <> 0 ;

      reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;

      

       A5: ex z be Integer st (z * (m . i)) = (( Product m) / (m . j)) by A1, A2, A3, A4, Lm6;

      per cases ;

        suppose

         A0: (m . i) = 0 ;

        thus thesis by A0;

      end;

        suppose

         A6: (m . i) <> 0 ;

        reconsider u = (( Product m) / (m . j)) as Integer by A2, A4, Th9;

        

         A7: (u / (m . i)) = (( Product m) * (((m . j) " ) * ((m . i) " )))

        .= (( Product m) / ((m . i) * (m . j))) by XCMPLX_1: 204;

        (m . i) divides u by A5, INT_1:def 3;

        hence thesis by A6, A7, WSIERP_1: 17;

      end;

    end;

    theorem :: INT_6:12

    for m be INT -valued FinSequence, i,j be Nat st i in ( dom m) & j in ( dom m) & j <> i & (m . j) <> 0 holds ex z be Integer st (z * (m . i)) = (( Product m) / (m . j)) by Lm6;

    begin

    theorem :: INT_6:13

    

     Th13: for i be Integer holds |.i.| divides i & i divides |.i.|

    proof

      let i be Integer;

      per cases by ABSVALUE: 1;

        suppose |.i.| = i;

        hence thesis;

      end;

        suppose

         A1: |.i.| = ( - i);

        then

         A2: (i * ( - 1)) = |.i.|;

        ( |.i.| * ( - 1)) = i by A1;

        hence thesis by A2, INT_1:def 3;

      end;

    end;

    theorem :: INT_6:14

    

     Th14: for i,j be Integer holds (i gcd j) = (i gcd |.j.|)

    proof

      let i,j be Integer;

      set k = (i gcd |.j.|);

      k divides |.j.| by INT_2:def 2;

      then

      consider x be Integer such that

       A1: (k * x) = |.j.| by INT_1:def 3;

       |.j.| divides j by Th13;

      then

      consider y be Integer such that

       A2: ( |.j.| * y) = j by INT_1:def 3;

      

       A3: for m be Integer st m divides i & m divides j holds m divides k

      proof

        j divides |.j.| by Th13;

        then

        consider y be Integer such that

         A4: (j * y) = |.j.| by INT_1:def 3;

        let m be Integer;

        assume that

         A5: m divides i and

         A6: m divides j;

        consider x be Integer such that

         A7: (m * x) = j by A6, INT_1:def 3;

        (m * (x * y)) = |.j.| by A7, A4;

        then m divides |.j.| by INT_1:def 3;

        hence thesis by A5, INT_2:def 2;

      end;

      (k * (x * y)) = j by A1, A2;

      then

       A8: k divides j by INT_1:def 3;

      k divides i by INT_2:def 2;

      hence thesis by A8, A3, INT_2:def 2;

    end;

    theorem :: INT_6:15

    

     Th15: for i,j be Integer st (i,j) are_coprime holds (i lcm j) = |.(i * j).|

    proof

      let i,j be Integer;

      assume

       A1: (i gcd j) = 1;

      per cases ;

        suppose

         A2: i = 0 or j = 0 ;

        

        hence (i lcm j) = 0 by INT_2: 4

        .= |.(i * j).| by A2, ABSVALUE: 2;

      end;

        suppose

         A3: i <> 0 & j <> 0 ;

        

         A4: for m be Integer st i divides m & j divides m holds |.(i * j).| divides m

        proof

          j divides (i lcm j) by INT_2:def 1;

          then

          consider kj be Integer such that

           A5: (j * kj) = (i lcm j) by INT_1:def 3;

          i divides (i lcm j) by INT_2:def 1;

          then

          consider ki be Integer such that

           A6: (i * ki) = (i lcm j) by INT_1:def 3;

          

           A7: j divides (i * j) by INT_2: 2;

          i divides (i * j) by INT_2: 2;

          then (i lcm j) divides (i * j) by A7, INT_2:def 1;

          then

          consider kij be Integer such that

           A8: ((i lcm j) * kij) = (i * j) by INT_1:def 3;

          (i * j) = (j * (kj * kij)) by A5, A8;

          then i = (kj * kij) by A3, XCMPLX_1: 5;

          then

           A9: kij divides i by INT_1:def 3;

          (i * j) = (i * (ki * kij)) by A6, A8;

          then j = (ki * kij) by A3, XCMPLX_1: 5;

          then kij divides j by INT_1:def 3;

          then

           A10: kij divides 1 by A1, A9, INT_2:def 2;

          let m be Integer;

          assume that

           A11: i divides m and

           A12: j divides m;

          

           A13: (i lcm j) divides m by A11, A12, INT_2:def 1;

          per cases by A10, INT_2: 13;

            suppose kij = 1;

            hence thesis by A8, A13, ABSVALUE:def 1;

          end;

            suppose

             A14: kij = ( - 1);

            ( - (i * j)) <> 0 by A3, XCMPLX_1: 6;

            then ( - ( - (i * j))) < 0 by A8, A14;

            hence thesis by A8, A13, A14, ABSVALUE:def 1;

          end;

        end;

        j divides |.j.| by Th13;

        then j divides ( |.i.| * |.j.|) by INT_2: 2;

        then

         A15: j divides |.(i * j).| by COMPLEX1: 65;

        i divides |.i.| by Th13;

        then i divides ( |.i.| * |.j.|) by INT_2: 2;

        then i divides |.(i * j).| by COMPLEX1: 65;

        hence thesis by A15, A4, INT_2:def 1;

      end;

    end;

    theorem :: INT_6:16

    

     Th16: for i,j,k be Integer holds ((i * j) gcd (i * k)) = ( |.i.| * (j gcd k))

    proof

      let i,j,k be Integer;

      per cases ;

        suppose

         A1: i = 0 ;

        

        hence ((i * j) gcd (i * k)) = ( 0 * (j gcd k)) by INT_2: 5

        .= ( |.i.| * (j gcd k)) by A1, ABSVALUE:def 1;

      end;

        suppose

         A2: i <> 0 ;

        set d = (j gcd k), e = ((i * j) gcd (i * k));

        per cases ;

          suppose

           A3: d = 0 ;

          then

           A4: k = 0 by INT_2: 5;

          j = 0 by A3, INT_2: 5;

          hence thesis by A3, A4;

        end;

          suppose

           A5: d <> 0 ;

          

           A6: e divides (i * k) by INT_2: 21;

          

           A7: (i * d) divides (i * k) by Th8, INT_2: 21;

          (i * d) divides (i * j) by Th8, INT_2: 21;

          then (i * d) divides e by A7, INT_2: 22;

          then

          consider g be Integer such that

           A8: e = ((i * d) * g) by INT_1:def 3;

          

           A9: e divides (i * j) by INT_2: 21;

          (d * g) divides j & (d * g) divides k

          proof

            consider h1 be Integer such that

             A10: (((i * d) * g) * h1) = (i * j) by A8, A9, INT_1:def 3;

            (i * ((d * g) * h1)) = (i * j) by A10;

            then ((d * g) * h1) = j by A2, XCMPLX_1: 5;

            hence (d * g) divides j by INT_1:def 3;

            consider h2 be Integer such that

             A11: (((i * d) * g) * h2) = (i * k) by A8, A6, INT_1:def 3;

            (i * ((d * g) * h2)) = (i * k) by A11;

            then ((d * g) * h2) = k by A2, XCMPLX_1: 5;

            hence thesis by INT_1:def 3;

          end;

          then (d * g) divides d by INT_2: 22;

          then

          consider h3 be Integer such that

           A12: ((d * g) * h3) = d by INT_1:def 3;

          (d * (g * h3)) = (d * 1) by A12;

          then (g * h3) = 1 by A5, XCMPLX_1: 5;

          then

           A13: g divides 1 by INT_1:def 3;

          per cases by A13, INT_2: 13;

            suppose

             A14: g = 1;

            i < 0 implies (d * i) < ( 0 * i) by A5, XREAL_1: 69;

            hence thesis by A8, A14, ABSVALUE:def 1;

          end;

            suppose

             A15: g = ( - 1);

             A16:

            now

              assume i > 0 ;

              then ( - ( - i)) > 0 ;

              then ( - i) < 0 ;

              hence (d * ( - i)) < ( 0 * ( - i)) by A5, XREAL_1: 69;

            end;

            ((i * j) gcd (i * k)) = (( - i) * d) by A8, A15;

            hence thesis by A2, A16, ABSVALUE:def 1;

          end;

        end;

      end;

    end;

    theorem :: INT_6:17

    

     Th17: for i,j be Integer holds ((i * j) gcd i) = |.i.|

    proof

      let i,j be Integer;

      

       A1: for m be Integer st m divides (i * j) & m divides i holds m divides |.i.|

      proof

        let m be Integer;

        assume that m divides (i * j) and

         A2: m divides i;

        consider k be Integer such that

         A3: (m * k) = i by A2, INT_1:def 3;

        i divides |.i.| by Th13;

        then

        consider l be Integer such that

         A4: (i * l) = |.i.| by INT_1:def 3;

        (m * (k * l)) = |.i.| by A3, A4;

        hence thesis by INT_1:def 3;

      end;

      

       A5: |.i.| divides i by Th13;

      then |.i.| divides (i * j) by INT_2: 2;

      hence thesis by A5, A1, INT_2:def 2;

    end;

    theorem :: INT_6:18

    

     Th18: for i,j,k be Integer holds (i gcd (j gcd k)) = ((i gcd j) gcd k)

    proof

      let i,j,k be Integer;

      per cases ;

        suppose i = 0 & j = 0 & k = 0 ;

        hence thesis;

      end;

        suppose

         A1: i <> 0 or j <> 0 or k <> 0 ;

         A2:

        now

          assume (i gcd (j gcd k)) = ( - ((i gcd j) gcd k));

          then (( - ((i gcd j) gcd k)) * ( - 1)) <= ( 0 * ( - 1));

          then

           A3: ((i gcd j) gcd k) = 0 ;

          then (i gcd j) = 0 by INT_2: 5;

          hence contradiction by A1, A3, INT_2: 5;

        end;

        

         A4: (i gcd (j gcd k)) divides i by INT_2: 21;

        

         A5: ((i gcd j) gcd k) divides k by INT_2: 21;

        

         A6: ((i gcd j) gcd k) divides (i gcd j) by INT_2: 21;

        (i gcd j) divides j by INT_2: 21;

        then ((i gcd j) gcd k) divides j by A6, INT_2: 9;

        then

         A7: ((i gcd j) gcd k) divides (j gcd k) by A5, INT_2: 22;

        (i gcd j) divides i by INT_2: 21;

        then ((i gcd j) gcd k) divides i by A6, INT_2: 9;

        then

         A8: ((i gcd j) gcd k) divides (i gcd (j gcd k)) by A7, INT_2: 22;

        

         A9: (i gcd (j gcd k)) divides (j gcd k) by INT_2: 21;

        (j gcd k) divides j by INT_2: 21;

        then (i gcd (j gcd k)) divides j by A9, INT_2: 9;

        then

         A10: (i gcd (j gcd k)) divides (i gcd j) by A4, INT_2: 22;

        (j gcd k) divides k by INT_2: 21;

        then (i gcd (j gcd k)) divides k by A9, INT_2: 9;

        then (i gcd (j gcd k)) divides ((i gcd j) gcd k) by A10, INT_2: 22;

        hence thesis by A8, A2, INT_2: 11;

      end;

    end;

    theorem :: INT_6:19

    

     Th19: for i,j,k be Integer st (i,j) are_coprime holds (i gcd (j * k)) = (i gcd k)

    proof

      let i,j,k be Integer;

      assume

       A1: (i gcd j) = 1;

      ((i * k) gcd (j * k)) = ( |.k.| * (i gcd j)) by Th16;

      

      then (i gcd |.k.|) = ((i gcd (i * k)) gcd (j * k)) by A1, Th18

      .= ( |.i.| gcd (j * k)) by Th17

      .= ((j * k) gcd i) by Th14;

      hence thesis by Th14;

    end;

    theorem :: INT_6:20

    

     Th20: for i,j be Integer st (i,j) are_coprime holds (i * j) divides (i lcm j)

    proof

      let i,j be Integer;

      assume (i,j) are_coprime ;

      then |.(i * j).| divides (i lcm j) by Th15;

      then

      consider z be Integer such that

       A1: ( |.(i * j).| * z) = (i lcm j) by INT_1:def 3;

      per cases ;

        suppose 0 <= (i * j);

        then (z * (i * j)) = (i lcm j) by A1, ABSVALUE:def 1;

        hence thesis by INT_1:def 3;

      end;

        suppose

         A2: 0 > (i * j);

        (( - z) * (i * j)) = (z * ( - (i * j)))

        .= (i lcm j) by A1, A2, ABSVALUE:def 1;

        hence thesis by INT_1:def 3;

      end;

    end;

    theorem :: INT_6:21

    

     Th21: for x,y,i,j be Integer st (i,j) are_coprime holds (x,y) are_congruent_mod i & (x,y) are_congruent_mod j implies (x,y) are_congruent_mod (i * j)

    proof

      let x,y,i,j be Integer;

      assume (i,j) are_coprime ;

      then

       A1: (i * j) divides (i lcm j) by Th20;

      assume that

       A2: (x,y) are_congruent_mod i and

       A3: (x,y) are_congruent_mod j;

      

       A4: j divides (x - y) by A3, INT_2: 15;

      i divides (x - y) by A2, INT_2: 15;

      then (i lcm j) divides (x - y) by A4, INT_2: 19;

      then (i * j) divides (x - y) by A1, INT_2: 9;

      hence thesis by INT_2: 15;

    end;

    theorem :: INT_6:22

    

     Th22: for i,j be Integer st (i,j) are_coprime holds ex s be Integer st ((s * i),1) are_congruent_mod j

    proof

      let i,j be Integer;

      assume (i gcd j) = 1;

      then

      consider s,t be Integer such that

       A1: 1 = ((s * i) + (t * j)) by NAT_D: 68;

      take s;

      ((s * i) - 1) = (( - t) * j) by A1;

      then j divides ((s * i) - 1) by INT_1:def 3;

      hence thesis by INT_2: 15;

    end;

    begin

    notation

      let f be INT -valued FinSequence;

      antonym f is multiplicative-trivial for f is non-empty;

    end

    definition

      let f be INT -valued FinSequence;

      :: original: multiplicative-trivial

      redefine

      :: INT_6:def1

      attr f is multiplicative-trivial means

      : Def1: ex i be Nat st i in ( dom f) & (f . i) = 0 ;

      compatibility ;

    end

    

     Lm7: for u be object st u in {1} holds u in INT by INT_1:def 1;

    registration

      cluster multiplicative-trivial for INT -valued FinSequence;

      existence

      proof

        set p = <* 0 *>;

        for u be object st u in { 0 } holds u in INT by INT_1:def 1;

        then { 0 } c= INT by TARSKI:def 3;

        then ( rng p) c= INT by FINSEQ_1: 39;

        then

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

        take f;

        take 1;

        ( len f) = 1 by FINSEQ_1: 40;

        then ( dom f) = ( Seg 1) by FINSEQ_1:def 3;

        hence 1 in ( dom f);

        thus thesis by FINSEQ_1: 40;

      end;

      cluster non multiplicative-trivial for INT -valued FinSequence;

      existence by Def1;

      cluster non empty positive-yielding for INT -valued FinSequence;

      existence

      proof

        set p = <*1*>;

         {1} c= INT by Lm7, TARSKI:def 3;

        then ( rng p) c= INT by FINSEQ_1: 39;

        then

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

        take f;

        now

          let r be Real;

          assume r in ( rng f);

          then r in {1} by FINSEQ_1: 39;

          hence 0 < r by TARSKI:def 1;

        end;

        hence thesis by PARTFUN3:def 1;

      end;

    end

    theorem :: INT_6:23

    for m be multiplicative-trivial INT -valued FinSequence holds ( Product m) = 0

    proof

      let m be multiplicative-trivial INT -valued FinSequence;

      ex i be Nat st i in ( dom m) & (m . i) = 0 by Def1;

      hence thesis by Th6;

    end;

    definition

      let f be INT -valued FinSequence;

      :: INT_6:def2

      attr f is Chinese_Remainder means

      : Def2: for i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j holds ((f . i),(f . j)) are_coprime ;

    end

    registration

      cluster non empty positive-yielding Chinese_Remainder for INT -valued FinSequence;

      existence

      proof

        set p = <*1*>;

         {1} c= INT by Lm7, TARSKI:def 3;

        then ( rng p) c= INT by FINSEQ_1: 39;

        then

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

        take f;

         A1:

        now

          let i be Element of NAT ;

          assume i in ( dom f);

          then i in ( Seg 1) by FINSEQ_1: 38;

          hence i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        end;

         A2:

        now

          let i9,j9 be Nat;

          assume that

           A3: i9 in ( dom f) and

           A4: j9 in ( dom f) and

           A5: i9 <> j9;

          reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;

          i = 1 by A1, A3

          .= j by A1, A4;

          hence ((f . i9),(f . j9)) are_coprime by A5;

        end;

        now

          let r be Real;

          assume r in ( rng f);

          then r in {1} by FINSEQ_1: 39;

          hence 0 < r by TARSKI:def 1;

        end;

        hence thesis by A2, PARTFUN3:def 1;

      end;

    end

    definition

      mode CR_Sequence is non empty positive-yielding Chinese_Remainder INT -valued FinSequence;

    end

    registration

      cluster -> non multiplicative-trivial for CR_Sequence;

      coherence

      proof

        let f be CR_Sequence;

        now

          let i be Nat;

          assume i in ( dom f);

          then (f . i) in ( rng f) by FUNCT_1: 3;

          hence (f . i) <> 0 by PARTFUN3:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      cluster multiplicative-trivial -> non empty for INT -valued FinSequence;

      coherence ;

    end

    theorem :: INT_6:24

    

     Th24: for f be CR_Sequence, m be Nat st 0 < m & m <= ( len f) holds (f | m) is CR_Sequence

    proof

      let f be CR_Sequence, m be Nat;

      reconsider fm = (f | m) as FinSequence of INT by Lm1;

      assume that

       A1: m > 0 and

       A2: m <= ( len f);

      

       A3: ( len fm) = m by A2, FINSEQ_1: 59;

       A4:

      now

        let i be Element of NAT ;

        assume i in ( dom fm);

        then

         A5: i in ( Seg m) by A3, FINSEQ_1:def 3;

        then i <= m by FINSEQ_1: 1;

        then

         A6: i <= ( len f) by A2, XXREAL_0: 2;

        1 <= i by A5, FINSEQ_1: 1;

        then i in ( Seg ( len f)) by A6;

        hence i in ( dom f) by FINSEQ_1:def 3;

      end;

       A7:

      now

        let i9,j9 be Nat;

        assume that

         A8: i9 in ( dom fm) and

         A9: j9 in ( dom fm) and

         A10: i9 <> j9;

        reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;

        

         A11: (f . i) = (fm . i) by A8, FUNCT_1: 47;

        

         A12: (f . j) = (fm . j) by A9, FUNCT_1: 47;

        

         A13: j in ( dom f) by A4, A9;

        i in ( dom f) by A4, A8;

        hence ((fm . i9),(fm . j9)) are_coprime by A10, A13, A11, A12, Def2;

      end;

      now

        let r be Real;

        assume r in ( rng fm);

        then

        consider i be object such that

         A14: i in ( dom fm) and

         A15: (fm . i) = r by FUNCT_1:def 3;

        reconsider i as Element of NAT by A14;

        (f . i) in ( rng f) by A4, A14, FUNCT_1: 3;

        then (f . i) > 0 by PARTFUN3:def 1;

        hence r > 0 by A14, A15, FUNCT_1: 47;

      end;

      hence thesis by A1, A7, Def2, PARTFUN3:def 1;

    end;

    

     Lm8: for m be CR_Sequence holds ( Product m) > 0

    proof

      defpred P[ Nat] means for f be CR_Sequence st ( len f) = $1 holds ( Product f) > 0 ;

      let m be CR_Sequence;

      

       A1: ex j be Nat st ( len m) = j;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: P[k];

        now

          let f be CR_Sequence;

          assume

           A4: ( len f) = (k + 1);

          set f1 = (f | k);

          per cases ;

            suppose k > 0 ;

            then

            reconsider f1 as CR_Sequence by A4, Th24, NAT_1: 11;

            

             A5: f = (f1 ^ <*(f . (k + 1))*>) by A4, FINSEQ_3: 55;

            1 <= (k + 1) by NAT_1: 11;

            then (k + 1) in ( Seg (k + 1));

            then (k + 1) in ( dom f) by A4, FINSEQ_1:def 3;

            then (f . (k + 1)) in ( rng f) by FUNCT_1: 3;

            then

             A6: (f . (k + 1)) > 0 by PARTFUN3:def 1;

            ( len f1) = k by A4, FINSEQ_1: 59, NAT_1: 11;

            then ( Product f1) > 0 by A3;

            then ( 0 * (f . (k + 1))) < (( Product f1) * (f . (k + 1))) by A6, XREAL_1: 68;

            hence ( Product f) > 0 by A5, RVSUM_1: 96;

          end;

            suppose k = 0 ;

            then

             A7: f = <*(f . 1)*> by A4, FINSEQ_1: 40;

            then ( dom f) = ( Seg 1) by FINSEQ_1: 38;

            then 1 in ( dom f);

            then (f . 1) in ( rng f) by FUNCT_1: 3;

            then (f . 1) > 0 by PARTFUN3:def 1;

            hence ( Product f) > 0 by A7;

          end;

        end;

        hence thesis;

      end;

      

       A8: P[ 0 ];

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

      hence thesis by A1;

    end;

    registration

      let m be CR_Sequence;

      cluster ( Product m) -> positive natural;

      coherence

      proof

        ( Product m) > 0 by Lm8;

        then ( Product m) is Element of NAT by INT_1: 3;

        hence thesis by Lm8;

      end;

    end

    theorem :: INT_6:25

    

     Th25: for m be CR_Sequence, i be Nat st i in ( dom m) holds for mm be Integer st mm = (( Product m) / (m . i)) holds (mm,(m . i)) are_coprime

    proof

      defpred P[ Nat] means for m be CR_Sequence st ( len m) = $1 holds for i be Nat st i in ( dom m) holds for mm be Integer st mm = (( Product m) / (m . i)) holds (mm,(m . i)) are_coprime ;

      let m be CR_Sequence, i be Nat;

      assume

       A1: i in ( dom m);

      let mm be Integer;

      

       A2: ex l be Element of NAT st ( len m) = l;

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        now

          let m be CR_Sequence;

          set m1 = (m | k);

          assume

           A5: ( len m) = (k + 1);

          

          then

           A6: (m1 ^ <*(m . (k + 1))*>) = (m | (k + 1)) by Th5

          .= m by A5, FINSEQ_1: 58;

          

           A7: ( len m1) = k by A5, FINSEQ_1: 59, NAT_1: 11;

          1 <= (k + 1) by NAT_1: 11;

          then (k + 1) in ( Seg (k + 1));

          then

           A8: (k + 1) in ( dom m) by A5, FINSEQ_1:def 3;

          let i9 be Nat;

          reconsider i = i9 as Element of NAT by ORDINAL1:def 12;

          assume

           A9: i9 in ( dom m);

          then

           A10: i in ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

          then

           A11: i <= (k + 1) by FINSEQ_1: 1;

          let mm be Integer;

          assume

           A12: mm = (( Product m) / (m . i9));

          per cases ;

            suppose k > 0 ;

            then

            reconsider m1 as CR_Sequence by A5, Th24, NAT_1: 11;

            per cases ;

              suppose

               A13: i in ( dom m1);

              then i in ( Seg k) by A7, FINSEQ_1:def 3;

              then i <= k by FINSEQ_1: 1;

              then i <> (k + 1) by NAT_1: 13;

              then

               A14: ((m . i),(m . (k + 1))) are_coprime by A9, A8, Def2;

              reconsider mm1 = (( Product m1) / (m1 . i)) as Integer by A13, Th9;

              

               A15: (m1 . i) = (m . i) by A13, FUNCT_1: 47;

              then (mm1,(m . i)) are_coprime by A4, A7, A13;

              

              then

               A16: ((m . i) gcd (mm1 * (m . (k + 1)))) = ((m . i) gcd (m . (k + 1))) by Th19

              .= 1 by A14;

              (mm1 * (m . (k + 1))) = ((( Product m1) * (m . (k + 1))) * ((m . i) " )) by A15

              .= mm by A12, A6, RVSUM_1: 96;

              hence (mm,(m . i9)) are_coprime by A16;

            end;

              suppose

               A17: not i in ( dom m1);

              (m . (k + 1)) in ( rng m) by A8, FUNCT_1: 3;

              then

               A18: (m . (k + 1)) > 0 by PARTFUN3:def 1;

              defpred Q[ Nat] means $1 <= ( len m1) implies for s be Element of NAT st s = $1 holds (( Product (m1 | s)),(m . (k + 1))) are_coprime ;

              

               A19: (m1 | ( len m1)) = m1 by FINSEQ_1: 58;

               A20:

              now

                let j be Element of NAT ;

                assume that 0 <= j and

                 A21: j < ( len m1);

                assume

                 A22: Q[j];

                now

                  assume

                   A23: (j + 1) <= ( len m1);

                  

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

                  then (j + 1) in ( Seg ( len m1)) by A23;

                  then

                   A25: (j + 1) in ( dom m1) by FINSEQ_1:def 3;

                  (j + 1) <= ( len m) by A5, A7, A21, XREAL_1: 8;

                  then (j + 1) in ( Seg ( len m)) by A24;

                  then

                   A26: (j + 1) in ( dom m) by FINSEQ_1:def 3;

                  (j + 1) <= k by A5, A23, FINSEQ_1: 59, NAT_1: 11;

                  then

                   A27: (j + 1) <> (k + 1) by NAT_1: 13;

                  now

                    reconsider s9 = j as Element of NAT ;

                    let s be Element of NAT ;

                    

                     A28: (m1 . (j + 1)) = (m . (j + 1)) by A25, FUNCT_1: 47;

                    

                     A29: ((m . (j + 1)),(m . (k + 1))) are_coprime by A8, A27, A26, Def2;

                    j <= (j + 1) by NAT_1: 11;

                    then (( Product (m1 | s9)),(m . (k + 1))) are_coprime by A22, A23, XXREAL_0: 2;

                    

                    then

                     A30: ((( Product (m1 | s9)) * (m . (j + 1))) gcd (m . (k + 1))) = ((m . (j + 1)) gcd (m . (k + 1))) by Th19

                    .= 1 by A29;

                    assume

                     A31: s = (j + 1);

                    then ((m1 | s9) ^ <*(m1 . s)*>) = (m1 | s) by A23, Th5;

                    then (( Product (m1 | s)) gcd (m . (k + 1))) = 1 by A31, A30, A28, RVSUM_1: 96;

                    hence (( Product (m1 | s)),(m . (k + 1))) are_coprime ;

                  end;

                  hence Q[(j + 1)];

                end;

                hence Q[(j + 1)];

              end;

              (m1 | 0 ) is empty;

              then

               A32: Q[ 0 ] by RVSUM_1: 94, WSIERP_1: 9;

              

               A33: for j be Element of NAT st 0 <= j & j <= ( len m1) holds Q[j] from INT_1:sch 7( A32, A20);

               not i in ( Seg k) by A7, A17, FINSEQ_1:def 3;

              then not (1 <= i & i <= k);

              then not i < (k + 1) by A10, FINSEQ_1: 1, NAT_1: 13;

              then

               A34: i = (k + 1) by A11, XXREAL_0: 1;

              

              then mm = ((( Product m1) * (m . (k + 1))) * ((m . (k + 1)) " )) by A12, A6, RVSUM_1: 96

              .= (( Product m1) * ((m . (k + 1)) * ((m . (k + 1)) " )))

              .= (( Product m1) * 1) by A18, XCMPLX_0:def 7;

              hence (mm,(m . i9)) are_coprime by A34, A33, A19;

            end;

          end;

            suppose k = 0 ;

            then

             A35: m = <*(m . 1)*> by A5, FINSEQ_1: 40;

            then

             A36: ( dom m) = ( Seg 1) by FINSEQ_1: 38;

            then

             A37: i <= 1 by A9, FINSEQ_1: 1;

            1 <= i by A9, A36, FINSEQ_1: 1;

            then

             A38: i = 1 by A37, XXREAL_0: 1;

            ( Product m) = (m . 1) by A35;

            then mm = 1 by A12, A38, XCMPLX_0:def 7;

            hence (mm,(m . i9)) are_coprime by WSIERP_1: 9;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A39: P[ 0 ];

      

       A40: for k be Nat holds P[k] from NAT_1:sch 2( A39, A3);

      assume mm = (( Product m) / (m . i));

      hence thesis by A1, A40, A2;

    end;

    

     Lm9: for u be INT -valued FinSequence, m be CR_Sequence holds for z1,z2 be Integer st 0 <= z1 & z1 < ( Product m) & (for i be Nat st i in ( dom m) holds (z1,(u . i)) are_congruent_mod (m . i)) & 0 <= z2 & z2 < ( Product m) & (for i be Nat st i in ( dom m) holds (z2,(u . i)) are_congruent_mod (m . i)) holds z1 = z2

    proof

      let u be INT -valued FinSequence, m be CR_Sequence;

      let z1,z2 be Integer;

      assume that

       A1: 0 <= z1 and

       A2: z1 < ( Product m) and

       A3: for i be Nat st i in ( dom m) holds (z1,(u . i)) are_congruent_mod (m . i) and

       A4: 0 <= z2 and

       A5: z2 < ( Product m) and

       A6: for i be Nat st i in ( dom m) holds (z2,(u . i)) are_congruent_mod (m . i);

      defpred P[ Nat] means for m1 be CR_Sequence st m1 = (m | $1) holds (z1,z2) are_congruent_mod ( Product m1);

       A7:

      now

        let i be Element of NAT ;

        assume

         A8: i in ( dom m);

        then

         A9: ((u . i),z2) are_congruent_mod (m . i) by A6, INT_1: 14;

        (z1,(u . i)) are_congruent_mod (m . i) by A3, A8;

        hence (z1,z2) are_congruent_mod (m . i) by A9, INT_1: 15;

      end;

       A10:

      now

        let k be Element of NAT ;

        assume that 0 <= k and

         A11: k < ( len m);

        assume

         A12: P[k];

        now

          set m2 = (m | k);

          let m1 be CR_Sequence;

          

           A13: 1 <= (k + 1) by NAT_1: 11;

          

           A14: (k + 1) <= ( len m) by A11, NAT_1: 13;

          then (k + 1) in ( Seg ( len m)) by A13;

          then

           A15: (k + 1) in ( dom m) by FINSEQ_1:def 3;

          assume

           A16: m1 = (m | (k + 1));

          then

           A17: ( len m1) = (k + 1) by A14, FINSEQ_1: 59;

          then (k + 1) in ( Seg ( len m1)) by A13;

          then

           A18: (k + 1) in ( dom m1) by FINSEQ_1:def 3;

          per cases ;

            suppose k > 0 ;

            then

            reconsider m2 as CR_Sequence by A11, Th24;

            set mm = (( Product m1) / (m1 . (k + 1)));

            

             A19: (z1,z2) are_congruent_mod ( Product m2) by A12;

            reconsider m9 = m as FinSequence of INT by Lm1;

            

             A20: (m . (k + 1)) = (m1 . (k + 1)) by A16, A18, FUNCT_1: 47;

            (m . (k + 1)) in ( rng m) by A15, FUNCT_1: 3;

            then

             A21: (m1 . (k + 1)) > 0 by A20, PARTFUN3:def 1;

            reconsider mm as Integer by A18, Th9;

            

             A22: (mm * (m1 . (k + 1))) = (( Product m1) * (((m1 . (k + 1)) " ) * (m1 . (k + 1))))

            .= (( Product m1) * 1) by A21, XCMPLX_0:def 7

            .= ( Product m1);

            ((m9 | (k + 1)) | k) = (m9 | k) by FINSEQ_1: 82, NAT_1: 11;

            then m1 = (m2 ^ <*(m1 . (k + 1))*>) by A16, A17, FINSEQ_3: 55;

            then ( Product m1) = (( Product m2) * (m1 . (k + 1))) by RVSUM_1: 96;

            then mm = (( Product m2) * ((m1 . (k + 1)) * ((m1 . (k + 1)) " )));

            then

             A23: mm = (( Product m2) * 1) by A21, XCMPLX_0:def 7;

            (z1,z2) are_congruent_mod (m1 . (k + 1)) by A7, A15, A20;

            hence (z1,z2) are_congruent_mod ( Product m1) by A18, A19, A23, A22, Th21, Th25;

          end;

            suppose k = 0 ;

            then

             A24: m1 = <*(m1 . 1)*> by A17, FINSEQ_1: 40;

            then ( dom m1) = ( Seg 1) by FINSEQ_1: 38;

            then

             A25: 1 in ( dom m1);

            1 <= ( len m) by A14, A13, XXREAL_0: 2;

            then 1 in ( Seg ( len m));

            then

             A26: 1 in ( dom m) by FINSEQ_1:def 3;

            ( Product m1) = (m1 . 1) by A24

            .= (m . 1) by A16, A25, FUNCT_1: 47;

            hence (z1,z2) are_congruent_mod ( Product m1) by A7, A26;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A27: (m | ( len m)) = m by FINSEQ_1: 58;

      

       A28: P[ 0 ];

      for k be Element of NAT st 0 <= k & k <= ( len m) holds P[k] from INT_1:sch 7( A28, A10);

      then

       A29: (z1,z2) are_congruent_mod ( Product m) by A27;

      

      thus z1 = (z1 mod ( Product m)) by A1, A2, NAT_D: 63

      .= (z2 mod ( Product m)) by A29, NAT_D: 64

      .= z2 by A4, A5, NAT_D: 63;

    end;

    begin

    definition

      let u be Integer, m be INT -valued FinSequence;

      :: INT_6:def3

      func mod (u,m) -> FinSequence means

      : Def3: ( len it ) = ( len m) & for i be Nat st i in ( dom it ) holds (it . i) = (u mod (m . i));

      existence

      proof

        defpred P[ set, set] means $2 = (u mod (m . $1));

        

         A1: for k be Nat st k in ( Seg ( len m)) holds ex x be Element of INT st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len m));

          reconsider j = (u mod (m . k)) as Element of INT by INT_1:def 2;

          take j;

          thus thesis;

        end;

        consider p be FinSequence of INT such that

         A2: ( dom p) = ( Seg ( len m)) & for k be Nat st k in ( Seg ( len m)) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        take p;

        thus ( len p) = ( len m) by A2, FINSEQ_1:def 3;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let z1,z2 be FinSequence;

        assume that

         A3: ( len z1) = ( len m) and

         A4: for i be Nat st i in ( dom z1) holds (z1 . i) = (u mod (m . i));

        assume that

         A5: ( len z2) = ( len m) and

         A6: for i be Nat st i in ( dom z2) holds (z2 . i) = (u mod (m . i));

        

         A7: ( dom z1) = ( Seg ( len z1)) by FINSEQ_1:def 3

        .= ( dom z2) by A3, A5, FINSEQ_1:def 3;

        now

          let x be object;

          assume

           A8: x in ( dom z1);

          then

          reconsider x9 = x as Element of NAT ;

          

          thus (z1 . x) = (u mod (m . x9)) by A4, A8

          .= (z2 . x) by A6, A7, A8;

        end;

        hence thesis by A7;

      end;

    end

    registration

      let u be Integer, m be INT -valued FinSequence;

      cluster ( mod (u,m)) -> INT -valued;

      coherence

      proof

        now

          let y be object;

          assume y in ( rng ( mod (u,m)));

          then

          consider x be object such that

           A1: x in ( dom ( mod (u,m))) and

           A2: (( mod (u,m)) . x) = y by FUNCT_1:def 3;

          reconsider x as Element of NAT by A1;

          reconsider x as Nat;

          y = (u mod (m . x)) by A1, A2, Def3;

          hence y in INT by INT_1:def 2;

        end;

        then ( rng ( mod (u,m))) c= INT by TARSKI:def 3;

        hence thesis by RELAT_1:def 19;

      end;

    end

    definition

      let m be CR_Sequence;

      :: INT_6:def4

      mode CR_coefficients of m -> FinSequence means

      : Def4: ( len it ) = ( len m) & for i be Nat st i in ( dom it ) holds ex s be Integer, mm be Integer st mm = (( Product m) / (m . i)) & ((s * mm),1) are_congruent_mod (m . i) & (it . i) = (s * (( Product m) / (m . i)));

      existence

      proof

        defpred P[ set, set] means ex s be Integer, mm be Integer st mm = (( Product m) / (m . $1)) & ((s * mm),1) are_congruent_mod (m . $1) & $2 = (s * (( Product m) / (m . $1)));

        

         A1: for k be Nat st k in ( Seg ( len m)) holds ex x be Element of INT st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len m));

          then

           A2: k in ( dom m) by FINSEQ_1:def 3;

          then

          reconsider mm = (( Product m) / (m . k)) as Integer by Th9;

          consider s be Integer such that

           A3: ((s * mm),1) are_congruent_mod (m . k) by A2, Th22, Th25;

          set x = (s * mm);

          reconsider x as Element of INT by INT_1:def 2;

          take x;

          take s;

          take mm;

          thus thesis by A3;

        end;

        consider p be FinSequence of INT such that

         A4: ( dom p) = ( Seg ( len m)) & for k be Nat st k in ( Seg ( len m)) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        take p;

        thus thesis by A4, FINSEQ_1:def 3;

      end;

    end

    registration

      let m be CR_Sequence;

      cluster -> INT -valued for CR_coefficients of m;

      coherence

      proof

        let c be CR_coefficients of m;

        now

          let u be object;

          assume u in ( rng c);

          then

          consider x be object such that

           A1: x in ( dom c) and

           A2: (c . x) = u by FUNCT_1:def 3;

          reconsider x as Element of NAT by A1;

          reconsider x as Nat;

          ex s be Integer, mm be Integer st mm = (( Product m) / (m . x)) & ((s * mm),1) are_congruent_mod (m . x) & (c . x) = (s * (( Product m) / (m . x))) by A1, Def4;

          hence u in INT by A2, INT_1:def 2;

        end;

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

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: INT_6:26

    

     Th26: for m be CR_Sequence, c be CR_coefficients of m, i be Nat st i in ( dom c) holds ((c . i),1) are_congruent_mod (m . i)

    proof

      let m be CR_Sequence, c be CR_coefficients of m, i be Nat;

      assume i in ( dom c);

      then ex s be Integer, mm be Integer st mm = (( Product m) / (m . i)) & ((s * mm),1) are_congruent_mod (m . i) & (c . i) = (s * (( Product m) / (m . i))) by Def4;

      hence thesis;

    end;

    theorem :: INT_6:27

    

     Th27: for m be CR_Sequence, c be CR_coefficients of m, i,j be Nat st i in ( dom c) & j in ( dom c) & i <> j holds ((c . i), 0 ) are_congruent_mod (m . j)

    proof

      let m be CR_Sequence, c be CR_coefficients of m, i,j be Nat;

      assume that

       A1: i in ( dom c) and

       A2: j in ( dom c) and

       A3: i <> j;

      consider s be Integer, mm be Integer such that

       A4: mm = (( Product m) / (m . i)) and ((s * mm),1) are_congruent_mod (m . i) and

       A5: (c . i) = (s * (( Product m) / (m . i))) by A1, Def4;

      ( len m) = ( len c) by Def4;

      

      then ( dom m) = ( Seg ( len c)) by FINSEQ_1:def 3

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

      then

      consider z be Integer such that

       A6: (z * (m . j)) = mm by A1, A2, A3, A4, Lm6;

      

       A7: ((m . j), 0 ) are_congruent_mod (m . j) by INT_1: 12;

      

       A8: (s,s) are_congruent_mod (m . j) by INT_1: 11;

      (z,z) are_congruent_mod (m . j) by INT_1: 11;

      then ((z * (m . j)),(z * 0 )) are_congruent_mod (m . j) by A7, INT_1: 18;

      then ((s * mm),(s * 0 )) are_congruent_mod (m . j) by A6, A8, INT_1: 18;

      hence thesis by A4, A5;

    end;

    theorem :: INT_6:28

    for m be CR_Sequence, c1,c2 be CR_coefficients of m, i be Nat st i in ( dom c1) holds ((c1 . i),(c2 . i)) are_congruent_mod (m . i)

    proof

      let m be CR_Sequence, c1,c2 be CR_coefficients of m, i be Nat;

      assume

       A1: i in ( dom c1);

      then

       A2: ex s1 be Integer, mm1 be Integer st mm1 = (( Product m) / (m . i)) & ((s1 * mm1),1) are_congruent_mod (m . i) & (c1 . i) = (s1 * (( Product m) / (m . i))) by Def4;

      

       A3: ( len c1) = ( len m) by Def4

      .= ( len c2) by Def4;

      ( dom c1) = ( Seg ( len c1)) by FINSEQ_1:def 3

      .= ( dom c2) by A3, FINSEQ_1:def 3;

      then

      consider s2 be Integer, mm2 be Integer such that

       A4: mm2 = (( Product m) / (m . i)) and

       A5: ((s2 * mm2),1) are_congruent_mod (m . i) and

       A6: (c2 . i) = (s2 * (( Product m) / (m . i))) by A1, Def4;

      (1,(s2 * mm2)) are_congruent_mod (m . i) by A5, INT_1: 14;

      hence thesis by A2, A4, A6, INT_1: 15;

    end;

    theorem :: INT_6:29

    

     Th29: for u be INT -valued FinSequence, m be CR_Sequence st ( len m) = ( len u) holds for c be CR_coefficients of m, i be Nat st i in ( dom m) holds (( Sum (u (#) c)),(u . i)) are_congruent_mod (m . i)

    proof

      let u be INT -valued FinSequence, m be CR_Sequence;

      assume

       A1: ( len m) = ( len u);

      let c be CR_coefficients of m, i be Nat;

      defpred P[ Nat] means for v,cc be INT -valued FinSequence st v = (u | $1) & cc = (c | $1) holds ($1 < i & (( Sum (v (#) cc)), 0 ) are_congruent_mod (m . i)) or ($1 >= i & (( Sum (v (#) cc)),(u . i)) are_congruent_mod (m . i));

      assume

       A2: i in ( dom m);

      

       A3: ( len m) = ( len c) by Def4;

      

      then

       A4: ( dom m) = ( Seg ( len c)) by FINSEQ_1:def 3

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

       A5:

      now

        let k be Element of NAT ;

        assume that 0 <= k and

         A6: k < ( len u) and

         A7: P[k];

        now

          set v9 = (u | k), cc9 = (c | k);

          let v,cc be INT -valued FinSequence;

          

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

          reconsider a = (v (#) cc), b = (v9 (#) cc9) as FinSequence of REAL by Lm5;

          assume that

           A9: v = (u | (k + 1)) and

           A10: cc = (c | (k + 1));

          (k + 1) <= ( len u) by A6, NAT_1: 13;

          then ( len v) = (k + 1) by A9, FINSEQ_1: 59;

          then (k + 1) in ( Seg ( len v)) by A8;

          then (k + 1) in ( dom v) by FINSEQ_1:def 3;

          then

           A11: (v . (k + 1)) = (u . (k + 1)) by A9, FUNCT_1: 47;

          

           A12: (k + 1) <= ( len c) by A1, A3, A6, NAT_1: 13;

          then (k + 1) in ( Seg ( len c)) by A8;

          then

           A13: (k + 1) in ( dom c) by FINSEQ_1:def 3;

          reconsider r = ((v . (k + 1)) * (cc . (k + 1))) as Element of REAL by XREAL_0:def 1;

          reconsider s = <*r*> as FinSequence of REAL ;

          

           A14: ( len u) = ( len c) by A1, Def4;

          ( len cc) = (k + 1) by A10, A12, FINSEQ_1: 59;

          then (k + 1) in ( Seg ( len cc)) by A8;

          then (k + 1) in ( dom cc) by FINSEQ_1:def 3;

          then

           A15: (cc . (k + 1)) = (c . (k + 1)) by A10, FUNCT_1: 47;

          

           A16: (k + 1) <= ( len u) by A6, NAT_1: 13;

          

           A17: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) = ((u (#) c) | (k + 1))

          proof

            set p = (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>), q = ((u (#) c) | (k + 1));

            

             A18: (k + 1) <= ( len (u (#) c)) by A1, A3, A16, Lm4;

            then

             A19: k <= ( len (u (#) c)) by NAT_1: 13;

            

             A20: ( len p) = (( len ((u (#) c) | k)) + 1) by FINSEQ_2: 16

            .= (k + 1) by A19, FINSEQ_1: 59;

            

             A21: (k + 1) = ( len q) by A18, FINSEQ_1: 59;

            now

              let j be Nat;

              assume that

               A22: 1 <= j and

               A23: j <= ( len p);

              per cases ;

                suppose

                 A24: j in ( dom ((u (#) c) | k));

                j in ( Seg (k + 1)) by A20, A22, A23;

                then

                 A25: j in ( dom q) by A21, FINSEQ_1:def 3;

                

                thus (p . j) = (((u (#) c) | k) . j) by A24, FINSEQ_1:def 7

                .= ((u (#) c) . j) by A24, FUNCT_1: 47

                .= (q . j) by A25, FUNCT_1: 47;

              end;

                suppose

                 A26: not j in ( dom ((u (#) c) | k));

                k <= ( len (u (#) c)) by A6, A14, Lm4;

                then

                 A27: ( len ((u (#) c) | k)) = k by FINSEQ_1: 59;

                then ( dom ((u (#) c) | k)) = ( Seg k) by FINSEQ_1:def 3;

                then j > k by A22, A26;

                then

                 A28: j >= (k + 1) by NAT_1: 13;

                then

                 A29: j = (k + 1) by A20, A23, XXREAL_0: 1;

                ( dom <*((v . (k + 1)) * (cc . (k + 1)))*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

                then 1 in ( dom <*((v . (k + 1)) * (cc . (k + 1)))*>) by TARSKI:def 1;

                

                then

                 A30: (p . (k + 1)) = ( <*((v . (k + 1)) * (cc . (k + 1)))*> . 1) by A27, FINSEQ_1:def 7

                .= ((v . (k + 1)) * (cc . (k + 1))) by FINSEQ_1: 40;

                (k + 1) <= ( len (u (#) c)) by A12, A14, Lm4;

                then j in ( Seg ( len (u (#) c))) by A8, A29;

                then

                 A31: j in ( dom (u (#) c)) by FINSEQ_1:def 3;

                j in ( Seg (k + 1)) by A20, A22, A23;

                then j in ( dom q) by A21, FINSEQ_1:def 3;

                

                then (q . j) = ((u (#) c) . j) by FUNCT_1: 47

                .= ((v . (k + 1)) * (cc . (k + 1))) by A15, A11, A29, A31, VALUED_1:def 4;

                hence (p . j) = (q . j) by A20, A23, A28, A30, XXREAL_0: 1;

              end;

            end;

            hence thesis by A20, A21;

          end;

          (v9 (#) cc9) = ((u (#) c) | k) by A6, A14, Th4;

          then a = (b ^ s) by A9, A10, A16, A14, A17, Th4;

          

          then

           A32: ( Sum (v (#) cc)) = (( Sum b) + ( Sum s)) by RVSUM_1: 75

          .= (( Sum (v9 (#) cc9)) + ((v . (k + 1)) * (cc . (k + 1)))) by RVSUM_1: 73;

          

           A33: k < (k + 1) by NAT_1: 13;

          now

            per cases by XXREAL_0: 1;

              case

               A34: (k + 1) < i;

              then k < i by NAT_1: 13;

              then

               A35: (( Sum (v9 (#) cc9)), 0 ) are_congruent_mod (m . i) by A7;

              

               A36: ((v . (k + 1)),(v . (k + 1))) are_congruent_mod (m . i) by INT_1: 11;

              ((cc . (k + 1)), 0 ) are_congruent_mod (m . i) by A2, A4, A13, A15, A34, Th27;

              then (((v . (k + 1)) * (cc . (k + 1))),((v . (k + 1)) * 0 )) are_congruent_mod (m . i) by A36, INT_1: 18;

              then (( Sum (v (#) cc)),( 0 + ((v . (k + 1)) * 0 ))) are_congruent_mod (m . i) by A32, A35, INT_1: 16;

              hence (( Sum (v (#) cc)), 0 ) are_congruent_mod (m . i);

            end;

              case

               A37: (k + 1) = i;

              

               A38: ((v . (k + 1)),(v . (k + 1))) are_congruent_mod (m . i) by INT_1: 11;

              ((cc . (k + 1)),1) are_congruent_mod (m . i) by A13, A15, A37, Th26;

              then

               A39: (((v . (k + 1)) * (cc . (k + 1))),((u . (k + 1)) * 1)) are_congruent_mod (m . i) by A11, A38, INT_1: 18;

              (( Sum (v9 (#) cc9)), 0 ) are_congruent_mod (m . i) by A7, A33, A37;

              hence (( Sum (v (#) cc)),( 0 + (u . i))) are_congruent_mod (m . i) by A32, A37, A39, INT_1: 16;

            end;

              case

               A40: (k + 1) > i;

              then k >= i by NAT_1: 13;

              then

               A41: (( Sum (v9 (#) cc9)),(u . i)) are_congruent_mod (m . i) by A7;

              

               A42: ((v . (k + 1)),(v . (k + 1))) are_congruent_mod (m . i) by INT_1: 11;

              ((cc . (k + 1)), 0 ) are_congruent_mod (m . i) by A2, A4, A13, A15, A40, Th27;

              then (((v . (k + 1)) * (cc . (k + 1))),((u . (k + 1)) * 0 )) are_congruent_mod (m . i) by A11, A42, INT_1: 18;

              hence (( Sum (v (#) cc)),((u . i) + 0 )) are_congruent_mod (m . i) by A32, A41, INT_1: 16;

            end;

          end;

          hence (k + 1) < i & (( Sum (v (#) cc)), 0 ) are_congruent_mod (m . i) or (k + 1) >= i & (( Sum (v (#) cc)),(u . i)) are_congruent_mod (m . i);

        end;

        hence P[(k + 1)];

      end;

      

       A43: ( dom m) = ( Seg ( len u)) by A1, FINSEQ_1:def 3;

      now

        let v,cc be INT -valued FinSequence;

        assume that

         A44: v = (u | 0 ) and cc = (c | 0 );

        (( dom v) /\ ( dom cc)) = {} by A44;

        then ( dom (v (#) cc)) = {} by VALUED_1:def 4;

        then (v (#) cc) = {} ;

        hence 0 < i & (( Sum (v (#) cc)), 0 ) are_congruent_mod (m . i) or 0 >= i & (( Sum (v (#) cc)),(u . i)) are_congruent_mod (m . i) by A2, A43, FINSEQ_1: 1, INT_1: 11, RVSUM_1: 72;

      end;

      then

       A45: P[ 0 ];

      

       A46: for k be Element of NAT st 0 <= k & k <= ( len u) holds P[k] from INT_1:sch 7( A45, A5);

      ( len u) = ( len c) by A1, Def4;

      then

       A47: (c | ( len u)) = c by FINSEQ_1: 58;

      

       A48: u = (u | ( len u)) by FINSEQ_1: 58;

      i <= ( len u) by A2, A43, FINSEQ_1: 1;

      hence thesis by A46, A48, A47;

    end;

    theorem :: INT_6:30

    

     Th30: for u be INT -valued FinSequence, m be CR_Sequence st ( len m) = ( len u) holds for c1,c2 be CR_coefficients of m holds (( Sum (u (#) c1)),( Sum (u (#) c2))) are_congruent_mod ( Product m)

    proof

      let u be INT -valued FinSequence, m be CR_Sequence;

      assume

       A1: ( len u) = ( len m);

      let c1,c2 be CR_coefficients of m;

      set s1 = (( Sum (u (#) c1)) mod ( Product m)), s2 = (( Sum (u (#) c2)) mod ( Product m));

      

       A2: s1 < ( Product m) by NAT_D: 62;

      

       A3: for i be Nat st i in ( dom m) holds (s1,(u . i)) are_congruent_mod (m . i)

      proof

        let i be Nat;

        (s1 mod ( Product m)) = (( Sum (u (#) c1)) mod ( Product m)) by NAT_D: 65;

        then

         A4: (s1,( Sum (u (#) c1))) are_congruent_mod ( Product m) by NAT_D: 64;

        assume

         A5: i in ( dom m);

        then (m . i) in ( rng m) by FUNCT_1: 3;

        then

         A6: (m . i) > 0 by PARTFUN3:def 1;

        ex z be Integer st (z * (m . i)) = ( Product m) by A5, Th10;

        then (s1,( Sum (u (#) c1))) are_congruent_mod (m . i) by A4, INT_1: 20;

        then

         A7: (s1 mod (m . i)) = (( Sum (u (#) c1)) mod (m . i)) by NAT_D: 64;

        (( Sum (u (#) c1)),(u . i)) are_congruent_mod (m . i) by A1, A5, Th29;

        then (( Sum (u (#) c1)) mod (m . i)) = ((u . i) mod (m . i)) by NAT_D: 64;

        hence thesis by A6, A7, NAT_D: 64;

      end;

      

       A8: 0 <= s2 by NAT_D: 62;

      

       A9: for i be Nat st i in ( dom m) holds (s2,(u . i)) are_congruent_mod (m . i)

      proof

        let i be Nat;

        (s2 mod ( Product m)) = (( Sum (u (#) c2)) mod ( Product m)) by NAT_D: 65;

        then

         A10: (s2,( Sum (u (#) c2))) are_congruent_mod ( Product m) by NAT_D: 64;

        assume

         A11: i in ( dom m);

        then (m . i) in ( rng m) by FUNCT_1: 3;

        then

         A12: (m . i) > 0 by PARTFUN3:def 1;

        ex z be Integer st (z * (m . i)) = ( Product m) by A11, Th10;

        then (s2,( Sum (u (#) c2))) are_congruent_mod (m . i) by A10, INT_1: 20;

        then

         A13: (s2 mod (m . i)) = (( Sum (u (#) c2)) mod (m . i)) by NAT_D: 64;

        (( Sum (u (#) c2)),(u . i)) are_congruent_mod (m . i) by A1, A11, Th29;

        then (( Sum (u (#) c2)) mod (m . i)) = ((u . i) mod (m . i)) by NAT_D: 64;

        hence thesis by A12, A13, NAT_D: 64;

      end;

      

       A14: s2 < ( Product m) by NAT_D: 62;

       0 <= s1 by NAT_D: 62;

      then s1 = s2 by A3, A9, A2, A8, A14, Lm9;

      hence thesis by NAT_D: 64;

    end;

    definition

      let u be INT -valued FinSequence, m be CR_Sequence;

      :: INT_6:def5

      func to_int (u,m) -> Integer means

      : Def5: for c be CR_coefficients of m holds it = (( Sum (u (#) c)) mod ( Product m));

      existence

      proof

        set cz = the CR_coefficients of m;

        set z = (( Sum (u (#) cz)) mod ( Product m));

        take z;

        for c be CR_coefficients of m holds z = (( Sum (u (#) c)) mod ( Product m)) by NAT_D: 64, A1, Th30;

        hence thesis;

      end;

      uniqueness

      proof

        set c = the CR_coefficients of m;

        let z1,z2 be Integer;

        assume

         A2: for c be CR_coefficients of m holds z1 = (( Sum (u (#) c)) mod ( Product m));

        assume

         A3: for c be CR_coefficients of m holds z2 = (( Sum (u (#) c)) mod ( Product m));

        

        thus z1 = (( Sum (u (#) c)) mod ( Product m)) by A2

        .= z2 by A3;

      end;

    end

    theorem :: INT_6:31

    

     Th31: for u be INT -valued FinSequence, m be CR_Sequence st ( len m) = ( len u) holds 0 <= ( to_int (u,m)) & ( to_int (u,m)) < ( Product m)

    proof

      let u be INT -valued FinSequence, m be CR_Sequence;

      set z = ( to_int (u,m));

      set c = the CR_coefficients of m;

      assume ( len u) = ( len m);

      then z = (( Sum (u (#) c)) mod ( Product m)) by Def5;

      hence thesis by NAT_D: 62;

    end;

    theorem :: INT_6:32

    

     Th32: for u be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (u,(( mod (u,m)) . i)) are_congruent_mod (m . i)

    proof

      let u be Integer, m be CR_Sequence;

      let i be Nat;

      

       A1: ( len ( mod (u,m))) = ( len m) by Def3;

      assume

       A2: i in ( dom m);

      then (m . i) in ( rng m) by FUNCT_1: 3;

      then (m . i) > 0 by PARTFUN3:def 1;

      then (u mod (m . i)) = (u - ((u div (m . i)) * (m . i))) by INT_1:def 10;

      then

       A3: (u - (u mod (m . i))) = ((u div (m . i)) * (m . i));

      ( dom ( mod (u,m))) = ( Seg ( len ( mod (u,m)))) by FINSEQ_1:def 3

      .= ( dom m) by A1, FINSEQ_1:def 3;

      then (( mod (u,m)) . i) = (u mod (m . i)) by A2, Def3;

      hence thesis by A3, INT_1:def 5;

    end;

    theorem :: INT_6:33

    

     Th33: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (((( mod (u,m)) + ( mod (v,m))) . i),(u + v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      assume

       A1: i in ( dom m);

      

       A2: ( len ( mod (v,m))) = ( len m) by Def3;

      

      then ( dom ( mod (v,m))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A3: (( mod (v,m)) . i) = (v mod (m . i)) by A1, Def3;

      

       A4: ( len ( mod (u,m))) = ( len m) by Def3;

      then ( len (( mod (u,m)) + ( mod (v,m)))) = ( len m) by A2, Lm2;

      

      then ( dom (( mod (u,m)) + ( mod (v,m)))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A5: ((( mod (u,m)) + ( mod (v,m))) . i) = ((( mod (u,m)) . i) + (( mod (v,m)) . i)) by A1, VALUED_1:def 1;

      ( dom ( mod (u,m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

      then (( mod (u,m)) . i) = (u mod (m . i)) by A1, Def3;

      then

       A6: (((( mod (u,m)) . i) + (( mod (v,m)) . i)) mod (m . i)) = ((u + v) mod (m . i)) by A3, NAT_D: 66;

      (m . i) in ( rng m) by A1, FUNCT_1: 3;

      then (m . i) > 0 by PARTFUN3:def 1;

      hence thesis by A5, A6, NAT_D: 64;

    end;

    

     Lm10: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (((( mod (u,m)) - ( mod (v,m))) . i),(u - v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      assume

       A1: i in ( dom m);

      

       A2: ( len ( mod (v,m))) = ( len m) by Def3;

      

      then ( dom ( mod (v,m))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A3: (( mod (v,m)) . i) = (v mod (m . i)) by A1, Def3;

      

       A4: ( len ( mod (u,m))) = ( len m) by Def3;

      then ( len (( mod (u,m)) - ( mod (v,m)))) = ( len m) by A2, Lm3;

      

      then ( dom (( mod (u,m)) - ( mod (v,m)))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A5: ((( mod (u,m)) - ( mod (v,m))) . i) = ((( mod (u,m)) . i) - (( mod (v,m)) . i)) by A1, VALUED_1: 13;

      ( dom ( mod (u,m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

      then (( mod (u,m)) . i) = (u mod (m . i)) by A1, Def3;

      then

       A6: (((( mod (u,m)) . i) - (( mod (v,m)) . i)) mod (m . i)) = ((u - v) mod (m . i)) by A3, Th7;

      (m . i) in ( rng m) by A1, FUNCT_1: 3;

      then (m . i) > 0 by PARTFUN3:def 1;

      hence thesis by A5, A6, NAT_D: 64;

    end;

    theorem :: INT_6:34

    

     Th34: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (((( mod (u,m)) (#) ( mod (v,m))) . i),(u * v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      assume

       A1: i in ( dom m);

      

       A2: ( len ( mod (v,m))) = ( len m) by Def3;

      

      then ( dom ( mod (v,m))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A3: (( mod (v,m)) . i) = (v mod (m . i)) by A1, Def3;

      

       A4: ( len ( mod (u,m))) = ( len m) by Def3;

      then ( len (( mod (u,m)) (#) ( mod (v,m)))) = ( len m) by A2, Lm4;

      

      then ( dom (( mod (u,m)) (#) ( mod (v,m)))) = ( Seg ( len m)) by FINSEQ_1:def 3

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

      then

       A5: ((( mod (u,m)) (#) ( mod (v,m))) . i) = ((( mod (u,m)) . i) * (( mod (v,m)) . i)) by A1, VALUED_1:def 4;

      ( dom ( mod (u,m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

      then (( mod (u,m)) . i) = (u mod (m . i)) by A1, Def3;

      then

       A6: (((( mod (u,m)) . i) * (( mod (v,m)) . i)) mod (m . i)) = ((u * v) mod (m . i)) by A3, NAT_D: 67;

      (m . i) in ( rng m) by A1, FUNCT_1: 3;

      then (m . i) > 0 by PARTFUN3:def 1;

      hence thesis by A5, A6, NAT_D: 64;

    end;

    theorem :: INT_6:35

    

     Th35: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (( to_int ((( mod (u,m)) + ( mod (v,m))),m)),(u + v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      set z = ( to_int ((( mod (u,m)) + ( mod (v,m))),m));

      set c = the CR_coefficients of m;

      

       A1: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A2: ( len (( mod (u,m)) + ( mod (v,m)))) = ( len m) by A1, Lm2;

      then z = (( Sum ((( mod (u,m)) + ( mod (v,m))) (#) c)) mod ( Product m)) by Def5;

      then (z mod ( Product m)) = (( Sum ((( mod (u,m)) + ( mod (v,m))) (#) c)) mod ( Product m)) by NAT_D: 65;

      then

       A3: (z,( Sum ((( mod (u,m)) + ( mod (v,m))) (#) c))) are_congruent_mod ( Product m) by NAT_D: 64;

      assume

       A4: i in ( dom m);

      then ex y be Integer st (y * (m . i)) = ( Product m) by Th10;

      then

       A5: (z,( Sum ((( mod (u,m)) + ( mod (v,m))) (#) c))) are_congruent_mod (m . i) by A3, INT_1: 20;

      (( Sum ((( mod (u,m)) + ( mod (v,m))) (#) c)),((( mod (u,m)) + ( mod (v,m))) . i)) are_congruent_mod (m . i) by A4, A2, Th29;

      then

       A6: (z,((( mod (u,m)) + ( mod (v,m))) . i)) are_congruent_mod (m . i) by A5, INT_1: 15;

      (((( mod (u,m)) + ( mod (v,m))) . i),(u + v)) are_congruent_mod (m . i) by A4, Th33;

      hence thesis by A6, INT_1: 15;

    end;

    theorem :: INT_6:36

    

     Th36: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (( to_int ((( mod (u,m)) - ( mod (v,m))),m)),(u - v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      set z = ( to_int ((( mod (u,m)) - ( mod (v,m))),m));

      set c = the CR_coefficients of m;

      

       A1: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A2: ( len (( mod (u,m)) - ( mod (v,m)))) = ( len m) by A1, Lm3;

      then z = (( Sum ((( mod (u,m)) - ( mod (v,m))) (#) c)) mod ( Product m)) by Def5;

      then (z mod ( Product m)) = (( Sum ((( mod (u,m)) - ( mod (v,m))) (#) c)) mod ( Product m)) by NAT_D: 65;

      then

       A3: (z,( Sum ((( mod (u,m)) - ( mod (v,m))) (#) c))) are_congruent_mod ( Product m) by NAT_D: 64;

      assume

       A4: i in ( dom m);

      then ex y be Integer st (y * (m . i)) = ( Product m) by Th10;

      then

       A5: (z,( Sum ((( mod (u,m)) - ( mod (v,m))) (#) c))) are_congruent_mod (m . i) by A3, INT_1: 20;

      (( Sum ((( mod (u,m)) - ( mod (v,m))) (#) c)),((( mod (u,m)) - ( mod (v,m))) . i)) are_congruent_mod (m . i) by A4, A2, Th29;

      then

       A6: (z,((( mod (u,m)) - ( mod (v,m))) . i)) are_congruent_mod (m . i) by A5, INT_1: 15;

      (((( mod (u,m)) - ( mod (v,m))) . i),(u - v)) are_congruent_mod (m . i) by A4, Lm10;

      hence thesis by A6, INT_1: 15;

    end;

    theorem :: INT_6:37

    

     Th37: for u,v be Integer, m be CR_Sequence, i be Nat st i in ( dom m) holds (( to_int ((( mod (u,m)) (#) ( mod (v,m))),m)),(u * v)) are_congruent_mod (m . i)

    proof

      let u,v be Integer, m be CR_Sequence, i be Nat;

      set z = ( to_int ((( mod (u,m)) (#) ( mod (v,m))),m));

      set c = the CR_coefficients of m;

      

       A1: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A2: ( len (( mod (u,m)) (#) ( mod (v,m)))) = ( len m) by A1, Lm4;

      then z = (( Sum ((( mod (u,m)) (#) ( mod (v,m))) (#) c)) mod ( Product m)) by Def5;

      then (z mod ( Product m)) = (( Sum ((( mod (u,m)) (#) ( mod (v,m))) (#) c)) mod ( Product m)) by NAT_D: 65;

      then

       A3: (z,( Sum ((( mod (u,m)) (#) ( mod (v,m))) (#) c))) are_congruent_mod ( Product m) by NAT_D: 64;

      assume

       A4: i in ( dom m);

      then ex y be Integer st (y * (m . i)) = ( Product m) by Th10;

      then

       A5: (z,( Sum ((( mod (u,m)) (#) ( mod (v,m))) (#) c))) are_congruent_mod (m . i) by A3, INT_1: 20;

      (( Sum ((( mod (u,m)) (#) ( mod (v,m))) (#) c)),((( mod (u,m)) (#) ( mod (v,m))) . i)) are_congruent_mod (m . i) by A4, A2, Th29;

      then

       A6: (z,((( mod (u,m)) (#) ( mod (v,m))) . i)) are_congruent_mod (m . i) by A5, INT_1: 15;

      (((( mod (u,m)) (#) ( mod (v,m))) . i),(u * v)) are_congruent_mod (m . i) by A4, Th34;

      hence thesis by A6, INT_1: 15;

    end;

    theorem :: INT_6:38

    for u,v be Integer, m be CR_Sequence st 0 <= (u + v) & (u + v) < ( Product m) holds ( to_int ((( mod (u,m)) + ( mod (v,m))),m)) = (u + v)

    proof

      let u,v be Integer, m be CR_Sequence;

      assume that

       A1: 0 <= (u + v) and

       A2: (u + v) < ( Product m);

      set z = ( to_int ((( mod (u,m)) + ( mod (v,m))),m));

      

       A3: for i be Nat st i in ( dom m) holds ((u + v),(( mod ((u + v),m)) . i)) are_congruent_mod (m . i) by Th32;

      

       A4: ( len ( mod ((u + v),m))) = ( len m) by Def3;

      

       A5: for i be Nat st i in ( dom m) holds (z,(( mod ((u + v),m)) . i)) are_congruent_mod (m . i)

      proof

        let i be Nat;

        assume

         A6: i in ( dom m);

        then (z,(u + v)) are_congruent_mod (m . i) by Th35;

        then

         A7: (z mod (m . i)) = ((u + v) mod (m . i)) by NAT_D: 64;

        ( dom ( mod ((u + v),m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

        then

         A8: (( mod ((u + v),m)) . i) = ((u + v) mod (m . i)) by A6, Def3;

        (m . i) in ( rng m) by A6, FUNCT_1: 3;

        then

         A9: (m . i) > 0 by PARTFUN3:def 1;

        then (m . i) is Element of NAT by INT_1: 3;

        then ((u + v) mod (m . i)) = (((u + v) mod (m . i)) mod (m . i)) by NAT_D: 65;

        hence thesis by A8, A7, A9, NAT_D: 64;

      end;

      

       A10: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A11: ( len (( mod (u,m)) + ( mod (v,m)))) = ( len m) by A10, Lm2;

      then

       A12: z < ( Product m) by Th31;

       0 <= z by A11, Th31;

      hence thesis by A1, A2, A3, A12, A5, Lm9;

    end;

    theorem :: INT_6:39

    for u,v be Integer, m be CR_Sequence st 0 <= (u - v) & (u - v) < ( Product m) holds ( to_int ((( mod (u,m)) - ( mod (v,m))),m)) = (u - v)

    proof

      let u,v be Integer, m be CR_Sequence;

      assume that

       A1: 0 <= (u - v) and

       A2: (u - v) < ( Product m);

      set z = ( to_int ((( mod (u,m)) - ( mod (v,m))),m));

      

       A3: for i be Nat st i in ( dom m) holds ((u - v),(( mod ((u - v),m)) . i)) are_congruent_mod (m . i) by Th32;

      

       A4: ( len ( mod ((u - v),m))) = ( len m) by Def3;

      

       A5: for i be Nat st i in ( dom m) holds (z,(( mod ((u - v),m)) . i)) are_congruent_mod (m . i)

      proof

        let i be Nat;

        assume

         A6: i in ( dom m);

        then (z,(u - v)) are_congruent_mod (m . i) by Th36;

        then

         A7: (z mod (m . i)) = ((u - v) mod (m . i)) by NAT_D: 64;

        ( dom ( mod ((u - v),m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

        then

         A8: (( mod ((u - v),m)) . i) = ((u - v) mod (m . i)) by A6, Def3;

        (m . i) in ( rng m) by A6, FUNCT_1: 3;

        then

         A9: (m . i) > 0 by PARTFUN3:def 1;

        then (m . i) is Element of NAT by INT_1: 3;

        then ((u - v) mod (m . i)) = (((u - v) mod (m . i)) mod (m . i)) by NAT_D: 65;

        hence thesis by A8, A7, A9, NAT_D: 64;

      end;

      

       A10: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A11: ( len (( mod (u,m)) - ( mod (v,m)))) = ( len m) by A10, Lm3;

      then

       A12: z < ( Product m) by Th31;

       0 <= z by A11, Th31;

      hence thesis by A1, A2, A3, A12, A5, Lm9;

    end;

    theorem :: INT_6:40

    for u,v be Integer, m be CR_Sequence st 0 <= (u * v) & (u * v) < ( Product m) holds ( to_int ((( mod (u,m)) (#) ( mod (v,m))),m)) = (u * v)

    proof

      let u,v be Integer, m be CR_Sequence;

      assume that

       A1: 0 <= (u * v) and

       A2: (u * v) < ( Product m);

      set z = ( to_int ((( mod (u,m)) (#) ( mod (v,m))),m));

      

       A3: for i be Nat st i in ( dom m) holds ((u * v),(( mod ((u * v),m)) . i)) are_congruent_mod (m . i) by Th32;

      

       A4: ( len ( mod ((u * v),m))) = ( len m) by Def3;

      

       A5: for i be Nat st i in ( dom m) holds (z,(( mod ((u * v),m)) . i)) are_congruent_mod (m . i)

      proof

        let i be Nat;

        assume

         A6: i in ( dom m);

        then (z,(u * v)) are_congruent_mod (m . i) by Th37;

        then

         A7: (z mod (m . i)) = ((u * v) mod (m . i)) by NAT_D: 64;

        ( dom ( mod ((u * v),m))) = ( Seg ( len m)) by A4, FINSEQ_1:def 3

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

        then

         A8: (( mod ((u * v),m)) . i) = ((u * v) mod (m . i)) by A6, Def3;

        (m . i) in ( rng m) by A6, FUNCT_1: 3;

        then

         A9: (m . i) > 0 by PARTFUN3:def 1;

        then (m . i) is Element of NAT by INT_1: 3;

        then ((u * v) mod (m . i)) = (((u * v) mod (m . i)) mod (m . i)) by NAT_D: 65;

        hence thesis by A8, A7, A9, NAT_D: 64;

      end;

      

       A10: ( len ( mod (u,m))) = ( len m) by Def3;

      ( len ( mod (v,m))) = ( len m) by Def3;

      then

       A11: ( len (( mod (u,m)) (#) ( mod (v,m)))) = ( len m) by A10, Lm4;

      then

       A12: z < ( Product m) by Th31;

       0 <= z by A11, Th31;

      hence thesis by A1, A2, A3, A12, A5, Lm9;

    end;

    begin

    theorem :: INT_6:41

    for u be INT -valued FinSequence, m be CR_Sequence st ( len u) = ( len m) holds ex z be Integer st 0 <= z & z < ( Product m) & for i be Nat st i in ( dom u) holds (z,(u . i)) are_congruent_mod (m . i)

    proof

      let u be INT -valued FinSequence, m be CR_Sequence;

      assume

       A1: ( len u) = ( len m);

      take z = ( to_int (u,m));

      now

        set c = the CR_coefficients of m;

        let i be Nat;

        assume

         A2: i in ( dom u);

        set s = (( Sum (u (#) c)) mod ( Product m));

        (s mod ( Product m)) = (( Sum (u (#) c)) mod ( Product m)) by NAT_D: 65;

        then

         A3: (s,( Sum (u (#) c))) are_congruent_mod ( Product m) by NAT_D: 64;

        

         A4: ( dom m) = ( Seg ( len u)) by A1, FINSEQ_1:def 3

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

        then ex y be Integer st (y * (m . i)) = ( Product m) by A2, Th10;

        then (s,( Sum (u (#) c))) are_congruent_mod (m . i) by A3, INT_1: 20;

        then

         A5: (s mod (m . i)) = (( Sum (u (#) c)) mod (m . i)) by NAT_D: 64;

        ( dom m) = ( Seg ( len u)) by A1, FINSEQ_1:def 3

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

        then (m . i) in ( rng m) by A2, FUNCT_1: 3;

        then

         A6: (m . i) > 0 by PARTFUN3:def 1;

        (( Sum (u (#) c)),(u . i)) are_congruent_mod (m . i) by A1, A2, A4, Th29;

        then (( Sum (u (#) c)) mod (m . i)) = ((u . i) mod (m . i)) by NAT_D: 64;

        then (s,(u . i)) are_congruent_mod (m . i) by A6, A5, NAT_D: 64;

        hence (z,(u . i)) are_congruent_mod (m . i) by A1, Def5;

      end;

      hence thesis by A1, Th31;

    end;

    theorem :: INT_6:42

    for u be INT -valued FinSequence, m be CR_Sequence holds for z1,z2 be Integer st 0 <= z1 & z1 < ( Product m) & (for i be Nat st i in ( dom m) holds (z1,(u . i)) are_congruent_mod (m . i)) & 0 <= z2 & z2 < ( Product m) & (for i be Nat st i in ( dom m) holds (z2,(u . i)) are_congruent_mod (m . i)) holds z1 = z2 by Lm9;