:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
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,
NUMBER09;
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
Sgm (dom f \ {n}) is one-to-one by FINSEQ_3:92;
hence thesis;
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;
aa: Y c= dom f1 by A1,XBOOLE_1:7;
then Y is included_in_Seg by A8;
then rng Sgm Y c= dom f1 by aa,FINSEQ_1:def 14;
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 X is included_in_Seg by A8;
then rng Sgm X c= dom f1 by A11,FINSEQ_1:def 14;
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;
A7: rng Sgm Y = Y by FINSEQ_1:def 14;
then reconsider f3 as FinSequence of REAL by A6,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 FINSEQ_1:def 14;
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;
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;
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;
end;
registration let a be Nat;
reduce a gcd 0 to a;
reducibility by NEWTON:52;
end;
registration let a be Integer;
reduce a gcd 1 to 1;
reducibility by WSIERP_1:8;
end;
theorem Th17:
for n0,m0 being Nat st
n0,m0 are_coprime holds k gcd (n0*m0) = (k gcd n0)*(k gcd m0)
proof
let n0,m0 be Nat;
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 & n0 <> 0 & m0 <> 0;
then reconsider k9 = k,m0,n0 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 thesis by NAT_4:21;
end;
suppose
A8: k <> 0 & n0 = 0;
m0 gcd n0 = 1 by A1,INT_2:def 3; then
m0 = 1 by A8; then
A9: k gcd m0 = 1;
k gcd (n0*m0) = k gcd 0 by A8
.= k
.= (k gcd n0)*(k gcd m0) by A8,A9;
hence thesis;
end;
suppose
A8: k <> 0 & m0 = 0;
m0 gcd n0 = 1 by A1,INT_2:def 3; then
n0 = 1 by A8; then
A9: k gcd n0 = 1;
k gcd (n0*m0) = k gcd 0 by A8
.= k
.= (k gcd n0)*(k gcd m0) by A8,A9;
hence thesis;
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;
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;
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;
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
::$L https://en.wikipedia.org/wiki/Wilson's_theorem 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;
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 14;
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 14;
end;
l! = Product Sgm(Seg l) & rng f c= Seg l by FINSEQ_1:def 14,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
::$L https://en.wikipedia.org/wiki/Fermat's_theorem_on_sums_of_two_squares Fermat's theorem on sums 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;
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;
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; :: redefines | (RELAT_1, definition)
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 included_in_Seg Subset of NAT st f = F 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 included_in_Seg Subset of NAT;
assume
A1: f = F;
reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1;
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 FINSEQ_3:92;
rng Sgm J = J by FINSEQ_1:def 14;
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 A4,FINSEQ_1:def 14;
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);
coherence;
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);
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 + 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 + 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 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 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
::$L https://en.wikipedia.org/wiki/EuclidâEuler_theorem 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 14;
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 FINSEQ_1:def 14;
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;
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;
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,Th24;
end;