:: The Perfect Number Theorem and Wilson's Theorem
::  by Marco Riccardi

environ

 vocabularies NUMBERS, ORDINAL1, XCMPLX_0, INT_2, NAT_3, XXREAL_0, XBOOLE_0,
      NEWTON, ARYTM_3, ARYTM_1, NAT_1, RELAT_1, CARD_1, ABIAN, SUBSET_1,
      FINSET_1, FINSEQ_1, FUNCT_1, FINSEQ_3, TARSKI, CARD_3, ORDINAL4, FUNCT_2,
      FINSEQ_2, FUNCOP_1, MOEBIUS1, COMPLEX1, INT_1, REALSET1, SQUARE_1, INT_5,
      ZFMISC_1, POWER, REAL_1, PRE_POLY, UPROOTS, BHSP_5, CLASSES1, PARTFUN1,
      RFUNCT_3, BINOP_2, PROB_1, WAYBEL29, MSSUBFAM, TOPGEN_1, EULER_1, NAT_5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCOP_1, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS,
      FINSEQ_1, FINSEQ_3, EXTREAL1, XCMPLX_0, XREAL_0, NAT_1, INT_1, INT_2,
      NAT_D, RVSUM_1, REAL_1, SQUARE_1, XXREAL_0, NEWTON, FINSEQ_2, ABIAN,
      PEPIN, INT_5, FINSEQOP, ENUMSET1, FINSET_1, COMPLEX1, NAT_3, DOMAIN_1,
      POWER, MOEBIUS1, BHSP_5, EULER_1, WSIERP_1, BINOP_1, RECDEF_1, UPROOTS,
      BINOP_2, FUNCT_3, RFUNCT_3, CLASSES1, PRE_POLY;
 constructors WELLORD2, REAL_1, NAT_D, BINOP_2, WSIERP_1, ABIAN, EULER_1,
      PEPIN, INT_5, RECDEF_1, MOEBIUS1, FINSEQOP, EXTREAL1, UPROOTS, NAT_3,
      REALSET1, POWER, BHSP_5, CALCUL_2, SUPINF_1, RFUNCT_3, CLASSES1, BINOP_1,
      NUMBERS;
 registrations XBOOLE_0, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RVSUM_1, VALUED_0, NEWTON,
      ABIAN, FUNCT_1, ZFMISC_1, SUBSET_1, MOEBIUS1, FUNCT_2, PRE_CIRC, RELAT_1,
      SQUARE_1, CARD_1, PREPOWER, NAT_3, PRE_POLY, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 equalities NEWTON, FINSEQ_1, FINSEQ_3, EULER_1, MOEBIUS1, ORDINAL1;
 expansions TARSKI, FINSEQ_1;
 theorems XBOOLE_0, XBOOLE_1, XXREAL_0, XREAL_1, XCMPLX_1, NAT_1, NAT_D,
      RELAT_1, FUNCT_1, INT_1, INT_2, INT_4, INT_5, NEWTON, EULER_1, EULER_2,
      FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, RVSUM_1, WSIERP_1, ORDINAL1,
      IDEA_1, INT_6, FIB_NUM3, POWER, PEPIN, SQUARE_1, CARD_1, CARD_2,
      ZFMISC_1, FINSEQ_4, JGRAPH_1, TARSKI, COMPLEX1, ABSVALUE, MOEBIUS1,
      CARD_3, MESFUNC3, FUNCT_2, EXTREAL1, FINSEQOP, FUNCOP_1, BAGORDER,
      RELSET_1, WELLORD2, PARTFUN1, BHSP_5, UPROOTS, RFINSEQ, BINOP_2, BINOP_1,
      FUNCT_3, RFUNCT_3, NAT_4, NAT_3, XREAL_0, ABIAN, ENUMSET1, MONOID_1,
      CLASSES1, PRE_POLY, XTUPLE_0, NUMBERS;
 schemes NAT_1, FUNCT_1, FUNCT_2, BINOP_2, FINSEQ_1;

