number01.miz

    begin

    registration

      cluster positive for Integer;

      existence

      proof

        take 1;

        thus thesis;

      end;

    end

    theorem :: NUMBER01:1

    for n be positive Integer holds (n + 1) divides ((n ^2 ) + 1) iff n = 1

    proof

      let n be positive Integer;

      thus (n + 1) divides ((n ^2 ) + 1) implies n = 1

      proof

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

        then

         n: (n + 1) divides ((n * (n + 1)) - (n - 1));

        (n + 1) divides (n * (n + 1)) by INT_1:def 3;

        then

         n1: (n + 1) divides (n - 1) by n, INT_5: 2;

        assume

         o: n <> 1;

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

        then n > 1 by o, XXREAL_0: 1;

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

        then (n + 1) <= (n - 1) by n1, INT_2: 27;

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

        hence contradiction;

      end;

      assume n = 1;

      hence (n + 1) divides ((n ^2 ) + 1);

    end;

    theorem :: NUMBER01:2



     lemmod: for i,n be Integer st |.i.| = n holds i = n or i = ( - n)

    proof

      let i,n be Integer;

      assume |.i.| = n & i <> n;

      then n = ( - i) by ABSVALUE:def 1;

      hence i = ( - n);

    end;

    theorem :: NUMBER01:3



     lem24nat: for n be natural number st n divides 24 holds n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24

    proof

      let n be natural number;

      assume

       n: n divides 24;

      then n <= 24 by INT_2: 27;

      then

       el: n = 0 or ... or n = 24;



       n0: not 0 divides 24 by INT_2: 3;

      (5 * 4) < 24 < (5 * (4 + 1));

      then

       n5: not 5 divides 24 by NEWTON03: 40;

      (7 * 3) < 24 < (7 * (3 + 1));

      then

       n7: not 7 divides 24 by NEWTON03: 40;

      (9 * 2) < 24 < (9 * (2 + 1));

      then

       n9: not 9 divides 24 by NEWTON03: 40;

      (10 * 2) < 24 < (10 * (2 + 1));

      then

       n10: not 10 divides 24 by NEWTON03: 40;

      (11 * 2) < 24 < (11 * (2 + 1));

      then

       n11: not 11 divides 24 by NEWTON03: 40;

      (13 * 1) < 24 < (13 * (1 + 1));

      then

       n13: not 13 divides 24 by NEWTON03: 40;

      (14 * 1) < 24 < (14 * (1 + 1));

      then

       n14: not 14 divides 24 by NEWTON03: 40;

      (15 * 1) < 24 < (15 * (1 + 1));

      then

       n15: not 15 divides 24 by NEWTON03: 40;

      (16 * 1) < 24 < (16 * (1 + 1));

      then

       n16: not 16 divides 24 by NEWTON03: 40;

      (17 * 1) < 24 < (17 * (1 + 1));

      then

       n17: not 17 divides 24 by NEWTON03: 40;

      (18 * 1) < 24 < (18 * (1 + 1));

      then

       n18: not 18 divides 24 by NEWTON03: 40;

      (19 * 1) < 24 < (19 * (1 + 1));

      then

       n19: not 19 divides 24 by NEWTON03: 40;

      (20 * 1) < 24 < (20 * (1 + 1));

      then

       n20: not 20 divides 24 by NEWTON03: 40;

      (21 * 1) < 24 < (21 * (1 + 1));

      then

       n21: not 21 divides 24 by NEWTON03: 40;

      (22 * 1) < 24 < (22 * (1 + 1));

      then

       n22: not 22 divides 24 by NEWTON03: 40;

      (23 * 1) < 24 < (23 * (1 + 1));

      then not 23 divides 24 by NEWTON03: 40;

      hence n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 by n, el, n0, n5, n7, n9, n10, n11, n13, n14, n15, n16, n17, n18, n19, n20, n21, n22;

    end;

    theorem :: NUMBER01:4



     lem24: for t be Integer st t divides 24 holds t = ( - 1) or t = 1 or t = ( - 2) or t = 2 or t = ( - 3) or t = 3 or t = ( - 4) or t = 4 or t = ( - 6) or t = 6 or t = ( - 8) or t = 8 or t = ( - 12) or t = 12 or t = ( - 24) or t = 24

    proof

      let t be Integer;

      reconsider n = |.t.| as Nat;

      assume t divides 24;

      then n divides |.24.| by INT_2: 16;

      then n divides 24;

      then n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 by lem24nat;

      hence t = ( - 1) or t = 1 or t = ( - 2) or t = 2 or t = ( - 3) or t = 3 or t = ( - 4) or t = 4 or t = ( - 6) or t = 6 or t = ( - 8) or t = 8 or t = ( - 12) or t = 12 or t = ( - 24) or t = 24 by lemmod;

    end;

    begin

    theorem :: NUMBER01:5

    for x be Integer st (x - 3) divides ((x |^ 3) - 3) holds x = ( - 21) or x = ( - 9) or x = ( - 5) or x = ( - 3) or x = ( - 1) or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27

    proof

      let x be Integer;

      assume

       x: (x - 3) divides ((x |^ 3) - 3);

      set t = (x - 3);



       e: (((t + 3) |^ (2 + 1)) - 3) = ((((t + 3) |^ (1 + 1)) * (t + 3)) - 3) by NEWTON: 6

      .= (((((t + 3) |^ 1) * (t + 3)) * (t + 3)) - 3) by NEWTON: 6

      .= ((((t + 3) * (t + 3)) * (t + 3)) - 3) by NEWTON: 5

      .= (((((t * t) * t) + (27 * t)) + ((9 * t) * t)) + 24);



       t: t divides ((t * t) * t) & t divides (27 * t) & t divides ((9 * t) * t) by INT_1:def 3;

      then t divides (((t * t) * t) + (27 * t)) by WSIERP_1: 4;

      then t divides ((((t * t) * t) + (27 * t)) + ((9 * t) * t)) by t, WSIERP_1: 4;

      then t divides 24 by x, e, INT_2: 1;

      then t = ( - 1) or t = 1 or t = ( - 2) or t = 2 or t = ( - 3) or t = 3 or t = ( - 4) or t = 4 or t = ( - 6) or t = 6 or t = ( - 8) or t = 8 or t = ( - 12) or t = 12 or t = ( - 24) or t = 24 by lem24;

      hence x = ( - 21) or x = ( - 9) or x = ( - 5) or x = ( - 3) or x = ( - 1) or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27;

    end;

    begin

    theorem :: NUMBER01:6

    { n where n be positive Integer : 5 divides ((4 * (n |^ 2)) + 1) & 13 divides ((4 * (n |^ 2)) + 1) } is infinite

    proof

      set S = { n where n be positive Integer : 5 divides ((4 * (n |^ 2)) + 1) & 13 divides ((4 * (n |^ 2)) + 1) };

      deffunc F( Nat) = ((65 * $1) + 56);

      consider f be ManySortedSet of NAT such that

       f: for n be Element of NAT holds (f . n) = F(n) from PBOOLE:sch 5;

      set R = ( rng f);



       d: ( dom f) = NAT by PARTFUN1:def 2;



       rs: R c= S

      proof

        let a be object;

        assume a in R;

        then

        consider k be object such that

         k: k in ( dom f) & a = (f . k) by FUNCT_1:def 3;

        reconsider k as Element of NAT by d, k;



         a: a = ((65 * k) + 56) by f, k;

        then

        reconsider n = a as positive Integer;



         c: ((4 * (n |^ (1 + 1))) + 1) = ((4 * ((n |^ 1) * n)) + 1) by NEWTON: 6

        .= ((4 * (n * n)) + 1) by NEWTON: 5;

        65 = (5 * 13);

        then

         p: 13 divides (65 - 0 ) by INT_1:def 3;

        (((65 * k) + 56) - 1) = (5 * ((13 * k) + 11));

        then 5 divides (((65 * k) + 56) - 1) by INT_1:def 3;

        then (n,1) are_congruent_mod 5 by a, INT_1:def 4;

        then ((n * n),(1 * 1)) are_congruent_mod 5 & (4,4) are_congruent_mod 5 by INT_1: 18, INT_1: 11;

        then ((4 * (n * n)),(1 * 4)) are_congruent_mod 5 & (1,1) are_congruent_mod 5 by INT_1: 18, INT_1: 11;

        then (((4 * (n * n)) + 1),(4 + 1)) are_congruent_mod 5 & (5, 0 ) are_congruent_mod 5 by INT_1: 16, INT_1: 12;

        then (((4 * (n * n)) + 1), 0 ) are_congruent_mod 5 by INT_1: 15;

        then (((4 * (n |^ 2)) + 1), 0 ) are_congruent_mod 5 by c;

        then

         d1: 5 divides (((4 * (n |^ 2)) + 1) - 0 ) by INT_1:def 4;

        (((65 * k) + 56) - 4) = (13 * ((5 * k) + 4));

        then 13 divides (((65 * k) + 56) - 4) by INT_1:def 3;

        then (n,4) are_congruent_mod 13 by a, INT_1:def 4;

        then ((n * n),(4 * 4)) are_congruent_mod 13 & (4,4) are_congruent_mod 13 by INT_1: 18, INT_1: 11;

        then ((4 * (n * n)),((4 * 4) * 4)) are_congruent_mod 13 & (1,1) are_congruent_mod 13 by INT_1: 18, INT_1: 11;

        then (((4 * (n * n)) + 1),(64 + 1)) are_congruent_mod 13 & (65, 0 ) are_congruent_mod 13 by INT_1: 16, INT_1:def 4, p;

        then (((4 * (n * n)) + 1), 0 ) are_congruent_mod 13 by INT_1: 15;

        then (((4 * (n |^ 2)) + 1), 0 ) are_congruent_mod 13 by c;

        then 13 divides (((4 * (n |^ 2)) + 1) - 0 ) by INT_1:def 4;

        hence a in S by d1;

      end;

      for m be Element of NAT holds ex n be Element of NAT st n >= m & n in R

      proof

        let m be Element of NAT ;

        take n = F(m);

        (65 * m) >= (1 * m) by XREAL_1: 66;

        hence n >= m by XREAL_1: 38;

        m in ( dom f) by d;

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

        hence n in R by f;

      end;

      then R is infinite by PYTHTRIP: 9;

      hence thesis by rs, FINSET_1: 1;

    end;

    begin

    theorem :: NUMBER01:7

    for n be positive Integer holds 169 divides (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27)

    proof

      let n be positive Integer;

      reconsider k = n as Nat by TARSKI: 1;

      defpred P[ Nat] means 169 divides (((3 |^ ((3 * $1) + 3)) - (26 * $1)) - 27);



       tt: (3 |^ (2 + 1)) = ((3 |^ (1 + 1)) * 3) by NEWTON: 6

      .= (((3 |^ ( 0 + 1)) * 3) * 3) by NEWTON: 6

      .= ((3 * 3) * 3) by NEWTON: 5;

      (((3 |^ ((3 * 1) + 3)) - (26 * 1)) - 27) = ((3 |^ (5 + 1)) - 53)

      .= (((3 |^ (4 + 1)) * 3) - 53) by NEWTON: 6

      .= ((((3 |^ (3 + 1)) * 3) * 3) - 53) by NEWTON: 6

      .= (((((3 |^ (2 + 1)) * 3) * 3) * 3) - 53) by NEWTON: 6

      .= (169 * 4) by tt;

      then

       o: P[1] by INT_1:def 3;

       i:

      now

        let n be Nat;

        assume

         n: 1 <= n & P[n];



         d: 13 divides (13 * 2) by INT_1:def 3;



         e: ((((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27)) = (((((3 |^ 3) * (3 |^ ((3 * n) + 3))) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27)) by NEWTON: 8

        .= (26 * ((3 |^ ((3 * n) + 3)) - 1)) by tt;

        ((3 |^ (2 + 1)) - 1) = (((3 |^ (1 + 1)) * 3) - 1) by NEWTON: 6

        .= ((((3 |^ ( 0 + 1)) * 3) * 3) - 1) by NEWTON: 6

        .= (((3 * 3) * 3) - 1) by NEWTON: 5;

        then ((3 |^ 3) - 1) = (13 * 2);

        then

         t: 13 divides ((3 |^ 3) - 1) by INT_1:def 3;

        ((3 |^ (3 * (n + 1))) - 1) = (((3 |^ 3) |^ (n + 1)) - 1) by NEWTON: 9

        .= (((3 |^ 3) |^ (n + 1)) - (1 |^ (n + 1))) by NEWTON: 10;

        then ((3 |^ 3) - 1) divides ((3 |^ ((3 * n) + 3)) - 1) by NEWTON01: 33;

        then 13 divides ((3 |^ ((3 * n) + 3)) - 1) by t, INT_2: 9;

        then (13 * 13) divides ((((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ (3 * (n + 1))) - (26 * n)) - 27)) by d, e, NEWTON03: 5;

        then 169 divides ( - ((((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27))) by INT_2: 10;

        then 169 divides ((((3 |^ ((3 * n) + 3)) - (26 * n)) - 27) - (((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27));

        then 169 divides (((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) by n, INT_5: 2;

        hence P[(n + 1)];

      end;

      for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( o, i);

      then P[k] by NAT_1: 14;

      hence thesis;

    end;

    begin

    theorem :: NUMBER01:8

    for k be Nat holds 19 divides ((2 |^ (2 |^ ((6 * k) + 2))) + 3)

    proof

      let k be Nat;

      (2 |^ 1) = 2 by NEWTON: 5;

      then

       d2: (2 |^ (1 + 1)) = (2 * 2) by NEWTON: 6;

      then (2 |^ (2 + 1)) = (2 * 4) by NEWTON: 6;

      then

       d4: (2 |^ (3 + 1)) = (2 * 8) by NEWTON: 6;

      then (2 |^ (4 + 1)) = (2 * 16) by NEWTON: 6;

      then

       d6: (2 |^ (5 + 1)) = (2 * 32) by NEWTON: 6;

      (64 - 1) = (9 * 7);

      then 9 divides ((2 |^ 6) - 1) by d6, INT_1:def 3;

      then ((2 |^ 6),1) are_congruent_mod 9 by INT_1:def 4;

      then (((2 |^ 6) |^ k),(1 |^ k)) are_congruent_mod 9 by GR_CY_3: 34;

      then ((2 |^ (6 * k)),(1 |^ k)) are_congruent_mod 9 by NEWTON: 9;

      then

       a: ((2 |^ (6 * k)),1) are_congruent_mod 9 by NEWTON: 10;

      ((2 |^ 2),(2 |^ 2)) are_congruent_mod 9 by INT_1: 11;

      then (((2 |^ (6 * k)) * (2 |^ 2)),(1 * (2 |^ 2))) are_congruent_mod 9 by a, INT_1: 18;

      then

       c9: ((2 |^ ((6 * k) + 2)),(2 |^ 2)) are_congruent_mod 9 by NEWTON: 8;

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

      then ((2 |^ ((6 * k) + 2)), 0 ) are_congruent_mod 2 & ((2 |^ 2), 0 ) are_congruent_mod 2 by INT_1: 60;

      then ((2 |^ ((6 * k) + 2)), 0 ) are_congruent_mod 2 & ( 0 ,(2 |^ 2)) are_congruent_mod 2 by INT_1: 14;

      then

       c2: ((2 |^ ((6 * k) + 2)),(2 |^ 2)) are_congruent_mod 2 by INT_1: 15;

      3 is odd by POLYFORM: 6;

      then (3 * 3) is odd;

      then ((2 |^ 1),9) are_coprime by NAT_5: 3;

      then (2,9) are_coprime by NEWTON: 5;

      then ((2 |^ ((6 * k) + 2)),(2 |^ 2)) are_congruent_mod (2 * 9) by c2, c9, INT_6: 21;

      then

      consider t be Integer such that

       t: ((2 |^ ((6 * k) + 2)) - (2 |^ 2)) = (18 * t) by INT_1:def 5;



       t1: (2 |^ ((6 * k) + 2)) = ((18 * t) + (2 |^ 2)) by t

      .= ((18 * t) + 4) by d2;

      ((6 * k) + 2) >= ( 0 + 2) by XREAL_1: 7;

      then (2 |^ ((6 * k) + 2)) >= (2 |^ 2) by NAT_6: 1;

      then (18 * t) >= 0 & 18 > 0 by t, XREAL_1: 48;

      then t >= 0 by XREAL_1: 132;

      then t in NAT by INT_1: 3;

      then

      reconsider t as Nat;



       dz: 19 is prime by NAT_4: 29;

      2 is prime by INT_2: 28;

      then (2,19) are_coprime by dz, INT_2: 30;

      then ((2 |^ ( Euler 19)) mod 19) = 1 & 18 = (19 - 1) by EULER_2: 18;

      then ((2 |^ 18) mod 19) = 1 by EULER_1: 20, dz;

      then ((2 |^ 18),1) are_congruent_mod 19 by NAT_6: 10;

      then (((2 |^ 18) |^ t),(1 |^ t)) are_congruent_mod 19 by GR_CY_3: 34;

      then ((2 |^ (18 * t)),(1 |^ t)) are_congruent_mod 19 by NEWTON: 9;

      then ((2 |^ (18 * t)),1) are_congruent_mod 19 & ((2 |^ 4),(2 |^ 4)) are_congruent_mod 19 by NEWTON: 10, INT_1: 11;

      then (((2 |^ (18 * t)) * (2 |^ 4)),(1 * (2 |^ 4))) are_congruent_mod 19 by INT_1: 18;

      then ((2 |^ ((18 * t) + 4)),(2 |^ 4)) are_congruent_mod 19 by NEWTON: 8;

      then ((2 |^ (2 |^ ((6 * k) + 2))),(2 |^ 4)) are_congruent_mod 19 & (3,3) are_congruent_mod 19 by t1, INT_1: 11;

      then (((2 |^ (2 |^ ((6 * k) + 2))) + 3),((2 |^ 4) + 3)) are_congruent_mod 19 by INT_1: 16;

      then (((2 |^ (2 |^ ((6 * k) + 2))) + 3),19) are_congruent_mod 19 & (19, 0 ) are_congruent_mod 19 by d4, INT_1: 12;

      then (((2 |^ (2 |^ ((6 * k) + 2))) + 3), 0 ) are_congruent_mod 19 by INT_1: 15;

      then 19 divides (((2 |^ (2 |^ ((6 * k) + 2))) + 3) - 0 ) by INT_1:def 4;

      hence thesis;

    end;

    begin

    theorem :: NUMBER01:9

    13 divides ((2 |^ 70) + (3 |^ 70))

    proof



       dp: 2 is prime by INT_2: 28;



       tp: 13 is prime by NAT_4: 28;

      then (2,13) are_coprime by dp, INT_2: 30;

      then ((2 |^ ( Euler 13)) mod 13) = 1 & 12 = (13 - 1) by EULER_2: 18;

      then ((2 |^ 12) mod 13) = 1 by EULER_1: 20, tp;

      then ((2 |^ 12),1) are_congruent_mod 13 by NAT_6: 10;

      then (((2 |^ 12) |^ 5),(1 |^ 5)) are_congruent_mod 13 by GR_CY_3: 34;

      then ((2 |^ (12 * 5)),(1 |^ 5)) are_congruent_mod 13 by NEWTON: 9;

      then

       ds: ((2 |^ 60),1) are_congruent_mod 13 by NEWTON: 10;

      (2 |^ 1) = 2 by NEWTON: 5;

      then (2 |^ (1 + 1)) = (2 * 2) by NEWTON: 6;

      then (2 |^ (2 + 1)) = (2 * 4) by NEWTON: 6;

      then (2 |^ (3 + 1)) = (2 * 8) by NEWTON: 6;

      then (2 |^ (4 + 1)) = (2 * 16) by NEWTON: 6;

      then ((2 |^ 5) - 6) = (13 * 2);

      then ((2 |^ 5),6) are_congruent_mod 13 by INT_1:def 5;

      then (((2 |^ 5) |^ 2),(6 |^ 2)) are_congruent_mod 13 by GR_CY_3: 34;

      then ((2 |^ (5 * 2)),(6 |^ 2)) are_congruent_mod 13 by NEWTON: 9;

      then

       ts: ((2 |^ (5 * 2)),(6 * 6)) are_congruent_mod 13 by WSIERP_1: 1;

      (36 - ( - 3)) = (13 * 3);

      then (36,( - 3)) are_congruent_mod 13 by INT_1:def 5;

      then ((2 |^ 10),( - 3)) are_congruent_mod 13 by ts, INT_1: 15;

      then (((2 |^ 60) * (2 |^ 10)),(1 * ( - 3))) are_congruent_mod 13 by ds, INT_1: 18;

      then

       dsi: ((2 |^ (60 + 10)),( - 3)) are_congruent_mod 13 by NEWTON: 8;

      (3 |^ (2 + 1)) = ((3 |^ 2) * 3) by NEWTON: 6

      .= ((3 * 3) * 3) by WSIERP_1: 1

      .= ((2 * 13) + 1);

      then ((3 |^ 3) - 1) = (2 * 13);

      then ((3 |^ 3),1) are_congruent_mod 13 by INT_1:def 5;

      then (((3 |^ 3) |^ 23),(1 |^ 23)) are_congruent_mod 13 by GR_CY_3: 34;

      then ((3 |^ (3 * 23)),(1 |^ 23)) are_congruent_mod 13 by NEWTON: 9;

      then ((3 |^ 69),1) are_congruent_mod 13 & (3,3) are_congruent_mod 13 by NEWTON: 10, INT_1: 11;

      then (((3 |^ 69) * 3),(1 * 3)) are_congruent_mod 13 by INT_1: 18;

      then ((3 |^ (69 + 1)),(1 * 3)) are_congruent_mod 13 by NEWTON: 6;

      then (((2 |^ 70) + (3 |^ 70)),(( - 3) + 3)) are_congruent_mod 13 by dsi, INT_1: 16;

      then 13 divides (((2 |^ 70) + (3 |^ 70)) - 0 ) by INT_1:def 4;

      hence thesis;

    end;

    begin

    theorem :: NUMBER01:10

    ((11 * 31) * 61) divides ((20 |^ 15) - 1)

    proof

      (20 |^ 15) >= (1 |^ 15) by PREPOWER: 9;

      then (20 |^ 15) >= 1 by NEWTON: 10;

      then ((20 |^ 15) - 1) >= (1 - 1) by XREAL_1: 9;

      then ((20 |^ 15) - 1) in NAT by INT_1: 3;

      then

      reconsider D = ((20 |^ 15) - 1) as Nat;



       jp: 11 is prime by NAT_4: 27;



       tp: 31 is prime by NUMERAL2: 24;



       sp: 61 is prime by NUMERAL2: 29;



       jtc: (11,31) are_coprime by jp, tp, INT_2: 30;



       cp1: (11,61) are_coprime by jp, sp, INT_2: 30;



       cp2: (31,61) are_coprime by tp, sp, INT_2: 30;



       jsc: ((11 * 31),61) are_coprime by cp1, cp2, EULER_1: 14;

      (2 |^ 1) = 2 by NEWTON: 5;

      then (2 |^ (1 + 1)) = (2 * 2) by NEWTON: 6;

      then (2 |^ (2 + 1)) = (2 * 4) by NEWTON: 6;

      then (2 |^ (3 + 1)) = (2 * 8) by NEWTON: 6;

      then

       dc: (2 |^ (4 + 1)) = (2 * 16) & (3 * 11) = (32 - ( - 1)) by NEWTON: 6;

      then

       dp: ((2 |^ 5),( - 1)) are_congruent_mod 11 by INT_1:def 5;

      5 = ((2 * 2) + 1);

      then

       po: 5 is odd;

      reconsider J = ( - 1) as Integer;

      (11 * 1) = (10 - ( - 1));

      then (10,( - 1)) are_congruent_mod 11 by INT_1:def 5;

      then ((10 |^ 5),(( - 1) |^ 5)) are_congruent_mod 11 by GR_CY_3: 34;

      then ((10 |^ 5),( - 1)) are_congruent_mod 11 by po, POLYFORM: 9;

      then (((2 |^ 5) * (10 |^ 5)),(J * J)) are_congruent_mod 11 by dp, INT_1: 18;

      then (((2 * 10) |^ 5),1) are_congruent_mod 11 by NEWTON: 7;

      then (((20 |^ 5) |^ 3),(1 |^ 3)) are_congruent_mod 11 by GR_CY_3: 34;

      then ((20 |^ (5 * 3)),(1 |^ 3)) are_congruent_mod 11 by NEWTON: 9;

      then ((20 |^ 15),1) are_congruent_mod 11 by NEWTON: 10;

      then

       jd: 11 divides D by INT_1:def 4;

      (31 * 4) = (121 - ( - 3));

      then

       sd: (121,( - 3)) are_congruent_mod 31 by INT_1:def 5;

      (31 * 1) = (33 - 2);

      then

       tt: (33,2) are_congruent_mod 31 by INT_1:def 5;

      (31 * 1) = (20 - ( - 11));

      then

       dw: (20,( - 11)) are_congruent_mod 31 by INT_1:def 5;

      then ((20 |^ 2),(( - 11) |^ 2)) are_congruent_mod 31 by GR_CY_3: 34;

      then ((20 |^ 2),(( - 11) * ( - 11))) are_congruent_mod 31 by WSIERP_1: 1;

      then ((20 |^ 2),( - 3)) are_congruent_mod 31 by sd, INT_1: 15;

      then ((20 * (20 |^ 2)),(( - 11) * ( - 3))) are_congruent_mod 31 by dw, INT_1: 18;

      then ((20 |^ (2 + 1)),33) are_congruent_mod 31 by NEWTON: 6;

      then ((20 |^ 3),2) are_congruent_mod 31 by tt, INT_1: 15;

      then (((20 |^ 3) |^ 5),(2 |^ 5)) are_congruent_mod 31 by GR_CY_3: 34;

      then

       dwp: ((20 |^ (3 * 5)),(2 |^ 5)) are_congruent_mod 31 by NEWTON: 9;

      (31 * 1) = ((2 |^ 5) - 1) by dc;

      then ((2 |^ 5),1) are_congruent_mod 31 by INT_1:def 5;

      then ((20 |^ 15),1) are_congruent_mod 31 by dwp, INT_1: 15;

      then 31 divides D by INT_1:def 4;

      then

       jtd: (11 * 31) divides D by jd, jtc, PEPIN: 4;

      (3 |^ (2 + 2)) = ((3 |^ 2) * (3 |^ 2)) by NEWTON: 8

      .= ((3 * 3) * (3 |^ 2)) by WSIERP_1: 1

      .= ((3 * 3) * (3 * 3)) by WSIERP_1: 1;

      then (61 * 1) = ((3 |^ 4) - 20);

      then ((3 |^ 4),20) are_congruent_mod 61 by INT_1:def 5;

      then (((3 |^ 4) |^ 15),(20 |^ 15)) are_congruent_mod 61 by GR_CY_3: 34;

      then ((3 |^ (4 * 15)),(20 |^ 15)) are_congruent_mod 61 by NEWTON: 9;

      then

       f: ((20 |^ 15),(3 |^ 60)) are_congruent_mod 61 by INT_1: 14;

      (3,61) are_coprime by sp, PEPIN: 41, INT_2: 30;

      then ((3 |^ ( Euler 61)) mod 61) = 1 & 60 = (61 - 1) by EULER_2: 18;

      then ((3 |^ 60) mod 61) = 1 by EULER_1: 20, sp;

      then ((3 |^ 60),1) are_congruent_mod 61 by NAT_6: 10;

      then ((20 |^ 15),1) are_congruent_mod 61 by f, INT_1: 15;

      then 61 divides D by INT_1:def 4;

      then ((11 * 31) * 61) divides D by jsc, jtd, PEPIN: 4;

      hence thesis;

    end;

    theorem :: NUMBER01:11



     lemdiv: for a be Integer, m be Nat holds (a - 1) divides ((a |^ m) - 1)

    proof

      let a be Integer, m be Nat;

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

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

      then

       z: P[ 0 ] by INT_2: 12;

       i:

      now

        let k be Nat;

        assume P[k];

        then

        consider l be Integer such that

         l: ((a |^ k) - 1) = ((a - 1) * l) by INT_1:def 3;

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

        .= ((a - 1) * ((a |^ k) + l)) by l;

        hence P[(k + 1)] by INT_1:def 3;

      end;

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

      hence thesis;

    end;

    theorem :: NUMBER01:12



     lempowers: for a be Nat, m be positive Integer, f be XFinSequence of INT st a > 1 & ( len f) = (m - 1) & for i be Nat st i in ( dom f) holds (f . i) = ((a |^ (i + 1)) - 1) holds (((a |^ m) - 1) div (a - 1)) = (( Sum f) + m)

    proof

      let a be Nat, m be positive Integer, f be XFinSequence of INT such that

       f: a > 1 & ( len f) = (m - 1) & for i be Nat st i in ( dom f) holds (f . i) = ((a |^ (i + 1)) - 1);



       a: (a - 1) <> 0 by f;

      reconsider a1 = (a - 1) as Nat by f, INT_1: 74;

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

      then

      reconsider m0 = m as Nat by POLYFORM: 3;

      reconsider m1 = (m0 - 1) as Nat by INT_1: 74;

      defpred P[ Nat] means for f be XFinSequence of INT st ( len f) = $1 & for i be Nat st i in ( dom f) holds (f . i) = ((a |^ (i + 1)) - 1) holds (((a |^ ($1 + 1)) - 1) div (a - 1)) = (( Sum f) + ($1 + 1));



       z: P[ 0 ]

      proof

        let f0 be XFinSequence of INT such that

         f0: ( len f0) = 0 & for i be Nat st i in ( dom f0) holds (f0 . i) = ((a |^ (i + 1)) - 1);

        f0 = {} by f0;

        then

         sz: ( Sum f0) = 0 ;



        thus (((a |^ ( 0 + 1)) - 1) div (a - 1)) = ((a - 1) div (a - 1)) by NEWTON: 5

        .= (( Sum f0) + ( 0 + 1)) by sz, a, INT_1: 49;

      end;

       k:

      now

        let k be Nat;

        assume

         pk: P[k];

        thus P[(k + 1)]

        proof

          let f1 be XFinSequence of INT such that

           f1: ( len f1) = (k + 1) & for i be Nat st i in ( dom f1) holds (f1 . i) = ((a |^ (i + 1)) - 1);

          set fk = (f1 | k);



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

          then

           df: ( dom fk) = k by f1, AFINSQ_1: 11;

          k in ( Segm (k + 1)) & ( dom f1) = (k + 1) by f1, km, NAT_1: 44;

          then

           kd: k in ( dom f1);



           lek: ( len fk) = k by km, f1, AFINSQ_1: 54;

          now

            let i be Nat;

            assume

             idk: i in ( dom fk);

            ( dom fk) c= ( dom f1) by RELAT_1: 60;

            then

             idf: i in ( dom f1) by idk;



            thus (fk . i) = (f1 . i) by df, km, idk, f1, AFINSQ_1: 53

            .= ((a |^ (i + 1)) - 1) by f1, idf;

          end;

          then

           pek: (((a |^ (k + 1)) - 1) div (a - 1)) = (( Sum fk) + (k + 1)) by pk, lek;



           sf: ( Sum <%(f1 . k)%>) = (f1 . k) by AFINSQ_2: 53;

          f1 = (fk ^ <%(f1 . k)%>) by f1, AFINSQ_1: 56;

          then

           ss: ( Sum f1) = (( Sum fk) + (f1 . k)) by sf, AFINSQ_2: 55;



           ld: (a - 1) divides ((a |^ ((k + 1) + 1)) - 1) & (a - 1) divides ((a |^ (k + 1)) - 1) by lemdiv;



          hence (((a |^ ((k + 1) + 1)) - 1) div (a - 1)) = (((a |^ ((k + 1) + 1)) - 1) / a1) by RING_3: 6

          .= ((((((a |^ (k + 1)) * a) + (a |^ (k + 1))) - (a |^ (k + 1))) - 1) / a1) by NEWTON: 6

          .= ((((a |^ (k + 1)) * (a - 1)) + ((a |^ (k + 1)) - 1)) / a1)

          .= ((((a |^ (k + 1)) * (a - 1)) / a1) + (((a |^ (k + 1)) - 1) / a1)) by XCMPLX_1: 62

          .= ((a |^ (k + 1)) + (((a |^ (k + 1)) - 1) / a1)) by a, XCMPLX_1: 89

          .= ((a |^ (k + 1)) + (((a |^ (k + 1)) - 1) div a1)) by ld, RING_3: 6

          .= ((((a |^ (k + 1)) - 1) + ( Sum fk)) + ((k + 1) + 1)) by pek

          .= (((f1 . k) + ( Sum fk)) + ((k + 1) + 1)) by f1, kd

          .= (( Sum f1) + ((k + 1) + 1)) by ss;

        end;

      end;

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

      then (((a |^ (m1 + 1)) - 1) div (a - 1)) = (( Sum f) + (m1 + 1)) by f;

      hence (((a |^ m) - 1) div (a - 1)) = (( Sum f) + m);

    end;

    begin

    theorem :: NUMBER01:13

    for m be positive Integer, a be Nat st a > 1 holds ((((a |^ m) - 1) div (a - 1)) gcd (a - 1)) = ((a - 1) gcd m)

    proof

      let m be positive Integer, a be Nat such that

       a: a > 1;

      set d = ((((a |^ m) - 1) div (a - 1)) gcd (a - 1));

      set d1 = ((a - 1) gcd m);

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

      then

      reconsider m0 = m as Nat by POLYFORM: 3;

      reconsider m1 = (m0 - 1) as Nat by INT_1: 74;

      deffunc F( Nat) = ((a |^ ($1 + 1)) - 1);

      consider f be XFinSequence such that

       f: ( len f) = m1 & for i be Nat st i in m1 holds (f . i) = F(i) from AFINSQ_1:sch 2;

      ( rng f) c= INT

      proof

        let o be object;

        assume o in ( rng f);

        then

        consider x be object such that

         x: x in ( dom f) & o = (f . x) by FUNCT_1:def 3;

        reconsider x as Nat by x;

        o = ((a |^ (x + 1)) - 1) by f, x;

        hence o in INT by INT_1:def 2;

      end;

      then

      reconsider f as XFinSequence of INT by RELAT_1:def 19;



       d2: d divides (a - 1) & d divides (((a |^ m) - 1) div (a - 1)) by INT_2:def 2;

      now

        let i be Nat;

        assume i in ( dom f);

        then (f . i) = ((a |^ (i + 1)) - 1) by f;

        hence (a - 1) divides (f . i) by lemdiv;

      end;

      then

       ad: (a - 1) divides ( Sum f) by NUMERAL2: 16;

      then

       ds: d divides ( Sum f) by d2, INT_2: 9;



       ss: (((a |^ m) - 1) div (a - 1)) = (( Sum f) + m) by a, f, lempowers;

      then d divides (( Sum f) + m) by d2;

      then

       d1: d divides m by ds, INT_2: 1;

      now

        let q be Integer;

        assume

         q: q divides (a - 1) & q divides m;

        then q divides ( Sum f) by ad, INT_2: 9;

        then q divides (((a |^ m) - 1) div (a - 1)) by ss, q, WSIERP_1: 4;

        hence q divides d by q, INT_2:def 2;

      end;

      hence d = d1 by d1, d2, INT_2:def 2;

    end;

    begin

    theorem :: NUMBER01:14

    for s1,s2 be XFinSequence of NAT , n be Nat st (( len s1) = (n + 1) & for i be Nat st i in ( dom s1) holds (s1 . i) = (i |^ 5)) & (( len s2) = (n + 1) & for i be Nat st i in ( dom s2) holds (s2 . i) = (i |^ 3)) holds ( Sum s2) divides (3 * ( Sum s1))

    proof

      let s1,s2 be XFinSequence of NAT , n be Nat;

      assume that

       s1: ( len s1) = (n + 1) & for i be Nat st i in ( dom s1) holds (s1 . i) = (i |^ 5) and

       s2: ( len s2) = (n + 1) & for i be Nat st i in ( dom s2) holds (s2 . i) = (i |^ 3);

      deffunc F( Nat) = ($1 |^ 3);

      consider S2 be Real_Sequence such that

       S2: for i be Nat holds (S2 . i) = F(i) from SEQ_1:sch 1;

      ( Segm (n + 1)) c= NAT & ( dom S2) = NAT by MEMBERED: 6, PARTFUN1:def 2;

      then ( dom (S2 | ( Segm (n + 1)))) = ( Segm (n + 1)) by RELAT_1: 62;

      then

       dr: ( dom (S2 | ( Segm (n + 1)))) = ( dom s2) by s2;

      now

        let o be object;

        assume

         o: o in ( dom s2);

        then o in ( Segm (n + 1)) by s2;

        then o is natural by MEMBERED:def 6;

        then

        reconsider on = o as Nat by TARSKI: 1;



        thus (s2 . o) = (on |^ 3) by s2, o

        .= (S2 . on) by S2

        .= ((S2 | ( Segm (n + 1))) . o) by o, dr, FUNCT_1: 47;

      end;

      then s2 = (S2 | ( Segm (n + 1))) by dr, FUNCT_1: 2;

      then ( Sum s2) = (( Partial_Sums S2) . n) by RVSUM_4: 4;

      then

       ss: ( Sum s2) = (((n |^ 2) * ((n + 1) |^ 2)) / 4) by S2, SERIES_2: 15;

      deffunc G( Nat) = ($1 |^ 5);

      consider S1 be Real_Sequence such that

       S1: for i be Nat holds (S1 . i) = G(i) from SEQ_1:sch 1;

      ( Segm (n + 1)) c= NAT & ( dom S1) = NAT by MEMBERED: 6, PARTFUN1:def 2;

      then ( dom (S1 | ( Segm (n + 1)))) = ( Segm (n + 1)) by RELAT_1: 62;

      then

       ds: ( dom (S1 | ( Segm (n + 1)))) = ( dom s1) by s1;

      now

        let o be object;

        assume

         o: o in ( dom s1);

        then o in ( Segm (n + 1)) by s1;

        then o is natural by MEMBERED:def 6;

        then

        reconsider on = o as Nat by TARSKI: 1;



        thus (s1 . o) = (on |^ 5) by s1, o

        .= (S1 . on) by S1

        .= ((S1 | ( Segm (n + 1))) . o) by o, ds, FUNCT_1: 47;

      end;

      then s1 = (S1 | ( Segm (n + 1))) by ds, FUNCT_1: 2;

      then ( Sum s1) = (( Partial_Sums S1) . n) by RVSUM_4: 4;

      then ( Sum s1) = ((((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12) by S1, SERIES_2: 19;

      then (3 * ( Sum s1)) = ((((2 * (n |^ 2)) + (2 * n)) - 1) * ( Sum s2)) by ss;

      hence ( Sum s2) divides (3 * ( Sum s1)) by INT_1:def 3;

    end;

    theorem :: NUMBER01:15



     lemman02: for a,b be Integer, m be positive Nat holds ( Sum ((a,b) In_Power m)) = (((a |^ m) + (b |^ m)) + ( Sum ((((a,b) In_Power m) | m) /^ 1)))

    proof

      let a,b be Integer;

      let m be positive Nat;

      ( len ((a,b) In_Power m)) = (m + 1) by NEWTON:def 4;



      then ( Sum ((a,b) In_Power m)) = ((( Sum ((((a,b) In_Power m) | m) /^ 1)) + (((a,b) In_Power m) . 1)) + (((a,b) In_Power m) . (m + 1))) by NEWTON02: 115

      .= ((( Sum ((((a,b) In_Power m) | m) /^ 1)) + (a |^ m)) + (((a,b) In_Power m) . (m + 1))) by NEWTON: 28

      .= ((( Sum ((((a,b) In_Power m) | m) /^ 1)) + (a |^ m)) + (b |^ m)) by NEWTON: 29;

      hence thesis;

    end;

    theorem :: NUMBER01:16



     lemmandiv: for n,k be Nat st n is odd holds n divides ((k |^ n) + ((n - k) |^ n))

    proof

      let n,k be Nat;

      assume

       no: n is odd;

      then

      reconsider p = n as positive Nat;



       kk: ((k |^ p) + ((p + ( - k)) |^ p)) = ((k |^ p) + ( Sum ((p,( - k)) In_Power p))) by NEWTON: 30

      .= ((k |^ p) + (((p |^ p) + (( - k) |^ p)) + ( Sum ((((p,( - k)) In_Power p) | p) /^ 1)))) by lemman02

      .= ((k |^ p) + (((p |^ p) + ( - (k |^ p))) + ( Sum ((((p,( - k)) In_Power p) | p) /^ 1)))) by no, POWER: 2

      .= ((p |^ p) + ( Sum ((((p,( - k)) In_Power p) | p) /^ 1)));



       pp: p divides (p |^ p) by NAT_3: 3;

      reconsider S = ( Sum ((((p,( - k)) In_Power p) | p) /^ 1)) as Integer;

      reconsider f = ((((p,( - k)) In_Power p) | p) /^ 1) as INT -valued FinSequence;

      now

        let o be Nat;

        assume

         o: o in ( dom f);

        then f <> {} ;

        then 1 <= ( len (((p,( - k)) In_Power p) | p)) by RFINSEQ:def 1;

        then

         rf: ( len f) = (( len (((p,( - k)) In_Power p) | p)) - 1) & for l be Nat st l in ( dom f) holds (f . l) = ((((p,( - k)) In_Power p) | p) . (l + 1)) by RFINSEQ:def 1;



         elen: ( len ((p,( - k)) In_Power p)) = (n + 1) & for i,l,m be Nat st i in ( dom ((p,( - k)) In_Power p)) & m = (i - 1) & l = (n - m) holds (((p,( - k)) In_Power p) . i) = (((n choose m) * (p |^ l)) * (( - k) |^ m)) by NEWTON:def 4;



         x: ( 0 + 1) <= (o + 1) by XREAL_1: 6;



         pz: (p + 0 ) <= (n + 1) by XREAL_1: 6;

        ( len (((p,( - k)) In_Power p) | p)) = p by elen, pz, FINSEQ_1: 17;

        then

         lp: ( len f) = (p - 1) by rf;

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

        then o <= (p - 1) by lp, FINSEQ_1: 1;

        then

         op: (o + 1) <= ((p - 1) + 1) by XREAL_1: 6;

        then

         el: (o + 1) in ( Seg p) by x;

        set i = (o + 1);

        i < (p + 1) by NAT_1: 13, op;

        then i in ( Seg ( len ((p,( - k)) In_Power p))) by x, elen;

        then

         i: i in ( dom ((p,( - k)) In_Power p)) by FINSEQ_1:def 3;

        reconsider m = (i - 1) as Nat;



         po: (p - o) >= ((o + 1) - o) by op, XREAL_1: 9;

        then

        reconsider l = (n - m) as Nat;



         fo: (f . o) = ((((p,( - k)) In_Power p) | p) . (o + 1)) by o, rf

        .= (((p,( - k)) In_Power p) . (o + 1)) by el, FUNCT_1: 49

        .= (((n choose m) * (p |^ l)) * (( - k) |^ m)) by elen, i

        .= ((p |^ l) * ((n choose m) * (( - k) |^ m)));

        p divides (p |^ l) by po, NAT_3: 3;

        hence n divides (f . o) by fo, INT_2: 2;

      end;

      then n divides ( Sum f) by NEWTON04: 80;

      then n divides ((k |^ n) + ((n + ( - k)) |^ n)) by kk, pp, WSIERP_1: 4;

      hence n divides ((k |^ n) + ((n - k) |^ n));

    end;

    begin

    theorem :: NUMBER01:17

    for s be FinSequence of NAT , n be Nat st n > 1 & ( len s) = (n - 1) & for i be Nat st i in ( dom s) holds (s . i) = (i |^ n) holds n is odd implies n divides ( Sum s)

    proof

      let s be FinSequence of NAT , n be Nat such that

       n: n > 1 & ( len s) = (n - 1) and

       s: for i be Nat st i in ( dom s) holds (s . i) = (i |^ n);

      ( rng s) c= REAL ;

      then

      reconsider s0 = s as FinSequence of REAL by FINSEQ_1:def 4;

      reconsider ser = ( Sum s) as Nat by TARSKI: 1;



       d: ( dom s) = ( dom ( Rev s)) by FINSEQ_5: 57;



       d2: ( dom (s + ( Rev s))) = (( dom s) /\ ( dom ( Rev s))) by VALUED_1:def 1

      .= ( dom s) by d;



      then ( Seg ( len (s + ( Rev s)))) = ( dom s) by FINSEQ_1:def 3

      .= ( Seg ( len s)) by FINSEQ_1:def 3;

      then

       l1: ( len s0) = ( len (s0 + ( Rev s0))) by FINSEQ_1: 6;

      ( Seg ( len s)) = ( dom ( Rev s)) by d, FINSEQ_1:def 3;

      then

       l2: ( len s0) = ( len ( Rev s0)) by FINSEQ_1:def 3;

      for k be Nat st k in ( dom s0) holds ((s0 + ( Rev s0)) . k) = ((s0 . k) + (( Rev s0) . k)) by d2, VALUED_1:def 1;



      then

       ss: ( Sum (s0 + ( Rev s0))) = (( Sum s0) + ( Sum ( Rev s0))) by l1, l2, ENTROPY1: 7

      .= (( Sum s) + ( Sum s)) by POLYNOM3: 3

      .= (2 * ( Sum s));

      ( rng (s + ( Rev s))) c= NAT

      proof

        let o be object;

        assume o in ( rng (s + ( Rev s)));

        then

        consider a be object such that

         a: a in ( dom (s + ( Rev s))) & o = ((s + ( Rev s)) . a) by FUNCT_1:def 3;

        reconsider a as Nat by a;

        o = ((s . a) + (( Rev s) . a)) by a, VALUED_1:def 1;

        hence o in NAT by ORDINAL1:def 12;

      end;

      then

      reconsider sr = (s + ( Rev s)) as FinSequence of NAT by FINSEQ_1:def 4;

      thus n is odd implies n divides ( Sum s)

      proof

        assume

         no: n is odd;

        (2 |^ 1) = 2 by NEWTON: 5;

        then

         2c: (2,n) are_coprime by NAT_5: 3, no;

        now

          let k be Nat;

          assume

           k: k in ( dom sr);



          then

           serek: (sr . k) = ((s . k) + (( Rev s) . k)) by VALUED_1:def 1

          .= ((k |^ n) + (( Rev s) . k)) by d2, k, s

          .= ((k |^ n) + (s . ((( len s) - k) + 1))) by FINSEQ_5: 58, k, d2

          .= ((k |^ n) + (s . (n - k))) by n;

          k in ( Seg ( len s)) by k, d2, FINSEQ_1:def 3;

          then

           kk: 1 <= k & k <= (n - 1) by FINSEQ_1: 1, n;

          then

           nk: (n - k) <= (n - 1) by XREAL_1: 10;

          (k + (1 - k)) <= ((n - 1) + (1 - k)) by kk, XREAL_1: 6;

          then

           jk: 1 <= (n - k);

          then

          reconsider nik = (n - k) as Nat;

          nik in ( Seg ( len s)) by n, jk, nk;

          then (n - k) in ( dom s) by FINSEQ_1:def 3;

          then (sr . k) = ((k |^ n) + ((n - k) |^ n)) by serek, s;

          hence n divides (sr . k) by no, lemmandiv;

        end;

        then n divides ( Sum sr) by NEWTON04: 80;

        then n divides (2 * ( Sum s)) by ss;

        then n divides ser by 2c, EULER_1: 13;

        hence n divides ( Sum s);

      end;

    end;