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