nat_5.miz



    begin

    reserve k,n,m,l,p for Nat;

    reserve n0,m0 for non zero Nat;

    

     Lm1: p is prime implies (p |-count (n0 gcd m0)) = ( min ((p |-count n0),(p |-count m0)))

    proof

      reconsider h9 = (n0 gcd m0) as non zero Nat by INT_2: 5;

      assume

       A1: p is prime;

      then

      reconsider p9 = p as Prime;

      h9 divides n0 by INT_2:def 2;

      then

       A2: (p9 |-count h9) <= (p9 |-count n0) by NAT_3: 30;

      h9 divides m0 by INT_2:def 2;

      then

       A3: (p9 |-count h9) <= (p9 |-count m0) by NAT_3: 30;

      per cases ;

        suppose

         A4: (p |-count n0) <= (p |-count m0);

        set k = (p9 |^ (p9 |-count n0));

        

         A5: (p9 |^ (p |-count n0)) divides m0 by A4, MOEBIUS1: 9;

        

         A6: p > 1 by A1, INT_2:def 4;

        then k divides n0 by NAT_3:def 7;

        then k divides h9 by A5, INT_2:def 2;

        then (p9 |-count k) <= (p9 |-count h9) by NAT_3: 30;

        then (p9 |-count n0) <= (p9 |-count h9) by A6, NAT_3: 25;

        then (p |-count (n0 gcd m0)) = (p |-count n0) by A2, XXREAL_0: 1;

        hence thesis by A4, XXREAL_0:def 9;

      end;

        suppose

         A7: not (p |-count n0) <= (p |-count m0);

        set k = (p9 |^ (p9 |-count m0));

        

         A8: (p9 |^ (p |-count m0)) divides n0 by A7, MOEBIUS1: 9;

        

         A9: p > 1 by A1, INT_2:def 4;

        then k divides m0 by NAT_3:def 7;

        then k divides h9 by A8, INT_2:def 2;

        then (p9 |-count k) <= (p9 |-count h9) by NAT_3: 30;

        then (p9 |-count m0) <= (p9 |-count h9) by A9, NAT_3: 25;

        then (p |-count (n0 gcd m0)) = (p |-count m0) by A3, XXREAL_0: 1;

        hence thesis by A7, XXREAL_0:def 9;

      end;

    end;

    theorem :: NAT_5:1

    

     Th1: (2 |^ (n + 1)) < ((2 |^ (n + 2)) - 1)

    proof

      defpred P[ Nat] means (2 |^ ($1 + 1)) < ((2 |^ ($1 + 2)) - 1);

      

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

      proof

        let k be Nat;

        assume P[k];

        then ((2 |^ (k + 1)) * 2) < (((2 |^ (k + 2)) - 1) * 2) by XREAL_1: 68;

        then (2 |^ ((k + 1) + 1)) < (((2 |^ (k + 2)) * 2) - (1 * 2)) by NEWTON: 6;

        then

         A2: (2 |^ ((k + 1) + 1)) < ((2 |^ ((k + 2) + 1)) - 2) by NEWTON: 6;

        (( - 2) + (2 |^ ((k + 1) + 2))) < (( - 1) + (2 |^ ((k + 1) + 2))) by XREAL_1: 8;

        hence P[(k + 1)] by A2, XXREAL_0: 2;

      end;

      (2 |^ 1) < (((2 |^ 1) * 2) - 1);

      then (2 |^ 1) < ((2 |^ (1 + 1)) - 1) by NEWTON: 6;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: NAT_5:2

    

     Th2: n0 is even implies ex k, m st m is odd & k > 0 & n0 = ((2 |^ k) * m)

    proof

      assume

       A1: n0 is even;

      set k = (2 |-count n0);

      (2 |^ k) divides n0 by NAT_3:def 7;

      then

      consider m be Nat such that

       A2: n0 = ((2 |^ k) * m) by NAT_D:def 3;

      take k, m;

       A3:

      now

        reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

        assume not m is odd;

        then

        consider m99 be Nat such that

         A4: m9 = (2 * m99) by ABIAN:def 2;

        n0 = (((2 |^ k) * 2) * m99) by A2, A4

        .= ((2 |^ (k + 1)) * m99) by NEWTON: 6;

        then (2 |^ (k + 1)) divides n0 by NAT_D:def 3;

        hence contradiction by NAT_3:def 7;

      end;

      hence m is odd;

      now

        assume k = 0 ;

        then n0 = (1 * m) by A2, NEWTON: 4;

        hence contradiction by A1, A3;

      end;

      hence k > 0 ;

      thus n0 = ((2 |^ k) * m) by A2;

    end;

    theorem :: NAT_5:3

    

     Th3: n = (2 |^ k) & m is odd implies (n,m) are_coprime

    proof

      assume

       A1: n = (2 |^ k);

      assume

       A2: m is odd;

      then

      reconsider h = (n gcd m) as non zero Nat by INT_2: 5;

      for p be Element of NAT st p is prime holds (p |-count h) = (p |-count 1)

      proof

        reconsider n9 = n, m9 = m as non zero Nat by A1, A2;

        let p be Element of NAT ;

        assume

         A3: p is prime;

        

         A4: ( min ((p |-count n),(p |-count m))) = 0

        proof

          per cases ;

            suppose

             A5: p = 2;

             not p divides m

            proof

              assume p divides m;

              then

              consider m9 be Nat such that

               A6: m = (p * m9) by NAT_D:def 3;

              thus contradiction by A2, A5, A6;

            end;

            then (p |-count m) = 0 by A5, NAT_3: 27;

            hence thesis by XXREAL_0:def 9;

          end;

            suppose

             A7: p <> 2;

            p <> 1 by A3, INT_2:def 4;

            then

             A8: (p |-count 2) = 0 by A7, INT_2: 28, NAT_3: 24;

            (p |-count n) = (k * (p |-count 2)) by A1, A3, NAT_3: 32

            .= (k * 0 qua Nat) by A8;

            hence thesis by XXREAL_0:def 9;

          end;

        end;

        p > 1 & (p |-count (n9 gcd m9)) = ( min ((p |-count n9),(p |-count m9))) by A3, Lm1, INT_2:def 4;

        hence (p |-count h) = (p |-count 1) by A4, NAT_3: 21;

      end;

      then (n gcd m) = 1 by NAT_4: 21;

      hence (n,m) are_coprime by INT_2:def 3;

    end;

    theorem :: NAT_5:4

    

     Th4: {n} is finite Subset of NAT by ORDINAL1:def 12, ZFMISC_1: 31;

    theorem :: NAT_5:5

    

     Th5: {n, m} is finite Subset of NAT

    proof

      n in NAT & m in NAT by ORDINAL1:def 12;

      hence {n, m} is finite Subset of NAT by ZFMISC_1: 32;

    end;

    

     Lm2: {n, m, l} is finite Subset of NAT

    proof

      reconsider Y = {m, l} as finite Subset of NAT by Th5;

      reconsider X = {n} as finite Subset of NAT by Th4;

       {n, m, l} = (X \/ Y) by ENUMSET1: 2;

      hence {n, m, l} is finite Subset of NAT ;

    end;

    

     Lm3: {n, m, l, k} is finite Subset of NAT

    proof

      reconsider Y = {l, k} as finite Subset of NAT by Th5;

      reconsider X = {n, m} as finite Subset of NAT by Th5;

       {n, m, l, k} = (X \/ Y) by ENUMSET1: 5;

      hence {n, m, l, k} is finite Subset of NAT ;

    end;

    reserve f for FinSequence;

    reserve x,X,Y for set;

    theorem :: NAT_5:6

    

     Th6: f is one-to-one implies ( Del (f,n)) is one-to-one

    proof

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

      then

       A1: ( Sgm (( dom f) \ {n})) is one-to-one by FINSEQ_3: 92, XBOOLE_1: 36;

      assume f is one-to-one;

      hence ( Del (f,n)) is one-to-one by A1;

    end;

    theorem :: NAT_5:7

    

     Th7: f is one-to-one & n in ( dom f) implies not (f . n) in ( rng ( Del (f,n)))

    proof

      assume

       A1: f is one-to-one;

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

      

       A2: ( dom ( Del (f,n9))) c= ( dom f) by WSIERP_1: 39;

      assume

       A3: n in ( dom f);

      then

      consider m be Nat such that

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

       A5: ( len ( Del (f,n))) = m by FINSEQ_3: 104;

      assume (f . n) in ( rng ( Del (f,n)));

      then

      consider j be object such that

       A6: j in ( dom ( Del (f,n))) and

       A7: (f . n) = (( Del (f,n)) . j) by FUNCT_1:def 3;

      

       A8: j in ( Seg m) by A5, A6, FINSEQ_1:def 3;

      reconsider j as Element of NAT by A6;

      per cases ;

        suppose

         A9: j < n9;

        then (f . n) = (f . j) by A7, FINSEQ_3: 110;

        hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def 4;

      end;

        suppose

         A10: j >= n9;

        

         A11: (j + 1) >= ( 0 + 1) by XREAL_1: 6;

        

         A12: j <= m by A8, FINSEQ_1: 1;

        then (j + 1) <= (m + 1) by XREAL_1: 6;

        then (j + 1) in ( Seg (m + 1)) by A11;

        then

         A13: (j + 1) in ( dom f) by A4, FINSEQ_1:def 3;

        

         A14: (j + 1) <> n by A10, NAT_1: 13;

        (f . n) = (f . (j + 1)) by A3, A4, A7, A10, A12, FINSEQ_3: 111;

        hence contradiction by A1, A3, A13, A14, FUNCT_1:def 4;

      end;

    end;

    theorem :: NAT_5:8

    

     Th8: x in ( rng f) & not x in ( rng ( Del (f,n))) implies x = (f . n)

    proof

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

      assume

       A1: x in ( rng f);

      then

      consider j be object such that

       A2: j in ( dom f) and

       A3: x = (f . j) by FUNCT_1:def 3;

      for X be set st ( card X) = 0 holds X = {} ;

      then

      consider m be Nat such that

       A4: ( len f) = (m + 1) by A1, NAT_1: 6, RELAT_1: 38;

      

       A5: j in ( Seg (m + 1)) by A2, A4, FINSEQ_1:def 3;

      assume

       A6: not x in ( rng ( Del (f,n)));

      then

       A7: n in ( dom f) by A1, FINSEQ_3: 104;

      then

       A8: ( len ( Del (f,n))) = m by A4, FINSEQ_3: 109;

      

       A9: n in ( Seg (m + 1)) by A4, A7, FINSEQ_1:def 3;

      then

       A10: 1 <= n by FINSEQ_1: 1;

      reconsider j as Element of NAT by A2;

      reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

      assume

       A11: not x = (f . n);

      

       A12: n <= (m + 1) by A9, FINSEQ_1: 1;

      per cases ;

        suppose

         A13: j < n9;

        then (( Del (f,n9)) . j) = (f . j) by FINSEQ_3: 110;

        then not j in ( dom ( Del (f,n))) by A3, A6, FUNCT_1:def 3;

        then not j in ( Seg m) by A8, FINSEQ_1:def 3;

        then

         A14: j < 1 or j > m;

        j <= (m + 1) by A5, FINSEQ_1: 1;

        hence contradiction by A5, A12, A13, A14, FINSEQ_1: 1, NAT_1: 8;

      end;

        suppose

         A15: j >= n9;

        set j9 = (j -' 1);

        j <= (m + 1) by A5, FINSEQ_1: 1;

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

        then

         A16: j9 <= m9 by XREAL_0:def 2;

        j > n9 by A3, A11, A15, XXREAL_0: 1;

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

        then

         A17: (j - 1) >= ((n9 + 1) - 1) by XREAL_1: 9;

        then j9 >= n9 by XREAL_0:def 2;

        then j9 >= 1 by A10, XXREAL_0: 2;

        then j9 in ( Seg m) by A16;

        then

         A18: j9 in ( dom ( Del (f,n))) by A8, FINSEQ_1:def 3;

        

         A19: n9 in ( dom f) by A1, A6, FINSEQ_3: 104;

        n9 <= j9 by A17, XREAL_0:def 2;

        then (( Del (f,n9)) . j9) = (f . (j9 + 1)) by A4, A19, A16, FINSEQ_3: 111;

        then (f . j) <> (f . (j9 + 1)) by A3, A6, A18, FUNCT_1:def 3;

        then (f . j) <> (f . ((j - 1) + 1)) by A17, XREAL_0:def 2;

        hence contradiction;

      end;

    end;

    theorem :: NAT_5:9

    

     Th9: for f1 be FinSequence of NAT , f2 be FinSequence of X st ( rng f1) c= ( dom f2) holds (f2 * f1) is FinSequence of X

    proof

      let f1 be FinSequence of NAT ;

      let f2 be FinSequence of X;

      consider n be Nat such that

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

      assume ( rng f1) c= ( dom f2);

      then ( dom (f2 * f1)) = ( Seg n) by A1, RELAT_1: 27;

      then

       A2: (f2 * f1) is FinSequence by FINSEQ_1:def 2;

      ( rng (f2 * f1)) c= X;

      hence (f2 * f1) is FinSequence of X by A2, FINSEQ_1:def 4;

    end;

    reserve f1,f2,f3 for FinSequence of REAL ;

    theorem :: NAT_5:10

    

     Th10: (X \/ Y) = ( dom f1) & X misses Y & f2 = (f1 * ( Sgm X)) & f3 = (f1 * ( Sgm Y)) implies ( Sum f1) = (( Sum f2) + ( Sum f3))

    proof

      assume

       A1: (X \/ Y) = ( dom f1);

      assume

       A2: X misses Y;

      assume

       A3: f2 = (f1 * ( Sgm X));

      assume

       A4: f3 = (f1 * ( Sgm Y));

      per cases ;

        suppose

         A5: ( dom f1) = {} ;

        then Y = {} by A1;

        then

         A6: f3 = {} by A4, FINSEQ_3: 43;

        X = {} by A1, A5;

        then f2 = {} by A3, FINSEQ_3: 43;

        hence thesis by A5, A6, RELAT_1: 41, RVSUM_1: 72;

      end;

        suppose

         A7: ( dom f1) <> {} ;

        

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

        then

        reconsider F = ( id ( dom f1)) as FinSequence by FINSEQ_2: 48;

        reconsider D = ( dom f1) as non empty set by A7;

        reconsider F1 = f1 as FinSequence of ExtREAL by MESFUNC3: 11;

        

         A9: ( dom F1) = ( dom F);

        Y c= ( dom f1) by A1, XBOOLE_1: 7;

        then ( rng ( Sgm Y)) c= ( dom f1) by A8, FINSEQ_1:def 13;

        then

        reconsider sy = ( Sgm Y) as FinSequence of D by FINSEQ_1:def 4;

        (( dom f1) \ X) = Y by A1, A2, XBOOLE_1: 88;

        then (( rng F) \ X) = Y;

        then

         A10: (F " (( rng F) \ X)) = Y by FUNCT_2: 94;

        

         A11: X c= ( dom f1) by A1, XBOOLE_1: 7;

        then ( rng ( Sgm X)) c= ( dom f1) by A8, FINSEQ_1:def 13;

        then

        reconsider sx = ( Sgm X) as FinSequence of D by FINSEQ_1:def 4;

        (F " X) = X by A11, FUNCT_2: 94;

        then

        reconsider s = (( Sgm X) ^ ( Sgm Y)) as Permutation of ( dom F1) by A10, A9, FINSEQ_3: 114;

        ( rng s) c= ( dom f1) by FUNCT_2:def 3;

        then

        reconsider g = (f1 * s) as FinSequence of REAL by Th9;

        reconsider f19 = f1 as Function of D, REAL by FINSEQ_2: 26;

        reconsider G = g as FinSequence of ExtREAL by MESFUNC3: 11;

         not -infty in ( rng F1);

        then ( Sum F1) = ( Sum G) by EXTREAL1: 11;

        then

         A12: ( Sum f1) = ( Sum G) by MESFUNC3: 2;

        g = ((f19 * sx) ^ (f19 * sy)) by FINSEQOP: 9;

        then ( Sum g) = (( Sum (f19 * sx)) + ( Sum (f19 * sy))) by RVSUM_1: 75;

        hence ( Sum f1) = (( Sum f2) + ( Sum f3)) by A3, A4, A12, MESFUNC3: 2;

      end;

    end;

    theorem :: NAT_5:11

    

     Th11: f2 = (f1 * ( Sgm X)) & (( dom f1) \ (f1 " { 0 })) c= X & X c= ( dom f1) implies ( Sum f1) = ( Sum f2)

    proof

      assume

       A1: f2 = (f1 * ( Sgm X));

      set Y = (( dom f1) \ X);

      assume

       A2: (( dom f1) \ (f1 " { 0 })) c= X;

      assume

       A3: X c= ( dom f1);

      per cases ;

        suppose

         A4: Y = {} ;

        (X \ ( dom f1)) = {} by A3, XBOOLE_1: 37;

        then X = ( dom f1) by A4, XBOOLE_1: 32;

        then X = ( Seg ( len f1)) by FINSEQ_1:def 3;

        then ( Sgm X) = ( idseq ( len f1)) by FINSEQ_3: 48;

        hence thesis by A1, FINSEQ_2: 54;

      end;

        suppose

         A5: Y <> {} ;

        set f3 = (f1 * ( Sgm Y));

        

         A6: Y c= ( dom f1) by XBOOLE_1: 36;

        then

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

        then ( rng ( Sgm Y)) c= ( dom f1) by A6, FINSEQ_1:def 13;

        then

        reconsider f3 as FinSequence of REAL by Th9;

        

         A8: X misses Y by XBOOLE_1: 79;

        

         A9: Y c= (f1 " { 0 })

        proof

          assume not Y c= (f1 " { 0 });

          then

          consider x be object such that

           A10: x in Y and

           A11: not x in (f1 " { 0 });

          x in ( dom f1) by A10, XBOOLE_0:def 5;

          then x in (( dom f1) \ (f1 " { 0 })) by A11, XBOOLE_0:def 5;

          then x in (X /\ Y) by A2, A10, XBOOLE_0:def 4;

          hence contradiction by A8, XBOOLE_0:def 7;

        end;

        for y be object holds y in ( rng f3) iff y = 0

        proof

          let y be object;

          consider x be object such that

           A12: x in Y by A5, XBOOLE_0:def 1;

          hereby

            assume y in ( rng f3);

            then

            consider x be object such that

             A13: x in ( dom f3) and

             A14: y = (f3 . x) by FUNCT_1:def 3;

            

             A15: x in ( dom ( Sgm Y)) by A13, FUNCT_1: 11;

            then (( Sgm Y) . x) in ( rng ( Sgm Y)) by FUNCT_1: 3;

            then (( Sgm Y) . x) in Y by A7, FINSEQ_1:def 13;

            then (f1 . (( Sgm Y) . x)) in { 0 } by A9, FUNCT_1:def 7;

            then (f3 . x) in { 0 } by A15, FUNCT_1: 13;

            hence y = 0 by A14, TARSKI:def 1;

          end;

          assume

           A16: y = 0 ;

          x in ( rng ( Sgm Y)) by A7, A12, FINSEQ_1:def 13;

          then

          consider x9 be object such that

           A17: x9 in ( dom ( Sgm Y)) and

           A18: x = (( Sgm Y) . x9) by FUNCT_1:def 3;

          (f1 . x) in { 0 } by A9, A12, FUNCT_1:def 7;

          then (f1 . (( Sgm Y) . x9)) = y by A16, A18, TARSKI:def 1;

          then

           A19: (f3 . x9) = y by A17, FUNCT_1: 13;

          x in ( dom f1) by A9, A12, FUNCT_1:def 7;

          then x9 in ( dom f3) by A17, A18, FUNCT_1: 11;

          hence y in ( rng f3) by A19, FUNCT_1:def 3;

        end;

        then ( dom f3) = ( Seg ( len f3)) & ( rng f3) = { 0 } by FINSEQ_1:def 3, TARSKI:def 1;

        then f3 = (( Seg ( len f3)) --> 0 ) by FUNCOP_1: 9;

        then

         A20: f3 = (( len f3) |-> 0 ) by FINSEQ_2:def 2;

        then

        reconsider f3 as FinSequence of NAT ;

        (X \/ Y) = ( dom f1) by A3, XBOOLE_1: 45;

        then

         A21: ( Sum f1) = (( Sum f2) + ( Sum f3)) by A1, Th10, XBOOLE_1: 79;

        ( Sum f3) = 0 by A20, BAGORDER: 4;

        hence ( Sum f1) = ( Sum f2) by A21;

      end;

    end;

    theorem :: NAT_5:12

    

     Th12: f2 = (f1 - { 0 }) implies ( Sum f1) = ( Sum f2)

    proof

      

       A1: (( dom f1) \ (f1 " { 0 })) c= ( dom f1) by XBOOLE_1: 36;

      assume f2 = (f1 - { 0 });

      hence ( Sum f1) = ( Sum f2) by A1, Th11;

    end;

    theorem :: NAT_5:13

    

     Th13: for f be FinSequence of NAT holds f is FinSequence of REAL

    proof

      let f be FinSequence of NAT ;

      for n be Nat st n in ( dom f) holds (f . n) in REAL by XREAL_0:def 1;

      hence thesis by FINSEQ_2: 12;

    end;

    reserve n1,n2,m1,m2 for Nat;

    theorem :: NAT_5:14

    

     Th14: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) & (n,m) are_coprime implies (n1,m1) are_coprime

    proof

      

       A1: (n1 gcd m1) divides m1 by INT_2:def 2;

      assume n1 in ( NatDivisors n);

      then

       A2: n1 divides n by MOEBIUS1: 39;

      (n1 gcd m1) divides n1 by INT_2:def 2;

      then

       A3: (n1 gcd m1) divides n by A2, INT_2: 9;

      assume

       A4: m1 in ( NatDivisors m);

      then m1 divides m by MOEBIUS1: 39;

      then

       A5: (n1 gcd m1) divides m by A1, INT_2: 9;

       0 < m1 by A4, MOEBIUS1: 39;

      then (n1 gcd m1) <> 0 by INT_2: 5;

      then ((n1 gcd m1) + 1) > ( 0 + 1) by XREAL_1: 8;

      then

       A6: (n1 gcd m1) >= 1 by NAT_1: 13;

      assume

       A7: (n,m) are_coprime ;

      assume not (n1,m1) are_coprime ;

      then

       A8: (n1 gcd m1) <> 1 by INT_2:def 3;

      (n gcd m) > 0 by A7, INT_2:def 3;

      then (n1 gcd m1) <= (n gcd m) by A3, A5, INT_2: 22, INT_2: 27;

      then (n gcd m) <> 1 by A8, A6, XXREAL_0: 1;

      hence contradiction by A7, INT_2:def 3;

    end;

    theorem :: NAT_5:15

    

     Th15: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) & n2 in ( NatDivisors n) & m2 in ( NatDivisors m) & (n,m) are_coprime & (n1 * m1) = (n2 * m2) implies n1 = n2 & m1 = m2

    proof

      assume

       A1: n1 in ( NatDivisors n);

      then

       A2: n1 divides n by MOEBIUS1: 39;

      assume

       A3: m1 in ( NatDivisors m);

      then

       A4: m1 divides m by MOEBIUS1: 39;

      assume

       A5: n2 in ( NatDivisors n);

      then

       A6: n2 divides n by MOEBIUS1: 39;

      assume

       A7: m2 in ( NatDivisors m);

      assume

       A8: (n,m) are_coprime ;

      assume

       A9: (n1 * m1) = (n2 * m2);

      

       A10: m2 divides m by A7, MOEBIUS1: 39;

       A11:

      now

        reconsider m19 = m1, m29 = m2 as non zero Nat by A3, A7, MOEBIUS1: 39;

        

         A12: (n gcd m) > 0 by A8, INT_2:def 3;

        reconsider n19 = n1, n29 = n2 as non zero Nat by A1, A5, MOEBIUS1: 39;

        assume n1 <> n2;

        then

        consider p be Element of NAT such that

         A13: p is prime and

         A14: (p |-count n19) <> (p |-count n29) by NAT_4: 21;

        reconsider p as Prime by A13;

        ((p |-count n19) + (p |-count m19)) = (p |-count (n19 * m19)) by NAT_3: 28

        .= ((p |-count n29) + (p |-count m29)) by A9, NAT_3: 28;

        then (p |-count m19) <> 0 or (p |-count m29) <> 0 by A14;

        then p divides m19 or p divides m29 by MOEBIUS1: 6;

        then

         A15: p divides m by A4, A10, INT_2: 9;

        (p |-count n19) <> 0 or (p |-count n29) <> 0 by A14;

        then p divides n19 or p divides n29 by MOEBIUS1: 6;

        then p divides n by A2, A6, INT_2: 9;

        then p divides (n gcd m) by A15, INT_2:def 2;

        then

         A16: p <= (n gcd m) by A12, INT_2: 27;

        p > 1 by INT_2:def 4;

        hence contradiction by A8, A16, INT_2:def 3;

      end;

      

       A17: 0 < n2 by A5, MOEBIUS1: 39;

      assume not (n1 = n2 & m1 = m2);

      hence contradiction by A17, A9, A11, XCMPLX_1: 5;

    end;

    theorem :: NAT_5:16

    

     Th16: n1 in ( NatDivisors n0) & m1 in ( NatDivisors m0) implies (n1 * m1) in ( NatDivisors (n0 * m0))

    proof

      reconsider b = (n0 * m0) as non zero Nat;

      assume

       A1: n1 in ( NatDivisors n0);

      then

       A2: 0 < n1;

      

       A3: n1 divides n0 by A1, MOEBIUS1: 39;

      assume

       A4: m1 in ( NatDivisors m0);

      then

       A5: 0 < m1;

      then

      reconsider a = (n1 * m1) as non zero Nat by A2;

      

       A6: m1 divides m0 by A4, MOEBIUS1: 39;

      

       A7: (n1 * m1) in NAT by ORDINAL1:def 12;

      for p be Element of NAT st p is prime holds (p |-count a) <= (p |-count b)

      proof

        reconsider n19 = n1, m19 = m1 as non zero Nat by A1, A4;

        let p be Element of NAT ;

        assume p is prime;

        then

        reconsider p9 = p as Prime;

        

         A8: (p9 |-count (n19 * m19)) = ((p9 |-count n19) + (p9 |-count m19)) & (p9 |-count (n0 * m0)) = ((p9 |-count n0) + (p9 |-count m0)) by NAT_3: 28;

        (p9 |-count n19) <= (p9 |-count n0) & (p9 |-count m19) <= (p9 |-count m0) by A3, A6, NAT_3: 30;

        hence (p |-count a) <= (p |-count b) by A8, XREAL_1: 7;

      end;

      then ex c be Element of NAT st (n0 * m0) = ((n1 * m1) * c) by NAT_4: 20;

      then (n1 * m1) divides (n0 * m0) by NAT_D:def 3;

      hence (n1 * m1) in ( NatDivisors (n0 * m0)) by A2, A5, A7;

    end;

    theorem :: NAT_5:17

    

     Th17: (n0,m0) are_coprime implies (k gcd (n0 * m0)) = ((k gcd n0) * (k gcd m0))

    proof

      assume

       A1: (n0,m0) are_coprime ;

      per cases ;

        suppose

         A2: k = 0 ;

        

        hence (k gcd (n0 * m0)) = |.(n0 * m0).| by WSIERP_1: 8

        .= ( |.n0.| * |.m0.|) by COMPLEX1: 65

        .= ((k gcd n0) * |.m0.|) by A2, WSIERP_1: 8

        .= ((k gcd n0) * (k gcd m0)) by A2, WSIERP_1: 8;

      end;

        suppose k <> 0 ;

        then

        reconsider k9 = k as non zero Nat;

        reconsider a = (k gcd (n0 * m0)) as non zero Nat by INT_2: 5;

        reconsider b1 = (k gcd n0), b2 = (k gcd m0) as non zero Nat by INT_2: 5;

        (k gcd n0) <> 0 & (k gcd m0) <> 0 by INT_2: 5;

        then

        reconsider b = ((k gcd n0) * (k gcd m0)) as non zero Nat;

        for p be Element of NAT st p is prime holds (p |-count a) = (p |-count b)

        proof

          let p be Element of NAT ;

          assume p is prime;

          then

          reconsider p9 = p as Prime;

          

           A3: (p9 |-count a) = ( min ((p9 |-count k9),(p9 |-count (n0 * m0)))) by Lm1

          .= ( min ((p9 |-count k),((p9 |-count n0) + (p9 |-count m0)))) by NAT_3: 28;

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

          then p9 > 1 & (p9 |-count 1) = ( min ((p9 |-count n0),(p9 |-count m0))) by Lm1, INT_2:def 4;

          then

           A4: ( min ((p9 |-count n0),(p9 |-count m0))) = 0 by NAT_3: 21;

          

           A5: (p9 |-count b) = ((p9 |-count b1) + (p9 |-count b2)) by NAT_3: 28

          .= (( min ((p9 |-count k9),(p9 |-count n0))) + (p9 |-count b2)) by Lm1

          .= (( min ((p9 |-count k9),(p9 |-count n0))) + ( min ((p9 |-count k9),(p9 |-count m0)))) by Lm1;

          per cases by A4, XXREAL_0: 15;

            suppose

             A6: (p9 |-count n0) = 0 ;

            then ( min ((p9 |-count k),(p9 |-count n0))) = (p9 |-count n0) by XXREAL_0:def 9;

            hence (p |-count a) = (p |-count b) by A3, A5, A6;

          end;

            suppose

             A7: (p9 |-count m0) = 0 ;

            then ( min ((p9 |-count k),(p9 |-count m0))) = (p9 |-count m0) by XXREAL_0:def 9;

            hence (p |-count a) = (p |-count b) by A3, A5, A7;

          end;

        end;

        hence (k gcd (n0 * m0)) = ((k gcd n0) * (k gcd m0)) by NAT_4: 21;

      end;

    end;

    theorem :: NAT_5:18

    

     Th18: (n0,m0) are_coprime & k in ( NatDivisors (n0 * m0)) implies ex n1, m1 st n1 in ( NatDivisors n0) & m1 in ( NatDivisors m0) & k = (n1 * m1)

    proof

      assume

       A1: (n0,m0) are_coprime ;

      set m1 = (k gcd m0);

      set n1 = (k gcd n0);

      assume

       A2: k in ( NatDivisors (n0 * m0));

      take n1, m1;

      n1 divides n0 & n1 > 0 by NAT_D:def 5, NEWTON: 58;

      hence n1 in ( NatDivisors n0);

      m1 divides m0 & m1 > 0 by NAT_D:def 5, NEWTON: 58;

      hence m1 in ( NatDivisors m0);

      k divides (n0 * m0) by A2, MOEBIUS1: 39;

      

      hence k = (k gcd (n0 * m0)) by NEWTON: 49

      .= (n1 * m1) by A1, Th17;

    end;

    theorem :: NAT_5:19

    

     Th19: p is prime implies ( NatDivisors (p |^ n)) = { (p |^ k) where k be Element of NAT : k <= n }

    proof

      assume

       A1: p is prime;

      for x be object holds x in ( NatDivisors (p |^ n)) iff x in { (p |^ k) where k be Element of NAT : k <= n }

      proof

        let x be object;

        hereby

          assume

           A2: x in ( NatDivisors (p |^ n));

          then

          reconsider x9 = x as Nat;

          x9 divides (p |^ n) by A2, MOEBIUS1: 39;

          then ex t be Element of NAT st x9 = (p |^ t) & t <= n by A1, PEPIN: 34;

          hence x in { (p |^ k) where k be Element of NAT : k <= n };

        end;

        assume x in { (p |^ k) where k be Element of NAT : k <= n };

        then

         A3: ex t be Element of NAT st x = (p |^ t) & t <= n;

        then

        reconsider x9 = x as Nat;

        x9 divides (p |^ n) by A3, NEWTON: 89;

        hence x in ( NatDivisors (p |^ n)) by A1, A3, MOEBIUS1: 39;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: NAT_5:20

    

     Th20: 0 <> l & p > l & p > n1 & p > n2 & ((l * n1) mod p) = ((l * n2) mod p) & p is prime implies n1 = n2

    proof

      assume that

       A1: l <> 0 & p > l and

       A2: p > n1 and

       A3: p > n2;

      assume

       A4: ((l * n1) mod p) = ((l * n2) mod p);

      assume

       A5: p is prime;

      then (((l * n1) - (l * n2)) mod p) = 0 by A4, INT_4: 22;

      then

       A6: p divides (l * (n1 - n2)) by A5, INT_1: 62;

      per cases by A5, A6, INT_5: 7;

        suppose p divides l;

        hence thesis by A1, NAT_D: 7;

      end;

        suppose

         A7: p divides (n1 - n2);

        per cases ;

          suppose

           A8: (n1 - n2) > 0 ;

          then p divides (n1 -' n2) & (n1 -' n2) > 0 by A7, XREAL_0:def 2;

          then p <= (n1 -' n2) by NAT_D: 7;

          then (p + n2) <= ((n1 -' n2) + n2) by XREAL_1: 6;

          then (p + n2) <= ((n1 - n2) + n2) by A8, XREAL_0:def 2;

          then (p + n2) < p by A2, XXREAL_0: 2;

          then ((p + n2) - p) < (p - p) by XREAL_1: 9;

          then n2 < 0 ;

          hence thesis;

        end;

          suppose (n1 - n2) = 0 ;

          hence thesis;

        end;

          suppose (n1 - n2) < 0 ;

          then

           A9: ( - (n1 - n2)) > 0 ;

          then

           A10: (n2 - n1) > 0 ;

          then

           A11: (n2 -' n1) > 0 by XREAL_0:def 2;

          p divides ( - (n1 - n2)) by A7, INT_2: 10;

          then p divides (n2 -' n1) by A10, XREAL_0:def 2;

          then p <= (n2 -' n1) by A11, NAT_D: 7;

          then (p + n1) <= ((n2 -' n1) + n1) by XREAL_1: 6;

          then (p + n1) <= ((n2 - n1) + n1) by A9, XREAL_0:def 2;

          then (p + n1) < p by A3, XXREAL_0: 2;

          then ((p + n1) - p) < (p - p) by XREAL_1: 9;

          then n1 < 0 ;

          hence thesis;

        end;

      end;

    end;

    theorem :: NAT_5:21

    p is prime implies (p |-count (n0 gcd m0)) = ( min ((p |-count n0),(p |-count m0))) by Lm1;

    

     Lm4: k < m iff k <= (m - 1)

    proof

       A1:

      now

        assume k <= (m - 1);

        then

         A2: (k + 1) <= m by XREAL_1: 19;

        k < (k + 1) by XREAL_1: 29;

        hence k < m by A2, XXREAL_0: 2;

      end;

      now

        assume k < m;

        then (k + 1) <= m by INT_1: 7;

        hence k <= (m - 1) by XREAL_1: 19;

      end;

      hence thesis by A1;

    end;

    

     Lm5: for a be Element of NAT , fs be FinSequence holds a in ( dom fs) implies ex fs1,fs2 be FinSequence st fs = ((fs1 ^ <*(fs . a)*>) ^ fs2) & ( len fs1) = (a - 1) & ( len fs2) = (( len fs) - a)

    proof

      let a be Element of NAT ;

      let fs be FinSequence;

      assume

       A1: a in ( dom fs);

      then a >= 1 & a <= ( len fs) by FINSEQ_3: 25;

      then

      reconsider b = (( len fs) - a), d = (a - 1) as Element of NAT by INT_1: 5;

      ( len fs) = (a + b);

      then

      consider fs3,fs2 be FinSequence such that

       A2: ( len fs3) = a and

       A3: ( len fs2) = b and

       A4: fs = (fs3 ^ fs2) by FINSEQ_2: 22;

      a = (d + 1);

      then

      consider fs1 be FinSequence, v be object such that

       A5: fs3 = (fs1 ^ <*v*>) by A2, FINSEQ_2: 18;

      

       A6: (( len fs1) + 1) = (d + 1) by A2, A5, FINSEQ_2: 16;

      fs3 <> {} by A1, A2, FINSEQ_3: 25;

      then a in ( dom fs3) by A2, FINSEQ_5: 6;

      then (fs3 . a) = (fs . a) by A4, FINSEQ_1:def 7;

      then (fs . a) = v by A5, A6, FINSEQ_1: 42;

      hence thesis by A3, A4, A5, A6;

    end;

    

     Lm6: for a be Element of NAT , fs,fs1,fs2 be FinSequence, v be set holds a in ( dom fs) & fs = ((fs1 ^ <*v*>) ^ fs2) & ( len fs1) = (a - 1) implies ( Del (fs,a)) = (fs1 ^ fs2)

    proof

      let a be Element of NAT ;

      let fs,fs1,fs2 be FinSequence;

      let v be set;

      assume that

       A1: a in ( dom fs) and

       A2: fs = ((fs1 ^ <*v*>) ^ fs2) and

       A3: ( len fs1) = (a - 1);

      

       A4: (( len ( Del (fs,a))) + 1) = ( len fs) by A1, WSIERP_1:def 1;

      ( len fs) = (( len (fs1 ^ <*v*>)) + ( len fs2)) by A2, FINSEQ_1: 22

      .= ((( len fs1) + 1) + ( len fs2)) by FINSEQ_2: 16

      .= (a + ( len fs2)) by A3;

      then ( len ( Del (fs,a))) = (( len fs2) + ( len fs1)) by A3, A4;

      then

       A5: ( len (fs1 ^ fs2)) = ( len ( Del (fs,a))) by FINSEQ_1: 22;

      

       A6: ( len <*v*>) = 1 by FINSEQ_1: 39;

      

       A7: fs = (fs1 ^ ( <*v*> ^ fs2)) by A2, FINSEQ_1: 32;

      then ( len fs) = ((a - 1) + ( len ( <*v*> ^ fs2))) by A3, FINSEQ_1: 22;

      then

       A8: ( len ( <*v*> ^ fs2)) = (( len fs) - (a - 1));

      now

        let e be Nat;

        assume that

         A9: 1 <= e and

         A10: e <= ( len ( Del (fs,a)));

        now

          per cases ;

            suppose

             A11: e < a;

            then e <= (a - 1) by Lm4;

            then

             A12: e in ( dom fs1) by A3, A9, FINSEQ_3: 25;

            

            hence ((fs1 ^ fs2) . e) = (fs1 . e) by FINSEQ_1:def 7

            .= (fs . e) by A7, A12, FINSEQ_1:def 7

            .= (( Del (fs,a)) . e) by A1, A11, WSIERP_1:def 1;

          end;

            suppose

             A13: e >= a;

            then

             A14: e > (a - 1) by Lm4;

            then

             A15: (e + 1) > a by XREAL_1: 19;

            then ((e + 1) - a) > 0 by XREAL_1: 50;

            then

             A16: (((e + 1) - a) + 1) > ( 0 qua Nat + 1) by XREAL_1: 6;

            

             A17: (e + 1) > (a - 1) by A15, XREAL_1: 146, XXREAL_0: 2;

            then ((e + 1) - (a - 1)) > 0 by XREAL_1: 50;

            then

            reconsider f = ((e + 1) - (a - 1)) as Element of NAT by INT_1: 3;

            

             A18: (e + 1) <= ( len fs) by A4, A10, XREAL_1: 6;

            then

             A19: ((e + 1) - (a - 1)) <= ( len ( <*v*> ^ fs2)) by A8, XREAL_1: 9;

            

            thus ((fs1 ^ fs2) . e) = (fs2 . (e - ( len fs1))) by A3, A5, A10, A14, FINSEQ_1: 24

            .= (fs2 . (f - 1)) by A3

            .= (( <*v*> ^ fs2) . f) by A6, A16, A19, FINSEQ_1: 24

            .= ((fs1 ^ ( <*v*> ^ fs2)) . (e + 1)) by A3, A7, A17, A18, FINSEQ_1: 24

            .= (( Del (fs,a)) . e) by A1, A7, A13, WSIERP_1:def 1;

          end;

        end;

        hence ((fs1 ^ fs2) . e) = (( Del (fs,a)) . e);

      end;

      hence thesis by A5;

    end;

    

     Lm7: for fs be FinSequence holds 1 <= ( len fs) implies fs = ( <*(fs . 1)*> ^ ( Del (fs,1))) & fs = (( Del (fs,( len fs))) ^ <*(fs . ( len fs))*>)

    proof

      let fs be FinSequence;

      set fs1 = ( <*(fs . 1)*> ^ ( Del (fs,1)));

      set fs2 = (( Del (fs,( len fs))) ^ <*(fs . ( len fs))*>);

      

       A1: ( len <*(fs . 1)*>) = 1 by FINSEQ_1: 39;

      assume

       A2: 1 <= ( len fs);

      then

       A3: ( len fs) in ( dom fs) by FINSEQ_3: 25;

      

       A4: 1 in ( dom fs) by A2, FINSEQ_3: 25;

      

      then

       A5: ( len fs) = (( len <*(fs . 1)*>) + ( len ( Del (fs,1)))) by A1, WSIERP_1:def 1

      .= ( len fs1) by FINSEQ_1: 22;

      for b be Nat st 1 <= b & b <= ( len fs) holds (fs . b) = (fs1 . b)

      proof

        let b be Nat;

        assume that

         A6: 1 <= b and

         A7: b <= ( len fs);

        now

          per cases by A6, XXREAL_0: 1;

            suppose

             A8: b = 1;

            1 in ( dom <*(fs . 1)*>) by A1, FINSEQ_3: 25;

            

            hence (fs1 . b) = ( <*(fs . 1)*> . 1) by A8, FINSEQ_1:def 7

            .= (fs . b) by A8, FINSEQ_1: 40;

          end;

            suppose

             A9: b > 1;

            then

             A10: (b - 1) > 0 by XREAL_1: 50;

            then

            reconsider e = (b - 1) as Element of NAT by INT_1: 3;

            

             A11: e >= 1 by A10, NAT_1: 14;

            

            thus (fs1 . b) = (( Del (fs,1)) . e) by A1, A5, A7, A9, FINSEQ_1: 24

            .= (fs . (e + 1)) by A4, A11, WSIERP_1:def 1

            .= (fs . b);

          end;

        end;

        hence thesis;

      end;

      hence fs1 = fs by A5;

      ( len <*(fs . ( len fs))*>) = 1 by FINSEQ_1: 39;

      

      then

       A12: ( len fs) = (( len <*(fs . ( len fs))*>) + ( len ( Del (fs,( len fs))))) by A3, WSIERP_1:def 1

      .= ( len fs2) by FINSEQ_1: 22;

      

       A13: (( len ( Del (fs,( len fs)))) + 1) = ( len fs) by A3, WSIERP_1:def 1;

      then

       A14: ( len ( Del (fs,( len fs)))) = (( len fs) - 1);

      for b be Nat st 1 <= b & b <= ( len fs) holds (fs . b) = (fs2 . b)

      proof

        let b be Nat;

        assume that

         A15: 1 <= b and

         A16: b <= ( len fs);

        now

          per cases by A16, XXREAL_0: 1;

            suppose

             A17: b = ( len fs);

            reconsider e = (b - (b - 1)) as Element of NAT ;

            

            thus (fs2 . b) = ( <*(fs . ( len fs))*> . e) by A13, A12, A17, FINSEQ_1: 24, XREAL_1: 146

            .= (fs . b) by A17, FINSEQ_1: 40;

          end;

            suppose

             A18: b < ( len fs);

            then (b + 1) <= ( len fs) by NAT_1: 13;

            then b <= ( len ( Del (fs,( len fs)))) by A14, XREAL_1: 19;

            then b in ( dom ( Del (fs,( len fs)))) by A15, FINSEQ_3: 25;

            

            hence (fs2 . b) = (( Del (fs,( len fs))) . b) by FINSEQ_1:def 7

            .= (fs . b) by A3, A18, WSIERP_1:def 1;

          end;

        end;

        hence thesis;

      end;

      hence fs2 = fs by A12;

    end;

    

     Lm8: for a be Nat, ft be FinSequence of REAL holds a in ( dom ft) implies (( Product ( Del (ft,a))) * (ft . a)) = ( Product ft)

    proof

      let a be Nat;

      let ft be FinSequence of REAL ;

      defpred P[ Nat] means $1 in ( dom ft) implies ((ft . $1) * ( Product ( Del (ft,$1)))) = ( Product ft);

      

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

      proof

        let a be Nat such that P[a];

        now

          per cases ;

            suppose

             A2: a = 0 ;

            thus P[(a + 1)]

            proof

              assume (a + 1) in ( dom ft);

              then (a + 1) <= ( len ft) by FINSEQ_3: 25;

              then ( <*(ft . 1)*> ^ ( Del (ft,1))) = ft by A2, Lm7;

              

              then ( Product ft) = (( Product <*(ft . 1)*>) * ( Product ( Del (ft,1)))) by RVSUM_1: 97

              .= ((ft . 1) * ( Product ( Del (ft,1))));

              hence thesis by A2;

            end;

          end;

            suppose a > 0 & a < ( len ft);

            then (a + 1) >= 1 & (a + 1) <= ( len ft) by NAT_1: 11, NAT_1: 13;

            then

             A3: (a + 1) in ( dom ft) by FINSEQ_3: 25;

            then

            consider fs1,fs2 be FinSequence such that

             A4: ft = ((fs1 ^ <*(ft . (a + 1))*>) ^ fs2) and

             A5: ( len fs1) = ((a + 1) - 1) and ( len fs2) = (( len ft) - (a + 1)) by Lm5;

            

             A6: ( Del (ft,(a + 1))) = (fs1 ^ fs2) by A3, A4, A5, Lm6;

            reconsider fs2 as FinSequence of REAL by A4, FINSEQ_1: 36;

            reconsider fs1 as FinSequence of REAL by A6, FINSEQ_1: 36;

            ( Product ft) = (( Product (fs1 ^ <*(ft . (a + 1))*>)) * ( Product fs2)) by A4, RVSUM_1: 97

            .= ((( Product fs1) * ( Product <*(ft . (a + 1))*>)) * ( Product fs2)) by RVSUM_1: 97

            .= (((ft . (a + 1)) * ( Product fs1)) * ( Product fs2))

            .= ((ft . (a + 1)) * (( Product fs1) * ( Product fs2)));

            hence P[(a + 1)] by A6, RVSUM_1: 97;

          end;

            suppose a >= ( len ft);

            then ( len ft) < (a + 1) by NAT_1: 13;

            hence P[(a + 1)] by FINSEQ_3: 25;

          end;

        end;

        hence thesis;

      end;

      

       A7: P[ 0 ] by FINSEQ_3: 25;

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

      hence thesis;

    end;

    

     Lm9: (n + 2) is prime implies for l st l in ( Seg n) & l <> 1 holds ex k st k in ( Seg n) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1

    proof

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

      assume

       A1: (n + 2) is prime;

      then

       A2: 1 < (n9 + 2) by INT_2:def 4;

      let l;

      reconsider l9 = l as Element of NAT by ORDINAL1:def 12;

      assume

       A3: l in ( Seg n);

      then

       A4: l9 <> 0 by FINSEQ_1: 1;

      assume

       A5: l <> 1;

      

       A6: l <= n by A3, FINSEQ_1: 1;

      then

       A7: l < (n + 1) by NAT_1: 13;

      

       A8: (1 + n) < (2 + n) by XREAL_1: 6;

      then l9 < (n9 + 2) by A7, XXREAL_0: 2;

      then

      consider k be Nat such that

       A9: ((k * l9) mod (n9 + 2)) = 1 and

       A10: k < (n9 + 2) by A1, A2, A4, IDEA_1: 1;

      take k;

      k <> 0 by A9, NAT_D: 26;

      then

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

      

       A12: 1 <= l by A3, FINSEQ_1: 1;

      then

       A13: (1 - 1) <= (l - 1) by XREAL_1: 9;

      

       A14: l < (n + 2) by A7, A8, XXREAL_0: 2;

      then

       A15: (n + 2) > 1 by A12, XXREAL_0: 2;

      

       A16: (l + 1) < ((n + 1) + 1) by A7, XREAL_1: 6;

      

       A17: k <> (n + 1)

      proof

        assume k = (n + 1);

        

        then (((n + 1) * l) mod (n + 2)) = (1 mod (n + 2)) by A9, A15, NAT_D: 14

        .= ((((n + 2) * l) + 1) mod (n + 2)) by NAT_D: 21;

        

        then 0 = (((((n + 2) * l) + 1) - ((n + 1) * l)) mod (n + 2)) by INT_4: 22

        .= (l + 1) by A16, NAT_D: 24;

        hence contradiction;

      end;

      k < ((n + 1) + 1) by A10;

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

      then k < (n + 1) by A17, XXREAL_0: 1;

      then k <= n by NAT_1: 13;

      hence k in ( Seg n) by A11;

      (l - 1) < ((n + 2) - 1) by A14, XREAL_1: 9;

      then (l - 1) < (n + 2) by A8, XXREAL_0: 2;

      then

       A18: (l -' 1) < (n + 2) by XREAL_0:def 2;

      thus

       A19: k <> 1

      proof

        assume k = 1;

        then ((1 * l) mod (n + 2)) = (1 mod (n + 2)) by A9, A10, NAT_D: 14;

        

        then 0 = ((l - 1) mod (n + 2)) by INT_4: 22

        .= ((l -' 1) mod (n + 2)) by A13, XREAL_0:def 2

        .= (l -' 1) by A18, NAT_D: 24

        .= (l - 1) by A13, XREAL_0:def 2;

        hence contradiction by A5;

      end;

      thus k <> l

      proof

        assume

         A20: k = l;

        then ((l * l) mod (n + 2)) = (1 mod (n + 2)) by A9, A15, NAT_D: 14;

        then 0 = (((l * l) - 1) mod (n + 2)) by INT_4: 22;

        then

         A21: (n + 2) divides ((l + 1) * (l - 1)) by INT_1: 62;

        per cases by A1, A21, INT_5: 7;

          suppose (n + 2) divides (l + 1);

          then (n + 2) <= (l + 1) by NAT_D: 7;

          then ((n + 2) - 1) <= ((l + 1) - 1) by XREAL_1: 9;

          hence contradiction by A7;

        end;

          suppose (n + 2) divides (l - 1);

          then

           A22: (n + 2) divides (l -' 1) by A13, XREAL_0:def 2;

          per cases ;

            suppose l = 1;

            hence contradiction by A19, A20;

          end;

            suppose l <> 1;

            then l > 1 by A12, XXREAL_0: 1;

            then (l - 1) > (1 - 1) by XREAL_1: 9;

            then (l -' 1) > 0 by XREAL_0:def 2;

            then (n + 2) <= (l -' 1) by A22, NAT_D: 7;

            then (n + 2) <= (l - 1) by XREAL_0:def 2;

            then ((n + 2) + 1) <= ((l - 1) + 1) by XREAL_1: 6;

            then (n + 3) <= n by A6, XXREAL_0: 2;

            then ((n + 3) - n) <= (n - n) by XREAL_1: 9;

            then 3 <= 0 ;

            hence contradiction;

          end;

        end;

      end;

      thus ((l * k) mod (n + 2)) = 1 by A9;

    end;

    

     Lm10: for f be FinSequence of NAT st (n + 2) is prime & ( rng f) c= ( Seg n) & f is one-to-one & (for l st l in ( rng f) & l <> 1 holds ex k st k in ( rng f) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1) holds (( Product f) mod (n + 2)) = 1

    proof

      defpred P[ Nat] means for f be FinSequence of NAT st ( len f) = $1 & (n + 2) is prime & ( rng f) c= ( Seg n) & f is one-to-one & (for l st l in ( rng f) & l <> 1 holds ex k st k in ( rng f) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1) holds (( Product f) mod (n + 2)) = 1;

      let f be FinSequence of NAT ;

      set n9 = ( len f);

      

       A1: for k9 be Nat st for n9 be Nat st n9 < k9 holds P[n9] holds P[k9]

      proof

        let k9 be Nat;

        assume

         A2: for n9 be Nat st n9 < k9 holds P[n9];

        thus P[k9]

        proof

          let f be FinSequence of NAT ;

          assume

           A3: ( len f) = k9;

          assume

           A4: (n + 2) is prime;

          assume

           A5: ( rng f) c= ( Seg n);

          assume

           A6: f is one-to-one;

          assume

           A7: for l st l in ( rng f) & l <> 1 holds ex k st k in ( rng f) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1;

          per cases ;

            suppose

             A8: k9 = 0 ;

            

             A9: ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

            f = ( <*> NAT ) by A3, A8;

            then ( Product f) = 1 by RVSUM_1: 94;

            hence (( Product f) mod (n + 2)) = 1 by A9, NAT_D: 24;

          end;

            suppose

             A10: k9 <> 0 ;

            reconsider f9 = f as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

            ( dom f) <> {} by A3, A10, CARD_1: 27, RELAT_1: 41;

            then

            consider x1 be object such that

             A11: x1 in ( dom f) by XBOOLE_0:def 1;

            reconsider x1 as Element of NAT by A11;

            

             A12: ex m be Nat st ( len f) = (m + 1) & ( len ( Del (f,x1))) = m by A11, FINSEQ_3: 104;

            

             A13: (( Product ( Del (f9,x1))) * (f9 . x1)) = ( Product f) by A11, Lm8;

            

             A14: ( rng ( Del (f,x1))) c= ( rng f) by FINSEQ_3: 106;

            then

             A15: ( rng ( Del (f,x1))) c= ( Seg n) by A5;

            set n19 = ( len ( Del (f,x1)));

            

             A16: ( 0 + n19) < (1 + n19) by XREAL_1: 6;

            

             A17: ( Del (f,x1)) is one-to-one by A6, Th6;

            per cases ;

              suppose

               A18: (f9 . x1) = 1;

              for l st l in ( rng ( Del (f,x1))) & l <> 1 holds ex k st k in ( rng ( Del (f,x1))) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1

              proof

                let l;

                assume

                 A19: l in ( rng ( Del (f,x1)));

                assume l <> 1;

                then

                consider k such that

                 A20: k in ( rng f) and

                 A21: k <> 1 and

                 A22: k <> l & ((l * k) mod (n + 2)) = 1 by A7, A14, A19;

                take k;

                thus k in ( rng ( Del (f,x1))) by A18, A20, A21, Th8;

                thus k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1 by A21, A22;

              end;

              hence (( Product f) mod (n + 2)) = 1 by A2, A3, A4, A13, A15, A17, A12, A16, A18;

            end;

              suppose

               A23: (f9 . x1) <> 1;

              set f99 = ( Del (f,x1));

              

               A24: f99 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

              set l = (f . x1);

              

               A25: l in ( rng f) by A11, FUNCT_1: 3;

              then

              consider k be Nat such that

               A26: k in ( rng f) and k <> 1 and

               A27: k <> l and

               A28: ((l * k) mod (n + 2)) = 1 by A7, A23;

              k in ( rng f99) by A26, A27, Th8;

              then

              consider x2 be object such that

               A29: x2 in ( dom f99) and

               A30: k = (f99 . x2) by FUNCT_1:def 3;

              reconsider x2 as Element of NAT by A29;

              

               A31: ( rng ( Del (f99,x2))) c= ( rng ( Del (f9,x1))) by FINSEQ_3: 106;

              then

               A32: ( rng ( Del (f99,x2))) c= ( Seg n) by A15;

              

               A33: for l st l in ( rng ( Del (f99,x2))) & l <> 1 holds ex k st k in ( rng ( Del (f99,x2))) & k <> 1 & k <> l & ((l * k) mod (n + 2)) = 1

              proof

                

                 A34: 1 <= l by A5, A25, FINSEQ_1: 1;

                

                 A35: ( 0 + n) < (2 + n) by XREAL_1: 6;

                l <= n by A5, A25, FINSEQ_1: 1;

                then

                 A36: (n + 2) > l by A35, XXREAL_0: 2;

                k <= n by A5, A26, FINSEQ_1: 1;

                then

                 A37: (n + 2) > k by A35, XXREAL_0: 2;

                let l9 be Nat;

                

                 A38: ( 0 + n) < (2 + n) by XREAL_1: 6;

                assume

                 A39: l9 in ( rng ( Del (f99,x2)));

                then

                 A40: l9 in ( rng ( Del (f9,x1))) by A31;

                then l9 in ( rng f) by A14;

                then

                 A41: l9 <= n by A5, FINSEQ_1: 1;

                assume l9 <> 1;

                then

                consider k9 be Nat such that

                 A42: k9 in ( rng f) and

                 A43: k9 <> 1 & k9 <> l9 and

                 A44: ((l9 * k9) mod (n + 2)) = 1 by A7, A14, A40;

                take k9;

                

                 A45: 1 <= k by A5, A26, FINSEQ_1: 1;

                thus k9 in ( rng ( Del (f99,x2)))

                proof

                  assume

                   A46: not k9 in ( rng ( Del (f99,x2)));

                  per cases ;

                    suppose

                     A47: k9 in ( rng f99);

                    

                     A48: l9 < (n + 2) by A41, A38, XXREAL_0: 2;

                    ((k * l) mod (n + 2)) = ((k * l9) mod (n + 2)) by A28, A30, A44, A46, A47, Th8;

                    then l9 = l by A4, A45, A37, A36, A48, Th20;

                    hence contradiction by A6, A11, A31, A39, Th7;

                  end;

                    suppose

                     A49: not k9 in ( rng f99);

                    

                     A50: l9 < (n + 2) by A41, A38, XXREAL_0: 2;

                    ((l * k) mod (n + 2)) = ((l * l9) mod (n + 2)) by A28, A42, A44, A49, Th8;

                    then (f99 . x2) in ( rng ( Del (f99,x2))) by A4, A30, A39, A34, A37, A36, A50, Th20;

                    hence contradiction by A6, A29, Th6, Th7;

                  end;

                end;

                thus k9 <> 1 & k9 <> l9 & ((l9 * k9) mod (n + 2)) = 1 by A43, A44;

              end;

              set n299 = ( len ( Del (f99,x2)));

              

               A51: ( 0 + n299) < (1 + n299) by XREAL_1: 6;

              ex m be Nat st ( len ( Del (f9,x1))) = (m + 1) & ( len ( Del (f99,x2))) = m by A29, FINSEQ_3: 104;

              then

               A52: n299 < k9 by A3, A12, A16, A51, XXREAL_0: 2;

              

               A53: ( Del (f99,x2)) is one-to-one by A17, Th6;

              (( Product ( Del (f99,x2))) * (f99 . x2)) = ( Product f99) by A29, Lm8, A24;

              then (( Product ( Del (f99,x2))) * (k * l)) = ( Product f) by A13, A30;

              

              hence (( Product f) mod (n + 2)) = ((( Product ( Del (f99,x2))) * ((k * l) mod (n + 2))) mod (n + 2)) by EULER_2: 7

              .= 1 by A2, A4, A28, A32, A53, A33, A52;

            end;

          end;

        end;

      end;

      for n9 be Nat holds P[n9] from NAT_1:sch 4( A1);

      then P[n9];

      hence thesis;

    end;

    begin

    ::$Notion-Name

    theorem :: NAT_5:22

    n is prime iff ((((n -' 1) ! ) + 1) mod n) = 0 & n > 1

    proof

      thus n is prime implies ((((n -' 1) ! ) + 1) mod n) = 0 & n > 1

      proof

        assume

         A1: n is prime;

        per cases ;

          suppose n < 2;

          then n < (1 + 1);

          then n <= 1 by NAT_1: 13;

          hence thesis by A1, INT_2:def 4;

        end;

          suppose n >= 2;

          then

           A2: (n - 2) >= (2 - 2) by XREAL_1: 9;

          then

           A3: ((n - 2) + 1) >= ( 0 + 1) by XREAL_1: 6;

          set l = (n -' 2);

          

           A4: (2 + l) > (1 + l) by XREAL_1: 6;

          set f = ( Sgm ( Seg l));

          

           A5: ((n * 1) mod n) = 0 by NAT_D: 13;

          

           A6: l = (n - 2) by A2, XREAL_0:def 2;

          

          then

           A7: (l + 1) = (n - 1)

          .= (n -' 1) by A3, XREAL_0:def 2;

          

           A8: for l9 be Nat st l9 in ( rng f) & l9 <> 1 holds ex k9 be Nat st k9 in ( rng f) & k9 <> 1 & k9 <> l9 & ((l9 * k9) mod (l + 2)) = 1

          proof

            let l9 be Nat;

            assume l9 in ( rng f);

            then

             A9: l9 in ( Seg l) by FINSEQ_1:def 13;

            assume l9 <> 1;

            then

            consider k9 be Nat such that

             A10: k9 in ( Seg l) & k9 <> 1 & k9 <> l9 & ((l9 * k9) mod (l + 2)) = 1 by A1, A6, A9, Lm9;

            take k9;

            thus thesis by A10, FINSEQ_1:def 13;

          end;

          (l ! ) = ( Product ( Sgm ( Seg l))) & ( rng f) c= ( Seg l) by FINSEQ_1:def 13, FINSEQ_3: 48;

          then

           A11: ((l ! ) mod (l + 2)) = 1 by A1, A6, A8, Lm10, FINSEQ_3: 92;

          (((l + 1) ! ) mod (l + 2)) = (((l + 1) * (l ! )) mod (l + 2)) by NEWTON: 15

          .= (((l + 1) * 1) mod (l + 2)) by A11, EULER_2: 7

          .= (l + 1) by A4, NAT_D: 24;

          then (((((l + 1) ! ) mod (l + 2)) + 1) mod (l + 2)) = 0 by A6, A5;

          hence thesis by A1, A6, A7, INT_2:def 4, NAT_D: 22;

        end;

      end;

      thus ((((n -' 1) ! ) + 1) mod n) = 0 & n > 1 implies n is prime

      proof

        assume that

         A12: ((((n -' 1) ! ) + 1) mod n) = 0 and

         A13: n > 1;

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

        then

        consider k be Element of NAT such that

         A14: k is prime and

         A15: k divides n by INT_2: 31;

        consider i be Nat such that

         A16: n = (k * i) by A15, NAT_D:def 3;

        

         A17: k <> 1 by A14, INT_2:def 4;

        ((((n -' 1) ! ) + 1) mod n) = ((((n -' 1) ! ) + 1) mod k) by A12, A13, A14, A16, PEPIN: 9;

        then k divides (((n -' 1) ! ) + 1) by A12, A14, PEPIN: 6;

        then k > (n -' 1) by A14, A17, NEWTON: 42;

        then k > (n - 1) by XREAL_0:def 2;

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

        then k >= n by NAT_1: 13;

        then (k / k) >= ((k * i) / k) by A16, XREAL_1: 72;

        then 1 >= ((k * i) / k) by A14, XCMPLX_1: 60;

        then 1 >= (i * (k / k)) by XCMPLX_1: 74;

        then

         A18: 1 >= (i * 1) by A14, XCMPLX_1: 60;

        assume

         A19: not n is prime;

        i <> 0 by A13, A16;

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

        then i = 1 by A18, XXREAL_0: 1;

        hence contradiction by A19, A14, A16;

      end;

    end;

    begin

    ::$Notion-Name

    theorem :: NAT_5:23

    p is prime & (p mod 4) = 1 implies ex n, m st p = ((n ^2 ) + (m ^2 ))

    proof

       0 <= ( sqrt p) by SQUARE_1:def 2;

      then

      reconsider p9 = [\( sqrt p)/] as Element of NAT by INT_1: 3, INT_1: 54;

      reconsider p99 = (p9 + 1) as Element of NAT ;

      set X = ( Segm p99);

      

       A1: (( sqrt p) * ( card X)) < (( card X) * ( card X)) by INT_1: 29, XREAL_1: 68;

      assume

       A2: p is prime;

      then p > 1 by INT_2:def 4;

      then (p + 1) > (1 + 1) by XREAL_1: 6;

      then

       A3: p >= 2 by NAT_1: 13;

      

       A4: (p9 ^2 ) <> p

      proof

        assume (p9 ^2 ) = p;

        then

        reconsider p99 = ( sqrt p) as Element of NAT by SQUARE_1:def 2;

        (p99 ^2 ) = p by SQUARE_1:def 2;

        then

         A5: (p99 * p99) = p by SQUARE_1:def 1;

        then

         A6: p99 divides p by INT_1:def 3;

        per cases by A2, A6, INT_2:def 4;

          suppose p99 = 1;

          hence contradiction by A2, A5, INT_2:def 4;

        end;

          suppose p99 = p;

          

          then 1 = ((p * p) / p) by A2, A5, XCMPLX_1: 60

          .= (p * (p / p)) by XCMPLX_1: 74

          .= (p * 1) by A2, XCMPLX_1: 60;

          hence contradiction by A2, INT_2:def 4;

        end;

      end;

      p9 <= ( sqrt p) by INT_1:def 6;

      then (p9 ^2 ) <= (( sqrt p) ^2 ) by SQUARE_1: 15;

      then (p9 ^2 ) <= p by SQUARE_1:def 2;

      then

       A7: (p9 ^2 ) < p by A4, XXREAL_0: 1;

      assume

       A8: (p mod 4) = 1;

      then p <> 2 by NAT_D: 24;

      then p > 2 by A3, XXREAL_0: 1;

      then ( - 1) is_quadratic_residue_mod p by A2, A8, INT_5: 37;

      then

      consider s be Integer such that

       A9: (((s ^2 ) - ( - 1)) mod p) = 0 by INT_5:def 2;

       0 < ( sqrt p) by A2, SQUARE_1: 25;

      then (( sqrt p) * ( sqrt p)) < (( card X) * ( sqrt p)) by INT_1: 29, XREAL_1: 68;

      then (( sqrt p) * ( sqrt p)) < (( card X) * ( card X)) by A1, XXREAL_0: 2;

      then ( sqrt (p * p)) < (( card X) * ( card X)) by SQUARE_1: 29;

      then ( sqrt (p ^2 )) < (( card X) * ( card X)) by SQUARE_1:def 1;

      then p < (( card X) * ( card X)) by SQUARE_1: 22;

      then

       A10: p < ( card [:X, X:]) by CARD_2: 46;

      for s be Integer holds ex x9,x99,y9,y99 be Nat st x9 in X & x99 in X & y9 in X & y99 in X & [x9, y9] <> [x99, y99] & ((x9 - (s * y9)) mod p) = ((x99 - (s * y99)) mod p)

      proof

        set A = [:X, X:];

        reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

        let s be Integer;

        set B = ( Segm p9);

        defpred P[ object, object] means ex n1,n2,n3 be Element of NAT st $1 = [n1, n2] & $2 = n3 & ((n1 - (s * n2)) mod p) = n3;

        

         A11: ( card B) in ( Segm ( card A)) by A10, NAT_1: 44;

        

         A12: for x be object st x in A holds ex y be object st y in B & P[x, y]

        proof

          let x be object;

          assume x in A;

          then

          consider n1,n2 be object such that

           A13: n1 in X & n2 in X and

           A14: x = [n1, n2] by ZFMISC_1:def 2;

          reconsider n1, n2 as Element of NAT by A13;

          set y = ((n1 - (s * n2)) mod p);

          reconsider y as Element of NAT by INT_1: 3, INT_1: 57;

          take y;

          y < p by A2, INT_1: 58;

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

          hence y in B;

          thus P[x, y] by A14;

        end;

        consider f be Function of A, B such that

         A15: for x be object st x in A holds P[x, (f . x)] from FUNCT_2:sch 1( A12);

        B <> {} by A2;

        then

        consider x1,x2 be object such that

         A16: x1 in A and

         A17: x2 in A and

         A18: x1 <> x2 and

         A19: (f . x1) = (f . x2) by A11, FINSEQ_4: 65;

        consider x9,y9 be object such that

         A20: x9 in X & y9 in X and

         A21: x1 = [x9, y9] by A16, ZFMISC_1:def 2;

        reconsider x9, y9 as Nat by A20;

        consider x99,y99 be object such that

         A22: x99 in X & y99 in X and

         A23: x2 = [x99, y99] by A17, ZFMISC_1:def 2;

        reconsider x99, y99 as Nat by A22;

        take x9, x99, y9, y99;

        thus x9 in X & x99 in X & y9 in X & y99 in X by A20, A22;

        thus [x9, y9] <> [x99, y99] by A18, A21, A23;

        consider n11,n12,n13 be Element of NAT such that

         A24: x1 = [n11, n12] and

         A25: (f . x1) = n13 & ((n11 - (s * n12)) mod p) = n13 by A15, A16;

        

         A26: n11 = x9 & n12 = y9 by A21, A24, XTUPLE_0: 1;

        consider n21,n22,n23 be Element of NAT such that

         A27: x2 = [n21, n22] and

         A28: (f . x2) = n23 & ((n21 - (s * n22)) mod p) = n23 by A15, A17;

        n21 = x99 by A23, A27, XTUPLE_0: 1;

        hence ((x9 - (s * y9)) mod p) = ((x99 - (s * y99)) mod p) by A19, A23, A25, A27, A28, A26, XTUPLE_0: 1;

      end;

      then

      consider x9,x99,y9,y99 be Nat such that

       A29: x9 in X and

       A30: x99 in X and

       A31: y9 in X and

       A32: y99 in X and

       A33: [x9, y9] <> [x99, y99] and

       A34: ((x9 - (s * y9)) mod p) = ((x99 - (s * y99)) mod p);

      set m9 = (y9 - y99);

      

       A35: 0 = (((((s ^2 ) + 1) mod p) * ((m9 ^2 ) mod p)) mod p) by A9, INT_1: 73

      .= ((((s ^2 ) + 1) * (m9 ^2 )) mod p) by NAT_D: 67

      .= ((((s ^2 ) * (m9 ^2 )) + (m9 ^2 )) mod p)

      .= ((((s * m9) ^2 ) + (m9 ^2 )) mod p) by SQUARE_1: 9;

      set n9 = (x9 - x99);

      

       A36: ((n9 + (s * m9)) * (n9 - (s * m9))) = ((n9 to_power 2) - ((s * m9) to_power 2)) by FIB_NUM3: 7

      .= ((n9 ^2 ) - ((s * m9) to_power 2)) by POWER: 46

      .= ((n9 ^2 ) - ((s * m9) ^2 )) by POWER: 46;

      (((x9 - (s * y9)) mod p) - ((x99 - (s * y99)) mod p)) = 0 by A34;

      then (((x9 - (s * y9)) - (x99 - (s * y99))) mod p) = ( 0 mod p) by INT_6: 7;

      then (((x9 - x99) - (s * (y9 - y99))) mod p) = 0 by INT_1: 73;

      

      then 0 = ((((n9 + (s * m9)) mod p) * ((n9 - (s * m9)) mod p)) mod p) by INT_1: 73

      .= (((n9 ^2 ) - ((s * m9) ^2 )) mod p) by A36, NAT_D: 67;

      

      then 0 = (((((n9 ^2 ) - ((s * m9) ^2 )) mod p) + ((((s * m9) ^2 ) + (m9 ^2 )) mod p)) mod p) by A35, INT_1: 73

      .= ((((n9 ^2 ) - ((s * m9) ^2 )) + (((s * m9) ^2 ) + (m9 ^2 ))) mod p) by NAT_D: 66

      .= (((n9 ^2 ) + (m9 ^2 )) mod p);

      then p divides ((n9 ^2 ) + (m9 ^2 )) by A2, INT_1: 62;

      then

      consider i be Integer such that

       A37: ((n9 ^2 ) + (m9 ^2 )) = (p * i) by INT_1:def 3;

      

       A38: (p * i) = (( |.n9.| ^2 ) + (m9 ^2 )) by A37, COMPLEX1: 75

      .= (( |.n9.| ^2 ) + ( |.m9.| ^2 )) by COMPLEX1: 75;

      y9 in ( Segm p99) by A31;

      then y9 < p99 by NAT_1: 44;

      then

       A39: y9 <= p9 by NAT_1: 13;

      x99 in ( Segm p99) by A30;

      then x99 < p99 by NAT_1: 44;

      then

       A40: x99 <= p9 by NAT_1: 13;

      y99 in ( Segm p99) by A32;

      then y99 < p99 by NAT_1: 44;

      then

       A41: y99 <= p9 by NAT_1: 13;

      x9 in ( Segm p99) by A29;

      then x9 < p99 by NAT_1: 44;

      then

       A42: x9 <= p9 by NAT_1: 13;

      set m = |.m9.|;

      set n = |.n9.|;

      reconsider x9, x99, y9, y99 as Real;

       |.(y9 - y99).| <= (p9 - 0 ) by A39, A41, JGRAPH_1: 27;

      then (m ^2 ) <= (p9 ^2 ) by SQUARE_1: 15;

      then

       A43: (m ^2 ) < p by A7, XXREAL_0: 2;

       |.(x9 - x99).| <= (p9 - 0 ) by A42, A40, JGRAPH_1: 27;

      then (n ^2 ) <= (p9 ^2 ) by SQUARE_1: 15;

      then (n ^2 ) < p by A7, XXREAL_0: 2;

      then ((n ^2 ) + (m ^2 )) < (p + p) by A43, XREAL_1: 8;

      then ((i * p) / p) < ((2 * p) / p) by A2, A38, XREAL_1: 74;

      then ((i * p) / p) < (2 * (p / p)) by XCMPLX_1: 74;

      then (i * (p / p)) < (2 * (p / p)) by XCMPLX_1: 74;

      then (i * (p / p)) < (2 * 1) by A2, XCMPLX_1: 60;

      then (i * 1) < 2 by A2, XCMPLX_1: 60;

      then (i + 1) <= 2 by INT_1: 7;

      then

       A44: ((i + 1) - 1) <= (2 - 1) by XREAL_1: 9;

      reconsider n, m as Nat by TARSKI: 1;

      take n, m;

      ((n ^2 ) + (m ^2 )) <> 0

      proof

        assume

         A45: ((n ^2 ) + (m ^2 )) = 0 ;

        then (m ^2 ) = 0 ;

        then (m * m) = 0 by SQUARE_1:def 1;

        then m = 0 ;

        then

         A46: (y9 - y99) = 0 by ABSVALUE: 2;

        (n ^2 ) = 0 by A45;

        then (n * n) = 0 by SQUARE_1:def 1;

        then n = 0 ;

        then (x9 - x99) = 0 by ABSVALUE: 2;

        hence contradiction by A33, A46;

      end;

      then i > 0 by A38;

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

      then i = 1 by A44, XXREAL_0: 1;

      hence thesis by A38;

    end;

    begin

    definition

      let I be set;

      let f be Function of I, NAT ;

      let J be finite Subset of I;

      :: original: |

      redefine

      func f | J -> bag of J ;

      correctness ;

    end

    registration

      let I be set;

      let f be Function of I, NAT ;

      let J be finite Subset of I;

      cluster ( Sum (f | J)) -> natural;

      correctness

      proof

        set b = (f | J);

        consider f9 be FinSequence of REAL such that

         A1: ( Sum b) = ( Sum f9) and

         A2: f9 = (b * ( canFS ( support b))) by UPROOTS:def 3;

        ( rng f9) c= NAT by A2, ORDINAL1:def 12;

        then

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

        ( Sum f9) is Element of NAT ;

        hence thesis by A1;

      end;

    end

    theorem :: NAT_5:24

    

     Th24: for f be sequence of NAT , F be sequence of REAL , J be finite Subset of NAT st f = F & (ex k st J c= ( Seg k)) holds ( Sum (f | J)) = ( Sum ( Func_Seq (F,( Sgm J))))

    proof

      let f be sequence of NAT ;

      let F be sequence of REAL ;

      let J be finite Subset of NAT ;

      assume

       A1: f = F;

      reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;

      assume

       A2: ex k st J c= ( Seg k);

      reconsider f9 = (f | J9) as bag of J;

      

       A3: ( dom f) = NAT by FUNCT_2:def 1;

      then

       A4: J = ( dom (f | J9)) by RELAT_1: 62;

      ( support f9) c= J9;

      then

      consider fs be FinSequence of REAL such that

       A5: fs = (f9 * ( canFS J9)) and

       A6: ( Sum f9) = ( Sum fs) by UPROOTS: 14;

      

       A7: ( rng ( canFS J)) = J by FUNCT_2:def 3

      .= ( dom f9) by A3, RELAT_1: 62;

      then ( dom ( canFS J)) = ( dom fs) by A5, RELAT_1: 27;

      then

       A8: (fs,f9) are_fiberwise_equipotent by A5, A7, CLASSES1: 77;

      

       A9: ( Sgm J) is one-to-one by A2, FINSEQ_3: 92;

      ( rng ( Sgm J)) = J by A2, FINSEQ_1:def 13;

      

      then

       A10: (f * ( Sgm J)) = (f * (J |` ( Sgm J)))

      .= ((f | J) * ( Sgm J)) by MONOID_1: 1;

      

       A11: ( rng ( Sgm J)) = ( dom (f | J)) by A2, A4, FINSEQ_1:def 13;

      then ( dom ( Sgm J)) = ( dom ((f | J) * ( Sgm J))) by RELAT_1: 27;

      then (((f | J) * ( Sgm J)),(f | J)) are_fiberwise_equipotent by A11, A9, CLASSES1: 77;

      then (( Func_Seq (F,( Sgm J))),(f | J)) are_fiberwise_equipotent by A1, A10, BHSP_5:def 4;

      hence ( Sum (f | J)) = ( Sum ( Func_Seq (F,( Sgm J)))) by A6, A8, CLASSES1: 76, RFINSEQ: 9;

    end;

    theorem :: NAT_5:25

    

     Th25: for I be non empty set, F be PartFunc of I, REAL , f be Function of I, NAT , J be finite Subset of I st f = F holds ( Sum (f | J)) = ( Sum (F,J))

    proof

      let I be non empty set;

      let F be PartFunc of I, REAL ;

      let f be Function of I, NAT ;

      let J be finite Subset of I;

      reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;

      reconsider f9 = (f | J9) as bag of J;

      

       A1: ( dom (F | J)) is finite;

      assume f = F;

      then

       A2: ((f | J),( FinS (F,J))) are_fiberwise_equipotent by A1, RFUNCT_3:def 13;

      

       A3: ( dom f) = I by FUNCT_2:def 1;

      ( support f9) c= J9;

      then

      consider fs be FinSequence of REAL such that

       A4: fs = (f9 * ( canFS J9)) and

       A5: ( Sum f9) = ( Sum fs) by UPROOTS: 14;

      

       A6: ( rng ( canFS J)) = J by FUNCT_2:def 3

      .= ( dom f9) by A3, RELAT_1: 62;

      then ( dom ( canFS J)) = ( dom fs) by A4, RELAT_1: 27;

      then (fs,f9) are_fiberwise_equipotent by A4, A6, CLASSES1: 77;

      then ( Sum fs) = ( Sum ( FinS (F,J))) by A2, CLASSES1: 76, RFINSEQ: 9;

      hence ( Sum (f | J)) = ( Sum (F,J)) by A5, RFUNCT_3:def 14;

    end;

    reserve I,j for set;

    reserve f,g for Function of I, NAT ;

    reserve J,K for finite Subset of I;

    theorem :: NAT_5:26

    

     Th26: J misses K implies ( Sum (f | (J \/ K))) = (( Sum (f | J)) + ( Sum (f | K)))

    proof

      assume

       A1: J misses K;

      per cases ;

        suppose

         A2: I is empty;

        set b = ( EmptyBag {} );

        

         A3: ( Sum b) = 0 by UPROOTS: 11;

        J = {} & (f | J) = {} by A2;

        hence ( Sum (f | (J \/ K))) = (( Sum (f | J)) + ( Sum (f | K))) by A3;

      end;

        suppose I is non empty;

        then

        reconsider I9 = I as non empty set;

         [:I9, NAT :] c= [:I9, REAL :] by ZFMISC_1: 95, NUMBERS: 19;

        then

        reconsider F = f as PartFunc of I9, REAL by XBOOLE_1: 1;

        

         A4: ( dom (F | (J \/ K))) is finite;

        

        thus ( Sum (f | (J \/ K))) = ( Sum (F,(J \/ K))) by Th25

        .= (( Sum (F,J)) + ( Sum (F,K))) by A1, A4, RFUNCT_3: 83

        .= (( Sum (f | J)) + ( Sum (F,K))) by Th25

        .= (( Sum (f | J)) + ( Sum (f | K))) by Th25;

      end;

    end;

    theorem :: NAT_5:27

    

     Th27: for j be object holds J = {j} implies ( Sum (f | J)) = (f . j)

    proof

      let j be object;

      consider f9 be FinSequence of REAL such that

       A1: ( Sum (f | J)) = ( Sum f9) and

       A2: f9 = ((f | J) * ( canFS ( support (f | J)))) by UPROOTS:def 3;

      assume

       A3: J = {j};

      then

       A4: j in J by TARSKI:def 1;

      then j in I;

      then j in ( dom f) by FUNCT_2:def 1;

      then J c= ( dom f) by A3, ZFMISC_1: 31;

      then

       A5: ( dom (f | J)) = J by RELAT_1: 62;

      per cases by A3, ZFMISC_1: 33;

        suppose

         A6: ( support (f | J)) = {} ;

        now

          assume (f . j) <> 0 ;

          then ((f | J) . j) <> 0 by A4, FUNCT_1: 49;

          hence contradiction by A6, PRE_POLY:def 7;

        end;

        hence ( Sum (f | J)) = (f . j) by A1, A2, A6, RVSUM_1: 72;

      end;

        suppose ( support (f | J)) = J;

        then ( canFS ( support (f | J))) = <*j*> by A3, FINSEQ_1: 94;

        then f9 = <*((f | J) . j)*> by A4, A5, A2, FINSEQ_2: 34;

        then f9 = <*(f . j)*> by A4, FUNCT_1: 49;

        hence ( Sum (f | J)) = (f . j) by A1, RVSUM_1: 73;

      end;

    end;

    

     Lm11: for j be object holds J = {j} implies ( Sum (( multnat * [:f, g:]) | [:J, K:])) = ((f . j) * ( Sum (g | K)))

    proof

      let j be object;

      defpred P[ Nat] means for I be set, j be object, f,g be Function of I, NAT , J,K be finite Subset of I st J = {j} & $1 = ( card K) holds ( Sum (( multnat * [:f, g:]) | [:J, K:])) = ((f . j) * ( Sum (g | K)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds P[n];

        thus P[k]

        proof

          k = 0 or (k + 1) > ( 0 + 1) by XREAL_1: 8;

          then

           A3: k = 0 or k >= 1 by NAT_1: 13;

          let I be set, j be object;

          let f,g be Function of I, NAT ;

          let J,K be finite Subset of I;

          assume

           A4: J = {j};

          assume

           A5: k = ( card K);

          per cases by A3, XXREAL_0: 1;

            suppose

             A6: k = 0 ;

            set b = ( EmptyBag {} );

            

             A7: ( Sum b) = 0 by UPROOTS: 11;

            

             A8: K = {} by A5, A6;

            then (g | K) = {} & [:J, K:] = {} ;

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = ((f . j) * ( Sum (g | K))) by A8, A7;

          end;

            suppose

             A9: k = 1;

            set x = the set;

            ( card {x}) = ( card K) by A5, A9, CARD_1: 30;

            then

            consider k9 be object such that

             A10: K = {k9} by CARD_1: 29;

            set b = (( multnat * [:f, g:]) | [:J, K:]);

            consider f9 be FinSequence of REAL such that

             A11: ( Sum b) = ( Sum f9) and

             A12: f9 = (b * ( canFS ( support b))) by UPROOTS:def 3;

            

             A13: [:J, K:] = { [j, k9]} by A4, A10, ZFMISC_1: 29;

            then

             A14: [j, k9] in [:J, K:] by TARSKI:def 1;

            then [j, k9] in [:I, I:];

            then

             A15: [j, k9] in ( dom ( multnat * [:f, g:])) by FUNCT_2:def 1;

            then [:J, K:] c= ( dom ( multnat * [:f, g:])) by A13, ZFMISC_1: 31;

            then

             A16: ( dom b) = [:J, K:] by RELAT_1: 62;

            ( Sum b) = ((f . j) * (g . k9))

            proof

              reconsider I9 = I as non empty set by A4;

              reconsider j99 = j, k99 = k9 as Element of I9 by A4, A10, ZFMISC_1: 31;

              set n1 = (f . j), n2 = (g . k9);

              

               A17: ((f . j) * (g . k9)) = ( multnat . (n1,n2)) by BINOP_2:def 24

              .= ( multnat . [(f . j99), (g . k99)]) by BINOP_1:def 1

              .= ( multnat . ( [:f, g:] . (j99,k99))) by FUNCT_3: 75

              .= ( multnat . ( [:f, g:] . [j, k9])) by BINOP_1:def 1

              .= (( multnat * [:f, g:]) . [j, k9]) by A15, FUNCT_1: 12

              .= (b . [j, k9]) by A14, FUNCT_1: 49;

              per cases by A13, ZFMISC_1: 33;

                suppose

                 A18: ( support b) = {} ;

                then ((f . j) * (g . k9)) = 0 by A17, PRE_POLY:def 7;

                hence ( Sum b) = ((f . j) * (g . k9)) by A11, A12, A18, RVSUM_1: 72;

              end;

                suppose ( support b) = { [j, k9]};

                then ( canFS ( support b)) = <* [j, k9]*> by FINSEQ_1: 94;

                then f9 = <*(b . [j, k9])*> by A12, A14, A16, FINSEQ_2: 34;

                hence ( Sum b) = ((f . j) * (g . k9)) by A11, A17, RVSUM_1: 73;

              end;

            end;

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = ((f . j) * ( Sum (g | K))) by A10, Th27;

          end;

            suppose

             A19: k > 1;

            then K <> {} by A5;

            then

            consider k9 be object such that

             A20: k9 in K by XBOOLE_0:def 1;

            set K0 = {k9};

            set K1 = (K \ K0);

            reconsider K0 as finite Subset of I by A20, ZFMISC_1: 31;

            ( card K0) < k by A19, CARD_1: 30;

            then

             A21: (( - 1) + k) < ( 0 + k) & ( Sum (( multnat * [:f, g:]) | [:J, K0:])) = ((f . j) * ( Sum (g | K0))) by A2, A4, XREAL_1: 8;

            K1 misses K0 by XBOOLE_1: 79;

            then

             A22: [:J, K1:] misses [:J, K0:] by ZFMISC_1: 104;

            k9 in K0 by TARSKI:def 1;

            then not k9 in K1 by XBOOLE_0:def 5;

            then

             A23: ( card (K1 \/ K0)) = (( card K1) + 1) by CARD_2: 41;

            

             A24: (K1 \/ K0) = (K \/ {k9}) by XBOOLE_1: 39

            .= K by A20, ZFMISC_1: 40;

            then [:J, K:] = ( [:J, K1:] \/ [:J, K0:]) by ZFMISC_1: 97;

            

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (( multnat * [:f, g:]) | [:J, K1:])) + ( Sum (( multnat * [:f, g:]) | [:J, K0:]))) by A22, Th26

            .= (((f . j) * ( Sum (g | K1))) + ((f . j) * ( Sum (g | K0)))) by A2, A4, A5, A23, A24, A21

            .= ((f . j) * (( Sum (g | K1)) + ( Sum (g | K0))))

            .= ((f . j) * ( Sum (g | K))) by A24, Th26, XBOOLE_1: 79;

          end;

        end;

      end;

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

      then P[( card K)];

      hence thesis;

    end;

    theorem :: NAT_5:28

    

     Th28: ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (f | J)) * ( Sum (g | K)))

    proof

      defpred P[ Nat] means for I be set, f,g be Function of I, NAT , J,K be finite Subset of I st $1 = ( card J) holds ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (f | J)) * ( Sum (g | K)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds P[n];

        thus P[k]

        proof

          k = 0 or (k + 1) > ( 0 + 1) by XREAL_1: 8;

          then

           A3: k = 0 or k >= 1 by NAT_1: 13;

          let I be set;

          let f,g be Function of I, NAT ;

          let J,K be finite Subset of I;

          assume

           A4: k = ( card J);

          per cases by A3, XXREAL_0: 1;

            suppose k = 0 ;

            then

             A5: J = {} by A4;

            then

             A6: [:J, K:] = {} ;

            

             A7: ( EmptyBag {} ) = ( {} --> 0 )

            .= {} ;

            then ( Sum (f | J)) = 0 by A5, RELAT_1: 81, UPROOTS: 11;

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (f | J)) * ( Sum (g | K))) by A6, A7, RELAT_1: 81, UPROOTS: 11;

          end;

            suppose

             A8: k = 1;

            set x = the set;

            ( card {x}) = ( card J) by A4, A8, CARD_1: 30;

            then

            consider j be object such that

             A9: J = {j} by CARD_1: 29;

            ( Sum (( multnat * [:f, g:]) | [:J, K:])) = ((f . j) * ( Sum (g | K))) by A9, Lm11;

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (f | J)) * ( Sum (g | K))) by A9, Th27;

          end;

            suppose

             A10: k > 1;

            then J <> {} by A4;

            then

            consider j be object such that

             A11: j in J by XBOOLE_0:def 1;

            set J0 = {j};

            set J1 = (J \ J0);

            reconsider J0 as finite Subset of I by A11, ZFMISC_1: 31;

            

             A12: (J1 \/ J0) = (J \/ {j}) by XBOOLE_1: 39

            .= J by A11, ZFMISC_1: 40;

            then

             A13: ( Sum (f | J)) = (( Sum (f | J1)) + ( Sum (f | J0))) by Th26, XBOOLE_1: 79;

            ( card J0) < k by A10, CARD_1: 30;

            then

             A14: (( - 1) + k) < ( 0 + k) & ( Sum (( multnat * [:f, g:]) | [:J0, K:])) = (( Sum (f | J0)) * ( Sum (g | K))) by A2, XREAL_1: 8;

            J1 misses J0 by XBOOLE_1: 79;

            then

             A15: [:J1, K:] misses [:J0, K:] by ZFMISC_1: 104;

            j in J0 by TARSKI:def 1;

            then not j in J1 by XBOOLE_0:def 5;

            then

             A16: ( card (J1 \/ J0)) = (( card J1) + 1) by CARD_2: 41;

             [:J, K:] = ( [:J1, K:] \/ [:J0, K:]) by A12, ZFMISC_1: 97;

            

            hence ( Sum (( multnat * [:f, g:]) | [:J, K:])) = (( Sum (( multnat * [:f, g:]) | [:J1, K:])) + ( Sum (( multnat * [:f, g:]) | [:J0, K:]))) by A15, Th26

            .= ((( Sum (f | J1)) * ( Sum (g | K))) + (( Sum (f | J0)) * ( Sum (g | K)))) by A2, A4, A16, A12, A14

            .= (( Sum (f | J)) * ( Sum (g | K))) by A13;

          end;

        end;

      end;

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

      then P[( card J)];

      hence thesis;

    end;

    definition

      let k be natural Number;

      :: NAT_5:def1

      func EXP (k) -> sequence of NAT means

      : Def1: for n be Nat holds (it . n) = (n |^ k);

      existence

      proof

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

        deffunc F( Element of NAT ) = ($1 |^ k9);

        consider f be sequence of NAT such that

         A1: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        for n be Nat holds (f . n) = (n |^ k)

        proof

          let n be Nat;

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

          (f . n9) = F(n9) by A1;

          hence (f . n) = (n |^ k);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of NAT ;

        assume

         A2: for n be Nat holds (f1 . n) = (n |^ k);

        assume

         A3: for n be Nat holds (f2 . n) = (n |^ k);

        for x be object st x in NAT holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          (f1 . n) = (n |^ k) by A2

          .= (f2 . n) by A3;

          hence (f1 . x) = (f2 . x);

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    definition

      let k,n be natural Number;

      :: NAT_5:def2

      func sigma (k,n) -> Element of NAT means

      : Def2: for m be non zero Nat st n = m holds it = ( Sum (( EXP k) | ( NatDivisors m))) if n <> 0

      otherwise it = 0 ;

      correctness

      proof

        

         A1: for n1,n2 be Element of NAT holds ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2) & (n <> 0 & (for m be non zero Nat st n = m holds n1 = ( Sum (( EXP k) | ( NatDivisors m)))) & (for m be non zero Nat st n = m holds n2 = ( Sum (( EXP k) | ( NatDivisors m)))) implies n1 = n2)

        proof

          let n1,n2 be Element of NAT ;

          thus not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2;

          assume n <> 0 ;

          then

          reconsider m = n as non zero Nat by TARSKI: 1;

          assume for m be non zero Nat st n = m holds n1 = ( Sum (( EXP k) | ( NatDivisors m)));

          then n1 = ( Sum (( EXP k) | ( NatDivisors m)));

          hence thesis;

        end;

        n <> 0 implies ex n1 be Element of NAT st for m be non zero Nat st n = m holds n1 = ( Sum (( EXP k) | ( NatDivisors m)))

        proof

          assume n <> 0 ;

          then

          reconsider n9 = n as non zero Nat by TARSKI: 1;

          reconsider n1 = ( Sum (( EXP k) | ( NatDivisors n9))) as Element of NAT by ORDINAL1:def 12;

          take n1;

          thus thesis;

        end;

        hence thesis by A1;

      end;

    end

    definition

      let k be natural Number;

      :: NAT_5:def3

      func Sigma (k) -> sequence of NAT means

      : Def3: for n be Nat holds (it . n) = ( sigma (k,n));

      existence

      proof

        deffunc F( Element of NAT ) = ( sigma (k,$1));

        consider f be sequence of NAT such that

         A1: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take f;

        let n be Nat;

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

        

        thus (f . n) = (f . n9)

        .= ( sigma (k,n)) by A1;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of NAT ;

        assume

         A2: for n be Nat holds (f1 . n) = ( sigma (k,n));

        assume

         A3: for n be Nat holds (f2 . n) = ( sigma (k,n));

        for x be object st x in NAT holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          

          thus (f1 . x) = ( sigma (k,n)) by A2

          .= (f2 . x) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    definition

      let n be natural Number;

      :: NAT_5:def4

      func sigma n -> Element of NAT equals ( sigma (1,n));

      correctness ;

    end

    theorem :: NAT_5:29

    

     Th29: ( sigma (k,1)) = 1

    proof

      set b = (( EXP k) | ( NatDivisors 1));

      consider f be FinSequence of REAL such that

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

       A2: f = (b * ( canFS ( support b))) by UPROOTS:def 3;

      1 in NAT ;

      then

       A3: 1 in ( dom ( EXP k)) by FUNCT_2:def 1;

      1 in ( NatDivisors 1);

      then

       A4: 1 in ( dom b) by A3, RELAT_1: 57;

      

      then

       A5: (b . 1) = (( EXP k) . 1) by FUNCT_1: 47

      .= (1 |^ k) by Def1

      .= 1;

      then for x be object holds x in ( support b) iff x = 1 by MOEBIUS1: 41, TARSKI:def 1, PRE_POLY:def 7;

      then ( support b) = {1} by TARSKI:def 1;

      

      then f = (b * <*1*>) by A2, FINSEQ_1: 94

      .= <*(b . 1)*> by A4, FINSEQ_2: 34;

      then ( Sum b) = 1 by A5, A1, RVSUM_1: 73;

      hence ( sigma (k,1)) = 1 by Def2;

    end;

    theorem :: NAT_5:30

    

     Th30: p is prime implies ( sigma (p |^ n)) = (((p |^ (n + 1)) - 1) / (p - 1))

    proof

      defpred P[ Nat] means for p be Nat st p is prime holds ( sigma (p |^ $1)) = (((p |^ ($1 + 1)) - 1) / (p - 1));

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        thus P[(k + 1)]

        proof

          let p be Nat;

          reconsider k9 = (k + 1), p9 = p as Element of NAT by ORDINAL1:def 12;

          assume

           A3: p is prime;

          then

          reconsider J = ( NatDivisors (p |^ k)) as finite Subset of NAT ;

          reconsider m9 = (p |^ k) as non zero Nat by A3;

          

           A4: ( Sum (( EXP 1) | J)) = ( sigma (1,m9)) by Def2

          .= ( sigma (p |^ k))

          .= (((p |^ (k + 1)) - 1) / (p - 1)) by A2, A3;

          (p9 |^ k9) in NAT ;

          then

          reconsider K = {(p |^ (k + 1))} as finite Subset of NAT by ZFMISC_1: 31;

          

           A5: p > 1 by A3, INT_2:def 4;

          then

           A6: (p - 1) > (1 - 1) by XREAL_1: 14;

          now

            let x be object;

            assume

             A7: x in (J /\ K);

            then x in J by XBOOLE_0:def 4;

            then x in { (p |^ t) where t be Element of NAT : t <= k } by A3, Th19;

            then

            consider t be Element of NAT such that

             A8: x = (p |^ t) and

             A9: t <= k;

            x in K by A7, XBOOLE_0:def 4;

            then (p |^ (k + 1)) = (p |^ t) by A8, TARSKI:def 1;

            then (p |-count (p |^ (k + 1))) = t by A5, NAT_3: 25;

            then (k + 1) = t by A5, NAT_3: 25;

            then ((k + 1) - k) <= (k - k) by A9, XREAL_1: 9;

            then 1 <= 0 ;

            hence contradiction;

          end;

          then (J /\ K) = {} by XBOOLE_0:def 1;

          then

           A10: J misses K by XBOOLE_0:def 7;

          reconsider m = (p |^ (k + 1)) as non zero Nat by A3;

          

           A11: (( EXP 1) . (p |^ (k + 1))) = ((p |^ (k + 1)) |^ 1) by Def1

          .= (p |^ ((k + 1) * 1))

          .= (p |^ (k + 1));

          for x be object holds x in ( NatDivisors (p |^ (k + 1))) iff x in (( NatDivisors (p |^ k)) \/ {(p |^ (k + 1))})

          proof

            let x be object;

            hereby

              assume x in ( NatDivisors (p |^ (k + 1)));

              then x in { (p |^ t) where t be Element of NAT : t <= (k + 1) } by A3, Th19;

              then

              consider t be Element of NAT such that

               A12: x = (p |^ t) and

               A13: t <= (k + 1);

              per cases ;

                suppose t <= k;

                then x in { (p |^ t9) where t9 be Element of NAT : t9 <= k } by A12;

                then x in ( NatDivisors (p |^ k)) by A3, Th19;

                hence x in (( NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}) by XBOOLE_0:def 3;

              end;

                suppose t > k;

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

                then t = (k + 1) by A13, XXREAL_0: 1;

                then x in {(p |^ (k + 1))} by A12, TARSKI:def 1;

                hence x in (( NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}) by XBOOLE_0:def 3;

              end;

            end;

            assume

             A14: x in (( NatDivisors (p |^ k)) \/ {(p |^ (k + 1))});

            per cases by A14, XBOOLE_0:def 3;

              suppose x in ( NatDivisors (p |^ k));

              then x in { (p |^ t) where t be Element of NAT : t <= k } by A3, Th19;

              then

              consider t be Element of NAT such that

               A15: x = (p |^ t) and

               A16: t <= k;

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

              then t <= (k + 1) by A16, XXREAL_0: 2;

              then x in { (p |^ t9) where t9 be Element of NAT : t9 <= (k + 1) } by A15;

              hence x in ( NatDivisors (p |^ (k + 1))) by A3, Th19;

            end;

              suppose x in {(p |^ (k + 1))};

              then x = (p |^ k9) by TARSKI:def 1;

              then x in { (p |^ t) where t be Element of NAT : t <= (k + 1) };

              hence x in ( NatDivisors (p |^ (k + 1))) by A3, Th19;

            end;

          end;

          then ( NatDivisors (p |^ (k + 1))) = (( NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}) by TARSKI: 2;

          

          then ( sigma (1,m)) = ( Sum (( EXP 1) | (J \/ K))) by Def2

          .= (( Sum (( EXP 1) | J)) + ( Sum (( EXP 1) | K))) by A10, Th26

          .= (( Sum (( EXP 1) | J)) + (( EXP 1) . (p |^ (k + 1)))) by Th27;

          

          hence ( sigma (p |^ (k + 1))) = ((((p |^ (k + 1)) - 1) / (p - 1)) + (((p |^ (k + 1)) * (p - 1)) / (p - 1))) by A6, A11, A4, XCMPLX_1: 89

          .= ((((p |^ (k + 1)) - 1) + ((p |^ (k + 1)) * (p - 1))) / (p - 1)) by XCMPLX_1: 62

          .= ((((p |^ (k + 1)) * p) - 1) / (p - 1))

          .= (((p |^ ((k + 1) + 1)) - 1) / (p - 1)) by NEWTON: 6;

        end;

      end;

      

       A17: P[ 0 ]

      proof

        let p be Nat;

        assume p is prime;

        then p > 1 by INT_2:def 4;

        then

         A18: (p - 1) > (1 - 1) by XREAL_1: 14;

        

        thus ( sigma (p |^ 0 )) = ( sigma 1) by NEWTON: 4

        .= 1 by Th29

        .= ((p - 1) / (p - 1)) by A18, XCMPLX_1: 60

        .= (((p |^ ( 0 + 1)) - 1) / (p - 1));

      end;

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

      hence thesis;

    end;

    theorem :: NAT_5:31

    

     Th31: m divides n0 & n0 <> m & m <> 1 implies ((1 + m) + n0) <= ( sigma n0)

    proof

      assume

       A1: m divides n0;

      assume

       A2: n0 <> m;

      assume

       A3: m <> 1;

      per cases ;

        suppose n0 = 1;

        hence thesis by A1, A2, WSIERP_1: 15;

      end;

        suppose

         A4: n0 <> 1;

        reconsider X2 = {m, n0} as finite Subset of NAT by Th5;

        set X1 = {1};

        now

          let x be object;

          assume

           A5: x in (X1 /\ X2);

          then x in X1 by XBOOLE_0:def 4;

          then

           A6: x = 1 by TARSKI:def 1;

          x in X2 by A5, XBOOLE_0:def 4;

          hence contradiction by A3, A4, A6, TARSKI:def 2;

        end;

        then (X1 /\ X2) = {} by XBOOLE_0:def 1;

        then

         A7: X1 misses X2 by XBOOLE_0:def 7;

        reconsider X4 = {n0} as finite Subset of NAT by Th4;

        reconsider X3 = {m} as finite Subset of NAT by Th4;

        reconsider X = {1, m, n0} as finite Subset of NAT by Lm2;

        set Y = (( NatDivisors n0) \ X);

        

         A8: ( 0 + ( Sum (( EXP 1) | X))) <= (( Sum (( EXP 1) | Y)) + ( Sum (( EXP 1) | X))) by XREAL_1: 7;

        for x be object st x in X holds x in ( NatDivisors n0)

        proof

          let x be object;

          assume

           A9: x in X;

          then

          reconsider x9 = x as Element of NAT ;

          x = 1 or x = m or x = n0 by A9, ENUMSET1:def 1;

          then x9 <> 0 & x9 divides n0 by A1, INT_2: 3, NAT_D: 6;

          hence x in ( NatDivisors n0);

        end;

        then X c= ( NatDivisors n0);

        then ( NatDivisors n0) = (X \/ Y) by XBOOLE_1: 45;

        

        then

         A10: ( sigma n0) = ( Sum (( EXP 1) | (X \/ Y))) by Def2

        .= (( Sum (( EXP 1) | X)) + ( Sum (( EXP 1) | Y))) by Th26, XBOOLE_1: 79;

        now

          let x be object;

          assume

           A11: x in (X3 /\ X4);

          then x in X3 by XBOOLE_0:def 4;

          then

           A12: x = m by TARSKI:def 1;

          x in X4 by A11, XBOOLE_0:def 4;

          hence contradiction by A2, A12, TARSKI:def 1;

        end;

        then (X3 /\ X4) = {} by XBOOLE_0:def 1;

        then

         A13: X2 = (X3 \/ X4) & X3 misses X4 by ENUMSET1: 1, XBOOLE_0:def 7;

        X = (X1 \/ X2) by ENUMSET1: 2;

        

        then ( Sum (( EXP 1) | X)) = (( Sum (( EXP 1) | X1)) + ( Sum (( EXP 1) | X2))) by A7, Th26

        .= ((( EXP 1) . 1) + ( Sum (( EXP 1) | X2))) by Th27

        .= ((( EXP 1) . 1) + (( Sum (( EXP 1) | X3)) + ( Sum (( EXP 1) | X4)))) by A13, Th26

        .= ((( EXP 1) . 1) + ((( EXP 1) . m) + ( Sum (( EXP 1) | X4)))) by Th27

        .= (((( EXP 1) . 1) + (( EXP 1) . m)) + ( Sum (( EXP 1) | X4)))

        .= (((( EXP 1) . 1) + (( EXP 1) . m)) + (( EXP 1) . n0)) by Th27

        .= (((1 |^ 1) + (( EXP 1) . m)) + (( EXP 1) . n0)) by Def1

        .= (((1 |^ 1) + (m |^ 1)) + (( EXP 1) . n0)) by Def1

        .= (((1 |^ 1) + (m |^ 1)) + (n0 |^ 1)) by Def1

        .= ((1 + (m |^ 1)) + (n0 |^ 1))

        .= ((1 + m) + (n0 |^ 1))

        .= ((1 + m) + n0);

        hence ((1 + m) + n0) <= ( sigma n0) by A10, A8;

      end;

    end;

    theorem :: NAT_5:32

    

     Th32: m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k implies (((1 + m) + k) + n0) <= ( sigma n0)

    proof

      assume that

       A1: m divides n0 and

       A2: k divides n0 and

       A3: n0 <> m and

       A4: n0 <> k and

       A5: m <> 1 and

       A6: k <> 1 and

       A7: m <> k;

      per cases ;

        suppose n0 = 1;

        hence thesis by A1, A3, WSIERP_1: 15;

      end;

        suppose

         A8: n0 <> 1;

        reconsider X2 = {m, k, n0} as finite Subset of NAT by Lm2;

        set X1 = {1};

        now

          let x be object;

          assume

           A9: x in (X1 /\ X2);

          then x in X1 by XBOOLE_0:def 4;

          then

           A10: x = 1 by TARSKI:def 1;

          x in X2 by A9, XBOOLE_0:def 4;

          hence contradiction by A5, A6, A8, A10, ENUMSET1:def 1;

        end;

        then (X1 /\ X2) = {} by XBOOLE_0:def 1;

        then

         A11: X1 misses X2 by XBOOLE_0:def 7;

        reconsider X5 = {m} as finite Subset of NAT by Th4;

        reconsider X4 = {n0} as finite Subset of NAT by Th4;

        reconsider X6 = {k} as finite Subset of NAT by Th4;

        reconsider X3 = {m, k} as finite Subset of NAT by Th5;

        reconsider X = {1, m, k, n0} as finite Subset of NAT by Lm3;

        set Y = (( NatDivisors n0) \ X);

        

         A12: ( 0 + ( Sum (( EXP 1) | X))) <= (( Sum (( EXP 1) | Y)) + ( Sum (( EXP 1) | X))) by XREAL_1: 7;

        now

          let x be object;

          assume

           A13: x in (X5 /\ X6);

          then x in X5 by XBOOLE_0:def 4;

          then

           A14: x = m by TARSKI:def 1;

          x in X6 by A13, XBOOLE_0:def 4;

          hence contradiction by A7, A14, TARSKI:def 1;

        end;

        then (X5 /\ X6) = {} by XBOOLE_0:def 1;

        then

         A15: X3 = (X5 \/ X6) & X5 misses X6 by ENUMSET1: 1, XBOOLE_0:def 7;

        for x be object st x in X holds x in ( NatDivisors n0)

        proof

          let x be object;

          assume

           A16: x in X;

          then

          reconsider x9 = x as Element of NAT ;

          x = 1 or x = m or x = k or x = n0 by A16, ENUMSET1:def 2;

          then x9 <> 0 & x9 divides n0 by A1, A2, INT_2: 3, NAT_D: 6;

          hence x in ( NatDivisors n0);

        end;

        then X c= ( NatDivisors n0);

        then ( NatDivisors n0) = (X \/ Y) by XBOOLE_1: 45;

        

        then

         A17: ( sigma n0) = ( Sum (( EXP 1) | (X \/ Y))) by Def2

        .= (( Sum (( EXP 1) | X)) + ( Sum (( EXP 1) | Y))) by Th26, XBOOLE_1: 79;

        now

          let x be object;

          assume

           A18: x in (X3 /\ X4);

          then x in X4 by XBOOLE_0:def 4;

          then

           A19: x = n0 by TARSKI:def 1;

          x in X3 by A18, XBOOLE_0:def 4;

          hence contradiction by A3, A4, A19, TARSKI:def 2;

        end;

        then (X3 /\ X4) = {} by XBOOLE_0:def 1;

        then

         A20: X2 = (X3 \/ X4) & X3 misses X4 by ENUMSET1: 3, XBOOLE_0:def 7;

        X = (X1 \/ X2) by ENUMSET1: 4;

        

        then ( Sum (( EXP 1) | X)) = (( Sum (( EXP 1) | X1)) + ( Sum (( EXP 1) | X2))) by A11, Th26

        .= ((( EXP 1) . 1) + ( Sum (( EXP 1) | X2))) by Th27

        .= ((( EXP 1) . 1) + (( Sum (( EXP 1) | X3)) + ( Sum (( EXP 1) | X4)))) by A20, Th26

        .= ((( EXP 1) . 1) + ((( Sum (( EXP 1) | X5)) + ( Sum (( EXP 1) | X6))) + ( Sum (( EXP 1) | X4)))) by A15, Th26

        .= ((( EXP 1) . 1) + (((( EXP 1) . m) + ( Sum (( EXP 1) | X6))) + ( Sum (( EXP 1) | X4)))) by Th27

        .= (((( EXP 1) . 1) + (( EXP 1) . m)) + (( Sum (( EXP 1) | X6)) + ( Sum (( EXP 1) | X4))))

        .= (((( EXP 1) . 1) + (( EXP 1) . m)) + ((( EXP 1) . k) + ( Sum (( EXP 1) | X4)))) by Th27

        .= ((((( EXP 1) . 1) + (( EXP 1) . m)) + (( EXP 1) . k)) + ( Sum (( EXP 1) | X4)))

        .= ((((( EXP 1) . 1) + (( EXP 1) . m)) + (( EXP 1) . k)) + (( EXP 1) . n0)) by Th27

        .= ((((1 |^ 1) + (( EXP 1) . m)) + (( EXP 1) . k)) + (( EXP 1) . n0)) by Def1

        .= ((((1 |^ 1) + (m |^ 1)) + (( EXP 1) . k)) + (( EXP 1) . n0)) by Def1

        .= ((((1 |^ 1) + (m |^ 1)) + (k |^ 1)) + (( EXP 1) . n0)) by Def1

        .= ((((1 |^ 1) + (m |^ 1)) + (k |^ 1)) + (n0 |^ 1)) by Def1

        .= (((1 + (m |^ 1)) + (k |^ 1)) + (n0 |^ 1))

        .= (((1 + m) + (k |^ 1)) + (n0 |^ 1))

        .= (((1 + m) + k) + (n0 |^ 1))

        .= (((1 + m) + k) + n0);

        hence (((1 + m) + k) + n0) <= ( sigma n0) by A17, A12;

      end;

    end;

    theorem :: NAT_5:33

    

     Th33: ( sigma n0) = (n0 + m) & m divides n0 & n0 <> m implies m = 1 & n0 is prime

    proof

      assume

       A1: ( sigma n0) = (n0 + m);

      assume

       A2: m divides n0;

      assume

       A3: n0 <> m;

      per cases ;

        suppose n0 = 1;

        then 1 = (1 + m) by A1, Th29;

        hence thesis by A2, INT_2: 3;

      end;

        suppose

         A4: n0 <> 1;

        consider k be Nat such that

         A5: n0 = (m * k) by A2, NAT_D:def 3;

        

         A6: k <> m

        proof

          assume k = m;

          then m <> 1 by A4, A5;

          then ((1 + m) + n0) <= ( sigma n0) by A2, A3, Th31;

          then (((1 + m) + n0) - (m + n0)) <= ((n0 + m) - (m + n0)) by A1, XREAL_1: 9;

          hence contradiction;

        end;

        k = n0

        proof

          

           A7: k divides n0 & k <> 1 by A3, A5, NAT_D:def 3;

          assume

           A8: k <> n0;

          then m <> 1 by A5;

          then (((1 + m) + k) + n0) <= ( sigma n0) by A2, A3, A6, A8, A7, Th32;

          then ((((1 + m) + k) + n0) - (m + n0)) <= ((n0 + m) - (m + n0)) by A1, XREAL_1: 9;

          then (1 + k) <= 0 ;

          hence contradiction;

        end;

        then (n0 / n0) = m by A5, XCMPLX_1: 89;

        hence

         A9: m = 1 by XCMPLX_1: 60;

        

         A10: for k be Nat holds not k divides n0 or k = 1 or k = n0

        proof

          let k be Nat;

          assume that

           A11: k divides n0 and

           A12: k <> 1;

          assume k <> n0;

          then ((1 + k) + n0) <= (n0 + 1) by A1, A9, A11, A12, Th31;

          then (((1 + k) + n0) - (1 + n0)) <= ((n0 + 1) - (1 + n0)) by XREAL_1: 9;

          then k = 0 ;

          hence contradiction by A11, INT_2: 3;

        end;

        n0 > 1 by A4, NAT_1: 25;

        hence n0 is prime by A10, INT_2:def 4;

      end;

    end;

    definition

      let f be sequence of NAT ;

      :: NAT_5:def5

      attr f is multiplicative means for n0,m0 be non zero Nat st (n0,m0) are_coprime holds (f . (n0 * m0)) = ((f . n0) * (f . m0));

    end

    theorem :: NAT_5:34

    

     Th34: for f,F be sequence of NAT st f is multiplicative & (for n0 holds (F . n0) = ( Sum (f | ( NatDivisors n0)))) holds F is multiplicative

    proof

      let f,F be sequence of NAT ;

      assume

       A1: f is multiplicative;

      assume

       A2: for n0 holds (F . n0) = ( Sum (f | ( NatDivisors n0)));

      for n,m be non zero Nat st (n,m) are_coprime holds (F . (n * m)) = ((F . n) * (F . m))

      proof

        let n,m be non zero Nat;

        set b1 = (f | ( NatDivisors (n * m)));

        set b2 = (( multnat * [:f, f:]) | [:( NatDivisors n), ( NatDivisors m):]);

        consider f1 be FinSequence of REAL such that

         A3: ( Sum b1) = ( Sum f1) and

         A4: f1 = (b1 * ( canFS ( support b1))) by UPROOTS:def 3;

        set h9 = ( multnat | [:( NatDivisors n), ( NatDivisors m):]);

        set g2 = ( canFS ( support b2));

        set g1 = ( canFS ( support b1));

        consider f2 be FinSequence of REAL such that

         A5: ( Sum b2) = ( Sum f2) and

         A6: f2 = (b2 * ( canFS ( support b2))) by UPROOTS:def 3;

        ( dom multnat ) = [: NAT , NAT :] by FUNCT_2:def 1;

        then

         A7: ( dom h9) = [:( NatDivisors n), ( NatDivisors m):] by RELAT_1: 62;

        assume

         A8: (n,m) are_coprime ;

        for x1,x2 be object st x1 in ( dom h9) & x2 in ( dom h9) & (h9 . x1) = (h9 . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A9: x1 in ( dom h9);

          then

          consider n1,m1 be object such that

           A10: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) and

           A11: x1 = [n1, m1] by ZFMISC_1:def 2;

          reconsider n1, m1 as Element of NAT by A10;

          

           A12: (h9 . x1) = ( multnat . x1) by A9, FUNCT_1: 47

          .= ( multnat . (n1,m1)) by A11, BINOP_1:def 1

          .= (n1 * m1) by BINOP_2:def 24;

          assume

           A13: x2 in ( dom h9);

          then

          consider n2,m2 be object such that

           A14: n2 in ( NatDivisors n) and

           A15: m2 in ( NatDivisors m) and

           A16: x2 = [n2, m2] by ZFMISC_1:def 2;

          reconsider n2, m2 as Element of NAT by A14, A15;

          assume

           A17: (h9 . x1) = (h9 . x2);

          

           A18: (h9 . x2) = ( multnat . x2) by A13, FUNCT_1: 47

          .= ( multnat . (n2,m2)) by A16, BINOP_1:def 1

          .= (n2 * m2) by BINOP_2:def 24;

          then n1 = n2 by A8, A10, A14, A15, A17, A12, Th15;

          hence x1 = x2 by A8, A10, A11, A15, A16, A17, A12, A18, Th15;

        end;

        then

        reconsider h9 as one-to-one Function by FUNCT_1:def 4;

        set h = (((g1 " ) * h9) * g2);

        

         A19: ( support b2) c= ( dom b2) by PRE_POLY: 37;

        

         A20: ( dom [:f, f:]) = [: NAT , NAT :] by FUNCT_2:def 1;

        for x be object st x in ( support b2) holds x in ( dom ((g1 " ) * h9))

        proof

          let x be object;

          

           A21: ( rng g1) = ( support b1) by FUNCT_2:def 3;

          assume

           A22: x in ( support b2);

          then

           A23: (b2 . x) <> 0 by PRE_POLY:def 7;

          

           A24: x in [:( NatDivisors n), ( NatDivisors m):] by A22;

          consider n1,m1 be object such that

           A25: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) and

           A26: x = [n1, m1] by A22, ZFMISC_1:def 2;

          reconsider n1, m1 as Element of NAT by A25;

          

           A27: (n1,m1) are_coprime by A8, A25, Th14;

          reconsider n19 = n1, m19 = m1 as non zero Nat by A25;

          set x9 = ((g1 " ) . (n1 * m1));

          set fn1 = (f . n1), fm1 = (f . m1);

          (b2 . x) = (( multnat * [:f, f:]) . x) by A22, FUNCT_1: 49

          .= ( multnat . ( [:f, f:] . x)) by A20, A24, FUNCT_1: 13

          .= ( multnat . ( [:f, f:] . (n1,m1))) by A26, BINOP_1:def 1

          .= ( multnat . [(f . n1), (f . m1)]) by FUNCT_3: 75

          .= ( multnat . ((f . n1),(f . m1))) by BINOP_1:def 1

          .= (fn1 * fm1) by BINOP_2:def 24

          .= (f . (n19 * m19)) by A1, A27

          .= ((f | ( NatDivisors (n * m))) . (n1 * m1)) by A25, Th16, FUNCT_1: 49;

          then

           A28: (n1 * m1) in ( rng g1) by A23, A21, PRE_POLY:def 7;

          then (n1 * m1) in ( dom (g1 " )) by FUNCT_1: 33;

          then x9 in ( rng (g1 " )) by FUNCT_1: 3;

          then

           A29: x9 in ( dom g1) by FUNCT_1: 33;

          (g1 . x9) = (n1 * m1) by A28, FUNCT_1: 35

          .= ( multnat . (n1,m1)) by BINOP_2:def 24

          .= ( multnat . [n1, m1]) by BINOP_1:def 1

          .= (h9 . x) by A22, A26, FUNCT_1: 49;

          then (h9 . x) in ( rng g1) by A29, FUNCT_1:def 3;

          then (h9 . x) in ( dom (g1 " )) by FUNCT_1: 33;

          hence x in ( dom ((g1 " ) * h9)) by A7, A22, FUNCT_1: 11;

        end;

        then ( support b2) c= ( dom ((g1 " ) * h9));

        then ( rng g2) c= ( dom ((g1 " ) * h9));

        then

         A30: ( dom (((g1 " ) * h9) * g2)) = ( dom g2) by RELAT_1: 27;

        ( rng g2) c= ( dom b2) by A19;

        then

         A31: ( dom h) = ( dom f2) by A6, A30, RELAT_1: 27;

        

         A32: for x be object st x in ( dom f2) holds (f2 . x) = (f1 . (h . x))

        proof

          let x be object;

          set x9 = (g2 . x);

          

           A33: ((b1 * g1) * ((g1 " ) * h9)) = (((b1 * g1) * (g1 " )) * h9) by RELAT_1: 36

          .= ((b1 * (g1 * (g1 " ))) * h9) by RELAT_1: 36

          .= ((b1 * ( id ( rng g1))) * h9) by FUNCT_1: 39

          .= ((b1 * ( id ( support b1))) * h9) by FUNCT_2:def 3;

          assume

           A34: x in ( dom f2);

          then

           A35: x in ( dom g2) by A6, FUNCT_1: 11;

          then

           A36: x9 in ( rng g2) by FUNCT_1: 3;

          then

           A37: ( support b2) c= ( dom b2) & x9 in ( support b2) by PRE_POLY: 37;

          then

          consider n1,m1 be object such that

           A38: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) and

           A39: x9 = [n1, m1] by ZFMISC_1:def 2;

          reconsider n1, m1 as Element of NAT by A38;

          

           A40: (n1,m1) are_coprime by A8, A38, Th14;

          reconsider n19 = n1, m19 = m1 as non zero Nat by A38;

          set fn1 = (f . n1), fm1 = (f . m1);

          

           A41: x9 in [:( NatDivisors n), ( NatDivisors m):] by A37;

          

           A42: (b2 . x9) = (( multnat * [:f, f:]) . x9) by A37, FUNCT_1: 49

          .= ( multnat . ( [:f, f:] . x9)) by A20, A41, FUNCT_1: 13

          .= ( multnat . ( [:f, f:] . (n1,m1))) by A39, BINOP_1:def 1

          .= ( multnat . [(f . n1), (f . m1)]) by FUNCT_3: 75

          .= ( multnat . ((f . n1),(f . m1))) by BINOP_1:def 1

          .= (fn1 * fm1) by BINOP_2:def 24

          .= (f . (n19 * m19)) by A1, A40;

          

           A43: (b2 . x9) <> 0 by A36, PRE_POLY:def 7;

          (f . (n19 * m19)) = ((f | ( NatDivisors (n * m))) . (n1 * m1)) by A38, Th16, FUNCT_1: 49;

          then

           A44: (n1 * m1) in ( support b1) by A43, A42, PRE_POLY:def 7;

          then

           A45: (n1 * m1) in ( dom ( id ( support b1)));

          

           A46: (h9 . x9) = ( multnat . x9) by A7, A37, FUNCT_1: 47

          .= ( multnat . (n1,m1)) by A39, BINOP_1:def 1

          .= (n1 * m1) by BINOP_2:def 24;

          

           A47: ((b1 * g1) . (h . x)) = (((b1 * g1) * h) . x) by A31, A34, FUNCT_1: 13

          .= ((((b1 * g1) * ((g1 " ) * h9)) * g2) . x) by RELAT_1: 36

          .= (((b1 * g1) * ((g1 " ) * h9)) . (g2 . x)) by A35, FUNCT_1: 13;

          (((b1 * ( id ( support b1))) * h9) . x9) = ((b1 * ( id ( support b1))) . (h9 . x9)) by A7, A37, FUNCT_1: 13

          .= (b1 . (( id ( support b1)) . (n1 * m1))) by A45, A46, FUNCT_1: 13

          .= (b1 . (n1 * m1)) by A44, FUNCT_1: 18

          .= (b2 . x9) by A38, A42, Th16, FUNCT_1: 49;

          hence (f2 . x) = (f1 . (h . x)) by A4, A6, A35, A47, A33, FUNCT_1: 13;

        end;

        for y be object st y in ( rng g1) holds y in ( rng (h9 * g2))

        proof

          let y be object;

          assume y in ( rng g1);

          then

           A48: y in ( support b1) by FUNCT_2:def 3;

          consider n1,m1 be Nat such that

           A49: n1 in ( NatDivisors n) & m1 in ( NatDivisors m) and

           A50: y = (n1 * m1) by A8, A48, Th18;

          reconsider n19 = n1, m19 = m1 as non zero Nat by A49;

          reconsider n1, m1 as Element of NAT by ORDINAL1:def 12;

          

           A51: (n1,m1) are_coprime by A8, A49, Th14;

          

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

          

           A53: [n1, m1] in [:( NatDivisors n), ( NatDivisors m):] by A49, ZFMISC_1:def 2;

          set x = ((g2 " ) . [n1, m1]);

          

           A54: [n1, m1] in [:( NatDivisors n), ( NatDivisors m):] by A49, ZFMISC_1:def 2;

          (b1 . y) = (f . y) by A48, FUNCT_1: 49

          .= ((f . n19) * (f . m19)) by A1, A50, A51

          .= ( multnat . ((f . n1),(f . m1))) by BINOP_2:def 24

          .= ( multnat . [(f . n1), (f . m1)]) by BINOP_1:def 1

          .= ( multnat . ( [:f, f:] . (n1,m1))) by FUNCT_3: 75

          .= ( multnat . ( [:f, f:] . [n1, m1])) by BINOP_1:def 1

          .= (( multnat * [:f, f:]) . [n1, m1]) by A20, FUNCT_1: 13

          .= (b2 . [n1, m1]) by A54, FUNCT_1: 49;

          then [n1, m1] in ( support b2) by A52, PRE_POLY:def 7;

          then

           A55: [n1, m1] in ( rng g2) by FUNCT_2:def 3;

          then [n1, m1] in ( dom (g2 " )) by FUNCT_1: 33;

          then x in ( rng (g2 " )) by FUNCT_1: 3;

          then

           A56: x in ( dom g2) by FUNCT_1: 33;

          

           A57: y = ( multnat . (n1,m1)) by A50, BINOP_2:def 24

          .= ( multnat . [n1, m1]) by BINOP_1:def 1

          .= (( multnat | [:( NatDivisors n), ( NatDivisors m):]) . [n1, m1]) by A53, FUNCT_1: 49

          .= (h9 . (g2 . ((g2 " ) . [n1, m1]))) by A55, FUNCT_1: 35

          .= ((h9 * g2) . x) by A56, FUNCT_1: 13;

          (g2 . ((g2 " ) . [n1, m1])) = [n1, m1] by A55, FUNCT_1: 35;

          then x in ( dom (h9 * g2)) by A7, A53, A56, FUNCT_1: 11;

          hence y in ( rng (h9 * g2)) by A57, FUNCT_1:def 3;

        end;

        then ( rng g1) c= ( rng (h9 * g2));

        then ( dom (g1 " )) c= ( rng (h9 * g2)) by FUNCT_1: 33;

        then ( rng ((g1 " ) * (h9 * g2))) = ( rng (g1 " )) by RELAT_1: 28;

        then

         A58: ( rng ((g1 " ) * (h9 * g2))) = ( dom g1) by FUNCT_1: 33;

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

        then ( rng g1) c= ( dom b1) by FUNCT_2:def 3;

        then ( dom (b1 * g1)) = ( dom g1) by RELAT_1: 27;

        then

         A59: ( rng h) = ( dom f1) by A4, A58, RELAT_1: 36;

        then for x be object holds x in ( dom f2) iff x in ( dom h) & (h . x) in ( dom f1) by A31, FUNCT_1: 3;

        then f2 = (f1 * h) by A32, FUNCT_1: 10;

        then

         A60: (f1,f2) are_fiberwise_equipotent by A31, A59, CLASSES1: 77;

        

        thus (F . (n * m)) = ( Sum (f | ( NatDivisors (n * m)))) by A2

        .= ( Sum (( multnat * [:f, f:]) | [:( NatDivisors n), ( NatDivisors m):])) by A3, A5, A60, RFINSEQ: 9

        .= (( Sum (f | ( NatDivisors n))) * ( Sum (f | ( NatDivisors m)))) by Th28

        .= (( Sum (f | ( NatDivisors n))) * (F . m)) by A2

        .= ((F . n) * (F . m)) by A2;

      end;

      hence F is multiplicative;

    end;

    theorem :: NAT_5:35

    

     Th35: ( EXP k) is multiplicative

    proof

      for n,m be non zero Nat st (n,m) are_coprime holds (( EXP k) . (n * m)) = ((( EXP k) . n) * (( EXP k) . m))

      proof

        let n,m be non zero Nat;

        assume (n,m) are_coprime ;

        

        thus (( EXP k) . (n * m)) = ((n * m) |^ k) by Def1

        .= ((n |^ k) * (m |^ k)) by NEWTON: 7

        .= ((( EXP k) . n) * (m |^ k)) by Def1

        .= ((( EXP k) . n) * (( EXP k) . m)) by Def1;

      end;

      hence ( EXP k) is multiplicative;

    end;

    theorem :: NAT_5:36

    

     Th36: ( Sigma k) is multiplicative

    proof

      for n be non zero Nat holds (( Sigma k) . n) = ( Sum (( EXP k) | ( NatDivisors n)))

      proof

        let n be non zero Nat;

        

        thus (( Sigma k) . n) = ( sigma (k,n)) by Def3

        .= ( Sum (( EXP k) | ( NatDivisors n))) by Def2;

      end;

      hence ( Sigma k) is multiplicative by Th34, Th35;

    end;

    theorem :: NAT_5:37

    

     Th37: (n0,m0) are_coprime implies ( sigma (n0 * m0)) = (( sigma n0) * ( sigma m0))

    proof

      assume

       A1: (n0,m0) are_coprime ;

      

       A2: ( Sigma 1) is multiplicative by Th36;

      

      thus ( sigma (n0 * m0)) = (( Sigma 1) . (n0 * m0)) by Def3

      .= ((( Sigma 1) . n0) * (( Sigma 1) . m0)) by A1, A2

      .= (( sigma (1,n0)) * (( Sigma 1) . m0)) by Def3

      .= (( sigma n0) * ( sigma m0)) by Def3;

    end;

    begin

    definition

      let n0 be non zero natural Number;

      :: NAT_5:def6

      attr n0 is perfect means ( sigma n0) = (2 * n0);

    end

    theorem :: NAT_5:38

    ((2 |^ p) -' 1) is prime & n0 = ((2 |^ (p -' 1)) * ((2 |^ p) -' 1)) implies n0 is perfect

    proof

      set n1 = (2 |^ (p -' 1));

      set k = (p -' 2);

      

       A1: (((2 |^ p) - 1) |^ 2) = (((2 |^ p) - 1) |^ (1 + 1))

      .= ((((2 |^ p) - 1) |^ 1) * ((2 |^ p) - 1)) by NEWTON: 6

      .= (((2 |^ p) - 1) * ((2 |^ p) - 1))

      .= (((2 |^ p) - 1) ^2 ) by SQUARE_1:def 1

      .= ((((2 |^ p) ^2 ) - ((2 * (2 |^ p)) * 1)) + (1 ^2 )) by SQUARE_1: 5

      .= ((((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 ^2 )) by SQUARE_1:def 1

      .= ((((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 * 1)) by SQUARE_1:def 1

      .= (((2 |^ p) * ((2 |^ p) - 2)) + 1);

      (2 |^ p) > p by NEWTON: 86;

      then (2 |^ p) >= (p + 1) by NAT_1: 13;

      then

       A2: ((2 |^ p) - 2) >= ((p + 1) - 2) by XREAL_1: 9;

      assume

       A3: ((2 |^ p) -' 1) is prime;

       A4:

      now

        assume

         A5: p <= 1;

        per cases by A5, NAT_1: 25;

          suppose p = 0 ;

          

          then ((2 |^ p) -' 1) = (1 -' 1) by NEWTON: 4

          .= (1 - 1) by XREAL_0:def 2

          .= 0 ;

          hence contradiction by A3;

        end;

          suppose p = 1;

          

          then ((2 |^ p) -' 1) = (2 -' 1)

          .= (2 - 1) by XREAL_0:def 2

          .= 1;

          hence contradiction by A3, INT_2:def 4;

        end;

      end;

      then

       A6: (p - 1) > (1 - 1) by XREAL_1: 9;

      then

       A7: (p -' 1) = (p - 1) by XREAL_0:def 2;

      p >= (1 + 1) by A4, NAT_1: 13;

      then (p - 2) >= (2 - 2) by XREAL_1: 9;

      then

       A8: k = (p - 2) by XREAL_0:def 2;

      then

       A9: p = (k + 2);

      (2 |^ p) > p by NEWTON: 86;

      then (2 |^ p) > 1 by A4, XXREAL_0: 2;

      then

       A10: ((2 |^ p) - 1) > (1 - 1) by XREAL_1: 9;

      then

       A11: ((2 |^ p) - 1) = ((2 |^ p) -' 1) by XREAL_0:def 2;

      reconsider n2 = ((2 |^ p) -' 1) as non zero Nat by A10, XREAL_0:def 2;

      assume

       A12: n0 = ((2 |^ (p -' 1)) * ((2 |^ p) -' 1));

      (p -' 1) = (k + 1) by A6, A8, XREAL_0:def 2;

      then (n1,n2) are_coprime by A3, A11, A9, Th1, EULER_1: 2;

      

      then ( sigma n0) = (( sigma n1) * ( sigma n2)) by A12, Th37

      .= ((((2 |^ ((p -' 1) + 1)) - 1) / (2 - 1)) * ( sigma n2)) by Th30, INT_2: 28

      .= (( sigma (n2 |^ 1)) * ((2 |^ p) -' 1)) by A7, A11

      .= ((((n2 |^ (1 + 1)) - 1) / (n2 - 1)) * ((2 |^ p) -' 1)) by A3, Th30

      .= ((2 |^ ((p -' 1) + 1)) * ((2 |^ p) -' 1)) by A6, A7, A11, A1, A2, XCMPLX_1: 89

      .= (((2 |^ (p -' 1)) * 2) * ((2 |^ p) -' 1)) by NEWTON: 6

      .= (2 * n0) by A12;

      hence n0 is perfect;

    end;

    ::$Notion-Name

    theorem :: NAT_5:39

    n0 is even & n0 is perfect implies ex p be Nat st ((2 |^ p) -' 1) is prime & n0 = ((2 |^ (p -' 1)) * ((2 |^ p) -' 1))

    proof

      assume n0 is even;

      then

      consider k9,n9 be Nat such that

       A1: n9 is odd and

       A2: k9 > 0 and

       A3: n0 = ((2 |^ k9) * n9) by Th2;

      reconsider n2 = n9 as non zero Nat by A1;

      set p = (k9 + 1);

      

       A4: (p - 1) = (p -' 1) by XREAL_0:def 2;

      

      then

       A5: ((2 |^ p) - 1) = (((2 |^ ((p -' 1) + 1)) - 2) + 1)

      .= ((((2 |^ (p -' 1)) * 2) - 2) + 1) by NEWTON: 6

      .= ((2 * ((2 |^ (p -' 1)) - 1)) + 1);

      assume n0 is perfect;

      then

       A6: ( sigma n0) = (2 * n0);

      take p;

      (2 |^ p) > p by NEWTON: 86;

      then

       A7: ((2 |^ p) - 1) > (p - 1) by XREAL_1: 14;

      then

       A8: ((2 |^ p) - 1) = ((2 |^ p) -' 1) by XREAL_0:def 2;

      ( sigma (2 |^ (p -' 1))) = (((2 |^ ((p -' 1) + 1)) - 1) / (2 - 1)) by Th30, INT_2: 28

      .= ((2 |^ p) - 1) by A4;

      

      then

       A9: (((2 |^ p) - 1) * ( sigma n9)) = ((2 * (2 |^ (p -' 1))) * n9) by A1, A3, A6, A4, Th3, Th37

      .= ((2 |^ p) * n9) by A4, NEWTON: 6;

      then ((2 |^ p) -' 1) divides ((2 |^ p) * n2) by A8, INT_1:def 3;

      then ((2 |^ p) -' 1) divides n2 by A8, A5, Th3, EULER_1: 13;

      then

      consider n99 be Nat such that

       A10: n9 = (((2 |^ p) -' 1) * n99) by NAT_D:def 3;

      (( sigma n9) * ((2 |^ p) - 1)) = (((2 |^ p) * n99) * ((2 |^ p) - 1)) by A8, A9, A10;

      

      then

       A11: ( sigma n2) = ((((2 |^ p) - 1) * n99) + n99) by A7, XCMPLX_1: 5

      .= (n9 + n99) by A7, A10, XREAL_0:def 2;

      

       A12: n99 divides n9 by A10, NAT_D:def 3;

      k9 >= ( 0 + 1) by A2, NAT_1: 13;

      then

       B01: (k9 + 1) >= (1 + 1) by XREAL_1: 7;

      (2 |^ p) > p by NEWTON: 86;

      then (2 |^ p) > 2 by B01, XXREAL_0: 2;

      then

       A13: ((2 |^ p) - 1) > (2 - 1) by XREAL_1: 14;

      then (((2 |^ p) -' 1) * n2) > (1 * n2) by A8, XREAL_1: 68;

      then

       A14: n99 = 1 by A10, A12, A11, Th33;

      hence ((2 |^ p) -' 1) is prime by A8, A10, A12, A13, A11, Th33;

      thus n0 = ((2 |^ (p -' 1)) * ((2 |^ p) -' 1)) by A3, A4, A10, A14;

    end;

    begin

    definition

      :: NAT_5:def7

      func Euler_phi -> sequence of NAT means

      : Def7: for k be Element of NAT holds (it . k) = ( Euler k);

      existence

      proof

        ex f be sequence of NAT st for k be Element of NAT holds (f . k) = ( Euler k) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        

         A1: for f1,f2 be sequence of NAT st (for x be Element of NAT holds (f1 . x) = ( Euler x)) & (for x be Element of NAT holds (f2 . x) = ( Euler x)) holds f1 = f2 from BINOP_2:sch 1;

        let f1,f2 be sequence of NAT ;

        assume (for k be Element of NAT holds (f1 . k) = ( Euler k)) & for k be Element of NAT holds (f2 . k) = ( Euler k);

        hence thesis by A1;

      end;

    end

    theorem :: NAT_5:40

    ( Sum ( Euler_phi | ( NatDivisors n0))) = n0

    proof

      ( dom Euler_phi ) = NAT & ( rng Euler_phi ) c= REAL by FUNCT_2:def 1;

      then

      reconsider EU9 = Euler_phi as sequence of REAL by FUNCT_2: 2;

      set X = ( Seg n0);

      defpred P[ set, set] means $2 = { i where i be Element of NAT : ex h be Nat st i in X & $1 in ( NatDivisors n0) & h = $1 & (i gcd n0) = (n0 / h) };

      

       A1: ( dom Euler_phi ) = NAT by FUNCT_2:def 1;

      

       A2: for k be Nat st k in X holds ex x be Element of ( bool X) st P[k, x]

      proof

        let k be Nat;

        set X9 = { i where i be Element of NAT : ex h be Nat st i in X & k in ( NatDivisors n0) & h = k & (i gcd n0) = (n0 / h) };

        for x be object st x in X9 holds x in X

        proof

          let x be object;

          assume x in X9;

          then ex i be Element of NAT st i = x & ex h be Nat st i in X & k in ( NatDivisors n0) & h = k & (i gcd n0) = (n0 / h);

          hence x in X;

        end;

        then

        reconsider X9 as Element of ( bool X) by TARSKI:def 3;

        assume k in X;

        take X9;

        thus P[k, X9];

      end;

      consider fp be FinSequence of ( bool X) such that

       A3: ( dom fp) = X & for k be Nat st k in X holds P[k, (fp . k)] from FINSEQ_1:sch 5( A2);

      

       A4: ( NatDivisors n0) c= ( Seg n0) by MOEBIUS1: 40;

      then

       A5: ( rng ( Sgm ( NatDivisors n0))) c= ( dom fp) by A3, FINSEQ_1:def 13;

      then

       A6: ( rng ( Sgm ( NatDivisors n0))) c= ( dom ( Card fp)) by CARD_3:def 2;

      then

      reconsider f1 = (( Card fp) * ( Sgm ( NatDivisors n0))) as FinSequence of NAT by Th9;

      

       A7: ( NatDivisors n0) c= ( dom fp) by A3, MOEBIUS1: 40;

      

       A8: ( dom (( Card fp) * ( Sgm ( NatDivisors n0)))) = ( dom ( Sgm ( NatDivisors n0))) by A6, RELAT_1: 27

      .= ( dom ( Euler_phi * ( Sgm ( NatDivisors n0)))) by A5, A1, RELAT_1: 27, XBOOLE_1: 1;

      for k be Element of NAT st k in ( dom (( Card fp) * ( Sgm ( NatDivisors n0)))) holds ((( Card fp) * ( Sgm ( NatDivisors n0))) . k) = (( Euler_phi * ( Sgm ( NatDivisors n0))) . k)

      proof

        let k be Element of NAT ;

        set k9 = (( Sgm ( NatDivisors n0)) . k);

        set Y = { l where l be Element of NAT : (k9,l) are_coprime & l >= 1 & l <= k9 };

        set Z = { i where i be Element of NAT : ex h be Nat st i in X & k9 in ( NatDivisors n0) & h = k9 & (i gcd n0) = (n0 / h) };

        deffunc F( Nat) = (($1 * n0) / k9);

        

         A9: for x be object st x in Y holds x in NAT

        proof

          let x be object;

          assume x in Y;

          then ex l be Element of NAT st x = l & (k9,l) are_coprime & l >= 1 & l <= k9;

          hence x in NAT ;

        end;

        assume

         A10: k in ( dom (( Card fp) * ( Sgm ( NatDivisors n0))));

        then k in ( dom ( Sgm ( NatDivisors n0))) by FUNCT_1: 11;

        then k9 in ( rng ( Sgm ( NatDivisors n0))) by FUNCT_1: 3;

        then

         A11: k9 in ( NatDivisors n0) by A4, FINSEQ_1:def 13;

        then

         A12: 1 <= k9 by A3, A7, FINSEQ_1: 1;

        (k9,1) are_coprime by WSIERP_1: 9;

        then 1 in Y by A12;

        then

        reconsider Y as non empty Subset of NAT by A9, TARSKI:def 3;

        consider f be Function such that

         A13: ( dom f) = Y & for d be Element of Y holds (f . d) = F(d) from FUNCT_1:sch 4;

        for y be object holds y in ( rng f) iff y in Z

        proof

          let y be object;

          hereby

            assume y in ( rng f);

            then

            consider x be object such that

             A14: x in ( dom f) and

             A15: y = (f . x) by FUNCT_1:def 3;

            reconsider x as Element of Y by A13, A14;

            

             A16: 0 < k9 by A11;

            k9 divides n0 by A11, MOEBIUS1: 39;

            then

            consider j be Nat such that

             A17: n0 = (k9 * j) by NAT_D:def 3;

            y = F(x) by A13, A15

            .= (x * (n0 / k9)) by XCMPLX_1: 74;

            

            then

             A18: y = (x * (j / (k9 / k9))) by A17, XCMPLX_1: 77

            .= (x * (j / 1)) by A16, XCMPLX_1: 60

            .= (x * j);

            then

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

            x in Y;

            then

            consider l be Element of NAT such that

             A19: x = l and

             A20: (k9,l) are_coprime and

             A21: l >= 1 and

             A22: l <= k9;

            

             A23: (x * j) <= (k9 * j) by A19, A22, XREAL_1: 64;

            j <> 0 by A17;

            then (j + 1) > ( 0 + 1) by XREAL_1: 6;

            then 1 <= j by NAT_1: 13;

            then (1 * 1) <= (x * j) by A19, A21, XREAL_1: 66;

            then

             A24: i in X by A17, A18, A23;

            

             A25: (k9 gcd l) = 1 by A20, INT_2:def 3;

            (n0 / k9) = (j / (k9 / k9)) by A17, XCMPLX_1: 77

            .= (j / 1) by A16, XCMPLX_1: 60;

            then (i gcd n0) = (n0 / k9) by A19, A17, A18, A25, EULER_1: 5;

            hence y in Z by A11, A24;

          end;

          assume y in Z;

          then

          consider i be Element of NAT such that

           A26: i = y and

           A27: ex h be Nat st i in X & k9 in ( NatDivisors n0) & h = k9 & (i gcd n0) = (n0 / h);

          (i gcd n0) divides i by INT_2:def 2;

          then

          consider x be Nat such that

           A28: i = ((i gcd n0) * x) by NAT_D:def 3;

          

           A29: y = ((x * n0) / k9) by A26, A27, A28, XCMPLX_1: 74;

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

          

           A30: k9 <> 0 by A27;

          

           A31: (k9 * (i gcd n0)) = (n0 / (k9 / k9)) by A27, XCMPLX_1: 81

          .= (n0 / 1) by A30, XCMPLX_1: 60;

          then

           A32: (k9,x) are_coprime by A27, A28, EULER_1: 6;

          x <> 0 by A27, A28, FINSEQ_1: 1;

          then (x + 1) > ( 0 + 1) by XREAL_1: 6;

          then

           A33: x >= 1 by NAT_1: 13;

          i <= n0 by A27, FINSEQ_1: 1;

          then x <= k9 by A27, A28, A31, XREAL_1: 68;

          then x in ( dom f) by A13, A32, A33;

          then

          reconsider x as Element of Y by A13;

          y = (f . x) by A13, A29;

          hence y in ( rng f) by A13, FUNCT_1:def 3;

        end;

        then

         A34: ( rng f) = Z by TARSKI: 2;

        for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume x1 in ( dom f);

          then

          reconsider x19 = x1 as Element of Y by A13;

          assume x2 in ( dom f);

          then

          reconsider x29 = x2 as Element of Y by A13;

          assume

           A35: (f . x1) = (f . x2);

          

           A36: F(x19) = (f . x19) by A13

          .= F(x29) by A13, A35;

          (x19 * (n0 / k9)) = ((x19 * n0) / k9) by XCMPLX_1: 74

          .= (x29 * (n0 / k9)) by A36, XCMPLX_1: 74;

          hence x1 = x2 by A12, XCMPLX_1: 5;

        end;

        then f is one-to-one by FUNCT_1:def 4;

        then

         A37: (Y,Z) are_equipotent by A13, A34, WELLORD2:def 4;

        (fp . k9) = Z by A3, A7, A11;

        then ( card (fp . k9)) = ( card Y) by A37, CARD_1: 5;

        then (( Card fp) . k9) = ( Euler k9) by A7, A11, CARD_3:def 2;

        then

         A38: (( Card fp) . k9) = ( Euler_phi . k9) by Def7;

        ((( Card fp) * ( Sgm ( NatDivisors n0))) . k) = (( Card fp) . k9) by A10, FUNCT_1: 12;

        hence thesis by A8, A10, A38, FUNCT_1: 12;

      end;

      then

       A39: (( Card fp) * ( Sgm ( NatDivisors n0))) = ( Euler_phi * ( Sgm ( NatDivisors n0))) by A8, PARTFUN1: 5;

      set k = ( len fp);

      

       A40: ( Func_Seq ( Euler_phi ,( Sgm ( NatDivisors n0)))) = ( Euler_phi * ( Sgm ( NatDivisors n0))) by BHSP_5:def 4

      .= ( Func_Seq (EU9,( Sgm ( NatDivisors n0)))) by BHSP_5:def 4;

      

       A41: for x be object holds x in ( NatDivisors n0) iff x in ( Seg n0) & not x in (( Card fp) " { 0 })

      proof

        reconsider y = 0 as Element of NAT ;

        let x be object;

        

         A42: y in { 0 } by TARSKI:def 1;

        hereby

          assume

           A43: x in ( NatDivisors n0);

          then

          reconsider k = x as Element of NAT ;

          thus x in ( Seg n0) by A4, A43;

          assume x in (( Card fp) " { 0 });

          then

          consider y be object such that

           A44: [x, y] in ( Card fp) & y in { 0 } by RELAT_1:def 14;

          y = 0 & y = (( Card fp) . x) by A44, FUNCT_1: 1, TARSKI:def 1;

          then ( card (fp . x)) = {} by A3, A4, A43, CARD_3:def 2;

          then

           A45: (fp . x) = {} ;

          k divides n0 by A43, MOEBIUS1: 39;

          then

          consider i be Nat such that

           A46: n0 = (k * i) by NAT_D:def 3;

          i <> 0 by A46;

          then ( 0 + 1) < (i + 1) by XREAL_1: 6;

          then

           A47: 1 <= i by NAT_1: 13;

          

           A48: i divides n0 by A46, NAT_D:def 3;

          then i <= n0 by NAT_D: 7;

          then

           A49: i in X by A47;

          

           A50: k <> 0 by A46;

          n0 = (k * (i gcd n0)) by A46, A48, NEWTON: 49;

          

          then (n0 / k) = ((i gcd n0) * (k / k)) by XCMPLX_1: 74

          .= ((i gcd n0) * 1) by A50, XCMPLX_1: 60;

          then i in { i9 where i9 be Element of NAT : ex h be Nat st i9 in X & k in ( NatDivisors n0) & h = k & (i9 gcd n0) = (n0 / h) } by A43, A49;

          hence contradiction by A3, A4, A43, A45;

        end;

        assume

         A51: x in ( Seg n0);

        then

        reconsider k = x as Element of NAT ;

        

         A52: (fp . k) = { i9 where i9 be Element of NAT : ex h be Nat st i9 in X & k in ( NatDivisors n0) & h = k & (i9 gcd n0) = (n0 / h) } by A3, A51;

        assume

         A53: not x in (( Card fp) " { 0 });

        assume

         A54: not x in ( NatDivisors n0);

        (fp . k) = {}

        proof

          assume (fp . k) <> {} ;

          then

          consider x9 be object such that

           A55: x9 in (fp . k) by XBOOLE_0:def 1;

          ex i be Element of NAT st x9 = i & ex h be Nat st i in X & k in ( NatDivisors n0) & h = k & (i gcd n0) = (n0 / h) by A52, A55;

          hence contradiction by A54;

        end;

        then

         A56: y = (( Card fp) . x) by A3, A51, CARD_1: 27, CARD_3:def 2;

        x in ( dom ( Card fp)) by A3, A51, CARD_3:def 2;

        then [k, y] in ( Card fp) by A56, FUNCT_1: 1;

        hence contradiction by A53, A42, RELSET_1: 30;

      end;

      reconsider f29 = ( Card fp) as FinSequence of REAL by Th13;

      reconsider f19 = f1 as FinSequence of REAL by Th13;

      

       A57: ( NatDivisors n0) c= ( Seg n0) by MOEBIUS1: 40;

      ( Seg n0) = ( dom ( Card fp)) by A3, CARD_3:def 2;

      then f19 = (f29 - { 0 }) by A41, XBOOLE_0:def 5;

      then

       A58: ( Sum f19) = ( Sum f29) by Th12;

      

       A59: for d,e be Nat st d in ( dom fp) & e in ( dom fp) & d <> e holds (fp . d) misses (fp . e)

      proof

        let d,e be Nat;

        assume d in ( dom fp);

        then

         A60: (fp . d) = { i where i be Element of NAT : ex h be Nat st i in X & d in ( NatDivisors n0) & h = d & (i gcd n0) = (n0 / h) } by A3;

        assume e in ( dom fp);

        then

         A61: (fp . e) = { i where i be Element of NAT : ex h be Nat st i in X & e in ( NatDivisors n0) & h = e & (i gcd n0) = (n0 / h) } by A3;

        assume

         A62: d <> e;

        assume not (fp . d) misses (fp . e);

        then ((fp . d) /\ (fp . e)) <> {} by XBOOLE_0:def 7;

        then

        consider x be object such that

         A63: x in ((fp . d) /\ (fp . e)) by XBOOLE_0:def 1;

        x in (fp . d) by A63, XBOOLE_0:def 4;

        then

         A64: ex i1 be Element of NAT st x = i1 & ex h be Nat st i1 in X & d in ( NatDivisors n0) & h = d & (i1 gcd n0) = (n0 / h) by A60;

        x in (fp . e) by A63, XBOOLE_0:def 4;

        then ex i2 be Element of NAT st x = i2 & ex h be Nat st i2 in X & e in ( NatDivisors n0) & h = e & (i2 gcd n0) = (n0 / h) by A61;

        then d = (n0 / (n0 / e)) by A64, XCMPLX_1: 52;

        hence contradiction by A62, XCMPLX_1: 52;

      end;

      

       A65: for x be object holds x in ( union ( rng fp)) iff x in X

      proof

        let x be object;

        thus x in ( union ( rng fp)) implies x in X;

        assume

         A66: x in X;

        then

        reconsider i = x as Nat;

        (i gcd n0) divides n0 by NAT_D:def 5;

        then

        consider h be Nat such that

         A67: n0 = ((i gcd n0) * h) by NAT_D:def 3;

        

         A68: 0 < h by A67;

        then ( 0 + 1) < (h + 1) by XREAL_1: 6;

        then

         A69: 1 <= h by NAT_1: 13;

        

         A70: h divides n0 by A67, NAT_D:def 3;

        then

         A71: h in ( NatDivisors n0) by A68, MOEBIUS1: 39;

        set Y = (fp . h);

        

         A72: h <> 0 by A67;

        h <= n0 by A70, NAT_D: 7;

        then

         A73: h in ( dom fp) by A3, A69;

        then

         A74: Y in ( rng fp) by FUNCT_1: 3;

        

         A75: (fp . h) = { i9 where i9 be Element of NAT : ex h9 be Nat st i9 in X & h in ( NatDivisors n0) & h9 = h & (i9 gcd n0) = (n0 / h9) } by A3, A73;

        (n0 / h) = ((i gcd n0) * (h / h)) by A67, XCMPLX_1: 74

        .= ((i gcd n0) * 1) by A72, XCMPLX_1: 60;

        then x in Y by A66, A71, A75;

        hence x in ( union ( rng fp)) by A74, TARSKI:def 4;

      end;

      ( card ( union ( rng fp))) = ( Sum ( Card fp)) by A59, INT_5: 48;

      then

       A76: ( card X) = ( Sum ( Card fp)) by A65, TARSKI: 2;

      ( card X) = ( card n0) by FINSEQ_1: 55;

      then n0 = ( Sum ( Card fp)) by A76;

      then ( Sum ( Func_Seq ( Euler_phi ,( Sgm ( NatDivisors n0))))) = n0 by A58, A39, BHSP_5:def 4;

      hence thesis by A40, A57, Th24;

    end;