:: The Perfect Number Theorem and Wilson's Theorem :: by Marco Riccardi :: :: Received March 3, 2009 :: Copyright (c) 2009-2016 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; 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; definitions TARSKI; equalities NEWTON, FINSEQ_1, FINSEQ_3, EULER_1, MOEBIUS1, CARD_1, ORDINAL1; expansions TARSKI, FINSEQ_1; theorems XBOOLE_0, XBOOLE_1, XXREAL_0, XREAL_1, XCMPLX_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, INT_1, INT_2, INT_4, INT_5, NEWTON, EULER_1, EULER_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, RVSUM_1, WSIERP_1, ORDINAL1, IDEA_1, INT_6, FIB_NUM3, POWER, PEPIN, SQUARE_1, CARD_1, CARD_2, ZFMISC_1, FINSEQ_4, JGRAPH_1, TARSKI, COMPLEX1, ABSVALUE, MOEBIUS1, CARD_3, MESFUNC3, FUNCT_2, EXTREAL1, FINSEQOP, FUNCOP_1, BAGORDER, RELSET_1, WELLORD2, PARTFUN1, BHSP_5, UPROOTS, RFINSEQ, BINOP_2, BINOP_1, FUNCT_3, RFUNCT_3, NAT_4, NAT_3, XREAL_0, ABIAN, ENUMSET1, MONOID_1, CLASSES1, PRE_POLY, XTUPLE_0, NUMBERS; schemes NAT_1, FUNCT_1, FUNCT_2, BINOP_2, FINSEQ_1; begin :: Preliminaries reserve k,n,m,l,p for Nat; reserve n0,m0 for non zero Nat; Lm1: p is prime implies p |-count (n0 gcd m0) = min(p |-count n0,p |-count m0) proof reconsider h9=n0 gcd m0 as non zero Nat by INT_2:5; assume A1: p is prime; then reconsider p9=p as Prime; h9 divides n0 by INT_2:def 2; then A2: p9 |-count h9 <= p9 |-count n0 by NAT_3:30; h9 divides m0 by INT_2:def 2; then A3: p9 |-count h9 <= p9 |-count m0 by NAT_3:30; per cases; suppose A4: p |-count n0 <= p |-count m0; set k = p9 |^ (p9|-count n0); A5: p9|^(p |-count n0) divides m0 by A4,MOEBIUS1:9; A6: p>1 by A1,INT_2:def 4; then k divides n0 by NAT_3:def 7; then k divides h9 by A5,INT_2:def 2; then p9 |-count k <= p9 |-count h9 by NAT_3:30; then p9 |-count n0 <= p9 |-count h9 by A6,NAT_3:25; then p |-count (n0 gcd m0) = p |-count n0 by A2,XXREAL_0:1; hence thesis by A4,XXREAL_0:def 9; end; suppose A7: not p |-count n0 <= p |-count m0; set k = p9 |^ (p9|-count m0); A8: p9|^(p |-count m0) divides n0 by A7,MOEBIUS1:9; A9: p>1 by A1,INT_2:def 4; then k divides m0 by NAT_3:def 7; then k divides h9 by A8,INT_2:def 2; then p9 |-count k <= p9 |-count h9 by NAT_3:30; then p9 |-count m0 <= p9 |-count h9 by A9,NAT_3:25; then p |-count (n0 gcd m0) = p |-count m0 by A3,XXREAL_0:1; hence thesis by A7,XXREAL_0:def 9; end; end; theorem Th1: 2|^(n+1) < 2|^(n+2) - 1 proof defpred P[Nat] means 2|^(\$1+1) < 2|^(\$1+2) - 1; A1: for k be Nat st P[k] holds P[k + 1] proof let k be Nat; assume P[k]; then 2|^(k+1)*2 < (2|^(k+2) - 1)*2 by XREAL_1:68; then 2|^((k+1)+1) < 2|^(k+2)*2 - 1*2 by NEWTON:6; then A2: 2|^((k+1)+1) < 2|^((k+2)+1) - 2 by NEWTON:6; -2 + 2|^((k+1)+2) < -1 + 2|^((k+1)+2) by XREAL_1:8; hence P[k + 1] by A2,XXREAL_0:2; end; 2|^1 < 2|^1*2 - 1; then 2|^1 < 2|^(1+1) - 1 by NEWTON:6; then A3: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem Th2: n0 is even implies ex k,m st m is odd & k > 0 & n0 = 2|^k * m proof assume A1: n0 is even; set k = 2 |-count n0; 2|^k divides n0 by NAT_3:def 7; then consider m be Nat such that A2: n0 = 2|^k * m by NAT_D:def 3; take k,m; A3: now reconsider m9=m as Element of NAT by ORDINAL1:def 12; assume not m is odd; then consider m99 be Nat such that A4: m9 = 2 * m99 by ABIAN:def 2; n0 = 2|^k * 2 * m99 by A2,A4 .= 2|^(k+1)*m99 by NEWTON:6; then 2|^(k+1) divides n0 by NAT_D:def 3; hence contradiction by NAT_3:def 7; end; hence m is odd; now assume k = 0; then n0 = 1*m by A2,NEWTON:4; hence contradiction by A1,A3; end; hence k > 0; thus n0 = 2|^k * m by A2; end; theorem Th3: n=2|^k & m is odd implies n,m are_coprime proof assume A1: n=2|^k; assume A2: m is odd; then reconsider h = n gcd m as non zero Nat by INT_2:5; for p being Element of NAT st p is prime holds p |-count h = p |-count 1 proof reconsider n9=n,m9=m as non zero Nat by A1,A2; let p be Element of NAT; assume A3: p is prime; A4: min(p |-count n,p |-count m) = 0 proof per cases; suppose A5: p=2; not p divides m proof assume p divides m; then consider m9 be Nat such that A6: m = p * m9 by NAT_D:def 3; thus contradiction by A2,A5,A6; end; then p |-count m = 0 by A5,NAT_3:27; hence thesis by XXREAL_0:def 9; end; suppose A7: p<>2; p<>1 by A3,INT_2:def 4; then A8: p |-count 2 = 0 by A7,INT_2:28,NAT_3:24; p |-count n = k * (p |-count 2) by A1,A3,NAT_3:32 .= k * (0 qua Nat) by A8; hence thesis by XXREAL_0:def 9; end; end; p > 1 & p |-count (n9 gcd m9) = min(p |-count n9,p |-count m9) by A3,Lm1, INT_2:def 4; hence p |-count h = p |-count 1 by A4,NAT_3:21; end; then n gcd m = 1 by NAT_4:21; hence n,m are_coprime by INT_2:def 3; end; theorem Th4: {n} is finite Subset of NAT by ORDINAL1:def 12,ZFMISC_1:31; theorem Th5: {n,m} is finite Subset of NAT proof n in NAT & m in NAT by ORDINAL1:def 12; hence {n,m} is finite Subset of NAT by ZFMISC_1:32; end; Lm2: {n,m,l} is finite Subset of NAT proof reconsider Y = {m,l} as finite Subset of NAT by Th5; reconsider X = {n} as finite Subset of NAT by Th4; {n,m,l} = X \/ Y by ENUMSET1:2; hence {n,m,l} is finite Subset of NAT; end; Lm3: {n,m,l,k} is finite Subset of NAT proof reconsider Y = {l,k} as finite Subset of NAT by Th5; reconsider X = {n,m} as finite Subset of NAT by Th5; {n,m,l,k} = X \/ Y by ENUMSET1:5; hence {n,m,l,k} is finite Subset of NAT; end; :: FinSequence reserve f for FinSequence; reserve x,X,Y for set; theorem Th6: f is one-to-one implies Del(f,n) is one-to-one proof dom f = Seg len f by FINSEQ_1:def 3; then A1: Sgm (dom f \ {n}) is one-to-one by FINSEQ_3:92,XBOOLE_1:36; assume f is one-to-one; hence Del(f,n) is one-to-one by A1; end; theorem Th7: f is one-to-one & n in dom f implies not f.n in rng Del(f,n) proof assume A1: f is one-to-one; reconsider n9=n as Element of NAT by ORDINAL1:def 12; A2: dom Del(f,n9) c= dom f by WSIERP_1:39; assume A3: n in dom f; then consider m be Nat such that A4: len f = m + 1 and A5: len Del(f,n) = m by FINSEQ_3:104; assume f.n in rng Del(f,n); then consider j be object such that A6: j in dom Del(f,n) and A7: f.n = Del(f,n).j by FUNCT_1:def 3; A8: j in Seg m by A5,A6,FINSEQ_1:def 3; reconsider j as Element of NAT by A6; per cases; suppose A9: j=n9; 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: jm; j<=m+1 by A5,FINSEQ_1:1; hence contradiction by A5,A12,A13,A14,FINSEQ_1:1,NAT_1:8; end; suppose A15: j>=n9; set j9=j-'1; j <= m+1 by A5,FINSEQ_1:1; then j-1 <= m+1-1 by XREAL_1:9; then A16: j9<=m9 by XREAL_0:def 2; j>n9 by A3,A11,A15,XXREAL_0:1; then j>=n9+1 by NAT_1:13; then A17: j-1>=n9+1-1 by XREAL_1:9; then j9>=n9 by XREAL_0:def 2; then j9>=1 by A10,XXREAL_0:2; then j9 in Seg m by A16; then A18: j9 in dom Del(f,n) by A8,FINSEQ_1:def 3; A19: n9 in dom f by A1,A6,FINSEQ_3:104; n9<=j9 by A17,XREAL_0:def 2; then Del(f,n9).j9 = f.(j9+1) by A4,A19,A16,FINSEQ_3:111; then f.j <> f.(j9+1) by A3,A6,A18,FUNCT_1:def 3; then f.j <> f.(j-1+1) by A17,XREAL_0:def 2; hence contradiction; end; end; theorem Th9: for f1 being FinSequence of NAT, f2 being FinSequence of X st rng f1 c= dom f2 holds f2*f1 is FinSequence of X proof let f1 be FinSequence of NAT; let f2 be FinSequence of X; consider n be Nat such that A1: dom f1 = Seg n by FINSEQ_1:def 2; assume rng f1 c= dom f2; then dom(f2*f1) = Seg n by A1,RELAT_1:27; then A2: f2*f1 is FinSequence by FINSEQ_1:def 2; rng(f2*f1) c= X; hence f2*f1 is FinSequence of X by A2,FINSEQ_1:def 4; end; reserve f1,f2,f3 for FinSequence of REAL; theorem Th10: X \/ Y = dom f1 & X misses Y & f2 = f1*Sgm(X) & f3 = f1*Sgm(Y) implies Sum f1 = Sum f2 + Sum f3 proof assume A1: X \/ Y = dom f1; assume A2: X misses Y; assume A3: f2 = f1*Sgm(X); assume A4: f3 = f1*Sgm(Y); per cases; suppose A5: dom f1 = {}; then Y = {} by A1; then A6: f3 = {} by A4,FINSEQ_3:43; X = {} by A1,A5; then f2 = {} by A3,FINSEQ_3:43; hence thesis by A5,A6,RELAT_1:41,RVSUM_1:72; end; suppose A7: dom f1 <> {}; A8: dom f1 = Seg len f1 by FINSEQ_1:def 3; then reconsider F = id dom f1 as FinSequence by FINSEQ_2:48; reconsider D = dom f1 as non empty set by A7; reconsider F1=f1 as FinSequence of ExtREAL by MESFUNC3:11; A9: dom F1 = dom F; Y c= dom f1 by A1,XBOOLE_1:7; then rng Sgm Y c= dom f1 by A8,FINSEQ_1:def 13; then reconsider sy = Sgm(Y) as FinSequence of D by FINSEQ_1:def 4; dom f1 \ X = Y by A1,A2,XBOOLE_1:88; then rng F \ X = Y; then A10: F"(rng F \ X) = Y by FUNCT_2:94; A11: X c= dom f1 by A1,XBOOLE_1:7; then rng Sgm X c= dom f1 by A8,FINSEQ_1:def 13; then reconsider sx = Sgm(X) as FinSequence of D by FINSEQ_1:def 4; F"X = X by A11,FUNCT_2:94; then reconsider s = Sgm(X)^Sgm(Y) as Permutation of dom F1 by A10,A9, FINSEQ_3:114; rng s c= dom f1 by FUNCT_2:def 3; then reconsider g=f1*s as FinSequence of REAL by Th9; reconsider f19 = f1 as Function of D,REAL by FINSEQ_2:26; reconsider G = g as FinSequence of ExtREAL by MESFUNC3:11; not -infty in rng F1; then Sum F1 = Sum G by EXTREAL1:11; then A12: Sum f1 = Sum G by MESFUNC3:2; g = (f19*sx)^(f19*sy) by FINSEQOP:9; then Sum g = Sum(f19*sx) + Sum(f19*sy) by RVSUM_1:75; hence Sum f1 = Sum f2 + Sum f3 by A3,A4,A12,MESFUNC3:2; end; end; theorem Th11: f2 = f1*Sgm(X) & dom f1 \ f1"{0} c= X & X c= dom f1 implies Sum f1 = Sum f2 proof assume A1: f2 = f1*Sgm(X); set Y = dom f1 \ X; assume A2: dom f1 \ f1"{0} c= X; assume A3: X c= dom f1; per cases; suppose A4: Y = {}; X \ dom f1 = {} by A3,XBOOLE_1:37; then X = dom f1 by A4,XBOOLE_1:32; then X = Seg len f1 by FINSEQ_1:def 3; then Sgm X = idseq len f1 by FINSEQ_3:48; hence thesis by A1,FINSEQ_2:54; end; suppose A5: Y <> {}; set f3 = f1*Sgm(Y); A6: Y c= dom f1 by XBOOLE_1:36; then A7: Y c= Seg len f1 by FINSEQ_1:def 3; then rng Sgm Y c= dom f1 by A6,FINSEQ_1:def 13; then reconsider f3 as FinSequence of REAL by Th9; A8: X misses Y by XBOOLE_1:79; A9: Y c= f1"{0} proof assume not Y c= f1"{0}; then consider x be object such that A10: x in Y and A11: not x in f1"{0}; x in dom f1 by A10,XBOOLE_0:def 5; then x in dom f1 \ f1"{0} by A11,XBOOLE_0:def 5; then x in X /\ Y by A2,A10,XBOOLE_0:def 4; hence contradiction by A8,XBOOLE_0:def 7; end; for y being object holds y in rng f3 iff y = 0 proof let y be object; consider x be object such that A12: x in Y by A5,XBOOLE_0:def 1; hereby assume y in rng f3; then consider x be object such that A13: x in dom f3 and A14: y = f3.x by FUNCT_1:def 3; A15: x in dom Sgm Y by A13,FUNCT_1:11; then (Sgm Y).x in rng Sgm Y by FUNCT_1:3; then (Sgm Y).x in Y by A7,FINSEQ_1:def 13; then f1.((Sgm Y).x) in {0} by A9,FUNCT_1:def 7; then f3.x in {0} by A15,FUNCT_1:13; hence y = 0 by A14,TARSKI:def 1; end; assume A16: y = 0; x in rng Sgm Y by A7,A12,FINSEQ_1:def 13; then consider x9 be object such that A17: x9 in dom Sgm Y and A18: x = (Sgm Y).x9 by FUNCT_1:def 3; f1.x in {0} by A9,A12,FUNCT_1:def 7; then f1.((Sgm Y).x9) = y by A16,A18,TARSKI:def 1; then A19: f3.x9 = y by A17,FUNCT_1:13; x in dom f1 by A9,A12,FUNCT_1:def 7; then x9 in dom f3 by A17,A18,FUNCT_1:11; hence y in rng f3 by A19,FUNCT_1:def 3; end; then dom f3 = Seg len f3 & rng f3 = {0} by FINSEQ_1:def 3,TARSKI:def 1; then f3 = (Seg len f3) --> 0 by FUNCOP_1:9; then A20: f3 = (len f3) |-> 0 by FINSEQ_2:def 2; then reconsider f3 as FinSequence of NAT; X \/ Y = dom f1 by A3,XBOOLE_1:45; then A21: Sum f1 = Sum f2 + Sum f3 by A1,Th10,XBOOLE_1:79; Sum f3 = 0 by A20,BAGORDER:4; hence Sum f1 = Sum f2 by A21; end; end; theorem Th12: f2 = f1 - {0} implies Sum f1 = Sum f2 proof A1: dom f1 \ f1"{0} c= dom f1 by XBOOLE_1:36; assume f2 = f1 - {0}; hence Sum f1 = Sum f2 by A1,Th11; end; :: like FINSEQ_3:126 theorem Th13: for f being FinSequence of NAT holds f is FinSequence of REAL proof let f be FinSequence of NAT; for n being Nat st n in dom f holds f.n in REAL by XREAL_0:def 1; hence thesis by FINSEQ_2:12; end; :: NatDivisors reserve n1,n2,m1,m2 for Nat; theorem Th14: n1 in NatDivisors n & m1 in NatDivisors m & n,m are_coprime implies n1,m1 are_coprime proof A1: n1 gcd m1 divides m1 by INT_2:def 2; assume n1 in NatDivisors n; then A2: n1 divides n by MOEBIUS1:39; n1 gcd m1 divides n1 by INT_2:def 2; then A3: n1 gcd m1 divides n by A2,INT_2:9; assume A4: m1 in NatDivisors m; then m1 divides m by MOEBIUS1:39; then A5: n1 gcd m1 divides m by A1,INT_2:9; 0 < m1 by A4,MOEBIUS1:39; then n1 gcd m1 <> 0 by INT_2:5; then n1 gcd m1 + 1 > 0 + 1 by XREAL_1:8; then A6: n1 gcd m1 >= 1 by NAT_1:13; assume A7: n,m are_coprime; assume not n1,m1 are_coprime; then A8: n1 gcd m1 <> 1 by INT_2:def 3; n gcd m > 0 by A7,INT_2:def 3; then n1 gcd m1 <= n gcd m by A3,A5,INT_2:22,27; then n gcd m <> 1 by A8,A6,XXREAL_0:1; hence contradiction by A7,INT_2:def 3; end; theorem Th15: n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_coprime & n1*m1=n2*m2 implies n1=n2 & m1 =m2 proof assume A1: n1 in NatDivisors n; then A2: n1 divides n by MOEBIUS1:39; assume A3: m1 in NatDivisors m; then A4: m1 divides m by MOEBIUS1:39; assume A5: n2 in NatDivisors n; then A6: n2 divides n by MOEBIUS1:39; assume A7: m2 in NatDivisors m; assume A8: n,m are_coprime; assume A9: n1*m1=n2*m2; A10: m2 divides m by A7,MOEBIUS1:39; A11: now reconsider m19=m1,m29=m2 as non zero Nat by A3,A7,MOEBIUS1:39; A12: n gcd m > 0 by A8,INT_2:def 3; reconsider n19=n1,n29=n2 as non zero Nat by A1,A5,MOEBIUS1:39; assume n1<>n2; then consider p be Element of NAT such that A13: p is prime and A14: p |-count n19 <> p |-count n29 by NAT_4:21; reconsider p as Prime by A13; (p |-count n19) + (p |-count m19) = p |-count (n19*m19) by NAT_3:28 .= (p |-count n29) + (p |-count m29) by A9,NAT_3:28; then p |-count m19 <> 0 or p |-count m29 <> 0 by A14; then p divides m19 or p divides m29 by MOEBIUS1:6; then A15: p divides m by A4,A10,INT_2:9; p |-count n19 <> 0 or p |-count n29 <> 0 by A14; then p divides n19 or p divides n29 by MOEBIUS1:6; then p divides n by A2,A6,INT_2:9; then p divides n gcd m by A15,INT_2:def 2; then A16: p <= n gcd m by A12,INT_2:27; p > 1 by INT_2:def 4; hence contradiction by A8,A16,INT_2:def 3; end; A17: 0 < n2 by A5,MOEBIUS1:39; assume not (n1=n2 & m1=m2); hence contradiction by A17,A9,A11,XCMPLX_1:5; end; theorem Th16: n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1*m1 in NatDivisors(n0*m0) proof reconsider b=n0*m0 as non zero Nat; assume A1: n1 in NatDivisors n0; then A2: 0 < n1; A3: n1 divides n0 by A1,MOEBIUS1:39; assume A4: m1 in NatDivisors m0; then A5: 0 < m1; then reconsider a=n1*m1 as non zero Nat by A2; A6: m1 divides m0 by A4,MOEBIUS1:39; A7: n1*m1 in NAT by ORDINAL1:def 12; for p being Element of NAT st p is prime holds p |-count a <= p |-count b proof reconsider n19=n1,m19=m1 as non zero Nat by A1,A4; let p be Element of NAT; assume p is prime; then reconsider p9=p as Prime; A8: p9 |-count(n19*m19) = p9 |-count n19 + p9 |-count m19 & p9 |-count(n0* m0) = p9 |-count n0 + p9 |-count m0 by NAT_3:28; p9 |-count n19 <= p9 |-count n0 & p9 |-count m19 <= p9 |-count m0 by A3,A6, NAT_3:30; hence p |-count a <= p |-count b by A8,XREAL_1:7; end; then ex c being Element of NAT st n0*m0=(n1*m1)*c by NAT_4:20; then n1*m1 divides n0*m0 by NAT_D:def 3; hence n1*m1 in NatDivisors(n0*m0) by A2,A5,A7; end; theorem Th17: n0,m0 are_coprime implies k gcd n0*m0 = (k gcd n0)*(k gcd m0) proof assume A1: n0,m0 are_coprime; per cases; suppose A2: k = 0; hence k gcd n0*m0 = |.n0*m0.| by WSIERP_1:8 .= |.n0.|*|.m0.| by COMPLEX1:65 .= (k gcd n0)*|.m0.| by A2,WSIERP_1:8 .= (k gcd n0)*(k gcd m0) by A2,WSIERP_1:8; end; suppose k <> 0; then reconsider k9 = k as non zero Nat; reconsider a = k gcd n0*m0 as non zero Nat by INT_2:5; reconsider b1 = k gcd n0, b2 = k gcd m0 as non zero Nat by INT_2:5; k gcd n0 <> 0 & k gcd m0 <> 0 by INT_2:5; then reconsider b = (k gcd n0)*(k gcd m0) as non zero Nat; for p being Element of NAT st p is prime holds p |-count a = p |-count b proof let p be Element of NAT; assume p is prime; then reconsider p9=p as Prime; A3: p9 |-count a = min(p9 |-count k9,p9 |-count(n0*m0)) by Lm1 .= min(p9 |-count k,p9 |-count n0 + p9 |-count m0) by NAT_3:28; n0 gcd m0 = 1 by A1,INT_2:def 3; then p9 > 1 & p9 |-count 1 = min(p9 |-count n0,p9 |-count m0) by Lm1, INT_2:def 4; then A4: min(p9 |-count n0,p9 |-count m0) = 0 by NAT_3:21; A5: p9 |-count b = p9 |-count b1 + p9 |-count b2 by NAT_3:28 .= min(p9 |-count k9,p9 |-count n0) + p9 |-count b2 by Lm1 .= min(p9 |-count k9,p9 |-count n0) + min(p9 |-count k9,p9 |-count m0) by Lm1; per cases by A4,XXREAL_0:15; suppose A6: p9 |-count n0 = 0; then min(p9 |-count k,p9 |-count n0) = p9 |-count n0 by XXREAL_0:def 9; hence p |-count a = p |-count b by A3,A5,A6; end; suppose A7: p9 |-count m0 = 0; then min(p9 |-count k,p9 |-count m0) = p9 |-count m0 by XXREAL_0:def 9; hence p |-count a = p |-count b by A3,A5,A7; end; end; hence k gcd n0*m0 = (k gcd n0)*(k gcd m0) by NAT_4:21; end; end; theorem Th18: n0,m0 are_coprime & k in NatDivisors(n0*m0) implies ex n1 ,m1 st n1 in NatDivisors n0 & m1 in NatDivisors m0 & k=n1*m1 proof assume A1: n0,m0 are_coprime; set m1 = k gcd m0; set n1 = k gcd n0; assume A2: k in NatDivisors(n0*m0); take n1,m1; n1 divides n0 & n1 > 0 by NAT_D:def 5,NEWTON:58; hence n1 in NatDivisors n0; m1 divides m0 & m1 > 0 by NAT_D:def 5,NEWTON:58; hence m1 in NatDivisors m0; k divides n0*m0 by A2,MOEBIUS1:39; hence k = k gcd n0*m0 by NEWTON:49 .= n1*m1 by A1,Th17; end; theorem Th19: p is prime implies NatDivisors(p|^n) = {p|^k where k is Element of NAT : k <= n} proof assume A1: p is prime; for x being object holds x in NatDivisors(p|^n) iff x in {p|^k where k is Element of NAT : k <= n} proof let x be object; hereby assume A2: x in NatDivisors(p|^n); then reconsider x9=x as Nat; x9 divides p|^n by A2,MOEBIUS1:39; then ex t be Element of NAT st x9 = p|^t & t<=n by A1,PEPIN:34; hence x in {p|^k where k is Element of NAT : k <= n}; end; assume x in {p|^k where k is Element of NAT : k <= n}; then A3: ex t be Element of NAT st x=p|^t & t <= n; then reconsider x9=x as Nat; x9 divides p|^n by A3,NEWTON:89; hence x in NatDivisors(p|^n) by A1,A3,MOEBIUS1:39; end; hence thesis by TARSKI:2; end; theorem Th20: 0 <> l & p > l & p > n1 & p > n2 & l*n1 mod p = l*n2 mod p & p is prime implies n1=n2 proof assume that A1: l<>0 & p > l and A2: p > n1 and A3: p > n2; assume A4: l*n1 mod p = l*n2 mod p; assume A5: p is prime; then (l*n1-l*n2) mod p = 0 by A4,INT_4:22; then A6: p divides l*(n1-n2) by A5,INT_1:62; per cases by A5,A6,INT_5:7; suppose p divides l; hence thesis by A1,NAT_D:7; end; suppose A7: p divides n1-n2; per cases; suppose A8: n1-n2 > 0; then p divides n1-'n2 & n1-'n2>0 by A7,XREAL_0:def 2; then p <= n1-'n2 by NAT_D:7; then p+n2 <= n1-'n2+n2 by XREAL_1:6; then p+n2 <= n1-n2+n2 by A8,XREAL_0:def 2; then p+n2 < p by A2,XXREAL_0:2; then p+n2-p < p-p by XREAL_1:9; then n2 < 0; hence thesis; end; suppose n1-n2 = 0; hence thesis; end; suppose n1-n2 < 0; then A9: (-(n1-n2)) > 0; then A10: n2-n1 > 0; then A11: n2-'n1>0 by XREAL_0:def 2; p divides -(n1-n2) by A7,INT_2:10; then p divides n2-'n1 by A10,XREAL_0:def 2; then p <= n2-'n1 by A11,NAT_D:7; then p+n1 <= n2-'n1+n1 by XREAL_1:6; then p+n1 <= n2-n1+n1 by A9,XREAL_0:def 2; then p+n1 < p by A3,XXREAL_0:2; then p+n1-p < p-p by XREAL_1:9; then n1 < 0; hence thesis; end; end; end; theorem p is prime implies p |-count(n0 gcd m0) = min(p |-count n0,p |-count m0) by Lm1; :: lemmas Lm4: k^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 A14: e>a-1 by Lm4; then A15: e+1>a by XREAL_1:19; then e+1-a>0 by XREAL_1:50; then A16: e+1-a+1>0 qua Nat+1 by XREAL_1:6; A17: e+1>a-1 by A15,XREAL_1:146,XXREAL_0:2; then e+1-(a-1)>0 by XREAL_1:50; then reconsider f=e+1-(a-1) as Element of NAT by INT_1:3; A18: e+1<=len fs by A4,A10,XREAL_1:6; then A19: e+1-(a-1)<=len(<*v*>^fs2) by A8,XREAL_1:9; thus (fs1^fs2).e=fs2.(e-len fs1) by A3,A5,A10,A14,FINSEQ_1:24 .=fs2.(f-1) by A3 .=(<*v*>^fs2).f by A6,A16,A19,FINSEQ_1:24 .=(fs1^(<*v*>^fs2)).(e+1) by A3,A7,A17,A18,FINSEQ_1:24 .=(Del(fs,a)).e by A1,A7,A13,WSIERP_1:def 1; end; end; hence (fs1^fs2).e=(Del(fs,a)).e; end; hence thesis by A5; end; :: Lm17 by WSIERP_1 Lm7: for fs being FinSequence holds 1<=len fs implies fs=<*fs.1*>^Del(fs,1) & fs=Del(fs,len fs)^<*fs.(len fs)*> proof let fs be FinSequence; set fs1=<*fs.1*>^Del(fs,1); set fs2=Del(fs,len fs)^<*fs.(len fs)*>; A1: len <*fs.1*>=1 by FINSEQ_1:39; assume A2: 1<=len fs; then A3: len fs in dom fs by FINSEQ_3:25; A4: 1 in dom fs by A2,FINSEQ_3:25; then A5: len fs=len <*fs.1*> + len Del(fs,1) by A1,WSIERP_1:def 1 .=len fs1 by FINSEQ_1:22; for b be Nat st 1<=b & b<=len fs holds fs.b=fs1.b proof let b be Nat; assume that A6: 1<=b and A7: b<=len fs; now per cases by A6,XXREAL_0:1; suppose A8: b=1; 1 in dom <*fs.1*> by A1,FINSEQ_3:25; hence fs1.b=<*fs.1*>.1 by A8,FINSEQ_1:def 7 .=fs.b by A8,FINSEQ_1:40; end; suppose A9: b>1; then A10: b-1>0 by XREAL_1:50; then reconsider e=b-1 as Element of NAT by INT_1:3; A11: e>=1 by A10,NAT_1:14; thus fs1.b=(Del(fs,1)).e by A1,A5,A7,A9,FINSEQ_1:24 .=fs.(e+1) by A4,A11,WSIERP_1:def 1 .=fs.b; end; end; hence thesis; end; hence fs1=fs by A5; len <*fs.(len fs)*>=1 by FINSEQ_1:39; then A12: len fs=len <*fs.(len fs)*> + len Del(fs,len fs) by A3,WSIERP_1:def 1 .=len fs2 by FINSEQ_1:22; A13: len(Del(fs,len fs))+1=len fs by A3,WSIERP_1:def 1; then A14: len Del(fs,len fs)=len fs -1; for b be Nat st 1<=b & b<=len fs holds fs.b=fs2.b proof let b be Nat; assume that A15: 1<=b and A16: b<=len fs; now per cases by A16,XXREAL_0:1; suppose A17: b=len fs; reconsider e=b-(b-1) as Element of NAT; thus fs2.b=<*fs.(len fs)*>.e by A13,A12,A17,FINSEQ_1:24,XREAL_1:146 .=fs.b by A17,FINSEQ_1:40; end; suppose A18: b^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) by RVSUM_1:95; hence thesis by A2; end; end; suppose a>0 & a=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) by RVSUM_1:95 .=(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: 10 by FINSEQ_1:1; assume A5: l<>1; A6: l<=n by A3,FINSEQ_1:1; then A7: l0 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 1 by A12,XXREAL_0:2; A16: l+1 n+1 proof assume k = n+1; then (n+1)*l mod (n+2) = 1 mod (n+2) by A9,A15,NAT_D:14 .= ((n+2)*l+1) mod (n+2) by NAT_D:21; then 0 = ((n+2)*l+1-(n+1)*l) mod (n+2) by INT_4:22 .= l+1 by A16,NAT_D:24; hence contradiction; end; k < n+1+1 by A10; then k <= n+1 by NAT_1:13; then k < n+1 by A17,XXREAL_0:1; then k <= n by NAT_1:13; hence k in Seg n by A11; l-1 < n+2-1 by A14,XREAL_1:9; then l-1 < n+2 by A8,XXREAL_0:2; then A18: l-'1 < n+2 by XREAL_0:def 2; thus A19: k<>1 proof assume k = 1; then 1*l mod (n+2) = 1 mod (n+2) by A9,A10,NAT_D:14; then 0 = (l-1) mod (n+2) by INT_4:22 .= (l-'1) mod (n+2) by A13,XREAL_0:def 2 .= l-'1 by A18,NAT_D:24 .= l-1 by A13,XREAL_0:def 2; hence contradiction by A5; end; thus k<>l proof assume A20: k=l; then l*l mod (n+2) = 1 mod (n+2) by A9,A15,NAT_D:14; then 0 = (l*l-1) mod (n+2) by INT_4:22; then A21: n+2 divides (l+1)*(l-1) by INT_1:62; per cases by A1,A21,INT_5:7; suppose n+2 divides l+1; then n+2 <= l+1 by NAT_D:7; then n+2-1 <= l+1-1 by XREAL_1:9; hence contradiction by A7; end; suppose n+2 divides l-1; then A22: n+2 divides l-'1 by A13,XREAL_0:def 2; per cases; suppose l=1; hence contradiction by A19,A20; end; suppose l<>1; then l>1 by A12,XXREAL_0:1; then l-1>1-1 by XREAL_1:9; then l-'1>0 by XREAL_0:def 2; then n+2 <= l-'1 by A22,NAT_D:7; then n+2 <= l-1 by XREAL_0:def 2; then n+2+1 <= l-1+1 by XREAL_1:6; then n+3 <= n by A6,XXREAL_0:2; then n+3-n <= n-n by XREAL_1:9; then 3 <= 0; hence contradiction; end; end; end; thus l*k mod (n+2) = 1 by A9; end; Lm10: for f being FinSequence of NAT st n+2 is prime & rng f c= Seg n & f is one-to-one & (for l st l in rng f & l<>1 holds ex k st k in rng f & k<>1 & k<>l & l*k mod (n+2) = 1) holds (Product f) mod (n+2) = 1 proof defpred P[Nat] means for f being FinSequence of NAT st len f = \$1 & n+2 is prime & rng f c= Seg n & f is one-to-one & (for l st l in rng f & l<>1 holds ex k st k in rng f & k<>1 & k<>l & l*k mod (n+2) = 1) holds (Product f) mod (n+2) = 1; let f be FinSequence of NAT; set n9 = len f; A1: for k9 being Nat st for n9 being Nat st n9 < k9 holds P[n9] holds P[k9] proof let k9 be Nat; assume A2: for n9 being Nat st n9 < k9 holds P[n9]; thus P[k9] proof let f be FinSequence of NAT; assume A3: len f = k9; assume A4: n+2 is prime; assume A5: rng f c= Seg n; assume A6: f is one-to-one; assume A7: for l st l in rng f & l<>1 holds ex k st k in rng f & k<>1 & k<> l & l*k mod (n+2) = 1; per cases; suppose A8: k9=0; A9: 0+1 < n+1+1 by XREAL_1:6; f = <*>NAT by A3,A8; then Product f = 1 by RVSUM_1:94; hence (Product f) mod (n+2) = 1 by A9,NAT_D:24; end; suppose A10: k9<>0; reconsider f9=f as FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; dom f <> {} by A3,A10,CARD_1:27,RELAT_1:41; then consider x1 be object such that A11: x1 in dom f by XBOOLE_0:def 1; reconsider x1 as Element of NAT by A11; A12: ex m be Nat st len f = m + 1 & len Del(f,x1) = m by A11,FINSEQ_3:104; A13: Product Del(f9,x1)*(f9.x1) = Product f by A11,Lm8; A14: rng Del(f,x1) c= rng f by FINSEQ_3:106; then A15: rng Del(f,x1) c= Seg n by A5; set n19 = len Del(f,x1); A16: 0 + n19 < 1 + n19 by XREAL_1:6; A17: Del(f,x1) is one-to-one by A6,Th6; per cases; suppose A18: f9.x1 = 1; for l st l in rng Del(f,x1) & l<>1 holds ex k st k in rng Del(f ,x1) & k<>1 & k<>l & l*k mod (n+2) = 1 proof let l; assume A19: l in rng Del(f,x1); assume l<>1; then consider k such that A20: k in rng f and A21: k<>1 and A22: k<>l & l*k mod (n+2) = 1 by A7,A14,A19; take k; thus k in rng Del(f,x1) by A18,A20,A21,Th8; thus k<>1 & k<>l & l*k mod (n+2) = 1 by A21,A22; end; hence (Product f) mod (n+2) = 1 by A2,A3,A4,A13,A15,A17,A12,A16,A18; end; suppose A23: f9.x1 <> 1; set f99 = Del(f,x1); A24: f99 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19; set l=f.x1; A25: l in rng f by A11,FUNCT_1:3; then consider k be Nat such that A26: k in rng f and k<>1 and A27: k<>l and A28: l*k mod (n+2) = 1 by A7,A23; k in rng f99 by A26,A27,Th8; then consider x2 be object such that A29: x2 in dom f99 and A30: k = f99.x2 by FUNCT_1:def 3; reconsider x2 as Element of NAT by A29; A31: rng Del(f99,x2) c= rng Del(f9,x1) by FINSEQ_3:106; then A32: rng Del(f99,x2) c= Seg n by A15; A33: for l st l in rng Del(f99,x2) & l<>1 holds ex k st k in rng Del (f99,x2) & k<>1 & k<>l & l*k mod (n+2) = 1 proof A34: 1 <= l by A5,A25,FINSEQ_1:1; A35: 0+n < 2+n by XREAL_1:6; l <= n by A5,A25,FINSEQ_1:1; then A36: n+2 > l by A35,XXREAL_0:2; k <= n by A5,A26,FINSEQ_1:1; then A37: n+2 > k by A35,XXREAL_0:2; let l9 be Nat; A38: 0+n < 2+n by XREAL_1:6; assume A39: l9 in rng Del(f99,x2); then A40: l9 in rng Del(f9,x1) by A31; then l9 in rng f by A14; then A41: l9 <= n by A5,FINSEQ_1:1; assume l9<>1; then consider k9 be Nat such that A42: k9 in rng f and A43: k9<>1 & k9<>l9 and A44: l9*k9 mod (n+2) = 1 by A7,A14,A40; take k9; A45: 1 <= k by A5,A26,FINSEQ_1:1; thus k9 in rng Del(f99,x2) proof assume A46: not k9 in rng Del(f99,x2); per cases; suppose A47: k9 in rng f99; A48: l9 < n+2 by A41,A38,XXREAL_0:2; k*l mod (n+2) = k*l9 mod (n+2) by A28,A30,A44,A46,A47,Th8; then l9=l by A4,A45,A37,A36,A48,Th20; hence contradiction by A6,A11,A31,A39,Th7; end; suppose A49: not k9 in rng f99; A50: l9 < n+2 by A41,A38,XXREAL_0:2; l*k mod (n+2) = l*l9 mod (n+2) by A28,A42,A44,A49,Th8; then f99.x2 in rng Del(f99,x2) by A4,A30,A39,A34,A37,A36,A50 ,Th20; hence contradiction by A6,A29,Th6,Th7; end; end; thus k9<>1 & k9<>l9 & l9*k9 mod (n+2) = 1 by A43,A44; end; set n299 = len Del(f99,x2); A51: 0 + n299 < 1 + n299 by XREAL_1:6; ex m be Nat st len Del(f9,x1) = m + 1 & len Del(f99,x2) = m by A29, FINSEQ_3:104; then A52: n299 < k9 by A3,A12,A16,A51,XXREAL_0:2; A53: Del(f99,x2) is one-to-one by A17,Th6; Product Del(f99,x2)*(f99.x2) = Product f99 by A29,Lm8,A24; then Product Del(f99,x2)*(k*l) = Product f by A13,A30; hence (Product f) mod (n+2) = (Product Del(f99,x2)*((k*l) mod (n+2))) mod (n+2) by EULER_2:7 .= 1 by A2,A4,A28,A32,A53,A33,A52; end; end; end; end; for n9 being Nat holds P[n9] from NAT_1:sch 4(A1); then P[n9]; hence thesis; end; begin :: Wilson's Theorem :: Number Theory (Andrews) p.61-66 ::\$N Wilson's Theorem theorem n is prime iff (n-'1)! + 1 mod n = 0 & n>1 proof thus n is prime implies (n-'1)!+1 mod n = 0 & n>1 proof assume A1: n is prime; per cases; suppose n<2; then n < 1+1; then n <= 1 by NAT_1:13; hence thesis by A1,INT_2:def 4; end; suppose n>=2; then A2: n-2>=2-2 by XREAL_1:9; then A3: n-2+1>=0+1 by XREAL_1:6; set l = n-'2; A4: 2+l > 1+l by XREAL_1:6; set f = Sgm(Seg l); A5: (n*1) mod n = 0 by NAT_D:13; A6: l = n-2 by A2,XREAL_0:def 2; then A7: l+1 = n-1 .= n-'1 by A3,XREAL_0:def 2; A8: for l9 being Nat st l9 in rng f & l9<>1 holds ex k9 being Nat st k9 in rng f & k9<>1 & k9<>l9 & l9*k9 mod (l+2) = 1 proof let l9 be Nat; assume l9 in rng f; then A9: l9 in Seg l by FINSEQ_1:def 13; assume l9<>1; then consider k9 be Nat such that A10: k9 in Seg l & k9<>1 & k9<>l9 & l9*k9 mod (l+2) = 1 by A1,A6,A9,Lm9; take k9; thus thesis by A10,FINSEQ_1:def 13; end; l! = Product Sgm(Seg l) & rng f c= Seg l by FINSEQ_1:def 13,FINSEQ_3:48; then A11: l! mod (l+2) = 1 by A1,A6,A8,Lm10,FINSEQ_3:92; (l+1)! mod (l+2) = (l+1)*(l!) mod (l+2) by NEWTON:15 .= ((l+1)*1) mod (l+2) by A11,EULER_2:7 .= l+1 by A4,NAT_D:24; then ((l+1)! mod (l+2))+1 mod (l+2) = 0 by A6,A5; hence thesis by A1,A6,A7,INT_2:def 4,NAT_D:22; end; end; thus (n-'1)!+1 mod n = 0 & n>1 implies n is prime proof assume that A12: (n-'1)!+1 mod n = 0 and A13: n>1; n>=1+1 by A13,NAT_1:13; then consider k be Element of NAT such that A14: k is prime and A15: k divides n by INT_2:31; consider i be Nat such that A16: n = k * i by A15,NAT_D:def 3; A17: k<>1 by A14,INT_2:def 4; (n-'1)!+1 mod n = (n-'1)!+1 mod k by A12,A13,A14,A16,PEPIN:9; then k divides (n-'1)!+1 by A12,A14,PEPIN:6; then k > n-'1 by A14,A17,NEWTON:42; then k > n-1 by XREAL_0:def 2; then k+1 > n-1+1 by XREAL_1:6; then k >= n by NAT_1:13; then k/k >= k*i/k by A16,XREAL_1:72; then 1 >= k*i/k by A14,XCMPLX_1:60; then 1 >= i*(k/k) by XCMPLX_1:74; then A18: 1 >= i*1 by A14,XCMPLX_1:60; assume A19: not n is prime; i<>0 by A13,A16; then i>=0+1 by NAT_1:13; then i = 1 by A18,XXREAL_0:1; hence contradiction by A19,A14,A16; end; end; begin :: All Primes (1 mod 4) Equal the Sum of Two Squares :: Proofs from THE BOOK (Aigner-Ziegler) p.19 ::\$N All Primes (1 mod 4) Equal the Sum of Two Squares theorem p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2 proof 0 <= sqrt(p) by SQUARE_1:def 2; then reconsider p9 = [\ sqrt(p) /] as Element of NAT by INT_1:3,54; reconsider p99 = p9 + 1 as Element of NAT; set X = Segm p99; A1: sqrt(p) * card X < card X * card X by INT_1:29,XREAL_1:68; assume A2: p is prime; then p > 1 by INT_2:def 4; then p + 1 > 1 + 1 by XREAL_1:6; then A3: p >= 2 by NAT_1:13; A4: p9^2 <> p proof assume p9^2 = p; then reconsider p99=sqrt(p) as Element of NAT by SQUARE_1:def 2; p99^2 = p by SQUARE_1:def 2; then A5: p99*p99 = p by SQUARE_1:def 1; then A6: p99 divides p by INT_1:def 3; per cases by A2,A6,INT_2:def 4; suppose p99 = 1; hence contradiction by A2,A5,INT_2:def 4; end; suppose p99 = p; then 1 = (p*p)/p by A2,A5,XCMPLX_1:60 .= p*(p/p) by XCMPLX_1:74 .= p*1 by A2,XCMPLX_1:60; hence contradiction by A2,INT_2:def 4; end; end; p9 <= sqrt(p) by INT_1:def 6; then p9^2 <= (sqrt p)^2 by SQUARE_1:15; then p9^2 <= p by SQUARE_1:def 2; then A7: p9^2 < p by A4,XXREAL_0:1; assume A8: p mod 4 = 1; then p <> 2 by NAT_D:24; then p > 2 by A3,XXREAL_0:1; then (-1) is_quadratic_residue_mod p by A2,A8,INT_5:37; then consider s be Integer such that A9: (s^2-(-1)) mod p = 0 by INT_5:def 2; 0 < sqrt(p) by A2,SQUARE_1:25; then sqrt(p) * sqrt(p) < card X * sqrt(p) by INT_1:29,XREAL_1:68; then sqrt(p) * sqrt(p) < card X * card X by A1,XXREAL_0:2; then sqrt(p*p) < card X * card X by SQUARE_1:29; then sqrt(p^2) < card X * card X by SQUARE_1:def 1; then p < card X * card X by SQUARE_1:22; then A10: p < card [: X, X :] by CARD_2:46; for s being Integer holds ex x9,x99,y9,y99 being Nat st x9 in X & x99 in X & y9 in X & y99 in X & [x9,y9]<>[x99,y99] & (x9 - s*y9) mod p = (x99 - s*y99) mod p proof set A = [: X, X :]; reconsider p9=p as Element of NAT by ORDINAL1:def 12; let s be Integer; set B = Segm p9; defpred P[object,object] means ex n1,n2,n3 being Element of NAT st \$1=[n1,n2] & \$2=n3 & (n1-s*n2) mod p = n3; A11: card B in Segm card A by A10,NAT_1:44; A12: for x being object st x in A ex y being object st y in B & P[x,y] proof let x be object; assume x in A; then consider n1,n2 be object such that A13: n1 in X & n2 in X and A14: x = [n1,n2] by ZFMISC_1:def 2; reconsider n1,n2 as Element of NAT by A13; set y = (n1-s*n2) mod p; reconsider y as Element of NAT by INT_1:3,57; take y; y < p by A2,INT_1:58; then y in Segm p by NAT_1:44; hence y in B; thus P[x,y] by A14; end; consider f be Function of A,B such that A15: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A12); B <> {} by A2; then consider x1,x2 be object such that A16: x1 in A and A17: x2 in A and A18: x1 <> x2 and A19: f.x1 = f.x2 by A11,FINSEQ_4:65; consider x9,y9 be object such that A20: x9 in X & y9 in X and A21: x1 = [x9,y9] by A16,ZFMISC_1:def 2; reconsider x9,y9 as Nat by A20; consider x99,y99 be object such that A22: x99 in X & y99 in X and A23: x2 = [x99,y99] by A17,ZFMISC_1:def 2; reconsider x99,y99 as Nat by A22; take x9,x99,y9,y99; thus x9 in X & x99 in X & y9 in X & y99 in X by A20,A22; thus [x9,y9]<>[x99,y99] by A18,A21,A23; consider n11,n12,n13 be Element of NAT such that A24: x1=[n11,n12] and A25: f.x1=n13 & (n11-s*n12) mod p = n13 by A15,A16; A26: n11 = x9 & n12 = y9 by A21,A24,XTUPLE_0:1; consider n21,n22,n23 be Element of NAT such that A27: x2=[n21,n22] and A28: f.x2=n23 & (n21-s*n22) mod p = n23 by A15,A17; n21 = x99 by A23,A27,XTUPLE_0:1; hence (x9 - s*y9) mod p = (x99 - s*y99) mod p by A19,A23,A25,A27,A28,A26, XTUPLE_0:1; end; then consider x9,x99,y9,y99 be Nat such that A29: x9 in X and A30: x99 in X and A31: y9 in X and A32: y99 in X and A33: [x9,y9]<>[x99,y99] and A34: (x9 - s*y9) mod p = (x99 - s*y99) mod p; set m9 = y9-y99; A35: 0 = (((s^2+1) mod p)*(m9^2 mod p)) mod p by A9,INT_4:12 .= ((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_4:12; then 0 = (((n9 +s*m9) mod p)*((n9 -s*m9) mod p)) mod p by INT_4:12 .= (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_4:12 .= ((n9^2 - (s*m9)^2) + ((s*m9)^2+m9^2)) mod p by NAT_D:66 .= (n9^2+m9^2) mod p; then p divides (n9^2+m9^2) by A2,INT_1:62; then consider i be Integer such that A37: (n9^2+m9^2) = p * i by INT_1:def 3; A38: p * i = |.n9.|^2+m9^2 by A37,COMPLEX1:75 .= |.n9.|^2+|.m9.|^2 by COMPLEX1:75; y9 in Segm p99 by A31; then y9 < p99 by NAT_1:44; then A39: y9 <= p9 by NAT_1:13; x99 in Segm p99 by A30; then x99 < p99 by NAT_1:44; then A40: x99 <= p9 by NAT_1:13; y99 in Segm p99 by A32; then y99 < p99 by NAT_1:44; then A41: y99 <= p9 by NAT_1:13; x9 in Segm p99 by A29; then x9 < p99 by NAT_1:44; then A42: x9 <= p9 by NAT_1:13; set m = |.m9.|; set n = |.n9.|; reconsider x9,x99,y9,y99 as Real; |.y9-y99.| <= p9 - 0 by A39,A41,JGRAPH_1:27; then m^2 <= p9^2 by SQUARE_1:15; then A43: m^2 < p by A7,XXREAL_0:2; |.x9-x99.| <= p9 - 0 by A42,A40,JGRAPH_1:27; then n^2 <= p9^2 by SQUARE_1:15; then n^2 < p by A7,XXREAL_0:2; then n^2 + m^2 < p + p by A43,XREAL_1:8; then (i*p)/p < (2*p)/p by A2,A38,XREAL_1:74; then (i*p)/p < 2*(p/p) by XCMPLX_1:74; then i*(p/p) < 2*(p/p) by XCMPLX_1:74; then i*(p/p) < 2*1 by A2,XCMPLX_1:60; then i*1 < 2 by A2,XCMPLX_1:60; then i+1 <= 2 by INT_1:7; then A44: i+1-1 <= 2-1 by XREAL_1:9; reconsider n,m as Nat by TARSKI:1; take n,m; n^2 + m^2 <> 0 proof assume A45: n^2 + m^2 = 0; then m^2 = 0; then m*m = 0 by SQUARE_1:def 1; then m = 0; then A46: y9-y99 = 0 by ABSVALUE:2; n^2 = 0 by A45; then n*n = 0 by SQUARE_1:def 1; then n = 0; then x9-x99 = 0 by ABSVALUE:2; hence contradiction by A33,A46; end; then i > 0 by A38; then i >= 0+1 by INT_1:7; then i = 1 by A44,XXREAL_0:1; hence thesis by A38; end; begin :: The Sum of Divisors Function definition let I be set; let f be Function of I, NAT; let J be finite Subset of I; redefine func f|J -> bag of J; correctness; end; registration let I be set; let f be Function of I, NAT; let J be finite Subset of I; cluster Sum(f|J) -> natural; correctness proof set b = f|J; consider f9 be FinSequence of REAL such that A1: Sum b = Sum f9 and A2: f9 = b*canFS(support b) by UPROOTS:def 3; rng f9 c= NAT by A2,ORDINAL1:def 12; then reconsider f9 as FinSequence of NAT by FINSEQ_1:def 4; Sum f9 is Element of NAT; hence thesis by A1; end; end; theorem Th24: for f being sequence of NAT, F being sequence of REAL, J being finite Subset of NAT st f = F & (ex k st J c= Seg k) holds Sum(f|J) = Sum Func_Seq(F,Sgm J) proof let f be sequence of NAT; let F be sequence of REAL; let J be finite Subset of NAT; assume A1: f = F; reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1; assume A2: ex k st J c= Seg k; reconsider f9 = f|J9 as bag of J; A3: dom f = NAT by FUNCT_2:def 1; then A4: J = dom(f|J9) by RELAT_1:62; support f9 c= J9; then consider fs be FinSequence of REAL such that A5: fs = f9*canFS(J9) and A6: Sum f9 = Sum fs by UPROOTS:14; A7: rng canFS J = J by FUNCT_2:def 3 .= dom f9 by A3,RELAT_1:62; then dom canFS J = dom fs by A5,RELAT_1:27; then A8: fs,f9 are_fiberwise_equipotent by A5,A7,CLASSES1:77; A9: Sgm J is one-to-one by A2,FINSEQ_3:92; rng Sgm J = J by A2,FINSEQ_1:def 13; then A10: f*Sgm J = f*(J|`Sgm J) .= (f|J)*Sgm J by MONOID_1:1; A11: rng Sgm J = dom(f|J) by A2,A4,FINSEQ_1:def 13; then dom Sgm J = dom((f|J)*Sgm J) by RELAT_1:27; then (f|J)*Sgm J, f|J are_fiberwise_equipotent by A11,A9,CLASSES1:77; then Func_Seq(F,Sgm J), f|J are_fiberwise_equipotent by A1,A10,BHSP_5:def 4 ; hence Sum(f|J) = Sum Func_Seq(F,Sgm J) by A6,A8,CLASSES1:76,RFINSEQ:9; end; theorem Th25: for I being non empty set, F being PartFunc of I, REAL, f being Function of I, NAT, J being finite Subset of I st f = F holds Sum(f|J) = Sum(F, J) proof let I be non empty set; let F be PartFunc of I, REAL; let f be Function of I, NAT; let J be finite Subset of I; reconsider J9 = J as finite Subset of J by ZFMISC_1:def 1; reconsider f9 = f|J9 as bag of J; A1: dom(F|J) is finite; assume f = F; then A2: f|J,FinS(F,J) are_fiberwise_equipotent by A1,RFUNCT_3:def 13; A3: dom f = I by FUNCT_2:def 1; support f9 c= J9; then consider fs be FinSequence of REAL such that A4: fs = f9*canFS(J9) and A5: Sum f9 = Sum fs by UPROOTS:14; A6: rng canFS J = J by FUNCT_2:def 3 .= dom f9 by A3,RELAT_1:62; then dom canFS J = dom fs by A4,RELAT_1:27; then fs,f9 are_fiberwise_equipotent by A4,A6,CLASSES1:77; then Sum fs = Sum FinS(F,J) by A2,CLASSES1:76,RFINSEQ:9; hence Sum(f|J) = Sum(F,J) by A5,RFUNCT_3:def 14; end; reserve I,j for set; reserve f,g for Function of I, NAT; reserve J,K for finite Subset of I; theorem Th26: J misses K implies Sum(f|(J \/ K)) = Sum(f|J) + Sum(f|K) proof assume A1: J misses K; per cases; suppose A2: I is empty; set b = EmptyBag {}; A3: Sum b = 0 by UPROOTS:11; J = {} & f|J = {} by A2; hence Sum(f|(J \/ K)) = Sum(f|J) + Sum(f|K) by A3; end; suppose I is non empty; then reconsider I9 = I as non empty set; [:I9,NAT:] c= [:I9,REAL:] by ZFMISC_1:95,NUMBERS:19; then reconsider F = f as PartFunc of I9, REAL by XBOOLE_1:1; A4: dom(F|(J \/ K)) is finite; thus Sum(f|(J \/ K)) = Sum(F,J \/ K) by Th25 .= Sum(F,J) + Sum(F,K) by A1,A4,RFUNCT_3:83 .= Sum(f|J) + Sum(F,K) by Th25 .= Sum(f|J) + Sum(f|K) by Th25; end; end; theorem Th27: for j being object holds J = {j} implies Sum(f|J) = f.j proof let j be object; consider f9 be FinSequence of REAL such that A1: Sum(f|J) = Sum f9 and A2: f9 = (f|J)*canFS(support(f|J)) by UPROOTS:def 3; assume A3: J = {j}; then A4: j in J by TARSKI:def 1; then j in I; then j in dom f by FUNCT_2:def 1; then J c= dom f by A3,ZFMISC_1:31; then A5: dom(f|J) = J by RELAT_1:62; per cases by A3,ZFMISC_1:33; suppose A6: support(f|J) = {}; now assume f.j <> 0; then (f|J).j <> 0 by A4,FUNCT_1:49; hence contradiction by A6,PRE_POLY:def 7; end; hence Sum(f|J) = f.j by A1,A2,A6,RVSUM_1:72; end; suppose support(f|J) = J; then canFS(support(f|J)) = <*j*> by A3,FINSEQ_1:94; then f9 = <*(f|J).j*> by A4,A5,A2,FINSEQ_2:34; then f9 = <* f.j *> by A4,FUNCT_1:49; hence Sum(f|J) = f.j by A1,RVSUM_1:73; end; end; Lm11: for j being object holds J = {j} implies Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K) proof let j be object; defpred P[Nat] means for I being set,j being object, f,g being Function of I, NAT, J,K being finite Subset of I st J = {j} & \$1 = card K holds Sum((multnat*[:f,g:])| [:J,K:]) = f.j * Sum(g|K); A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k] proof let k be Nat; assume A2: for n being Nat st n < k holds P[n]; thus P[k] proof k = 0 or k + 1 > 0 + 1 by XREAL_1:8; then A3: k = 0 or k >= 1 by NAT_1:13; let I be set,j be object; let f,g be Function of I, NAT; let J,K be finite Subset of I; assume A4: J = {j}; assume A5: k = card K; per cases by A3,XXREAL_0:1; suppose A6: k = 0; set b = EmptyBag {}; A7: Sum b = 0 by UPROOTS:11; A8: K = {} by A5,A6; then g|K = {} & [:J,K:] = {}; hence Sum((multnat*[:f,g:])|[:J,K:])=f.j*Sum(g|K) by A8,A7; end; suppose A9: k = 1; set x = the set; card {x} = card K by A5,A9,CARD_1:30; then consider k9 be object such that A10: K = {k9} by CARD_1:29; set b = (multnat*[:f,g:])|[:J,K:]; consider f9 be FinSequence of REAL such that A11: Sum b = Sum f9 and A12: f9 = b*canFS(support b) by UPROOTS:def 3; A13: [:J,K:] = {[j,k9]} by A4,A10,ZFMISC_1:29; then A14: [j,k9] in [:J,K:] by TARSKI:def 1; then [j,k9] in [:I,I:]; then A15: [j,k9] in dom(multnat*[:f,g:]) by FUNCT_2:def 1; then [:J,K:] c= dom(multnat*[:f,g:]) by A13,ZFMISC_1:31; then A16: dom b = [:J,K:] by RELAT_1:62; Sum b = f.j * g.k9 proof reconsider I9 = I as non empty set by A4; reconsider j99=j,k99=k9 as Element of I9 by A4,A10,ZFMISC_1:31; set n1=f.j,n2=g.k9; A17: f.j * g.k9 = multnat.(n1,n2) by BINOP_2:def 24 .= multnat.[f.j99,g.k99] by BINOP_1:def 1 .= multnat.([:f,g:].(j99,k99)) by FUNCT_3:75 .= multnat.([:f,g:].[j,k9]) by BINOP_1:def 1 .= (multnat*[:f,g:]).[j,k9] by A15,FUNCT_1:12 .= b.[j,k9] by A14,FUNCT_1:49; per cases by A13,ZFMISC_1:33; suppose A18: support b = {}; then f.j * g.k9 = 0 by A17,PRE_POLY:def 7; hence Sum b = f.j * g.k9 by A11,A12,A18,RVSUM_1:72; end; suppose support b = {[j,k9]}; then canFS(support b) = <* [j,k9] *> by FINSEQ_1:94; then f9 = <* b.[j,k9] *> by A12,A14,A16,FINSEQ_2:34; hence Sum b = f.j * g.k9 by A11,A17,RVSUM_1:73; end; end; hence Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K) by A10,Th27; end; suppose A19: k > 1; then K <> {} by A5; then consider k9 be object such that A20: k9 in K by XBOOLE_0:def 1; set K0 = {k9}; set K1 = K \ K0; reconsider K0 as finite Subset of I by A20,ZFMISC_1:31; card K0 < k by A19,CARD_1:30; then A21: -1+k < 0+k & Sum((multnat*[:f,g:])|[:J,K0:]) = f.j * Sum(g|K0) by A2,A4 ,XREAL_1:8; K1 misses K0 by XBOOLE_1:79; then A22: [:J,K1:] misses [:J,K0:] by ZFMISC_1:104; k9 in K0 by TARSKI:def 1; then not k9 in K1 by XBOOLE_0:def 5; then A23: card (K1 \/ K0) = card K1 + 1 by CARD_2:41; A24: K1 \/ K0 = K \/ {k9} by XBOOLE_1:39 .= K by A20,ZFMISC_1:40; then [:J,K:] = [:J,K1:] \/ [:J,K0:] by ZFMISC_1:97; hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum((multnat*[:f,g:])|[:J,K1:]) + Sum((multnat*[:f,g:])|[:J,K0:]) by A22,Th26 .= f.j * Sum(g|K1) + f.j * Sum(g|K0) by A2,A4,A5,A23,A24,A21 .= f.j * (Sum(g|K1) + Sum(g|K0)) .= f.j * Sum(g|K) by A24,Th26,XBOOLE_1:79; end; end; end; for k being Nat holds P[k] from NAT_1:sch 4(A1); then P[card K]; hence thesis; end; theorem Th28: Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K) proof defpred P[Nat] means for I being set, f,g being Function of I, NAT, J,K being finite Subset of I st \$1 = card J holds Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K); A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k] proof let k be Nat; assume A2: for n being Nat st n < k holds P[n]; thus P[k] proof k = 0 or k + 1 > 0 + 1 by XREAL_1:8; then A3: k = 0 or k >= 1 by NAT_1:13; let I be set; let f,g be Function of I, NAT; let J,K be finite Subset of I; assume A4: k = card J; per cases by A3,XXREAL_0:1; suppose k = 0; then A5: J = {} by A4; then A6: [:J,K:] = {}; A7: EmptyBag {} = {} --> 0 .= {}; then Sum(f|J) = 0 by A5,RELAT_1:81,UPROOTS:11; hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K) by A6,A7, RELAT_1:81,UPROOTS:11; end; suppose A8: k = 1; set x = the set; card {x} = card J by A4,A8,CARD_1:30; then consider j be object such that A9: J = {j} by CARD_1:29; Sum((multnat*[:f,g:])|[:J,K:]) = f.j * Sum(g|K) by A9,Lm11; hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K) by A9,Th27; end; suppose A10: k > 1; then J <> {} by A4; then consider j be object such that A11: j in J by XBOOLE_0:def 1; set J0 = {j}; set J1 = J \ J0; reconsider J0 as finite Subset of I by A11,ZFMISC_1:31; A12: J1 \/ J0 = J \/ {j} by XBOOLE_1:39 .= J by A11,ZFMISC_1:40; then A13: Sum(f|J) = Sum(f|J1) + Sum(f|J0) by Th26,XBOOLE_1:79; card J0 < k by A10,CARD_1:30; then A14: -1+k < 0+k & Sum((multnat*[:f,g:])|[:J0,K:]) = Sum(f|J0) * Sum(g| K) by A2,XREAL_1:8; J1 misses J0 by XBOOLE_1:79; then A15: [:J1,K:] misses [:J0,K:] by ZFMISC_1:104; j in J0 by TARSKI:def 1; then not j in J1 by XBOOLE_0:def 5; then A16: card (J1 \/ J0) = card J1 + 1 by CARD_2:41; [:J,K:] = [:J1,K:] \/ [:J0,K:] by A12,ZFMISC_1:97; hence Sum((multnat*[:f,g:])|[:J,K:]) = Sum((multnat*[:f,g:])|[:J1,K:]) + Sum((multnat*[:f,g:])|[:J0,K:]) by A15,Th26 .= Sum(f|J1) * Sum(g|K) + Sum(f|J0) * Sum(g|K) by A2,A4,A16,A12,A14 .= Sum(f|J) * Sum(g|K) by A13; end; end; end; for k being Nat holds P[k] from NAT_1:sch 4(A1); then P[card J]; hence thesis; end; definition let k be natural Number; func EXP(k) -> sequence of NAT means :Def1: for n being Nat holds it.n = n|^k; existence proof reconsider k9=k as Element of NAT by ORDINAL1:def 12; deffunc F(Element of NAT) = \$1|^k9; consider f be sequence of NAT such that A1: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4; take f; for n being Nat holds f.n = n|^k proof let n be Nat; reconsider n9=n as Element of NAT by ORDINAL1:def 12; f.n9 = F(n9) by A1; hence f.n = n|^k; end; hence thesis; end; uniqueness proof let f1, f2 be sequence of NAT; assume A2: for n being Nat holds f1.n = n|^k; assume A3: for n being Nat holds f2.n = n|^k; for x being object st x in NAT holds f1.x = f2.x proof let x be object; assume x in NAT; then reconsider n=x as Nat; f1.n = n|^k by A2 .= f2.n by A3; hence f1.x = f2.x; end; hence f1 = f2 by FUNCT_2:12; end; end; definition let k,n be natural Number; func sigma(k,n) -> Element of NAT means :Def2: for m being non zero Nat st n = m holds it = Sum((EXP k)|NatDivisors m) if n<>0 otherwise it = 0; correctness proof A1: for n1, n2 being Element of NAT holds (not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2) & (n <> 0 & (for m being non zero Nat st n = m holds n1 = Sum((EXP k)|NatDivisors m)) & (for m being non zero Nat st n = m holds n2 = Sum((EXP k)|NatDivisors m)) implies n1 = n2) proof let n1, n2 be Element of NAT; thus not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2; assume n <> 0; then reconsider m=n as non zero Nat by TARSKI:1; assume for m being non zero Nat st n = m holds n1 = Sum((EXP k)|NatDivisors m); then n1 = Sum((EXP k)|NatDivisors m); hence thesis; end; n <> 0 implies ex n1 being Element of NAT st for m being non zero Nat st n = m holds n1 = Sum((EXP k)|NatDivisors m) proof assume n <> 0; then reconsider n9=n as non zero Nat by TARSKI:1; reconsider n1 = Sum((EXP k)|NatDivisors n9) as Element of NAT by ORDINAL1:def 12; take n1; thus thesis; end; hence thesis by A1; end; end; definition let k be natural Number; func Sigma(k) -> sequence of NAT means :Def3: for n being Nat holds it.n = sigma(k,n); existence proof deffunc F(Element of NAT) = sigma(k,\$1); consider f be sequence of NAT such that A1: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4; take f; let n be Nat; reconsider n9=n as Element of NAT by ORDINAL1:def 12; thus f.n = f.n9 .= sigma(k,n) by A1; end; uniqueness proof let f1,f2 be sequence of NAT; assume A2: for n being Nat holds f1.n = sigma(k,n); assume A3: for n being Nat holds f2.n = sigma(k,n); for x being object st x in NAT holds f1.x = f2.x proof let x be object; assume x in NAT; then reconsider n=x as Nat; thus f1.x = sigma(k,n) by A2 .= f2.x by A3; end; hence f1 = f2 by FUNCT_2:12; end; end; definition let n be natural Number; func sigma n -> Element of NAT equals sigma(1,n); correctness; end; theorem Th29: sigma(k,1) = 1 proof set b = (EXP k)|NatDivisors 1; consider f be FinSequence of REAL such that A1: Sum b = Sum f and A2: f = b * (canFS (support b)) by UPROOTS:def 3; 1 in NAT; then A3: 1 in dom EXP k by FUNCT_2:def 1; 1 in NatDivisors 1; then A4: 1 in dom b by A3,RELAT_1:57; then A5: b.1 = (EXP k).1 by FUNCT_1:47 .= 1|^k by Def1 .= 1; then for x being object holds x in support b iff x = 1 by MOEBIUS1:41,TARSKI:def 1,PRE_POLY:def 7; then support b = {1} by TARSKI:def 1; then f = b * <*1*> by A2,FINSEQ_1:94 .= <*b.1*> by A4,FINSEQ_2:34; then Sum b = 1 by A5,A1,RVSUM_1:73; hence sigma(k,1) = 1 by Def2; end; theorem Th30: p is prime implies sigma(p|^n) = (p|^(n+1) - 1)/(p - 1) proof defpred P[Nat] means for p being Nat st p is prime holds sigma(p |^\$1) = (p|^(\$1+1) - 1)/(p - 1); A1: for k be Nat st P[k] holds P[k + 1] proof let k be Nat; assume A2: P[k]; thus P[k + 1] proof let p be Nat; reconsider k9=k+1,p9=p as Element of NAT by ORDINAL1:def 12; assume A3: p is prime; then reconsider J = NatDivisors(p|^k) as finite Subset of NAT; reconsider m9 = p|^k as non zero Nat by A3; A4: Sum((EXP 1)|J) = sigma(1,m9) by Def2 .= sigma(p|^k) .= (p|^(k+1) - 1)/(p - 1) by A2,A3; p9|^k9 in NAT; then reconsider K = {p|^(k+1)} as finite Subset of NAT by ZFMISC_1:31; A5: p > 1 by A3,INT_2:def 4; then A6: p-1 > 1-1 by XREAL_1:14; now let x be object; assume A7: x in J /\ K; then x in J by XBOOLE_0:def 4; then x in {p|^t where t is Element of NAT : t <= k} by A3,Th19; then consider t be Element of NAT such that A8: x = p|^t and A9: t <= k; x in K by A7,XBOOLE_0:def 4; then p|^(k+1) = p|^t by A8,TARSKI:def 1; then p |-count p|^(k+1) = t by A5,NAT_3:25; then k+1 = t by A5,NAT_3:25; then k+1-k <= k-k by A9,XREAL_1:9; then 1 <= 0; hence contradiction; end; then J /\ K = {} by XBOOLE_0:def 1; then A10: J misses K by XBOOLE_0:def 7; reconsider m = p|^(k+1) as non zero Nat by A3; A11: (EXP 1).(p|^(k+1)) = (p|^(k+1))|^1 by Def1 .= p|^((k+1)*1) .= p|^(k+1); for x being object holds x in NatDivisors(p|^(k+1)) iff x in NatDivisors(p|^k) \/ {p|^(k+1)} proof let x be object; hereby assume x in NatDivisors(p|^(k+1)); then x in {p|^t where t is Element of NAT : t <= k+1} by A3,Th19; then consider t be Element of NAT such that A12: x = p|^t and A13: t <= (k+1); per cases; suppose t <= k; then x in {p|^t9 where t9 is Element of NAT : t9 <= k} by A12; then x in NatDivisors(p|^k) by A3,Th19; hence x in NatDivisors(p|^k) \/ {p|^(k+1)} by XBOOLE_0:def 3; end; suppose t > k; then t >= k+1 by NAT_1:13; then t = k+1 by A13,XXREAL_0:1; then x in {p|^(k+1)} by A12,TARSKI:def 1; hence x in NatDivisors(p|^k) \/ {p|^(k+1)} by XBOOLE_0:def 3; end; end; assume A14: x in NatDivisors(p|^k) \/ {p|^(k+1)}; per cases by A14,XBOOLE_0:def 3; suppose x in NatDivisors(p|^k); then x in {p|^t where t is Element of NAT : t <= k} by A3,Th19; then consider t be Element of NAT such that A15: x = p|^t and A16: t <= k; 0+k <= 1+k by XREAL_1:7; then t <= k+1 by A16,XXREAL_0:2; then x in {p|^t9 where t9 is Element of NAT : t9 <= k+1} by A15; hence x in NatDivisors(p|^(k+1)) by A3,Th19; end; suppose x in {p|^(k+1)}; then x = p|^k9 by TARSKI:def 1; then x in {p|^t where t is Element of NAT : t <= k+1}; hence x in NatDivisors(p|^(k+1)) by A3,Th19; end; end; then NatDivisors(p|^(k+1)) = NatDivisors(p|^k) \/ {p|^(k+1)} by TARSKI:2; then sigma(1,m) = Sum((EXP 1)|(J \/ K)) by Def2 .= Sum((EXP 1)|J) + Sum((EXP 1)|K) by A10,Th26 .= Sum((EXP 1)|J) + (EXP 1).(p|^(k+1)) by Th27; hence sigma(p|^(k+1)) = (p|^(k+1) - 1)/(p - 1) + p|^(k+1)*(p - 1)/(p - 1) by A6,A11,A4,XCMPLX_1:89 .= ((p|^(k+1) - 1) + p|^(k+1)*(p - 1))/(p - 1) by XCMPLX_1:62 .= (p|^(k+1)*p - 1)/(p - 1) .= (p|^((k+1)+1) - 1)/(p - 1) by NEWTON:6; end; end; A17: P[0] proof let p be Nat; assume p is prime; then p > 1 by INT_2:def 4; then A18: p-1 > 1-1 by XREAL_1:14; thus sigma(p|^0) = sigma(1) by NEWTON:4 .= 1 by Th29 .= (p - 1)/(p - 1) by A18,XCMPLX_1:60 .= (p|^(0+1) - 1)/(p - 1); end; for k being Nat holds P[k] from NAT_1:sch 2(A17,A1); hence thesis; end; theorem Th31: m divides n0 & n0<>m & m<>1 implies 1+m+n0 <= sigma n0 proof assume A1: m divides n0; assume A2: n0<>m; assume A3: m<>1; per cases; suppose n0 = 1; hence thesis by A1,A2,WSIERP_1:15; end; suppose A4: n0 <> 1; reconsider X2 = {m,n0} as finite Subset of NAT by Th5; set X1 = {1}; now let x be object; assume A5: x in X1 /\ X2; then x in X1 by XBOOLE_0:def 4; then A6: x = 1 by TARSKI:def 1; x in X2 by A5,XBOOLE_0:def 4; hence contradiction by A3,A4,A6,TARSKI:def 2; end; then X1 /\ X2 = {} by XBOOLE_0:def 1; then A7: X1 misses X2 by XBOOLE_0:def 7; reconsider X4 = {n0} as finite Subset of NAT by Th4; reconsider X3 = {m} as finite Subset of NAT by Th4; reconsider X = {1,m,n0} as finite Subset of NAT by Lm2; set Y = NatDivisors(n0) \ X; A8: 0 + Sum((EXP 1)|X) <= Sum((EXP 1)|Y) + Sum((EXP 1)|X) by XREAL_1:7; for x being object st x in X holds x in NatDivisors n0 proof let x be object; assume A9: x in X; then reconsider x9=x as Element of NAT; x = 1 or x = m or x = n0 by A9,ENUMSET1:def 1; then x9 <> 0 & x9 divides n0 by A1,INT_2:3,NAT_D:6; hence x in NatDivisors n0; end; then X c= NatDivisors n0; then NatDivisors n0 = X \/ Y by XBOOLE_1:45; then A10: sigma n0 = Sum((EXP 1)|(X \/ Y)) by Def2 .= Sum((EXP 1)|X) + Sum((EXP 1)|Y) by Th26,XBOOLE_1:79; now let x be object; assume A11: x in X3 /\ X4; then x in X3 by XBOOLE_0:def 4; then A12: x = m by TARSKI:def 1; x in X4 by A11,XBOOLE_0:def 4; hence contradiction by A2,A12,TARSKI:def 1; end; then X3 /\ X4 = {} by XBOOLE_0:def 1; then A13: X2 = X3 \/ X4 & X3 misses X4 by ENUMSET1:1,XBOOLE_0:def 7; X = X1 \/ X2 by ENUMSET1:2; then Sum((EXP 1)|X) = Sum((EXP 1)|X1) + Sum((EXP 1)|X2) by A7,Th26 .= (EXP 1).1 + Sum((EXP 1)|X2) by Th27 .= (EXP 1).1 + (Sum((EXP 1)|X3) + Sum((EXP 1)|X4)) by A13,Th26 .= (EXP 1).1 + ((EXP 1).m + Sum((EXP 1)|X4)) by Th27 .= ((EXP 1).1 + (EXP 1).m) + Sum((EXP 1)|X4) .= (EXP 1).1 + (EXP 1).m + (EXP 1).n0 by Th27 .= 1|^1 + (EXP 1).m + (EXP 1).n0 by Def1 .= 1|^1 + m|^1 + (EXP 1).n0 by Def1 .= 1|^1 + m|^1 + n0|^1 by Def1 .= 1 + m|^1 + n0|^1 .= 1 + m + n0|^1 .= 1 + m + n0; hence 1+m+n0 <= sigma n0 by A10,A8; end; end; theorem Th32: m divides n0 & k divides n0 & n0<>m & n0<>k & m<>1 & k<>1 & m<>k implies 1+m+k+n0 <= sigma n0 proof assume that A1: m divides n0 and A2: k divides n0 and A3: n0<>m and A4: n0<>k and A5: m<>1 and A6: k<>1 and A7: m<>k; per cases; suppose n0 = 1; hence thesis by A1,A3,WSIERP_1:15; end; suppose A8: n0 <> 1; reconsider X2 = {m,k,n0} as finite Subset of NAT by Lm2; set X1 = {1}; now let x be object; assume A9: x in X1 /\ X2; then x in X1 by XBOOLE_0:def 4; then A10: x = 1 by TARSKI:def 1; x in X2 by A9,XBOOLE_0:def 4; hence contradiction by A5,A6,A8,A10,ENUMSET1:def 1; end; then X1 /\ X2 = {} by XBOOLE_0:def 1; then A11: X1 misses X2 by XBOOLE_0:def 7; reconsider X5 = {m} as finite Subset of NAT by Th4; reconsider X4 = {n0} as finite Subset of NAT by Th4; reconsider X6 = {k} as finite Subset of NAT by Th4; reconsider X3 = {m,k} as finite Subset of NAT by Th5; reconsider X = {1,m,k,n0} as finite Subset of NAT by Lm3; set Y = NatDivisors(n0) \ X; A12: 0 + Sum((EXP 1)|X) <= Sum((EXP 1)|Y) + Sum((EXP 1)|X) by XREAL_1:7; now let x be object; assume A13: x in X5 /\ X6; then x in X5 by XBOOLE_0:def 4; then A14: x = m by TARSKI:def 1; x in X6 by A13,XBOOLE_0:def 4; hence contradiction by A7,A14,TARSKI:def 1; end; then X5 /\ X6 = {} by XBOOLE_0:def 1; then A15: X3 = X5 \/ X6 & X5 misses X6 by ENUMSET1:1,XBOOLE_0:def 7; for x being object st x in X holds x in NatDivisors n0 proof let x be object; assume A16: x in X; then reconsider x9=x as Element of NAT; x = 1 or x = m or x = k or x = n0 by A16,ENUMSET1:def 2; then x9 <> 0 & x9 divides n0 by A1,A2,INT_2:3,NAT_D:6; hence x in NatDivisors n0; end; then X c= NatDivisors n0; then NatDivisors n0 = X \/ Y by XBOOLE_1:45; then A17: sigma n0 = Sum((EXP 1)|(X \/ Y)) by Def2 .= Sum((EXP 1)|X) + Sum((EXP 1)|Y) by Th26,XBOOLE_1:79; now let x be object; assume A18: x in X3 /\ X4; then x in X4 by XBOOLE_0:def 4; then A19: x = n0 by TARSKI:def 1; x in X3 by A18,XBOOLE_0:def 4; hence contradiction by A3,A4,A19,TARSKI:def 2; end; then X3 /\ X4 = {} by XBOOLE_0:def 1; then A20: X2 = X3 \/ X4 & X3 misses X4 by ENUMSET1:3,XBOOLE_0:def 7; X = X1 \/ X2 by ENUMSET1:4; then Sum((EXP 1)|X) = Sum((EXP 1)|X1) + Sum((EXP 1)|X2) by A11,Th26 .= (EXP 1).1 + Sum((EXP 1)|X2) by Th27 .= (EXP 1).1 + (Sum((EXP 1)|X3) + Sum((EXP 1)|X4)) by A20,Th26 .= (EXP 1).1 + (Sum((EXP 1)|X5) + Sum((EXP 1)|X6) + Sum((EXP 1)|X4)) by A15,Th26 .= (EXP 1).1 + ((EXP 1).m + Sum((EXP 1)|X6) + Sum((EXP 1)|X4)) by Th27 .= ((EXP 1).1 + (EXP 1).m) + (Sum((EXP 1)|X6) + Sum((EXP 1)|X4)) .= ((EXP 1).1 + (EXP 1).m) + ((EXP 1).k + Sum((EXP 1)|X4)) by Th27 .= ((EXP 1).1 + (EXP 1).m + (EXP 1).k) + Sum((EXP 1)|X4) .= (EXP 1).1 + (EXP 1).m + (EXP 1).k + (EXP 1).n0 by Th27 .= 1|^1 + (EXP 1).m + (EXP 1).k + (EXP 1).n0 by Def1 .= 1|^1 + m|^1 + (EXP 1).k + (EXP 1).n0 by Def1 .= 1|^1 + m|^1 + k|^1 + (EXP 1).n0 by Def1 .= 1|^1 + m|^1 + k|^1 + n0|^1 by Def1 .= 1 + m|^1 + k|^1 + n0|^1 .= 1 + m + k|^1 + n0|^1 .= 1 + m + k + n0|^1 .= 1 + m + k + n0; hence 1+m+k+n0 <= sigma n0 by A17,A12; end; end; theorem Th33: sigma n0 = n0 + m & m divides n0 & n0<>m implies m = 1 & n0 is prime proof assume A1: sigma n0 = n0 + m; assume A2: m divides n0; assume A3: n0 <> m; per cases; suppose n0 = 1; then 1 = 1 + m by A1,Th29; hence thesis by A2,INT_2:3; end; suppose A4: n0 <> 1; consider k be Nat such that A5: n0 = m * k by A2,NAT_D:def 3; A6: k <> m proof assume k = m; then m <> 1 by A4,A5; then 1 + m + n0 <= sigma n0 by A2,A3,Th31; then 1 + m + n0 - (m + n0) <= n0 + m - (m + n0) by A1,XREAL_1:9; hence contradiction; end; k = n0 proof A7: k divides n0 & k <> 1 by A3,A5,NAT_D:def 3; assume A8: k <> n0; then m<>1 by A5; then 1 + m + k + n0 <= sigma n0 by A2,A3,A6,A8,A7,Th32; then 1 + m + k + n0 - (m + n0) <= n0 + m - (m + n0) by A1,XREAL_1:9; then 1 + k <= 0; hence contradiction; end; then n0/n0 = m by A5,XCMPLX_1:89; hence A9: m = 1 by XCMPLX_1:60; A10: for k being Nat holds not k divides n0 or k = 1 or k = n0 proof let k be Nat; assume that A11: k divides n0 and A12: k <> 1; assume k <> n0; then 1 + k + n0 <= n0 + 1 by A1,A9,A11,A12,Th31; then 1 + k + n0 - (1 + n0) <= n0 + 1 - (1 + n0) by XREAL_1:9; then k = 0; hence contradiction by A11,INT_2:3; end; n0 > 1 by A4,NAT_1:25; hence n0 is prime by A10,INT_2:def 4; end; end; definition let f be sequence of NAT; attr f is multiplicative means for n0,m0 being non zero Nat st n0,m0 are_coprime holds f.(n0*m0) = f.n0 * f.m0; end; theorem Th34: for f,F being sequence of NAT st f is multiplicative & (for n0 holds F.n0 = Sum(f|NatDivisors n0)) holds F is multiplicative proof let f,F be sequence of NAT; assume A1: f is multiplicative; assume A2: for n0 holds F.n0 = Sum(f|NatDivisors n0); for n,m being non zero Nat st n,m are_coprime holds F. (n*m) = F.n * F.m proof let n,m be non zero Nat; set b1 = f|NatDivisors(n*m); set b2 = (multnat * [:f,f:])|[:NatDivisors n, NatDivisors m:]; consider f1 be FinSequence of REAL such that A3: Sum b1 = Sum f1 and A4: f1 = b1 * (canFS (support b1)) by UPROOTS:def 3; set h9 = multnat|[:NatDivisors n, NatDivisors m:]; set g2 = canFS (support b2); set g1 = canFS (support b1); consider f2 be FinSequence of REAL such that A5: Sum b2 = Sum f2 and A6: f2 = b2 * (canFS (support b2)) by UPROOTS:def 3; dom multnat = [:NAT, NAT:] by FUNCT_2:def 1; then A7: dom h9 = [:NatDivisors n, NatDivisors m:] by RELAT_1:62; assume A8: n,m are_coprime; for x1,x2 being object st x1 in dom h9 & x2 in dom h9 & h9.x1 = h9.x2 holds x1 = x2 proof let x1,x2 be object; assume A9: x1 in dom h9; then consider n1, m1 be object such that A10: n1 in NatDivisors n & m1 in NatDivisors m and A11: x1 = [n1,m1] by ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by A10; A12: h9.x1 = multnat.x1 by A9,FUNCT_1:47 .= multnat.(n1,m1) by A11,BINOP_1:def 1 .= n1*m1 by BINOP_2:def 24; assume A13: x2 in dom h9; then consider n2, m2 be object such that A14: n2 in NatDivisors n and A15: m2 in NatDivisors m and A16: x2 = [n2,m2] by ZFMISC_1:def 2; reconsider n2,m2 as Element of NAT by A14,A15; assume A17: h9.x1 = h9.x2; A18: h9.x2 = multnat.x2 by A13,FUNCT_1:47 .= multnat.(n2,m2) by A16,BINOP_1:def 1 .= n2*m2 by BINOP_2:def 24; then n1=n2 by A8,A10,A14,A15,A17,A12,Th15; hence x1 = x2 by A8,A10,A11,A15,A16,A17,A12,A18,Th15; end; then reconsider h9 as one-to-one Function by FUNCT_1:def 4; set h = g1" * h9 * g2; A19: support b2 c= dom b2 by PRE_POLY:37; A20: dom [:f,f:] = [:NAT, NAT:] by FUNCT_2:def 1; for x being object st x in support b2 holds x in dom(g1" * h9) proof let x be object; A21: rng g1 = support b1 by FUNCT_2:def 3; assume A22: x in support b2; then A23: b2.x <> 0 by PRE_POLY:def 7; A24: x in [:NatDivisors n, NatDivisors m:] by A22; consider n1, m1 be object such that A25: n1 in NatDivisors n & m1 in NatDivisors m and A26: x = [n1,m1] by A22,ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by A25; A27: n1,m1 are_coprime by A8,A25,Th14; reconsider n19=n1,m19=m1 as non zero Nat by A25; set x9 = (g1").(n1*m1); set fn1=f.n1,fm1=f.m1; b2.x = (multnat * [:f,f:]).x by A22,FUNCT_1:49 .= multnat.([:f,f:].x) by A20,A24,FUNCT_1:13 .= multnat.([:f,f:].(n1,m1)) by A26,BINOP_1:def 1 .= multnat.[f.n1,f.m1] by FUNCT_3:75 .= multnat.(f.n1,f.m1) by BINOP_1:def 1 .= (fn1)*(fm1) by BINOP_2:def 24 .= f.(n19*m19) by A1,A27 .= (f|NatDivisors(n*m)).(n1*m1) by A25,Th16,FUNCT_1:49; then A28: n1*m1 in rng g1 by A23,A21,PRE_POLY:def 7; then n1*m1 in dom(g1") by FUNCT_1:33; then x9 in rng(g1") by FUNCT_1:3; then A29: x9 in dom g1 by FUNCT_1:33; g1.x9 = n1*m1 by A28,FUNCT_1:35 .= multnat.(n1,m1) by BINOP_2:def 24 .= multnat.[n1,m1] by BINOP_1:def 1 .= h9.x by A22,A26,FUNCT_1:49; then h9.x in rng g1 by A29,FUNCT_1:def 3; then h9.x in dom(g1") by FUNCT_1:33; hence x in dom(g1" * h9) by A7,A22,FUNCT_1:11; end; then support b2 c= dom(g1" * h9); then rng g2 c= dom(g1" * h9); then A30: dom(g1" * h9 * g2) = dom g2 by RELAT_1:27; rng g2 c= dom b2 by A19; then A31: dom h = dom f2 by A6,A30,RELAT_1:27; A32: for x being object st x in dom f2 holds f2.x = f1.(h.x) proof let x be object; set x9 = g2.x; A33: b1*g1*(g1" * h9) = b1*g1* g1" * h9 by RELAT_1:36 .= b1*(g1* g1")*h9 by RELAT_1:36 .= b1*(id rng g1)*h9 by FUNCT_1:39 .= b1*(id support b1)*h9 by FUNCT_2:def 3; assume A34: x in dom f2; then A35: x in dom g2 by A6,FUNCT_1:11; then A36: x9 in rng g2 by FUNCT_1:3; then A37: support b2 c= dom b2 & x9 in support b2 by PRE_POLY:37; then consider n1, m1 be object such that A38: n1 in NatDivisors n & m1 in NatDivisors m and A39: x9 = [n1,m1] by ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by A38; A40: n1,m1 are_coprime by A8,A38,Th14; reconsider n19=n1,m19=m1 as non zero Nat by A38; set fn1=f.n1,fm1=f.m1; A41: x9 in [:NatDivisors n, NatDivisors m:] by A37; A42: b2.x9 = (multnat * [:f,f:]).x9 by A37,FUNCT_1:49 .= multnat.([:f,f:].x9) by A20,A41,FUNCT_1:13 .= multnat.([:f,f:].(n1,m1)) by A39,BINOP_1:def 1 .= multnat.[f.n1,f.m1] by FUNCT_3:75 .= multnat.(f.n1,f.m1) by BINOP_1:def 1 .= (fn1)*(fm1) by BINOP_2:def 24 .= f.(n19*m19) by A1,A40; A43: b2.x9 <> 0 by A36,PRE_POLY:def 7; f.(n19*m19) = (f|NatDivisors(n*m)).(n1*m1) by A38,Th16,FUNCT_1:49; then A44: n1*m1 in support b1 by A43,A42,PRE_POLY:def 7; then A45: n1*m1 in dom (id support b1); A46: h9.x9 = multnat.x9 by A7,A37,FUNCT_1:47 .= multnat.(n1,m1) by A39,BINOP_1:def 1 .= n1*m1 by BINOP_2:def 24; A47: (b1*g1).(h.x) = (b1*g1*h).x by A31,A34,FUNCT_1:13 .= (b1*g1*(g1" * h9) * g2).x by RELAT_1:36 .= (b1*g1*(g1" * h9)).(g2.x) by A35,FUNCT_1:13; (b1*(id support b1)*h9).x9 = (b1*(id support b1)).(h9.x9) by A7,A37, FUNCT_1:13 .= b1.((id support b1).(n1*m1)) by A45,A46,FUNCT_1:13 .= b1.(n1*m1) by A44,FUNCT_1:18 .= b2.x9 by A38,A42,Th16,FUNCT_1:49; hence f2.x = f1.(h.x) by A4,A6,A35,A47,A33,FUNCT_1:13; end; for y being object st y in rng g1 holds y in rng(h9 * g2) proof let y be object; assume y in rng g1; then A48: y in support b1 by FUNCT_2:def 3; consider n1,m1 be Nat such that A49: n1 in NatDivisors n & m1 in NatDivisors m and A50: y=n1*m1 by A8,A48,Th18; reconsider n19=n1,m19=m1 as non zero Nat by A49; reconsider n1,m1 as Element of NAT by ORDINAL1:def 12; A51: n1,m1 are_coprime by A8,A49,Th14; A52: b1.y <> 0 by A48,PRE_POLY:def 7; A53: [n1,m1] in [:NatDivisors n, NatDivisors m:] by A49,ZFMISC_1:def 2; set x = g2".[n1,m1]; A54: [n1,m1] in [:NatDivisors n, NatDivisors m:] by A49,ZFMISC_1:def 2; b1.y = f.y by A48,FUNCT_1:49 .= (f.n19)*(f.m19) by A1,A50,A51 .= multnat.(f.n1,f.m1) by BINOP_2:def 24 .= multnat.[f.n1,f.m1] by BINOP_1:def 1 .= multnat.([:f,f:].(n1,m1)) by FUNCT_3:75 .= multnat.([:f,f:].[n1,m1]) by BINOP_1:def 1 .= (multnat * [:f,f:]).[n1,m1] by A20,FUNCT_1:13 .= b2.[n1,m1] by A54,FUNCT_1:49; then [n1,m1] in support b2 by A52,PRE_POLY:def 7; then A55: [n1,m1] in rng g2 by FUNCT_2:def 3; then [n1,m1] in dom(g2") by FUNCT_1:33; then x in rng(g2") by FUNCT_1:3; then A56: x in dom g2 by FUNCT_1:33; A57: y = multnat.(n1,m1) by A50,BINOP_2:def 24 .= multnat.[n1,m1] by BINOP_1:def 1 .= (multnat|[:NatDivisors n, NatDivisors m:]).[n1,m1] by A53,FUNCT_1:49 .= h9.(g2.(g2".[n1,m1])) by A55,FUNCT_1:35 .= (h9 * g2).x by A56,FUNCT_1:13; g2.(g2".[n1,m1]) = [n1,m1] by A55,FUNCT_1:35; then x in dom(h9 * g2) by A7,A53,A56,FUNCT_1:11; hence y in rng(h9 * g2) by A57,FUNCT_1:def 3; end; then rng g1 c= rng(h9 * g2); then dom(g1") c= rng(h9 * g2) by FUNCT_1:33; then rng(g1" * (h9 * g2)) = rng(g1") by RELAT_1:28; then A58: rng(g1" * (h9 * g2)) = dom g1 by FUNCT_1:33; support b1 c= dom b1 by PRE_POLY:37; then rng g1 c= dom b1 by FUNCT_2:def 3; then dom(b1 * g1) = dom g1 by RELAT_1:27; then A59: rng h = dom f1 by A4,A58,RELAT_1:36; then for x being object holds x in dom f2 iff x in dom h & h.x in dom f1 by A31,FUNCT_1:3; then f2 = f1 * h by A32,FUNCT_1:10; then A60: f1,f2 are_fiberwise_equipotent by A31,A59,CLASSES1:77; thus F.(n*m) = Sum(f|NatDivisors(n*m)) by A2 .= Sum((multnat * [:f,f:])|[:NatDivisors n, NatDivisors m:]) by A3,A5,A60 ,RFINSEQ:9 .= Sum(f|NatDivisors n) * Sum(f|NatDivisors m) by Th28 .= Sum(f|NatDivisors n) * F.m by A2 .= F.n * F.m by A2; end; hence F is multiplicative; end; theorem Th35: EXP(k) is multiplicative proof for n,m being non zero Nat st n,m are_coprime holds ( EXP(k)).(n*m) = (EXP(k)).n * (EXP(k)).m proof let n,m be non zero Nat; assume n,m are_coprime; thus (EXP(k)).(n*m) = (n*m)|^k by Def1 .= n|^k * m|^k by NEWTON:7 .= (EXP(k)).n * m|^k by Def1 .= (EXP(k)).n * (EXP(k)).m by Def1; end; hence EXP(k) is multiplicative; end; theorem Th36: Sigma(k) is multiplicative proof for n being non zero Nat holds (Sigma k).n = Sum((EXP k)| NatDivisors n) proof let n be non zero Nat; thus (Sigma k).n = sigma(k,n) by Def3 .= Sum((EXP k)|NatDivisors n) by Def2; end; hence Sigma(k) is multiplicative by Th34,Th35; end; theorem Th37: n0,m0 are_coprime implies sigma(n0*m0) = sigma(n0) * sigma m0 proof assume A1: n0,m0 are_coprime; A2: Sigma 1 is multiplicative by Th36; thus sigma(n0*m0) = (Sigma 1).(n0*m0) by Def3 .= ((Sigma 1).n0) * (Sigma 1).m0 by A1,A2 .= sigma(1,n0) * (Sigma 1).m0 by Def3 .= sigma(n0) * sigma m0 by Def3; end; begin :: The Perfect Number Theorem definition let n0 be non zero natural Number; attr n0 is perfect means sigma n0 = 2 * n0; end; :: Fundamentals of Number Theory (LeVeque) p.123 :: Euclid theorem 2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1) implies n0 is perfect proof set n1=2|^(p -' 1); set k = p -' 2; A1: (2|^p - 1)|^2 = (2|^p - 1)|^(1+1) .= ((2|^p - 1)|^1)*(2|^p - 1) by NEWTON:6 .= (2|^p - 1)*(2|^p - 1) .= (2|^p - 1)^2 by SQUARE_1:def 1 .= (2|^p)^2 - 2*(2|^p)*1 + 1^2 by SQUARE_1:5 .= (2|^p)*(2|^p) -2*(2|^p) + 1^2 by SQUARE_1:def 1 .= (2|^p)*(2|^p) -2*(2|^p) + 1*1 by SQUARE_1:def 1 .= (2|^p)*(2|^p - 2) + 1; 2|^p > p by NEWTON:86; then 2|^p >= p+1 by NAT_1:13; then A2: 2|^p - 2 >= p+1-2 by XREAL_1:9; assume A3: 2|^p -' 1 is prime; A4: now assume A5: p <= 1; per cases by A5,NAT_1:25; suppose p = 0; then 2|^p -' 1 = 1 -' 1 by NEWTON:4 .= 1 - 1 by XREAL_0:def 2 .= 0; hence contradiction by A3; end; suppose p = 1; then 2|^p -' 1 = 2 -' 1 .= 2 - 1 by XREAL_0:def 2 .= 1; hence contradiction by A3,INT_2:def 4; end; end; then A6: p-1>1-1 by XREAL_1:9; then A7: p -' 1 = p - 1 by XREAL_0:def 2; p>=1+1 by A4,NAT_1:13; then p-2 >= 2-2 by XREAL_1:9; then A8: k = p - 2 by XREAL_0:def 2; then A9: p = k + 2; 2|^p > p by NEWTON:86; then 2|^p > 1 by A4,XXREAL_0:2; then A10: 2|^p - 1 > 1 - 1 by XREAL_1:9; then A11: 2|^p - 1 = 2|^p -' 1 by XREAL_0:def 2; reconsider n2=2|^p -' 1 as non zero Nat by A10,XREAL_0:def 2; assume A12: n0 = 2|^(p -' 1)*(2|^p -' 1); p -' 1 = k + 1 by A6,A8,XREAL_0:def 2; then n1,n2 are_coprime by A3,A11,A9,Th1,EULER_1:2; then sigma n0 = (sigma n1)*sigma n2 by A12,Th37 .= (2|^(p -' 1 + 1) - 1)/(2 - 1)*sigma n2 by Th30,INT_2:28 .= sigma(n2|^1)*(2|^p -' 1) by A7,A11 .= (n2|^(1+1)-1)/(n2 - 1)*(2|^p -' 1) by A3,Th30 .= 2|^(p -' 1 + 1)*(2|^p -' 1) by A6,A7,A11,A1,A2,XCMPLX_1:89 .= 2|^(p -' 1)*2*(2|^p -' 1) by NEWTON:6 .= 2 * n0 by A12; hence n0 is perfect; end; :: Euler ::\$N The Perfect Number Theorem theorem n0 is even & n0 is perfect implies ex p being Nat st 2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1) proof assume n0 is even; then consider k9,n9 be Nat such that A1: n9 is odd and A2: k9 > 0 and A3: n0 = 2|^k9 * n9 by Th2; reconsider n2=n9 as non zero Nat by A1; set p=k9+1; A4: p - 1 = p -' 1 by XREAL_0:def 2; then A5: 2|^p - 1 = 2|^(p-'1+1)-2+1 .= 2|^(p-'1)*2-2+1 by NEWTON:6 .= 2*(2|^(p-'1)-1)+1; assume n0 is perfect; then A6: sigma n0 = 2 * n0; take p; 2|^p > p by NEWTON:86; then A7: 2|^p - 1 > p - 1 by XREAL_1:14; then A8: 2|^p - 1 = 2|^p -' 1 by XREAL_0:def 2; sigma(2|^(p -' 1)) = (2|^(p -' 1 + 1) - 1)/(2 - 1) by Th30,INT_2:28 .= 2|^p - 1 by A4; then A9: (2|^p - 1)*sigma(n9) = 2 * 2|^(p -' 1)*n9 by A1,A3,A6,A4,Th3,Th37 .= 2|^p*n9 by A4,NEWTON:6; then (2|^p -' 1) divides 2|^p*n2 by A8,INT_1:def 3; then (2|^p -' 1) divides n2 by A8,A5,Th3,EULER_1:13; then consider n99 be Nat such that A10: n9 = (2|^p -' 1)*n99 by NAT_D:def 3; sigma(n9)*(2|^p - 1) = 2|^p*n99*(2|^p - 1) by A8,A9,A10; then A11: sigma(n2) = (2|^p - 1)*n99 + n99 by A7,XCMPLX_1:5 .= n9 + n99 by A7,A10,XREAL_0:def 2; A12: n99 divides n9 by A10,NAT_D:def 3; k9>=0+1 by A2,NAT_1:13; then B01: k9+1 >= 1+1 by XREAL_1:7; 2|^p > p by NEWTON:86; then 2|^p > 2 by B01,XXREAL_0:2; then A13: 2|^p -1 > 2-1 by XREAL_1:14; then (2|^p -' 1)*n2 > 1*n2 by A8,XREAL_1:68; then A14: n99=1 by A10,A12,A11,Th33; hence 2|^p -' 1 is prime by A8,A10,A12,A13,A11,Th33; thus n0 = 2|^(p -' 1)*(2|^p -' 1) by A3,A4,A10,A14; end; begin :: A Formula involving Euler's Function definition func Euler_phi -> sequence of NAT means :Def7: for k being Element of NAT holds it.k = Euler(k); existence proof ex f being sequence of NAT st for k being Element of NAT holds f.k = Euler(k) from FUNCT_2:sch 4; hence thesis; end; uniqueness proof A1: for f1, f2 be sequence of NAT st (for x being Element of NAT holds f1.x = Euler(x)) & (for x being Element of NAT holds f2.x = Euler(x)) holds f1 = f2 from BINOP_2:sch 1; let f1, f2 be sequence of NAT; assume ( for k being Element of NAT holds f1.k = Euler(k))& for k being Element of NAT holds f2.k = Euler(k); hence thesis by A1; end; end; :: Number Theory (Andrews) p.76 theorem Sum(Euler_phi|NatDivisors n0) = n0 proof dom Euler_phi = NAT & rng Euler_phi c= REAL by FUNCT_2:def 1; then reconsider EU9 = Euler_phi as sequence of REAL by FUNCT_2:2; set X = Seg n0; defpred P[set,set] means \$2 = {i where i is Element of NAT: ex h being Nat st i in X & \$1 in NatDivisors n0 & h=\$1 & i gcd n0 = n0 / h}; A1: dom Euler_phi = NAT by FUNCT_2:def 1; A2: for k being Nat st k in X ex x being Element of bool X st P[k ,x] proof let k be Nat; set X9 = {i where i is Element of NAT: ex h being Nat st i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h}; for x being object st x in X9 holds x in X proof let x be object; assume x in X9; then ex i be Element of NAT st i=x & ex h being Nat st i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h; hence x in X; end; then reconsider X9 as Element of bool X by TARSKI:def 3; assume k in X; take X9; thus P[k,X9]; end; consider fp be FinSequence of bool X such that A3: dom fp = X & for k being Nat st k in X holds P[k,fp.k] from FINSEQ_1:sch 5(A2); A4: NatDivisors n0 c= Seg n0 by MOEBIUS1:40; then A5: rng Sgm NatDivisors n0 c= dom fp by A3,FINSEQ_1:def 13; then A6: rng Sgm NatDivisors n0 c= dom Card fp by CARD_3:def 2; then reconsider f1 = (Card fp)*Sgm NatDivisors n0 as FinSequence of NAT by Th9; A7: NatDivisors n0 c= dom fp by A3,MOEBIUS1:40; A8: dom((Card fp)*Sgm NatDivisors n0) = dom Sgm NatDivisors n0 by A6,RELAT_1:27 .= dom(Euler_phi * Sgm NatDivisors n0) by A5,A1,RELAT_1:27,XBOOLE_1:1; for k being Element of NAT st k in dom((Card fp)*Sgm NatDivisors n0) holds ((Card fp)*Sgm NatDivisors n0).k = (Euler_phi * Sgm NatDivisors n0).k proof let k be Element of NAT; set k9 = (Sgm NatDivisors n0).k; set Y = {l where l is Element of NAT : k9,l are_coprime & l >= 1 & l <= k9}; set Z = {i where i is Element of NAT: ex h being Nat st i in X & k9 in NatDivisors n0 & h=k9 & i gcd n0 = n0 / h}; deffunc F(Nat) = \$1*n0/k9; A9: for x being object st x in Y holds x in NAT proof let x be object; assume x in Y; then ex l be Element of NAT st x=l & k9,l are_coprime & l >= 1 & l <= k9; hence x in NAT; end; assume A10: k in dom((Card fp)*Sgm NatDivisors n0); then k in dom Sgm NatDivisors n0 by FUNCT_1:11; then k9 in rng Sgm NatDivisors n0 by FUNCT_1:3; then A11: k9 in NatDivisors n0 by A4,FINSEQ_1:def 13; then A12: 1 <= k9 by A3,A7,FINSEQ_1:1; k9,1 are_coprime by WSIERP_1:9; then 1 in Y by A12; then reconsider Y as non empty Subset of NAT by A9,TARSKI:def 3; consider f be Function such that A13: dom f = Y & for d being Element of Y holds f.d = F(d) from FUNCT_1:sch 4; for y being object holds y in rng f iff y in Z proof let y be object; hereby assume y in rng f; then consider x be object such that A14: x in dom f and A15: y = f.x by FUNCT_1:def 3; reconsider x as Element of Y by A13,A14; A16: 0 < k9 by A11; k9 divides n0 by A11,MOEBIUS1:39; then consider j be Nat such that A17: n0 = k9*j by NAT_D:def 3; y = F(x) by A13,A15 .= x*(n0/k9) by XCMPLX_1:74; then A18: y = x*(j/(k9/k9)) by A17,XCMPLX_1:77 .= x*(j/1) by A16,XCMPLX_1:60 .= x*j; then reconsider i=y as Element of NAT by ORDINAL1:def 12; x in Y; then consider l be Element of NAT such that A19: x=l and A20: k9,l are_coprime and A21: l >= 1 and A22: l <= k9; A23: x*j <= k9*j by A19,A22,XREAL_1:64; j<>0 by A17; then j+1 > 0+1 by XREAL_1:6; then 1 <= j by NAT_1:13; then 1*1 <= x*j by A19,A21,XREAL_1:66; then A24: i in X by A17,A18,A23; A25: k9 gcd l = 1 by A20,INT_2:def 3; n0/k9 = j/(k9/k9) by A17,XCMPLX_1:77 .= j/1 by A16,XCMPLX_1:60; then i gcd n0 = n0 / k9 by A19,A17,A18,A25,EULER_1:5; hence y in Z by A11,A24; end; assume y in Z; then consider i be Element of NAT such that A26: i=y and A27: ex h being Nat st i in X & k9 in NatDivisors n0 & h =k9 & i gcd n0 = n0 / h; i gcd n0 divides i by INT_2:def 2; then consider x be Nat such that A28: i = (i gcd n0)*x by NAT_D:def 3; A29: y = x*n0/k9 by A26,A27,A28,XCMPLX_1:74; reconsider x as Element of NAT by ORDINAL1:def 12; A30: k9<>0 by A27; A31: k9*(i gcd n0) = n0/(k9/k9) by A27,XCMPLX_1:81 .= n0/1 by A30,XCMPLX_1:60; then A32: k9,x are_coprime by A27,A28,EULER_1:6; x<>0 by A27,A28,FINSEQ_1:1; then x+1 > 0+1 by XREAL_1:6; then A33: x >= 1 by NAT_1:13; i <= n0 by A27,FINSEQ_1:1; then x <= k9 by A27,A28,A31,XREAL_1:68; then x in dom f by A13,A32,A33; then reconsider x as Element of Y by A13; y = f.x by A13,A29; hence y in rng f by A13,FUNCT_1:def 3; end; then A34: rng f = Z by TARSKI:2; for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2 proof let x1,x2 be object; assume x1 in dom f; then reconsider x19=x1 as Element of Y by A13; assume x2 in dom f; then reconsider x29=x2 as Element of Y by A13; assume A35: f.x1 = f.x2; A36: F(x19) = f.x19 by A13 .= F(x29) by A13,A35; x19*(n0/k9) = x19*n0/k9 by XCMPLX_1:74 .= x29*(n0/k9) by A36,XCMPLX_1:74; hence x1 = x2 by A12,XCMPLX_1:5; end; then f is one-to-one by FUNCT_1:def 4; then A37: Y,Z are_equipotent by A13,A34,WELLORD2:def 4; fp.k9 = Z by A3,A7,A11; then card (fp.k9) = card Y by A37,CARD_1:5; then (Card fp).k9 = Euler(k9) by A7,A11,CARD_3:def 2; then A38: (Card fp).k9 = Euler_phi.k9 by Def7; ((Card fp)*Sgm NatDivisors n0).k = (Card fp).k9 by A10,FUNCT_1:12; hence thesis by A8,A10,A38,FUNCT_1:12; end; then A39: (Card fp)*Sgm NatDivisors n0 = Euler_phi * Sgm NatDivisors n0 by A8, PARTFUN1:5; set k = len fp; A40: Func_Seq(Euler_phi,Sgm NatDivisors n0) = Euler_phi*(Sgm NatDivisors n0 ) by BHSP_5:def 4 .= Func_Seq(EU9,Sgm NatDivisors n0) by BHSP_5:def 4; A41: for x being object holds x in NatDivisors n0 iff x in Seg n0 & not x in ( Card fp)"{0} proof reconsider y = 0 as Element of NAT; let x be object; A42: y in {0} by TARSKI:def 1; hereby assume A43: x in NatDivisors n0; then reconsider k=x as Element of NAT; thus x in Seg n0 by A4,A43; assume x in (Card fp)"{0}; then consider y be object such that A44: [x,y] in Card fp & y in {0} by RELAT_1:def 14; y = 0 & y = (Card fp).x by A44,FUNCT_1:1,TARSKI:def 1; then card (fp.x) = {} by A3,A4,A43,CARD_3:def 2; then A45: fp.x = {}; k divides n0 by A43,MOEBIUS1:39; then consider i be Nat such that A46: n0 = k * i by NAT_D:def 3; i <> 0 by A46; then 0+1 < i+1 by XREAL_1:6; then A47: 1 <= i by NAT_1:13; A48: i divides n0 by A46,NAT_D:def 3; then i <= n0 by NAT_D:7; then A49: i in X by A47; A50: k <> 0 by A46; n0 = k * (i gcd n0) by A46,A48,NEWTON:49; then n0 / k = (i gcd n0) * (k / k) by XCMPLX_1:74 .= (i gcd n0) * 1 by A50,XCMPLX_1:60; then i in {i9 where i9 is Element of NAT: ex h being Nat st i9 in X & k in NatDivisors n0 & h=k & i9 gcd n0 = n0 / h} by A43,A49; hence contradiction by A3,A4,A43,A45; end; assume A51: x in Seg n0; then reconsider k=x as Element of NAT; A52: fp.k = {i9 where i9 is Element of NAT: ex h being Nat st i9 in X & k in NatDivisors n0 & h=k & i9 gcd n0 = n0 / h} by A3,A51; assume A53: not x in (Card fp)"{0}; assume A54: not x in NatDivisors n0; fp.k = {} proof assume fp.k <> {}; then consider x9 be object such that A55: x9 in fp.k by XBOOLE_0:def 1; ex i be Element of NAT st x9 = i & ex h being Nat st i in X & k in NatDivisors n0 & h=k & i gcd n0 = n0 / h by A52,A55; hence contradiction by A54; end; then A56: y = (Card fp).x by A3,A51,CARD_1:27,CARD_3:def 2; x in dom Card fp by A3,A51,CARD_3:def 2; then [k,y] in Card fp by A56,FUNCT_1:1; hence contradiction by A53,A42,RELSET_1:30; end; reconsider f29=Card fp as FinSequence of REAL by Th13; reconsider f19=f1 as FinSequence of REAL by Th13; A57: NatDivisors n0 c= Seg n0 by MOEBIUS1:40; Seg n0 = dom Card fp by A3,CARD_3:def 2; then f19 = f29 - {0} by A41,XBOOLE_0:def 5; then A58: Sum f19 = Sum f29 by Th12; A59: for d,e being Nat st d in dom fp & e in dom fp & d<>e holds fp.d misses fp.e proof let d,e be Nat; assume d in dom fp; then A60: fp.d = {i where i is Element of NAT: ex h being Nat st i in X & d in NatDivisors n0 & h=d & i gcd n0 = n0 / h} by A3; assume e in dom fp; then A61: fp.e = {i where i is Element of NAT: ex h being Nat st i in X & e in NatDivisors n0 & h=e & i gcd n0 = n0 / h} by A3; assume A62: d<>e; assume not fp.d misses fp.e; then fp.d /\ fp.e <> {} by XBOOLE_0:def 7; then consider x be object such that A63: x in fp.d /\ fp.e by XBOOLE_0:def 1; x in fp.d by A63,XBOOLE_0:def 4; then A64: ex i1 be Element of NAT st x=i1 & ex h being Nat st i1 in X & d in NatDivisors n0 & h=d & i1 gcd n0 = n0 / h by A60; x in fp.e by A63,XBOOLE_0:def 4; then ex i2 be Element of NAT st x=i2 & ex h being Nat st i2 in X & e in NatDivisors n0 & h=e & i2 gcd n0 = n0 / h by A61; then d = n0 / (n0 / e) by A64,XCMPLX_1:52; hence contradiction by A62,XCMPLX_1:52; end; A65: for x being object holds x in union rng fp iff x in X proof let x be object; thus x in union rng fp implies x in X; assume A66: x in X; then reconsider i=x as Nat; i gcd n0 divides n0 by NAT_D:def 5; then consider h be Nat such that A67: n0 = (i gcd n0) * h by NAT_D:def 3; A68: 0 < h by A67; then 0+1 < h+1 by XREAL_1:6; then A69: 1 <= h by NAT_1:13; A70: h divides n0 by A67,NAT_D:def 3; then A71: h in NatDivisors n0 by A68,MOEBIUS1:39; set Y = fp.h; A72: h <> 0 by A67; h <= n0 by A70,NAT_D:7; then A73: h in dom fp by A3,A69; then A74: Y in rng fp by FUNCT_1:3; A75: fp.h = {i9 where i9 is Element of NAT: ex h9 being Nat st i9 in X & h in NatDivisors n0 & h9=h & i9 gcd n0 = n0 / h9} by A3,A73; n0 / h = (i gcd n0) * (h / h) by A67,XCMPLX_1:74 .= (i gcd n0) * 1 by A72,XCMPLX_1:60; then x in Y by A66,A71,A75; hence x in union rng fp by A74,TARSKI:def 4; end; len fp = k; then card union rng fp = Sum Card fp by A59,INT_5:48; then A76: card X = Sum Card fp by A65,TARSKI:2; card X = card n0 by FINSEQ_1:55; then n0 = Sum Card fp by A76; then Sum Func_Seq(Euler_phi,Sgm NatDivisors n0) = n0 by A58,A39,BHSP_5:def 4; hence thesis by A40,A57,Th24; end;