int_7.miz



    begin

    reserve x,y for object,

X for set;

    

     Lm1: for z be object st z <> x holds (((X --> 0 ) +* (x,y)) . z) = 0

    proof

      let z be object;

      assume

       A1: z <> x;

      

       A2: ( dom (X --> 0 )) = X by FUNCOP_1: 13;

      per cases ;

        suppose

         A3: z in X;

        (((X --> 0 ) +* (x,y)) . z) = ((X --> 0 ) . z) by A1, FUNCT_7: 32

        .= 0 by A3, FUNCOP_1: 7;

        hence thesis;

      end;

        suppose

         A4: not z in X;

        (((X --> 0 ) +* (x,y)) . z) = ((X --> 0 ) . z) by A1, FUNCT_7: 32

        .= 0 by A2, A4, FUNCT_1:def 2;

        hence thesis;

      end;

    end;

    theorem :: INT_7:1

    

     Th1: for p be ManySortedSet of X st ( support p) = {x} holds p = ((X --> 0 ) +* (x,(p . x)))

    proof

      let p be ManySortedSet of X;

      assume

       A1: ( support p) = {x};

      

       A2: for y be object st y in ( dom p) holds (p . y) = (((X --> 0 ) +* (x,(p . x))) . y)

      proof

        let y be object;

        assume y in ( dom p);

        then y in X;

        then

         A3: y in ( dom (X --> 0 )) by FUNCOP_1: 13;

        per cases ;

          suppose x = y;

          hence thesis by A3, FUNCT_7: 31;

        end;

          suppose

           A4: x <> y;

          then not y in ( support p) by A1, TARSKI:def 1;

          then (p . y) = 0 by PRE_POLY:def 7;

          hence thesis by A4, Lm1;

        end;

      end;

      ( dom ((X --> 0 ) +* (x,(p . x)))) = ( dom (X --> 0 )) by FUNCT_7: 30

      .= X by FUNCOP_1: 13;

      then ( dom p) = ( dom ((X --> 0 ) +* (x,(p . x)))) by PARTFUN1:def 2;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: INT_7:2

    

     Th2: for X be set, p,q,r be real-valued ManySortedSet of X st (( support p) /\ ( support q)) = {} & (( support p) \/ ( support q)) = ( support r) & (p | ( support p)) = (r | ( support p)) & (q | ( support q)) = (r | ( support q)) holds (p + q) = r

    proof

      let X be set, p,q,r be real-valued ManySortedSet of X;

      assume that

       A1: (( support p) /\ ( support q)) = {} and

       A2: (( support p) \/ ( support q)) = ( support r) and

       A3: (p | ( support p)) = (r | ( support p)) and

       A4: (q | ( support q)) = (r | ( support q));

      for x be object st x in X holds (r . x) = ((p . x) + (q . x))

      proof

        let x be object;

        assume x in X;

        per cases ;

          suppose

           A5: x in (( support p) \/ ( support q));

          now

            per cases by A5, XBOOLE_0:def 3;

              suppose

               A6: x in ( support p);

              then

               A7: not x in ( support q) by A1, XBOOLE_0:def 4;

              

              thus (r . x) = ((r | ( support p)) . x) by A6, FUNCT_1: 49

              .= ((p . x) + 0 ) by A3, A6, FUNCT_1: 49

              .= ((p . x) + (q . x)) by A7, PRE_POLY:def 7;

            end;

              suppose

               A8: x in ( support q);

              then

               A9: not x in ( support p) by A1, XBOOLE_0:def 4;

              

              thus (r . x) = ((r | ( support q)) . x) by A8, FUNCT_1: 49

              .= ( 0 + (q . x)) by A4, A8, FUNCT_1: 49

              .= ((p . x) + (q . x)) by A9, PRE_POLY:def 7;

            end;

          end;

          hence thesis;

        end;

          suppose

           A10: not x in (( support p) \/ ( support q));

          then

           A11: not x in ( support q) by XBOOLE_0:def 3;

          

           A12: not x in ( support p) by A10, XBOOLE_0:def 3;

          

          thus (r . x) = 0 by A2, A10, PRE_POLY:def 7

          .= ( 0 + (q . x)) by A11, PRE_POLY:def 7

          .= ((p . x) + (q . x)) by A12, PRE_POLY:def 7;

        end;

      end;

      hence r = (p + q) by PRE_POLY: 33;

    end;

    theorem :: INT_7:3

    

     Th3: for X be set, p,q be ManySortedSet of X st (p | ( support p)) = (q | ( support q)) holds p = q

    proof

      let X be set, p,q be ManySortedSet of X;

      

       A1: ( dom (p | ( support p))) = (( dom p) /\ ( support p)) by RELAT_1: 61

      .= ( support p) by PRE_POLY: 37, XBOOLE_1: 28;

      

       A2: ( dom (q | ( support q))) = (( dom q) /\ ( support q)) by RELAT_1: 61

      .= ( support q) by PRE_POLY: 37, XBOOLE_1: 28;

      assume

       A3: (p | ( support p)) = (q | ( support q));

      

       A4: for x be object st x in X holds (p . x) = (q . x)

      proof

        let x be object;

        assume x in X;

        per cases ;

          suppose

           A5: x in ( support p);

          

          hence (p . x) = ((p | ( support p)) . x) by FUNCT_1: 49

          .= (q . x) by A3, A1, A2, A5, FUNCT_1: 49;

        end;

          suppose

           A6: not x in ( support p);

          

          hence (p . x) = 0 by PRE_POLY:def 7

          .= (q . x) by A3, A1, A2, A6, PRE_POLY:def 7;

        end;

      end;

      

       A7: ( dom q) = X by PARTFUN1:def 2;

      ( dom p) = X by PARTFUN1:def 2;

      hence thesis by A4, A7, FUNCT_1: 2;

    end;

    theorem :: INT_7:4

    

     Th4: for X be set, p,q be bag of X st ( support p) = {} & ( support q) = {} holds p = q

    proof

      let X be set, p,q be bag of X;

      assume that

       A1: ( support p) = {} and

       A2: ( support q) = {} ;

      

       A3: {} = (( dom q) /\ {} )

      .= ( dom (q | ( support q))) by A2;

      

       A4: ( dom (p | ( support p))) = (( dom p) /\ ( support p)) by RELAT_1: 61

      .= {} by A1;

      then for x be object st x in ( dom (p | ( support p))) holds ((p | ( support p)) . x) = ((q | ( support q)) . x);

      hence thesis by A4, A3, Th3, FUNCT_1: 2;

    end;

    

     Lm2: for p,q be bag of SetPrimes st ( support p) c= ( support q) & (p | ( support p)) = (q | ( support p)) holds ex r be bag of SetPrimes st ( support r) = (( support q) \ ( support p)) & ( support p) misses ( support r) & (r | ( support r)) = (q | ( support r)) & (p + r) = q

    proof

      deffunc G( object) = 0 ;

      let p,q be bag of SetPrimes ;

      assume that

       A1: ( support p) c= ( support q) and

       A2: (p | ( support p)) = (q | ( support p));

      deffunc F( object) = (q . $1);

      defpred C[ object] means $1 in (( support q) \ ( support p));

      

       A3: for x be object st x in SetPrimes holds ( C[x] implies F(x) in NAT ) & ( not C[x] implies G(x) in NAT ) by ORDINAL1:def 12;

      consider f be Function of SetPrimes , NAT such that

       A4: for x be object st x in SetPrimes holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A3);

      

       A5: for x be set st x in SetPrimes holds x in (( support q) \ ( support p)) implies (f . x) <> 0

      proof

        let x be set;

        assume that x in SetPrimes and

         A6: x in (( support q) \ ( support p));

        x in ( support q) by A6, XBOOLE_0:def 5;

        then (q . x) <> 0 by PRE_POLY:def 7;

        hence thesis by A4, A6;

      end;

      

       A7: for x st not x in SetPrimes holds (f . x) = 0

      proof

        let x;

        assume not x in SetPrimes ;

        then not x in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

      

       A8: for x holds x in (( support q) \ ( support p)) iff (f . x) <> 0

      proof

        let x;

        per cases ;

          suppose x in SetPrimes ;

          hence thesis by A4, A5;

        end;

          suppose not x in SetPrimes ;

          hence thesis by A7;

        end;

      end;

      then ( support f) is finite by PRE_POLY:def 7;

      then

      reconsider r = f as bag of SetPrimes by PRE_POLY:def 8;

      

       A9: (( support p) \/ ( support r)) = (( support p) \/ (( support q) \ ( support p))) by A8, PRE_POLY:def 7

      .= (( support p) \/ ( support q)) by XBOOLE_1: 39

      .= ( support q) by A1, XBOOLE_1: 12;

      

       A10: ( dom (f | ( support f))) = (( dom f) /\ ( support f)) by RELAT_1: 61

      .= ( support f) by PRE_POLY: 37, XBOOLE_1: 28;

      

       A11: ( support f) = (( support q) \ ( support p)) by A8, PRE_POLY:def 7;

      

       A12: for x be object st x in ( dom (f | ( support f))) holds ((f | ( support f)) . x) = ((q | ( support f)) . x)

      proof

        let x be object;

        assume

         A13: x in ( dom (f | ( support f)));

        then

         A14: ((q | ( support f)) . x) = (q . x) by A10, FUNCT_1: 49;

        ((f | ( support f)) . x) = (f . x) by A10, A13, FUNCT_1: 49;

        hence thesis by A4, A11, A10, A13, A14;

      end;

      ( dom (q | ( support f))) = (( dom q) /\ ( support f)) by RELAT_1: 61

      .= (( dom q) /\ (( support q) \ ( support p))) by A8, PRE_POLY:def 7

      .= ((( dom q) /\ ( support q)) \ ( support p)) by XBOOLE_1: 49

      .= (( support q) \ ( support p)) by PRE_POLY: 37, XBOOLE_1: 28

      .= ( support f) by A8, PRE_POLY:def 7;

      then

       A15: (f | ( support f)) = (q | ( support f)) by A10, A12, FUNCT_1:def 11;

      

       A16: ( support p) misses ( support f)

      proof

        assume ( support p) meets ( support f);

        then ex x be object st x in ( support p) & x in ( support f) by XBOOLE_0: 3;

        hence contradiction by A11, XBOOLE_0:def 5;

      end;

      then (( support p) /\ ( support f)) = {} by XBOOLE_0:def 7;

      then (p + r) = q by A2, A15, A9, Th2;

      hence thesis by A11, A16, A15;

    end;

    

     Lm3: for p be bag of SetPrimes , X be set st X c= ( support p) holds ex q,r be bag of SetPrimes st ( support q) = (( support p) \ X) & ( support r) = X & ( support q) misses ( support r) & (q | ( support q)) = (p | ( support q)) & (r | ( support r)) = (p | ( support r)) & (q + r) = p

    proof

      let p be bag of SetPrimes , X be set;

      set fq = (p +* (X --> 0 ));

      

       A1: ( rng fq) c= (( rng p) \/ ( rng (X --> 0 ))) by FUNCT_4: 17;

      

       A2: ( rng p) c= NAT by VALUED_0:def 6;

      then (( rng p) \/ ( rng (X --> 0 ))) c= NAT by XBOOLE_1: 8;

      then

       A3: ( rng fq) c= NAT by A1;

      set fr = (p +* (( SetPrimes \ X) --> 0 ));

      

       A4: ( dom fr) = (( dom p) \/ ( dom (( SetPrimes \ X) --> 0 ))) by FUNCT_4:def 1

      .= (( dom p) \/ ( SetPrimes \ X)) by FUNCOP_1: 13

      .= ( SetPrimes \/ ( SetPrimes \ X)) by PARTFUN1:def 2

      .= SetPrimes by XBOOLE_1: 12, XBOOLE_1: 36;

      

       A5: ( rng fr) c= (( rng p) \/ ( rng (( SetPrimes \ X) --> 0 ))) by FUNCT_4: 17;

      (( rng p) \/ ( rng (( SetPrimes \ X) --> 0 ))) c= NAT by A2, XBOOLE_1: 8;

      then ( rng fr) c= NAT by A5;

      then

      reconsider fr as Function of SetPrimes , NAT by A4, FUNCT_2:def 1, RELSET_1: 4;

      assume

       A6: X c= ( support p);

      

       A7: not x in X & x in SetPrimes implies (fr . x) = 0

      proof

        assume that

         A8: not x in X and

         A9: x in SetPrimes ;

        

         A10: x in ( SetPrimes \ X) by A8, A9, XBOOLE_0:def 5;

        then x in ( dom (( SetPrimes \ X) --> 0 )) by FUNCOP_1: 13;

        then (fr . x) = ((( SetPrimes \ X) --> 0 ) . x) by FUNCT_4: 13;

        hence thesis by A10, FUNCOP_1: 7;

      end;

      

       A11: ( dom (X --> 0 )) = X by FUNCOP_1: 13;

      

      then ( dom fq) = (( dom p) \/ X) by FUNCT_4:def 1

      .= ( SetPrimes \/ X) by PARTFUN1:def 2

      .= SetPrimes by A6, XBOOLE_1: 1, XBOOLE_1: 12;

      then

      reconsider fq as Function of SetPrimes , NAT by A3, FUNCT_2:def 1, RELSET_1: 4;

      

       A12: ( dom (fq | ( support fq))) = (( dom fq) /\ ( support fq)) by RELAT_1: 61

      .= ( support fq) by PRE_POLY: 37, XBOOLE_1: 28;

      

       A13: for x st not x in SetPrimes holds (fr . x) = 0 & (fq . x) = 0

      proof

        let x;

        assume

         A14: not x in SetPrimes ;

        then

         A15: not x in ( dom fr);

         not x in ( dom fq) by A14;

        hence thesis by A15, FUNCT_1:def 2;

      end;

      

       A16: x in X implies (fr . x) = (p . x)

      proof

        assume x in X;

        then not x in ( dom (( SetPrimes \ X) --> 0 )) by XBOOLE_0:def 5;

        hence thesis by FUNCT_4: 11;

      end;

      

       A17: for x st x in SetPrimes & x in X holds (fr . x) <> 0

      proof

        let x;

        assume that x in SetPrimes and

         A18: x in X;

        (p . x) <> 0 by A6, A18, PRE_POLY:def 7;

        hence thesis by A16, A18;

      end;

      

       A19: for x holds x in X iff (fr . x) <> 0

      proof

        let x;

        now

          per cases ;

            suppose x in SetPrimes ;

            hence thesis by A7, A17;

          end;

            suppose

             A20: not x in SetPrimes ;

            X c= SetPrimes by A6, XBOOLE_1: 1;

            hence thesis by A13, A20;

          end;

        end;

        hence thesis;

      end;

      then

       A21: ( support fr) = X by PRE_POLY:def 7;

      then

      reconsider r = fr as bag of SetPrimes by A6, PRE_POLY:def 8;

      

       A22: ( support p) c= ( dom p) by PRE_POLY: 37;

      

       A23: ( dom (fr | ( support fr))) = (( dom fr) /\ ( support fr)) by RELAT_1: 61

      .= ( support fr) by PRE_POLY: 37, XBOOLE_1: 28

      .= X by A19, PRE_POLY:def 7;

      

       A24: for x be object st x in ( dom (fr | ( support fr))) holds ((fr | ( support fr)) . x) = ((p | ( support fr)) . x)

      proof

        let x be object;

        assume

         A25: x in ( dom (fr | ( support fr)));

        then

         A26: ((p | ( support fr)) . x) = (p . x) by A21, A23, FUNCT_1: 49;

        ((fr | ( support fr)) . x) = (fr . x) by A21, A23, A25, FUNCT_1: 49;

        hence thesis by A16, A23, A25, A26;

      end;

      ( dom (p | ( support fr))) = (( dom p) /\ ( support fr)) by RELAT_1: 61

      .= (( dom p) /\ X) by A19, PRE_POLY:def 7

      .= X by A6, A22, XBOOLE_1: 1, XBOOLE_1: 28;

      then

       A27: (fr | ( support fr)) = (p | ( support fr)) by A23, A24, FUNCT_1:def 11;

      

       A28: x in X implies (fq . x) = 0

      proof

        assume

         A29: x in X;

        

        hence (fq . x) = ((X --> 0 ) . x) by A11, FUNCT_4: 13

        .= 0 by A29, FUNCOP_1: 7;

      end;

      

       A30: for x holds x in (( support p) \ X) iff (fq . x) <> 0

      proof

        let x;

        per cases ;

          suppose x in X;

          hence thesis by A28, XBOOLE_0:def 5;

        end;

          suppose

           A31: not x in X;

          then

           A32: (fq . x) = (p . x) by A11, FUNCT_4: 11;

          per cases ;

            suppose x in ( support p);

            hence thesis by A31, A32, PRE_POLY:def 7, XBOOLE_0:def 5;

          end;

            suppose not x in ( support p);

            hence thesis by A32, PRE_POLY:def 7, XBOOLE_0:def 5;

          end;

        end;

      end;

      then

       A33: ( support fq) = (( support p) \ X) by PRE_POLY:def 7;

      then

      reconsider q = fq as bag of SetPrimes by PRE_POLY:def 8;

      

       A34: ( dom (p | ( support fq))) = (( dom p) /\ ( support fq)) by RELAT_1: 61

      .= (( dom p) /\ (( support p) \ X)) by A30, PRE_POLY:def 7

      .= ((( dom p) /\ ( support p)) \ X) by XBOOLE_1: 49

      .= (( support p) \ X) by PRE_POLY: 37, XBOOLE_1: 28

      .= ( support fq) by A30, PRE_POLY:def 7;

      (( support p) \ X) misses X by XBOOLE_1: 79;

      then

       A35: (( support fq) /\ ( support fr)) = {} by A21, A33, XBOOLE_0:def 7;

      

       A36: for x be set st x in SetPrimes & x in ( support fq) holds (p . x) = (fq . x)

      proof

        let x be set;

        assume that x in SetPrimes and

         A37: x in ( support fq);

         not x in X by A21, A35, A37, XBOOLE_0:def 4;

        hence thesis by A11, FUNCT_4: 11;

      end;

      for x be object st x in ( dom (fq | ( support fq))) holds ((fq | ( support fq)) . x) = ((p | ( support fq)) . x)

      proof

        let x be object;

        assume

         A38: x in ( dom (fq | ( support fq)));

        then

         A39: ((p | ( support fq)) . x) = (p . x) by A12, FUNCT_1: 49;

        ((fq | ( support fq)) . x) = (fq . x) by A12, A38, FUNCT_1: 49;

        hence thesis by A12, A36, A38, A39;

      end;

      then

       A40: (fq | ( support fq)) = (p | ( support fq)) by A12, A34, FUNCT_1:def 11;

      (( support fr) \/ ( support fq)) = (( support fr) \/ (( support p) \ ( support fr))) by A19, A33, PRE_POLY:def 7

      .= (( support fr) \/ ( support p)) by XBOOLE_1: 39

      .= ( support p) by A6, A21, XBOOLE_1: 12;

      then (q + r) = p by A35, A40, A27, Th2;

      hence thesis by A21, A33, A40, A27, XBOOLE_1: 79;

    end;

    definition

      let p be bag of SetPrimes ;

      :: INT_7:def1

      attr p is prime-factorization-like means for x be Prime st x in ( support p) holds ex n be Nat st 0 < n & (p . x) = (x |^ n);

    end

    registration

      let n be non zero Nat;

      cluster ( ppf n) -> prime-factorization-like;

      coherence

      proof

        let p be Prime;

        assume

         A1: p in ( support ( ppf n));

        

         A2: (p |-count n) <> 0

        proof

          assume (p |-count n) = 0 ;

          then (( ppf n) . p) = 0 by NAT_3: 55;

          hence contradiction by A1, PRE_POLY:def 7;

        end;

        take (p |-count n);

        p in ( support ( pfexp n)) by A1, NAT_3:def 9;

        hence thesis by A2, NAT_3:def 9;

      end;

    end

    theorem :: INT_7:5

    

     Th5: for p,q be Prime, n,m be Nat st p divides (m * (q |^ n)) & p <> q holds p divides m

    proof

      let p,q be Prime;

      let n,m be Nat;

      assume that

       A1: p divides (m * (q |^ n)) and

       A2: p <> q;

      p divides m or p divides (q |^ n) by A1, NEWTON: 80;

      hence thesis by A2, NAT_3: 6;

    end;

    

     Lm4: for a be Prime, b be bag of SetPrimes st b is prime-factorization-like & a in ( support b) holds a divides ( Product b) & ex n be Nat st (a |^ n) divides ( Product b)

    proof

      let a be Prime, b be bag of SetPrimes ;

      assume that

       A1: b is prime-factorization-like and

       A2: a in ( support b);

      consider n be Nat such that

       A3: 0 < n and

       A4: (b . a) = (a |^ n) by A1, A2;

      

       A5: a divides (b . a) by A3, A4, NAT_3: 3;

      

       A6: ( rng b) c= NAT by VALUED_0:def 6;

      a in ( rng ( canFS ( support b))) by A2, FUNCT_2:def 3;

      then

      consider d be object such that

       A7: d in ( dom ( canFS ( support b))) and

       A8: a = (( canFS ( support b)) . d) by FUNCT_1:def 3;

      consider f be FinSequence of COMPLEX such that

       A9: ( Product b) = ( Product f) and

       A10: f = (b * ( canFS ( support b))) by NAT_3:def 5;

      ( rng f) c= ( rng b) by A10, RELAT_1: 26;

      then ( rng f) c= NAT by A6;

      then

      reconsider f as FinSequence of NAT by FINSEQ_1:def 4;

      

       A11: ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

      ( support b) c= ( dom b) by PRE_POLY: 37;

      then

       A12: ( dom f) = ( dom ( canFS ( support b))) by A10, A11, RELAT_1: 27;

      then (b . a) = ((b * ( canFS ( support b))) . d) by A10, A7, A8, FUNCT_1: 12;

      then (b . a) in ( rng f) by A10, A12, A7, FUNCT_1: 3;

      then (a |^ n) divides ( Product f) by A4, NAT_3: 7;

      hence thesis by A9, A4, A5, NAT_D: 4;

    end;

    

     Lm5: for p be FinSequence of NAT , x be Element of NAT , b be bag of SetPrimes st b is prime-factorization-like & (p ^ <*x*>) = (b * ( canFS ( support b))) holds ex p1 be FinSequence of NAT , q be Prime, n be Element of NAT , b1 be bag of SetPrimes st 0 < n & b1 is prime-factorization-like & q in ( support b) & ( support b1) = (( support b) \ {q}) & x = (q |^ n) & ( len p1) = ( len p) & ( Product p) = ( Product p1) & p1 = (b1 * ( canFS ( support b1)))

    proof

      deffunc G( set) = 0 ;

      let p be FinSequence of NAT , x be Element of NAT , b be bag of SetPrimes ;

      assume that

       A1: b is prime-factorization-like and

       A2: (p ^ <*x*>) = (b * ( canFS ( support b)));

      

       A3: ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

      ( dom b) = SetPrimes by PARTFUN1:def 2;

      then

       A4: ( dom (b * ( canFS ( support b)))) = ( dom ( canFS ( support b))) by A3, RELAT_1: 27;

      p = ((b * ( canFS ( support b))) | ( dom p)) by A2, FINSEQ_1: 21;

      then ( dom p) = (( dom (b * ( canFS ( support b)))) /\ ( dom p)) by RELAT_1: 61;

      then

       A5: ( dom (( canFS ( support b)) | ( dom p))) = ( dom p) by A4, RELAT_1: 62, XBOOLE_1: 17;

      deffunc F( set) = (b . $1);

      

       A6: ( card ( support b)) = ( len ( canFS ( support b))) by FINSEQ_1: 93;

      ( dom b) = SetPrimes by PARTFUN1:def 2;

      then

       A7: ( dom (b * ( canFS ( support b)))) = ( dom ( canFS ( support b))) by A3, RELAT_1: 27;

      

       A8: (( len p) + 1) in ( Seg (( len p) + 1)) by FINSEQ_1: 4;

      

       A9: ( len <*x*>) = 1 by FINSEQ_1: 40;

      then ( len (p ^ <*x*>)) = (( len p) + 1) by FINSEQ_1: 22;

      then

       A10: (( len p) + 1) in ( dom (b * ( canFS ( support b)))) by A2, A8, FINSEQ_1:def 3;

      

       A11: x = ((p ^ <*x*>) . (( len p) + 1)) by FINSEQ_1: 42

      .= (b . (( canFS ( support b)) . (( len p) + 1))) by A2, A7, A10, FUNCT_1: 13;

      

       A12: ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

      then

       A13: (( canFS ( support b)) . (( len p) + 1)) in ( support b) by A7, A10, FUNCT_1: 3;

      then

      reconsider q = (( canFS ( support b)) . (( len p) + 1)) as Prime by NEWTON:def 6;

      defpred P[ set] means $1 in (( support b) \ {q});

      consider b1 be ManySortedSet of SetPrimes such that

       A14: for i be Element of SetPrimes st i in SetPrimes holds ( P[i] implies (b1 . i) = F(i)) & ( not P[i] implies (b1 . i) = G(i)) from PRE_CIRC:sch 2;

      

       A15: ( rng b1) c= NAT

      proof

        let y be object;

        assume y in ( rng b1);

        then

        consider x be object such that

         A16: x in ( dom b1) and

         A17: y = (b1 . x) by FUNCT_1:def 3;

        reconsider x as Element of SetPrimes by A16;

        (b1 . x) in NAT

        proof

          per cases ;

            suppose x in (( support b) \ {q});

            then (b1 . x) = (b . x) by A14;

            hence thesis;

          end;

            suppose not x in (( support b) \ {q});

            then (b1 . x) = 0 by A14;

            hence thesis;

          end;

        end;

        hence thesis by A17;

      end;

      now

        let z be object;

        assume

         A18: z in ( support b1);

        z in ( dom b1)

        proof

          assume not z in ( dom b1);

          then (b1 . z) = {} by FUNCT_1:def 2;

          hence contradiction by A18, PRE_POLY:def 7;

        end;

        then

        reconsider y = z as Element of SetPrimes ;

        assume

         A19: not z in (( support b) \ {q});

        (b1 . y) <> 0 by A18, PRE_POLY:def 7;

        hence contradiction by A14, A19;

      end;

      then

       A20: ( support b1) c= (( support b) \ {q});

      now

        let z be object;

        assume

         A21: z in (( support b) \ {q});

        then

         A22: z in ( support b) by XBOOLE_0:def 5;

        reconsider y = z as Element of SetPrimes by A21;

        (b1 . y) = (b . y) by A14, A21;

        then (b1 . y) <> 0 by A22, PRE_POLY:def 7;

        hence z in ( support b1) by PRE_POLY:def 7;

      end;

      then

       A23: (( support b) \ {q}) c= ( support b1);

      then

       A24: ( support b1) = (( support b) \ {q}) by A20, XBOOLE_0:def 10;

      reconsider b1 as bag of SetPrimes by A20, A15, PRE_POLY:def 8, VALUED_0:def 6;

      consider n be Nat such that

       A25: 0 < n and

       A26: (b . q) = (q |^ n) by A1, A13;

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

      

       A27: ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

       SetPrimes = ( dom b) by PARTFUN1:def 2;

      

      then ( card ( dom (b * ( canFS ( support b))))) = ( card ( dom ( canFS ( support b)))) by A27, RELAT_1: 27

      .= ( card ( Seg ( len ( canFS ( support b))))) by FINSEQ_1:def 3

      .= ( card ( len ( canFS ( support b)))) by FINSEQ_1: 55

      .= ( len ( canFS ( support b)));

      

      then

       A28: ( len ( canFS ( support b))) = ( card ( Seg ( len (p ^ <*x*>)))) by A2, FINSEQ_1:def 3

      .= ( card ( len (p ^ <*x*>))) by FINSEQ_1: 55

      .= (( len p) + 1) by A9, FINSEQ_1: 22;

      ( card (( support b) \ {q})) = (( card ( support b)) - ( card {q})) by A7, A12, A10, EULER_1: 4, FUNCT_1: 3

      .= (( card ( support b)) - 1) by CARD_1: 30;

      then

       A29: ( len ( canFS ( support b1))) = ( len p) by A24, A28, A6, FINSEQ_1: 93;

      then

       A30: ( dom ( canFS ( support b1))) = ( Seg ( len p)) by FINSEQ_1:def 3;

      then

       A31: ( dom ( canFS ( support b1))) = ( dom p) by FINSEQ_1:def 3;

       A32:

      now

        let x be Prime;

        assume

         A33: x in ( support b1);

        (( support b) \ {q}) c= ( support b) by XBOOLE_1: 36;

        then

        consider m be Nat such that

         A34: 0 < m and

         A35: (b . x) = (x |^ m) by A1, A24, A33;

        take m;

        thus 0 < m by A34;

        thus (b1 . x) = (x |^ m) by A14, A20, A33, A35;

      end;

      per cases ;

        suppose

         A36: ( dom p) = {} ;

        set p1 = (b1 * ( canFS ( support b1)));

        

         A37: p = {} by A36;

        ( Seg ( len ( canFS ( support b1)))) = ( dom ( canFS ( support b1))) by FINSEQ_1:def 3

        .= ( Seg ( len p)) by A29, FINSEQ_1:def 3

        .= ( Seg 0 ) by A37;

        then ( canFS ( support b1)) = {} ;

        then

         A38: p1 = ( <*> NAT );

        then

        reconsider p1 as FinSequence of NAT ;

        take p1, q, n, b1;

        thus thesis by A7, A12, A10, A11, A25, A26, A20, A23, A32, A36, A38, FUNCT_1: 3, RELAT_1: 41, XBOOLE_0:def 10;

      end;

        suppose

         A39: ( dom p) <> {} ;

        

         A40: ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

        now

          let y be object;

          assume

           A41: y in (( support b) \ {q});

          then y in ( rng ( canFS ( support b))) by A40, XBOOLE_0:def 5;

          then

          consider x be object such that

           A42: x in ( dom ( canFS ( support b))) and

           A43: y = (( canFS ( support b)) . x) by FUNCT_1:def 3;

          

           A44: x in ( dom p)

          proof

            assume not x in ( dom p);

            then

             A45: not x in ( Seg ( len p)) by FINSEQ_1:def 3;

            

             A46: x in ( Seg (( len p) + 1)) by A28, A42, FINSEQ_1:def 3;

            reconsider x as Element of NAT by A42;

            1 <= x by A46, FINSEQ_1: 1;

            then ( len p) < x by A45;

            then

             A47: (( len p) + 1) <= x by NAT_1: 13;

            x <= (( len p) + 1) by A46, FINSEQ_1: 1;

            then x = (( len p) + 1) by A47, XXREAL_0: 1;

            then y in {q} by A43, TARSKI:def 1;

            hence contradiction by A41, XBOOLE_0:def 5;

          end;

          then x in (( dom ( canFS ( support b))) /\ ( dom p)) by A42, XBOOLE_0:def 4;

          then

           A48: x in ( dom (( canFS ( support b)) | ( dom p))) by RELAT_1: 61;

          y = ((( canFS ( support b)) | ( dom p)) . x) by A43, A44, FUNCT_1: 49;

          hence y in ( rng (( canFS ( support b)) | ( dom p))) by A48, FUNCT_1: 3;

        end;

        then

         A49: (( support b) \ {q}) c= ( rng (( canFS ( support b)) | ( dom p)));

        now

          let y be object;

          assume y in ( rng (( canFS ( support b)) | ( dom p)));

          then

          consider x be object such that

           A50: x in ( dom (( canFS ( support b)) | ( dom p))) and

           A51: y = ((( canFS ( support b)) | ( dom p)) . x) by FUNCT_1:def 3;

          

           A52: y = (( canFS ( support b)) . x) by A50, A51, FUNCT_1: 47;

          

           A53: x in (( dom ( canFS ( support b))) /\ ( dom p)) by A50, RELAT_1: 61;

          then

           A54: x in ( dom ( canFS ( support b))) by XBOOLE_0:def 4;

          

           A55: x in ( dom p) by A53, XBOOLE_0:def 4;

          y <> q

          proof

            (( len p) + 1) in ( Seg (( len p) + 1)) by FINSEQ_1: 4;

            then

             A56: (( len p) + 1) in ( dom ( canFS ( support b))) by A28, FINSEQ_1:def 3;

            assume y = q;

            then (( len p) + 1) = x by A52, A54, A56, FUNCT_1:def 4;

            then

             A57: (( len p) + 1) in ( Seg ( len p)) by A55, FINSEQ_1:def 3;

            (( len p) + 0 ) < (1 + ( len p)) by XREAL_1: 8;

            hence contradiction by A57, FINSEQ_1: 1;

          end;

          then

           A58: not y in {q} by TARSKI:def 1;

          y in ( rng ( canFS ( support b))) by A52, A54, FUNCT_1: 3;

          hence y in (( support b) \ {q}) by A58, XBOOLE_0:def 5;

        end;

        then ( rng (( canFS ( support b)) | ( dom p))) c= (( support b) \ {q});

        then

         A59: ( rng (( canFS ( support b)) | ( dom p))) = (( support b) \ {q}) by A49, XBOOLE_0:def 10;

        then

        reconsider L0 = (( canFS ( support b)) | ( dom p)) as Function of ( dom p), (( support b) \ {q}) by A5, FUNCT_2: 1;

        

         A60: L0 is one-to-one by FUNCT_1: 52;

        then

         A61: ( dom (L0 " )) = (( support b) \ {q}) by A59, FUNCT_1: 33;

        

         A62: (( support b) \ {q}) <> {} by A20, A30, A39, FINSEQ_1:def 3;

        then ( dom L0) = ( dom p) by FUNCT_2:def 1;

        then

         A63: ( rng (L0 " )) = ( dom p) by A60, FUNCT_1: 33;

        then

        reconsider LL1 = (L0 " ) as Function of (( support b) \ {q}), ( dom p) by A61, FUNCT_2: 1;

        

         A64: ( rng ( canFS ( support b1))) = ( support b1) by FUNCT_2:def 3;

        then ( canFS ( support b1)) is Function of ( dom p), (( support b) \ {q}) by A24, A31, FUNCT_2: 1;

        then

        reconsider L0L = (LL1 * ( canFS ( support b1))) as Function of ( dom p), ( dom p) by A62, FUNCT_2: 13;

        

         A65: L0 is one-to-one by FUNCT_1: 52;

        ( rng L0L) = ( dom p) by A23, A61, A63, A64, RELAT_1: 28;

        then L0L is onto by FUNCT_2:def 3;

        then

        reconsider LL = L0L as Permutation of ( dom p) by A65;

        ((( canFS ( support b)) | ( dom p)) * LL) = (((( canFS ( support b)) | ( dom p)) * LL1) * ( canFS ( support b1))) by RELAT_1: 36

        .= (( id ( support b1)) * ( canFS ( support b1))) by A24, A62, A59, A65, FUNCT_2: 29

        .= ( canFS ( support b1)) by FUNCT_2: 17;

        then

         A66: (( canFS ( support b1)) * (LL " )) = ((( canFS ( support b)) | ( dom p)) * (LL * (LL " ))) by RELAT_1: 36;

        reconsider FS = ( canFS ( support b1)) as FinSequence;

        reconsider L = (LL " ) as Permutation of ( dom p);

        

         A67: ( rng L) = ( dom FS) by A31, FUNCT_2:def 3;

        

        then

         A68: ( dom (FS * L)) = ( dom L) by RELAT_1: 27

        .= ( dom p) by A39, FUNCT_2:def 1;

        set p1 = (b1 * FS);

        

         A69: ( rng ( canFS ( support b1))) = ( support b1) by FUNCT_2:def 3;

         SetPrimes = ( dom b1) by PARTFUN1:def 2;

        then

         A70: ( dom (b1 * FS)) = ( dom p) by A31, A69, RELAT_1: 27;

        then ( dom p1) = ( Seg ( len p)) by FINSEQ_1:def 3;

        then

         A71: p1 is FinSequence by FINSEQ_1:def 2;

        

         A72: ( rng (FS * L)) = ( rng FS) by A67, RELAT_1: 28

        .= (( support b) \ {q}) by A24, FUNCT_2:def 3;

         SetPrimes = ( dom b1) by PARTFUN1:def 2;

        then

         A73: ( dom p) = ( dom (b1 * (FS * L))) by A68, A72, RELAT_1: 27;

        ( rng LL) = ( dom p) by FUNCT_2:def 3;

        then

         A74: (( canFS ( support b1)) * (LL " )) = ((( canFS ( support b)) | ( dom p)) * ( id ( dom p))) by A39, A66, FUNCT_2: 29;

        now

          let k be object;

          

           A75: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

          assume

           A76: k in ( dom p);

          then

           A77: ((FS * L) . k) in (( support b) \ {q}) by A68, A72, FUNCT_1: 3;

          

          thus (p . k) = ((p ^ <*x*>) . k) by A76, FINSEQ_1:def 7

          .= (b . (( canFS ( support b)) . k)) by A2, A76, A75, FUNCT_1: 12

          .= (b . ((( canFS ( support b)) | ( dom p)) . k)) by A76, FUNCT_1: 49

          .= (b . ((FS * L) . k)) by A74, FUNCT_2: 17

          .= (b1 . ((FS * L) . k)) by A14, A77

          .= ((b1 * (FS * L)) . k) by A73, A76, FUNCT_1: 12;

        end;

        

        then p = (b1 * (FS * L)) by A73, FUNCT_1: 2

        .= (p1 * L) by RELAT_1: 36;

        then

         A78: (p,p1) are_fiberwise_equipotent by A70, CLASSES1: 80;

        ( rng p1) c= NAT by VALUED_0:def 6;

        then

        reconsider p1 as FinSequence of NAT by A71, FINSEQ_1:def 4;

        take p1, q, n, b1;

        ( Seg ( len p1)) = ( dom p) by A70, FINSEQ_1:def 3;

        hence thesis by A7, A12, A10, A11, A25, A26, A20, A23, A32, A78, EULER_2: 10, FINSEQ_1:def 3, FUNCT_1: 3, XBOOLE_0:def 10;

      end;

    end;

    

     Lm6: for i be Element of NAT , f be FinSequence of NAT , b be bag of SetPrimes , a be Prime st ( len f) = i & b is prime-factorization-like & ( Product b) <> 1 & a divides ( Product b) & ( Product b) = ( Product f) & f = (b * ( canFS ( support b))) holds a in ( support b)

    proof

      defpred P[ Nat] means for f be FinSequence of NAT , b be bag of SetPrimes , a be Prime st ( len f) = $1 & b is prime-factorization-like & ( Product b) <> 1 & a divides ( Product b) & ( Product b) = ( Product f) & f = (b * ( canFS ( support b))) holds a in ( support b);

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        thus P[(k + 1)]

        proof

          

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

          let f be FinSequence of NAT , b be bag of SetPrimes , a be Prime;

          assume that

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

           A5: b is prime-factorization-like and ( Product b) <> 1 and

           A6: a divides ( Product b) and

           A7: ( Product b) = ( Product f) and

           A8: f = (b * ( canFS ( support b)));

          reconsider p = (f | k) as FinSequence of NAT ;

          reconsider x = (f . (k + 1)) as Element of NAT ;

          

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

          

           A10: f = ((f | k) ^ <*(f /. ( len f))*>) by A4, FINSEQ_5: 21

          .= (p ^ <*x*>) by A4, A3, FINSEQ_4: 15;

          then

          consider p1 be FinSequence of NAT , q be Prime, n be Element of NAT , b1 be bag of SetPrimes such that 0 < n and

           A11: b1 is prime-factorization-like and

           A12: q in ( support b) and

           A13: ( support b1) = (( support b) \ {q}) and

           A14: x = (q |^ n) and

           A15: ( len p1) = ( len p) and

           A16: ( Product p) = ( Product p1) and

           A17: p1 = (b1 * ( canFS ( support b1))) by A5, A8, Lm5;

          

           A18: ( Product f) = (( Product p1) * x) by A10, A16, RVSUM_1: 96;

          ( rng p1) c= COMPLEX by NUMBERS: 20;

          then p1 is FinSequence of COMPLEX by FINSEQ_1:def 4;

          then

           A19: ( Product b1) = ( Product p1) by A17, NAT_3:def 5;

          now

            per cases ;

              suppose

               A20: ( Product p1) = 1;

              a <> 1 by INT_2:def 4;

              then ex k be Element of NAT st a = (q * k) by A6, A7, A14, A18, A20, PEPIN: 32;

              then

               A21: q divides a by INT_1:def 3;

              q <> 1 by INT_2:def 4;

              hence thesis by A12, A21, INT_2:def 4;

            end;

              suppose

               A22: ( Product p1) <> 1;

              per cases ;

                suppose a = q;

                hence thesis by A12;

              end;

                suppose

                 A23: a <> q;

                

                 A24: ( support b1) c= ( support b) by A13, XBOOLE_1: 36;

                a in ( support b1) by A2, A6, A7, A9, A11, A14, A15, A17, A18, A19, A22, A23, Th5;

                hence thesis by A24;

              end;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A25: P[ 0 ]

      proof

        let f be FinSequence of NAT , b be bag of SetPrimes , a be Prime;

        assume ( len f) = 0 ;

        then f = ( <*> NAT );

        hence thesis by RVSUM_1: 94;

      end;

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

      hence thesis;

    end;

    theorem :: INT_7:6

    

     Th6: for f be FinSequence of NAT , b be bag of SetPrimes , a be Prime st b is prime-factorization-like & ( Product b) <> 1 & a divides ( Product b) & ( Product b) = ( Product f) & f = (b * ( canFS ( support b))) holds a in ( support b)

    proof

      let f be FinSequence of NAT , b be bag of SetPrimes , a be Prime;

      assume that

       A1: b is prime-factorization-like and

       A2: ( Product b) <> 1 and

       A3: a divides ( Product b) and

       A4: ( Product b) = ( Product f) and

       A5: f = (b * ( canFS ( support b)));

      ( len f) is Element of NAT ;

      hence thesis by A1, A2, A3, A4, A5, Lm6;

    end;

    

     Lm7: for a be Prime, b be bag of SetPrimes st b is prime-factorization-like & a divides ( Product b) holds a in ( support b)

    proof

      let a be Prime, b be bag of SetPrimes ;

      assume that

       A1: b is prime-factorization-like and

       A2: a divides ( Product b);

      per cases ;

        suppose

         A3: ( Product b) = 1;

        a <> 1 by INT_2:def 4;

        hence thesis by A2, A3, WSIERP_1: 15;

      end;

        suppose

         A4: ( Product b) <> 1;

        

         A5: ( rng b) c= NAT by VALUED_0:def 6;

        consider f be FinSequence of COMPLEX such that

         A6: ( Product b) = ( Product f) and

         A7: f = (b * ( canFS ( support b))) by NAT_3:def 5;

        ( rng f) c= ( rng b) by A7, RELAT_1: 26;

        then ( rng f) c= NAT by A5;

        then

        reconsider f as FinSequence of NAT by FINSEQ_1:def 4;

        ( Product b) = ( Product f) by A6;

        hence thesis by A1, A2, A4, A7, Th6;

      end;

    end;

    theorem :: INT_7:7

    

     Th7: for p,q be bag of SetPrimes st ( support p) c= ( support q) & (p | ( support p)) = (q | ( support p)) holds ( Product p) divides ( Product q)

    proof

      let p,q be bag of SetPrimes ;

      assume that

       A1: ( support p) c= ( support q) and

       A2: (p | ( support p)) = (q | ( support p));

      consider r be bag of SetPrimes such that ( support r) = (( support q) \ ( support p)) and

       A3: ( support p) misses ( support r) and (r | ( support r)) = (q | ( support r)) and

       A4: (p + r) = q by A1, A2, Lm2;

      (( Product p) * ( Product r)) = ( Product q) by A3, A4, NAT_3: 19;

      hence thesis by INT_1:def 3;

    end;

    theorem :: INT_7:8

    for p be bag of SetPrimes , x be Prime st p is prime-factorization-like holds x divides ( Product p) iff x in ( support p) by Lm4, Lm7;

    theorem :: INT_7:9

    

     Th9: for n,m,k be non zero Nat st k = (n lcm m) holds ( support ( ppf k)) = (( support ( ppf n)) \/ ( support ( ppf m)))

    proof

      let n,m,k be non zero Nat;

      assume

       A1: k = (n lcm m);

      

       A2: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9;

      

       A3: (( support ( pfexp n)) \/ ( support ( pfexp m))) c= ( support ( max (( pfexp n),( pfexp m))))

      proof

        let x be object;

        assume

         A4: x in (( support ( pfexp n)) \/ ( support ( pfexp m)));

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in ( support ( pfexp n));

          

           A6: (( pfexp n) . x) <= (( max (( pfexp n),( pfexp m))) . x)

          proof

            per cases ;

              suppose (( pfexp n) . x) <= (( pfexp m) . x);

              hence thesis by NAT_3:def 4;

            end;

              suppose (( pfexp n) . x) > (( pfexp m) . x);

              hence thesis by NAT_3:def 4;

            end;

          end;

          (( pfexp n) . x) <> 0 by A5, PRE_POLY:def 7;

          then 0 < (( pfexp n) . x);

          hence thesis by A6, PRE_POLY:def 7;

        end;

          suppose

           A7: x in ( support ( pfexp m));

          

           A8: (( pfexp m) . x) <= (( max (( pfexp n),( pfexp m))) . x)

          proof

            per cases ;

              suppose (( pfexp n) . x) <= (( pfexp m) . x);

              hence thesis by NAT_3:def 4;

            end;

              suppose (( pfexp n) . x) > (( pfexp m) . x);

              hence thesis by NAT_3:def 4;

            end;

          end;

          (( pfexp m) . x) <> 0 by A7, PRE_POLY:def 7;

          then 0 < (( pfexp m) . x);

          hence thesis by A8, PRE_POLY:def 7;

        end;

      end;

      

       A9: ( support ( ppf m)) = ( support ( pfexp m)) by NAT_3:def 9;

      

       A10: ( support ( ppf k)) = ( support ( pfexp k)) by NAT_3:def 9

      .= ( support ( max (( pfexp n),( pfexp m)))) by A1, NAT_3: 54;

      then ( support ( ppf k)) c= (( support ( ppf n)) \/ ( support ( ppf m))) by A2, A9, NAT_3: 18;

      hence thesis by A10, A2, A9, A3, XBOOLE_0:def 10;

    end;

    theorem :: INT_7:10

    

     Th10: for X be set, b1,b2 be bag of X holds ( support ( min (b1,b2))) = (( support b1) /\ ( support b2))

    proof

      let X be set;

      let b1,b2 be bag of X;

      set f = ( min (b1,b2));

      

       A1: for x be object holds x in ( support ( min (b1,b2))) implies x in ( support b1) & x in ( support b2)

      proof

        let x be object;

        assume

         A2: x in ( support ( min (b1,b2)));

        assume

         A3: not x in ( support b1) or not x in ( support b2);

        now

          per cases ;

            case

             A4: (b1 . x) <= (b2 . x);

            

             A5: not x in ( support b1)

            proof

              assume

               A6: x in ( support b1);

              then

               A7: (b1 . x) <> 0 by PRE_POLY:def 7;

              (b2 . x) = 0 by A3, A6, PRE_POLY:def 7;

              hence contradiction by A4, A7;

            end;

            (f . x) = (b1 . x) by A4, NAT_3:def 3

            .= 0 by A5, PRE_POLY:def 7;

            hence contradiction by A2, PRE_POLY:def 7;

          end;

            case

             A8: (b2 . x) < (b1 . x);

            

            then (f . x) = (b2 . x) by NAT_3:def 3

            .= 0 by A3, A8, PRE_POLY:def 7;

            hence contradiction by A2, PRE_POLY:def 7;

          end;

        end;

        hence thesis;

      end;

      for x be object holds x in ( support b1) & x in ( support b2) implies x in ( support ( min (b1,b2)))

      proof

        let x be object;

        assume that

         A9: x in ( support b1) and

         A10: x in ( support b2);

        

         A11: (b2 . x) <> 0 by A10, PRE_POLY:def 7;

        

         A12: (f . x) = (b1 . x) or (f . x) = (b2 . x) by NAT_3:def 3;

        (b1 . x) <> 0 by A9, PRE_POLY:def 7;

        hence thesis by A11, A12, PRE_POLY:def 7;

      end;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: INT_7:11

    for n,m,k be non zero Nat st k = (n gcd m) holds ( support ( ppf k)) = (( support ( ppf n)) /\ ( support ( ppf m)))

    proof

      let n,m,k be non zero Nat;

      assume

       A1: k = (n gcd m);

      

       A2: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9;

      

       A3: ( support ( ppf m)) = ( support ( pfexp m)) by NAT_3:def 9;

      ( support ( ppf k)) = ( support ( pfexp k)) by NAT_3:def 9

      .= ( support ( min (( pfexp n),( pfexp m)))) by A1, NAT_3: 53;

      hence thesis by A2, A3, Th10;

    end;

    theorem :: INT_7:12

    

     Th12: for p,q be bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & ( support p) misses ( support q) holds (( Product p),( Product q)) are_coprime

    proof

      let p,q be bag of SetPrimes ;

      assume that

       A1: p is prime-factorization-like and

       A2: q is prime-factorization-like and

       A3: ( support p) misses ( support q);

      assume not (( Product p),( Product q)) are_coprime ;

      then

      consider x be prime Nat such that

       A4: x divides ( Product p) and

       A5: x divides ( Product q) by PYTHTRIP:def 2;

      

       A6: x in ( support q) by A2, A5, Lm7;

      x in ( support p) by A1, A4, Lm7;

      hence contradiction by A3, A6, XBOOLE_0: 3;

    end;

    

     Lm8: for q be Prime, g be Element of NAT st g <> 0 holds ex p1 be bag of SetPrimes st p1 = (( SetPrimes --> 0 ) +* (q,g)) & ( support p1) = {q} & ( Product p1) = g

    proof

      let q be Prime, g be Element of NAT ;

      set p = (( SetPrimes --> 0 ) +* (q,g));

      reconsider p as ManySortedSet of SetPrimes ;

      ( dom ( SetPrimes --> 0 )) = SetPrimes by FUNCOP_1: 13;

      then q in ( dom ( SetPrimes --> 0 )) by NEWTON:def 6;

      then

       A1: (p . q) = g by FUNCT_7: 31;

      

       A2: for x st not x in {q} holds (p . x) = 0

      proof

        let x;

        assume not x in {q};

        then x <> q by TARSKI:def 1;

        hence thesis by Lm1;

      end;

      now

        let z be set;

        assume

         A3: z in ( support p);

        z in ( dom p)

        proof

          assume not z in ( dom p);

          then (p . z) = {} by FUNCT_1:def 2;

          hence contradiction by A3, PRE_POLY:def 7;

        end;

        then

        reconsider y = z as Element of SetPrimes ;

        assume not z in {q};

        (p . y) <> 0 by A3, PRE_POLY:def 7;

        hence z in {q} by A2;

      end;

      then for z be object st z in ( support p) holds z in {q};

      then

       A4: ( support p) c= {q};

      assume

       A5: g <> 0 ;

      now

        let z be object;

        assume z in {q};

        then

         A6: z = q by TARSKI:def 1;

        thus z in ( support p) by A5, A1, A6, PRE_POLY:def 7;

      end;

      then

       A7: {q} c= ( support p);

      then

       A8: ( support p) = {q} by A4, XBOOLE_0:def 10;

      reconsider p as bag of SetPrimes by A4, PRE_POLY:def 8;

      

       A9: q in ( support p) by A8, TARSKI:def 1;

      

       A10: q in ( dom p)

      proof

        assume not q in ( dom p);

        then (p . q) = {} by FUNCT_1:def 2;

        hence contradiction by A9, PRE_POLY:def 7;

      end;

      take p;

      consider f be FinSequence of COMPLEX such that

       A11: ( Product p) = ( Product f) and

       A12: f = (p * ( canFS ( support p))) by NAT_3:def 5;

      f = (p * <*q*>) by A8, A12, FINSEQ_1: 94;

      then f = <*(p . q)*> by A10, FINSEQ_2: 34;

      hence thesis by A1, A4, A7, A11, RVSUM_1: 95, XBOOLE_0:def 10;

    end;

    

     Lm9: for p be bag of SetPrimes , x be Prime st p is prime-factorization-like & x in ( support p) & (p . x) = x holds ex p1,r1 be bag of SetPrimes st p1 is prime-factorization-like & ( support r1) = {x} & ( Product r1) = x & ( support p1) = (( support p) \ {x}) & (p1 | ( support p1)) = (p | ( support p1)) & ( Product p) = (( Product p1) * x)

    proof

      let p be bag of SetPrimes , x be Prime;

      assume that

       A1: p is prime-factorization-like and

       A2: x in ( support p) and

       A3: (p . x) = x;

      consider nx be Nat such that

       A4: 0 < nx and

       A5: (p . x) = (x |^ nx) by A1, A2;

      consider mx be Nat such that

       A6: nx = (mx + 1) by A4, NAT_1: 6;

      

       A7: mx = 0

      proof

        assume mx <> 0 ;

        then

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

        1 < x by INT_2:def 4;

        then (x to_power 1) < (x to_power nx) by A6, A8, POWER: 39;

        then (x |^ 1) < (x to_power nx) by POWER: 41;

        then (x |^ 1) < (x |^ nx) by POWER: 41;

        hence contradiction by A3, A5;

      end;

       {x} c= ( support p) by A2, ZFMISC_1: 31;

      then

      consider q,r be bag of SetPrimes such that

       A9: ( support q) = (( support p) \ {x}) and

       A10: ( support r) = {x} and

       A11: ( support q) misses ( support r) and

       A12: (q | ( support q)) = (p | ( support q)) and

       A13: (r | ( support r)) = (p | ( support r)) and

       A14: (q + r) = p by Lm3;

      

       A15: r = (( SetPrimes --> 0 ) +* (x,(r . x))) by A10, Th1;

      now

        let z be Prime;

        assume

         A16: z in ( support q);

        ( support q) c= ( support p) by A9, XBOOLE_1: 36;

        then

        consider n be Nat such that

         A17: 0 < n and

         A18: (p . z) = (z |^ n) by A1, A16;

        take n;

        (q . z) = ((q | ( support q)) . z) by A16, FUNCT_1: 49

        .= (p . z) by A12, A16, FUNCT_1: 49;

        hence 0 < n & (q . z) = (z |^ n) by A17, A18;

      end;

      then

       A19: q is prime-factorization-like;

      

       A20: x in ( support r) by A10, TARSKI:def 1;

      

      then (r . x) = ((r | ( support r)) . x) by FUNCT_1: 49

      .= (p . x) by A13, A20, FUNCT_1: 49

      .= x by A5, A6, A7;

      then

       A21: ex rr1 be bag of SetPrimes st rr1 = r & ( support rr1) = {x} & ( Product rr1) = x by A15, Lm8;

      (( Product q) * ( Product r)) = ( Product p) by A11, A14, NAT_3: 19;

      hence thesis by A9, A12, A19, A21;

    end;

    

     Lm10: for p be bag of SetPrimes , x be Prime st p is prime-factorization-like & x in ( support p) & (p . x) <> x holds ex p1,r1 be bag of SetPrimes st p1 is prime-factorization-like & ( support r1) = {x} & ( Product r1) = x & ( support p1) = ( support p) & (p1 | (( support p1) \ {x})) = (p | (( support p1) \ {x})) & (p . x) = ((p1 . x) * x) & ( Product p) = (( Product p1) * x)

    proof

      let p be bag of SetPrimes , x be Prime;

      assume that

       A1: p is prime-factorization-like and

       A2: x in ( support p) and

       A3: (p . x) <> x;

      consider nx be Nat such that

       A4: 0 < nx and

       A5: (p . x) = (x |^ nx) by A1, A2;

      consider mx be Nat such that

       A6: nx = (mx + 1) by A4, NAT_1: 6;

      

       A7: mx <> 0 by A3, A5, A6;

      

       A8: ( dom ( SetPrimes --> 0 )) = SetPrimes by FUNCOP_1: 13;

      then

       A9: x in ( dom ( SetPrimes --> 0 )) by NEWTON:def 6;

      set r10 = (( SetPrimes --> 0 ) +* (x,x));

      x is Element of NAT by ORDINAL1:def 12;

      then

       A10: ex r1 be bag of SetPrimes st r1 = r10 & ( support r1) = {x} & ( Product r1) = x by Lm8;

      

       A11: {x} c= ( support p) by A2, ZFMISC_1: 31;

      then

      consider q,r be bag of SetPrimes such that

       A12: ( support q) = (( support p) \ {x}) and

       A13: ( support r) = {x} and

       A14: ( support q) misses ( support r) and

       A15: (q | ( support q)) = (p | ( support q)) and

       A16: (r | ( support r)) = (p | ( support r)) and

       A17: (q + r) = p by Lm3;

      

       A18: x in ( support r) by A13, TARSKI:def 1;

      

      then

       A19: (r . x) = ((r | ( support r)) . x) by FUNCT_1: 49

      .= (p . x) by A16, A18, FUNCT_1: 49;

      

      then

       A20: ((r . x) / x) = (((x |^ mx) * x) / x) by A5, A6, NEWTON: 6

      .= (x |^ mx) by XCMPLX_1: 89;

      then

      reconsider rxx = ((r . x) / x) as Element of NAT by ORDINAL1:def 12;

      set r20 = (( SetPrimes --> 0 ) +* (x,rxx));

      rxx <> 0

      proof

        assume

         A21: rxx = 0 ;

        (r . x) = (rxx * x) by XCMPLX_1: 87

        .= 0 by A21;

        hence contradiction by A5, A19;

      end;

      then

      consider r2 be bag of SetPrimes such that

       A22: r2 = r20 and

       A23: ( support r2) = {x} and

       A24: ( Product r2) = rxx by Lm8;

      set p1 = (q + r2);

      

       A25: r = (( SetPrimes --> 0 ) +* (x,(r . x))) by A13, Th1;

       A26:

      now

        let z be set;

        

         A27: (p1 . z) = ((q . z) + (r2 . z)) by PRE_POLY:def 5;

        assume

         A28: z in (( support p1) \ {x});

        then not z in {x} by XBOOLE_0:def 5;

        then

         A29: (r2 . z) = 0 by A23, PRE_POLY:def 7;

        z in ( support p1) by A28, XBOOLE_0:def 5;

        then z in (( support q) \/ ( support r2)) by PRE_POLY: 38;

        then

         A30: z in ( support q) or z in ( support r2) by XBOOLE_0:def 3;

        

        then (q . z) = ((q | ( support q)) . z) by A23, A28, FUNCT_1: 49, XBOOLE_0:def 5

        .= (p . z) by A15, A23, A28, A30, FUNCT_1: 49, XBOOLE_0:def 5;

        hence (p1 . z) = (p . z) by A27, A29;

      end;

      ( dom p1) = SetPrimes by PARTFUN1:def 2

      .= ( dom p) by PARTFUN1:def 2;

      then

       A31: (p1 | (( support p1) \ {x})) = (p | (( support p1) \ {x})) by A26, FUNCT_1: 96;

      

       A32: (( support q) /\ ( support r)) = {} by A14, XBOOLE_0:def 7;

      now

        let z be Prime;

        

         A33: (p1 . z) = ((q . z) + (r2 . z)) by PRE_POLY:def 5;

        assume z in ( support p1);

        then

         A34: z in (( support q) \/ ( support r2)) by PRE_POLY: 38;

        per cases by A34, XBOOLE_0:def 3;

          suppose

           A35: z in ( support q);

          then not z in {x} by A12, XBOOLE_0:def 5;

          then

           A36: (r2 . z) = 0 by A23, PRE_POLY:def 7;

          

           A37: ( support q) c= ( support p) by A12, XBOOLE_1: 36;

          (q . z) = ((q | ( support q)) . z) by A35, FUNCT_1: 49

          .= (p . z) by A15, A35, FUNCT_1: 49;

          hence ex n be Nat st 0 < n & (p1 . z) = (z |^ n) by A1, A33, A35, A37, A36;

        end;

          suppose

           A38: z in ( support r2);

          take mx;

          thus 0 < mx by A7;

          

           A39: z = x by A23, A38, TARSKI:def 1;

          

           A40: not z in ( support q) by A13, A32, A23, A38, XBOOLE_0:def 4;

          (p1 . z) = ((q . z) + (r2 . z)) by PRE_POLY:def 5

          .= ( 0 + (r2 . z)) by A40, PRE_POLY:def 7

          .= (z |^ mx) by A20, A22, A8, A38, A39, FUNCT_7: 31;

          hence (p1 . z) = (z |^ mx);

        end;

      end;

      then

       A41: p1 is prime-factorization-like;

      x in {x} by TARSKI:def 1;

      then

       A42: not x in ( support q) by A12, XBOOLE_0:def 5;

      (p1 . x) = ((q . x) + (r2 . x)) by PRE_POLY:def 5

      .= ( 0 + (r2 . x)) by A42, PRE_POLY:def 7

      .= rxx by A22, A9, FUNCT_7: 31;

      then

       A43: (p . x) = ((p1 . x) * x) by A19, XCMPLX_1: 87;

      (r . x) = (rxx * x) by XCMPLX_1: 87;

      then ex rr1 be bag of SetPrimes st rr1 = r & ( support rr1) = {x} & ( Product rr1) = (rxx * x) by A5, A19, A25, Lm8;

      

      then

       A44: ( Product p) = (( Product q) * (( Product r2) * x)) by A14, A17, A24, NAT_3: 19

      .= ((( Product q) * ( Product r2)) * x)

      .= (( Product p1) * x) by A13, A14, A23, NAT_3: 19;

      ( support p1) = ((( support p) \ {x}) \/ {x}) by A12, A23, PRE_POLY: 38

      .= (( support p) \/ {x}) by XBOOLE_1: 39

      .= ( support p) by A11, XBOOLE_1: 12;

      hence thesis by A10, A43, A44, A41, A31;

    end;

    theorem :: INT_7:13

    

     Th13: for p be bag of SetPrimes st p is prime-factorization-like holds ( Product p) <> 0

    proof

      let p be bag of SetPrimes ;

      assume

       A1: p is prime-factorization-like;

      

       A2: ( rng ( canFS ( support p))) = ( support p) by FUNCT_2:def 3;

      consider f be FinSequence of COMPLEX such that

       A3: ( Product p) = ( Product f) and

       A4: f = (p * ( canFS ( support p))) by NAT_3:def 5;

      reconsider f as complex-valued FinSequence;

      assume ( Product p) = 0 ;

      then

      consider k be Nat such that

       A5: k in ( dom f) and

       A6: (f . k) = 0 by A3, RVSUM_1: 103;

      k in ( dom ( canFS ( support p))) by A4, A5, FUNCT_1: 11;

      then

       A7: (( canFS ( support p)) . k) in ( support p) by A2, FUNCT_1: 3;

      then

      reconsider q = (( canFS ( support p)) . k) as Prime by NEWTON:def 6;

      ex n be Nat st 0 < n & (p . q) = (q |^ n) by A1, A7;

      hence contradiction by A4, A5, A6, FUNCT_1: 12;

    end;

    theorem :: INT_7:14

    

     Th14: for p be bag of SetPrimes st p is prime-factorization-like holds ( Product p) = 1 iff ( support p) = {}

    proof

      let p be bag of SetPrimes ;

      assume

       A1: p is prime-factorization-like;

       A2:

      now

        assume

         A3: ( Product p) = 1;

        thus ( support p) = {}

        proof

          assume ( support p) <> {} ;

          then

          consider q be object such that

           A4: q in ( support p) by XBOOLE_0:def 1;

          q in SetPrimes by A4;

          then

          reconsider q as Element of NAT ;

          reconsider q as Prime by A4, NEWTON:def 6;

          q = 1 by A1, A3, A4, Lm4, WSIERP_1: 15;

          hence contradiction by INT_2:def 4;

        end;

      end;

      now

        consider f be FinSequence of COMPLEX such that

         A5: ( Product p) = ( Product f) and

         A6: f = (p * ( canFS ( support p))) by NAT_3:def 5;

        assume ( support p) = {} ;

        hence ( Product p) = 1 by A5, A6, RVSUM_1: 94;

      end;

      hence thesis by A2;

    end;

    

     Lm11: for n be Element of NAT , p,q be bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & ( Product p) <= (2 |^ n) & ( Product p) = ( Product q) holds p = q

    proof

      defpred P[ Nat] means for p,q be bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & ( Product p) <= (2 |^ $1) & ( Product p) = ( Product q) holds p = q;

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        now

          let p,q be bag of SetPrimes ;

          assume that

           A3: p is prime-factorization-like and

           A4: q is prime-factorization-like and

           A5: ( Product p) <= (2 |^ (k + 1)) and

           A6: ( Product p) = ( Product q);

          now

            per cases ;

              suppose

               A7: ( support p) = {} ;

              then ( Product p) = 1 by A3, Th14;

              then ( support q) = {} by A4, A6, Th14;

              hence p = q by A7, Th4;

            end;

              suppose ( support p) <> {} ;

              then

              consider x be object such that

               A8: x in ( support p) by XBOOLE_0:def 1;

              reconsider x as Prime by A8, NEWTON:def 6;

              

               A9: x divides ( Product p) by A3, A8, Lm4;

              then

               A10: x in ( support q) by A4, A6, Lm7;

              per cases ;

                suppose (p . x) <> x;

                then

                consider p1,r1 be bag of SetPrimes such that

                 A11: p1 is prime-factorization-like and ( support r1) = {x} and ( Product r1) = x and

                 A12: ( support p1) = ( support p) and

                 A13: (p1 | (( support p1) \ {x})) = (p | (( support p1) \ {x})) and

                 A14: (p . x) = ((p1 . x) * x) and

                 A15: ( Product p) = (( Product p1) * x) by A3, A8, Lm10;

                per cases ;

                  suppose

                   A16: (q . x) <> x;

                  1 < x by INT_2:def 4;

                  then (1 + 1) <= x by NAT_1: 13;

                  then

                   A17: ((2 |^ (k + 1)) / x) <= ((2 |^ (k + 1)) / 2) by XREAL_1: 118;

                  consider q1,r2 be bag of SetPrimes such that

                   A18: q1 is prime-factorization-like and ( support r2) = {x} and ( Product r2) = x and

                   A19: ( support q1) = ( support q) and

                   A20: (q1 | (( support q1) \ {x})) = (q | (( support q1) \ {x})) and

                   A21: (q . x) = ((q1 . x) * x) and

                   A22: ( Product q) = (( Product q1) * x) by A4, A6, A9, A16, Lm7, Lm10;

                  ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / x) by A5, A15, XREAL_1: 72;

                  then ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / 2) by A17, XXREAL_0: 2;

                  then ( Product p1) <= ((2 |^ (k + 1)) / 2) by XCMPLX_1: 89;

                  then ( Product p1) <= (((2 |^ k) * (2 |^ 1)) / 2) by NEWTON: 8;

                  then

                   A23: ( Product p1) <= (((2 |^ k) * 2) / 2);

                  then

                   A24: p1 = q1 by A2, A6, A11, A15, A18, A22, XCMPLX_1: 5;

                   A25:

                  now

                    let z be set;

                    assume

                     A26: z in ( support p);

                    per cases ;

                      suppose not z in {x};

                      then

                       A27: z in (( support p1) \ {x}) by A12, A26, XBOOLE_0:def 5;

                      

                      hence (p . z) = ((p | (( support p1) \ {x})) . z) by FUNCT_1: 49

                      .= (q . z) by A13, A20, A24, A27, FUNCT_1: 49;

                    end;

                      suppose

                       A28: z in {x};

                      

                      hence (p . z) = ((p1 . x) * x) by A14, TARSKI:def 1

                      .= ((q1 . x) * x) by A2, A6, A11, A15, A18, A22, A23, XCMPLX_1: 5

                      .= (q . z) by A21, A28, TARSKI:def 1;

                    end;

                  end;

                  

                   A29: ( dom p) = SetPrimes by PARTFUN1:def 2

                  .= ( dom q) by PARTFUN1:def 2;

                  ( support p) = ( support q) by A2, A6, A11, A12, A15, A18, A19, A22, A23, XCMPLX_1: 5;

                  then (p | ( support p)) = (q | ( support q)) by A29, A25, FUNCT_1: 96;

                  hence p = q by Th3;

                end;

                  suppose

                   A30: (q . x) = x;

                  1 < x by INT_2:def 4;

                  then (1 + 1) <= x by NAT_1: 13;

                  then

                   A31: ((2 |^ (k + 1)) / x) <= ((2 |^ (k + 1)) / 2) by XREAL_1: 118;

                  ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / x) by A5, A15, XREAL_1: 72;

                  then ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / 2) by A31, XXREAL_0: 2;

                  then ( Product p1) <= ((2 |^ (k + 1)) / 2) by XCMPLX_1: 89;

                  then ( Product p1) <= (((2 |^ k) * (2 |^ 1)) / 2) by NEWTON: 8;

                  then

                   A32: ( Product p1) <= (((2 |^ k) * 2) / 2);

                  ex q1,r2 be bag of SetPrimes st q1 is prime-factorization-like & ( support r2) = {x} & ( Product r2) = x & ( support q1) = (( support q) \ {x}) & (q1 | ( support q1)) = (q | ( support q1)) & ( Product q) = (( Product q1) * x) by A4, A6, A9, A30, Lm7, Lm9;

                  then ( support p) = (( support q) \ {x}) by A2, A6, A11, A12, A15, A32, XCMPLX_1: 5;

                  then not x in {x} by A8, XBOOLE_0:def 5;

                  hence p = q by TARSKI:def 1;

                end;

              end;

                suppose

                 A33: (p . x) = x;

                then

                consider p1,r1 be bag of SetPrimes such that

                 A34: p1 is prime-factorization-like and ( support r1) = {x} and ( Product r1) = x and

                 A35: ( support p1) = (( support p) \ {x}) and

                 A36: (p1 | ( support p1)) = (p | ( support p1)) and

                 A37: ( Product p) = (( Product p1) * x) by A3, A8, Lm9;

                per cases ;

                  suppose

                   A38: (q . x) <> x;

                  1 < x by INT_2:def 4;

                  then (1 + 1) <= x by NAT_1: 13;

                  then

                   A39: ((2 |^ (k + 1)) / x) <= ((2 |^ (k + 1)) / 2) by XREAL_1: 118;

                  ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / x) by A5, A37, XREAL_1: 72;

                  then ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / 2) by A39, XXREAL_0: 2;

                  then ( Product p1) <= ((2 |^ (k + 1)) / 2) by XCMPLX_1: 89;

                  then ( Product p1) <= (((2 |^ k) * (2 |^ 1)) / 2) by NEWTON: 8;

                  then

                   A40: ( Product p1) <= (((2 |^ k) * 2) / 2);

                  ex q1,r2 be bag of SetPrimes st q1 is prime-factorization-like & ( support r2) = {x} & ( Product r2) = x & ( support q1) = ( support q) & (q1 | (( support q1) \ {x})) = (q | (( support q1) \ {x})) & (q . x) = ((q1 . x) * x) & ( Product q) = (( Product q1) * x) by A4, A6, A9, A38, Lm7, Lm10;

                  then (( support p) \ {x}) = ( support q) by A2, A6, A34, A35, A37, A40, XCMPLX_1: 5;

                  then not x in {x} by A10, XBOOLE_0:def 5;

                  hence p = q by TARSKI:def 1;

                end;

                  suppose

                   A41: (q . x) = x;

                  1 < x by INT_2:def 4;

                  then (1 + 1) <= x by NAT_1: 13;

                  then

                   A42: ((2 |^ (k + 1)) / x) <= ((2 |^ (k + 1)) / 2) by XREAL_1: 118;

                  consider q1,r2 be bag of SetPrimes such that

                   A43: q1 is prime-factorization-like and ( support r2) = {x} and ( Product r2) = x and

                   A44: ( support q1) = (( support q) \ {x}) and

                   A45: (q1 | ( support q1)) = (q | ( support q1)) and

                   A46: ( Product q) = (( Product q1) * x) by A4, A6, A9, A41, Lm7, Lm9;

                  ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / x) by A5, A37, XREAL_1: 72;

                  then ((( Product p1) * x) / x) <= ((2 |^ (k + 1)) / 2) by A42, XXREAL_0: 2;

                  then ( Product p1) <= ((2 |^ (k + 1)) / 2) by XCMPLX_1: 89;

                  then ( Product p1) <= (((2 |^ k) * (2 |^ 1)) / 2) by NEWTON: 8;

                  then

                   A47: ( Product p1) <= (((2 |^ k) * 2) / 2);

                  then (( support p) \ {x}) = (( support q) \ {x}) by A2, A6, A34, A35, A37, A43, A44, A46, XCMPLX_1: 5;

                  then (( support p) \/ {x}) = ((( support q) \ {x}) \/ {x}) by XBOOLE_1: 39;

                  then

                   A48: (( support p) \/ {x}) = (( support q) \/ {x}) by XBOOLE_1: 39;

                  

                   A49: p1 = q1 by A2, A6, A34, A37, A43, A46, A47, XCMPLX_1: 5;

                   A50:

                  now

                    let z be set;

                    assume

                     A51: z in ( support p);

                    per cases ;

                      suppose not z in {x};

                      then

                       A52: z in ( support p1) by A35, A51, XBOOLE_0:def 5;

                      

                      hence (p . z) = ((p1 | ( support p1)) . z) by A36, FUNCT_1: 49

                      .= (q . z) by A45, A49, A52, FUNCT_1: 49;

                    end;

                      suppose

                       A53: z in {x};

                      

                      hence (p . z) = x by A33, TARSKI:def 1

                      .= (q . z) by A41, A53, TARSKI:def 1;

                    end;

                  end;

                  

                   A54: {x} c= ( support q) by A10, ZFMISC_1: 31;

                   {x} c= ( support p) by A8, ZFMISC_1: 31;

                  then

                   A55: ( support p) = (( support q) \/ {x}) by A48, XBOOLE_1: 12;

                  ( dom p) = SetPrimes by PARTFUN1:def 2

                  .= ( dom q) by PARTFUN1:def 2;

                  

                  then (p | ( support p)) = (q | ( support p)) by A50, FUNCT_1: 96

                  .= (q | ( support q)) by A54, A55, XBOOLE_1: 12;

                  hence p = q by Th3;

                end;

              end;

            end;

          end;

          hence p = q;

        end;

        hence P[(k + 1)];

      end;

      

       A56: P[ 0 ]

      proof

        let p,q be bag of SetPrimes ;

        assume that

         A57: p is prime-factorization-like and

         A58: q is prime-factorization-like and

         A59: ( Product p) <= (2 |^ 0 ) and

         A60: ( Product p) = ( Product q);

        ( Product p) <> 0 by A57, Th13;

        then

         A61: ( 0 + 1) <= ( Product p) by NAT_1: 13;

        ( Product p) <= 1 by A59, NEWTON: 4;

        then

         A62: ( Product p) = 1 by A61, XXREAL_0: 1;

        then

         A63: ( support p) = {} by A57, Th14;

        ( support q) = {} by A58, A60, A62, Th14;

        hence thesis by A63, Th4;

      end;

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

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: INT_7:15

    

     Th15: for p,q be bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & ( Product p) = ( Product q) holds p = q

    proof

      let p,q be bag of SetPrimes ;

      assume that

       A1: p is prime-factorization-like and

       A2: q is prime-factorization-like and

       A3: ( Product p) = ( Product q);

      reconsider n = ( Product p) as Element of NAT ;

      n <= (2 |^ n) by NEWTON: 86;

      hence thesis by A1, A2, A3, Lm11;

    end;

    theorem :: INT_7:16

    for p be bag of SetPrimes , n be non zero Nat st p is prime-factorization-like & n = ( Product p) holds ( ppf n) = p

    proof

      let p be bag of SetPrimes , n be non zero Nat;

      assume that

       A1: p is prime-factorization-like and

       A2: n = ( Product p);

      ( Product ( ppf n)) = ( Product p) by A2, NAT_3: 61;

      hence thesis by A1, Th15;

    end;

    theorem :: INT_7:17

    

     Th17: for n,m be Element of NAT st 1 <= n & 1 <= m holds ex m0,n0 be Element of NAT st (n lcm m) = (n0 * m0) & (n0 gcd m0) = 1 & n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0

    proof

      let n1,m1 be Element of NAT ;

      assume that

       A1: 1 <= n1 and

       A2: 1 <= m1;

      reconsider n = n1, m = m1 as non zero Nat by A1, A2;

      set nm1 = (n1 lcm m1);

      reconsider nm = nm1 as non zero Nat by A1, A2, INT_2: 4;

      set N1 = { p where p be Element of NAT : p in ( support ( ppf n)) & (( pfexp nm) . p) = (( pfexp n) . p) };

      set N2 = (( support ( ppf nm)) \ N1);

      

       A3: N1 c= ( support ( ppf n))

      proof

        let x be object;

        assume x in N1;

        then ex p be Element of NAT st x = p & p in ( support ( ppf n)) & (( pfexp nm) . p) = (( pfexp n) . p);

        hence thesis;

      end;

      

       A4: for x be set st x in N2 holds (( pfexp nm) . x) = (( pfexp m) . x)

      proof

        let x be set;

        

         A5: (( pfexp n) . x) > (( pfexp m) . x) implies (( max (( pfexp n),( pfexp m))) . x) = (( pfexp n) . x) by NAT_3:def 4;

        assume x in N2;

        then

         A6: not x in N1 by XBOOLE_0:def 5;

        

         A7: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9;

        

         A8: not (( pfexp n) . x) > (( pfexp m) . x)

        proof

          assume

           A9: (( pfexp n) . x) > (( pfexp m) . x);

          then

           A10: (( pfexp nm) . x) = (( pfexp n) . x) by A5, NAT_3: 54;

          

           A11: x in ( support ( pfexp n)) by A9, PRE_POLY:def 7;

          then x in SetPrimes ;

          hence contradiction by A6, A7, A10, A11;

        end;

        (( pfexp n) . x) <= (( pfexp m) . x) implies (( max (( pfexp n),( pfexp m))) . x) = (( pfexp m) . x) by NAT_3:def 4;

        hence thesis by A8, NAT_3: 54;

      end;

      

       A12: ( Product ( ppf m)) = m by NAT_3: 61;

      

       A13: ( support ( ppf nm)) = (( support ( ppf n)) \/ ( support ( ppf m))) by Th9;

      then

       A14: ( support ( ppf n)) c= ( support ( ppf nm)) by XBOOLE_1: 7;

      then

      consider ppm,ppn be bag of SetPrimes such that

       A15: ( support ppm) = (( support ( ppf nm)) \ N1) and

       A16: ( support ppn) = N1 and

       A17: ( support ppm) misses ( support ppn) and

       A18: (ppm | ( support ppm)) = (( ppf nm) | ( support ppm)) and

       A19: (ppn | ( support ppn)) = (( ppf nm) | ( support ppn)) and

       A20: (ppm + ppn) = ( ppf nm) by A3, Lm3, XBOOLE_1: 1;

      reconsider n0 = ( Product ppn), m0 = ( Product ppm) as Element of NAT ;

      

       A21: ( Product ( ppf n)) = n by NAT_3: 61;

      

       A22: N2 c= ( support ( ppf m))

      proof

        let x be object;

        

         A23: (( pfexp n) . x) <= (( pfexp m) . x) implies (( max (( pfexp n),( pfexp m))) . x) = (( pfexp m) . x) by NAT_3:def 4;

        

         A24: (( pfexp n) . x) > (( pfexp m) . x) implies (( max (( pfexp n),( pfexp m))) . x) = (( pfexp n) . x) by NAT_3:def 4;

        assume

         A25: x in N2;

        then

         A26: x in SetPrimes ;

        

         A27: x in ( support ( ppf nm)) by A25, XBOOLE_0:def 5;

        then x in ( support ( pfexp nm)) by NAT_3:def 9;

        then

         A28: (( pfexp nm) . x) = (( pfexp m) . x) implies (( pfexp m) . x) <> 0 by PRE_POLY:def 7;

         not x in N1 by A25, XBOOLE_0:def 5;

        then

         A29: not x in ( support ( ppf n)) or (( pfexp nm) . x) <> (( pfexp n) . x) by A26;

        ( support ( ppf m)) = ( support ( pfexp m)) by NAT_3:def 9;

        hence thesis by A13, A27, A29, A23, A24, A28, NAT_3: 54, PRE_POLY:def 7, XBOOLE_0:def 3;

      end;

      (N1 \/ N2) = ( support ( ppf nm)) by A14, A3, XBOOLE_1: 1, XBOOLE_1: 45;

      then

       A30: N2 c= ( support ( ppf nm)) by XBOOLE_1: 7;

       A31:

      now

        let x2 be set;

        assume

         A32: x2 in N2;

        then

        reconsider x = x2 as Prime by NEWTON:def 6;

        x2 in ( support ( ppf m)) by A22, A32;

        then

         A33: x2 in ( support ( pfexp m)) by NAT_3:def 9;

        x2 in ( support ( ppf nm)) by A30, A32;

        then x2 in ( support ( pfexp nm)) by NAT_3:def 9;

        

        hence (( ppf nm) . x2) = (x |^ (x |-count nm)) by NAT_3:def 9

        .= (x |^ (( pfexp nm) . x)) by NAT_3:def 8

        .= (x |^ (( pfexp m) . x)) by A4, A32

        .= (x |^ (x |-count m)) by NAT_3:def 8

        .= (( ppf m) . x2) by A33, NAT_3:def 9;

      end;

      ( dom ( ppf nm)) = SetPrimes by PARTFUN1:def 2

      .= ( dom ( ppf m)) by PARTFUN1:def 2;

      then (ppm | N2) = (( ppf m) | N2) by A15, A18, A31, FUNCT_1: 96;

      then

       A34: m0 divides m by A22, A12, A15, Th7;

      

       A35: (n0 * m0) = ( Product ( ppf nm)) by A17, A20, NAT_3: 19

      .= nm by NAT_3: 61;

      then

       A36: m0 <> 0 ;

      now

        let x be Prime;

        assume

         A37: x in ( support ppm);

        then x in ( support ( ppf nm)) by A15, XBOOLE_0:def 5;

        then

         A38: x in ( support ( pfexp nm)) by NAT_3:def 9;

        then

         A39: (( ppf nm) . x) = (x |^ (x |-count nm)) by NAT_3:def 9;

        (( pfexp nm) . x) <> 0 by A38, NAT_3: 36, NAT_3: 38;

        then

         A40: 0 < (x |-count nm) by NAT_3:def 8;

        (ppm . x) = ((ppm | ( support ppm)) . x) by A37, FUNCT_1: 49

        .= (( ppf nm) . x) by A18, A37, FUNCT_1: 49;

        hence ex m be Nat st 0 < m & (ppm . x) = (x |^ m) by A39, A40;

      end;

      then

       A41: ppm is prime-factorization-like;

      

       A42: N1 c= ( support ( ppf nm)) by A14, A3;

      now

        let x be Prime;

        assume

         A43: x in ( support ppn);

        then x in ( support ( ppf nm)) by A42, A16;

        then

         A44: x in ( support ( pfexp nm)) by NAT_3:def 9;

        then

         A45: (( ppf nm) . x) = (x |^ (x |-count nm)) by NAT_3:def 9;

        (( pfexp nm) . x) <> 0 by A44, NAT_3: 36, NAT_3: 38;

        then

         A46: 0 < (x |-count nm) by NAT_3:def 8;

        (ppn . x) = ((ppn | ( support ppn)) . x) by A43, FUNCT_1: 49

        .= (( ppf nm) . x) by A19, A43, FUNCT_1: 49;

        hence ex n be Nat st 0 < n & (ppn . x) = (x |^ n) by A45, A46;

      end;

      then ppn is prime-factorization-like;

      then (n0,m0) are_coprime by A17, A41, Th12;

      then

       A47: (n0 gcd m0) = 1 by INT_2:def 3;

      

       A48: for x be set st x in N1 holds (( pfexp nm) . x) = (( pfexp n) . x)

      proof

        let x be set;

        assume x in N1;

        then ex p be Element of NAT st x = p & p in ( support ( ppf n)) & (( pfexp nm) . p) = (( pfexp n) . p);

        hence thesis;

      end;

       A49:

      now

        let x1 be set;

        assume

         A50: x1 in N1;

        then

         A51: x1 in ( support ( ppf nm)) by A42;

        then

        reconsider x = x1 as Prime by NEWTON:def 6;

        x1 in ( support ( ppf n)) by A3, A50;

        then

         A52: x1 in ( support ( pfexp n)) by NAT_3:def 9;

        x1 in ( support ( pfexp nm)) by A51, NAT_3:def 9;

        

        hence (( ppf nm) . x1) = (x |^ (x |-count nm)) by NAT_3:def 9

        .= (x |^ (( pfexp nm) . x)) by NAT_3:def 8

        .= (x |^ (( pfexp n) . x)) by A48, A50

        .= (x |^ (x |-count n)) by NAT_3:def 8

        .= (( ppf n) . x1) by A52, NAT_3:def 9;

      end;

      ( dom ( ppf nm)) = SetPrimes by PARTFUN1:def 2

      .= ( dom ( ppf n)) by PARTFUN1:def 2;

      then

       A53: (ppn | N1) = (( ppf n) | N1) by A16, A19, A49, FUNCT_1: 96;

      n0 <> 0 by A35;

      hence thesis by A3, A21, A16, A53, A35, A34, A36, A47, Th7;

    end;

    begin

    definition

      let n be Nat;

      assume

       A1: 1 < n;

      :: INT_7:def2

      func Segm0 (n) -> non empty finite Subset of NAT equals

      : Def2: (( Segm n) \ { 0 });

      correctness

      proof

        

         A2: not 1 in { 0 } by TARSKI:def 1;

        1 in ( Segm n) by A1, NAT_1: 44;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

    end

    theorem :: INT_7:18

    

     Th18: for n be Nat st 1 < n holds ( card ( Segm0 n)) = (n - 1)

    proof

      let n be Nat;

      

       A1: ( card ( Segm n)) = n;

      assume

       A2: 1 < n;

      then

       A3: 0 in ( Segm n) by NAT_1: 44;

      

       A4: ( card { 0 }) = 1 by CARD_1: 30;

      ( Segm0 n) = (( Segm n) \ { 0 }) by A2, Def2;

      hence thesis by A1, A3, A4, EULER_1: 4;

    end;

    definition

      let n be Prime;

      :: INT_7:def3

      func multint0 (n) -> BinOp of ( Segm0 n) equals (( multint n) || ( Segm0 n));

      coherence

      proof

        

         A1: 1 < n by INT_2:def 4;

        then ( Segm0 n) = (( Segm n) \ { 0 }) by Def2;

        then

        reconsider S = ( Segm0 n) as Subset of ( Segm n) by XBOOLE_1: 36;

        ( multint n) is S -subsetpreserving

        proof

          let x be set;

          

           A2: 0 in ( Segm n) by NAT_1: 44;

          assume x in [:S, S:];

          then

          consider a,b be object such that

           A3: a in ( Segm0 n) and

           A4: b in ( Segm0 n) and

           A5: x = [a, b] by ZFMISC_1:def 2;

          

           A6: b in (( Segm n) \ { 0 }) by A1, A4, Def2;

          then

          reconsider b1 = b as Element of ( INT.Ring n) by XBOOLE_0:def 5;

           not b in { 0 } by A6, XBOOLE_0:def 5;

          then b <> 0 by TARSKI:def 1;

          then

           A7: b <> ( 0. ( INT.Ring n)) by A2, SUBSET_1:def 8;

          

           A8: a in (( Segm n) \ { 0 }) by A1, A3, Def2;

          then

          reconsider a1 = a as Element of ( INT.Ring n) by XBOOLE_0:def 5;

          set y = (( multint n) . (a,b));

          

           A9: y = (a1 * b1);

           not a in { 0 } by A8, XBOOLE_0:def 5;

          then a <> 0 by TARSKI:def 1;

          then a <> ( 0. ( INT.Ring n)) by A2, SUBSET_1:def 8;

          then y <> ( In ( 0 ,( Segm n))) by A9, A7, VECTSP_1: 12;

          then y <> 0 by A9;

          then not y in { 0 } by TARSKI:def 1;

          then y in (( Segm n) \ { 0 }) by A9, XBOOLE_0:def 5;

          hence (( multint n) . x) in S by A1, A5, Def2;

        end;

        hence thesis by REALSET1: 6;

      end;

    end

    

     Lm12: for p be Prime, a,b be Element of multMagma (# ( Segm0 p), ( multint0 p) #), x,y be Element of ( INT.Ring p) st a = x & y = b holds (x * y) = (a * b)

    proof

      let p be Prime, a,b be Element of multMagma (# ( Segm0 p), ( multint0 p) #), x,y be Element of ( INT.Ring p);

      assume that

       A1: a = x and

       A2: y = b;

      

      thus (a * b) = (( multint p) . [a, b]) by FUNCT_1: 49

      .= (x * y) by A1, A2;

    end;

    theorem :: INT_7:19

    

     Th19: for p be Prime holds multMagma (# ( Segm0 p), ( multint0 p) #) is associative commutative Group-like

    proof

      let p be Prime;

      set Zp = multMagma (# ( Segm0 p), ( multint0 p) #);

      

       A1: not 1 in { 0 } by TARSKI:def 1;

      

       A2: 1 < p by INT_2:def 4;

      then 1 in ( Segm p) by NAT_1: 44;

      then 1 in (( Segm p) \ { 0 }) by A1, XBOOLE_0:def 5;

      then 1 in ( Segm0 p) by A2, Def2;

      then

      reconsider e = ( 1. ( INT.Ring p)) as Element of Zp by A2, INT_3: 14;

      

       A3: Zp is associative

      proof

        let x,y,z be Element of Zp;

        x in ( Segm0 p);

        then x in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider x1 = x as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        y in ( Segm0 p);

        then y in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider y1 = y as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        z in ( Segm0 p);

        then z in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider z1 = z as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        

         A4: (y * z) = (y1 * z1) by Lm12;

        (x * y) = (x1 * y1) by Lm12;

        

        then ((x * y) * z) = ((x1 * y1) * z1) by Lm12

        .= (x1 * (y1 * z1)) by GROUP_1:def 3

        .= (x * (y * z)) by A4, Lm12;

        hence thesis;

      end;

       A5:

      now

        let h be Element of Zp;

        h in ( Segm0 p);

        then

         A6: h in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider hp = h as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        

        thus (h * e) = (hp * ( 1_ ( INT.Ring p))) by Lm12

        .= h;

        

        thus (e * h) = (( 1_ ( INT.Ring p)) * hp) by Lm12

        .= h;

         not h in { 0 } by A6, XBOOLE_0:def 5;

        then

         A7: hp <> 0 by TARSKI:def 1;

         0 in ( Segm p) by NAT_1: 44;

        then hp <> ( 0. ( INT.Ring p)) by A7, SUBSET_1:def 8;

        then

        consider hpd be Element of ( INT.Ring p) such that

         A8: (hpd * hp) = ( 1. ( INT.Ring p)) by VECTSP_1:def 9;

        hpd <> ( 0. ( INT.Ring p)) by A8;

        then hpd <> 0 ;

        then not hpd in { 0 } by TARSKI:def 1;

        then hpd in (( Segm p) \ { 0 }) by XBOOLE_0:def 5;

        then

        reconsider g = hpd as Element of Zp by A2, Def2;

        

         A9: (g * h) = e by A8, Lm12;

        (h * g) = e by A8, Lm12;

        hence ex g be Element of Zp st (h * g) = e & (g * h) = e by A9;

      end;

      Zp is commutative

      proof

        let x,y be Element of Zp;

        x in ( Segm0 p);

        then x in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider x1 = x as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        y in ( Segm0 p);

        then y in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider y1 = y as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        (x * y) = (x1 * y1) by Lm12

        .= (y * x) by Lm12;

        hence thesis;

      end;

      hence thesis by A5, A3;

    end;

    definition

      let p be Prime;

      :: INT_7:def4

      func Z/Z* (p) -> commutative Group equals multMagma (# ( Segm0 p), ( multint0 p) #);

      correctness by Th19;

    end

    theorem :: INT_7:20

    for p be Prime, x,y be Element of ( Z/Z* p), x1,y1 be Element of ( INT.Ring p) st x = x1 & y = y1 holds (x * y) = (x1 * y1) by Lm12;

    theorem :: INT_7:21

    

     Th21: for p be Prime holds ( 1_ ( Z/Z* p)) = 1 & ( 1_ ( Z/Z* p)) = ( 1. ( INT.Ring p))

    proof

      let p be Prime;

      

       A1: not 1 in { 0 } by TARSKI:def 1;

      

       A2: 1 < p by INT_2:def 4;

      then 1 in ( Segm p) by NAT_1: 44;

      then 1 in (( Segm p) \ { 0 }) by A1, XBOOLE_0:def 5;

      then 1 in ( Segm0 p) by A2, Def2;

      then

      reconsider e = ( 1. ( INT.Ring p)) as Element of ( Z/Z* p) by A2, INT_3: 14;

      now

        let h be Element of ( Z/Z* p);

        h in ( Segm0 p);

        then h in (( Segm p) \ { 0 }) by A2, Def2;

        then

        reconsider hp = h as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        

        thus (h * e) = (hp * ( 1_ ( INT.Ring p))) by Lm12

        .= h;

        

        thus (e * h) = (( 1_ ( INT.Ring p)) * hp) by Lm12

        .= h;

      end;

      then e = ( 1_ ( Z/Z* p)) by GROUP_1:def 4;

      hence thesis by A2, INT_3: 14;

    end;

    theorem :: INT_7:22

    for p be Prime, x be Element of ( Z/Z* p), x1 be Element of ( INT.Ring p) st x = x1 holds (x " ) = (x1 " )

    proof

      let p be Prime, h be Element of ( Z/Z* p), hp be Element of ( INT.Ring p);

      assume

       A1: h = hp;

      

       A2: 0 in ( Segm p) by NAT_1: 44;

      set hpd = (hp " );

      

       A3: 1 < p by INT_2:def 4;

      h in ( Segm0 p);

      then h in (( Segm p) \ { 0 }) by A3, Def2;

      then not h in { 0 } by XBOOLE_0:def 5;

      then hp <> 0 by A1, TARSKI:def 1;

      then

       A4: hp <> ( 0. ( INT.Ring p)) by A2, SUBSET_1:def 8;

      then (hp * hpd) = ( 1. ( INT.Ring p)) by VECTSP_1:def 10;

      then hpd <> ( 0. ( INT.Ring p));

      then hpd <> 0 ;

      then not hpd in { 0 } by TARSKI:def 1;

      then hpd in (( Segm p) \ { 0 }) by XBOOLE_0:def 5;

      then

      reconsider g = hpd as Element of ( Z/Z* p) by A3, Def2;

      (h * g) = (hp * hpd) by A1, Lm12

      .= ( 1. ( INT.Ring p)) by A4, VECTSP_1:def 10

      .= ( 1_ ( Z/Z* p)) by Th21;

      hence thesis by GROUP_1:def 5;

    end;

    registration

      let p be Prime;

      cluster ( Z/Z* p) -> finite;

      coherence ;

    end

    theorem :: INT_7:23

    for p be Prime holds ( card ( Z/Z* p)) = (p - 1) by INT_2:def 4, Th18;

    theorem :: INT_7:24

    for G be Group, a be Element of G, i be Integer st not a is being_of_order_0 holds ex n,k be Element of NAT st (a |^ i) = (a |^ n) & n = ((k * ( ord a)) + i)

    proof

      let G be Group, a be Element of G, i be Integer;

      assume not a is being_of_order_0;

      then ( ord a) <> 0 by GROUP_1:def 11;

      then

       A1: |.i.| <= ( |.i.| * ( ord a)) by NAT_1: 14, XREAL_1: 151;

       0 <= (( |.i.| * ( ord a)) + i)

      proof

        per cases ;

          suppose

           A2: i < 0 ;

          

           A3: ( |.i.| + i) <= (( |.i.| * ( ord a)) + i) by A1, XREAL_1: 6;

           |.i.| = ( - i) by A2, ABSVALUE:def 1;

          hence thesis by A3;

        end;

          suppose 0 <= i;

          hence thesis;

        end;

      end;

      then

       A4: (( |.i.| * ( ord a)) + i) is Element of NAT by INT_1: 3;

      (a |^ (( |.i.| * ( ord a)) + i)) = ((a |^ ( |.i.| * ( ord a))) * (a |^ i)) by GROUP_1: 33

      .= (((a |^ ( ord a)) |^ |.i.|) * (a |^ i)) by GROUP_1: 35

      .= ((( 1_ G) |^ |.i.|) * (a |^ i)) by GROUP_1: 41

      .= (( 1_ G) * (a |^ i)) by GROUP_1: 31

      .= (a |^ i) by GROUP_1:def 4;

      hence thesis by A4;

    end;

    theorem :: INT_7:25

    

     Th25: for G be commutative Group, a,b be Element of G, n,m be Nat st G is finite & ( ord a) = n & ( ord b) = m & (n gcd m) = 1 holds ( ord (a * b)) = (n * m)

    proof

      let G be commutative Group, a,b be Element of G, n,m be Nat;

      assume that

       A1: G is finite and

       A2: ( ord a) = n and

       A3: ( ord b) = m and

       A4: (n gcd m) = 1;

       not b is being_of_order_0 by A1, GR_CY_1: 6;

      then

       A5: m <> 0 by A3, GROUP_1:def 11;

      

       A6: not (a * b) is being_of_order_0 by A1, GR_CY_1: 6;

      

       A7: ((a * b) |^ (n * m)) = ((a |^ (n * m)) * (b |^ (n * m))) by GROUP_1: 48

      .= (((a |^ n) |^ m) * (b |^ (n * m))) by GROUP_1: 35

      .= (((a |^ n) |^ m) * ((b |^ m) |^ n)) by GROUP_1: 35

      .= ((( 1_ G) |^ m) * ((b |^ m) |^ n)) by A2, GROUP_1: 41

      .= ((( 1_ G) |^ m) * (( 1_ G) |^ n)) by A3, GROUP_1: 41

      .= (( 1_ G) * (( 1_ G) |^ n)) by GROUP_1: 31

      .= (( 1_ G) * ( 1_ G)) by GROUP_1: 31

      .= ( 1_ G) by GROUP_1:def 4;

      

       A8: (m * n) is Element of NAT by ORDINAL1:def 12;

      reconsider n1 = n, m1 = m as Integer;

      

       A9: (n1,m1) are_coprime by A4, INT_2:def 3;

       not a is being_of_order_0 by A1, GR_CY_1: 6;

      then

       A10: n <> 0 by A2, GROUP_1:def 11;

       A11:

      now

        let k be Nat;

        assume that

         A12: ((a * b) |^ k) = ( 1_ G) and

         A13: k <> 0 ;

        reconsider k1 = k as Integer;

        ( 1_ G) = (( 1_ G) |^ n) by GROUP_1: 31

        .= ((a * b) |^ (k * n)) by A12, GROUP_1: 35

        .= ((a |^ (k * n)) * (b |^ (k * n))) by GROUP_1: 48

        .= (((a |^ n) |^ k) * (b |^ (k * n))) by GROUP_1: 35

        .= ((( 1_ G) |^ k) * (b |^ (k * n))) by A2, GROUP_1: 41

        .= (( 1_ G) * (b |^ (k * n))) by GROUP_1: 31

        .= (b |^ (k * n)) by GROUP_1:def 4;

        then m1 divides k1 by A3, A9, GROUP_1: 44, INT_2: 25;

        then

        consider i be Integer such that

         A14: k1 = (m1 * i) by INT_1:def 3;

        ( 1_ G) = (( 1_ G) |^ m) by GROUP_1: 31

        .= ((a * b) |^ (k * m)) by A12, GROUP_1: 35

        .= ((a |^ (k * m)) * (b |^ (k * m))) by GROUP_1: 48

        .= ((a |^ (k * m)) * ((b |^ m) |^ k)) by GROUP_1: 35

        .= ((a |^ (k * m)) * (( 1_ G) |^ k)) by A3, GROUP_1: 41

        .= ((a |^ (k * m)) * ( 1_ G)) by GROUP_1: 31

        .= (a |^ (k * m)) by GROUP_1:def 4;

        then n1 divides k1 by A2, A9, GROUP_1: 44, INT_2: 25;

        then n1 divides i by A9, A14, INT_2: 25;

        then

        consider j be Integer such that

         A15: i = (n1 * j) by INT_1:def 3;

        k1 = ((m1 * n1) * j) by A14, A15;

        then (k / (m * n)) = j by A10, A5, XCMPLX_1: 6, XCMPLX_1: 89;

        then

         A16: j is Element of NAT by INT_1: 3;

        j <> 0 by A13, A14, A15;

        then ((m * n) * 1) <= ((m * n) * j) by A16, NAT_1: 14, XREAL_1: 64;

        hence (m * n) <= k by A14, A15;

      end;

      (n * m) <> 0 by A10, A5, XCMPLX_1: 6;

      hence thesis by A6, A7, A8, A11, GROUP_1:def 11;

    end;

    

     Lm13: for L be Field, n be Element of NAT , f be non-zero Polynomial of L st ( deg f) = n holds ex m be Element of NAT st m = ( card ( Roots f)) & m <= n

    proof

      let L be Field;

      defpred P[ Nat] means for f be non-zero Polynomial of L st ( deg f) = $1 holds ex m be Element of NAT st m = ( card ( Roots f)) & m <= $1;

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        now

          let f be non-zero Polynomial of L;

          

           A3: f <> ( 0_. L) by UPROOTS:def 5;

          assume

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

          thus ex m be Element of NAT st m = ( card ( Roots f)) & m <= (k + 1)

          proof

            per cases ;

              suppose ( Roots f) = {} ;

              hence thesis;

            end;

              suppose

               A5: ( Roots f) <> {} ;

              set RF = ( Roots f);

              consider z be object such that

               A6: z in ( Roots f) by A5, XBOOLE_0:def 1;

              reconsider z as Element of L by A6;

              set g = (f div ( rpoly (1,z)));

              

               A7: z is_a_root_of f by A6, POLYNOM5:def 10;

              then ( rpoly (1,z)) divides f by HURWITZ: 35;

              then ( 0_. L) = (f mod ( rpoly (1,z)));

              then (g *' ( rpoly (1,z))) = ((f - (g *' ( rpoly (1,z)))) + (g *' ( rpoly (1,z)))) by POLYNOM3: 28;

              then (g *' ( rpoly (1,z))) = (f + (( - (g *' ( rpoly (1,z)))) + (g *' ( rpoly (1,z))))) by POLYNOM3: 26;

              then (g *' ( rpoly (1,z))) = (f + ((g *' ( rpoly (1,z))) - (g *' ( rpoly (1,z)))));

              then (g *' ( rpoly (1,z))) = (f + ( 0_. L)) by POLYNOM3: 29;

              then

               A8: f = (g *' ( rpoly (1,z))) by POLYNOM3: 28;

              then g <> ( 0_. L) by A3, POLYNOM3: 34;

              then

              reconsider g as non-zero Polynomial of L by UPROOTS:def 5;

              set RG = ( Roots g);

              ( deg g) = ((k + 1) - 1) by A3, A4, A7, HURWITZ: 36

              .= k;

              then ex m1 be Element of NAT st m1 = ( card ( Roots g)) & m1 <= k by A2;

              then

               A9: (( card RG) + 1) <= (k + 1) by XREAL_1: 6;

              ( Roots f) c= (( Roots g) \/ {z})

              proof

                let y be object;

                assume

                 A10: y in ( Roots f);

                then

                reconsider y1 = y as Element of L;

                y1 is_a_root_of f by A10, POLYNOM5:def 10;

                then ( eval (f,y1)) = ( 0. L) by POLYNOM5:def 7;

                then (( eval (g,y1)) * ( eval (( rpoly (1,z)),y1))) = ( 0. L) by A8, POLYNOM4: 24;

                then

                 A11: (( eval (g,y1)) * (y1 - z)) = ( 0. L) by HURWITZ: 29;

                now

                  per cases ;

                    suppose y1 = z;

                    then y in {z} by TARSKI:def 1;

                    hence thesis by XBOOLE_0:def 3;

                  end;

                    suppose y1 <> z;

                    then (y1 - z) <> ( 0. L) by RLVECT_1: 21;

                    then ( eval (g,y1)) = ( 0. L) by A11, VECTSP_1: 12;

                    then y1 is_a_root_of g by POLYNOM5:def 7;

                    then y1 in ( Roots g) by POLYNOM5:def 10;

                    hence thesis by XBOOLE_0:def 3;

                  end;

                end;

                hence thesis;

              end;

              then

               A12: ( card RF) <= ( card (RG \/ {z})) by NAT_1: 43;

              ( card (RG \/ {z})) <= (( card RG) + ( card {z})) by CARD_2: 43;

              then ( card (RG \/ {z})) <= (( card RG) + 1) by CARD_2: 42;

              then ( card RF) <= (( card RG) + 1) by A12, XXREAL_0: 2;

              hence thesis by A9, XXREAL_0: 2;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A13: P[ 0 ]

      proof

        let f be non-zero Polynomial of L;

        assume

         A14: ( deg f) = 0 ;

        reconsider x = (f . 0 ) as Element of L;

        

         A15: f <> ( 0_. L) by UPROOTS:def 5;

        

         A16: (f . 0 ) <> ( 0. L)

        proof

          assume (f . 0 ) = ( 0. L);

          then f = <%( 0. L)%> by A14, ALGSEQ_1:def 5;

          hence contradiction by A15, POLYNOM5: 34;

        end;

         A17:

        now

          let z be Element of L;

          ( eval ( <%x%>,z)) = ( eval ( <%x, ( 0. L)%>,z)) by POLYNOM5: 43

          .= x by POLYNOM5: 45;

          hence ( eval ( <%x%>,z)) <> ( 0. L) by A16;

        end;

        

         A18: f = <%x%> by A14, ALGSEQ_1:def 5;

        ( Roots f) = {}

        proof

          assume ( Roots f) <> {} ;

          then

          consider z be object such that

           A19: z in ( Roots f) by XBOOLE_0:def 1;

          reconsider z as Element of L by A19;

          z is_a_root_of f by A19, POLYNOM5:def 10;

          then ( eval ( <%x%>,z)) = ( 0. L) by A18, POLYNOM5:def 7;

          hence contradiction by A17;

        end;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: INT_7:26

    

     Th26: for L be non empty ZeroStr, p be Polynomial of L st 0 <= ( deg p) holds p is non-zero

    proof

      let L be non empty ZeroStr, p be Polynomial of L;

      assume 0 <= ( deg p);

      then ( deg p) <> ( - 1);

      then p <> ( 0_. L) by HURWITZ: 20;

      hence thesis by UPROOTS:def 5;

    end;

    theorem :: INT_7:27

    

     Th27: for L be Field, f be Polynomial of L st 0 <= ( deg f) holds ( Roots f) is finite set & ex m,n be Element of NAT st n = ( deg f) & m = ( card ( Roots f)) & m <= n

    proof

      let L be Field, f be Polynomial of L;

      assume

       A1: 0 <= ( deg f);

      then

      reconsider n = ( deg f) as Element of NAT by INT_1: 3;

      reconsider f as non-zero Polynomial of L by A1, Th26;

      ex m be Element of NAT st m = ( card ( Roots f)) & m <= n by Lm13;

      hence thesis;

    end;

    theorem :: INT_7:28

    

     Th28: for p be Prime, z be Element of ( Z/Z* p), y be Element of ( INT.Ring p) st z = y holds for n be Element of NAT holds (( power ( Z/Z* p)) . (z,n)) = (( power ( INT.Ring p)) . (y,n))

    proof

      let p be Prime, z be Element of ( Z/Z* p), y be Element of ( INT.Ring p);

      defpred P[ Nat] means (( power ( Z/Z* p)) . (z,$1)) = (( power ( INT.Ring p)) . (y,$1));

      assume

       A1: z = y;

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        (( power ( Z/Z* p)) . (z,(k + 1))) = ((( power ( Z/Z* p)) . (z,k)) * z) by GROUP_1:def 7

        .= ((( power ( INT.Ring p)) . (y,k)) * y) by A1, A3, Lm12

        .= (( power ( INT.Ring p)) . (y,(k + 1))) by GROUP_1:def 7;

        hence P[(k + 1)];

      end;

      (( power ( Z/Z* p)) . (z, 0 )) = ( 1_ ( Z/Z* p)) by GROUP_1:def 7

      .= ( 1_ ( INT.Ring p)) by Th21

      .= (( power ( INT.Ring p)) . (y, 0 )) by GROUP_1:def 7;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    

     Lm14: for p be Prime, L be Field, n be Nat st 0 < n & L = ( INT.Ring p) holds ex f be Polynomial of L st ( deg f) = n & for x be Element of L, xz be Element of ( Z/Z* p), xn be Element of ( INT.Ring p) st x = xz & xn = (xz |^ n) holds ( eval (f,x)) = (xn - ( 1_ ( INT.Ring p)))

    proof

      let p be Prime, L be Field, n be Nat;

      assume that

       A1: 0 < n and

       A2: L = ( INT.Ring p);

      set qq = ( 1_. L);

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

      set f = (( <%( 0. L), ( 1. L)%> `^ n0) - ( 1_. L));

      set pp = ( <%( 0. L), ( 1. L)%> `^ n0);

       A3:

      now

        let x be Element of L, xz be Element of ( Z/Z* p), xn be Element of ( INT.Ring p);

        assume that

         A4: x = xz and

         A5: xn = (xz |^ n);

        

         A6: xn = (xz |^ n0) by A5

        .= (( power L) . (x,n0)) by A2, A4, Th28;

        

        thus ( eval (f,x)) = (( eval (pp,x)) - ( eval (qq,x))) by POLYNOM4: 21

        .= (( eval (( <%( 0. L), ( 1. L)%> `^ n0),x)) - ( 1. L)) by POLYNOM4: 18

        .= ((( power L) . (( eval ( <%( 0. L), ( 1. L)%>,x)),n0)) - ( 1. L)) by POLYNOM5: 22

        .= (xn - ( 1_ ( INT.Ring p))) by A2, A6, POLYNOM5: 48;

      end;

      

       A7: ( len ( 1_. L)) = 1 by POLYNOM4: 4;

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

      

      then

       A8: ( len ( <%( 0. L), ( 1. L)%> `^ n0)) = (((n * 2) - n) + 1) by POLYNOM5: 23

      .= (n + 1);

      

       A9: ( 0 + 1) < (n + 1) by A1, XREAL_1: 8;

      then ( len ( <%( 0. L), ( 1. L)%> `^ n0)) <> ( len ( - ( 1_. L))) by A8, A7, POLYNOM4: 8;

      

      then ( len f) = ( max (( len ( <%( 0. L), ( 1. L)%> `^ n0)),( len ( - ( 1_. L))))) by POLYNOM4: 7

      .= ( max ((n + 1),1)) by A8, A7, POLYNOM4: 8

      .= (n + 1) by A9, XXREAL_0:def 10;

      then ( deg f) = n;

      hence thesis by A3;

    end;

    theorem :: INT_7:29

    

     Th29: for p be Prime, a,b be Element of ( Z/Z* p), n be Nat st 0 < n & ( ord a) = n & (b |^ n) = 1 holds b is Element of ( gr {a})

    proof

      let p be Prime, a,b be Element of ( Z/Z* p), n be Nat;

      assume that

       A1: 0 < n and

       A2: ( ord a) = n and

       A3: (b |^ n) = 1;

      reconsider XX = the carrier of ( gr {a}) as finite set;

      

       A4: ex D be finite set st D = the carrier of ( gr {a}) & ( card ( gr {a})) = ( card D);

      reconsider L = ( INT.Ring p) as unital non empty doubleLoopStr;

      consider f be Polynomial of L such that

       A5: ( deg f) = n and

       A6: for x be Element of L, xz be Element of ( Z/Z* p), xn be Element of ( INT.Ring p) st x = xz & xn = (xz |^ n) holds ( eval (f,x)) = (xn - ( 1_ ( INT.Ring p))) by A1, Lm14;

      consider m,n0 be Element of NAT such that

       A7: n0 = ( deg f) and

       A8: m = ( card ( Roots f)) and

       A9: m <= n0 by A5, Th27;

      assume not b is Element of ( gr {a});

      

      then ( card (the carrier of ( gr {a}) \/ {b})) = (( card XX) + 1) by CARD_2: 41

      .= (n0 + 1) by A2, A5, A7, A4, GR_CY_1: 7;

      then

       A10: ( card (n0 + 1)) = ( card (the carrier of ( gr {a}) \/ {b}));

      

       A11: 1 < p by INT_2:def 4;

      

       A12: for x be Element of ( Z/Z* p) st (x |^ n) = 1 holds x in ( Roots f)

      proof

        let x1 be Element of ( Z/Z* p);

        assume (x1 |^ n) = 1;

        

        then

         A13: (x1 |^ n) = ( 1_ ( Z/Z* p)) by Th21

        .= ( 1_ ( INT.Ring p)) by Th21;

        (x1 |^ n) in ( Segm0 p);

        then (x1 |^ n) in (( Segm p) \ { 0 }) by A11, Def2;

        then

        reconsider x2 = (x1 |^ n) as Element of ( INT.Ring p) by XBOOLE_0:def 5;

        x1 in ( Segm0 p);

        then x1 in (( Segm p) \ { 0 }) by A11, Def2;

        then

        reconsider x3 = x1 as Element of L by XBOOLE_0:def 5;

        ( eval (f,x3)) = (x2 - ( 1_ ( INT.Ring p))) by A6

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

        then x3 is_a_root_of f by POLYNOM5:def 7;

        hence thesis by POLYNOM5:def 10;

      end;

      

       A14: the carrier of ( gr {a}) c= ( Roots f)

      proof

        let x be object;

        assume

         A15: x in the carrier of ( gr {a});

        then x in ( gr {a});

        then x in ( Z/Z* p) by GROUP_2: 40;

        then

        reconsider x1 = x as Element of ( Z/Z* p);

        x1 in ( gr {a}) by A15;

        then

        consider j be Integer such that

         A16: x1 = (a |^ j) by GR_CY_1: 5;

        (x1 |^ n) = (a |^ (j * n)) by A16, GROUP_1: 35

        .= ((a |^ n) |^ j) by GROUP_1: 35

        .= (( 1_ ( Z/Z* p)) |^ j) by A2, GROUP_1: 41

        .= ( 1_ ( Z/Z* p)) by GROUP_1: 31

        .= 1 by Th21;

        hence thesis by A12;

      end;

      b in ( Roots f) by A3, A12;

      then {b} c= ( Roots f) by ZFMISC_1: 31;

      then (the carrier of ( gr {a}) \/ {b}) c= ( Roots f) by A14, XBOOLE_1: 8;

      then

       A17: ( card (the carrier of ( gr {a}) \/ {b})) c= ( card ( Roots f)) by CARD_1: 11;

      ( card m) = ( card ( Roots f)) by A8;

      then ( Segm (n0 + 1)) c= ( Segm m) by A17, A10;

      then (n0 + 1) <= m by NAT_1: 39;

      hence contradiction by A9, NAT_1: 16, XXREAL_0: 2;

    end;

    theorem :: INT_7:30

    

     Th30: for G be Group, z be Element of G, d,l be Element of NAT st G is finite & ( ord z) = (d * l) holds ( ord (z |^ d)) = l

    proof

      let G be Group, z be Element of G, d,l be Element of NAT ;

      assume that

       A1: G is finite and

       A2: ( ord z) = (d * l);

      set m = (d * l);

      reconsider H = ( gr {z}) as strict Subgroup of G;

      reconsider H as finite strict Subgroup of G by A1;

      z in ( gr {z}) by GR_CY_2: 2;

      then

      reconsider z1 = z as Element of H;

      

       A3: ( gr {z}) = ( gr {z1}) by GR_CY_2: 3;

      ( card H) = m by A1, A2, GR_CY_1: 7;

      then ( ord (z1 |^ d)) = l by A3, GR_CY_2: 8;

      hence thesis by A1, GROUP_8: 3, GROUP_8: 5;

    end;

    theorem :: INT_7:31

    for p be Prime holds ( Z/Z* p) is cyclic Group

    proof

      let p be Prime;

      set a = the Element of ( Z/Z* p);

      set ZP = ( Z/Z* p);

      defpred P[ Nat, Element of ZP, Element of ZP] means ( ord $2) < ( ord $3);

      assume

       A1: not ( Z/Z* p) is cyclic Group;

      

       A2: for x be Element of ( Z/Z* p) holds ( ord x) < ( card ( Z/Z* p))

      proof

        let x be Element of ( Z/Z* p);

        

         A3: ( ord x) <= ( card ( Z/Z* p)) by GR_CY_1: 8, NAT_D: 7;

        ( ord x) <> ( card ( Z/Z* p)) by A1, GR_CY_1: 19;

        hence thesis by A3, XXREAL_0: 1;

      end;

      

       A4: for n be Nat holds for x be Element of ZP holds ex y be Element of ZP st P[n, x, y]

      proof

        let n be Nat, x be Element of ZP;

        set n = ( ord x);

        n < ( card ( Z/Z* p)) by A2;

        then

         A5: ( card ( gr {x})) <> ( card ( Z/Z* p)) by GR_CY_1: 7;

        the carrier of ( gr {x}) c= the carrier of ( Z/Z* p) by GROUP_2:def 5;

        then the carrier of ( gr {x}) c< the carrier of ( Z/Z* p) by A5, XBOOLE_0:def 8;

        then (the carrier of ( Z/Z* p) \ the carrier of ( gr {x})) <> {} by XBOOLE_1: 105;

        then

        consider z be object such that

         A6: z in (the carrier of ( Z/Z* p) \ the carrier of ( gr {x})) by XBOOLE_0:def 1;

        reconsider z as Element of ZP by A6;

        set m = ( ord z);

        now

          set l = (m lcm n);

          1 <= ( card ( gr {x})) by GROUP_1: 45;

          then

           A7: 1 <= n by GR_CY_1: 7;

           not m divides n

          proof

            assume m divides n;

            then

            consider j be Integer such that

             A8: n = (m * j) by INT_1:def 3;

            (z |^ n) = ((z |^ m) |^ j) by A8, GROUP_1: 35

            .= (( 1_ ( Z/Z* p)) |^ j) by GROUP_1: 41

            .= ( 1_ ( Z/Z* p)) by GROUP_1: 31

            .= 1 by Th21;

            then z is Element of ( gr {x}) by A7, Th29;

            hence contradiction by A6, XBOOLE_0:def 5;

          end;

          then

           A9: n <> l by INT_2: 18;

          1 <= ( card ( gr {z})) by GROUP_1: 45;

          then

           A10: 1 <= m by GR_CY_1: 7;

          then

          consider m0,n0 be Element of NAT such that

           A11: l = (n0 * m0) and

           A12: (n0 gcd m0) = 1 and

           A13: n0 divides n and

           A14: m0 divides m and

           A15: n0 <> 0 and

           A16: m0 <> 0 by A7, Th17;

          consider j be Integer such that

           A17: n = (n0 * j) by A13, INT_1:def 3;

          consider u be Integer such that

           A18: m = (m0 * u) by A14, INT_1:def 3;

          (m / m0) = u by A16, A18, XCMPLX_1: 89;

          then

          reconsider d2 = (m / m0) as Element of NAT by INT_1: 3;

          m = ((m / m0) * m0) by A16, XCMPLX_1: 87;

          then

           A19: ( ord (z |^ d2)) = m0 by Th30;

          (n / n0) = j by A15, A17, XCMPLX_1: 89;

          then

          reconsider d1 = (n / n0) as Element of NAT by INT_1: 3;

          n divides (m lcm n) by INT_2: 18;

          then

          consider j be Integer such that

           A20: l = (n * j) by INT_1:def 3;

          take y = ((x |^ d1) * (z |^ d2));

          n = ((n / n0) * n0) by A15, XCMPLX_1: 87;

          then ( ord (x |^ d1)) = n0 by Th30;

          then

           A21: ( ord y) = (m0 * n0) by A12, A19, Th25;

          (l / n) = j by A7, A20, XCMPLX_1: 89;

          then

           A22: j is Element of NAT by INT_1: 3;

          j <> 0 by A7, A10, A20, INT_2: 4;

          then (n * 1) <= (n * j) by A22, NAT_1: 14, XREAL_1: 64;

          hence n < ( ord y) by A11, A21, A9, A20, XXREAL_0: 1;

        end;

        hence thesis;

      end;

      consider f be sequence of the carrier of ZP such that

       A23: (f . 0 ) = a & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A4);

      deffunc F( Nat) = ( ord (f . $1));

      consider g be sequence of NAT such that

       A24: for k be Element of NAT holds (g . k) = F(k) from FUNCT_2:sch 4;

      

       A25: for k be Nat holds (g . k) = F(k)

      proof

        let k be Nat;

        k in NAT by ORDINAL1:def 12;

        hence thesis by A24;

      end;

       A26:

      now

        let k be Nat;

        

         A27: (g . (k + 1)) = ( ord (f . (k + 1))) by A25;

        (g . k) = ( ord (f . k)) by A25;

        hence (g . k) < (g . (k + 1)) by A23, A27;

      end;

      

       A28: for k,m be Element of NAT holds (g . k) < (g . ((k + 1) + m))

      proof

        let k be Element of NAT ;

        defpred P[ Nat] means (g . k) < (g . ((k + 1) + $1));

         A29:

        now

          let m be Nat;

          assume

           A30: P[m];

          (g . ((k + 1) + m)) < (g . (((k + 1) + m) + 1)) by A26;

          hence P[(m + 1)] by A30, XXREAL_0: 2;

        end;

        

         A31: P[ 0 ] by A26;

        for m be Nat holds P[m] from NAT_1:sch 2( A31, A29);

        hence thesis;

      end;

      

       A32: for k,m be Element of NAT st k < m holds (g . k) < (g . m)

      proof

        let k,m be Element of NAT ;

        assume

         A33: k < m;

        then (m - k) is Element of NAT by INT_1: 5;

        then

        reconsider mk = (m - k) as Nat;

        (m - k) <> 0 by A33;

        then

        consider n0 be Nat such that

         A34: mk = (n0 + 1) by NAT_1: 6;

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

        m = ((k + 1) + n) by A34;

        hence thesis by A28;

      end;

      now

        let x1,x2 be object;

        assume that

         A35: x1 in NAT and

         A36: x2 in NAT and

         A37: (g . x1) = (g . x2);

        reconsider xx1 = x1, xx2 = x2 as Element of NAT by A35, A36;

        

         A38: xx2 <= xx1 by A32, A37;

        xx1 <= xx2 by A32, A37;

        hence x2 = x1 by A38, XXREAL_0: 1;

      end;

      then g is one-to-one by FUNCT_2: 19;

      then (( dom g),( rng g)) are_equipotent by WELLORD2:def 4;

      then ( card ( dom g)) = ( card ( rng g)) by CARD_1: 5;

      then

       A39: ( card ( rng g)) = ( card NAT ) by FUNCT_2:def 1;

      ( rng g) c= ( Segm ( card ZP))

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A40: x in NAT and

         A41: y = (g . x) by FUNCT_2: 11;

        reconsider x as Element of NAT by A40;

        reconsider gg = (g . x) as Element of NAT ;

        (g . x) = ( ord (f . x)) by A25;

        then gg < ( card ZP) by A2;

        hence thesis by A41, NAT_1: 44;

      end;

      hence contradiction by A39;

    end;