begin :: Preliminaries

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 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 being Nat holds P[k] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem 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 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 being 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 Th4:
  {n} is finite Subset of NAT by ORDINAL1:def 12,ZFMISC_1:31;

theorem 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;

:: FinSequence

reserve f for FinSequence;
reserve x,X,Y for set;

theorem 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 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 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 being 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 Th9:
  for f1 being FinSequence of NAT, f2 being 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 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 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 being 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 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;

:: like FINSEQ_3:126

theorem Th13:
  for f being FinSequence of NAT holds f is FinSequence of REAL
proof
  let f be FinSequence of NAT;
  for n being Nat st n in dom f holds f.n in REAL by XREAL_0:def 1;
  hence thesis by FINSEQ_2:12;
end;

:: NatDivisors

reserve n1,n2,m1,m2 for Nat;

theorem 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,27;
  then n gcd m <> 1 by A8,A6,XXREAL_0:1;
  hence contradiction by A7,INT_2:def 3;
end;

theorem 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 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 being 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 being 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 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 being 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 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 Th19:
  p is prime implies NatDivisors(p|^n) = {p|^k where k is Element
  of NAT : k <= n}
proof
  assume
A1: p is prime;
  for x being object holds x in NatDivisors(p|^n) iff x in {p|^k where k is
  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 is Element of NAT : k <= n};
    end;
    assume x in {p|^k where k is 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 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
  p is prime implies p |-count(n0 gcd m0) = min(p |-count n0,p |-count
  m0) by Lm1;

:: lemmas

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;

:: Lm12 by WSIERP_1

Lm5: for a being Element of NAT, fs being FinSequence holds a in dom fs
implies ex fs1,fs2 being 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;

:: Lm13 by WSIERP_1

Lm6: for a being Element of NAT, fs,fs1,fs2 being FinSequence, v being 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;

:: Lm17 by WSIERP_1

Lm7: for fs being 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;

:: Lm18 in WSIERP_1

Lm8: for a being Nat, ft being 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 being 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,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 being 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 being 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 being 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 being Nat st for n9 being Nat st n9 < k9
  holds P[n9] holds P[k9]
  proof
    let k9 be Nat;
    assume
A2: for n9 being 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 being Nat holds P[n9] from NAT_1:sch 4(A1);
  then P[n9];
  hence thesis;
end;

begin :: Wilson's Theorem
:: Number Theory (Andrews) p.61-66

::$N Wilson's Theorem
theorem
  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 being Nat st l9 in rng f & l9<>1 holds ex k9
being 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 :: All Primes (1 mod 4) Equal the Sum of Two Squares
:: Proofs from THE BOOK (Aigner-Ziegler) p.19

::$N All Primes (1 mod 4) Equal the Sum of Two Squares
theorem
  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,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 being Integer holds ex x9,x99,y9,y99 being 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 being 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 being object st x in A ex y being 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,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 being 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 :: The Sum of Divisors Function

definition
  let I be set;
  let f be Function of I, NAT;
  let J be finite Subset of I;
  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 Th24:
  for f being sequence of NAT, F being sequence of REAL,
  J being 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 Th25:
  for I being non empty set, F being PartFunc of I, REAL, f being
Function of I, NAT, J being 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 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 Th27:
 for j being 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 being 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 being set,j being object, f,g being Function of I, NAT, J,K
being 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 being Nat st for n being Nat st n < k holds P[n] holds P[k]
  proof
    let k be Nat;
    assume
A2: for n being 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 being Nat holds P[k] from NAT_1:sch 4(A1);
  then P[card K];
  hence thesis;
end;

theorem Th28:
  Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K)
proof
  defpred P[Nat] means for I being set, f,g being Function of I, NAT, J,K
