:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies ORDINAL2, ARYTM, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1,
BOOLE, QC_LANG1, CARD_3, FINSET_1, XREAL_0, GROUP_1, NAT_1, INT_1,
FILTER_0, CARD_1, TARSKI, SQUARE_1, POWER, EULER_1, MATRIX_2, INT_5,
ABSVALUE, GR_CY_1, COMPLEX1, MOEBIUS1, BHSP_5, NAT_5, FUNCT_2, RLVECT_1,
SUPINF_1, FUNCOP_1, FINSEQ_2, WAYBEL29, TOPGEN_1, COHSP_1, POLYNOM1,
UPROOTS, ALGSEQ_1, MONOID_0, RFINSEQ, PARTFUN1, RFUNCT_3, INT_2, NAT_3,
NAT_LAT, XXREAL_2, MEMBERED, PROB_1;
notations VALUED_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCOP_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, ORDINAL1,
NUMBERS, CARD_3, CARD_1, XCMPLX_0, XREAL_0, FINSEQ_1, FINSEQ_2, FINSEQ_3,
INT_1, INT_2, NAT_1, NAT_D, RVSUM_1, REAL_1, SQUARE_1, XXREAL_0, NEWTON,
ABIAN, EULER_2, PEPIN, ABSVALUE, EQREL_1, INT_5, MEMBERED, FINSEQOP,
CARD_FIN, ENUMSET1, FINSET_1, COMPLEX1, NAT_3, DOMAIN_1, POWER, MOEBIUS1,
INT_3, BHSP_5, EULER_1, WSIERP_1, BINOP_1, PROB_3, RECDEF_1, SUPINF_1,
CONVFUN1, POLYNOM1, UPROOTS, BINOP_2, FUNCT_3, RFINSEQ, RFUNCT_3,
XXREAL_2, CLASSES1;
constructors VALUED_1, RELAT_2, PARTFUN1, MCART_1, SETFAM_1, FUNCT_2,
WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2, INT_2, FINSOP_1,
RVSUM_1, NEWTON, WSIERP_1, ABIAN, EULER_1, EULER_2, PEPIN, ABSVALUE,
EQREL_1, INT_4, ZFMISC_1, RELSET_1, INT_5, RECDEF_1, MEMBERED, SEQ_4,
MOEBIUS1, PRE_CIRC, FINSEQOP, NUMBERS, MESFUNC2, CONVFUN1, CARD_FIN,
XXREAL_0, COMPLEX1, INT_1, TARSKI, ENUMSET1, FUNCOP_1, XREAL_0, CARD_1,
XCMPLX_0, UPROOTS, NAT_3, REALSET1, FUNCT_1, POWER, INT_3, BHSP_5,
FINSEQ_1, FINSEQ_5, RFINSEQ, CALCUL_2, BINOP_1, PROB_3, SUPINF_1,
FINSEQ_3, GOBRD10, POLYNOM1, FUNCT_3, RFUNCT_3, VALUED_0, XXREAL_2,
CLASSES1, PBOOLE;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, INT_1, INT_2, MEMBERED, FINSEQ_1, FINSEQ_2,
RVSUM_1, VALUED_0, NEWTON, ABIAN, PEPIN, ABSVALUE, EQREL_1, INT_4,
FUNCT_1, ZFMISC_1, SUBSET_1, INT_5, MOEBIUS1, FUNCT_2, PRE_CIRC,
CARD_FIN, DYNKIN, RELAT_1, PARTFUN1, SQUARE_1, CARD_1, PREPOWER, POWER,
INT_3, BHSP_5, WSIERP_1, FINSEQ_5, FINSEQ_7, RFINSEQ, CALCUL_2, BINOP_1,
SUPINF_1, CONVFUN1, POLYNOM1, NAT_3, UPROOTS, BINOP_2, FUNCT_3, XXREAL_2,
CLASSES1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, INT_1,
INT_2, INT_5, NEWTON, FINSEQ_1, FINSEQ_3, RVSUM_1, ORDINAL1, ABIAN,
EULER_1, ABSVALUE, MOEBIUS1, FUNCT_2, PRE_CIRC, CLASSES1;
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, INT_3, FIB_NUM3, POWER, PEPIN, SQUARE_1, CARD_1, CARD_2,
ZFMISC_1, ALGSEQ_1, FINSEQ_4, JGRAPH_1, TARSKI, COMPLEX1, ABSVALUE,
MOEBIUS1, CARD_3, MESFUNC3, FUNCT_2, CONVFUN1, FINSEQOP, FUNCOP_1,
BAGORDER, RELSET_1, WELLORD2, PARTFUN1, BHSP_5, UPROOTS, RFINSEQ,
BINOP_2, BINOP_1, POLYNOM1, FUNCT_3, RFUNCT_3, NAT_4, NAT_3, RADIX_1,
XREAL_0, ABIAN, ENUMSET1, MONOID_1, CLASSES1;
schemes NAT_1, FUNCT_1, FUNCT_2, BINOP_2, FINSEQ_1;
begin :: Preliminaries
reserve k,n,m,l,p for natural number;
reserve n0,m0 for non zero natural number;
Lm1:
p is prime implies p |-count (n0 gcd m0) = min(p |-count n0,p |-count m0)
proof
assume A1: p is prime; then
reconsider p'=p as Prime;
reconsider h'=n0 gcd m0 as non empty natural number by INT_2:5;
h' divides n0 by INT_2:def 3; then
A2: p' |-count h' <= p' |-count n0 by NAT_3:30;
h' divides m0 by INT_2:def 3; then
A3: p' |-count h' <= p' |-count m0 by NAT_3:30;
per cases;
suppose A4: p |-count n0 <= p |-count m0;
set k = p' |^ (p'|-count n0);
A5: p>1 by A1,INT_2:def 5; then
A6: k divides n0 by NAT_3:def 7;
p'|^(p |-count n0) divides m0 by A4,MOEBIUS1:9; then
k divides h' by A6,INT_2:def 3; then
p' |-count k <= p' |-count h' by NAT_3:30; then
p' |-count n0 <= p' |-count h' by A5,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 = p' |^ (p'|-count m0);
A8: p>1 by A1,INT_2:def 5; then
A9: k divides m0 by NAT_3:def 7;
p'|^(p |-count m0) divides n0 by A7,MOEBIUS1:9; then
k divides h' by A9,INT_2:def 3; then
p' |-count k <= p' |-count h' by NAT_3:30; then
p' |-count m0 <= p' |-count h' by A8,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: P[0]
proof
2 < 3; then
2|^1 < 2*2 - 1 by NEWTON:10; then
2|^1 < 2|^1*2 - 1 by NEWTON:10; then
2|^1 < 2|^(1+1) - 1 by NEWTON:11;
hence 2|^(0+1) < 2|^(0+2) - 1;
end;
A2: 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:70; then
2|^((k+1)+1) < 2|^(k+2)*2 - 1*2 by NEWTON:11; then
A3: 2|^((k+1)+1) < 2|^((k+2)+1) - 2 by NEWTON:11;
-2 + 2|^((k+1)+2) < -1 + 2|^((k+1)+2) by XREAL_1:10;
hence P[k + 1] by A3,XXREAL_0:2;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
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 natural number such that
A2: n0 = 2|^k * m by NAT_D:def 3;
take k,m;
A3: now assume A4: not m is odd;
reconsider m'=m as Element of NAT by ORDINAL1:def 13;
consider m'' be Element of NAT such that
A5: m' = 2 * m'' by A4,ABIAN:def 2;
n0 = 2|^k * 2 * m'' by A2,A5
.= 2|^(k+1)*m'' by NEWTON:11; 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:9;
hence contradiction by A3,A1;
end;
hence k > 0;
thus n0 = 2|^k * m by A2;
end;
theorem Th3:
n=2|^k & m is odd implies n,m are_relative_prime
proof
assume A1: n=2|^k;
assume A2: m is odd; then
reconsider h = n gcd m as non zero natural number by INT_2:5;
for p being Element of NAT st p is prime
holds p |-count h = p |-count 1
proof
let p be Element of NAT;
assume A3: p is prime; then
A4: p > 1 by INT_2:def 5;
reconsider n'=n,m'=m as non zero natural number by A2,A1;
A5: p |-count (n' gcd m') = min(p |-count n',p |-count m') by A3,Lm1;
min(p |-count n,p |-count m) = 0
proof
per cases;
suppose A6: p=2;
not p divides m
proof
assume p divides m; then
consider m' be natural number such that
A7: m = p * m' by NAT_D:def 3;
reconsider m' as Element of NAT by ORDINAL1:def 13;
thus contradiction by A2,A6,A7;
end; then
p |-count m = 0 by A6,NAT_3:27;
hence thesis by XXREAL_0:def 9;
end;
suppose A8: p<>2;
2 is prime & p<>1 by A3,INT_2:44,INT_2:def 5; then
A9: p |-count 2 = 0 by A8,NAT_3:24;
p |-count n = k * (p |-count 2) by A1,A3,NAT_3:32 .= k * 0 by A9;
hence thesis by XXREAL_0:def 9;
end;
end;
hence p |-count h = p |-count 1 by A4,A5,NAT_3:21;
end; then
n gcd m = 1 by NAT_4:21;
hence n,m are_relative_prime by INT_2:def 4;
end;
theorem Th4:
{n} is finite Subset of NAT
proof
n in NAT by ORDINAL1:def 13;
hence {n} is finite Subset of NAT by ZFMISC_1:37;
end;
theorem Th5:
{n,m} is finite Subset of NAT
proof
n in NAT & m in NAT by ORDINAL1:def 13;
hence {n,m} is finite Subset of NAT by ZFMISC_1:38;
end;
Lm2:
{n,m,l} is finite Subset of NAT
proof
reconsider X = {n} as finite Subset of NAT by Th4;
reconsider Y = {m,l} as finite Subset of NAT by Th5;
{n,m,l} = X \/ Y by ENUMSET1:42;
hence {n,m,l} is finite Subset of NAT;
end;
Lm3:
{n,m,l,k} is finite Subset of NAT
proof
reconsider X = {n,m} as finite Subset of NAT by Th5;
reconsider Y = {l,k} as finite Subset of NAT by Th5;
{n,m,l,k} = X \/ Y by ENUMSET1:45;
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
assume A1: f is one-to-one;
dom f = Seg len f by FINSEQ_1:def 3; then
Sgm (dom f \ {n}) is one-to-one by FINSEQ_3:99,XBOOLE_1:36;
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;
assume A2: n in dom f; then
consider m be Nat such that
A3: len f = m + 1 & len Del(f,n) = m by FINSEQ_3:113;
assume f.n in rng Del(f,n); then
consider j be set such that
A4: j in dom Del(f,n) & f.n = Del(f,n).j by FUNCT_1:def 5;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
A5: j in Seg m by A4,A3,FINSEQ_1:def 3;
reconsider j as Element of NAT by A4;
A6: dom Del(f,n') c= dom f by WSIERP_1:47;
per cases;
suppose A7: j=n';
A9: j <= m by A5,FINSEQ_1:3; then
A10: f.n = f.(j+1) by A2,A4,A3,A8,FINSEQ_3:120;
A11: j+1 <= m+1 by A9,XREAL_1:8;
j+1 >= 0+1 by XREAL_1:8; then
j+1 in Seg(m+1) by A11; then
j+1 in dom f & j+1 <> n by A8,A3,FINSEQ_1:def 3,NAT_1:13;
hence contradiction by A1,A10,A2,FUNCT_1:def 8;
end;
end;
theorem Th8:
x in rng f & not x in rng Del(f,n) implies x = f.n
proof
assume A1: x in rng f; then
consider j be set such that
A2: j in dom f & x = f.j by FUNCT_1:def 5;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
assume A3: not x in rng Del(f,n);
assume A4: not x = f.n;
for X being set st card X = 0 holds X = {}; then
consider m be natural number such that
A5: len f = m + 1 by NAT_1:6,A1,RELAT_1:60;
reconsider m'=m as Element of NAT by ORDINAL1:def 13;
A6: n in dom f by A1,A3,FINSEQ_3:113; then
A7: len Del(f,n) = m by A5,FINSEQ_3:118;
A8: j in Seg(m+1) by A5,A2,FINSEQ_1:def 3;
reconsider j as Element of NAT by A2;
n in Seg(m+1) by A5,A6,FINSEQ_1:def 3; then
A9: 1 <= n & n <= m+1 by FINSEQ_1:3;
per cases;
suppose A10: jm; then
j>m & j<=m+1 by A8,FINSEQ_1:3;
hence contradiction by A9,A10,NAT_1:8;
end;
suppose A11: j>=n';
set j'=j-'1;
j>n' by A11,A4,A2,XXREAL_0:1; then
j>=n'+1 by NAT_1:13; then
A12: j-1>=n'+1-1 by XREAL_1:11;
j <= m+1 by A8,FINSEQ_1:3; then
j-1 <= m+1-1 by XREAL_1:11; then
A13: len f = m'+1 & n' in dom f & n'<=j' & j'<=m'
by A5,A12,XREAL_0:def 2,A1,A3,FINSEQ_3:113; then
A14: Del(f,n').j' = f.(j'+1) by FINSEQ_3:120;
j'>=n' by A12,XREAL_0:def 2; then
j'>=1 by A9,XXREAL_0:2; then
j' in Seg m by A13; then
j' in dom Del(f,n) by A7,FINSEQ_1:def 3; then
f.j <> f.(j'+1) by A2,A3,A14,FUNCT_1:def 5; then
f.j <> f.(j-1+1) by A12,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;
assume A1: rng f1 c= dom f2;
consider n be natural number such that
A2: dom f1 = Seg n by FINSEQ_1:def 2;
dom(f2*f1) = Seg n by A1,A2,RELAT_1:46; then
A3: f2*f1 is FinSequence by FINSEQ_1:def 2;
rng(f2*f1) c= X;
hence f2*f1 is FinSequence of X by A3,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
X = {} & Y = {} by A1; then
f2 = {} & f3 = {} by A3,A4,FINSEQ_3:49;
hence thesis by A5,RVSUM_1:102,RELAT_1:64;
end;
suppose A6: dom f1 <> {};
reconsider F1=f1 as FinSequence of ExtREAL by MESFUNC3:11;
A7: dom f1 = Seg len f1 by FINSEQ_1:def 3; then
reconsider F = id dom f1 as FinSequence by FINSEQ_2:52;
dom f1 \ X = Y by A1,A2,XBOOLE_1:88; then
A8: rng F \ X = Y by RELAT_1:71;
A9: X c= dom f1 by A1,XBOOLE_1:7; then
A10: F"X = X by FUNCT_2:171;
A11: Y c= dom f1 by A1,XBOOLE_1:7; then
A12: F"(rng F \ X) = Y by A8,FUNCT_2:171;
dom F1 = dom F by RELAT_1:71; then
reconsider s = Sgm(X)^Sgm(Y) as Permutation of dom F1
by A10,A12,FINSEQ_3:123;
rng s c= dom f1 by FUNCT_2:def 3; then
reconsider g=f1*s as FinSequence of REAL by Th9;
reconsider G = g as FinSequence of ExtREAL by MESFUNC3:11;
not -infty in rng F1; then
Sum F1 = Sum G by CONVFUN1:8; then
A13: Sum f1 = Sum G by MESFUNC3:2;
reconsider D = dom f1 as non empty set by A6;
rng Sgm Y c= dom f1 by A7,A11,FINSEQ_1:def 13; then
reconsider sy = Sgm(Y) as FinSequence of D by FINSEQ_1:def 4;
rng Sgm X c= dom f1 by A7,A9,FINSEQ_1:def 13; then
reconsider sx = Sgm(X) as FinSequence of D by FINSEQ_1:def 4;
reconsider f1' = f1 as Function of D,REAL by FINSEQ_2:30;
g = (f1'*sx)^(f1'*sy) by FINSEQOP:10; then
Sum g = Sum(f1'*sx) + Sum(f1'*sy) by RVSUM_1:105;
hence Sum f1 = Sum f2 + Sum f3 by A13,A3,A4,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);
assume A2: dom f1 \ f1"{0} c= X;
assume A3: X c= dom f1;
set Y = dom f1 \ X;
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:54;
hence thesis by A1,FINSEQ_2:64;
end;
suppose A5: Y <> {};
A6: X \/ Y = dom f1 by A3,XBOOLE_1:45;
A7: X misses Y by XBOOLE_1:79;
set f3 = f1*Sgm(Y);
A8: Y c= dom f1 by XBOOLE_1:36; then
A9: Y c= Seg len f1 by FINSEQ_1:def 3; then
rng Sgm Y c= dom f1 by A8,FINSEQ_1:def 13; then
reconsider f3 as FinSequence of REAL by Th9;
A10: dom f3 = Seg len f3 by FINSEQ_1:def 3;
A11: Y c= f1"{0}
proof
assume not Y c= f1"{0}; then
consider x be set such that
A12: x in Y & not x in f1"{0} by TARSKI:def 3;
x in dom f1 & not x in X by A12,XBOOLE_0:def 5; then
x in dom f1 \ f1"{0} by A12,XBOOLE_0:def 5; then
x in X /\ Y by A2,A12,XBOOLE_0:def 4;
hence contradiction by A7,XBOOLE_0:def 7;
end;
for y being set holds y in rng f3 iff y = 0
proof
let y be set;
hereby
assume y in rng f3; then
consider x be set such that
A13: x in dom f3 & y = f3.x by FUNCT_1:def 5;
A14: x in dom Sgm Y & (Sgm Y).x in dom f1 by A13,FUNCT_1:21; then
(Sgm Y).x in rng Sgm Y by FUNCT_1:12; then
(Sgm Y).x in Y by A9,FINSEQ_1:def 13; then
f1.((Sgm Y).x) in {0} by A11,FUNCT_1:def 13; then
f3.x in {0} by A14,FUNCT_1:23;
hence y = 0 by A13,TARSKI:def 1;
end;
assume A15: y = 0;
consider x be set such that
A16: x in Y by A5,XBOOLE_0:def 1;
A17: x in dom f1 & f1.x in {0} by A16,A11,FUNCT_1:def 13;
x in rng Sgm Y by A16,A9,FINSEQ_1:def 13; then
consider x' be set such that
A18: x' in dom Sgm Y & x = (Sgm Y).x' by FUNCT_1:def 5;
A19: x' in dom f3 by A17,A18,FUNCT_1:21;
f1.((Sgm Y).x') = y by A15,A17,A18,TARSKI:def 1; then
f3.x' = y by A18,FUNCT_1:23;
hence y in rng f3 by A19,FUNCT_1:def 5;
end; then
rng f3 = {0} by TARSKI:def 1; then
f3 = (Seg len f3) --> 0 by A10,FUNCOP_1:15; then
A20: f3 = (len f3) |-> 0 by FINSEQ_2:def 2;
0 is Element of NAT by ORDINAL1:def 13; then
reconsider f3 as FinSequence of NAT by A20,FINSEQ_2:77;
A21: Sum f3 = 0 by A20,BAGORDER:5;
Sum f1 = Sum f2 + Sum f3 by Th10,A6,A1,XBOOLE_1:79;
hence Sum f1 = Sum f2 by A21;
end;
end;
theorem Th12:
f2 = f1 - {0} implies Sum f1 = Sum f2
proof
assume A1: f2 = f1 - {0};
dom f1 \ f1"{0} c= dom f1 by XBOOLE_1:36;
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 natural number st n in dom f holds f.n in REAL;
hence thesis by FINSEQ_2:14;
end;
:: NatDivisors
reserve n1,n2,m1,m2 for natural number;
theorem Th14:
n1 in NatDivisors n & m1 in NatDivisors m & n,m are_relative_prime
implies n1,m1 are_relative_prime
proof
assume n1 in NatDivisors n; then
A1: 0 < n1 & n1 divides n by MOEBIUS1:39;
assume m1 in NatDivisors m; then
A2: 0 < m1 & m1 divides m by MOEBIUS1:39;
assume A3: n,m are_relative_prime;
assume not n1,m1 are_relative_prime; then
A4: n1 gcd m1 <> 1 by INT_2:def 4;
n1 gcd m1 divides n1 & n1 gcd m1 divides m1 by INT_2:def 3; then
A5: n1 gcd m1 divides n & n1 gcd m1 divides m by A1,A2,INT_2:13;
n gcd m > 0 by A3,INT_2:def 4; then
A6: n1 gcd m1 <= n gcd m by A5,INT_2:43,INT_2:33;
n1 gcd m1 <> 0 by A2,INT_2:35; then
n1 gcd m1 + 1 > 0 + 1 by XREAL_1:10; then
n1 gcd m1 >= 1 by NAT_1:13; then
n gcd m <> 1 by A6,A4,XXREAL_0:1;
hence contradiction by A3,INT_2:def 4;
end;
theorem Th15:
n1 in NatDivisors n & m1 in NatDivisors m &
n2 in NatDivisors n & m2 in NatDivisors m &
n,m are_relative_prime & n1*m1=n2*m2 implies n1=n2 & m1=m2
proof
assume A1: n1 in NatDivisors n; then
A2: 0 < n1 & n1 divides n by MOEBIUS1:39;
assume A3: m1 in NatDivisors m; then
A4: 0 < m1 & m1 divides m by MOEBIUS1:39;
assume A5: n2 in NatDivisors n; then
A6: 0 < n2 & n2 divides n by MOEBIUS1:39;
assume A7: m2 in NatDivisors m; then
A8: 0 < m2 & m2 divides m by MOEBIUS1:39;
assume A9: n,m are_relative_prime;
assume A10: n1*m1=n2*m2;
assume A11: not (n1=n2 & m1=m2);
now assume A12: n1<>n2;
reconsider n1'=n1,n2'=n2 as non empty Nat by A1,A5,MOEBIUS1:39;
reconsider m1'=m1,m2'=m2 as non empty Nat by A3,A7,MOEBIUS1:39;
consider p be Element of NAT such that
A13: p is prime & p |-count n1' <> p |-count n2' by A12,NAT_4:21;
reconsider p as Prime by A13;
A14: (p |-count n1') + (p |-count m1') = p |-count (n1'*m1') by NAT_3:28
.= (p |-count n2') + (p |-count m2') by A10,NAT_3:28;
p |-count m1' <> 0 or p |-count m2' <> 0 by A13,A14; then
p divides m1' or p divides m2' by MOEBIUS1:6; then
A15: p divides m by A4,A8,INT_2:13;
p |-count n1' <> 0 or p |-count n2' <> 0 by A13; then
p divides n1' or p divides n2' by MOEBIUS1:6; then
A16: p divides n by A2,A6,INT_2:13;
A17: n gcd m > 0 by A9,INT_2:def 4;
p divides n gcd m by A15,A16,INT_2:def 3; then
A18: p <= n gcd m by A17,INT_2:43;
p > 1 by INT_2:def 5;
hence contradiction by A18,A9,INT_2:def 4;
end;
hence contradiction by A10,A11,A6,XCMPLX_1:5;
end;
theorem Th16:
n1 in NatDivisors n0 & m1 in NatDivisors m0 implies
n1*m1 in NatDivisors(n0*m0)
proof
assume A1: n1 in NatDivisors n0; then
A2: 0 < n1 & n1 divides n0 by MOEBIUS1:39;
assume A3: m1 in NatDivisors m0; then
A4: 0 < m1 & m1 divides m0 by MOEBIUS1:39;
reconsider a=n1*m1 as non empty Nat by A2,A4;
reconsider b=n0*m0 as non empty 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 p'=p as Prime;
reconsider n1'=n1,m1'=m1 as non empty Nat by A1,A3,MOEBIUS1:39;
A5: p' |-count(n1'*m1') = p' |-count n1' + p' |-count m1' by NAT_3:28;
A6: p' |-count(n0*m0) = p' |-count n0 + p' |-count m0 by NAT_3:28;
A7: p' |-count n1' <= p' |-count n0 by A2,NAT_3:30;
p' |-count m1' <= p' |-count m0 by A4,NAT_3:30;
hence p |-count a <= p |-count b by A5,A6,A7,XREAL_1:9;
end; then
ex c being Element of NAT st n0*m0=(n1*m1)*c by NAT_4:20; then
A8: n1*m1 divides n0*m0 by NAT_D:def 3;
thus n1*m1 in NatDivisors(n0*m0) by A2,A4,A8,MOEBIUS1:39;
end;
theorem Th17:
n0,m0 are_relative_prime implies k gcd n0*m0 = (k gcd n0)*(k gcd m0)
proof
assume A1: n0,m0 are_relative_prime;
per cases;
suppose A2: k = 0;
thus k gcd n0*m0 = abs(n0*m0) by A2,WSIERP_1:13
.= abs(n0)*abs(m0) by COMPLEX1:151
.= (k gcd n0)*abs(m0) by A2,WSIERP_1:13
.= (k gcd n0)*(k gcd m0) by A2,WSIERP_1:13;
end;
suppose k <> 0; then
reconsider k' = k as non zero natural number;
reconsider a = k gcd n0*m0 as non empty 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 empty Nat;
reconsider b1 = k gcd n0, b2 = k gcd m0 as non empty Nat by INT_2:5;
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 p'=p as Prime;
A3: p' |-count a = min(p' |-count k',p' |-count(n0*m0)) by Lm1
.= min(p' |-count k,p' |-count n0 + p' |-count m0) by NAT_3:28;
A4: p' |-count b = p' |-count b1 + p' |-count b2 by NAT_3:28
.= min(p' |-count k',p' |-count n0) + p' |-count b2 by Lm1
.= min(p' |-count k',p' |-count n0) + min(p' |-count k',p' |-count m0)
by Lm1;
A5: p' > 1 by INT_2:def 5;
n0 gcd m0 = 1 by A1,INT_2:def 4; then
p' |-count 1 = min(p' |-count n0,p' |-count m0) by Lm1; then
A6: min(p' |-count n0,p' |-count m0) = 0 by A5,NAT_3:21;
per cases by A6,XXREAL_0:15;
suppose A7: p' |-count n0 = 0; then
min(p' |-count k,p' |-count n0) = p' |-count n0 by XXREAL_0:def 9;
hence p |-count a = p |-count b by A3,A4,A7;
end;
suppose A8: p' |-count m0 = 0; then
min(p' |-count k,p' |-count m0) = p' |-count m0 by XXREAL_0:def 9;
hence p |-count a = p |-count b by A3,A4,A8;
end;
end;
hence k gcd n0*m0 = (k gcd n0)*(k gcd m0) by NAT_4:21;
end;
end;
theorem Th18:
n0,m0 are_relative_prime & 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_relative_prime;
assume k in NatDivisors(n0*m0); then
A2: 0 < k & k divides n0*m0 by MOEBIUS1:39;
set n1 = k gcd n0;
set m1 = k gcd m0;
take n1,m1;
n1 divides n0 & n1 > 0 by NAT_D:def 5,NEWTON:71;
hence n1 in NatDivisors n0;
m1 divides m0 & m1 > 0 by NAT_D:def 5,NEWTON:71;
hence m1 in NatDivisors m0;
thus k = k gcd n0*m0 by A2,NEWTON:62
.= 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 set holds
x in NatDivisors(p|^n) iff x in {p|^k where k is Element of NAT : k <= n}
proof
let x be set;
hereby
assume A2: x in NatDivisors(p|^n); then
reconsider x'=x as natural number;
0 < x' & x' divides p|^n by A2,MOEBIUS1:39; then
consider t be Element of NAT such that
A3: x' = p|^t & t<=n by A1,PEPIN:35;
thus x in {p|^k where k is Element of NAT : k <= n} by A3;
end;
assume x in {p|^k where k is Element of NAT : k <= n}; then
consider t be Element of NAT such that
A4: x=p|^t & t <= n;
reconsider x'=x as natural number by A4;
0 < x' & x' divides p|^n by A1,A4,RADIX_1:7;
hence x in NatDivisors(p|^n) by 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 A1: l<>0 & p > l & p > n1 & p > n2;
assume A2: l*n1 mod p = l*n2 mod p;
assume A3: p is prime;
(l*n1-l*n2) mod p = 0 by A2,A3,INT_4:22; then
A4: p divides l*(n1-n2) by A3,INT_1:89;
per cases by A3,A4,INT_5:7;
suppose p divides l;
hence thesis by A1,NAT_D:7;
end;
suppose A5: p divides n1-n2;
per cases;
suppose A6: n1-n2 > 0; then
A7: p divides n1-'n2 by A5,XREAL_0:def 2;
n1-'n2>0 by A6,XREAL_0:def 2; then
p <= n1-'n2 by A7,NAT_D:7; then
p+n2 <= n1-'n2+n2 by XREAL_1:8; then
p+n2 <= n1-n2+n2 by A6,XREAL_0:def 2; then
p+n2 < p by A1,XXREAL_0:2; then
p+n2-p < p-p by XREAL_1:11; then
n2 < 0;
hence thesis;
end;
suppose n1-n2 = 0; hence thesis; end;
suppose n1-n2 < 0; then
A8: (-(n1-n2)) > 0; then
A9: n2-n1 > 0;
p divides -(n1-n2) by A5,INT_2:14; then
A10: p divides n2-'n1 by A9,XREAL_0:def 2;
n2-'n1>0 by A9,XREAL_0:def 2; then
p <= n2-'n1 by A10,NAT_D:7; then
p+n1 <= n2-'n1+n1 by XREAL_1:8; then
p+n1 <= n2-n1+n1 by A8,XREAL_0:def 2; then
p+n1 < p by A1,XXREAL_0:2; then
p+n1-p < p-p by XREAL_1:11; 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^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:27;
then reconsider b=len fs-a, d=a-1 as Element of NAT by INT_1:18;
len fs=a+b;
then consider fs3,fs2 be FinSequence such that
A2: len fs3=a & len fs2=b & fs=fs3^fs2 by FINSEQ_2:25;
fs3 <> {} by A2,A1,FINSEQ_3:27;
then a in dom fs3 by A2,FINSEQ_5:6;
then
A3: fs3.a=fs.a by A2,FINSEQ_1:def 7;
a=d+1;
then consider fs1 be FinSequence, v be set such that
A4: fs3=fs1^<*v*> by A2,FINSEQ_2:21;
A5: len fs1 + 1=d+1 by A2,A4,FINSEQ_2:19;
then fs.a=v by A3,A4,FINSEQ_1:59;
hence thesis by A2,A4,A5;
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
A1: a in dom fs & fs=fs1^<*v*>^fs2 & len fs1=a-1;
then
A2: len fs=len(fs1^<*v*>)+len fs2 by FINSEQ_1:35
.=len fs1 +1 +len fs2 by FINSEQ_2:19
.=a +len fs2 by A1;
A3: fs=fs1^(<*v*>^fs2) by A1,FINSEQ_1:45;
A4: len<*v*>=1 by FINSEQ_1:56;
len fs=(a-1) + len(<*v*>^fs2) by A1,A3,FINSEQ_1:35;
then
A5: len(<*v*>^fs2)=len fs -(a-1);
A6: len(Del(fs,a))+1=len fs by A1,WSIERP_1:def 1;
then len(Del(fs,a))=len fs2 +len fs1 by A1,A2;
then
A7: len(fs1^fs2)=len(Del(fs,a)) by FINSEQ_1:35;
now
let e be Nat;
assume
A8: 1<=e & e<=len Del(fs,a);
now per cases;
suppose
A9: e=a;
then
A12: e>a-1 by Lm4;
then
A13: e+1>a by XREAL_1:21;
then e+1-a>0 by XREAL_1:52;
then
A14: e+1-a+1>0 qua Nat+1 by XREAL_1:8;
A15: e+1>a-1 by A13,XREAL_1:148 ,XXREAL_0:2;
then e+1-(a-1)>0 by XREAL_1:52;
then reconsider f=e+1-(a-1) as Element of NAT by INT_1:16;
A16: e+1<=len fs by A6,A8,XREAL_1:8;
then
A17: e+1-(a-1)<=len(<*v*>^fs2) by A5,XREAL_1:11;
thus (fs1^fs2).e=fs2.(e-len fs1) by A1,A7,A8,A12,FINSEQ_1:37
.=fs2.(f-1) by A1
.=(<*v*>^fs2).f by A4,A14,A17,FINSEQ_1:37
.=(fs1^(<*v*>^fs2)).(e+1) by A1,A3,A15,A16,FINSEQ_1:37
.=(Del(fs,a)).e by A1,A3,A11,WSIERP_1:def 1;
end;
end;
hence (fs1^fs2).e=(Del(fs,a)).e;
end;
hence thesis by A7,FINSEQ_1:18;
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;
assume
A1: 1<=len fs;
set fs1=<*fs.1*>^Del(fs,1);
set fs2=Del(fs,len fs)^<*fs.(len fs)*>;
A2: len <*fs.1*>=1 & len <*fs.(len fs)*>=1 by FINSEQ_1:56;
A3: 1 in dom fs by A1,FINSEQ_3:27;
A4: len fs in dom fs by A1,FINSEQ_3:27;
then
A5: len(Del(fs,len fs))+1=len fs by WSIERP_1:def 1;
then
A6: len Del(fs,len fs)=len fs -1;
A7: len fs=len <*fs.1*> + len Del(fs,1) by A2,A3,WSIERP_1:def 1
.=len fs1 by FINSEQ_1:35;
A8: len fs=len <*fs.(len fs)*> + len Del(fs,len fs) by A2,A4,WSIERP_1:def 1
.=len fs2 by FINSEQ_1:35;
for b be Nat st 1<=b & b<=len fs holds fs.b=fs1.b
proof
let b be Nat;
assume
A9: 1<=b & b<=len fs;
now per cases by A9,XXREAL_0:1;
suppose
A10: b=1;
1 in dom <*fs.1*> by A2,FINSEQ_3:27;
hence fs1.b=<*fs.1*>.1 by A10,FINSEQ_1:def 7
.=fs.b by A10,FINSEQ_1:57;
end;
suppose
A11: b>1;
then
A12: b-1>0 by XREAL_1:52;
then reconsider e=b-1 as Element of NAT by INT_1:16;
A13: e>=1 by A12,NAT_1:14;
thus fs1.b=(Del(fs,1)).e by A2,A7,A9,A11,FINSEQ_1:37
.=fs.(e+1) by A3,A13,WSIERP_1:def 1
.=fs.b;
end;
end;
hence thesis;
end;
hence fs1=fs by A7,FINSEQ_1:18;
for b be Nat st 1<=b & b<=len fs holds fs.b=fs2.b
proof
let b be Nat;
assume
A14: 1<=b & b<=len fs;
now per cases by A14,XXREAL_0:1;
suppose
A15: b=len fs;
reconsider e=b-(b-1) as Element of NAT;
thus fs2.b=<*fs.(len fs)*>.e by A5,A8,A15,FINSEQ_1:37,XREAL_1:148
.=fs.b by A15,FINSEQ_1:57;
end;
suppose
A16: b^Del(ft,1)=ft by A3,Lm7;
then Product(ft)=Product(<*ft.1*>)*Product Del(ft,1) by RVSUM_1:127
.=(ft.1)*Product Del(ft,1) by RVSUM_1:125;
hence thesis by A3;
end;
end;
suppose
A4: a>0 & a=1 by NAT_1:11;
a+1<=len ft by A4,NAT_1:13;
then
A6: (a+1) in dom ft by A5,FINSEQ_3:27;
then consider fs1,fs2 be FinSequence such that
A7: ft=fs1^<*ft.(a+1)*>^fs2 &
len fs1=(a+1)-1 & len fs2=len ft-(a+1) by Lm5;
A8: Del(ft,a+1)=fs1^fs2 by A6,A7,Lm6;
then reconsider fs1 as FinSequence of REAL by FINSEQ_1:50;
reconsider fs2 as FinSequence of REAL by A7,FINSEQ_1:50;
Product(ft)=Product(fs1^<*ft.(a+1)*>)*Product(fs2) by A7,RVSUM_1:127
.=Product(fs1)*Product(<*ft.(a+1)*>)*Product(fs2) by RVSUM_1:127
.=(ft.(a+1))*Product(fs1)*Product(fs2) by RVSUM_1:125
.=(ft.(a+1))*(Product(fs1)*Product(fs2));
hence P[a+1] by A8,RVSUM_1:127;
end;
suppose a>=len ft;
then len ft < a+1 by NAT_1:13;
hence P[a+1] by FINSEQ_3:27;
end;
end;
hence thesis;
end;
for a being Element of NAT holds P[a] from NAT_1:sch 1(A1,A2);
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
assume A1: n+2 is prime;
let l;
assume A2: l in Seg n; then
A3: 1<=l & l<=n by FINSEQ_1:3; then
A4: l1;
reconsider l'=l as Element of NAT by ORDINAL1:def 13;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
reconsider n''=n'+2 as Element of NAT;
n'' is prime & l'0
by A2,A1,A7,A4,XXREAL_0:2,INT_2:def 5,FINSEQ_1:3; then
consider k be Element of NAT such that
A11: k*l' mod (n'+2) = 1 & k < n'+2 by IDEA_1:1;
take k;
k<>0 by A11,NAT_D:26; then
A12: k>=0+1 by NAT_1:13;
k < n+1+1 by A11; then
A13: k <= n+1 by NAT_1:13;
A14: n+2 > 1 by A8,A3,XXREAL_0:2;
k <> n+1
proof
assume k = n+1; then
(n+1)*l mod (n+2) = 1 mod (n+2) by A11,A14,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 A5,NAT_D:24;
hence contradiction;
end; then
k < n+1 by A13,XXREAL_0:1; then
k <= n by NAT_1:13;
hence k in Seg n by A12;
thus A15: k<>1
proof
assume k = 1; then
1*l mod (n+2) = 1 mod (n+2) by A11,NAT_D:14; then
0 = (l-1) mod (n+2) by INT_4:22
.= (l-'1) mod (n+2) by A6,XREAL_0:def 2
.= l-'1 by A9,NAT_D:24
.= l-1 by A6,XREAL_0:def 2;
hence contradiction by A10;
end;
thus k<>l
proof
assume A16: k=l; then
l*l mod (n+2) = 1 mod (n+2) by A11,A14,NAT_D:14; then
0 = (l*l-1) mod (n+2) by INT_4:22; then
A17: n+2 divides (l+1)*(l-1) by INT_1:89;
per cases by A1,A17,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:11;
hence contradiction by A4;
end;
suppose n+2 divides l-1; then
A18: n+2 divides l-'1 by A6,XREAL_0:def 2;
per cases;
suppose l=1;
hence contradiction by A15,A16;
end;
suppose l<>1; then
l>1 by A3,XXREAL_0:1; then
l-1>1-1 by XREAL_1:11; then
l-'1>0 by XREAL_0:def 2; then
n+2 <= l-'1 by A18,NAT_D:7; then
n+2 <= l-1 by XREAL_0:def 2; then
n+2+1 <= l-1+1 by XREAL_1:8; then
n+3 <= n by A3,XXREAL_0:2; then
n+3-n <= n-n by XREAL_1:11; then
3 <= 0;
hence contradiction;
end;
end;
end;
thus l*k mod (n+2) = 1 by A11;
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[natural number] 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;
A1: for k' being natural number
st for n' being natural number st n' < k' holds P[n'] holds P[k']
proof
let k' be natural number;
assume A2: for n' being natural number st n' < k' holds P[n'];
thus P[k']
proof
let f be FinSequence of NAT;
assume A3: len f = k';
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 k'=0; then
A8: Product f = 1 by RVSUM_1:124,A3,FINSEQ_1:32;
0+1 < n+1+1 by XREAL_1:8;
hence (Product f) mod (n+2) = 1 by A8,NAT_D:24;
end;
suppose k'<>0; then
dom f <> {} by RELAT_1:64,A3,CARD_1:47; then
consider x1 be set such that
A9: x1 in dom f by XBOOLE_0:def 1;
reconsider x1 as Element of NAT by A9;
reconsider f'=f as FinSequence of REAL by FINSEQ_2:27;
A10: Product Del(f',x1)*(f'.x1) = Product f by A9,Lm8;
A11: rng Del(f,x1) c= rng f by FINSEQ_3:115; then
A12: rng Del(f,x1) c= Seg n by A5,XBOOLE_1:1;
A13: Del(f,x1) is one-to-one by A6,Th6;
set n1' = len Del(f,x1);
consider m be Nat such that
A14: len f = m + 1 & len Del(f,x1) = m by A9,FINSEQ_3:113;
A15: 0 + n1' < 1 + n1' by XREAL_1:8;
per cases;
suppose A16: f'.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 A17: l in rng Del(f,x1);
assume l<>1; then
consider k such that
A18: k in rng f & k<>1 & k<>l & l*k mod (n+2) = 1 by A7,A17,A11;
take k;
thus k in rng Del(f,x1) by A16,A18,Th8;
thus k<>1 & k<>l & l*k mod (n+2) = 1 by A18;
end;
hence (Product f) mod (n+2) = 1 by A10,A16,A4,A12,A13,A15,A2,A3,A14;
end;
suppose A19: f'.x1 <> 1;
set l=f.x1;
A20: l in rng f & l <> 1 by A19,A9,FUNCT_1:12; then
consider k be natural number such that
A21: k in rng f & k<>1 & k<>l & l*k mod (n+2) = 1 by A7;
set f'' = Del(f,x1);
A22: k in rng f'' by A21,Th8;
consider x2 be set such that
A23: x2 in dom f'' & k = f''.x2 by A22,FUNCT_1:def 5;
reconsider x2 as Element of NAT by A23;
Product Del(f'',x2)*(f''.x2) = Product f'' by A23,Lm8; then
A24: Product Del(f'',x2)*(k*l)
= Product f by A10,A23;
set n2'' = len Del(f'',x2);
A25: rng Del(f'',x2) c= rng Del(f',x1) by FINSEQ_3:115; then
A26: rng Del(f'',x2) c= Seg n by A12,XBOOLE_1:1;
A27: Del(f'',x2) is one-to-one by A13,Th6;
A28: for l st l in rng Del(f'',x2) & l<>1 holds
ex k st k in rng Del(f'',x2) & k<>1 & k<>l & l*k mod (n+2) = 1
proof
let l' be natural number;
assume A29: l' in rng Del(f'',x2); then
A30: l' in rng Del(f',x1) by A25; then
l' in rng f by A11; then
A31: l' <= n by FINSEQ_1:3,A5;
A32: 0+n < 2+n by XREAL_1:8;
assume l'<>1; then
consider k' be natural number such that
A33: k' in rng f & k'<>1 & k'<>l' & l'*k' mod (n+2) = 1
by A7,A11,A30;
take k';
A34: 1 <= k & k <= n & 1 <= l & l <= n by A5,A20,A21,FINSEQ_1:3;
0+n < 2+n by XREAL_1:8; then
A35: n+2 > k & n+2 > l by A34,XXREAL_0:2;
thus k' in rng Del(f'',x2)
proof
assume A36: not k' in rng Del(f'',x2);
per cases;
suppose k' in rng f''; then
A37: l<>k & k*l mod (n+2) = k*l' mod (n+2) & l' < n+2 &
n+2 is prime by A4,A21,A23,A33,A31,A32,XXREAL_0:2,A36,Th8;
l'=l by A34,A35,A37,Th20;
hence contradiction by A9,A6,A25,A29,Th7;
end;
suppose not k' in rng f''; then
A38: k<>l & l*k mod (n+2) = l*l' mod (n+2) & l' < n+2 &
n+2 is prime by A4,A21,A33,A31,A32,XXREAL_0:2,Th8;
f''.x2 in rng Del(f'',x2) by A23,A29,A34,A35,A38,Th20;
hence contradiction by A23,A6,Th6,Th7;
end;
end;
thus k'<>1 & k'<>l' & l'*k' mod (n+2) = 1 by A33;
end;
consider m be Nat such that
A39: len Del(f',x1) = m + 1 & len Del(f'',x2) = m
by A23,FINSEQ_3:113;
0 + n2'' < 1 + n2'' by XREAL_1:8; then
A40: n2'' < k' by A39,A15,XXREAL_0:2,A3,A14;
thus (Product f) mod (n+2)
= (Product Del(f'',x2)*((k*l) mod (n+2))) mod (n+2) by A24,EULER_2:9
.= 1 by A40,A2,A4,A26,A27,A28,A21;
end;
end;
end;
end;
A41: for n' being natural number holds P[n'] from NAT_1:sch 4(A1);
let f be FinSequence of NAT;
set n' = len f;
P[n'] by A41;
hence thesis;
end;
begin :: Wilson's Theorem
:: Number Theory (Andrews) p.61-66
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 5;
end;
suppose n>=2; then
A2: n-2>=2-2 by XREAL_1:11;
A3: n-2+1>=0+1 by A2,XREAL_1:8;
set l = n-'2;
A4: l = n-2 by A2,XREAL_0:def 2;
A5: l+1 = n-1 by A4
.= n-'1 by A3,XREAL_0:def 2;
A6: 2+l > 1+l by XREAL_1:8;
A7: l! = Product Sgm(Seg l) by FINSEQ_3:54;
set f = Sgm(Seg l);
A8: rng f c= Seg l by FINSEQ_1:def 13;
A9: for l' being natural number st l' in rng f & l'<>1 holds
ex k' being natural number st
k' in rng f & k'<>1 & k'<>l' & l'*k' mod (l+2) = 1
proof
let l' be natural number;
assume l' in rng f; then
A10: l' in Seg l by FINSEQ_1:def 13;
assume A11: l'<>1;
consider k' be natural number such that
A12: k' in Seg l & k'<>1 & k'<>l' & l'*k' mod (l+2) = 1
by A10,A11,A1,A4,Lm9;
take k';
thus thesis by A12,FINSEQ_1:def 13;
end;
A13: l! mod (l+2) = 1 by A4,A1,A7,A8,FINSEQ_3:99,A9,Lm10;
A14: (l+1)! mod (l+2)
= (l+1)*(l!) mod (l+2) by NEWTON:21
.= ((l+1)*1) mod (l+2) by A13,EULER_2:9
.= l+1 by A6,NAT_D:24;
(n*1) mod n = 0 by NAT_D:13; then
((l+1)! mod (l+2))+1 mod (l+2) = 0 by A4,A14;
hence thesis by A4,A5,NAT_D:22,A1,INT_2:def 5;
end;
end;
thus (n-'1)!+1 mod n = 0 & n>1 implies n is prime
proof
assume A15: (n-'1)!+1 mod n = 0 & n>1;
assume A16: not n is prime;
n>=1+1 by A15,NAT_1:13; then
consider k be Element of NAT such that
A17: k is prime & k divides n by INT_2:48;
consider i be Nat such that
A18: n = k * i by A17,NAT_D:def 3;
(n-'1)!+1 mod n = (n-'1)!+1 mod k by A15,A17,A18,PEPIN:9; then
A19: k divides (n-'1)!+1 by A15,A17,PEPIN:6;
k<>1 & k<>0 by A17,INT_2:def 5; then
A20: k > n-'1 by A19,NEWTON:55;
k > n-1 by A20,XREAL_0:def 2; then
k+1 > n-1+1 by XREAL_1:8; then
k >= n by NAT_1:13; then
k/k >= k*i/k by A18,XREAL_1:74; then
1 >= k*i/k by A17,XCMPLX_1:60; then
1 >= i*(k/k) by XCMPLX_1:75; then
A21: 1 >= i*1 by A17,XCMPLX_1:60;
i<>0 by A15,A18; then
i>=0+1 by NAT_1:13; then
i = 1 by A21,XXREAL_0:1;
hence contradiction by A16,A17,A18;
end;
end;
begin :: All Primes (1 mod 4) Equal the Sum of Two Squares
:: Proofs from THE BOOK (Aigner-Ziegler) p.19
theorem
p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2
proof
assume A1: p is prime;
assume A2: p mod 4 = 1;
A3: 0 <= sqrt(p) by SQUARE_1:def 4;
reconsider p' = [\ sqrt(p) /] as Element of NAT by A3,INT_1:16,INT_1:81;
reconsider p'' = p' + 1 as Element of NAT;
set X = Segm p'';
A4: card X = card p'' by CARD_1:def 12
.= 1 + [\ sqrt(p) /] by CARD_1:def 5;
A5: sqrt(p) * card X < card X * card X by A4,INT_1:52,XREAL_1:70;
0 < sqrt(p) by A1,SQUARE_1:93; then
sqrt(p) * sqrt(p) < card X * sqrt(p) by A4,INT_1:52,XREAL_1:70; then
sqrt(p) * sqrt(p) < card X * card X by A5,XXREAL_0:2; then
sqrt(p*p) < card X * card X by SQUARE_1:97; then
sqrt(p^2) < card X * card X by SQUARE_1:def 3; then
p < card X * card X by SQUARE_1:89; then
A6: p < card [: X, X :] by CARD_2:65;
A7: for s being integer number holds
ex x',x'',y',y'' being natural number st
x' in X & x'' in X & y' in X & y'' in X & [x',y']<>[x'',y''] &
(x' - s*y') mod p = (x'' - s*y'') mod p
proof
let s be integer number;
reconsider p'=p as Element of NAT by ORDINAL1:def 13;
set A = [: X, X :];
set B = Segm p';
card B = card p' by CARD_1:def 12 .= p by CARD_1:def 5; then
A8: card B in card A by A6,NAT_1:45;
A9: B <> {} by A1,ALGSEQ_1:10;
defpred P[set,set] means
ex n1,n2,n3 being Element of NAT st $1=[n1,n2] & $2=n3 &
(n1-s*n2) mod p = n3;
A10: for x being set st x in A ex y being set st y in B & P[x,y]
proof
let x be set;
assume x in A; then
consider n1,n2 be set such that
A11: n1 in X & n2 in X & x = [n1,n2] by ZFMISC_1:def 2;
reconsider n1,n2 as Element of NAT by A11;
set y = (n1-s*n2) mod p;
reconsider y as Element of NAT by INT_1:16,INT_1:84;
take y;
y < p by A1,INT_1:85; then
y in p by NAT_1:45;
hence y in B by CARD_1:def 12;
thus P[x,y] by A11;
end;
consider f be Function of A,B such that
A12: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A10);
consider x1,x2 be set such that
A13: x1 in A & x2 in A & x1 <> x2 & f.x1 = f.x2 by A8,A9,FINSEQ_4:80;
consider x',y' be set such that
A14: x' in X & y' in X & x1 = [x',y'] by A13,ZFMISC_1:def 2;
reconsider x',y' as natural number by A14;
consider x'',y'' be set such that
A15: x'' in X & y'' in X & x2 = [x'',y''] by A13,ZFMISC_1:def 2;
reconsider x'',y'' as natural number by A15;
take x',x'',y',y'';
thus x' in X & x'' in X & y' in X & y'' in X by A14,A15;
thus [x',y']<>[x'',y''] by A13,A14,A15;
consider n11,n12,n13 be Element of NAT such that
A16: x1=[n11,n12] & f.x1=n13 & (n11-s*n12) mod p = n13 by A12,A13;
consider n21,n22,n23 be Element of NAT such that
A17: x2=[n21,n22] & f.x2=n23 & (n21-s*n22) mod p = n23 by A12,A13;
A18: n11 = x' & n12 = y' by A14,A16,ZFMISC_1:33;
n21 = x'' & n22 = y'' by A15,A17,ZFMISC_1:33;
hence (x' - s*y') mod p = (x'' - s*y'') mod p by A18,A16,A17,A13;
end;
A19: p <> 2 by NAT_D:24,A2;
p > 1 by A1,INT_2:def 5; then
p + 1 > 1 + 1 by XREAL_1:8; then
p >= 2 by NAT_1:13; then
p > 2 by A19,XXREAL_0:1; then
(-1) is_quadratic_residue_mod p by A1,A2,INT_5:37; then
consider s be Integer such that
A20: (s^2-(-1)) mod p = 0 by INT_5:def 2;
consider x',x'',y',y'' be natural number such that
A21: x' in X & x'' in X & y' in X & y'' in X & [x',y']<>[x'',y''] &
(x' - s*y') mod p = (x'' - s*y'') mod p by A7;
(x' - s*y') mod p - ((x'' - s*y'') mod p) = 0 by A21; then
((x' - s*y')-(x'' - s*y'')) mod p = 0 mod p by INT_6:7; then
A22: ( x' - x'' -s*(y' - y'')) mod p = 0 by INT_4:12;
set n' = x'-x'';
set m' = y'-y'';
A23: (n' +s*m')*(n' -s*m') = n' to_power 2 - (s*m') to_power 2 by FIB_NUM3:7
.= n'^2 - (s*m') to_power 2 by POWER:53
.= n'^2 - (s*m')^2 by POWER:53;
A24: 0 = (((n' +s*m') mod p)*((n' -s*m') mod p)) mod p by A22,INT_4:12
.= (n'^2 - (s*m')^2) mod p by A23,INT_3:15;
0 = (((s^2+1) mod p)*(m'^2 mod p)) mod p by A20,INT_4:12
.= ((s^2+1)*(m'^2)) mod p by INT_3:15
.= ((s^2*m'^2)+m'^2) mod p
.= ((s*m')^2+m'^2) mod p by SQUARE_1:68; then
0 = ((n'^2 -(s*m')^2) mod p +(((s*m')^2+m'^2) mod p))mod p by A24,INT_4:12
.= ((n'^2 - (s*m')^2) + ((s*m')^2+m'^2)) mod p by INT_3:14
.= (n'^2+m'^2) mod p; then
p divides (n'^2+m'^2) by A1,INT_1:89; then
consider i be Integer such that
A25: (n'^2+m'^2) = p * i by INT_1:def 9;
A26: p * i = |.n'.|^2+m'^2 by A25,COMPLEX1:161
.= (abs n')^2+(abs m')^2 by COMPLEX1:161;
x' in p'' & x'' in p'' & y' in p'' & y'' in p'' by A21,CARD_1:def 12; then
x' < p'' & x'' < p'' & y' < p'' & y'' < p'' by NAT_1:45; then
A27: x' <= p' & x'' <= p' & y' <= p' & y'' <= p' by NAT_1:13;
x' in NAT & x'' in NAT & y' in NAT & y'' in NAT by ORDINAL1:def 13; then
reconsider x',x'',y',y'' as Real;
0 is Element of NAT by ORDINAL1:def 13; then
A28: abs(x'-x'') <= p' - 0 & abs(y'-y'') <= p' - 0 by A27,JGRAPH_1:31;
set n = abs n';
set m = abs m';
A29: n^2 <= p'^2 & m^2 <= p'^2 by A28,SQUARE_1:77;
p' <= sqrt(p) by INT_1:def 4; then
p'^2 <= (sqrt p)^2 by SQUARE_1:77; then
A30: p'^2 <= p by SQUARE_1:def 4;
p'^2 <> p
proof
assume p'^2 = p; then
reconsider p''=sqrt(p) as Element of NAT by SQUARE_1:def 4;
p''^2 = p by SQUARE_1:def 4; then
A31: p''*p'' = p by SQUARE_1:def 3; then
A32: p'' divides p by INT_1:def 9;
per cases by A32,A1,INT_2:def 5;
suppose p'' = 1;
hence contradiction by A31,A1,INT_2:def 5;
end;
suppose p'' = p; then
1 = (p*p)/p by A31,A1,XCMPLX_1:60
.= p*(p/p) by XCMPLX_1:75
.= p*1 by A1,XCMPLX_1:60;
hence contradiction by A1,INT_2:def 5;
end;
end; then
p'^2 < p by A30,XXREAL_0:1; then
n^2 < p & m^2 < p by A29,XXREAL_0:2; then
n^2 + m^2 < p + p by XREAL_1:10; then
(i*p)/p < (2*p)/p by A26,A1,XREAL_1:76; then
(i*p)/p < 2*(p/p) by XCMPLX_1:75; then
i*(p/p) < 2*(p/p) by XCMPLX_1:75; then
i*(p/p) < 2*1 by A1,XCMPLX_1:60; then
i*1 < 2 by A1,XCMPLX_1:60; then
i+1 <= 2 by INT_1:20; then
A33: i+1-1 <= 2-1 by XREAL_1:11;
n^2 + m^2 <> 0
proof
assume n^2 + m^2 = 0; then
n^2 = 0 & m^2 = 0; then
n*n = 0 & m*m = 0 by SQUARE_1:def 3; then
n = 0 & m = 0; then
x'-x'' = 0 & y'-y'' = 0 by ABSVALUE:7;
hence contradiction by A21;
end; then
i > 0 by A26; then
i >= 0+1 by INT_1:20; then
A34: i = 1 by A33,XXREAL_0:1;
take n,m;
thus p = n^2 + m^2 by A26,A34;
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 number;
correctness
proof
set b = f|J;
consider f' be FinSequence of REAL such that
A1: Sum b = Sum f' and
A2: f' = b*canFS(support b) by UPROOTS:def 3;
rng f' c= NAT
proof
let y be set;
assume y in rng f';
then consider x be set such that
A3: x in dom f' & y = f'.x by FUNCT_1:def 5;
thus y in NAT by A3,ORDINAL1:def 13,A2;
end;
then reconsider f' as FinSequence of NAT by FINSEQ_1:def 4;
Sum f' is Element of NAT;
hence thesis by A1;
end;
end;
theorem Th24:
for f being Function of NAT, NAT, F being Function of NAT, 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 Function of NAT, NAT;
let F be Function of NAT, REAL;
let J be finite Subset of NAT;
assume A1: f = F;
assume A2: ex k st J c= Seg k;
reconsider J' = J as finite Subset of J by ZFMISC_1:def 1;
A3: dom f = NAT by FUNCT_2:def 1; then
A4: J = dom(f|J') by RELAT_1:91;
reconsider f' = f|J' as bag of J;
support f' c= J' by A4,POLYNOM1:41; then
consider fs be FinSequence of REAL such that
A5: fs = f'*canFS(J') & Sum f' = Sum fs by UPROOTS:16;
A6: rng canFS J = J by FUNCT_2:def 3
.= dom f' by A3,RELAT_1:91; then
A7: dom canFS J = dom fs by A5,RELAT_1:46;
A8: fs,f' are_fiberwise_equipotent by A5,A7,A6,CLASSES1:85;
consider k such that
A9: J c= Seg k by A2;
per cases;
suppose A10: J is empty; then
A11: Sum fs = 0 by A5,RVSUM_1:102;
Sgm J = {} by A9,A10,FINSEQ_1:72; then
F*(Sgm J) = {};
hence thesis by A5,A11,RVSUM_1:102,BHSP_5:def 4;
end;
suppose J is non empty; then
reconsider J''=J as right_end (non empty natural-membered set);
rng Sgm J = J by A9,FINSEQ_1:def 13; then
A12: f*Sgm J = f*(J|Sgm J) by RELAT_1:125
.= (f|J)*Sgm J by MONOID_1:2;
A13: rng Sgm J = dom(f|J) by A4,A9,FINSEQ_1:def 13; then
A14: dom Sgm J = dom((f|J)*Sgm J) by RELAT_1:46;
Sgm J is one-to-one by A9,FINSEQ_3:99; then
(f|J)*Sgm J, f|J are_fiberwise_equipotent by A14,A13,CLASSES1:85; then
Func_Seq(F,Sgm J), f|J are_fiberwise_equipotent by A12,A1,BHSP_5:def 4;
hence Sum(f|J) = Sum Func_Seq(F,Sgm J) by A8,A5,RFINSEQ:22,CLASSES1:84;
end;
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;
assume A1: f = F;
reconsider J' = J as finite Subset of J by ZFMISC_1:def 1;
A2: dom f = I by FUNCT_2:def 1; then
A3: J = dom(f|J') by RELAT_1:91;
reconsider f' = f|J' as bag of J;
support f' c= J' by A3,POLYNOM1:41; then
consider fs be FinSequence of REAL such that
A4: fs = f'*canFS(J') & Sum f' = Sum fs by UPROOTS:16;
dom(F|J) is finite; then
A5: f|J,FinS(F,J) are_fiberwise_equipotent by A1,RFUNCT_3:def 14;
A6: rng canFS J = J by FUNCT_2:def 3
.= dom f' by A2,RELAT_1:91; then
A7: dom canFS J = dom fs by A4,RELAT_1:46;
fs,f' are_fiberwise_equipotent by A4,A7,A6,CLASSES1:85; then
Sum fs = Sum FinS(F,J) by RFINSEQ:22,A5,CLASSES1:84;
hence Sum(f|J) = Sum(F,J) by A4,RFUNCT_3:def 15;
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; then
A3: J = {};
A4: f|J = {} by A2;
set b = EmptyBag {};
A5: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {};
Sum b = 0 by UPROOTS:13;
hence Sum(f|(J \/ K)) = Sum(f|J) + Sum(f|K) by A3,A4,A5;
end;
suppose I is non empty; then
reconsider I' = I as non empty set;
A6: [:I',NAT:] c= [:I',REAL:] by ZFMISC_1:118;
f c= [:I',REAL:] by A6,XBOOLE_1:1; then
reconsider F = f as PartFunc of I', REAL; :: by RELSET_1:def 1;
A7: dom(F|(J \/ K)) is finite;
thus Sum(f|(J \/ K)) = Sum(F,J \/ K) by Th25
.= Sum(F,J) + Sum(F,K) by A7,A1,RFUNCT_3:86
.= Sum(f|J) + Sum(F,K) by Th25
.= Sum(f|J) + Sum(f|K) by Th25;
end;
end;
theorem Th27:
J = {j} implies Sum(f|J) = f.j
proof
assume A1: J = {j}; then
A2: 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 A1,ZFMISC_1:37; then
A3: dom(f|J) = J by RELAT_1:91; then
A4: support(f|J) c= J by POLYNOM1:41;
consider f' be FinSequence of REAL such that
A5: Sum(f|J) = Sum f' & f' = (f|J)*canFS(support(f|J)) by UPROOTS:def 3;
per cases by A1,A4,ZFMISC_1:39;
suppose A6: support(f|J) = {};
now assume f.j <> 0; then
(f|J).j <> 0 by A2,FUNCT_1:72;
hence contradiction by A6,POLYNOM1:def 7;
end;
hence Sum(f|J) = f.j by A6,A5,RVSUM_1:102;
end;
suppose support(f|J) = J; then
canFS(support(f|J)) = <*j*> by A1,UPROOTS:6; then
f' = <*(f|J).j*> by A2,A3,A5,BAGORDER:3; then
f' = <* f.j *> by A2,FUNCT_1:72;
hence Sum(f|J) = f.j by A5,RVSUM_1:103;
end;
end;
Lm11:
J = {j} implies Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K)
proof
defpred P[Nat] means
for I,j being set,
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
let I,j be set;
let f,g be Function of I, NAT;
let J,K be finite Subset of I;
assume A3: J = {j};
assume A4: k = card K;
k = 0 or k + 1 > 0 + 1 by XREAL_1:10; then
A5: k = 0 or k >= 1 by NAT_1:13;
per cases by A5,XXREAL_0:1;
suppose A6: k = 0;
A7: K = {} by A4,A6;
A8: g|K = {} by A7;
A9: [:J,K:] = {} by A7;
set b = EmptyBag {};
A10: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {};
Sum b = 0 by UPROOTS:13;
hence Sum((multnat*[:f,g:])|[:J,K:])=f.j*Sum(g|K) by A7,A8,A10,A9;
end;
suppose A11: k = 1;
consider x be set;
card {x} = card K by A11,A4,CARD_1:50; then
consider k' be set such that
A12: K = {k'} by CARD_1:49;
set b = (multnat*[:f,g:])|[:J,K:];
consider f' be FinSequence of REAL such that
A13: Sum b = Sum f' & f' = b*canFS(support b) by UPROOTS:def 3;
A14: [:J,K:] = {[j,k']} by ZFMISC_1:35,A12,A3; then
A15: [j,k'] in [:J,K:] by TARSKI:def 1; then
[j,k'] in [:I,I:]; then
A16: [j,k'] in dom(multnat*[:f,g:]) by FUNCT_2:def 1; then
[:J,K:] c= dom(multnat*[:f,g:]) by A14,ZFMISC_1:37; then
A17: dom b = [:J,K:] by RELAT_1:91; then
A18: support b c= [:J,K:] by POLYNOM1:41;
Sum b = f.j * g.k'
proof
set n1=f.j,n2=g.k';
reconsider I' = I as non empty set by A3;
reconsider j''=j,k''=k' as Element of I' by A3,A12,ZFMISC_1:37;
A19: f.j * g.k' = multnat.(n1,n2) by BINOP_2:def 24
.= multnat.[f.j'',g.k''] by BINOP_1:def 1
.= multnat.([:f,g:].(j'',k'')) by FUNCT_3:96
.= multnat.([:f,g:].[j,k']) by BINOP_1:def 1
.= (multnat*[:f,g:]).[j,k'] by A16,FUNCT_1:22
.= b.[j,k'] by A15,FUNCT_1:72;
per cases by A14,A18,ZFMISC_1:39;
suppose A20: support b = {};
f.j * g.k' = 0 by A19,A20,POLYNOM1:def 7;
hence Sum b = f.j * g.k' by A20,A13,RVSUM_1:102;
end;
suppose support b = {[j,k']}; then
A21: canFS(support b) = <* [j,k'] *> by UPROOTS:6;
f' = <* b.[j,k'] *> by A15,A17,A21,A13,BAGORDER:3;
hence Sum b = f.j * g.k' by A19,A13,RVSUM_1:103;
end;
end;
hence Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K) by A12,Th27;
end;
suppose A22: k > 1; then
K <> {} by A4; then
consider k' be set such that
A23: k' in K by XBOOLE_0:def 1;
set K0 = {k'};
set K1 = K \ K0;
reconsider K0 as finite Subset of I by A23,ZFMISC_1:37;
k' in K0 by TARSKI:def 1; then
not k' in K1 by XBOOLE_0:def 5; then
A24: card (K1 \/ K0) = card K1 + 1 by CARD_2:54;
A25: -1+k < 0+k by XREAL_1:10;
A26: K1 \/ K0 = K \/ {k'} by XBOOLE_1:39
.= K by A23,ZFMISC_1:46;
A27: card K0 < k by A22,CARD_1:50;
A28: [:J,K:] = [:J,K1:] \/ [:J,K0:] by A26,ZFMISC_1:120;
A29: K1 misses K0 by XBOOLE_1:79;
A30: [:J,K1:] misses [:J,K0:] by A29,ZFMISC_1:127;
A31: Sum((multnat*[:f,g:])|[:J,K0:]) = f.j * Sum(g|K0) by A27,A3,A2;
thus Sum((multnat*[:f,g:])|[:J,K:])
= Sum((multnat*[:f,g:])|[:J,K1:]) + Sum((multnat*[:f,g:])|[:J,K0:])
by A30,Th26,A28
.= f.j * Sum(g|K1) + f.j * Sum(g|K0) by A26,A3,A2,A31,A25,A4,A24
.= f.j * (Sum(g|K1) + Sum(g|K0))
.= f.j * Sum(g|K) by Th26,A26,XBOOLE_1:79;
end;
end;
end;
A32: for k being Nat holds P[k] from NAT_1:sch 4(A1);
P[card K] by A32;
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
let I be set;
let f,g be Function of I, NAT;
let J,K be finite Subset of I;
assume A3: k = card J;
k = 0 or k + 1 > 0 + 1 by XREAL_1:10; then
A4: k = 0 or k >= 1 by NAT_1:13;
per cases by A4,XXREAL_0:1;
suppose A5: k = 0;
A6: J = {} by A3,A5;
A7: [:J,K:] = {} by A6;
set b = EmptyBag {};
A8: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {};
Sum(f|J) = 0 by A8,A6,RELAT_1:110,UPROOTS:13;
hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K)
by A8,A7,UPROOTS:13,RELAT_1:110;
end;
suppose A9: k = 1;
consider x be set;
card {x} = card J by A9,A3,CARD_1:50; then
consider j be set such that
A10: J = {j} by CARD_1:49;
Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K) by A10,Lm11;
hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K) by A10,Th27;
end;
suppose A11: k > 1; then
J <> {} by A3; then
consider j be set such that
A12: j in J by XBOOLE_0:def 1;
set J0 = {j};
set J1 = J \ J0;
reconsider J0 as finite Subset of I by A12,ZFMISC_1:37;
j in J0 by TARSKI:def 1; then
not j in J1 by XBOOLE_0:def 5; then
A13: card (J1 \/ J0) = card J1 + 1 by CARD_2:54;
A14: -1+k < 0+k by XREAL_1:10;
A15: J1 \/ J0 = J \/ {j} by XBOOLE_1:39
.= J by A12,ZFMISC_1:46;
A16: card J0 < k by A11,CARD_1:50;
A17: [:J,K:] = [:J1,K:] \/ [:J0,K:] by A15,ZFMISC_1:120;
A18: J1 misses J0 by XBOOLE_1:79;
A19: Sum(f|J) = Sum(f|J1) + Sum(f|J0) by Th26,A15,XBOOLE_1:79;
A20: [:J1,K:] misses [:J0,K:] by A18,ZFMISC_1:127;
A21: Sum((multnat*[:f,g:])|[:J0,K:]) = Sum(f|J0) * Sum(g|K) by A16,A2;
thus Sum((multnat*[:f,g:])|[:J,K:]) = Sum((multnat*[:f,g:])|[:J1,K:])
+ Sum((multnat*[:f,g:])|[:J0,K:]) by A20,Th26,A17
.= Sum(f|J1) * Sum(g|K) + Sum(f|J0) * Sum(g|K) by A21,A2,A14,A3,A13,A15
.= Sum(f|J) * Sum(g|K) by A19;
end;
end;
end;
A22: for k being Nat holds P[k] from NAT_1:sch 4(A1);
P[card J] by A22;
hence thesis;
end;
definition
let k be natural number;
func EXP(k) -> Function of NAT, NAT means :Def1:
for n being natural number holds it.n = n|^k;
existence
proof
reconsider k'=k as Element of NAT by ORDINAL1:def 13;
deffunc F(Element of NAT) = $1|^k';
consider f be Function of NAT, 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 natural number holds f.n = n|^k
proof
let n be natural number;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
f.n' = F(n') by A1;
hence f.n = n|^k;
end;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of NAT , NAT;
assume A2: for n being natural number holds f1.n = n|^k;
assume A3: for n being natural number holds f2.n = n|^k;
for x being set st x in NAT holds f1.x = f2.x
proof
let x be set;
assume x in NAT; then
reconsider n=x as natural number;
f1.n = n|^k by A2 .= f2.n by A3;
hence f1.x = f2.x;
end;
hence f1 = f2 by FUNCT_2:18;
end;
end;
definition
let k,n be natural number;
func sigma(k,n) -> Element of NAT means :Def2:
for m being non zero natural number st n = m holds
it = Sum((EXP k)|NatDivisors m) if n<>0
otherwise it = 0;
correctness
proof
A1: n <> 0 implies ex n1 being Element of NAT st
for m being non zero natural number st n = m holds
n1 = Sum((EXP k)|NatDivisors m)
proof
assume n <> 0; then
reconsider n'=n as non zero natural number;
reconsider n1 = Sum((EXP k)|NatDivisors n') as Element of NAT
by ORDINAL1:def 13;
take n1;
let m be non zero natural number;
assume n = m; hence n1 = Sum((EXP k)|NatDivisors m);
end;
A2: not n <> 0 implies ex n1 being Element of NAT st n1 = 0
proof
assume not n <> 0;
reconsider n1=0 as Element of NAT by ORDINAL1:def 13;
take n1;
thus n1=0;
end;
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 natural number st n = m
holds n1 = Sum((EXP k)|NatDivisors m)) &
(for m being non zero natural number 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 A3: n <> 0;
assume A4: for m being non zero natural number st n = m
holds n1 = Sum((EXP k)|NatDivisors m);
assume A5: for m being non zero natural number st n = m
holds n2 = Sum((EXP k)|NatDivisors m);
reconsider m=n as non zero natural number by A3;
n1 = Sum((EXP k)|NatDivisors m) by A4;
hence n1 = n2 by A5;
end;
hence thesis by A1,A2;
end;
end;
definition
let k be natural number;
func Sigma(k) -> Function of NAT, NAT means :Def3:
for n being natural number holds it.n = sigma(k,n);
existence
proof
deffunc F(Element of NAT) = sigma(k,$1);
consider f be Function of NAT,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 natural number;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
thus f.n = f.n' .= sigma(k,n) by A1;
end;
uniqueness
proof
let f1,f2 be Function of NAT,NAT;
assume A2: for n being natural number holds f1.n = sigma(k,n);
assume A3: for n being natural number holds f2.n = sigma(k,n);
for x being set st x in NAT holds f1.x = f2.x
proof
let x be set;
assume x in NAT; then
reconsider n=x as natural number;
thus f1.x = sigma(k,n) by A2 .= f2.x by A3;
end;
hence f1 = f2 by FUNCT_2:18;
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;
A1: support b c= dom b by POLYNOM1:41;
1 in NAT; then
A2: 1 in dom EXP k by FUNCT_2:def 1;
1 in NatDivisors 1; then
A3: 1 in dom b by A2,RELAT_1:86;
A4: b.1 = (EXP k).1 by A3,FUNCT_1:70
.= 1|^k by Def1
.= 1 by NEWTON:15;
for x being set holds x in support b iff x = 1
proof
let x be set;
hereby
assume x in support b; then
x in NatDivisors 1 by A1,RELAT_1:86;
hence x = 1 by TARSKI:def 1,MOEBIUS1:41;
end;
assume x = 1; hence x in support b by A4,POLYNOM1:def 7;
end; then
A5: support b = {1} by TARSKI:def 1;
consider f be FinSequence of REAL such that
A6: Sum b = Sum f & f = b * (canFS (support b)) by UPROOTS:def 3;
f = b * <*1*> by A6,A5,UPROOTS:6
.= <*b.1*> by A3,BAGORDER:3; then
A7: Sum b = 1 by A6,A4,RVSUM_1:103;
thus sigma(k,1) = 1 by A7,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 natural number st p is prime
holds sigma(p|^$1) = (p|^($1+1) - 1)/(p - 1);
A1: P[0]
proof
let p be natural number;
assume p is prime; then
p > 1 by INT_2:def 5; then
A2: p-1 > 1-1 by XREAL_1:16;
thus sigma(p|^0) = sigma(1) by NEWTON:9 .= 1 by Th29
.= (p - 1)/(p - 1) by A2,XCMPLX_1:60
.= (p|^(0+1) - 1)/(p - 1) by NEWTON:10;
end;
A3: for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A4: P[k];
thus P[k + 1]
proof
let p be natural number;
assume A5: p is prime; then
A6: p > 1 by INT_2:def 5; then
A7: p-1 > 1-1 by XREAL_1:16;
reconsider m = p|^(k+1) as non zero natural number by A5;
reconsider m' = p|^k as non zero natural number by A5;
reconsider k'=k+1,p'=p as Element of NAT by ORDINAL1:def 13;
for x being set holds x in NatDivisors(p|^(k+1)) iff
x in NatDivisors(p|^k) \/ {p|^(k+1)}
proof
let x be set;
hereby
assume x in NatDivisors(p|^(k+1)); then
x in {p|^t where t is Element of NAT : t <= k+1} by A5,Th19; then
consider t be Element of NAT such that
A8: x = p|^t & t <= (k+1);
per cases;
suppose t <= k; then
x in {p|^t' where t' is Element of NAT : t' <= k} by A8; then
x in NatDivisors(p|^k) by A5,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 A8,XXREAL_0:1; then
x in {p|^(k+1)} by A8,TARSKI:def 1;
hence x in NatDivisors(p|^k) \/ {p|^(k+1)} by XBOOLE_0:def 3;
end;
end;
assume A9: x in NatDivisors(p|^k) \/ {p|^(k+1)};
per cases by A9,XBOOLE_0:def 3;
suppose x in NatDivisors(p|^k); then
x in {p|^t where t is Element of NAT : t <= k} by A5,Th19; then
consider t be Element of NAT such that
A10: x = p|^t & t <= k;
0+k <= 1+k by XREAL_1:9; then
t <= k+1 by A10,XXREAL_0:2; then
x in {p|^t' where t' is Element of NAT : t' <= k+1} by A10;
hence x in NatDivisors(p|^(k+1)) by A5,Th19;
end;
suppose x in {p|^(k+1)}; then
x = p|^k' & k'<=k+1 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 A5,Th19;
end;
end; then
A11: NatDivisors(p|^(k+1)) = NatDivisors(p|^k) \/ {p|^(k+1)} by TARSKI:2;
reconsider J = NatDivisors(p|^k) as finite Subset of NAT by A5;
p'|^k' in NAT; then
reconsider K = {p|^(k+1)} as finite Subset of NAT by ZFMISC_1:37;
now let x be set;
assume x in J /\ K; then
A12: x in J & x in K by XBOOLE_0:def 4; then
x in {p|^t where t is Element of NAT : t <= k} by A5,Th19; then
consider t be Element of NAT such that
A13: x = p|^t & t <= k;
p|^(k+1) = p|^t by A13,A12,TARSKI:def 1; then
p |-count p|^(k+1) = t by A6,NAT_3:25; then
k+1 = t by A6,NAT_3:25; then
k+1-k <= k-k by A13,XREAL_1:11; then
1 <= 0;
hence contradiction;
end; then
J /\ K = {} by XBOOLE_0:def 1; then
A14: J misses K by XBOOLE_0:def 7;
A15: sigma(1,m) = Sum((EXP 1)|(J \/ K)) by Def2,A11
.= Sum((EXP 1)|J) + Sum((EXP 1)|K) by A14,Th26
.= Sum((EXP 1)|J) + (EXP 1).(p|^(k+1)) by Th27;
A16: (EXP 1).(p|^(k+1)) = (p|^(k+1))|^1 by Def1
.= p|^((k+1)*1) by NEWTON:14 .= p|^(k+1);
A17: Sum((EXP 1)|J) = sigma(1,m') by Def2 .= sigma(p|^k)
.= (p|^(k+1) - 1)/(p - 1) by A4,A5;
thus sigma(p|^(k+1)) = (p|^(k+1) - 1)/(p - 1) + p|^(k+1)*(p - 1)/(p - 1)
by A15,A16,A17,A7,XCMPLX_1:90
.= ((p|^(k+1) - 1) + p|^(k+1)*(p - 1))/(p - 1) by XCMPLX_1:63
.= (p|^(k+1)*p - 1)/(p - 1)
.= (p|^((k+1)+1) - 1)/(p - 1) by NEWTON:11;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A3);
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 A2,A1,WSIERP_1:20; end;
suppose A4: n0 <> 1;
reconsider X = {1,m,n0} as finite Subset of NAT by Lm2;
for x being set st x in X holds x in NatDivisors n0
proof
let x be set;
assume A5: x in X; then
A6: x = 1 or x = m or x = n0 by ENUMSET1:def 1;
reconsider x'=x as Element of NAT by A5;
A7: x' <> 0 by A6,A1,INT_2:10;
x' divides n0 by A6,A1,NAT_D:6;
hence x in NatDivisors n0 by A7;
end; then
A8: X c= NatDivisors n0 by TARSKI:def 3;
set Y = NatDivisors(n0) \ X;
A9: NatDivisors n0 = X \/ Y by A8,XBOOLE_1:45;
A10: sigma n0 = Sum((EXP 1)|(X \/ Y)) by A9,Def2
.= Sum((EXP 1)|X) + Sum((EXP 1)|Y) by XBOOLE_1:79,Th26;
set X1 = {1};
reconsider X2 = {m,n0} as finite Subset of NAT by Th5;
reconsider X3 = {m} as finite Subset of NAT by Th4;
reconsider X4 = {n0} as finite Subset of NAT by Th4;
A11: X2 = X3 \/ X4 by ENUMSET1:41;
now let x be set;
assume x in X3 /\ X4; then
x in X3 & x in X4 by XBOOLE_0:def 4; then
x = m & x = n0 by TARSKI:def 1;
hence contradiction by A2;
end; then
X3 /\ X4 = {} by XBOOLE_0:def 1; then
A12: X3 misses X4 by XBOOLE_0:def 7;
now let x be set;
assume x in X1 /\ X2; then
x in X1 & x in X2 by XBOOLE_0:def 4; then
x = 1 & x in X2 by TARSKI:def 1;
hence contradiction by A3,A4,TARSKI:def 2;
end; then
X1 /\ X2 = {} by XBOOLE_0:def 1; then
A13: X1 misses X2 by XBOOLE_0:def 7;
X = X1 \/ X2 by ENUMSET1:42; then
A14: Sum((EXP 1)|X) = Sum((EXP 1)|X1) + Sum((EXP 1)|X2) by A13,Th26
.= (EXP 1).1 + Sum((EXP 1)|X2) by Th27
.= (EXP 1).1 + (Sum((EXP 1)|X3) + Sum((EXP 1)|X4)) by A11,A12,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 by NEWTON:10
.= 1 + m + n0|^1 by NEWTON:10
.= 1 + m + n0 by NEWTON:10;
0 + Sum((EXP 1)|X) <= Sum((EXP 1)|Y) + Sum((EXP 1)|X) by XREAL_1:9;
hence 1+m+n0 <= sigma n0 by A10,A14;
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 A1: m divides n0;
assume A2: k divides n0;
assume A3: n0<>m;
assume A4: n0<>k;
assume A5: m<>1;
assume A6: k<>1;
assume A7: m<>k;
per cases;
suppose n0 = 1;
hence thesis by A3,A1,WSIERP_1:20;
end;
suppose A8: n0 <> 1;
reconsider X = {1,m,k,n0} as finite Subset of NAT by Lm3;
for x being set st x in X holds x in NatDivisors n0
proof
let x be set;
assume A9: x in X; then
A10: x = 1 or x = m or x = k or x = n0 by ENUMSET1:def 2;
reconsider x'=x as Element of NAT by A9;
A11: x' <> 0 by A10,A1,A2,INT_2:10;
x' divides n0 by A10,A1,A2,NAT_D:6;
hence x in NatDivisors n0 by A11;
end; then
A12: X c= NatDivisors n0 by TARSKI:def 3;
set Y = NatDivisors(n0) \ X;
A13: NatDivisors n0 = X \/ Y by A12,XBOOLE_1:45;
A14: sigma n0 = Sum((EXP 1)|(X \/ Y)) by A13,Def2
.= Sum((EXP 1)|X) + Sum((EXP 1)|Y) by XBOOLE_1:79,Th26;
set X1 = {1};
reconsider X2 = {m,k,n0} as finite Subset of NAT by Lm2;
reconsider X3 = {m,k} as finite Subset of NAT by Th5;
reconsider X4 = {n0} as finite Subset of NAT by Th4;
reconsider X5 = {m} as finite Subset of NAT by Th4;
reconsider X6 = {k} as finite Subset of NAT by Th4;
A15: X3 = X5 \/ X6 by ENUMSET1:41;
now let x be set;
assume x in X5 /\ X6; then
x in X5 & x in X6 by XBOOLE_0:def 4; then
x = m & x = k by TARSKI:def 1;
hence contradiction by A7;
end; then
X5 /\ X6 = {} by XBOOLE_0:def 1; then
A16: X5 misses X6 by XBOOLE_0:def 7;
A17: X2 = X3 \/ X4 by ENUMSET1:43;
now let x be set;
assume x in X3 /\ X4; then
x in X3 & x in X4 by XBOOLE_0:def 4; then
x in X3 & x = n0 by TARSKI:def 1;
hence contradiction by A3,A4,TARSKI:def 2;
end; then
X3 /\ X4 = {} by XBOOLE_0:def 1; then
A18: X3 misses X4 by XBOOLE_0:def 7;
now let x be set;
assume x in X1 /\ X2; then
x in X1 & x in X2 by XBOOLE_0:def 4; then
x = 1 & x in X2 by TARSKI:def 1;
hence contradiction by A5,A8,A6,ENUMSET1:def 1;
end; then
X1 /\ X2 = {} by XBOOLE_0:def 1; then
A19: X1 misses X2 by XBOOLE_0:def 7;
X = X1 \/ X2 by ENUMSET1:44; then
A20: Sum((EXP 1)|X) = Sum((EXP 1)|X1) + Sum((EXP 1)|X2) by A19,Th26
.= (EXP 1).1 + Sum((EXP 1)|X2) by Th27
.= (EXP 1).1 + (Sum((EXP 1)|X3) + Sum((EXP 1)|X4)) by A17,A18,Th26
.= (EXP 1).1 + (Sum((EXP 1)|X5) + Sum((EXP 1)|X6) + Sum((EXP 1)|X4))
by A15,A16,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 by NEWTON:10
.= 1 + m + k|^1 + n0|^1 by NEWTON:10
.= 1 + m + k + n0|^1 by NEWTON:10
.= 1 + m + k + n0 by NEWTON:10;
0 + Sum((EXP 1)|X) <= Sum((EXP 1)|Y) + Sum((EXP 1)|X) by XREAL_1:9;
hence 1+m+k+n0 <= sigma n0 by A14,A20;
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:10;
end;
suppose A4: n0 <> 1;
consider k be natural number such that
A5: n0 = m * k by A2,NAT_D:def 3;
A6: k <> m
proof
assume k = m; then
m <> 1 by A5,A4; then
1 + m + n0 <= sigma n0 by A2,A3,Th31; then
1 + m + n0 - (m + n0) <= n0 + m - (m + n0) by A1,XREAL_1:11;
hence contradiction;
end;
k = n0
proof
assume A7: k <> n0;
A8: k divides n0 by A5,NAT_D:def 3;
A9: k <> 1 by A5,A3;
m<>1 by A5,A7; then
1 + m + k + n0 <= sigma n0 by A2,A3,A7,A8,A9,A6,Th32; then
1 + m + k + n0 - (m + n0) <= n0 + m - (m + n0) by A1,XREAL_1:11; then
1 + k <= 0;
hence contradiction;
end; then
n0/n0 = m by A5,XCMPLX_1:90;
hence A10: m = 1 by XCMPLX_1:60;
A11: n0 > 1 by A4,NAT_1:26;
for k being natural number holds not k divides n0 or k = 1 or k = n0
proof
let k be natural number;
assume A12: k divides n0 & k <> 1;
assume k <> n0; then
1 + k + n0 <= n0 + 1 by A1,A10,A12,Th31; then
1 + k + n0 - (1 + n0) <= n0 + 1 - (1 + n0) by XREAL_1:11; then
k = 0;
hence contradiction by A12,INT_2:3;
end;
hence n0 is prime by A11,INT_2:def 5;
end;
end;
definition
let f be Function of NAT, NAT;
attr f is multiplicative means :Def5:
for n0,m0 being non zero natural number st n0,m0 are_relative_prime
holds f.(n0*m0) = f.n0 * f.m0;
end;
theorem Th34:
for f,F being Function of NAT, NAT st
f is multiplicative &
(for n0 holds F.n0 = Sum(f|NatDivisors n0))
holds F is multiplicative
proof
let f,F be Function of NAT, NAT;
assume A1: f is multiplicative;
assume A2: for n0 holds F.n0 = Sum(f|NatDivisors n0);
for n,m being non zero natural number st n,m are_relative_prime
holds F.(n*m) = F.n * F.m
proof
let n,m be non zero natural number;
assume A3: n,m are_relative_prime;
set b1 = f|NatDivisors(n*m);
set b2 = (multnat * [:f,f:])|[:NatDivisors n, NatDivisors m:];
consider f1 be FinSequence of REAL such that
A4: Sum b1 = Sum f1 & f1 = b1 * (canFS (support b1)) by UPROOTS:def 3;
consider f2 be FinSequence of REAL such that
A5: Sum b2 = Sum f2 & f2 = b2 * (canFS (support b2)) by UPROOTS:def 3;
set g1 = canFS (support b1);
set g2 = canFS (support b2);
set h' = multnat|[:NatDivisors n, NatDivisors m:];
dom multnat = [:NAT, NAT:] by FUNCT_2:def 1; then
A6: dom h' = [:NatDivisors n, NatDivisors m:] by RELAT_1:91;
A7: dom [:f,f:] = [:NAT, NAT:] by FUNCT_2:def 1;
dom(multnat * [:f,f:]) = [:NAT, NAT:] by FUNCT_2:def 1; then
A8: dom b2 = [:NatDivisors n, NatDivisors m:] by RELAT_1:91;
dom f = NAT by FUNCT_2:def 1; then
A9: dom b1 = NatDivisors(n*m) by RELAT_1:91;
for x1,x2 being set st x1 in dom h' & x2 in dom h' & h'.x1 = h'.x2
holds x1 = x2
proof
let x1,x2 be set;
assume A10: x1 in dom h'; then
consider n1, m1 be set such that
A11: n1 in NatDivisors n & m1 in NatDivisors m &
x1 = [n1,m1] by A6,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by A11;
assume A12: x2 in dom h'; then
consider n2, m2 be set such that
A13: n2 in NatDivisors n & m2 in NatDivisors m &
x2 = [n2,m2] by A6,ZFMISC_1:def 2;
reconsider n2,m2 as Element of NAT by A13;
assume A14: h'.x1 = h'.x2;
A15: h'.x1 = multnat.x1 by A10,FUNCT_1:70
.= multnat.(n1,m1) by A11,BINOP_1:def 1
.= n1*m1 by BINOP_2:def 24;
h'.x2 = multnat.x2 by A12,FUNCT_1:70
.= multnat.(n2,m2) by A13,BINOP_1:def 1
.= n2*m2 by BINOP_2:def 24; then
n1=n2 & m1=m2 by A11,A13,A3,A15,A14,Th15;
hence x1 = x2 by A11,A13;
end; then
reconsider h' as one-to-one Function by FUNCT_1:def 8;
set h = g1" * h' * g2;
A16: dom h = dom f2
proof
A17: support b2 c= dom b2 by POLYNOM1:41;
for x being set st x in support b2 holds x in dom(g1" * h')
proof
let x be set;
assume A18: x in support b2; then
A19: b2.x <> 0 by POLYNOM1:def 7;
A20: x in [:NatDivisors n, NatDivisors m:] by A8,A18,A17;
consider n1, m1 be set such that
A21: n1 in NatDivisors n & m1 in NatDivisors m &
x = [n1,m1] by A8,A18,A17,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by A21;
reconsider n1'=n1,m1'=m1 as non zero natural number by A21,MOEBIUS1:39;
set x' = (g1").(n1*m1);
A22: rng g1 = support b1 by FUNCT_2:def 3;
set fn1=f.n1,fm1=f.m1;
A23: n1,m1 are_relative_prime by Th14,A21,A3;
b2.x = (multnat * [:f,f:]).x by A8,A18,A17,FUNCT_1:72
.= multnat.([:f,f:].x) by A7,A20,FUNCT_1:23
.= multnat.([:f,f:].(n1,m1)) by A21,BINOP_1:def 1
.= multnat.[f.n1,f.m1] by FUNCT_3:96
.= multnat.(f.n1,f.m1) by BINOP_1:def 1
.= (fn1)*(fm1) by BINOP_2:def 24
.= f.(n1'*m1') by A23,A1,Def5
.= (f|NatDivisors(n*m)).(n1*m1) by A21,Th16,FUNCT_1:72; then
A24: n1*m1 in rng g1 by A22,A19,POLYNOM1:def 7; then
n1*m1 in dom(g1") by FUNCT_1:55; then
x' in rng(g1") by FUNCT_1:12; then
A25: x' in dom g1 by FUNCT_1:55;
g1.x' = n1*m1 by A24,FUNCT_1:57
.= multnat.(n1,m1) by BINOP_2:def 24
.= multnat.[n1,m1] by BINOP_1:def 1
.= h'.x by A21,A8,A18,A17,FUNCT_1:72; then
h'.x in rng g1 by A25,FUNCT_1:def 5; then
h'.x in dom(g1") by FUNCT_1:55;
hence x in dom(g1" * h') by A6,A8,A18,A17,FUNCT_1:21;
end; then
support b2 c= dom(g1" * h') by TARSKI:def 3; then
rng g2 c= dom(g1" * h') by FUNCT_2:def 3; then
A26: dom(g1" * h' * g2) = dom g2 by RELAT_1:46;
rng g2 c= dom b2 by A17,FUNCT_2:def 3;
hence thesis by A5,A26,RELAT_1:46;
end;
A27: rng h = dom f1
proof
A28: support b1 c= dom b1 by POLYNOM1:41;
rng g1 c= dom b1 by A28,FUNCT_2:def 3; then
A29: dom(b1 * g1) = dom g1 by RELAT_1:46;
for y being set st y in rng g1 holds y in rng(h' * g2)
proof
let y be set;
assume A30: y in rng g1; then
A31: y in support b1;
A32: b1.y <> 0 by A30,POLYNOM1:def 7;
A33: support b1 c= dom b1 by POLYNOM1:41;
consider n1,m1 be natural number such that
A34: n1 in NatDivisors n & m1 in NatDivisors m & y=n1*m1
by A33,Th18,A3,A9,A31;
reconsider n1'=n1,m1'=m1 as non zero natural number by A34,MOEBIUS1:39;
reconsider n1,m1 as Element of NAT by ORDINAL1:def 13;
set x = g2".[n1,m1];
A35: n1,m1 are_relative_prime by Th14,A34,A3;
set fn1=f.n1,fm1=f.m1;
A36: [n1,m1] in [:NatDivisors n, NatDivisors m:]
by A34,ZFMISC_1:def 2;
A37: [n1,m1] in [:NatDivisors n, NatDivisors m:] by A34,ZFMISC_1:def 2;
b1.y = f.y by A33,A9,A31,FUNCT_1:72
.= (f.n1')*(f.m1') by A34,A35,A1,Def5
.= 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:96
.= multnat.([:f,f:].[n1,m1]) by BINOP_1:def 1
.= (multnat * [:f,f:]).[n1,m1] by A7,FUNCT_1:23
.= b2.[n1,m1] by A37,FUNCT_1:72; then
[n1,m1] in support b2 by A32,POLYNOM1:def 7; then
A38: [n1,m1] in rng g2 by FUNCT_2:def 3; then
[n1,m1] in dom(g2") by FUNCT_1:55; then
x in rng(g2") by FUNCT_1:12; then
A39: x in dom g2 by FUNCT_1:55;
g2.(g2".[n1,m1]) = [n1,m1] by A38,FUNCT_1:57; then
A40: x in dom(h' * g2) by A39,A36,A6,FUNCT_1:21;
y = multnat.(n1,m1) by A34,BINOP_2:def 24
.= multnat.[n1,m1] by BINOP_1:def 1
.= (multnat|[:NatDivisors n, NatDivisors m:]).[n1,m1] by A36,FUNCT_1:72
.= h'.(g2.(g2".[n1,m1])) by A38,FUNCT_1:57
.= (h' * g2).x by A39,FUNCT_1:23;
hence y in rng(h' * g2) by A40,FUNCT_1:def 5;
end; then
rng g1 c= rng(h' * g2) by TARSKI:def 3; then
dom(g1") c= rng(h' * g2) by FUNCT_1:55; then
rng(g1" * (h' * g2)) = rng(g1") by RELAT_1:47; then
rng(g1" * (h' * g2)) = dom g1 by FUNCT_1:55;
hence thesis by A4,A29,RELAT_1:55;
end;
A41: for x being set holds x in dom f2 iff x in dom h & h.x in dom f1
by A16,A27,FUNCT_1:12;
A42: for x being set st x in dom f2 holds f2.x = f1.(h.x)
proof
let x be set;
assume A43: x in dom f2; then
A44: x in dom g2 & g2.x in dom b2 by A5,FUNCT_1:21;
A45: (b1*g1).(h.x) = (b1*g1*h).x by FUNCT_1:23,A43,A16
.= (b1*g1*(g1" * h') * g2).x by RELAT_1:55
.= (b1*g1*(g1" * h')).(g2.x) by A44,FUNCT_1:23;
set x' = g2.x;
A46: support b2 c= dom b2 by POLYNOM1:41;
A47: x' in rng g2 by A44,FUNCT_1:12; then
A48: x' in support b2;
A49: x' in [:NatDivisors n, NatDivisors m:] by A48,A46,A8;
consider n1, m1 be set such that
A50: n1 in NatDivisors n & m1 in NatDivisors m &
x' = [n1,m1] by A48,A46,A8,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by A50;
reconsider n1'=n1,m1'=m1 as non zero natural number by A50,MOEBIUS1:39;
set fn1=f.n1,fm1=f.m1;
A51: n1,m1 are_relative_prime by Th14,A50,A3;
A52: b1*g1*(g1" * h') = b1*g1* g1" * h' by RELAT_1:55
.= b1*(g1* g1")*h' by RELAT_1:55
.= b1*(id rng g1)*h' by FUNCT_1:61
.= b1*(id support b1)*h' by FUNCT_2:def 3;
A53: b2.x' <> 0 by A47,POLYNOM1:def 7;
A54: b2.x' = (multnat * [:f,f:]).x' by A48,A46,A8,FUNCT_1:72
.= multnat.([:f,f:].x') by A7,A49,FUNCT_1:23
.= multnat.([:f,f:].(n1,m1)) by A50,BINOP_1:def 1
.= multnat.[f.n1,f.m1] by FUNCT_3:96
.= multnat.(f.n1,f.m1) by BINOP_1:def 1
.= (fn1)*(fm1) by BINOP_2:def 24
.= f.(n1'*m1') by A51,A1,Def5;
f.(n1'*m1') = (f|NatDivisors(n*m)).(n1*m1) by A50,Th16,FUNCT_1:72; then
A55: n1*m1 in support b1 by A53,A54,POLYNOM1:def 7; then
A56: n1*m1 in dom (id support b1) by RELAT_1:71;
A57: h'.x' = multnat.x' by A48,A46,A6,A8,FUNCT_1:70
.= multnat.(n1,m1) by A50,BINOP_1:def 1
.= n1*m1 by BINOP_2:def 24;
(b1*(id support b1)*h').x'
= (b1*(id support b1)).(h'.x') by A48,A46,A6,A8,FUNCT_1:23
.= b1.((id support b1).(n1*m1)) by A57,A56,FUNCT_1:23
.= b1.(n1*m1) by A55,FUNCT_1:35
.= b2.x' by A54,A50,Th16,FUNCT_1:72;
hence f2.x = f1.(h.x) by A4,A5,A44,A45,A52,FUNCT_1:23;
end;
f2 = f1 * h by A41,A42,FUNCT_1:20; then
A58: f1,f2 are_fiberwise_equipotent by A16,A27,CLASSES1:85;
thus F.(n*m) = Sum(f|NatDivisors(n*m)) by A2
.= Sum((multnat * [:f,f:])|[:NatDivisors n, NatDivisors m:])
by A4,A5,A58,RFINSEQ:22
.= 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 by Def5;
end;
theorem Th35:
EXP(k) is multiplicative
proof
for n,m being non zero natural number st n,m are_relative_prime
holds (EXP(k)).(n*m) = (EXP(k)).n * (EXP(k)).m
proof
let n,m be non zero natural number;
assume n,m are_relative_prime;
thus (EXP(k)).(n*m) = (n*m)|^k by Def1
.= n|^k * m|^k by NEWTON:12
.= (EXP(k)).n * m|^k by Def1
.= (EXP(k)).n * (EXP(k)).m by Def1;
end;
hence EXP(k) is multiplicative by Def5;
end;
theorem Th36:
Sigma(k) is multiplicative
proof
for n being non zero natural number
holds (Sigma k).n = Sum((EXP k)|NatDivisors n)
proof
let n be non zero natural number;
thus (Sigma k).n = sigma(k,n) by Def3
.= Sum((EXP k)|NatDivisors n) by Def2;
end;
hence Sigma(k) is multiplicative by Th35,Th34;
end;
theorem Th37:
n0,m0 are_relative_prime implies sigma(n0*m0) = sigma(n0) * sigma m0
proof
assume A1: n0,m0 are_relative_prime;
A2: Sigma 1 is multiplicative by Th36;
thus sigma(n0*m0) = (Sigma 1).(n0*m0) by Def3
.= ((Sigma 1).n0) * (Sigma 1).m0 by A2,A1,Def5
.= 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 :Def6:
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
assume A1: 2|^p -' 1 is prime;
assume A2: n0 = 2|^(p -' 1)*(2|^p -' 1);
A3: now assume A4: p <= 1;
per cases by A4,NAT_1:26;
suppose p = 0; then
2|^p -' 1 = 1 -' 1 by NEWTON:9
.= 1 - 1 by XREAL_0:def 2 .= 0;
hence contradiction by A1;
end;
suppose p = 1; then
2|^p -' 1 = 2 -' 1 by NEWTON:10
.= 2 - 1 by XREAL_0:def 2 .= 1;
hence contradiction by A1,INT_2:def 5;
end;
end; then
A5: p-1>1-1 by XREAL_1:11; then
A6: p -' 1 = p - 1 by XREAL_0:def 2;
set n1=2|^(p -' 1);
A7: 2|^p > p by NEWTON:105;
2|^p > 1 by A3,XXREAL_0:2,NEWTON:105; then
A8: 2|^p - 1 > 1 - 1 by XREAL_1:11; then
A9: 2|^p - 1 = 2|^p -' 1 by XREAL_0:def 2;
reconsider n2=2|^p -' 1 as non zero natural number by A8,XREAL_0:def 2;
set k = p -' 2;
p>=1+1 by A3,NAT_1:13; then
p-2 >= 2-2 by XREAL_1:11; then
k = p - 2 by XREAL_0:def 2; then
p -' 1 = k + 1 & p = k + 2 by A5,XREAL_0:def 2; then
A10: n1,n2 are_relative_prime by A1,EULER_1:3,A9,Th1;
A11: (2|^p - 1)|^2 = (2|^p - 1)|^(1+1)
.= ((2|^p - 1)|^1)*(2|^p - 1) by NEWTON:11
.= (2|^p - 1)*(2|^p - 1) by NEWTON:10
.= (2|^p - 1)^2 by SQUARE_1:def 3
.= (2|^p)^2 - 2*(2|^p)*1 + 1^2 by SQUARE_1:64
.= (2|^p)*(2|^p) -2*(2|^p) + 1^2 by SQUARE_1:def 3
.= (2|^p)*(2|^p) -2*(2|^p) + 1*1 by SQUARE_1:def 3
.= (2|^p)*(2|^p - 2) + 1;
2|^p >= p+1 by A7,NAT_1:13; then
A12: 2|^p - 2 >= p+1-2 by XREAL_1:11;
sigma n0 = (sigma n1)*sigma n2 by A2,A10,Th37
.= (2|^(p -' 1 + 1) - 1)/(2 - 1)*sigma n2 by INT_2:44,Th30
.= sigma(n2|^1)*(2|^p -' 1) by A6,A9,NEWTON:10
.= (n2|^(1+1)-1)/(n2 - 1)*(2|^p -' 1) by A1,Th30
.= 2|^(p -' 1 + 1)*(2|^p -' 1) by A6,A9,A12,A5,XCMPLX_1:90,A11
.= 2|^(p -' 1)*2*(2|^p -' 1) by NEWTON:11
.= 2 * n0 by A2;
hence n0 is perfect by Def6;
end;
:: Euler
theorem
n0 is even & n0 is perfect implies
ex p being natural number
st 2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1)
proof
assume n0 is even; then
consider k',n' be natural number such that
A1: n' is odd & k' > 0 & n0 = 2|^k' * n' by Th2;
assume n0 is perfect; then
A2: sigma n0 = 2 * n0 by Def6;
k'>=0+1 by A1,NAT_1:13; then
A3: k'+1 >= 1+1 by XREAL_1:9;
set p=k'+1;
A4: p - 1 = p -' 1 by XREAL_0:def 2;
take p;
reconsider n2=n' as non zero natural number by A1;
A5: 2|^p - 1 > p - 1 by NEWTON:105,XREAL_1:16;
A6: 2|^p - 1 = 2|^p -' 1 by A5,XREAL_0:def 2;
sigma(2|^(p -' 1)) = (2|^(p -' 1 + 1) - 1)/(2 - 1) by INT_2:44,Th30
.= 2|^p - 1 by A4; then
A7: (2|^p - 1)*sigma(n') = 2 * 2|^(p -' 1)*n' by A4,Th37,A1,Th3,A2
.= 2|^p*n' by A4,NEWTON:11; then
A8: (2|^p -' 1) divides 2|^p*n2 by A6,INT_1:def 9;
2|^p - 1 = 2|^(p-'1+1)-2+1 by A4
.= 2|^(p-'1)*2-2+1 by NEWTON:11
.= 2*(2|^(p-'1)-1)+1; then
(2|^p -' 1) divides n2 by A8,EULER_1:14,A6,Th3; then
consider n'' be natural number such that
A9: n' = (2|^p -' 1)*n'' by NAT_D:def 3;
A10: n'' divides n' by A9,NAT_D:def 3;
2|^p > 2 by NEWTON:105,A3,XXREAL_0:2; then
2|^p -1 > 2-1 by XREAL_1:16; then
A11: (2|^p -' 1)*n2 > 1*n2 by A6,XREAL_1:70;
sigma(n')*(2|^p - 1) = 2|^p*n''*(2|^p - 1) by A6,A9,A7; then
sigma(n2) = (2|^p - 1)*n'' + n'' by A5,XCMPLX_1:5
.= n' + n'' by A5,XREAL_0:def 2,A9; then
A12: n''=1 & n' is prime by Th33,A10,A11,A9;
hence 2|^p -' 1 is prime by A9;
thus n0 = 2|^(p -' 1)*(2|^p -' 1) by A9,A12,A1,A4;
end;
begin :: A Formula involving Euler's Function
definition
func Euler_phi -> Function of NAT, NAT means :Def7:
for k being Element of NAT holds it.k = Euler(k);
existence
proof
ex f being Function of NAT,NAT st
for k being Element of NAT holds f.k = Euler(k) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of NAT, NAT such that
A1: for k being Element of NAT holds f1.k = Euler(k) and
A2: for k being Element of NAT holds f2.k = Euler(k);
for f1, f2 be Function of NAT, 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;
hence thesis by A1,A2;
end;
end;
:: Number Theory (Andrews) p.76
theorem
Sum(Euler_phi|NatDivisors n0) = n0
proof
set X = Seg n0;
defpred P[set,set] means
$2 = {i where i is Element of NAT: ex h being natural number st
i in X & $1 in NatDivisors n0 & h=$1 & i gcd n0 = n0 / h};
A1: for k being natural number st k in X
ex x being Element of bool X st P[k,x]
proof
let k be natural number;
assume k in X;
set X' = {i where i is Element of NAT: ex h being natural number st
i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h};
for x being set st x in X' holds x in X
proof
let x be set;
assume x in X'; then
consider i be Element of NAT such that
A2: i=x & ex h being natural number st
i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h;
thus x in X by A2;
end; then
reconsider X' as Element of bool X by TARSKI:def 3;
take X';
thus P[k,X'];
end;
consider fp be FinSequence of bool X such that
A3: dom fp = X & for k being natural number st k in X
holds P[k,fp.k] from FINSEQ_1:sch 5(A1);
set k = len fp;
A4: len fp = k;
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
A5: fp.d = {i where i is Element of NAT: ex h being natural number st
i in X & d in NatDivisors n0 & h=d & i gcd n0 = n0 / h} by A3;
assume e in dom fp; then
A6: fp.e = {i where i is Element of NAT: ex h being natural number st
i in X & e in NatDivisors n0 & h=e & i gcd n0 = n0 / h} by A3;
assume A7: d<>e;
assume not fp.d misses fp.e; then
fp.d /\ fp.e <> {} by XBOOLE_0:def 7; then
consider x be set such that
A8: x in fp.d /\ fp.e by XBOOLE_0:def 1;
A9: x in fp.d & x in fp.e by A8,XBOOLE_0:def 4;
consider i1 be Element of NAT such that
A10: x=i1 & ex h being natural number st
i1 in X & d in NatDivisors n0 & h=d & i1 gcd n0 = n0 / h by A5,A9;
consider i2 be Element of NAT such that
A11: x=i2 & ex h being natural number st
i2 in X & e in NatDivisors n0 & h=e & i2 gcd n0 = n0 / h by A6,A9;
d = n0 / (n0 / e) by A10,A11,XCMPLX_1:52;
hence contradiction by A7,XCMPLX_1:52;
end; then
A12: card union rng fp = Sum Card fp by A4,INT_5:48;
for x being set holds x in union rng fp iff x in X
proof
let x be set;
thus x in union rng fp implies x in X;
assume A13: x in X; then
reconsider i=x as natural number;
i gcd n0 divides n0 by NAT_D:def 5; then
consider h be natural number such that
A14: n0 = (i gcd n0) * h by NAT_D:def 3;
A15: h <> 0 by A14;
A16: n0 / h = (i gcd n0) * (h / h) by A14,XCMPLX_1:75
.= (i gcd n0) * 1 by A15,XCMPLX_1:60;
A17: h divides n0 by A14,NAT_D:def 3;
A18: 0 < h by A14; then
A19: h in NatDivisors n0 by A17,MOEBIUS1:39;
set Y = fp.h;
0+1 < h+1 by A18,XREAL_1:8; then
A20: 1 <= h by NAT_1:13;
h <= n0 by A17,NAT_D:7; then
A21: h in dom fp by A3,A20,FINSEQ_1:3; then
A22: fp.h = {i' where i' is Element of NAT: ex h' being natural number st
i' in X & h in NatDivisors n0 & h'=h & i' gcd n0 = n0 / h'} by A3;
A23: x in Y by A22,A19,A16,A13;
Y in rng fp by A21,FUNCT_1:12;
hence x in union rng fp by A23,TARSKI:def 4;
end; then
A24: card X = Sum Card fp by A12,TARSKI:2;
card X = card n0 by FINSEQ_1:76; then
A25: n0 = Sum Card fp by A24,CARD_1:def 5;
A26: Seg n0 = dom Card fp by A3,CARD_3:def 2;
A27: NatDivisors n0 c= Seg n0 by MOEBIUS1:40;
A28: NatDivisors n0 c= dom fp by A3,MOEBIUS1:40;
A29: rng Sgm NatDivisors n0 c= dom fp
by A3,A27,FINSEQ_1:def 13; then
A30: 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;
A31: for x being set holds
x in NatDivisors n0 iff x in Seg n0 & not x in (Card fp)"{0}
proof
let x be set;
hereby
assume A32: x in NatDivisors n0;
hence x in Seg n0 by A27;
assume x in (Card fp)"{0}; then
consider y be set such that
A33: [x,y] in Card fp & y in {0} by RELAT_1:def 14;
A34: y = 0 by A33,TARSKI:def 1;
A35: x in dom Card fp & y = (Card fp).x by A33,FUNCT_1:8;
card (fp.x) = {} by A35,A34,A3,A32,A27,CARD_3:def 2; then
A36: fp.x = {};
reconsider k=x as Element of NAT by A32;
k divides n0 by A32,MOEBIUS1:39; then
consider i be natural number such that
A37: n0 = k * i by NAT_D:def 3;
A38: i divides n0 by A37,NAT_D:def 3; then
A39: n0 = k * (i gcd n0) by A37,NEWTON:62;
A40: k <> 0 by A37;
A41: n0 / k = (i gcd n0) * (k / k) by A39,XCMPLX_1:75
.= (i gcd n0) * 1 by A40,XCMPLX_1:60;
i <> 0 by A37; then
0+1 < i+1 by XREAL_1:8; then
A42: 1 <= i by NAT_1:13;
i <= n0 by A38,NAT_D:7; then
A43: i in X by A42,FINSEQ_1:3;
i in {i' where i' is Element of NAT: ex h being natural number st
i' in X & k in NatDivisors n0 & h=k & i' gcd n0 = n0 / h} by A41,A43,A32;
hence contradiction by A3,A32,A27,A36;
end;
assume A44: x in Seg n0;
assume A45: not x in (Card fp)"{0};
reconsider k=x as Element of NAT by A44;
A46: fp.k = {i' where i' is Element of NAT: ex h being natural number st
i' in X & k in NatDivisors n0 & h=k & i' gcd n0 = n0 / h} by A3,A44;
assume A47: not x in NatDivisors n0;
A48: fp.k = {}
proof
assume fp.k <> {}; then
consider x' be set such that
A49: x' in fp.k by XBOOLE_0:def 1;
consider i be Element of NAT such that
A50: x' = i & ex h being natural number st
i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h by A49,A46;
thus contradiction by A50,A47;
end;
reconsider y = 0 as Element of NAT by ORDINAL1:def 13;
x in dom Card fp & y = (Card fp).x
by A3,A44,A48,CARD_3:def 2,CARD_1:47; then
A51: [k,y] in Card fp by FUNCT_1:8;
y in {0} by TARSKI:def 1;
hence contradiction by A45,A51,RELSET_1:53;
end;
reconsider f1'=f1 as FinSequence of REAL by Th13;
reconsider f2'=Card fp as FinSequence of REAL by Th13;
f1' = f2' - {0} by A31,A26,XBOOLE_0:def 5; then
A52: Sum f1' = Sum f2' by Th12;
A53: dom Euler_phi = NAT & X c= NAT by FUNCT_2:def 1;
A54: dom((Card fp)*Sgm NatDivisors n0)
= dom Sgm NatDivisors n0 by A30,RELAT_1:46
.= dom(Euler_phi * Sgm NatDivisors n0) by A29,A53,XBOOLE_1:1,RELAT_1:46;
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;
assume A55: k in dom((Card fp)*Sgm NatDivisors n0);
set k' = (Sgm NatDivisors n0).k;
A56: ((Card fp)*Sgm NatDivisors n0).k = (Card fp).k' by A55,FUNCT_1:22;
k in dom Sgm NatDivisors n0 by A55,FUNCT_1:21; then
k' in rng Sgm NatDivisors n0 by FUNCT_1:12; then
A57: k' in NatDivisors n0 by A27,FINSEQ_1:def 13;
set Y = {l where l is Element of NAT :
k',l are_relative_prime & l >= 1 & l <= k'};
set Z = {i where i is Element of NAT: ex h being natural number st
i in X & k' in NatDivisors n0 & h=k' & i gcd n0 = n0 / h};
A58: fp.k' = Z by A3,A57,A28;
deffunc F(Nat) = $1*n0/k';
A59: 1 <= k' & k' <= n0 by A3,A57,A28,FINSEQ_1:3;
k',1 are_relative_prime by WSIERP_1:14; then
A60: 1 in Y by A59;
A61: for x being set st x in Y holds x in NAT
proof
let x be set;
assume x in Y; then
consider l be Element of NAT such that
A62: x=l & k',l are_relative_prime & l >= 1 & l <= k';
thus x in NAT by A62;
end;
reconsider Y as non empty Subset of NAT by A60,A61,TARSKI:def 3;
consider f be Function such that
A63: dom f = Y &
for d being Element of Y holds f.d = F(d) from FUNCT_1:sch 4;
for x1,x2 being set st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be set;
assume x1 in dom f; then
reconsider x1'=x1 as Element of Y by A63;
assume x2 in dom f; then
reconsider x2'=x2 as Element of Y by A63;
assume A64: f.x1 = f.x2;
A65: F(x1') = f.x1' by A63 .= F(x2') by A64,A63;
x1'*(n0/k') = x1'*n0/k' by XCMPLX_1:75
.= x2'*(n0/k') by A65,XCMPLX_1:75;
hence x1 = x2 by A59,XCMPLX_1:5;
end; then
A66: f is one-to-one by FUNCT_1:def 8;
for y being set holds y in rng f iff y in Z
proof
let y be set;
hereby
assume y in rng f; then
consider x be set such that
A67: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Element of Y by A67,A63;
A68: y = F(x) by A67,A63
.= x*(n0/k') by XCMPLX_1:75;
x in Y; then
consider l be Element of NAT such that
A69: x=l & k',l are_relative_prime & l >= 1 & l <= k';
A70: 0 < k' & k' divides n0 by A57,MOEBIUS1:39; then
consider j be natural number such that
A71: n0 = k'*j by NAT_D:def 3;
A72: n0/k' = j/(k'/k') by A71,XCMPLX_1:78
.= j/1 by A70,XCMPLX_1:60;
A73: y = x*(j/(k'/k')) by A71,A68,XCMPLX_1:78
.= x*(j/1) by A70,XCMPLX_1:60
.= x*j; then
reconsider i=y as Element of NAT;
j<>0 by A71; then
j+1 > 0+1 by XREAL_1:8; then
1 <= j by NAT_1:13; then
A74: 1*1 <= x*j by A69,XREAL_1:68;
x*j <= k'*j by A69,XREAL_1:66; then
A75: i in X by A71,A73,A74;
k' gcd l = 1 by A69,INT_2:def 4; then
i gcd n0 = n0 / k' by A72,A69,A71,A73,EULER_1:6;
hence y in Z by A57,A75;
end;
assume y in Z; then
consider i be Element of NAT such that
A76: i=y & ex h being natural number st
i in X & k' in NatDivisors n0 & h=k' & i gcd n0 = n0 / h;
consider h be natural number such that
A77: i in X & k' in NatDivisors n0 & h=k' & i gcd n0 = n0 / h by A76;
i gcd n0 divides i by INT_2:def 3; then
consider x be natural number such that
A78: i = (i gcd n0)*x by NAT_D:def 3;
A79: y = x*n0/k' by A76,A78,XCMPLX_1:75;
reconsider x as Element of NAT by ORDINAL1:def 13;
A80: k'<>0 by A77,MOEBIUS1:39;
A81: 1 <= i & i <= n0 by A77,FINSEQ_1:3;
A82: x<>0 by A76,A78,FINSEQ_1:3;
A83: k'*(i gcd n0) = n0/(k'/k') by A77,XCMPLX_1:82
.= n0/1 by A80,XCMPLX_1:60; then
A84: k',x are_relative_prime by A78,A80,A82,A77,EULER_1:7;
x+1 > 0+1 by A82,XREAL_1:8; then
A85: x >= 1 by NAT_1:13;
x <= k' by A81,A78,A83,XREAL_1:70,A80,A77; then
x in dom f by A63,A85,A84; then
reconsider x as Element of Y by A63;
y = f.x by A79,A63;
hence y in rng f by FUNCT_1:def 5,A63;
end; then
rng f = Z by TARSKI:2; then
Y,Z are_equipotent by A63,A66,WELLORD2:def 4; then
card (fp.k') = card Y by A58,CARD_1:21; then
(Card fp).k' = Euler(k') by A57,A28,CARD_3:def 2; then
A86: (Card fp).k' = Euler_phi.k' by Def7;
thus thesis by A56,A55,A54,FUNCT_1:22,A86;
end; then
(Card fp)*Sgm NatDivisors n0 = Euler_phi * Sgm NatDivisors n0
by A54,PARTFUN1:34; then
A87: Sum Func_Seq(Euler_phi,Sgm NatDivisors n0) = n0 by A25,A52,BHSP_5:def 4;
A88: dom Euler_phi = NAT by FUNCT_2:def 1;
rng Euler_phi c= REAL; then
reconsider EU' = Euler_phi as Function of NAT, REAL
by A88,FUNCT_2:4;
A89: Func_Seq(Euler_phi,Sgm NatDivisors n0)
= Euler_phi*(Sgm NatDivisors n0) by BHSP_5:def 4
.= Func_Seq(EU',Sgm NatDivisors n0) by BHSP_5:def 4;
NatDivisors n0 c= Seg n0 by MOEBIUS1:40;
hence thesis by A89,A87,Th24;
end;