nat_3.miz



    begin

    reserve a,b,n for Nat,

r for Real,

f for FinSequence of REAL ;

    registration

      cluster natural-valued for FinSequence;

      existence

      proof

        set f = the FinSequence of NAT ;

        take f;

        thus thesis;

      end;

    end

    registration

      let a be non zero Nat;

      let b be Nat;

      cluster (a |^ b) -> non zero;

      coherence by CARD_4: 3;

    end

    registration

      cluster -> non zero for Prime;

      coherence by INT_2:def 4;

    end

    reserve p for Prime;

    theorem :: NAT_3:1

    

     Th1: for a,b,c,d be Nat st a divides c & b divides d holds (a * b) divides (c * d)

    proof

      let a,b,c,d be Nat;

      given x be Nat such that

       A1: c = (a * x);

      given y be Nat such that

       A2: d = (b * y);

      take (x * y);

      thus thesis by A1, A2;

    end;

    theorem :: NAT_3:2

    

     Th2: 1 < a implies b <= (a |^ b)

    proof

      defpred P[ Nat] means $1 <= (a |^ $1);

      assume

       A1: 1 < a;

      then

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

      

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

      proof

        let k be Nat;

        assume P[k];

        then

         A3: (k + 1) <= ((a |^ k) + 1) by XREAL_1: 6;

         A4:

        now

          set x = (a |^ k);

          assume (x + 1) > (x * a);

          then ((x * a) - (x + 1)) < ((x + 1) - (x + 1)) by XREAL_1: 14;

          then (((x * a1) - 1) + 1) < ( 0 + 1) by XREAL_1: 6;

          then x = 0 or a1 = 0 by NAT_1: 13;

          hence contradiction by A1;

        end;

        (a |^ (k + 1)) = ((a |^ k) * a) by NEWTON: 6;

        hence thesis by A3, A4, XXREAL_0: 2;

      end;

      

       A5: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: NAT_3:3

    

     Th3: a <> 0 implies n divides (n |^ a)

    proof

      assume a <> 0 ;

      then

      consider b be Nat such that

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

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

      (n |^ 1) divides (n |^ (b + 1)) by NAT_1: 12, NEWTON: 89;

      hence thesis by A1;

    end;

    theorem :: NAT_3:4

    

     Th4: for i,j,m,n be Nat st i < j & (m |^ j) divides n holds (m |^ (i + 1)) divides n

    proof

      let i,j,m,n be Nat such that

       A1: i < j and

       A2: (m |^ j) divides n;

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

      (i + 1) <= j by A1, NAT_1: 13;

      then (m |^ (i + 1)) divides (m |^ j) by NEWTON: 89;

      hence thesis by A2, NAT_D: 4;

    end;

    theorem :: NAT_3:5

    

     Th5: p divides (a |^ b) implies p divides a

    proof

      assume that

       A1: p divides (a |^ b) and

       A2: not p divides a;

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

      defpred P[ Nat] means p divides (a |^ ($1 + 1));

      

       A3: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n]

      proof

        let k be Nat such that

         A4: k <> 0 and

         A5: P[k];

        

         A6: p divides ((a |^ k) * a) by A5, NEWTON: 6;

        take (k -' 1);

        

         A7: k >= ( 0 + 1) by A4, NAT_1: 13;

        then (k - 1) >= (( 0 + 1) - 1) by XREAL_1: 13;

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

        then (k -' 1) < (k - 0 ) by XREAL_1: 15;

        hence (k -' 1) < k;

        ((k -' 1) + 1) = k by A7, XREAL_1: 235;

        hence thesis by A2, A6, NEWTON: 80;

      end;

      now

        assume ( 0 + 1) > b;

        then b = 0 by NAT_1: 13;

        then p divides 1 by A1, NEWTON: 4;

        then p = 1 by WSIERP_1: 15;

        hence contradiction by INT_2:def 4;

      end;

      then b = ((b -' 1) + 1) by XREAL_1: 235;

      then

       A8: ex k be Nat st P[k] by A1;

       P[ 0 ] from NAT_1:sch 7( A8, A3);

      hence thesis by A2;

    end;

    theorem :: NAT_3:6

    

     Th6: for a be Prime st a divides (p |^ b) holds a = p

    proof

      let a be Prime;

      assume a divides (p |^ b);

      then a <> 1 & a divides p by Th5, INT_2:def 4;

      hence thesis by INT_2:def 4;

    end;

    theorem :: NAT_3:7

    for f be FinSequence of NAT st a in ( rng f) holds a divides ( Product f)

    proof

      defpred P[ FinSequence of NAT ] means for a be Nat st a in ( rng $1) holds a divides ( Product $1);

      

       A1: for p be FinSequence of NAT , n be Element of NAT st P[p] holds P[(p ^ <*n*>)]

      proof

        let p be FinSequence of NAT , n be Element of NAT such that

         A2: P[p];

        set p1 = (p ^ <*n*>);

        

         A3: ( rng p1) = (( rng p) \/ ( rng <*n*>)) by FINSEQ_1: 31;

        

         A4: ( Product p1) = (( Product p) * n) by RVSUM_1: 96;

        let a be Nat such that

         A5: a in ( rng p1);

        per cases by A5, A3, XBOOLE_0:def 3;

          suppose a in ( rng p);

          hence thesis by A2, A4, NAT_D: 9;

        end;

          suppose a in ( rng <*n*>);

          then a in {n} by FINSEQ_1: 39;

          then a = n by TARSKI:def 1;

          hence thesis by A4;

        end;

      end;

      

       A6: P[( <*> NAT ) qua FinSequence of NAT ];

      for p be FinSequence of NAT holds P[p] from FINSEQ_2:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: NAT_3:8

    for f be FinSequence of SetPrimes st p divides ( Product f) holds p in ( rng f)

    proof

      let f be FinSequence of SetPrimes ;

      defpred P[ FinSequence] means ex f be FinSequence of SetPrimes st f = $1 & for p be Prime st p divides ( Product f) holds p in ( rng f);

       A1:

      now

        let f be FinSequence of SetPrimes , n be Element of SetPrimes ;

        set f1 = (f ^ <*n*>);

        assume

         A2: P[f];

        thus P[f1]

        proof

          reconsider nn = n as Nat;

          reconsider ff = f as FinSequence of NAT ;

          reconsider f2 = f1 as FinSequence of SetPrimes ;

          take f2;

          thus f2 = f1;

          let p be Prime;

          assume p divides ( Product f2);

          then

           A3: p divides (( Product ff) * n) by RVSUM_1: 96;

          per cases by A3, NEWTON: 80;

            suppose

             A4: p divides ( Product f);

            

             A5: ( rng f) c= ( rng f1) by FINSEQ_1: 29;

            p in ( rng f) by A2, A4;

            hence thesis by A5;

          end;

            suppose

             A6: p divides nn;

            nn is prime by NEWTON:def 6;

            then p = 1 or p = n by A6;

            then p in {n} by INT_2:def 4, TARSKI:def 1;

            then

             A7: p in ( rng <*n*>) by FINSEQ_1: 38;

            ( rng <*n*>) c= ( rng f1) by FINSEQ_1: 30;

            hence thesis by A7;

          end;

        end;

      end;

      

       A8: P[( <*> SetPrimes )]

      proof

        take ( <*> SetPrimes );

        thus thesis by INT_2:def 4, NAT_D: 7, RVSUM_1: 94;

      end;

      for p be FinSequence of SetPrimes holds P[p] from FINSEQ_2:sch 2( A8, A1);

      then P[f];

      hence thesis;

    end;

    definition

      let f be real-valued FinSequence;

      let a be Nat;

      :: NAT_3:def1

      func f |^ a -> FinSequence means

      : Def1: ( len it ) = ( len f) & for i be set st i in ( dom it ) holds (it . i) = ((f . i) |^ a);

      existence

      proof

        deffunc F( Nat) = ((f . $1) |^ a);

        consider p be FinSequence such that

         A1: ( len p) = ( len f) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        take p;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let g,h be FinSequence such that

         A2: ( len g) = ( len f) and

         A3: for i be set st i in ( dom g) holds (g . i) = ((f . i) |^ a) and

         A4: ( len h) = ( len f) and

         A5: for i be set st i in ( dom h) holds (h . i) = ((f . i) |^ a);

        

         A6: ( dom g) = ( Seg ( len g)) & ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3;

        for k be Nat st k in ( dom g) holds (g . k) = (h . k)

        proof

          let k be Nat such that

           A7: k in ( dom g);

          

          thus (g . k) = ((f . k) |^ a) by A3, A7

          .= (h . k) by A2, A4, A5, A6, A7;

        end;

        hence thesis by A2, A4, A6, FINSEQ_1: 13;

      end;

    end

    registration

      let f be real-valued FinSequence;

      let a be Nat;

      cluster (f |^ a) -> real-valued;

      coherence

      proof

        let x be object;

        set g = (f |^ a);

        assume x in ( dom g);

        then ((f |^ a) . x) = ((f . x) |^ a) by Def1;

        hence thesis;

      end;

    end

    registration

      let f be natural-valued FinSequence;

      let a be Nat;

      cluster (f |^ a) -> natural-valued;

      coherence

      proof

        let x be object;

        set g = (f |^ a);

        assume x in ( dom g);

        then ((f |^ a) . x) = ((f . x) |^ a) by Def1;

        hence thesis;

      end;

    end

    definition

      let f be FinSequence of REAL ;

      let a be Nat;

      :: original: |^

      redefine

      func f |^ a -> FinSequence of REAL ;

      coherence

      proof

        thus ( rng (f |^ a)) c= REAL ;

      end;

    end

    definition

      let f be FinSequence of NAT ;

      let a be Nat;

      :: original: |^

      redefine

      func f |^ a -> FinSequence of NAT ;

      coherence

      proof

        thus ( rng (f |^ a)) c= NAT by VALUED_0:def 6;

      end;

    end

    theorem :: NAT_3:9

    

     Th9: (f |^ 0 ) = (( len f) |-> 1)

    proof

      

       A1: ( len (f |^ 0 )) = ( len f) by Def1;

      

       A2: for k be Nat st 1 <= k & k <= ( len (f |^ 0 )) holds ((f |^ 0 ) . k) = ((( len f) |-> 1) . k)

      proof

        let k be Nat;

        assume

         A3: 1 <= k & k <= ( len (f |^ 0 ));

        then

         A4: k in ( dom (f |^ 0 )) by FINSEQ_3: 25;

        

         A5: k in ( Seg ( len f)) by A1, A3;

        

        thus ((f |^ 0 ) . k) = ((f . k) |^ 0 ) by A4, Def1

        .= 1 by NEWTON: 4

        .= ((( len f) |-> 1) . k) by A5, FUNCOP_1: 7;

      end;

      ( len (( len f) |-> 1)) = ( len f) by CARD_1:def 7;

      hence thesis by A1, A2;

    end;

    theorem :: NAT_3:10

    (f |^ 1) = f

    proof

      

       A1: for k be Nat st 1 <= k & k <= ( len (f |^ 1)) holds ((f |^ 1) . k) = (f . k)

      proof

        let k be Nat;

        assume 1 <= k & k <= ( len (f |^ 1));

        then k in ( dom (f |^ 1)) by FINSEQ_3: 25;

        

        hence ((f |^ 1) . k) = ((f . k) |^ 1) by Def1

        .= (f . k);

      end;

      ( len (f |^ 1)) = ( len f) by Def1;

      hence thesis by A1;

    end;

    theorem :: NAT_3:11

    

     Th11: (( <*> REAL ) |^ a) = ( <*> REAL )

    proof

      ( len (( <*> REAL ) |^ a)) = ( len ( <*> REAL )) by Def1

      .= 0 ;

      hence thesis;

    end;

    theorem :: NAT_3:12

    

     Th12: ( <*r*> |^ a) = <*(r |^ a)*>

    proof

      

       A1: ( len ( <*r*> |^ a)) = ( len <*r*>) by Def1

      .= 1 by FINSEQ_1: 40;

      ( 0 + 1) in ( Seg ( 0 + 1));

      then 1 in ( dom ( <*r*> |^ a)) by A1, FINSEQ_1:def 3;

      

      then (( <*r*> |^ a) . 1) = (( <*r*> . 1) |^ a) by Def1

      .= (r |^ a) by FINSEQ_1: 40;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: NAT_3:13

    

     Th13: ((f ^ <*r*>) |^ a) = ((f |^ a) ^ ( <*r*> |^ a))

    proof

      

       A1: ( len (f |^ a)) = ( len f) by Def1;

      

       A2: ( len ((f ^ <*r*>) |^ a)) = ( len (f ^ <*r*>)) by Def1

      .= (( len f) + ( len <*r*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by FINSEQ_1: 40;

      then

       A3: ( dom ((f ^ <*r*>) |^ a)) = ( Seg (( len f) + 1)) by FINSEQ_1:def 3;

       A4:

      now

        let i be Nat such that

         A5: i in ( dom ((f ^ <*r*>) |^ a));

        

         A6: 1 <= i by A3, A5, FINSEQ_1: 1;

        

         A7: i <= (( len f) + 1) by A3, A5, FINSEQ_1: 1;

        per cases by A7, XXREAL_0: 1;

          suppose i < (( len f) + 1);

          then

           A8: i <= ( len f) by NAT_1: 13;

          then

           A9: i in ( dom f) by A6, FINSEQ_3: 25;

          

           A10: i in ( dom (f |^ a)) by A1, A6, A8, FINSEQ_3: 25;

          

          thus (((f ^ <*r*>) |^ a) . i) = (((f ^ <*r*>) . i) |^ a) by A5, Def1

          .= ((f . i) |^ a) by A9, FINSEQ_1:def 7

          .= ((f |^ a) . i) by A10, Def1

          .= (((f |^ a) ^ ( <*r*> |^ a)) . i) by A10, FINSEQ_1:def 7;

        end;

          suppose

           A11: i = (( len f) + 1);

          

          thus (((f ^ <*r*>) |^ a) . i) = (((f ^ <*r*>) . i) |^ a) by A5, Def1

          .= (r |^ a) by A11, FINSEQ_1: 42

          .= (((f |^ a) ^ <*(r |^ a)*>) . i) by A1, A11, FINSEQ_1: 42

          .= (((f |^ a) ^ ( <*r*> |^ a)) . i) by Th12;

        end;

      end;

      ( len ((f |^ a) ^ ( <*r*> |^ a))) = (( len (f |^ a)) + ( len ( <*r*> |^ a))) by FINSEQ_1: 22

      .= (( len f) + ( len ( <*r*> |^ a))) by Def1

      .= (( len f) + ( len <*(r |^ a)*>)) by Th12

      .= (( len f) + 1) by FINSEQ_1: 40;

      hence thesis by A2, A4, FINSEQ_2: 9;

    end;

    theorem :: NAT_3:14

    

     Th14: ( Product (f |^ (b + 1))) = (( Product (f |^ b)) * ( Product f))

    proof

      defpred P[ FinSequence of REAL ] means for b be Nat holds ( Product ($1 |^ (b + 1))) = (( Product ($1 |^ b)) * ( Product $1));

       A1:

      now

        let p be FinSequence of REAL , x be Element of REAL such that

         A2: P[p];

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

        proof

          set p1 = (p ^ <*x*>);

          let b be Nat;

          reconsider xb1 = (x |^ (b + 1)), xb = (x |^ b) as Real;

          (p1 |^ (b + 1)) = ((p |^ (b + 1)) ^ ( <*x*> |^ (b + 1))) by Th13;

          

          hence ( Product (p1 |^ (b + 1))) = (( Product (p |^ (b + 1))) * ( Product ( <*x*> |^ (b + 1)))) by RVSUM_1: 97

          .= ((( Product (p |^ b)) * ( Product p)) * ( Product ( <*x*> |^ (b + 1)))) by A2

          .= ((( Product (p |^ b)) * ( Product p)) * ( Product <*xb1*>)) by Th12

          .= ((( Product (p |^ b)) * ( Product p)) * (x |^ (b + 1)))

          .= ((( Product (p |^ b)) * ( Product p)) * ((x |^ b) * x)) by NEWTON: 6

          .= (((( Product (p |^ b)) * (x |^ b)) * x) * ( Product p))

          .= ((( Product ((p |^ b) ^ <*xb*>)) * x) * ( Product p)) by RVSUM_1: 96

          .= ((( Product ((p |^ b) ^ ( <*x*> |^ b))) * x) * ( Product p)) by Th12

          .= ((( Product (p1 |^ b)) * x) * ( Product p)) by Th13

          .= (( Product (p1 |^ b)) * (( Product p) * x))

          .= (( Product (p1 |^ b)) * ( Product p1)) by RVSUM_1: 96;

        end;

      end;

      

       A3: P[( <*> REAL )]

      proof

        set f = ( <*> REAL );

        let b be Nat;

        

        thus ( Product (f |^ (b + 1))) = 1 by Th11, RVSUM_1: 94

        .= (( Product (f |^ b)) * ( Product f)) by Th11, RVSUM_1: 94;

      end;

      for p be FinSequence of REAL holds P[p] from FINSEQ_2:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: NAT_3:15

    ( Product (f |^ a)) = (( Product f) |^ a)

    proof

      defpred P[ Nat] means ( Product (f |^ $1)) = (( Product f) |^ $1);

      

       A1: P[b] implies P[(b + 1)]

      proof

        assume

         A2: P[b];

        

        thus ( Product (f |^ (b + 1))) = (( Product (f |^ b)) * ( Product f)) by Th14

        .= (( Product f) |^ (b + 1)) by A2, NEWTON: 6;

      end;

      ( Product (f |^ 0 )) = ( Product (( len f) |-> 1)) by Th9

      .= 1 by RVSUM_1: 102

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

      then

       A3: P[ 0 ];

       P[b] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    begin

    registration

      let X be set;

      cluster natural-valued finite-support for ManySortedSet of X;

      existence

      proof

        set r = the natural-valued finite-support ManySortedSet of X;

        r = r;

        hence thesis;

      end;

    end

    definition

      let X be set, b be real-valued ManySortedSet of X, a be Nat;

      :: NAT_3:def2

      func a * b -> ManySortedSet of X means

      : Def2: for i be object holds (it . i) = (a * (b . i));

      existence

      proof

        deffunc F( object) = (a * (b . $1));

        consider f be ManySortedSet of X such that

         A1: for i be object st i in X holds (f . i) = F(i) from PBOOLE:sch 4;

        take f;

        let i be object;

        per cases ;

          suppose i in X;

          hence thesis by A1;

        end;

          suppose

           A2: not i in X;

          

           A3: ( dom b) = X by PARTFUN1:def 2;

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

          

          hence (f . i) = (a * 0 qua Nat) by A2, FUNCT_1:def 2

          .= (a * (b . i)) by A2, A3, FUNCT_1:def 2;

        end;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of X such that

         A4: for i be object holds (f . i) = (a * (b . i)) and

         A5: for i be object holds (g . i) = (a * (b . i));

        for i be object st i in X holds (f . i) = (g . i)

        proof

          let i be object;

          assume i in X;

          

          thus (f . i) = (a * (b . i)) by A4

          .= (g . i) by A5;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set, b be real-valued ManySortedSet of X, a be Nat;

      cluster (a * b) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (a * b));

        ((a * b) . x) = (a * (b . x)) by Def2;

        then ((a * b) . x) is real;

        hence thesis;

      end;

    end

    registration

      let X be set, b be natural-valued ManySortedSet of X, a be Nat;

      cluster (a * b) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (a * b));

        ((a * b) . x) = (a * (b . x)) by Def2;

        hence thesis;

      end;

    end

    registration

      let X be set, b be real-valued ManySortedSet of X;

      cluster ( support ( 0 * b)) -> empty;

      coherence

      proof

        assume ( support ( 0 * b)) is non empty;

        then

        consider x be object such that

         A1: x in ( support ( 0 * b));

        (( 0 * b) . x) <> 0 by A1, PRE_POLY:def 7;

        then ( 0 * (b . x)) <> 0 by Def2;

        hence thesis;

      end;

    end

    theorem :: NAT_3:16

    

     Th16: for X be set, b be real-valued ManySortedSet of X st a <> 0 holds ( support b) = ( support (a * b))

    proof

      let X be set, b be real-valued ManySortedSet of X such that

       A1: a <> 0 ;

      hereby

        let x be object;

        assume x in ( support b);

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

        then (a * (b . x)) <> 0 by A1;

        then ((a * b) . x) <> 0 by Def2;

        hence x in ( support (a * b)) by PRE_POLY:def 7;

      end;

      let x be object;

      assume x in ( support (a * b));

      then ((a * b) . x) <> 0 by PRE_POLY:def 7;

      then (a * (b . x)) <> 0 by Def2;

      then (b . x) <> 0 ;

      hence thesis by PRE_POLY:def 7;

    end;

    registration

      let X be set, b be real-valued finite-support ManySortedSet of X, a be Nat;

      cluster (a * b) -> finite-support;

      coherence

      proof

        per cases ;

          suppose a = 0 ;

          hence ( support (a * b)) is finite;

        end;

          suppose a <> 0 ;

          then ( support (a * b)) = ( support b) by Th16;

          hence ( support (a * b)) is finite;

        end;

      end;

    end

    definition

      let X be set;

      let b1,b2 be real-valued ManySortedSet of X;

      :: NAT_3:def3

      func min (b1,b2) -> ManySortedSet of X means

      : Def3: for i be object holds ((b1 . i) <= (b2 . i) implies (it . i) = (b1 . i)) & ((b1 . i) > (b2 . i) implies (it . i) = (b2 . i));

      existence

      proof

        deffunc G( set) = (b2 . $1);

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

        defpred P[ set] means (b1 . $1) <= (b2 . $1);

        consider f be ManySortedSet of X such that

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

        take f;

        let i be object;

        per cases ;

          suppose i in X;

          hence thesis by A1;

        end;

          suppose

           A2: not i in X;

          then not i in ( dom f) by PARTFUN1:def 2;

          then

           A3: (f . i) = 0 by FUNCT_1:def 2;

          ( not i in ( dom b1)) & not i in ( dom b2) by A2, PARTFUN1:def 2;

          hence thesis by A3, FUNCT_1:def 2;

        end;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of X such that

         A4: for i be object holds ((b1 . i) <= (b2 . i) implies (f . i) = (b1 . i)) & ((b1 . i) > (b2 . i) implies (f . i) = (b2 . i)) and

         A5: for i be object holds ((b1 . i) <= (b2 . i) implies (g . i) = (b1 . i)) & ((b1 . i) > (b2 . i) implies (g . i) = (b2 . i));

        now

          let i be object;

          assume i in X;

          per cases ;

            suppose

             A6: (b1 . i) <= (b2 . i);

            

            hence (f . i) = (b1 . i) by A4

            .= (g . i) by A5, A6;

          end;

            suppose

             A7: (b1 . i) > (b2 . i);

            

            hence (f . i) = (b2 . i) by A4

            .= (g . i) by A5, A7;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set;

      let b1,b2 be real-valued ManySortedSet of X;

      cluster ( min (b1,b2)) -> real-valued;

      coherence

      proof

        let x be object;

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

        assume x in ( dom f);

        (b1 . x) <= (b2 . x) or (b1 . x) > (b2 . x);

        hence thesis by Def3;

      end;

    end

    registration

      let X be set;

      let b1,b2 be natural-valued ManySortedSet of X;

      cluster ( min (b1,b2)) -> natural-valued;

      coherence

      proof

        let x be object;

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

        assume x in ( dom f);

        (b1 . x) <= (b2 . x) or (b1 . x) > (b2 . x);

        hence thesis by Def3;

      end;

    end

    theorem :: NAT_3:17

    

     Th17: for X be set, b1,b2 be real-valued finite-support ManySortedSet of X holds ( support ( min (b1,b2))) c= (( support b1) \/ ( support b2))

    proof

      let X be set;

      let b1,b2 be real-valued finite-support ManySortedSet of X;

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

      let x be object;

      assume x in ( support f);

      then

       A1: (f . x) <> 0 by PRE_POLY:def 7;

      (f . x) = (b1 . x) or (f . x) = (b2 . x) by Def3;

      then x in ( support b1) or x in ( support b2) by A1, PRE_POLY:def 7;

      hence thesis by XBOOLE_0:def 3;

    end;

    registration

      let X be set;

      let b1,b2 be real-valued finite-support ManySortedSet of X;

      cluster ( min (b1,b2)) -> finite-support;

      coherence

      proof

        ( support ( min (b1,b2))) c= (( support b1) \/ ( support b2)) by Th17;

        hence ( support ( min (b1,b2))) is finite;

      end;

    end

    definition

      let X be set;

      let b1,b2 be real-valued ManySortedSet of X;

      :: NAT_3:def4

      func max (b1,b2) -> ManySortedSet of X means

      : Def4: for i be object holds ((b1 . i) <= (b2 . i) implies (it . i) = (b2 . i)) & ((b1 . i) > (b2 . i) implies (it . i) = (b1 . i));

      existence

      proof

        deffunc G( set) = (b1 . $1);

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

        defpred P[ set] means (b1 . $1) <= (b2 . $1);

        consider f be ManySortedSet of X such that

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

        take f;

        let i be object;

        per cases ;

          suppose i in X;

          hence thesis by A1;

        end;

          suppose

           A2: not i in X;

          then not i in ( dom f) by PARTFUN1:def 2;

          then

           A3: (f . i) = 0 by FUNCT_1:def 2;

          ( not i in ( dom b1)) & not i in ( dom b2) by A2, PARTFUN1:def 2;

          hence thesis by A3, FUNCT_1:def 2;

        end;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of X such that

         A4: for i be object holds ((b1 . i) <= (b2 . i) implies (f . i) = (b2 . i)) & ((b1 . i) > (b2 . i) implies (f . i) = (b1 . i)) and

         A5: for i be object holds ((b1 . i) <= (b2 . i) implies (g . i) = (b2 . i)) & ((b1 . i) > (b2 . i) implies (g . i) = (b1 . i));

        now

          let i be object;

          assume i in X;

          per cases ;

            suppose

             A6: (b1 . i) <= (b2 . i);

            

            hence (f . i) = (b2 . i) by A4

            .= (g . i) by A5, A6;

          end;

            suppose

             A7: (b1 . i) > (b2 . i);

            

            hence (f . i) = (b1 . i) by A4

            .= (g . i) by A5, A7;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set;

      let b1,b2 be real-valued ManySortedSet of X;

      cluster ( max (b1,b2)) -> real-valued;

      coherence

      proof

        let x be object;

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

        assume x in ( dom f);

        (b1 . x) <= (b2 . x) or (b1 . x) > (b2 . x);

        hence thesis by Def4;

      end;

    end

    registration

      let X be set;

      let b1,b2 be natural-valued ManySortedSet of X;

      cluster ( max (b1,b2)) -> natural-valued;

      coherence

      proof

        let x be object;

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

        assume x in ( dom f);

        (b1 . x) <= (b2 . x) or (b1 . x) > (b2 . x);

        hence thesis by Def4;

      end;

    end

    theorem :: NAT_3:18

    

     Th18: for X be set, b1,b2 be real-valued finite-support ManySortedSet of X holds ( support ( max (b1,b2))) c= (( support b1) \/ ( support b2))

    proof

      let X be set;

      let b1,b2 be real-valued finite-support ManySortedSet of X;

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

      let x be object;

      assume x in ( support f);

      then

       A1: (f . x) <> 0 by PRE_POLY:def 7;

      (f . x) = (b1 . x) or (f . x) = (b2 . x) by Def4;

      then x in ( support b1) or x in ( support b2) by A1, PRE_POLY:def 7;

      hence thesis by XBOOLE_0:def 3;

    end;

    registration

      let X be set;

      let b1,b2 be real-valued finite-support ManySortedSet of X;

      cluster ( max (b1,b2)) -> finite-support;

      coherence

      proof

        ( support ( max (b1,b2))) c= (( support b1) \/ ( support b2)) by Th18;

        hence ( support ( max (b1,b2))) is finite;

      end;

    end

    registration

      let A be set;

      cluster finite-support complex-valued for ManySortedSet of A;

      existence

      proof

        set f = the finite-support natural-valued ManySortedSet of A;

        f is complex-valued;

        hence thesis;

      end;

    end

    definition

      let A be set, b be finite-support complex-valued ManySortedSet of A;

      :: NAT_3:def5

      func Product b -> Complex means

      : Def5: ex f be FinSequence of COMPLEX st it = ( Product f) & f = (b * ( canFS ( support b)));

      existence

      proof

        set cS = ( canFS ( support b));

        set f = (b * cS);

        

         A1: ( rng f) c= COMPLEX by VALUED_0:def 1;

        ( support b) c= ( dom b) & ( rng cS) = ( support b) by FUNCT_2:def 3, PRE_POLY: 37;

        then ( dom f) = ( dom cS) by RELAT_1: 27;

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

        then f is FinSequence by FINSEQ_1:def 2;

        then

        reconsider f as FinSequence of COMPLEX by A1, FINSEQ_1:def 4;

        take ( Product f);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let A be set, b be bag of A;

      :: original: Product

      redefine

      func Product b -> Element of NAT ;

      coherence

      proof

        consider f be FinSequence of COMPLEX such that

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

         A2: f = (b * ( canFS ( support b))) by Def5;

        ( rng b) c= NAT & ( rng f) c= ( rng b) by A2, RELAT_1: 26, VALUED_0:def 6;

        then ( rng f) c= NAT ;

        then

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

        ( Product g) in NAT ;

        hence thesis by A1;

      end;

    end

    theorem :: NAT_3:19

    

     Th19: for X be set, a,b be bag of X st ( support a) misses ( support b) holds ( Product (a + b)) = (( Product a) * ( Product b))

    proof

      let X be set, a,b be bag of X;

      set ab = (a + b);

      set Pa = ( Product a), Pb = ( Product b), Pab = ( Product ab);

      set sab = ( support (a + b));

      set sa = ( support a);

      set sb = ( support b);

      set ca = ( canFS ( support a)), cb = ( canFS ( support b));

      set cg = (ca ^ cb), cf = ( canFS ( support ab));

      set p = ((cg " ) * cf);

      

       A1: ( rng cf) = sab by FUNCT_2:def 3;

      assume ( support a) misses ( support b);

      then

       A2: (( support a) /\ ( support b)) = {} ;

      

       A3: ( rng ca) = sa by FUNCT_2:def 3;

      

       A4: sab = (sa \/ sb) by PRE_POLY: 38;

      

       A5: ( rng cb) = sb by FUNCT_2:def 3;

      then

       A6: ( rng cg) = sab by A4, A3, FINSEQ_1: 31;

      

       A7: ( len cb) = ( card sb) & ( len ca) = ( card sa) by FINSEQ_1: 93;

      

      then

       A8: ( len cg) = ((( card sa) + ( card sb)) - ( card {} )) by FINSEQ_1: 22

      .= ( card sab) by A2, A4, CARD_2: 45;

      then

       A9: cg is one-to-one by A6, FINSEQ_4: 62;

      then

       A10: ( dom (cg " )) = sab by A6, FUNCT_1: 33;

      then

       A11: ( rng p) = ( rng (cg " )) by A1, RELAT_1: 28;

      ( dom cg) = ( Seg ( card sab)) by A8, FINSEQ_1:def 3;

      then

       A12: ( rng (cg " )) = ( Seg ( card sab)) by A9, FUNCT_1: 33;

      consider fa be FinSequence of COMPLEX such that

       A13: Pa = ( Product fa) and

       A14: fa = (a * ( canFS ( support a))) by Def5;

      consider fb be FinSequence of COMPLEX such that

       A15: Pb = ( Product fb) and

       A16: fb = (b * ( canFS ( support b))) by Def5;

      set g = (fa ^ fb);

      consider f be FinSequence of COMPLEX such that

       A17: Pab = ( Product f) and

       A18: f = (ab * ( canFS ( support ab))) by Def5;

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

      then

       A19: ( dom ca) = ( dom fa) by A14, A3, RELAT_1: 27;

      then

       A20: ( len ca) = ( len fa) by FINSEQ_3: 29;

      ( len cf) = ( card sab) by FINSEQ_1: 93;

      then

       A21: ( dom cf) = ( Seg ( card sab)) by FINSEQ_1:def 3;

      then

       A22: ( dom p) = ( Seg ( card sab)) by A1, A10, RELAT_1: 27;

      

       A23: ( dom ab) = X by PARTFUN1:def 2;

      then

       A24: ( dom f) = ( Seg ( card sab)) by A18, A21, A1, RELAT_1: 27;

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

      then ( dom cb) = ( dom fb) by A16, A5, RELAT_1: 27;

      then

       A25: ( len cb) = ( len fb) by FINSEQ_3: 29;

      

      then ( len g) = ((( card sa) + ( card sb)) - ( card {} )) by A7, A20, FINSEQ_1: 22

      .= ( card sab) by A2, A4, CARD_2: 45;

      then

       A26: ( dom g) = ( Seg ( card sab)) by FINSEQ_1:def 3;

      then

      reconsider p as Function of ( dom g), ( dom g) by A12, A22, A11, FUNCT_2: 1;

      p is onto by A12, A26, A11, FUNCT_2:def 3;

      then

      reconsider p as Permutation of ( dom g) by A9;

      

       A27: ( dom (g * p)) = ( Seg ( card sab)) by A12, A22, A26, A11, RELAT_1: 27;

      

       A28: ( len cg) = (( len ca) + ( len cb)) by FINSEQ_1: 22;

      now

        let x be object;

        set cgx = ((cg " ) . (cf . x));

        assume

         A29: x in ( dom f);

        

        then

         A30: ((g * p) . x) = (g . (p . x)) by A24, A27, FUNCT_1: 12

        .= (g . cgx) by A21, A24, A29, FUNCT_1: 13;

        

         A31: (cf . x) in sab by A21, A1, A24, A29, FUNCT_1: 3;

        then

        consider d be object such that

         A32: d in ( dom cg) and

         A33: (cg . d) = (cf . x) by A6, FUNCT_1:def 3;

        cgx in ( Seg ( card sab)) by A10, A12, A31, FUNCT_1: 3;

        then

        reconsider cgx as Nat;

        reconsider cgxN = cgx as Nat;

        

         A34: cgx = d by A9, A32, A33, FUNCT_1: 34;

        then

         A35: 1 <= cgxN by A32, FINSEQ_3: 25;

        

         A36: cgxN <= (( len fa) + ( len fb)) by A20, A25, A28, A32, A34, FINSEQ_3: 25;

        per cases by A4, A31, XBOOLE_0:def 3;

          suppose (cf . x) in sa;

          then

           A37: not (cf . x) in sb by A2, XBOOLE_0:def 4;

          now

            

             A38: (cgx - ( len ca)) <= ((( len ca) + ( len cb)) - ( len ca)) by A20, A25, A36, XREAL_1: 9;

            assume ( len fa) < cgx;

            then

             A39: (( len fa) + 1) <= cgx by NAT_1: 13;

            then

             A40: ((( len ca) + 1) - ( len ca)) <= (cgx - ( len ca)) by A20, XREAL_1: 9;

            then (cgx - ( len ca)) is Element of NAT by INT_1: 3;

            then

             A41: (cgx - ( len ca)) in ( dom cb) by A40, A38, FINSEQ_3: 25;

            (cg . cgxN) = (cb . (cgx - ( len ca))) by A20, A25, A36, A39, FINSEQ_1: 23;

            hence contradiction by A5, A33, A34, A37, A41, FUNCT_1: 3;

          end;

          then

           A42: cgxN in ( dom fa) by A35, FINSEQ_3: 25;

          then

           A43: (cg . cgx) = (ca . cgx) by A19, FINSEQ_1:def 7;

          

           A44: (g . cgx) = (fa . cgxN) by A42, FINSEQ_1:def 7

          .= (a . (cf . x)) by A14, A19, A33, A34, A42, A43, FUNCT_1: 13;

          

          thus (f . x) = (ab . (cf . x)) by A18, A29, FUNCT_1: 12

          .= ((a . (cf . x)) + (b . (cf . x))) by PRE_POLY:def 5

          .= ((a . (cf . x)) + 0 ) by A37, PRE_POLY:def 7

          .= ((g * p) . x) by A30, A44;

        end;

          suppose

           A45: (cf . x) in sb;

           A46:

          now

            assume (( len fa) + 1) > cgx;

            then cgx <= ( len fa) by NAT_1: 13;

            then

             A47: cgx in ( dom ca) by A19, A35, FINSEQ_3: 25;

            then (ca . cgx) in sa by A3, FUNCT_1: 3;

            then (cg . cgxN) in sa by A47, FINSEQ_1:def 7;

            hence contradiction by A2, A33, A34, A45, XBOOLE_0:def 4;

          end;

          then

           A48: (cg . cgx) = (cb . (cgx - ( len ca))) by A20, A25, A36, FINSEQ_1: 23;

          

           A49: (cgx - ( len ca)) <= ((( len ca) + ( len cb)) - ( len ca)) by A20, A25, A36, XREAL_1: 9;

          

           A50: ((( len ca) + 1) - ( len ca)) <= (cgx - ( len ca)) by A20, A46, XREAL_1: 9;

          then (cgxN - ( len ca)) in NAT by INT_1: 3;

          then

           A51: (cgxN - ( len ca)) in ( dom cb) by A49, A50, FINSEQ_3: 25;

          

           A52: (g . cgx) = (fb . (cgxN - ( len fa))) by A36, A46, FINSEQ_1: 23

          .= (b . (cf . x)) by A16, A20, A33, A34, A48, A51, FUNCT_1: 13;

          

           A53: not (cf . x) in sa by A2, A45, XBOOLE_0:def 4;

          

          thus (f . x) = (ab . (cf . x)) by A18, A29, FUNCT_1: 12

          .= ((a . (cf . x)) + (b . (cf . x))) by PRE_POLY:def 5

          .= ( 0 + (b . (cf . x))) by A53, PRE_POLY:def 7

          .= ((g * p) . x) by A30, A52;

        end;

      end;

      then

       A54: f = (g * p) by A18, A21, A1, A23, A27, FUNCT_1: 2, RELAT_1: 27;

      

      thus ( Product (a + b)) = ( multcomplex $$ f) by A17, RVSUM_1:def 13

      .= ( multcomplex $$ g) by A54, FINSOP_1: 7

      .= ( Product g) by RVSUM_1:def 13

      .= (( Product a) * ( Product b)) by A13, A15, RVSUM_1: 97;

    end;

    definition

      let X be set, b be real-valued ManySortedSet of X, n be non zero Nat;

      :: NAT_3:def6

      func b |^ n -> ManySortedSet of X means

      : Def6: ( support it ) = ( support b) & for i be object holds (it . i) = ((b . i) |^ n);

      existence

      proof

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

        deffunc F( Element of X) = ((b . $1) |^ n);

        defpred P[ object, object] means ex a be Element of X st a = $1 & $2 = F(a);

        

         A1: n1 >= 1 by NAT_1: 53;

        

         A2: for e be object st e in X holds ex u be object st P[e, u]

        proof

          let e be object;

          assume e in X;

          then

          reconsider f = e as Element of X;

          take F(f), f;

          thus thesis;

        end;

        consider f be Function such that

         A3: ( dom f) = X and

         A4: for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A2);

        reconsider f as ManySortedSet of X by A3, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        

         A5: ( dom b) = X by PARTFUN1:def 2;

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          hereby

            assume

             A6: x in ( support f);

            assume not x in ( support b);

            then (b . x) = 0 by PRE_POLY:def 7;

            then

             A7: ((b . xx) |^ n) = 0 by A1, NEWTON: 11;

            ( support f) c= X by A3, PRE_POLY: 37;

            then P[x, (f . x)] by A4, A6;

            hence contradiction by A6, A7, PRE_POLY:def 7;

          end;

           A8:

          now

            per cases ;

              suppose x in X;

              then P[x, (f . x)] by A4;

              hence (f . x) = ((b . xx) |^ n1);

            end;

              suppose

               A9: not x in X;

              

              hence (f . x) = 0 by A3, FUNCT_1:def 2

              .= ( 0 qua Nat |^ n1) by A1, NEWTON: 11

              .= ((b . xx) |^ n1) by A5, A9, FUNCT_1:def 2;

            end;

          end;

          assume x in ( support b);

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

          then (f . x) <> 0 by A8, CARD_4: 3;

          hence x in ( support f) by PRE_POLY:def 7;

        end;

        hence ( support f) = ( support b) by TARSKI: 2;

        let i be object;

        per cases ;

          suppose i in X;

          then P[i, (f . i)] by A4;

          hence thesis;

        end;

          suppose

           A10: not i in X;

          

          hence (f . i) = 0 by A3, FUNCT_1:def 2

          .= ( 0 qua Nat |^ n) by A1, NEWTON: 11

          .= ((b . i) |^ n) by A5, A10, FUNCT_1:def 2;

        end;

      end;

      uniqueness

      proof

        let it1,it2 be ManySortedSet of X such that ( support it1) = ( support b) and

         A11: for i be object holds (it1 . i) = ((b . i) |^ n) and ( support it2) = ( support b) and

         A12: for i be object holds (it2 . i) = ((b . i) |^ n);

        now

          let x be object such that x in X;

          

          thus (it1 . x) = ((b . x) |^ n) by A11

          .= (it2 . x) by A12;

        end;

        hence it1 = it2;

      end;

    end

    registration

      let X be set, b be natural-valued ManySortedSet of X, n be non zero Nat;

      cluster (b |^ n) -> natural-valued;

      coherence

      proof

        let x be object;

        set f = (b |^ n);

        assume x in ( dom f);

        (f . x) = ((b . x) |^ n) by Def6;

        hence thesis;

      end;

    end

    registration

      let X be set, b be real-valued finite-support ManySortedSet of X, n be non zero Nat;

      cluster (b |^ n) -> finite-support;

      coherence

      proof

        ( support (b |^ n)) = ( support b) by Def6;

        hence ( support (b |^ n)) is finite;

      end;

    end

    theorem :: NAT_3:20

    

     Th20: for A be set holds ( Product ( EmptyBag A)) = 1

    proof

      let A be set;

      set b = ( EmptyBag A);

      set cS = ( canFS ( support b));

      (b * cS) = ( <*> COMPLEX );

      hence thesis by Def5, RVSUM_1: 94;

    end;

    begin

    definition

      let n,d be Nat;

      :: NAT_3:def7

      func d |-count n -> Nat means

      : Def7: (d |^ it ) divides n & not (d |^ (it + 1)) divides n;

      existence

      proof

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

        per cases ;

          suppose

           A3: d = 0 ;

          take 0 ;

          ( 0 qua Nat |^ 0 ) = 1 by NEWTON: 4;

          hence (d |^ 0 ) divides n by A3, NAT_D: 6;

           not 0 divides n1 by A2;

          hence not (d |^ ( 0 + 1)) divides n by A3;

        end;

          suppose

           A4: d <> 0 ;

          defpred P[ Nat] means (d |^ $1) divides n;

          

           A5: for k be Nat st P[k] holds k <= n1

          proof

            let k be Nat;

            assume P[k];

            then

             A6: (d |^ k) <= n by A2, NAT_D: 7;

            k <= (d |^ k) by A1, A4, Th2, NAT_1: 25;

            hence thesis by A6, XXREAL_0: 2;

          end;

          

           A7: ex k be Nat st P[k]

          proof

            take 0 ;

            (d |^ 0 ) = 1 by NEWTON: 4;

            hence thesis by NAT_D: 6;

          end;

          consider k be Nat such that

           A8: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A5, A7);

          take k;

          (k + 0 qua Nat) < (k + 1) by XREAL_1: 6;

          hence thesis by A8;

        end;

      end;

      uniqueness

      proof

        reconsider d1 = d as Element of NAT by ORDINAL1:def 12;

        let a,b be Nat such that

         A9: (d |^ a) divides n and

         A10: ( not (d |^ (a + 1)) divides n) & (d |^ b) divides n and

         A11: not (d |^ (b + 1)) divides n and

         A12: a <> b;

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

        per cases by A12, XXREAL_0: 1;

          suppose

           A13: a < b;

          then

          consider x be Nat such that

           A14: (a + x) = b by NAT_1: 10;

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

          now

            assume ( 0 + 1) > x;

            then x = 0 by NAT_1: 13;

            hence contradiction by A13, A14;

          end;

          then (a + 1) <= (a + x) by XREAL_1: 6;

          then (d1 |^ (a + 1)) divides (d1 |^ (a + x)) by NEWTON: 89;

          hence contradiction by A10, A14, NAT_D: 4;

        end;

          suppose

           A15: b < a;

          then

          consider x be Nat such that

           A16: (b + x) = a by NAT_1: 10;

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

          now

            assume ( 0 + 1) > x;

            then x = 0 by NAT_1: 13;

            hence contradiction by A15, A16;

          end;

          then (b + 1) <= (b + x) by XREAL_1: 6;

          then (d1 |^ (b + 1)) divides (d1 |^ (b + x)) by NEWTON: 89;

          hence contradiction by A9, A11, A16, NAT_D: 4;

        end;

      end;

    end

    definition

      let n,d be Nat;

      :: original: |-count

      redefine

      func d |-count n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: NAT_3:21

    

     Th21: n <> 1 implies (n |-count 1) = 0

    proof

      assume

       A1: 1 <> n;

       A2:

      now

        assume

         A3: (n |^ ( 0 + 1)) divides 1;

        then (n |^ 1) <= 1 by NAT_D: 7;

        then n <= 1;

        then n = 0 by A1, NAT_1: 25;

        then 0 divides 1 by A3;

        hence contradiction;

      end;

      (n |^ 0 ) divides 1 by NEWTON: 4;

      hence thesis by A2, Def7;

    end;

    theorem :: NAT_3:22

    1 < n implies (n |-count n) = 1

    proof

      assume

       A1: 1 < n;

       A2:

      now

        assume (n |^ (1 + 1)) divides n;

        then (n |^ 2) <= n by A1, NAT_D: 7;

        hence contradiction by A1, PREPOWER: 13;

      end;

      (n |^ 1) divides n;

      hence thesis by A1, A2, Def7;

    end;

    theorem :: NAT_3:23

    

     Th23: b <> 0 & b < a & a <> 1 implies (a |-count b) = 0

    proof

      assume that

       A1: b <> 0 and

       A2: b < a and

       A3: a <> 1;

      (a |^ 0 ) = 1 by NEWTON: 4;

      then

       A4: (a |^ 0 ) divides b by NAT_D: 6;

       not (a |^ ( 0 + 1)) divides b by A1, A2, NAT_D: 7;

      hence thesis by A1, A3, A4, Def7;

    end;

    theorem :: NAT_3:24

    a <> 1 & a <> p implies (a |-count p) = 0

    proof

      assume that

       A1: a <> 1 and

       A2: a <> p;

      (a |^ 0 ) = 1 by NEWTON: 4;

      then

       A3: (a |^ 0 ) divides p by NAT_D: 6;

       not (a |^ ( 0 + 1)) divides p by A1, A2, INT_2:def 4;

      hence thesis by A1, A3, Def7;

    end;

    theorem :: NAT_3:25

    

     Th25: 1 < b implies (b |-count (b |^ a)) = a

    proof

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

      assume

       A1: b > 1;

      then

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

      now

        (b |^ a) divides (b |^ (a + 1)) by NAT_1: 11, NEWTON: 89;

        then

         A2: (b |^ a) <= (b |^ (a + 1)) by NAT_D: 7;

        assume (b |^ (a + 1)) divides (b |^ a);

        then (b |^ (a + 1)) <= (b |^ a) by NAT_D: 7;

        then (b |^ a) = (b |^ (a + 1)) by A2, XXREAL_0: 1;

        then (a + 0 ) = (a + 1) by A1, PEPIN: 30;

        hence contradiction;

      end;

      hence thesis by A1, Def7;

    end;

    theorem :: NAT_3:26

    

     Th26: b <> 1 & a <> 0 & b divides (b |^ (b |-count a)) implies b divides a

    proof

      assume that

       A1: b <> 1 & a <> 0 and

       A2: b divides (b |^ (b |-count a));

      (b |^ (b |-count a)) divides a by A1, Def7;

      hence thesis by A2, NAT_D: 4;

    end;

    theorem :: NAT_3:27

    

     Th27: b <> 1 implies (a <> 0 & (b |-count a) = 0 iff not b divides a)

    proof

      1 divides a by NAT_D: 6;

      then

       A1: (b |^ 0 ) divides a by NEWTON: 4;

      assume

       A2: b <> 1;

      thus a <> 0 & (b |-count a) = 0 implies not b divides a

      proof

        assume that

         A3: a <> 0 & (b |-count a) = 0 and

         A4: b divides a;

         not (b |^ ( 0 + 1)) divides a by A2, A3, Def7;

        hence contradiction by A4;

      end;

      assume not b divides a;

      then ( not (b |^ ( 0 + 1)) divides a) & a <> 0 by NAT_D: 6;

      hence thesis by A2, A1, Def7;

    end;

    theorem :: NAT_3:28

    

     Th28: for a,b be non zero Nat holds (p |-count (a * b)) = ((p |-count a) + (p |-count b))

    proof

      let a,b be non zero Nat;

      set x = (p |-count a);

      set y = (p |-count b);

      

       A1: p <> 1 by INT_2:def 4;

      then

       A2: (p |^ y) divides b by Def7;

      

       A3: (p |^ x) divides a by A1, Def7;

       A4:

      now

        assume (p |^ ((x + y) + 1)) divides (a * b);

        then

        consider v be Nat such that

         A5: (a * b) = ((p |^ ((x + y) + 1)) * v);

        (p |^ ((x + y) + 1)) = ((p |^ (x + y)) * p) by NEWTON: 6;

        then

         A6: (a * b) = ((p |^ (x + y)) * (p * v)) by A5;

        consider t be Nat such that

         A7: a = ((p |^ x) * t) by A3;

        

         A8: not (p |^ (x + 1)) divides a by A1, Def7;

        

         A9: not (p |^ (y + 1)) divides b by A1, Def7;

        consider u be Nat such that

         A10: b = ((p |^ y) * u) by A2;

        (a * b) = ((((p |^ x) * (p |^ y)) * t) * u) by A7, A10

        .= (((p |^ (x + y)) * t) * u) by NEWTON: 8

        .= ((p |^ (x + y)) * (t * u));

        then (p * v) = (t * u) by A6, XCMPLX_1: 5;

        then

         A11: p divides (t * u);

        per cases by A11, NEWTON: 80;

          suppose p divides t;

          then

          consider t1 be Nat such that

           A12: t = (p * t1);

          a = (((p |^ x) * p) * t1) by A7, A12

          .= ((p |^ (x + 1)) * t1) by NEWTON: 6;

          hence contradiction by A8;

        end;

          suppose p divides u;

          then

          consider t1 be Nat such that

           A13: u = (p * t1);

          b = (((p |^ y) * p) * t1) by A10, A13

          .= ((p |^ (y + 1)) * t1) by NEWTON: 6;

          hence contradiction by A9;

        end;

      end;

      (p |^ (x + y)) = ((p |^ x) * (p |^ y)) by NEWTON: 8;

      then (p |^ (x + y)) divides (a * b) by A3, A2, Th1;

      hence thesis by A1, A4, Def7;

    end;

    theorem :: NAT_3:29

    

     Th29: for a,b be non zero Nat holds (p |^ (p |-count (a * b))) = ((p |^ (p |-count a)) * (p |^ (p |-count b)))

    proof

      let a,b be non zero Nat;

      set x = (p |-count a);

      set y = (p |-count b);

      

      thus (p |^ (p |-count (a * b))) = (p |^ (x + y)) by Th28

      .= ((p |^ x) * (p |^ y)) by NEWTON: 8;

    end;

    theorem :: NAT_3:30

    

     Th30: for a,b be non zero Nat st b divides a holds (p |-count b) <= (p |-count a)

    proof

      let a,b be non zero Nat;

      set x = (p |-count a);

      set y = (p |-count b);

      set z = (p |-count (a div b));

      ( 0 + 1) <= (p |^ z) by NAT_1: 13;

      then

       A1: (1 * (p |^ y)) <= ((p |^ z) * (p |^ y)) by XREAL_1: 66;

      assume b divides a;

      then

       A2: a = (b * (a div b)) by NAT_D: 3;

      then (a div b) <> 0 ;

      then p > 1 & (p |^ y) <= (p |^ x) by A2, A1, Th29, INT_2:def 4;

      hence thesis by PEPIN: 66;

    end;

    theorem :: NAT_3:31

    

     Th31: for a,b be non zero Nat st b divides a holds (p |-count (a div b)) = ((p |-count a) -' (p |-count b))

    proof

      let a,b be non zero Nat;

      set x = (p |-count a);

      set y = (p |-count b);

      set z = (p |-count (a div b));

      assume

       A1: b divides a;

      then a = (b * (a div b)) by NAT_D: 3;

      then (a div b) <> 0 ;

      then (p |-count (b * (a div b))) = (y + z) by Th28;

      then

       A2: (z + y) = (x + 0 ) by A1, NAT_D: 3;

      y <= x by A1, Th30;

      then (y - y) <= (x - y) by XREAL_1: 13;

      hence thesis by A2, XREAL_0:def 2;

    end;

    theorem :: NAT_3:32

    

     Th32: for a be non zero Nat holds (p |-count (a |^ b)) = (b * (p |-count a))

    proof

      let a be non zero Nat;

      

       A1: p <> 1 by INT_2:def 4;

      defpred P[ Nat] means (p |-count (a |^ $1)) = ($1 * (p |-count a));

      

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

      proof

        let x be Nat such that

         A3: P[x];

        

        thus (p |-count (a |^ (x + 1))) = (p |-count ((a |^ x) * a)) by NEWTON: 6

        .= ((x * (p |-count a)) + (1 * (p |-count a))) by A3, Th28

        .= ((x + 1) * (p |-count a));

      end;

      (p |-count (a |^ 0 )) = (p |-count 1) by NEWTON: 4

      .= ( 0 * (p |-count a)) by A1, Th21;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    begin

    definition

      let n be Nat;

      :: NAT_3:def8

      func prime_exponents n -> ManySortedSet of SetPrimes means

      : Def8: for p be Prime holds (it . p) = (p |-count n);

      existence

      proof

        deffunc F( Nat) = ($1 |-count n);

        defpred P[ object, object] means ex w be Nat st w = $1 & $2 = F(w);

        

         A1: for i be object st i in SetPrimes holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in SetPrimes ;

          then

          reconsider i as prime Element of NAT by NEWTON:def 6;

          take F(i), i;

          thus thesis;

        end;

        consider f be ManySortedSet of SetPrimes such that

         A2: for i be object st i in SetPrimes holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        take f;

        let i be Prime;

        i in SetPrimes by NEWTON:def 6;

        then P[i, (f . i)] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of SetPrimes such that

         A3: for i be Prime holds (f . i) = (i |-count n) and

         A4: for i be Prime holds (g . i) = (i |-count n);

        now

          let i be object;

          assume i in SetPrimes ;

          then

          reconsider a = i as prime Element of NAT by NEWTON:def 6;

          

          thus (f . i) = (a |-count n) by A3

          .= (g . i) by A4;

        end;

        hence thesis;

      end;

    end

    notation

      let n be Nat;

      synonym pfexp n for prime_exponents n;

    end

    theorem :: NAT_3:33

    

     Th33: for x be set st x in ( dom ( pfexp n)) holds x is Prime

    proof

      let x be set;

      assume x in ( dom ( pfexp n));

      then x in SetPrimes by PARTFUN1:def 2;

      hence thesis by NEWTON:def 6;

    end;

    theorem :: NAT_3:34

    

     Th34: for x be set st x in ( support ( pfexp n)) holds x is Prime

    proof

      let x be set;

      set f = ( pfexp n);

      

       A1: ( support f) c= ( dom f) by PRE_POLY: 37;

      assume x in ( support f);

      hence thesis by A1, Th33;

    end;

    theorem :: NAT_3:35

    

     Th35: a > n & n <> 0 implies (( pfexp n) . a) = 0

    proof

      assume

       A1: a > n & n <> 0 ;

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

      per cases ;

        suppose not a is prime;

        then not a in ( dom ( pfexp n)) by Th33;

        hence thesis by FUNCT_1:def 2;

      end;

        suppose

         A2: a is prime;

        then a <> 1;

        then (a |-count n) = 0 by A1, Th23;

        hence thesis by A2, Def8;

      end;

    end;

    registration

      let n be Nat;

      cluster ( pfexp n) -> natural-valued;

      coherence

      proof

        let x be object;

        set f = ( pfexp n);

        assume x in ( dom f);

        then

        reconsider x as Prime by Th33;

        (f . x) = (x |-count n) by Def8;

        hence thesis;

      end;

    end

    theorem :: NAT_3:36

    a in ( support ( pfexp b)) implies a divides b

    proof

      set f = ( pfexp b);

      assume

       A1: a in ( support f);

      then

      reconsider a as Prime by Th34;

      

       A2: a <> 1 & (f . a) = (a |-count b) by Def8, INT_2:def 4;

      (f . a) <> 0 by A1, PRE_POLY:def 7;

      hence thesis by A2, Th27;

    end;

    theorem :: NAT_3:37

    

     Th37: b is non empty & a is Prime & a divides b implies a in ( support ( pfexp b))

    proof

      assume that

       A1: b is non empty and

       A2: a is Prime and

       A3: a divides b;

      1 < a by A2, INT_2:def 4;

      then

       A4: (a |-count b) <> 0 by A1, A3, Th27;

      (( pfexp b) . a) = (a |-count b) by A2, Def8;

      hence thesis by A4, PRE_POLY:def 7;

    end;

    registration

      let n be non zero Nat;

      cluster ( pfexp n) -> finite-support;

      coherence

      proof

        defpred P[ Nat] means $1 is prime;

        deffunc F( set) = $1;

        set f = ( pfexp n);

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

        set A = { F(i) where i be Nat : i <= n & P[i] };

        

         A1: ( support f) c= A

        proof

          let x be object;

          assume

           A2: x in ( support f);

          then

          reconsider x as Prime by Th34;

          (f . x) <> 0 by A2, PRE_POLY:def 7;

          then x is prime Element of NAT & x <= n by Th35, ORDINAL1:def 12;

          hence thesis;

        end;

        A is finite from FINSEQ_1:sch 6;

        hence ( support f) is finite by A1;

      end;

    end

    theorem :: NAT_3:38

    

     Th38: for a be non zero Nat st p divides a holds (( pfexp a) . p) <> 0

    proof

      let a be non zero Nat;

      assume p divides a;

      then

       A1: (p |^ ( 0 + 1)) divides a;

      (( pfexp a) . p) = (p |-count a) & p <> 1 by Def8, INT_2:def 4;

      hence thesis by A1, Def7;

    end;

    theorem :: NAT_3:39

    

     Th39: ( pfexp 1) = ( EmptyBag SetPrimes )

    proof

      set f = ( pfexp 1);

      for z be object st z in ( dom f) holds (f . z) = 0

      proof

        let z be object;

        assume z in ( dom f);

        then

        reconsider z as Prime by Th33;

        

         A1: z <> 1 by INT_2:def 4;

        (f . z) = (z |-count 1) by Def8

        .= 0 by A1, Th21;

        hence thesis;

      end;

      then

       A2: f = (( dom f) --> 0 ) by FUNCOP_1: 11;

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

      hence thesis by A2;

    end;

    registration

      cluster ( support ( pfexp 1)) -> empty;

      coherence by Th39;

    end

    theorem :: NAT_3:40

    

     Th40: (( pfexp (p |^ a)) . p) = a

    proof

      set f = ( pfexp (p |^ a));

      p > 1 & (f . p) = (p |-count (p |^ a)) by Def8, INT_2:def 4;

      hence thesis by Th25;

    end;

    theorem :: NAT_3:41

    (( pfexp p) . p) = 1

    proof

      p = (p |^ 1);

      hence thesis by Th40;

    end;

    theorem :: NAT_3:42

    

     Th42: a <> 0 implies ( support ( pfexp (p |^ a))) = {p}

    proof

      set f = ( pfexp (p |^ a));

      assume a <> 0 ;

      then p divides (p |^ a) by Th3;

      then

       A1: (f . p) <> 0 by Th38;

      thus ( support f) c= {p}

      proof

        let x be object;

        assume

         A2: x in ( support f);

        then

        reconsider x as Prime by Th34;

        

         A3: x <> 1 & (f . x) = (x |-count (p |^ a)) by Def8, INT_2:def 4;

        (f . x) <> 0 by A2, PRE_POLY:def 7;

        then x divides (p |^ a) by A3, Th27;

        then x = p by Th6;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {p};

      then x = p by TARSKI:def 1;

      hence thesis by A1, PRE_POLY:def 7;

    end;

    theorem :: NAT_3:43

    

     Th43: ( support ( pfexp p)) = {p}

    proof

      p = (p |^ 1);

      hence thesis by Th42;

    end;

    registration

      let p be Prime;

      let a be non zero Nat;

      cluster ( support ( pfexp (p |^ a))) -> 1 -element;

      coherence

      proof

        ( support ( pfexp (p |^ a))) = {p} by Th42;

        hence thesis;

      end;

    end

    registration

      let p be Prime;

      cluster ( support ( pfexp p)) -> 1 -element;

      coherence

      proof

        ( support ( pfexp p)) = {p} by Th43;

        hence thesis;

      end;

    end

    theorem :: NAT_3:44

    

     Th44: for a,b be non zero Nat st (a,b) are_coprime holds ( support ( pfexp a)) misses ( support ( pfexp b))

    proof

      let a,b be non zero Nat;

      set f = ( pfexp a);

      set g = ( pfexp b);

      assume (a,b) are_coprime ;

      then

       A1: (a gcd b) = 1;

      assume ( support f) meets ( support g);

      then

      consider x be object such that

       A2: x in ( support f) and

       A3: x in ( support g) by XBOOLE_0: 3;

      reconsider x as Prime by A2, Th34;

      

       A4: (f . x) = (x |-count a) by Def8;

      

       A5: (g . x) = (x |-count b) by Def8;

      (g . x) <> 0 by A3, PRE_POLY:def 7;

      then

       A6: x divides (x |^ (x |-count b)) by A5, Th3;

      

       A7: x <> 1 by INT_2:def 4;

      then (x |^ (x |-count b)) divides b by Def7;

      then

       A8: x divides b by A6, NAT_D: 4;

      (f . x) <> 0 by A2, PRE_POLY:def 7;

      then

       A9: x divides (x |^ (x |-count a)) by A4, Th3;

      (x |^ (x |-count a)) divides a by A7, Def7;

      then x divides a by A9, NAT_D: 4;

      then x divides 1 by A1, A8, NAT_D:def 5;

      hence contradiction by A7, WSIERP_1: 15;

    end;

    theorem :: NAT_3:45

    

     Th45: for a,b be non zero Nat holds ( support ( pfexp a)) c= ( support ( pfexp (a * b)))

    proof

      let a,b be non zero Nat;

      set f = ( pfexp a);

      set h = ( pfexp (a * b));

      let x be object;

      assume

       A1: x in ( support f);

      then

      reconsider x as Prime by Th34;

      

       A2: (f . x) = (x |-count a) by Def8;

      (f . x) <> 0 by A1, PRE_POLY:def 7;

      then

       A3: x divides (x |^ (x |-count a)) by A2, Th3;

      

       A4: x <> 1 by INT_2:def 4;

      then (x |^ (x |-count a)) divides a by Def7;

      then x divides a by A3, NAT_D: 4;

      then (x |^ 1) divides a;

      then

       A5: (x |^ ( 0 + 1)) divides (a * b) by NAT_D: 9;

      (h . x) = (x |-count (a * b)) by Def8;

      then (h . x) <> 0 by A4, A5, Def7;

      hence thesis by PRE_POLY:def 7;

    end;

    theorem :: NAT_3:46

    

     Th46: for a,b be non zero Nat holds ( support ( pfexp (a * b))) = (( support ( pfexp a)) \/ ( support ( pfexp b)))

    proof

      let a,b be non zero Nat;

      set f = ( pfexp a);

      set g = ( pfexp b);

      set h = ( pfexp (a * b));

      thus ( support h) c= (( support f) \/ ( support g))

      proof

        let x be object;

        assume

         A1: x in ( support h);

        then

        reconsider x as Prime by Th34;

        

         A2: (h . x) <> 0 by A1, PRE_POLY:def 7;

        

         A3: x <> 1 by INT_2:def 4;

        

         A4: (h . x) = (x |-count (a * b)) & (x |^ (x |-count (a * b))) = ((x |^ (x |-count a)) * (x |^ (x |-count b))) by Def8, Th29;

        per cases by A2, A4, Th3, NEWTON: 80;

          suppose x divides (x |^ (x |-count a));

          then x divides a by A3, Th26;

          then (f . x) <> 0 by Th38;

          then x in ( support f) by PRE_POLY:def 7;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x divides (x |^ (x |-count b));

          then x divides b by A3, Th26;

          then (g . x) <> 0 by Th38;

          then x in ( support g) by PRE_POLY:def 7;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ( support f) c= ( support h) & ( support g) c= ( support h) by Th45;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: NAT_3:47

    for a,b be non zero Nat st (a,b) are_coprime holds ( card ( support ( pfexp (a * b)))) = (( card ( support ( pfexp a))) + ( card ( support ( pfexp b))))

    proof

      let a,b be non zero Nat;

      assume

       A1: (a,b) are_coprime ;

      ( support ( pfexp (a * b))) = (( support ( pfexp a)) \/ ( support ( pfexp b))) by Th46;

      hence thesis by A1, Th44, CARD_2: 40;

    end;

    theorem :: NAT_3:48

    for a,b be non zero Nat holds ( support ( pfexp a)) = ( support ( pfexp (a |^ b)))

    proof

      let a,b be non zero Nat;

      set f = ( pfexp a);

      set g = ( pfexp (a |^ b));

      (a |^ b) = ((a |^ (b -' 1)) * a) by PEPIN: 26;

      hence ( support f) c= ( support g) by Th45;

      let x be object;

      assume

       A1: x in ( support g);

      then

      reconsider x as Prime by Th34;

      

       A2: (g . x) = (x |-count (a |^ b)) & x <> 1 by Def8, INT_2:def 4;

      (g . x) <> 0 by A1, PRE_POLY:def 7;

      then x divides (a |^ b) by A2, Th27;

      then (f . x) <> 0 by Th5, Th38;

      hence thesis by PRE_POLY:def 7;

    end;

    reserve n,m for non zero Nat;

    theorem :: NAT_3:49

    ( pfexp (n * m)) = (( pfexp n) + ( pfexp m))

    proof

      for i be object st i in SetPrimes holds (( pfexp (n * m)) . i) = ((( pfexp n) + ( pfexp m)) . i)

      proof

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider a = i as prime Element of NAT by NEWTON:def 6;

        

        thus (( pfexp (n * m)) . i) = (a |-count (n * m)) by Def8

        .= ((a |-count n) + (a |-count m)) by Th28

        .= ((( pfexp n) . i) + (a |-count m)) by Def8

        .= ((( pfexp n) . i) + (( pfexp m) . i)) by Def8

        .= ((( pfexp n) + ( pfexp m)) . i) by PRE_POLY:def 5;

      end;

      hence thesis;

    end;

    theorem :: NAT_3:50

    m divides n implies ( pfexp (n div m)) = (( pfexp n) -' ( pfexp m))

    proof

      assume

       A1: m divides n;

      for i be object st i in SetPrimes holds (( pfexp (n div m)) . i) = ((( pfexp n) -' ( pfexp m)) . i)

      proof

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider a = i as prime Element of NAT by NEWTON:def 6;

        

        thus (( pfexp (n div m)) . i) = (a |-count (n div m)) by Def8

        .= ((a |-count n) -' (a |-count m)) by A1, Th31

        .= ((( pfexp n) . i) -' (a |-count m)) by Def8

        .= ((( pfexp n) . i) -' (( pfexp m) . i)) by Def8

        .= ((( pfexp n) -' ( pfexp m)) . i) by PRE_POLY:def 6;

      end;

      hence thesis;

    end;

    theorem :: NAT_3:51

    ( pfexp (n |^ a)) = (a * ( pfexp n))

    proof

      for i be object st i in SetPrimes holds (( pfexp (n |^ a)) . i) = ((a * ( pfexp n)) . i)

      proof

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider x = i as prime Element of NAT by NEWTON:def 6;

        

        thus (( pfexp (n |^ a)) . i) = (x |-count (n |^ a)) by Def8

        .= (a * (x |-count n)) by Th32

        .= (a * (( pfexp n) . i)) by Def8

        .= ((a * ( pfexp n)) . i) by Def2;

      end;

      hence thesis;

    end;

    theorem :: NAT_3:52

    

     Th52: ( support ( pfexp n)) = {} implies n = 1

    proof

      assume that

       A1: ( support ( pfexp n)) = {} and

       A2: n <> 1;

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

      then n > 1 by A2, XXREAL_0: 1;

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

      then

      consider p be Element of NAT such that

       A3: p is prime and

       A4: p divides n by INT_2: 31;

      p > 1 by A3;

      then (p |-count n) <> 0 by A4, Th27;

      then (( pfexp n) . p) <> 0 by A3, Def8;

      hence contradiction by A1, PRE_POLY:def 7;

    end;

    theorem :: NAT_3:53

    for m,n be non zero Nat holds ( pfexp (n gcd m)) = ( min (( pfexp n),( pfexp m)))

    proof

      let m,n be non zero Nat;

      now

        set rhs = ( min (( pfexp n),( pfexp m)));

        set lhs = ( pfexp (n gcd m));

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider j = i as prime Element of NAT by NEWTON:def 6;

        set x = (j |-count n), y = (j |-count m), z = (j |-count (n gcd m));

        

         A1: (lhs . j) = z by Def8;

        

         A2: j <> 1 by INT_2:def 4;

        then

         A3: (j |^ x) divides n by Def7;

        

         A4: (n gcd m) <> 0 by INT_2: 5;

        then

         A5: (j |^ z) divides (n gcd m) by A2, Def7;

        

         A6: not (j |^ (z + 1)) divides (n gcd m) by A2, A4, Def7;

        

         A7: not (j |^ (y + 1)) divides m by A2, Def7;

        

         A8: (j |^ y) divides m by A2, Def7;

        (n gcd m) divides m by NAT_D:def 5;

        then

         A9: (j |^ z) divides m by A5, NAT_D: 4;

        

         A10: (( pfexp n) . j) = x by Def8;

        (n gcd m) divides n by NAT_D:def 5;

        then

         A11: (j |^ z) divides n by A5, NAT_D: 4;

        

         A12: (( pfexp m) . j) = y by Def8;

        

         A13: not (j |^ (x + 1)) divides n by A2, Def7;

        thus (lhs . i) = (rhs . i)

        proof

          per cases ;

            suppose

             A14: (( pfexp n) . j) <= (( pfexp m) . j);

             A15:

            now

              assume

               A16: z < x;

              then z < y by A10, A12, A14, XXREAL_0: 2;

              then

               A17: (j |^ (z + 1)) divides m by A8, Th4;

              (j |^ (z + 1)) divides n by A3, A16, Th4;

              hence contradiction by A6, A17, NAT_D:def 5;

            end;

            

             A18: z <= x by A13, A11, Th4;

            (rhs . j) = x by A10, A14, Def3;

            hence thesis by A1, A18, A15, XXREAL_0: 1;

          end;

            suppose

             A19: (( pfexp n) . j) > (( pfexp m) . j);

             A20:

            now

              assume

               A21: z < y;

              then z < x by A10, A12, A19, XXREAL_0: 2;

              then

               A22: (j |^ (z + 1)) divides n by A3, Th4;

              (j |^ (z + 1)) divides m by A8, A21, Th4;

              hence contradiction by A6, A22, NAT_D:def 5;

            end;

            

             A23: z <= y by A7, A9, Th4;

            (rhs . j) = y by A12, A19, Def3;

            hence thesis by A1, A23, A20, XXREAL_0: 1;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAT_3:54

    for m,n be non zero Nat holds ( pfexp (n lcm m)) = ( max (( pfexp n),( pfexp m)))

    proof

      let m,n be non zero Nat;

      now

        set rhs = ( max (( pfexp n),( pfexp m)));

        set lhs = ( pfexp (n lcm m));

        let i be object;

        

         A1: m divides (n lcm m) by NAT_D:def 4;

        assume i in SetPrimes ;

        then

        reconsider j = i as prime Element of NAT by NEWTON:def 6;

        set x = (j |-count n), y = (j |-count m), z = (j |-count (n lcm m));

        

         A2: (lhs . j) = z by Def8;

        

         A3: (( pfexp n) . j) = x by Def8;

        

         A4: j > 1 by INT_2:def 4;

        then

         A5: not (j |^ (x + 1)) divides n by Def7;

        

         A6: (n lcm m) <> 0 by INT_2: 4;

        then

         A7: (j |^ z) divides (n lcm m) by A4, Def7;

        

         A8: not (j |^ (z + 1)) divides (n lcm m) by A4, A6, Def7;

        

         A9: (( pfexp m) . j) = y by Def8;

        

         A10: n divides (n lcm m) by NAT_D:def 4;

        

         A11: (j |^ x) divides n by A4, Def7;

        then

         A12: (j |^ x) divides (n lcm m) by A10, NAT_D: 4;

        

         A13: not (j |^ (y + 1)) divides m by A4, Def7;

        

         A14: (j |^ y) divides m by A4, Def7;

        then

         A15: (j |^ y) divides (n lcm m) by A1, NAT_D: 4;

        thus (lhs . i) = (rhs . i)

        proof

          per cases ;

            suppose

             A16: (( pfexp n) . j) <= (( pfexp m) . j);

             A17:

            now

              consider p be Nat such that

               A18: y = (x + p) by A3, A9, A16, NAT_1: 10;

              consider t be Nat such that

               A19: n = ((j |^ x) * t) by A11;

               A20:

              now

                assume j divides t;

                then

                consider w be Nat such that

                 A21: t = (j * w);

                n = (((j |^ x) * j) * w) by A19, A21

                .= ((j |^ (x + 1)) * w) by NEWTON: 6;

                hence contradiction by A5;

              end;

              consider u be Nat such that

               A22: (n lcm m) = (n * u) by A10;

              assume y < z;

              then (j |^ (y + 1)) divides (n lcm m) by A7, Th4;

              then

              consider k be Nat such that

               A23: (n lcm m) = ((j |^ (y + 1)) * k);

              

               A24: (n lcm m) = (((j |^ y) * j) * k) by A23, NEWTON: 6

              .= ((j |^ y) * (k * j));

              ((j |^ x) * ((j |^ p) * (k * j))) = (((j |^ x) * (j |^ p)) * (k * j))

              .= ((j |^ x) * (t * u)) by A24, A19, A22, A18, NEWTON: 8;

              then (((j |^ p) * k) * j) = (t * u) by XCMPLX_1: 5;

              then j divides (t * u);

              then j divides u by A20, NEWTON: 80;

              then

              consider w be Nat such that

               A25: u = (j * w);

              (((j |^ y) * k) * j) = ((n * w) * j) by A24, A22, A25;

              then ((j |^ y) * k) = (n * w) by XCMPLX_1: 5;

              then

               A26: n divides ((j |^ y) * k);

              consider t be Nat such that

               A27: m = ((j |^ y) * t) by A14;

               A28:

              now

                assume j divides t;

                then

                consider w be Nat such that

                 A29: t = (j * w);

                m = (((j |^ y) * j) * w) by A27, A29

                .= ((j |^ (y + 1)) * w) by NEWTON: 6;

                hence contradiction by A13;

              end;

              consider u be Nat such that

               A30: (n lcm m) = (m * u) by A1;

              ((j |^ y) * (k * j)) = ((j |^ y) * (t * u)) by A24, A27, A30;

              then (k * j) = (t * u) by XCMPLX_1: 5;

              then j divides (t * u);

              then j divides u by A28, NEWTON: 80;

              then

              consider w be Nat such that

               A31: u = (j * w);

              (((j |^ y) * k) * j) = ((m * w) * j) by A24, A30, A31;

              then ((j |^ y) * k) = (m * w) by XCMPLX_1: 5;

              then m divides ((j |^ y) * k);

              then

               A32: (n lcm m) divides ((j |^ y) * k) by A26, NAT_D:def 4;

               0 <> k by A23, INT_2: 4;

              then (j |^ (y + 1)) <= (j |^ y) by A23, A32, NAT_D: 7, XREAL_1: 68;

              then ((j |^ y) * j) <= ((j |^ y) * 1) by NEWTON: 6;

              then j <= 1 by XREAL_1: 68;

              hence contradiction by INT_2:def 4;

            end;

            

             A33: y <= z by A8, A15, Th4;

            (rhs . j) = y by A9, A16, Def4;

            hence thesis by A2, A33, A17, XXREAL_0: 1;

          end;

            suppose

             A34: (( pfexp n) . j) > (( pfexp m) . j);

             A35:

            now

              consider p be Nat such that

               A36: x = (y + p) by A3, A9, A34, NAT_1: 10;

              consider t be Nat such that

               A37: m = ((j |^ y) * t) by A14;

               A38:

              now

                assume j divides t;

                then

                consider w be Nat such that

                 A39: t = (j * w);

                m = (((j |^ y) * j) * w) by A37, A39

                .= ((j |^ (y + 1)) * w) by NEWTON: 6;

                hence contradiction by A13;

              end;

              consider u be Nat such that

               A40: (n lcm m) = (m * u) by A1;

              assume x < z;

              then (j |^ (x + 1)) divides (n lcm m) by A7, Th4;

              then

              consider k be Nat such that

               A41: (n lcm m) = ((j |^ (x + 1)) * k);

              

               A42: (n lcm m) = (((j |^ x) * j) * k) by A41, NEWTON: 6

              .= ((j |^ x) * (k * j));

              ((j |^ y) * ((j |^ p) * (k * j))) = (((j |^ y) * (j |^ p)) * (k * j))

              .= ((j |^ y) * (t * u)) by A42, A37, A40, A36, NEWTON: 8;

              then (t * u) = (((j |^ p) * k) * j) by XCMPLX_1: 5;

              then j divides (t * u);

              then j divides u by A38, NEWTON: 80;

              then

              consider w be Nat such that

               A43: u = (j * w);

              (((j |^ x) * k) * j) = ((m * w) * j) by A42, A40, A43;

              then ((j |^ x) * k) = (m * w) by XCMPLX_1: 5;

              then

               A44: m divides ((j |^ x) * k);

              consider t be Nat such that

               A45: n = ((j |^ x) * t) by A11;

               A46:

              now

                assume j divides t;

                then

                consider w be Nat such that

                 A47: t = (j * w);

                n = (((j |^ x) * j) * w) by A45, A47

                .= ((j |^ (x + 1)) * w) by NEWTON: 6;

                hence contradiction by A5;

              end;

              consider u be Nat such that

               A48: (n lcm m) = (n * u) by A10;

              ((j |^ x) * (k * j)) = ((j |^ x) * (t * u)) by A42, A45, A48;

              then (k * j) = (t * u) by XCMPLX_1: 5;

              then j divides (t * u);

              then j divides u by A46, NEWTON: 80;

              then

              consider w be Nat such that

               A49: u = (j * w);

              (((j |^ x) * k) * j) = ((n * w) * j) by A42, A48, A49;

              then ((j |^ x) * k) = (n * w) by XCMPLX_1: 5;

              then n divides ((j |^ x) * k);

              then

               A50: (n lcm m) divides ((j |^ x) * k) by A44, NAT_D:def 4;

               0 <> k by A41, INT_2: 4;

              then (j |^ (x + 1)) <= (j |^ x) by A41, A50, NAT_D: 7, XREAL_1: 68;

              then ((j |^ x) * j) <= ((j |^ x) * 1) by NEWTON: 6;

              then j <= 1 by XREAL_1: 68;

              hence contradiction by INT_2:def 4;

            end;

            

             A51: x <= z by A8, A12, Th4;

            (rhs . j) = x by A3, A34, Def4;

            hence thesis by A2, A51, A35, XXREAL_0: 1;

          end;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let n be non zero Nat;

      :: NAT_3:def9

      func prime_factorization n -> ManySortedSet of SetPrimes means

      : Def9: ( support it ) = ( support ( pfexp n)) & for p be Nat st p in ( support ( pfexp n)) holds (it . p) = (p |^ (p |-count n));

      existence

      proof

        defpred P[ object, object] means for p be Prime st $1 = p holds (p in ( support ( pfexp n)) implies $2 = (p |^ (p |-count n))) & ( not p in ( support ( pfexp n)) implies $2 = 0 );

        

         A1: for x be object st x in SetPrimes holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in SetPrimes ;

          then

          reconsider i = x as prime Element of NAT by NEWTON:def 6;

          per cases ;

            suppose

             A2: i in ( support ( pfexp n));

            take (i |^ (i |-count n));

            let p be Prime;

            assume p = x;

            hence thesis by A2;

          end;

            suppose

             A3: not i in ( support ( pfexp n));

            take 0 ;

            let p be Prime;

            assume p = x;

            hence thesis by A3;

          end;

        end;

        consider f be Function such that

         A4: ( dom f) = SetPrimes and

         A5: for x be object st x in SetPrimes holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A6: ( support f) c= SetPrimes by A4, PRE_POLY: 37;

         A7:

        now

          let x be object;

          hereby

            assume

             A8: x in ( support f);

            then x in SetPrimes by A6;

            then

            reconsider i = x as prime Element of NAT by NEWTON:def 6;

            assume not x in ( support ( pfexp n));

            then (f . i) = 0 by A5, A6, A8;

            hence contradiction by A8, PRE_POLY:def 7;

          end;

          assume

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

          then x in SetPrimes ;

          then

          reconsider i = x as prime Element of NAT by NEWTON:def 6;

          (f . i) = (i |^ (i |-count n)) by A5, A9;

          hence x in ( support f) by PRE_POLY:def 7;

        end;

        reconsider f as ManySortedSet of SetPrimes by A4, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        thus ( support f) = ( support ( pfexp n)) by A7, TARSKI: 2;

        let p be Nat;

        assume

         A10: p in ( support ( pfexp n));

        then p is Prime by Th34;

        hence thesis by A5, A10;

      end;

      uniqueness

      proof

        let it1,it2 be ManySortedSet of SetPrimes such that

         A11: ( support it1) = ( support ( pfexp n)) and

         A12: for p be Nat st p in ( support ( pfexp n)) holds (it1 . p) = (p |^ (p |-count n)) and

         A13: ( support it2) = ( support ( pfexp n)) and

         A14: for p be Nat st p in ( support ( pfexp n)) holds (it2 . p) = (p |^ (p |-count n));

        now

          let i be object;

          assume i in SetPrimes ;

          then

          reconsider p = i as prime Element of NAT by NEWTON:def 6;

          per cases ;

            suppose

             A15: p in ( support ( pfexp n));

            

            hence (it1 . i) = (p |^ (p |-count n)) by A12

            .= (it2 . i) by A14, A15;

          end;

            suppose

             A16: not p in ( support ( pfexp n));

            

            hence (it1 . i) = 0 by A11, PRE_POLY:def 7

            .= (it2 . i) by A13, A16, PRE_POLY:def 7;

          end;

        end;

        hence it1 = it2;

      end;

    end

    notation

      let n be non zero Nat;

      synonym ppf n for prime_factorization n;

    end

    registration

      let n be non zero Nat;

      cluster ( ppf n) -> natural-valued finite-support;

      coherence

      proof

        ( rng ( ppf n)) c= NAT

        proof

          let y be object;

          assume y in ( rng ( ppf n));

          then

          consider x be object such that

           A1: x in ( dom ( ppf n)) and

           A2: (( ppf n) . x) = y by FUNCT_1:def 3;

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

          then

          reconsider x as prime Element of NAT by A1, NEWTON:def 6;

          per cases ;

            suppose x in ( support ( pfexp n));

            then (( ppf n) . x) = (x |^ (x |-count n)) by Def9;

            hence thesis by A2;

          end;

            suppose not x in ( support ( pfexp n));

            then not x in ( support ( ppf n)) by Def9;

            then (( ppf n) . x) = 0 by PRE_POLY:def 7;

            hence thesis by A2;

          end;

        end;

        hence ( ppf n) is natural-valued;

        ( support ( ppf n)) = ( support ( pfexp n)) by Def9;

        hence ( support ( ppf n)) is finite;

      end;

    end

    theorem :: NAT_3:55

    

     Th55: (p |-count n) = 0 implies (( ppf n) . p) = 0

    proof

      assume (p |-count n) = 0 ;

      then (( pfexp n) . p) = 0 by Def8;

      then not p in ( support ( pfexp n)) by PRE_POLY:def 7;

      then not p in ( support ( ppf n)) by Def9;

      hence thesis by PRE_POLY:def 7;

    end;

    theorem :: NAT_3:56

    

     Th56: (p |-count n) <> 0 implies (( ppf n) . p) = (p |^ (p |-count n))

    proof

      assume (p |-count n) <> 0 ;

      then (( pfexp n) . p) <> 0 by Def8;

      then p in ( support ( pfexp n)) by PRE_POLY:def 7;

      hence thesis by Def9;

    end;

    theorem :: NAT_3:57

    ( support ( ppf n)) = {} implies n = 1

    proof

      assume ( support ( ppf n)) = {} ;

      then ( support ( pfexp n)) = {} by Def9;

      hence thesis by Th52;

    end;

    theorem :: NAT_3:58

    

     Th58: for a,b be non zero Nat st (a,b) are_coprime holds ( ppf (a * b)) = (( ppf a) + ( ppf b))

    proof

      let a,b be non zero Nat such that

       A1: (a,b) are_coprime ;

      reconsider an = a, bn = b as non zero Nat;

      now

        

         A2: (a gcd b) = 1 by A1;

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider p = i as prime Element of NAT by NEWTON:def 6;

        

         A3: p > 1 by INT_2:def 4;

        

         A4: (p |-count (an * bn)) = ((p |-count a) + (p |-count b)) by Th28;

        per cases ;

          suppose

           A5: (p |-count (a * b)) = 0 ;

          then

           A6: (p |-count b) = 0 by A4;

          

           A7: (p |-count a) = 0 by A4, A5;

          

          thus (( ppf (a * b)) . i) = 0 by A5, Th55

          .= ( 0 + (( ppf b) . i)) by A6, Th55

          .= ((( ppf a) . i) + (( ppf b) . i)) by A7, Th55

          .= ((( ppf a) + ( ppf b)) . i) by PRE_POLY:def 5;

        end;

          suppose

           A8: (p |-count (a * b)) <> 0 ;

          thus (( ppf (a * b)) . i) = ((( ppf a) + ( ppf b)) . i)

          proof

            per cases by A4, A8;

              suppose

               A9: (p |-count a) <> 0 ;

               A10:

              now

                consider ka be Nat such that

                 A11: (p |-count a) = (ka + 1) by A9, NAT_1: 6;

                (p |^ (p |-count a)) divides a by A3, Def7;

                then (p * (p |^ ka)) divides a by A11, NEWTON: 6;

                then

                consider la be Nat such that

                 A12: a = ((p * (p |^ ka)) * la);

                a = (p * ((p |^ ka) * la)) by A12;

                then

                 A13: p divides a;

                assume (p |-count b) <> 0 ;

                then

                consider kb be Nat such that

                 A14: (p |-count b) = (kb + 1) by NAT_1: 6;

                (p |^ (p |-count b)) divides b by A3, Def7;

                then (p * (p |^ kb)) divides b by A14, NEWTON: 6;

                then

                consider lb be Nat such that

                 A15: b = ((p * (p |^ kb)) * lb);

                b = (p * ((p |^ kb) * lb)) by A15;

                then p divides b;

                then p divides 1 by A2, A13, NAT_D:def 5;

                hence contradiction by A3, NAT_D: 7;

              end;

              

              hence (( ppf (a * b)) . i) = (p |^ (p |-count a)) by A4, A8, Th56

              .= ((( ppf a) . p) + 0 ) by A9, Th56

              .= ((( ppf a) . p) + (( ppf b) . p)) by A10, Th55

              .= ((( ppf a) + ( ppf b)) . i) by PRE_POLY:def 5;

            end;

              suppose

               A16: (p |-count b) <> 0 ;

               A17:

              now

                assume (p |-count a) <> 0 ;

                then

                consider ka be Nat such that

                 A18: (p |-count a) = (ka + 1) by NAT_1: 6;

                (p |^ (p |-count a)) divides a by A3, Def7;

                then (p * (p |^ ka)) divides a by A18, NEWTON: 6;

                then

                consider la be Nat such that

                 A19: a = ((p * (p |^ ka)) * la);

                a = (p * ((p |^ ka) * la)) by A19;

                then

                 A20: p divides a;

                consider kb be Nat such that

                 A21: (p |-count b) = (kb + 1) by A16, NAT_1: 6;

                (p |^ (p |-count b)) divides b by A3, Def7;

                then (p * (p |^ kb)) divides b by A21, NEWTON: 6;

                then

                consider lb be Nat such that

                 A22: b = ((p * (p |^ kb)) * lb);

                b = (p * ((p |^ kb) * lb)) by A22;

                then p divides b;

                then p divides 1 by A2, A20, NAT_D:def 5;

                hence contradiction by A3, NAT_D: 7;

              end;

              

              hence (( ppf (a * b)) . i) = (p |^ (p |-count b)) by A4, A8, Th56

              .= ( 0 + (( ppf b) . p)) by A16, Th56

              .= ((( ppf a) . p) + (( ppf b) . p)) by A17, Th55

              .= ((( ppf a) + ( ppf b)) . i) by PRE_POLY:def 5;

            end;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAT_3:59

    

     Th59: (( ppf (p |^ n)) . p) = (p |^ n)

    proof

      p > 1 by INT_2:def 4;

      then (p |-count (p |^ n)) = n by Th25;

      hence thesis by Th56;

    end;

    theorem :: NAT_3:60

    ( ppf (n |^ m)) = (( ppf n) |^ m)

    proof

      now

        let i be object;

        

         A1: m >= ( 0 + 1) by NAT_1: 13;

        

         A2: ((( ppf n) |^ m) . i) = ((( ppf n) . i) |^ m) by Def6;

        assume i in SetPrimes ;

        then

        reconsider p = i as prime Element of NAT by NEWTON:def 6;

        

         A3: (p |-count (n |^ m)) = (m * (p |-count n)) by Th32;

        per cases ;

          suppose

           A4: (p |-count n) = 0 ;

          

          hence (( ppf (n |^ m)) . i) = 0 by A3, Th55

          .= ( 0 qua Nat |^ m) by A1, NEWTON: 11

          .= ((( ppf n) |^ m) . i) by A2, A4, Th55;

        end;

          suppose

           A5: (p |-count n) <> 0 ;

          

          hence (( ppf (n |^ m)) . i) = (p |^ (p |-count (n |^ m))) by A3, Th56

          .= ((p |^ (p |-count n)) |^ m) by A3, NEWTON: 9

          .= ((( ppf n) |^ m) . i) by A2, A5, Th56;

        end;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: NAT_3:61

    ( Product ( ppf n)) = n

    proof

      defpred P[ Nat] means for n be non zero Nat st ( support ( ppf n)) c= ( Seg $1) holds ( Product ( ppf n)) = n;

      

       A1: ( support ( ppf n)) = ( support ( pfexp n)) by Def9;

      

       A2: P[ 0 ]

      proof

        let n be non zero Nat;

        

         A3: {} c= ( support ( ppf n));

        assume ( support ( ppf n)) c= ( Seg 0 );

        then

         A4: ( support ( ppf n)) = {} by A3;

         A5:

        now

          reconsider k = n as Nat;

          assume n <> 1;

          then k > 1 by NAT_1: 53;

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

          then ex p be Element of NAT st p is prime & p divides k by INT_2: 31;

          then ( support ( pfexp n)) is non empty by Th37;

          hence contradiction by A4, Def9;

        end;

        ( ppf n) = ( EmptyBag SetPrimes ) by A4, PRE_POLY: 81;

        hence thesis by A5, Th20;

      end;

      

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

      proof

        let k be Nat;

        assume

         A7: P[k];

        let n be non zero Nat such that

         A8: ( support ( ppf n)) c= ( Seg (k + 1));

        

         A9: ( support ( ppf n)) = ( support ( pfexp n)) by Def9;

        per cases ;

          suppose

           A10: not ( support ( ppf n)) c= ( Seg k);

          set p = (k + 1);

          set e = (p |-count n);

          set s = (p |^ e);

           A11:

          now

            assume

             A12: not (k + 1) in ( support ( ppf n));

            ( support ( ppf n)) c= ( Seg k)

            proof

              let x be object;

              assume

               A13: x in ( support ( ppf n));

              then

              reconsider m = x as Nat;

              m <= (k + 1) by A8, A13, FINSEQ_1: 1;

              then m < (k + 1) by A12, A13, XXREAL_0: 1;

              then

               A14: m <= k by NAT_1: 13;

              x is Prime by A9, A13, Th34;

              then 1 <= m by INT_2:def 4;

              hence thesis by A14;

            end;

            hence contradiction by A10;

          end;

          then

           A15: p is Prime by A9, Th34;

          then

           A16: p > 1 by INT_2:def 4;

          then s divides n by Def7;

          then

          consider t be Nat such that

           A17: n = (s * t);

          reconsider s, t as non zero Nat by A17;

          

           A18: ( dom ( ppf s)) = SetPrimes by PARTFUN1:def 2;

          (( pfexp n) . p) = e by A15, Def8;

          then

           A19: e <> 0 by A9, A11, PRE_POLY:def 7;

          reconsider s1 = s, t1 = t as non zero Nat;

          

           A20: ( support ( ppf t)) = ( support ( pfexp t)) by Def9;

          

           A21: ( support ( ppf t)) c= ( Seg k)

          proof

            set f = (p |-count t);

            let x be object;

            assume

             A22: x in ( support ( ppf t));

            then

            reconsider m = x as Nat;

            

             A23: x in ( support ( pfexp t)) by A22, Def9;

             A24:

            now

              assume

               A25: m = p;

              (( pfexp t) . p) = f by A15, Def8;

              then f <> 0 by A23, A25, PRE_POLY:def 7;

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

              then

              consider g be Nat such that

               A26: f = (1 + g) by NAT_1: 10;

              (p |^ f) divides t by A16, Def7;

              then

              consider u be Nat such that

               A27: t = ((p |^ f) * u);

              n = (s * (((p |^ g) * p) * u)) by A17, A26, A27, NEWTON: 6

              .= ((s * p) * ((p |^ g) * u))

              .= ((p |^ (e + 1)) * ((p |^ g) * u)) by NEWTON: 6;

              then (p |^ (e + 1)) divides n;

              hence contradiction by A16, Def7;

            end;

            ( support ( ppf t)) c= ( support ( ppf n)) by A9, A17, A20, Th45;

            then m in ( support ( ppf n)) by A22;

            then m <= (k + 1) by A8, FINSEQ_1: 1;

            then m < p by A24, XXREAL_0: 1;

            then

             A28: m <= k by NAT_1: 13;

            x is Prime by A23, Th34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A28;

          end;

          (s1,t1) are_coprime

          proof

            set u = (s1 gcd t1);

            

             A29: u divides t1 by NAT_D:def 5;

            u <> 0 by INT_2: 5;

            then

             A30: ( 0 + 1) <= u by NAT_1: 13;

            assume (s1 gcd t1) <> 1;

            then u > 1 by A30, XXREAL_0: 1;

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

            then

            consider r be Element of NAT such that

             A31: r is prime and

             A32: r divides u by INT_2: 31;

            u divides s1 by NAT_D:def 5;

            then r divides s1 by A32, NAT_D: 4;

            then r divides p by A31, Th5;

            then r = 1 or r = p by A15, INT_2:def 4;

            then p divides t1 by A31, A32, A29, NAT_D: 4;

            then p in ( support ( pfexp t)) by A15, Th37;

            then (k + 1) <= k by A20, A21, FINSEQ_1: 1;

            hence contradiction by NAT_1: 13;

          end;

          then

           A33: ( ppf n) = (( ppf s) + ( ppf t)) by A17, Th58;

          consider f be FinSequence of COMPLEX such that

           A34: ( Product ( ppf s)) = ( Product f) and

           A35: f = (( ppf s) * ( canFS ( support ( ppf s)))) by Def5;

          ( support ( ppf s)) = ( support ( pfexp s)) by Def9;

          then

           A36: ( support ( ppf s)) = {p} by A15, A19, Th42;

          

          then f = (( ppf s) * <*p*>) by A35, FINSEQ_1: 94

          .= <*(( ppf s) . p)*> by A11, A18, FINSEQ_2: 34;

          

          then

           A37: ( Product ( ppf s)) = (( ppf s) . p) by A34

          .= s by A15, A19, Th59;

          now

            assume (( support ( ppf s)) /\ ( support ( ppf t))) <> {} ;

            then

            consider x be object such that

             A38: x in (( support ( ppf s)) /\ ( support ( ppf t))) by XBOOLE_0:def 1;

            x in ( support ( ppf s)) by A38, XBOOLE_0:def 4;

            then

             A39: x = p by A36, TARSKI:def 1;

            x in ( support ( ppf t)) by A38, XBOOLE_0:def 4;

            then p <= k by A21, A39, FINSEQ_1: 1;

            hence contradiction by NAT_1: 13;

          end;

          then

           A40: ( support ( ppf s)) misses ( support ( ppf t));

          ( Product ( ppf t)) = t by A7, A21;

          hence thesis by A17, A40, A33, A37, Th19;

        end;

          suppose ( support ( ppf n)) c= ( Seg k);

          hence thesis by A7;

        end;

      end;

      

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

      per cases ;

        suppose ( support ( ppf n)) is empty;

        hence thesis by A2;

      end;

        suppose ( support ( ppf n)) is non empty;

        then

        reconsider S = ( support ( ppf n)) as finite non empty Subset of NAT by XBOOLE_1: 1;

        

         A42: ( max S) is Nat by TARSKI: 1;

        ( support ( ppf n)) c= ( Seg ( max S))

        proof

          let x be object;

          assume

           A43: x in ( support ( ppf n));

          then

          reconsider m = x as Nat;

          x is Prime by A1, A43, Th34;

          then

           A44: 1 <= m by INT_2:def 4;

          m <= ( max S) by A43, XXREAL_2:def 8;

          hence thesis by A44;

        end;

        hence thesis by A42, A41;

      end;

    end;