being finite Subset of I st $1 = card J holds Sum((multnat*[:f,g:])|[:J,K:]) =
  Sum(f|J) * Sum(g|K);
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
  proof
    let k be Nat;
    assume
A2: for n being 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 being Nat holds P[k] from NAT_1:sch 4(A1);
  then P[card J];
  hence thesis;
end;

definition
  let k be natural Number;
  func EXP(k) -> sequence of NAT means
  :Def1:
  for n being 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 being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
    take f;
    for n being 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 being Nat holds f1.n = n|^k;
    assume
A3: for n being Nat holds f2.n = n|^k;
    for x being 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;
  func sigma(k,n) -> Element of NAT means
  :Def2:
  for m being 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 being Element of NAT holds (not n <> 0 & n1 = 0 & n2 = 0
    implies n1 = n2) & (n <> 0 & (for m being non zero Nat st n = m
holds n1 = Sum((EXP k)|NatDivisors m)) & (for m being 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 being 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 being Element of NAT st for m being 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;
  func Sigma(k) -> sequence of NAT means
  :Def3:
  for n being 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 being 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 being Nat holds f1.n = sigma(k,n);
    assume
A3: for n being Nat holds f2.n = sigma(k,n);
    for x being 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;
  func sigma n -> Element of NAT equals
  sigma(1,n);
  correctness;
end;

theorem 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 being 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 Th30:
  p is prime implies sigma(p|^n) = (p|^(n+1) - 1)/(p - 1)
proof
  defpred P[Nat] means for p being 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 is 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 being 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 is 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 is 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 is 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 is 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 is 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 being Nat holds P[k] from NAT_1:sch 2(A17,A1);
  hence thesis;
end;

theorem 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 being 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 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 being 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 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 being 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;
  attr f is multiplicative means

  for n0,m0 being non zero Nat
  st n0,m0 are_coprime holds f.(n0*m0) = f.n0 * f.m0;
end;

theorem Th34:
  for f,F being 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 being 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 being 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 being 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 being 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 being 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 being 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 Th35:
  EXP(k) is multiplicative
proof
  for n,m being 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 Th36:
  Sigma(k) is multiplicative
proof
  for n being 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 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 :: The Perfect Number Theorem

definition
  let n0 be non zero natural Number;
  attr n0 is perfect means
  sigma n0 = 2 * n0;
end;

:: Fundamentals of Number Theory (LeVeque) p.123
:: Euclid

theorem
  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;

:: Euler

::$N The Perfect Number Theorem
theorem
  n0 is even & n0 is perfect implies ex p being 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 :: A Formula involving Euler's Function

definition
  func Euler_phi -> sequence of NAT means
  :Def7:
  for k being Element of NAT holds it.k = Euler(k);
  existence
  proof
    ex f being sequence of NAT st for k being 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 being Element of NAT
    holds f1.x = Euler(x)) & (for x being 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 being Element of NAT holds f1.k = Euler(k))& for k being
    Element of NAT holds f2.k = Euler(k);
    hence thesis by A1;
  end;
end;

:: Number Theory (Andrews) p.76

theorem
  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 is Element of NAT: ex h being
  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 being Nat st k in X ex x being Element of bool X st P[k
  ,x]
  proof
    let k be Nat;
    set X9 = {i where i is Element of NAT: ex h being Nat st i in X
    & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h};
    for x being 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 being 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 being 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 being 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 is Element of NAT : k9,l are_coprime & l >= 1 &
    l <= k9};
    set Z = {i where i is Element of NAT: ex h being 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 being 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 being Element of Y holds f.d = F(d) from
    FUNCT_1:sch 4;
    for y being 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 being 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 being 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 being 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 is Element of NAT: ex h being 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 is Element of NAT: ex h being 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 being 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 being 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 is Element of NAT: ex h being 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 is Element of NAT: ex h being 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 being 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 being 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 being 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 is Element of NAT: ex h9 being 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;

{"subset_name": "curated", "file": "formal/mizar/nat_5.miz"}