:: NAT_5 semantic presentation begin Lm1: for p being Nat for n0, m0 being non zero Nat st p is prime holds p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) proof let p be Nat; ::_thesis: for n0, m0 being non zero Nat st p is prime holds p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) let n0, m0 be non zero Nat; ::_thesis: ( p is prime implies p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) ) reconsider h9 = n0 gcd m0 as non empty Nat by INT_2:5; assume A1: p is prime ; ::_thesis: p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) 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; percases ( p |-count n0 <= p |-count m0 or not p |-count n0 <= p |-count m0 ) ; supposeA4: p |-count n0 <= p |-count m0 ; ::_thesis: p |-count (n0 gcd m0) = min ((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 p9 |^ (p9 |-count n0) divides n0 by NAT_3:def_7; then p9 |^ (p9 |-count n0) divides h9 by A5, INT_2:def_2; then p9 |-count (p9 |^ (p9 |-count n0)) <= 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 p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by A4, XXREAL_0:def_9; ::_thesis: verum end; supposeA7: not p |-count n0 <= p |-count m0 ; ::_thesis: p |-count (n0 gcd m0) = min ((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 p9 |^ (p9 |-count m0) divides m0 by NAT_3:def_7; then p9 |^ (p9 |-count m0) divides h9 by A8, INT_2:def_2; then p9 |-count (p9 |^ (p9 |-count m0)) <= 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 p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by A7, XXREAL_0:def_9; ::_thesis: verum end; end; end; theorem Th1: :: NAT_5:1 for n being Nat holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1 proof let n be Nat; ::_thesis: 2 |^ (n + 1) < (2 |^ (n + 2)) - 1 defpred S1[ Nat] means 2 |^ ($1 + 1) < (2 |^ ($1 + 2)) - 1; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] 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 S1[k + 1] by A2, XXREAL_0:2; ::_thesis: verum end; 2 < 3 ; then 2 |^ 1 < (2 * 2) - 1 by NEWTON:5; then 2 |^ 1 < ((2 |^ 1) * 2) - 1 by NEWTON:5; then 2 |^ 1 < (2 |^ (1 + 1)) - 1 by NEWTON:6; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); hence 2 |^ (n + 1) < (2 |^ (n + 2)) - 1 ; ::_thesis: verum end; theorem Th2: :: NAT_5:2 for n0 being non zero Nat st n0 is even holds ex k, m being Nat st ( m is odd & k > 0 & n0 = (2 |^ k) * m ) proof let n0 be non zero Nat; ::_thesis: ( n0 is even implies ex k, m being Nat st ( m is odd & k > 0 & n0 = (2 |^ k) * m ) ) assume A1: n0 is even ; ::_thesis: ex k, m being Nat st ( m is odd & k > 0 & n0 = (2 |^ k) * m ) set k = 2 |-count n0; 2 |^ (2 |-count n0) divides n0 by NAT_3:def_7; then consider m being Nat such that A2: n0 = (2 |^ (2 |-count n0)) * m by NAT_D:def_3; take 2 |-count n0 ; ::_thesis: ex m being Nat st ( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m ) take m ; ::_thesis: ( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m ) A3: now__::_thesis:_m_is_odd reconsider m9 = m as Element of NAT by ORDINAL1:def_12; assume not m is odd ; ::_thesis: contradiction then consider m99 being Element of NAT such that A4: m9 = 2 * m99 by ABIAN:def_2; n0 = ((2 |^ (2 |-count n0)) * 2) * m99 by A2, A4 .= (2 |^ ((2 |-count n0) + 1)) * m99 by NEWTON:6 ; then 2 |^ ((2 |-count n0) + 1) divides n0 by NAT_D:def_3; hence contradiction by NAT_3:def_7; ::_thesis: verum end; hence m is odd ; ::_thesis: ( 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m ) now__::_thesis:_not_2_|-count_n0_=_0 assume 2 |-count n0 = 0 ; ::_thesis: contradiction then n0 = 1 * m by A2, NEWTON:4; hence contradiction by A1, A3; ::_thesis: verum end; hence 2 |-count n0 > 0 ; ::_thesis: n0 = (2 |^ (2 |-count n0)) * m thus n0 = (2 |^ (2 |-count n0)) * m by A2; ::_thesis: verum end; theorem Th3: :: NAT_5:3 for n, k, m being Nat st n = 2 |^ k & m is odd holds n,m are_relative_prime proof let n, k, m be Nat; ::_thesis: ( n = 2 |^ k & m is odd implies n,m are_relative_prime ) assume A1: n = 2 |^ k ; ::_thesis: ( not m is odd or n,m are_relative_prime ) assume A2: m is odd ; ::_thesis: n,m are_relative_prime 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 ; ::_thesis: ( p is prime implies p |-count h = p |-count 1 ) assume A3: p is prime ; ::_thesis: p |-count h = p |-count 1 A4: min ((p |-count n),(p |-count m)) = 0 proof percases ( p = 2 or p <> 2 ) ; supposeA5: p = 2 ; ::_thesis: min ((p |-count n),(p |-count m)) = 0 not p divides m proof assume p divides m ; ::_thesis: contradiction then consider m9 being Nat such that A6: m = p * m9 by NAT_D:def_3; thus contradiction by A2, A5, A6; ::_thesis: verum end; then p |-count m = 0 by A5, NAT_3:27; hence min ((p |-count n),(p |-count m)) = 0 by XXREAL_0:def_9; ::_thesis: verum end; supposeA7: p <> 2 ; ::_thesis: min ((p |-count n),(p |-count m)) = 0 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 by A8 ; hence min ((p |-count n),(p |-count m)) = 0 by XXREAL_0:def_9; ::_thesis: verum end; 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; ::_thesis: verum end; then n gcd m = 1 by NAT_4:21; hence n,m are_relative_prime by INT_2:def_3; ::_thesis: verum end; theorem Th4: :: NAT_5:4 for n being Nat holds {n} is finite Subset of NAT proof let n be Nat; ::_thesis: {n} is finite Subset of NAT n in NAT by ORDINAL1:def_12; hence {n} is finite Subset of NAT by ZFMISC_1:31; ::_thesis: verum end; theorem Th5: :: NAT_5:5 for n, m being Nat holds {n,m} is finite Subset of NAT proof let n, m be Nat; ::_thesis: {n,m} is finite Subset of NAT ( n in NAT & m in NAT ) by ORDINAL1:def_12; hence {n,m} is finite Subset of NAT by ZFMISC_1:32; ::_thesis: verum end; Lm2: for n, m, l being Nat holds {n,m,l} is finite Subset of NAT proof let n, m, l be Nat; ::_thesis: {n,m,l} is finite Subset of NAT 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 ; ::_thesis: verum end; Lm3: for n, m, l, k being Nat holds {n,m,l,k} is finite Subset of NAT proof let n, m, l, k be Nat; ::_thesis: {n,m,l,k} is finite Subset of NAT 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 ; ::_thesis: verum end; theorem Th6: :: NAT_5:6 for n being Nat for f being FinSequence st f is one-to-one holds Del (f,n) is one-to-one proof let n be Nat; ::_thesis: for f being FinSequence st f is one-to-one holds Del (f,n) is one-to-one let f be FinSequence; ::_thesis: ( f is one-to-one implies Del (f,n) is one-to-one ) 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 ; ::_thesis: Del (f,n) is one-to-one hence Del (f,n) is one-to-one by A1; ::_thesis: verum end; theorem Th7: :: NAT_5:7 for n being Nat for f being FinSequence st f is one-to-one & n in dom f holds not f . n in rng (Del (f,n)) proof let n be Nat; ::_thesis: for f being FinSequence st f is one-to-one & n in dom f holds not f . n in rng (Del (f,n)) let f be FinSequence; ::_thesis: ( f is one-to-one & n in dom f implies not f . n in rng (Del (f,n)) ) assume A1: f is one-to-one ; ::_thesis: ( not n in dom f or not f . n in rng (Del (f,n)) ) 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 ; ::_thesis: not f . n in rng (Del (f,n)) then consider m being 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)) ; ::_thesis: contradiction then consider j being set 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 = j as Element of NAT by A6; percases ( j < n9 or j >= n9 ) ; supposeA9: j < n9 ; ::_thesis: contradiction then f . n = f . j by A7, FINSEQ_3:110; hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def_4; ::_thesis: verum end; supposeA10: j >= n9 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; theorem Th8: :: NAT_5:8 for n being Nat for f being FinSequence for x being set st x in rng f & not x in rng (Del (f,n)) holds x = f . n proof let n be Nat; ::_thesis: for f being FinSequence for x being set st x in rng f & not x in rng (Del (f,n)) holds x = f . n let f be FinSequence; ::_thesis: for x being set st x in rng f & not x in rng (Del (f,n)) holds x = f . n let x be set ; ::_thesis: ( x in rng f & not x in rng (Del (f,n)) implies x = f . n ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume A1: x in rng f ; ::_thesis: ( x in rng (Del (f,n)) or x = f . n ) then consider j being set 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 being 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)) ; ::_thesis: x = 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 = j as Element of NAT by A2; reconsider m9 = m as Element of NAT by ORDINAL1:def_12; assume A11: not x = f . n ; ::_thesis: contradiction A12: n <= m + 1 by A9, FINSEQ_1:1; percases ( j < n9 or j >= n9 ) ; supposeA13: j < n9 ; ::_thesis: contradiction then (Del (f,n9)) . j = f . j by FINSEQ_3:110; then not j in dom (Del (f,n)) by A3, A6, FUNCT_1:def_3; then not j in Seg m by A8, FINSEQ_1:def_3; then A14: ( j < 1 or j > m ) ; j <= m + 1 by A5, FINSEQ_1:1; hence contradiction by A5, A12, A13, A14, FINSEQ_1:1, NAT_1:8; ::_thesis: verum end; supposeA15: j >= n9 ; ::_thesis: contradiction set j9 = j -' 1; j <= m + 1 by A5, FINSEQ_1:1; then j - 1 <= (m + 1) - 1 by XREAL_1:9; then A16: j -' 1 <= 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 j -' 1 >= n9 by XREAL_0:def_2; then j -' 1 >= 1 by A10, XXREAL_0:2; then j -' 1 in Seg m by A16; then A18: j -' 1 in dom (Del (f,n)) by A8, FINSEQ_1:def_3; A19: n9 in dom f by A1, A6, FINSEQ_3:104; n9 <= j -' 1 by A17, XREAL_0:def_2; then (Del (f,n9)) . (j -' 1) = f . ((j -' 1) + 1) by A4, A19, A16, FINSEQ_3:111; then f . j <> f . ((j -' 1) + 1) by A3, A6, A18, FUNCT_1:def_3; then f . j <> f . ((j - 1) + 1) by A17, XREAL_0:def_2; hence contradiction ; ::_thesis: verum end; end; end; theorem Th9: :: NAT_5:9 for X being set for f1 being FinSequence of NAT for f2 being FinSequence of X st rng f1 c= dom f2 holds f2 * f1 is FinSequence of X proof let X be set ; ::_thesis: for f1 being FinSequence of NAT for f2 being FinSequence of X st rng f1 c= dom f2 holds f2 * f1 is FinSequence of X let f1 be FinSequence of NAT ; ::_thesis: for f2 being FinSequence of X st rng f1 c= dom f2 holds f2 * f1 is FinSequence of X let f2 be FinSequence of X; ::_thesis: ( rng f1 c= dom f2 implies f2 * f1 is FinSequence of X ) consider n being Nat such that A1: dom f1 = Seg n by FINSEQ_1:def_2; assume rng f1 c= dom f2 ; ::_thesis: f2 * f1 is FinSequence of X 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; ::_thesis: verum end; theorem Th10: :: NAT_5:10 for X, Y being set for f1, f2, f3 being FinSequence of REAL st X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) holds Sum f1 = (Sum f2) + (Sum f3) proof let X, Y be set ; ::_thesis: for f1, f2, f3 being FinSequence of REAL st X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) holds Sum f1 = (Sum f2) + (Sum f3) let f1, f2, f3 be FinSequence of REAL ; ::_thesis: ( X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) implies Sum f1 = (Sum f2) + (Sum f3) ) assume A1: X \/ Y = dom f1 ; ::_thesis: ( not X misses Y or not f2 = f1 * (Sgm X) or not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) ) assume A2: X misses Y ; ::_thesis: ( not f2 = f1 * (Sgm X) or not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) ) assume A3: f2 = f1 * (Sgm X) ; ::_thesis: ( not f3 = f1 * (Sgm Y) or Sum f1 = (Sum f2) + (Sum f3) ) assume A4: f3 = f1 * (Sgm Y) ; ::_thesis: Sum f1 = (Sum f2) + (Sum f3) percases ( dom f1 = {} or dom f1 <> {} ) ; supposeA5: dom f1 = {} ; ::_thesis: Sum f1 = (Sum f2) + (Sum f3) then Y = {} by A1; then A6: f3 = {} by A4, FINSEQ_3:43; X = {} by A1, A5; then f2 = {} by A3, FINSEQ_3:43; hence Sum f1 = (Sum f2) + (Sum f3) by A5, A6, RELAT_1:41, RVSUM_1:72; ::_thesis: verum end; supposeA7: dom f1 <> {} ; ::_thesis: Sum f1 = (Sum f2) + (Sum f3) 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 by RELAT_1:45; A10: 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 by RELAT_1:45; then A11: F " ((rng F) \ X) = Y by A10, FUNCT_2:94; A12: 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 A12, FUNCT_2:94; then reconsider s = (Sgm X) ^ (Sgm Y) as Permutation of (dom F1) by A11, 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 A13: 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, A13, MESFUNC3:2; ::_thesis: verum end; end; end; theorem Th11: :: NAT_5:11 for X being set for f2, f1 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds Sum f1 = Sum f2 proof let X be set ; ::_thesis: for f2, f1 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds Sum f1 = Sum f2 let f2, f1 be FinSequence of REAL ; ::_thesis: ( f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 implies Sum f1 = Sum f2 ) assume A1: f2 = f1 * (Sgm X) ; ::_thesis: ( not (dom f1) \ (f1 " {0}) c= X or not X c= dom f1 or Sum f1 = Sum f2 ) set Y = (dom f1) \ X; assume A2: (dom f1) \ (f1 " {0}) c= X ; ::_thesis: ( not X c= dom f1 or Sum f1 = Sum f2 ) assume A3: X c= dom f1 ; ::_thesis: Sum f1 = Sum f2 percases ( (dom f1) \ X = {} or (dom f1) \ X <> {} ) ; supposeA4: (dom f1) \ X = {} ; ::_thesis: Sum f1 = Sum f2 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 Sum f1 = Sum f2 by A1, FINSEQ_2:54; ::_thesis: verum end; supposeA5: (dom f1) \ X <> {} ; ::_thesis: Sum f1 = Sum f2 set f3 = f1 * (Sgm ((dom f1) \ X)); A6: (dom f1) \ X c= dom f1 by XBOOLE_1:36; then A7: (dom f1) \ X c= Seg (len f1) by FINSEQ_1:def_3; then rng (Sgm ((dom f1) \ X)) c= dom f1 by A6, FINSEQ_1:def_13; then reconsider f3 = f1 * (Sgm ((dom f1) \ X)) as FinSequence of REAL by Th9; A8: X misses (dom f1) \ X by XBOOLE_1:79; A9: (dom f1) \ X c= f1 " {0} proof assume not (dom f1) \ X c= f1 " {0} ; ::_thesis: contradiction then consider x being set such that A10: x in (dom f1) \ X and A11: not x in f1 " {0} by TARSKI:def_3; 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 /\ ((dom f1) \ X) by A2, A10, XBOOLE_0:def_4; hence contradiction by A8, XBOOLE_0:def_7; ::_thesis: verum end; for y being set holds ( y in rng f3 iff y = 0 ) proof let y be set ; ::_thesis: ( y in rng f3 iff y = 0 ) consider x being set such that A12: x in (dom f1) \ X by A5, XBOOLE_0:def_1; hereby ::_thesis: ( y = 0 implies y in rng f3 ) assume y in rng f3 ; ::_thesis: y = 0 then consider x being set such that A13: x in dom f3 and A14: y = f3 . x by FUNCT_1:def_3; A15: x in dom (Sgm ((dom f1) \ X)) by A13, FUNCT_1:11; then (Sgm ((dom f1) \ X)) . x in rng (Sgm ((dom f1) \ X)) by FUNCT_1:3; then (Sgm ((dom f1) \ X)) . x in (dom f1) \ X by A7, FINSEQ_1:def_13; then f1 . ((Sgm ((dom f1) \ X)) . 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; ::_thesis: verum end; assume A16: y = 0 ; ::_thesis: y in rng f3 x in rng (Sgm ((dom f1) \ X)) by A7, A12, FINSEQ_1:def_13; then consider x9 being set such that A17: x9 in dom (Sgm ((dom f1) \ X)) and A18: x = (Sgm ((dom f1) \ X)) . x9 by FUNCT_1:def_3; f1 . x in {0} by A9, A12, FUNCT_1:def_7; then f1 . ((Sgm ((dom f1) \ X)) . 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; ::_thesis: verum 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 = f3 as FinSequence of NAT ; X \/ ((dom f1) \ X) = 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; ::_thesis: verum end; end; end; theorem Th12: :: NAT_5:12 for f2, f1 being FinSequence of REAL st f2 = f1 - {0} holds Sum f1 = Sum f2 proof let f2, f1 be FinSequence of REAL ; ::_thesis: ( f2 = f1 - {0} implies Sum f1 = Sum f2 ) A1: (dom f1) \ (f1 " {0}) c= dom f1 by XBOOLE_1:36; assume f2 = f1 - {0} ; ::_thesis: Sum f1 = Sum f2 hence Sum f1 = Sum f2 by A1, Th11; ::_thesis: verum end; theorem Th13: :: NAT_5:13 for f being FinSequence of NAT holds f is FinSequence of REAL proof let f be FinSequence of NAT ; ::_thesis: f is FinSequence of REAL for n being Nat st n in dom f holds f . n in REAL ; hence f is FinSequence of REAL by FINSEQ_2:12; ::_thesis: verum end; theorem Th14: :: NAT_5:14 for n, m, n1, m1 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n,m are_relative_prime holds n1,m1 are_relative_prime proof let n, m, n1, m1 be Nat; ::_thesis: ( n1 in NatDivisors n & m1 in NatDivisors m & n,m are_relative_prime implies n1,m1 are_relative_prime ) A1: n1 gcd m1 divides m1 by INT_2:def_2; assume n1 in NatDivisors n ; ::_thesis: ( not m1 in NatDivisors m or not n,m are_relative_prime or n1,m1 are_relative_prime ) 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 ; ::_thesis: ( not n,m are_relative_prime or n1,m1 are_relative_prime ) 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_relative_prime ; ::_thesis: n1,m1 are_relative_prime assume not n1,m1 are_relative_prime ; ::_thesis: contradiction 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, INT_2:27; then n gcd m <> 1 by A8, A6, XXREAL_0:1; hence contradiction by A7, INT_2:def_3; ::_thesis: verum end; theorem Th15: :: NAT_5:15 for n, m, n1, m1, n2, m2 being Nat st 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 holds ( n1 = n2 & m1 = m2 ) proof let n, m, n1, m1, n2, m2 be Nat; ::_thesis: ( 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 ) ) assume A1: n1 in NatDivisors n ; ::_thesis: ( not m1 in NatDivisors m or not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) ) then A2: n1 divides n by MOEBIUS1:39; assume A3: m1 in NatDivisors m ; ::_thesis: ( not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) ) then A4: m1 divides m by MOEBIUS1:39; assume A5: n2 in NatDivisors n ; ::_thesis: ( not m2 in NatDivisors m or not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) ) then A6: n2 divides n by MOEBIUS1:39; assume A7: m2 in NatDivisors m ; ::_thesis: ( not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) ) assume A8: n,m are_relative_prime ; ::_thesis: ( not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) ) assume A9: n1 * m1 = n2 * m2 ; ::_thesis: ( n1 = n2 & m1 = m2 ) A10: m2 divides m by A7, MOEBIUS1:39; A11: now__::_thesis:_not_n1_<>_n2 reconsider m19 = m1, m29 = m2 as non empty Nat by A3, A7, MOEBIUS1:39; A12: n gcd m > 0 by A8, INT_2:def_3; reconsider n19 = n1, n29 = n2 as non empty Nat by A1, A5, MOEBIUS1:39; assume n1 <> n2 ; ::_thesis: contradiction then consider p being Element of NAT such that A13: p is prime and A14: p |-count n19 <> p |-count n29 by NAT_4:21; reconsider p = 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; ::_thesis: verum end; A17: 0 < n2 by A5, MOEBIUS1:39; assume ( not n1 = n2 or not m1 = m2 ) ; ::_thesis: contradiction hence contradiction by A17, A9, A11, XCMPLX_1:5; ::_thesis: verum end; theorem Th16: :: NAT_5:16 for n0, m0 being non zero Nat for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds n1 * m1 in NatDivisors (n0 * m0) proof let n0, m0 be non zero Nat; ::_thesis: for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds n1 * m1 in NatDivisors (n0 * m0) let n1, m1 be Nat; ::_thesis: ( n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1 * m1 in NatDivisors (n0 * m0) ) reconsider b = n0 * m0 as non empty Nat ; assume A1: n1 in NatDivisors n0 ; ::_thesis: ( not m1 in NatDivisors m0 or n1 * m1 in NatDivisors (n0 * m0) ) then A2: 0 < n1 by MOEBIUS1:39; A3: n1 divides n0 by A1, MOEBIUS1:39; assume A4: m1 in NatDivisors m0 ; ::_thesis: n1 * m1 in NatDivisors (n0 * m0) then A5: 0 < m1 by MOEBIUS1:39; then reconsider a = n1 * m1 as non empty Nat by A2; A6: m1 divides m0 by A4, MOEBIUS1:39; for p being Element of NAT st p is prime holds p |-count a <= p |-count b proof reconsider n19 = n1, m19 = m1 as non empty Nat by A1, A4, MOEBIUS1:39; let p be Element of NAT ; ::_thesis: ( p is prime implies p |-count a <= p |-count b ) assume p is prime ; ::_thesis: p |-count a <= p |-count b then reconsider p9 = p as Prime ; A7: ( 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 A7, XREAL_1:7; ::_thesis: verum 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; ::_thesis: verum end; theorem Th17: :: NAT_5:17 for k being Nat for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) proof let k be Nat; ::_thesis: for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) let n0, m0 be non zero Nat; ::_thesis: ( n0,m0 are_relative_prime implies k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) ) assume A1: n0,m0 are_relative_prime ; ::_thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) percases ( k = 0 or k <> 0 ) ; supposeA2: k = 0 ; ::_thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) hence k gcd (n0 * m0) = abs (n0 * m0) by WSIERP_1:8 .= (abs n0) * (abs m0) by COMPLEX1:65 .= (k gcd n0) * (abs m0) by A2, WSIERP_1:8 .= (k gcd n0) * (k gcd m0) by A2, WSIERP_1:8 ; ::_thesis: verum end; suppose k <> 0 ; ::_thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) then reconsider k9 = k as non zero Nat ; reconsider a = k gcd (n0 * m0) as non empty Nat by INT_2:5; reconsider b1 = k gcd n0, b2 = k gcd 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 ; for p being Element of NAT st p is prime holds p |-count a = p |-count b proof let p be Element of NAT ; ::_thesis: ( p is prime implies p |-count a = p |-count b ) assume p is prime ; ::_thesis: p |-count a = p |-count b 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 ; percases ( p9 |-count n0 = 0 or p9 |-count m0 = 0 ) by A4, XXREAL_0:15; supposeA6: p9 |-count n0 = 0 ; ::_thesis: p |-count a = p |-count b 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; ::_thesis: verum end; supposeA7: p9 |-count m0 = 0 ; ::_thesis: p |-count a = p |-count b 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; ::_thesis: verum end; end; end; hence k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) by NAT_4:21; ::_thesis: verum end; end; end; theorem Th18: :: NAT_5:18 for k being Nat for n0, m0 being non zero Nat st n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) holds ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) proof let k be Nat; ::_thesis: for n0, m0 being non zero Nat st n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) holds ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) let n0, m0 be non zero Nat; ::_thesis: ( n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) implies ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) ) assume A1: n0,m0 are_relative_prime ; ::_thesis: ( not k in NatDivisors (n0 * m0) or ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) ) set m1 = k gcd m0; set n1 = k gcd n0; assume A2: k in NatDivisors (n0 * m0) ; ::_thesis: ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) take k gcd n0 ; ::_thesis: ex m1 being Nat st ( k gcd n0 in NatDivisors n0 & m1 in NatDivisors m0 & k = (k gcd n0) * m1 ) take k gcd m0 ; ::_thesis: ( k gcd n0 in NatDivisors n0 & k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) ) ( k gcd n0 divides n0 & k gcd n0 > 0 ) by NAT_D:def_5, NEWTON:58; hence k gcd n0 in NatDivisors n0 ; ::_thesis: ( k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) ) ( k gcd m0 divides m0 & k gcd m0 > 0 ) by NAT_D:def_5, NEWTON:58; hence k gcd m0 in NatDivisors m0 ; ::_thesis: k = (k gcd n0) * (k gcd m0) k divides n0 * m0 by A2, MOEBIUS1:39; hence k = k gcd (n0 * m0) by NEWTON:49 .= (k gcd n0) * (k gcd m0) by A1, Th17 ; ::_thesis: verum end; theorem Th19: :: NAT_5:19 for p, n being Nat st p is prime holds NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } proof let p, n be Nat; ::_thesis: ( p is prime implies NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } ) assume A1: p is prime ; ::_thesis: NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } 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 ; ::_thesis: ( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } ) hereby ::_thesis: ( x in { (p |^ k) where k is Element of NAT : k <= n } implies x in NatDivisors (p |^ n) ) assume A2: x in NatDivisors (p |^ n) ; ::_thesis: x in { (p |^ k) where k is Element of NAT : k <= n } then reconsider x9 = x as Nat ; x9 divides p |^ n by A2, MOEBIUS1:39; then ex t being 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 } ; ::_thesis: verum end; assume x in { (p |^ k) where k is Element of NAT : k <= n } ; ::_thesis: x in NatDivisors (p |^ n) then A3: ex t being 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; ::_thesis: verum end; hence NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } by TARSKI:1; ::_thesis: verum end; theorem Th20: :: NAT_5:20 for l, p, n1, n2 being Nat st 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime holds n1 = n2 proof let l, p, n1, n2 be Nat; ::_thesis: ( 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime implies n1 = n2 ) assume that A1: ( l <> 0 & p > l ) and A2: p > n1 and A3: p > n2 ; ::_thesis: ( not (l * n1) mod p = (l * n2) mod p or not p is prime or n1 = n2 ) assume A4: (l * n1) mod p = (l * n2) mod p ; ::_thesis: ( not p is prime or n1 = n2 ) assume A5: p is prime ; ::_thesis: n1 = n2 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; percases ( p divides l or p divides n1 - n2 ) by A5, A6, INT_5:7; suppose p divides l ; ::_thesis: n1 = n2 hence n1 = n2 by A1, NAT_D:7; ::_thesis: verum end; supposeA7: p divides n1 - n2 ; ::_thesis: n1 = n2 percases ( n1 - n2 > 0 or n1 - n2 = 0 or n1 - n2 < 0 ) ; supposeA8: n1 - n2 > 0 ; ::_thesis: n1 = n2 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 n1 = n2 ; ::_thesis: verum end; suppose n1 - n2 = 0 ; ::_thesis: n1 = n2 hence n1 = n2 ; ::_thesis: verum end; suppose n1 - n2 < 0 ; ::_thesis: n1 = n2 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 n1 = n2 ; ::_thesis: verum end; end; end; end; end; theorem :: NAT_5:21 for p being Nat for n0, m0 being non zero Nat st p is prime holds p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by Lm1; Lm4: for k, m being Nat holds ( k < m iff k <= m - 1 ) proof let k, m be Nat; ::_thesis: ( k < m iff k <= m - 1 ) A1: now__::_thesis:_(_k_<=_m_-_1_implies_k_<_m_) assume k <= m - 1 ; ::_thesis: k < m then A2: k + 1 <= m by XREAL_1:19; k < k + 1 by XREAL_1:29; hence k < m by A2, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_k_<_m_implies_k_<=_m_-_1_) assume k < m ; ::_thesis: k <= m - 1 then k + 1 <= m by INT_1:7; hence k <= m - 1 by XREAL_1:19; ::_thesis: verum end; hence ( k < m iff k <= m - 1 ) by A1; ::_thesis: verum end; Lm5: for a being Element of NAT for fs being FinSequence st a in dom fs holds ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) proof let a be Element of NAT ; ::_thesis: for fs being FinSequence st a in dom fs holds ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) let fs be FinSequence; ::_thesis: ( a in dom fs implies ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) ) assume A1: a in dom fs ; ::_thesis: ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) 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 being 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 being FinSequence, v being set 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 ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) by A3, A4, A5, A6; ::_thesis: verum end; Lm6: for a being Element of NAT for fs, fs1, fs2 being FinSequence for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 proof let a be Element of NAT ; ::_thesis: for fs, fs1, fs2 being FinSequence for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 let fs, fs1, fs2 be FinSequence; ::_thesis: for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 let v be set ; ::_thesis: ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 implies Del (fs,a) = fs1 ^ fs2 ) assume that A1: a in dom fs and A2: fs = (fs1 ^ <*v*>) ^ fs2 and A3: len fs1 = a - 1 ; ::_thesis: Del (fs,a) = fs1 ^ fs2 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__::_thesis:_for_e_being_Nat_st_1_<=_e_&_e_<=_len_(Del_(fs,a))_holds_ (fs1_^_fs2)_._e_=_(Del_(fs,a))_._e let e be Nat; ::_thesis: ( 1 <= e & e <= len (Del (fs,a)) implies (fs1 ^ fs2) . e = (Del (fs,a)) . e ) assume that A9: 1 <= e and A10: e <= len (Del (fs,a)) ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e now__::_thesis:_(fs1_^_fs2)_._e_=_(Del_(fs,a))_._e percases ( e < a or e >= a ) ; supposeA11: e < a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e then e <= a - 1 by Lm4; then A12: e in dom fs1 by A3, A9, FINSEQ_3:25; hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def_7 .= fs . e by A7, A12, FINSEQ_1:def_7 .= (Del (fs,a)) . e by A1, A11, WSIERP_1:def_1 ; ::_thesis: verum end; supposeA13: e >= a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e 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 + 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 ; ::_thesis: verum end; end; end; hence (fs1 ^ fs2) . e = (Del (fs,a)) . e ; ::_thesis: verum end; hence Del (fs,a) = fs1 ^ fs2 by A5, FINSEQ_1:14; ::_thesis: verum end; Lm7: for fs being FinSequence st 1 <= len fs holds ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) proof let fs be FinSequence; ::_thesis: ( 1 <= len fs implies ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) ) 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 ; ::_thesis: ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (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 (<*(fs . 1)*> ^ (Del (fs,1))) by FINSEQ_1:22 ; for b being Nat st 1 <= b & b <= len fs holds fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b proof let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b ) assume that A6: 1 <= b and A7: b <= len fs ; ::_thesis: fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b now__::_thesis:_(<*(fs_._1)*>_^_(Del_(fs,1)))_._b_=_fs_._b percases ( b = 1 or b > 1 ) by A6, XXREAL_0:1; supposeA8: b = 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b 1 in dom <*(fs . 1)*> by A1, FINSEQ_3:25; hence (<*(fs . 1)*> ^ (Del (fs,1))) . b = <*(fs . 1)*> . 1 by A8, FINSEQ_1:def_7 .= fs . b by A8, FINSEQ_1:40 ; ::_thesis: verum end; supposeA9: b > 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b 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 (<*(fs . 1)*> ^ (Del (fs,1))) . 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 ; ::_thesis: verum end; end; end; hence fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b ; ::_thesis: verum end; hence <*(fs . 1)*> ^ (Del (fs,1)) = fs by A5, FINSEQ_1:14; ::_thesis: fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> 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 ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) 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 being Nat st 1 <= b & b <= len fs holds fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b proof let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b ) assume that A15: 1 <= b and A16: b <= len fs ; ::_thesis: fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b now__::_thesis:_((Del_(fs,(len_fs)))_^_<*(fs_._(len_fs))*>)_._b_=_fs_._b percases ( b = len fs or b < len fs ) by A16, XXREAL_0:1; supposeA17: b = len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b reconsider e = b - (b - 1) as Element of NAT ; thus ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = <*(fs . (len fs))*> . e by A13, A12, A17, FINSEQ_1:24, XREAL_1:146 .= fs . b by A17, FINSEQ_1:40 ; ::_thesis: verum end; supposeA18: b < len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b then b + 1 <= len fs by NAT_1:13; then b <= len (Del (fs,(len fs))) by A14, XREAL_1:19; then b in dom (Del (fs,(len fs))) by A15, FINSEQ_3:25; hence ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = (Del (fs,(len fs))) . b by FINSEQ_1:def_7 .= fs . b by A3, A18, WSIERP_1:def_1 ; ::_thesis: verum end; end; end; hence fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b ; ::_thesis: verum end; hence (Del (fs,(len fs))) ^ <*(fs . (len fs))*> = fs by A12, FINSEQ_1:14; ::_thesis: verum end; Lm8: for a being Element of NAT for ft being FinSequence of REAL st a in dom ft holds (Product (Del (ft,a))) * (ft . a) = Product ft proof let a be Element of NAT ; ::_thesis: for ft being FinSequence of REAL st a in dom ft holds (Product (Del (ft,a))) * (ft . a) = Product ft let ft be FinSequence of REAL ; ::_thesis: ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) defpred S1[ Nat] means ( $1 in dom ft implies (ft . $1) * (Product (Del (ft,$1))) = Product ft ); A1: for a being Element of NAT st S1[a] holds S1[a + 1] proof let a be Element of NAT ; ::_thesis: ( S1[a] implies S1[a + 1] ) assume S1[a] ; ::_thesis: S1[a + 1] now__::_thesis:_S1[a_+_1] percases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ; supposeA2: a = 0 ; ::_thesis: S1[a + 1] thus S1[a + 1] ::_thesis: verum proof assume a + 1 in dom ft ; ::_thesis: (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft then a + 1 <= len ft by FINSEQ_3:25; then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm7; then Product ft = (Product <*(ft . 1)*>) * (Product (Del (ft,1))) by RVSUM_1:97 .= (ft . 1) * (Product (Del (ft,1))) by RVSUM_1:95 ; hence (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft by A2; ::_thesis: verum end; end; suppose ( a > 0 & a < len ft ) ; ::_thesis: S1[a + 1] then ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13; then A3: a + 1 in dom ft by FINSEQ_3:25; then consider fs1, fs2 being 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 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36; reconsider fs1 = 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 S1[a + 1] by A6, RVSUM_1:97; ::_thesis: verum end; suppose a >= len ft ; ::_thesis: S1[a + 1] then len ft < a + 1 by NAT_1:13; hence S1[a + 1] by FINSEQ_3:25; ::_thesis: verum end; end; end; hence S1[a + 1] ; ::_thesis: verum end; A7: S1[ 0 ] by FINSEQ_3:25; for a being Element of NAT holds S1[a] from NAT_1:sch_1(A7, A1); hence ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; ::_thesis: verum end; Lm9: for n being Nat st n + 2 is prime holds for l being Nat st l in Seg n & l <> 1 holds ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) proof let n be Nat; ::_thesis: ( n + 2 is prime implies for l being Nat st l in Seg n & l <> 1 holds ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume A1: n + 2 is prime ; ::_thesis: for l being Nat st l in Seg n & l <> 1 holds ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) then A2: 1 < n9 + 2 by INT_2:def_4; let l be Nat; ::_thesis: ( l in Seg n & l <> 1 implies ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) reconsider l9 = l as Element of NAT by ORDINAL1:def_12; assume A3: l in Seg n ; ::_thesis: ( not l <> 1 or ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) then A4: l9 <> 0 by FINSEQ_1:1; assume A5: l <> 1 ; ::_thesis: ex k being Nat st ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) A6: l <= n by A3, FINSEQ_1:1; then A7: l < n + 1 by NAT_1:13; A8: 1 + n < 2 + n by XREAL_1:6; then l9 < n9 + 2 by A7, XXREAL_0:2; then consider k being Element of NAT such that A9: (k * l9) mod (n9 + 2) = 1 and A10: k < n9 + 2 by A1, A2, A4, IDEA_1:1; take k ; ::_thesis: ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) k <> 0 by A9, NAT_D:26; then A11: k >= 0 + 1 by NAT_1:13; A12: 1 <= l by A3, FINSEQ_1:1; then A13: 1 - 1 <= l - 1 by XREAL_1:9; A14: l < n + 2 by A7, A8, XXREAL_0:2; then A15: n + 2 > 1 by A12, XXREAL_0:2; A16: l + 1 < (n + 1) + 1 by A7, XREAL_1:6; A17: k <> n + 1 proof assume k = n + 1 ; ::_thesis: contradiction 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 ; ::_thesis: verum 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; ::_thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) 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 ::_thesis: ( k <> l & (l * k) mod (n + 2) = 1 ) proof assume k = 1 ; ::_thesis: contradiction 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; ::_thesis: verum end; thus k <> l ::_thesis: (l * k) mod (n + 2) = 1 proof assume A20: k = l ; ::_thesis: contradiction 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; percases ( n + 2 divides l + 1 or n + 2 divides l - 1 ) by A1, A21, INT_5:7; suppose n + 2 divides l + 1 ; ::_thesis: contradiction then n + 2 <= l + 1 by NAT_D:7; then (n + 2) - 1 <= (l + 1) - 1 by XREAL_1:9; hence contradiction by A7; ::_thesis: verum end; suppose n + 2 divides l - 1 ; ::_thesis: contradiction then A22: n + 2 divides l -' 1 by A13, XREAL_0:def_2; percases ( l = 1 or l <> 1 ) ; suppose l = 1 ; ::_thesis: contradiction hence contradiction by A19, A20; ::_thesis: verum end; suppose l <> 1 ; ::_thesis: contradiction 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 ; ::_thesis: verum end; end; end; end; end; thus (l * k) mod (n + 2) = 1 by A9; ::_thesis: verum end; Lm10: for n being Nat for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds (Product f) mod (n + 2) = 1 proof let n be Nat; ::_thesis: for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds (Product f) mod (n + 2) = 1 defpred S1[ 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 being Nat st l in rng f & l <> 1 holds ex k being Nat 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 ; ::_thesis: ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) set n9 = len f; A1: for k9 being Nat st ( for n9 being Nat st n9 < k9 holds S1[n9] ) holds S1[k9] proof let k9 be Nat; ::_thesis: ( ( for n9 being Nat st n9 < k9 holds S1[n9] ) implies S1[k9] ) assume A2: for n9 being Nat st n9 < k9 holds S1[n9] ; ::_thesis: S1[k9] thus S1[k9] ::_thesis: verum proof let f be FinSequence of NAT ; ::_thesis: ( len f = k9 & n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) assume A3: len f = k9 ; ::_thesis: ( not n + 2 is prime or not rng f c= Seg n or not f is one-to-one or ex l being Nat st ( l in rng f & l <> 1 & ( for k being Nat holds ( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 ) assume A4: n + 2 is prime ; ::_thesis: ( not rng f c= Seg n or not f is one-to-one or ex l being Nat st ( l in rng f & l <> 1 & ( for k being Nat holds ( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 ) assume A5: rng f c= Seg n ; ::_thesis: ( not f is one-to-one or ex l being Nat st ( l in rng f & l <> 1 & ( for k being Nat holds ( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 ) assume A6: f is one-to-one ; ::_thesis: ( ex l being Nat st ( l in rng f & l <> 1 & ( for k being Nat holds ( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 ) assume A7: for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ; ::_thesis: (Product f) mod (n + 2) = 1 percases ( k9 = 0 or k9 <> 0 ) ; supposeA8: k9 = 0 ; ::_thesis: (Product f) mod (n + 2) = 1 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; ::_thesis: verum end; supposeA10: k9 <> 0 ; ::_thesis: (Product f) mod (n + 2) = 1 reconsider f9 = f as FinSequence of REAL by FINSEQ_2:24; dom f <> {} by A3, A10, CARD_1:27, RELAT_1:41; then consider x1 being set such that A11: x1 in dom f by XBOOLE_0:def_1; reconsider x1 = x1 as Element of NAT by A11; A12: ex m being 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, XBOOLE_1:1; set n19 = len (Del (f,x1)); A16: 0 + (len (Del (f,x1))) < 1 + (len (Del (f,x1))) by XREAL_1:6; A17: Del (f,x1) is one-to-one by A6, Th6; percases ( f9 . x1 = 1 or f9 . x1 <> 1 ) ; supposeA18: f9 . x1 = 1 ; ::_thesis: (Product f) mod (n + 2) = 1 for l being Nat st l in rng (Del (f,x1)) & l <> 1 holds ex k being Nat st ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) proof let l be Nat; ::_thesis: ( l in rng (Del (f,x1)) & l <> 1 implies ex k being Nat st ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) assume A19: l in rng (Del (f,x1)) ; ::_thesis: ( not l <> 1 or ex k being Nat st ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) assume l <> 1 ; ::_thesis: ex k being Nat st ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) then consider k being Nat 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 ; ::_thesis: ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) thus k in rng (Del (f,x1)) by A18, A20, A21, Th8; ::_thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) thus ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) by A21, A22; ::_thesis: verum end; hence (Product f) mod (n + 2) = 1 by A2, A3, A4, A13, A15, A17, A12, A16, A18; ::_thesis: verum end; supposeA23: f9 . x1 <> 1 ; ::_thesis: (Product f) mod (n + 2) = 1 set f99 = Del (f,x1); set l = f . x1; A24: f . x1 in rng f by A11, FUNCT_1:3; then consider k being Nat such that A25: k in rng f and k <> 1 and A26: k <> f . x1 and A27: ((f . x1) * k) mod (n + 2) = 1 by A7, A23; k in rng (Del (f,x1)) by A25, A26, Th8; then consider x2 being set such that A28: x2 in dom (Del (f,x1)) and A29: k = (Del (f,x1)) . x2 by FUNCT_1:def_3; reconsider x2 = x2 as Element of NAT by A28; A30: rng (Del ((Del (f,x1)),x2)) c= rng (Del (f9,x1)) by FINSEQ_3:106; then A31: rng (Del ((Del (f,x1)),x2)) c= Seg n by A15, XBOOLE_1:1; A32: for l being Nat st l in rng (Del ((Del (f,x1)),x2)) & l <> 1 holds ex k being Nat st ( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) proof A33: 1 <= f . x1 by A5, A24, FINSEQ_1:1; A34: 0 + n < 2 + n by XREAL_1:6; f . x1 <= n by A5, A24, FINSEQ_1:1; then A35: n + 2 > f . x1 by A34, XXREAL_0:2; k <= n by A5, A25, FINSEQ_1:1; then A36: n + 2 > k by A34, XXREAL_0:2; let l9 be Nat; ::_thesis: ( l9 in rng (Del ((Del (f,x1)),x2)) & l9 <> 1 implies ex k being Nat st ( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) ) A37: 0 + n < 2 + n by XREAL_1:6; assume A38: l9 in rng (Del ((Del (f,x1)),x2)) ; ::_thesis: ( not l9 <> 1 or ex k being Nat st ( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) ) then A39: l9 in rng (Del (f9,x1)) by A30; then l9 in rng f by A14; then A40: l9 <= n by A5, FINSEQ_1:1; assume l9 <> 1 ; ::_thesis: ex k being Nat st ( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) then consider k9 being Nat such that A41: k9 in rng f and A42: ( k9 <> 1 & k9 <> l9 ) and A43: (l9 * k9) mod (n + 2) = 1 by A7, A14, A39; take k9 ; ::_thesis: ( k9 in rng (Del ((Del (f,x1)),x2)) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 ) A44: 1 <= k by A5, A25, FINSEQ_1:1; thus k9 in rng (Del ((Del (f,x1)),x2)) ::_thesis: ( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 ) proof assume A45: not k9 in rng (Del ((Del (f,x1)),x2)) ; ::_thesis: contradiction percases ( k9 in rng (Del (f,x1)) or not k9 in rng (Del (f,x1)) ) ; supposeA46: k9 in rng (Del (f,x1)) ; ::_thesis: contradiction A47: l9 < n + 2 by A40, A37, XXREAL_0:2; (k * (f . x1)) mod (n + 2) = (k * l9) mod (n + 2) by A27, A29, A43, A45, A46, Th8; then l9 = f . x1 by A4, A44, A36, A35, A47, Th20; hence contradiction by A6, A11, A30, A38, Th7; ::_thesis: verum end; supposeA48: not k9 in rng (Del (f,x1)) ; ::_thesis: contradiction A49: l9 < n + 2 by A40, A37, XXREAL_0:2; ((f . x1) * k) mod (n + 2) = ((f . x1) * l9) mod (n + 2) by A27, A41, A43, A48, Th8; then (Del (f,x1)) . x2 in rng (Del ((Del (f,x1)),x2)) by A4, A29, A38, A33, A36, A35, A49, Th20; hence contradiction by A6, A28, Th6, Th7; ::_thesis: verum end; end; end; thus ( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 ) by A42, A43; ::_thesis: verum end; set n299 = len (Del ((Del (f,x1)),x2)); A50: 0 + (len (Del ((Del (f,x1)),x2))) < 1 + (len (Del ((Del (f,x1)),x2))) by XREAL_1:6; ex m being Nat st ( len (Del (f9,x1)) = m + 1 & len (Del ((Del (f,x1)),x2)) = m ) by A28, FINSEQ_3:104; then A51: len (Del ((Del (f,x1)),x2)) < k9 by A3, A12, A16, A50, XXREAL_0:2; A52: Del ((Del (f,x1)),x2) is one-to-one by A17, Th6; (Product (Del ((Del (f,x1)),x2))) * ((Del (f,x1)) . x2) = Product (Del (f,x1)) by A28, Lm8; then (Product (Del ((Del (f,x1)),x2))) * (k * (f . x1)) = Product f by A13, A29; hence (Product f) mod (n + 2) = ((Product (Del ((Del (f,x1)),x2))) * ((k * (f . x1)) mod (n + 2))) mod (n + 2) by EULER_2:7 .= 1 by A2, A4, A27, A31, A52, A32, A51 ; ::_thesis: verum end; end; end; end; end; end; for n9 being Nat holds S1[n9] from NAT_1:sch_4(A1); then S1[ len f] ; hence ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds ex k being Nat st ( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) ; ::_thesis: verum end; begin theorem :: NAT_5:22 for n being Nat holds ( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) ) proof let n be Nat; ::_thesis: ( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) ) thus ( n is prime implies ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) ) ::_thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 implies n is prime ) proof assume A1: n is prime ; ::_thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) percases ( n < 2 or n >= 2 ) ; suppose n < 2 ; ::_thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) then n < 1 + 1 ; then n <= 1 by NAT_1:13; hence ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) by A1, INT_2:def_4; ::_thesis: verum end; suppose n >= 2 ; ::_thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) 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 + (n -' 2) > 1 + (n -' 2) by XREAL_1:6; set f = Sgm (Seg (n -' 2)); A5: (n * 1) mod n = 0 by NAT_D:13; A6: n -' 2 = n - 2 by A2, XREAL_0:def_2; then A7: (n -' 2) + 1 = n - 1 .= n -' 1 by A3, XREAL_0:def_2 ; A8: for l9 being Nat st l9 in rng (Sgm (Seg (n -' 2))) & l9 <> 1 holds ex k9 being Nat st ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) proof let l9 be Nat; ::_thesis: ( l9 in rng (Sgm (Seg (n -' 2))) & l9 <> 1 implies ex k9 being Nat st ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) ) assume l9 in rng (Sgm (Seg (n -' 2))) ; ::_thesis: ( not l9 <> 1 or ex k9 being Nat st ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) ) then A9: l9 in Seg (n -' 2) by FINSEQ_1:def_13; assume l9 <> 1 ; ::_thesis: ex k9 being Nat st ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) then consider k9 being Nat such that A10: ( k9 in Seg (n -' 2) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) by A1, A6, A9, Lm9; take k9 ; ::_thesis: ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) thus ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) by A10, FINSEQ_1:def_13; ::_thesis: verum end; ( (n -' 2) ! = Product (Sgm (Seg (n -' 2))) & rng (Sgm (Seg (n -' 2))) c= Seg (n -' 2) ) by FINSEQ_1:def_13, FINSEQ_3:48; then A11: ((n -' 2) !) mod ((n -' 2) + 2) = 1 by A1, A6, A8, Lm10, FINSEQ_3:92; (((n -' 2) + 1) !) mod ((n -' 2) + 2) = (((n -' 2) + 1) * ((n -' 2) !)) mod ((n -' 2) + 2) by NEWTON:15 .= (((n -' 2) + 1) * 1) mod ((n -' 2) + 2) by A11, EULER_2:7 .= (n -' 2) + 1 by A4, NAT_D:24 ; then (((((n -' 2) + 1) !) mod ((n -' 2) + 2)) + 1) mod ((n -' 2) + 2) = 0 by A6, A5; hence ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) by A1, A6, A7, INT_2:def_4, NAT_D:22; ::_thesis: verum end; end; end; thus ( (((n -' 1) !) + 1) mod n = 0 & n > 1 implies n is prime ) ::_thesis: verum proof assume that A12: (((n -' 1) !) + 1) mod n = 0 and A13: n > 1 ; ::_thesis: n is prime n >= 1 + 1 by A13, NAT_1:13; then consider k being Element of NAT such that A14: k is prime and A15: k divides n by INT_2:31; consider i being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; begin theorem :: NAT_5:23 for p being Nat st p is prime & p mod 4 = 1 holds ex n, m being Nat st p = (n ^2) + (m ^2) proof let p be Nat; ::_thesis: ( p is prime & p mod 4 = 1 implies ex n, m being Nat st p = (n ^2) + (m ^2) ) 0 <= sqrt p by SQUARE_1:def_2; then reconsider p9 = [\(sqrt p)/] as Element of NAT by INT_1:3, INT_1:54; reconsider p99 = p9 + 1 as Element of NAT ; set X = Segm p99; A1: card (Segm p99) = card p99 by CARD_1:def_6 .= 1 + [\(sqrt p)/] by CARD_1:def_2 ; then A2: (sqrt p) * (card (Segm p99)) < (card (Segm p99)) * (card (Segm p99)) by INT_1:29, XREAL_1:68; assume A3: p is prime ; ::_thesis: ( not p mod 4 = 1 or ex n, m being Nat st p = (n ^2) + (m ^2) ) then p > 1 by INT_2:def_4; then p + 1 > 1 + 1 by XREAL_1:6; then A4: p >= 2 by NAT_1:13; A5: p9 ^2 <> p proof assume p9 ^2 = p ; ::_thesis: contradiction then reconsider p99 = sqrt p as Element of NAT by SQUARE_1:def_2; p99 ^2 = p by SQUARE_1:def_2; then A6: p99 * p99 = p by SQUARE_1:def_1; then A7: p99 divides p by INT_1:def_3; percases ( p99 = 1 or p99 = p ) by A3, A7, INT_2:def_4; suppose p99 = 1 ; ::_thesis: contradiction hence contradiction by A3, A6, INT_2:def_4; ::_thesis: verum end; suppose p99 = p ; ::_thesis: contradiction then 1 = (p * p) / p by A3, A6, XCMPLX_1:60 .= p * (p / p) by XCMPLX_1:74 .= p * 1 by A3, XCMPLX_1:60 ; hence contradiction by A3, INT_2:def_4; ::_thesis: verum end; 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 A8: p9 ^2 < p by A5, XXREAL_0:1; assume A9: p mod 4 = 1 ; ::_thesis: ex n, m being Nat st p = (n ^2) + (m ^2) then p <> 2 by NAT_D:24; then p > 2 by A4, XXREAL_0:1; then - 1 is_quadratic_residue_mod p by A3, A9, INT_5:37; then consider s being Integer such that A10: ((s ^2) - (- 1)) mod p = 0 by INT_5:def_2; 0 < sqrt p by A3, SQUARE_1:25; then (sqrt p) * (sqrt p) < (card (Segm p99)) * (sqrt p) by A1, INT_1:29, XREAL_1:68; then (sqrt p) * (sqrt p) < (card (Segm p99)) * (card (Segm p99)) by A2, XXREAL_0:2; then sqrt (p * p) < (card (Segm p99)) * (card (Segm p99)) by SQUARE_1:29; then sqrt (p ^2) < (card (Segm p99)) * (card (Segm p99)) by SQUARE_1:def_1; then p < (card (Segm p99)) * (card (Segm p99)) by SQUARE_1:22; then A11: p < card [:(Segm p99),(Segm p99):] by CARD_2:46; for s being integer number ex x9, x99, y9, y99 being Nat st ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) proof set A = [:(Segm p99),(Segm p99):]; reconsider p9 = p as Element of NAT by ORDINAL1:def_12; let s be integer number ; ::_thesis: ex x9, x99, y9, y99 being Nat st ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) set B = Segm p9; defpred S1[ set , set ] means ex n1, n2, n3 being Element of NAT st ( $1 = [n1,n2] & $2 = n3 & (n1 - (s * n2)) mod p = n3 ); card (Segm p9) = card p9 by CARD_1:def_6 .= p by CARD_1:def_2 ; then A12: card (Segm p9) in card [:(Segm p99),(Segm p99):] by A11, NAT_1:44; A13: for x being set st x in [:(Segm p99),(Segm p99):] holds ex y being set st ( y in Segm p9 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [:(Segm p99),(Segm p99):] implies ex y being set st ( y in Segm p9 & S1[x,y] ) ) assume x in [:(Segm p99),(Segm p99):] ; ::_thesis: ex y being set st ( y in Segm p9 & S1[x,y] ) then consider n1, n2 being set such that A14: ( n1 in Segm p99 & n2 in Segm p99 ) and A15: x = [n1,n2] by ZFMISC_1:def_2; reconsider n1 = n1, n2 = n2 as Element of NAT by A14; set y = (n1 - (s * n2)) mod p; reconsider y = (n1 - (s * n2)) mod p as Element of NAT by INT_1:3, INT_1:57; take y ; ::_thesis: ( y in Segm p9 & S1[x,y] ) y < p by A3, INT_1:58; then y in p by NAT_1:44; hence y in Segm p9 by CARD_1:def_6; ::_thesis: S1[x,y] thus S1[x,y] by A15; ::_thesis: verum end; consider f being Function of [:(Segm p99),(Segm p99):],(Segm p9) such that A16: for x being set st x in [:(Segm p99),(Segm p99):] holds S1[x,f . x] from FUNCT_2:sch_1(A13); Segm p9 <> {} by A3, ALGSEQ_1:1; then consider x1, x2 being set such that A17: x1 in [:(Segm p99),(Segm p99):] and A18: x2 in [:(Segm p99),(Segm p99):] and A19: x1 <> x2 and A20: f . x1 = f . x2 by A12, FINSEQ_4:65; consider x9, y9 being set such that A21: ( x9 in Segm p99 & y9 in Segm p99 ) and A22: x1 = [x9,y9] by A17, ZFMISC_1:def_2; reconsider x9 = x9, y9 = y9 as Nat by A21; consider x99, y99 being set such that A23: ( x99 in Segm p99 & y99 in Segm p99 ) and A24: x2 = [x99,y99] by A18, ZFMISC_1:def_2; reconsider x99 = x99, y99 = y99 as Nat by A23; take x9 ; ::_thesis: ex x99, y9, y99 being Nat st ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) take x99 ; ::_thesis: ex y9, y99 being Nat st ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) take y9 ; ::_thesis: ex y99 being Nat st ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) take y99 ; ::_thesis: ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) thus ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 ) by A21, A23; ::_thesis: ( [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ) thus [x9,y9] <> [x99,y99] by A19, A22, A24; ::_thesis: (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p consider n11, n12, n13 being Element of NAT such that A25: x1 = [n11,n12] and A26: ( f . x1 = n13 & (n11 - (s * n12)) mod p = n13 ) by A16, A17; A27: ( n11 = x9 & n12 = y9 ) by A22, A25, XTUPLE_0:1; consider n21, n22, n23 being Element of NAT such that A28: x2 = [n21,n22] and A29: ( f . x2 = n23 & (n21 - (s * n22)) mod p = n23 ) by A16, A18; n21 = x99 by A24, A28, XTUPLE_0:1; hence (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p by A20, A24, A26, A28, A29, A27, XTUPLE_0:1; ::_thesis: verum end; then consider x9, x99, y9, y99 being Nat such that A30: x9 in Segm p99 and A31: x99 in Segm p99 and A32: y9 in Segm p99 and A33: y99 in Segm p99 and A34: [x9,y9] <> [x99,y99] and A35: (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ; set m9 = y9 - y99; A36: 0 = ((((s ^2) + 1) mod p) * (((y9 - y99) ^2) mod p)) mod p by A10, INT_4:12 .= (((s ^2) + 1) * ((y9 - y99) ^2)) mod p by NAT_D:67 .= (((s ^2) * ((y9 - y99) ^2)) + ((y9 - y99) ^2)) mod p .= (((s * (y9 - y99)) ^2) + ((y9 - y99) ^2)) mod p by SQUARE_1:9 ; set n9 = x9 - x99; A37: ((x9 - x99) + (s * (y9 - y99))) * ((x9 - x99) - (s * (y9 - y99))) = ((x9 - x99) to_power 2) - ((s * (y9 - y99)) to_power 2) by FIB_NUM3:7 .= ((x9 - x99) ^2) - ((s * (y9 - y99)) to_power 2) by POWER:46 .= ((x9 - x99) ^2) - ((s * (y9 - y99)) ^2) by POWER:46 ; ((x9 - (s * y9)) mod p) - ((x99 - (s * y99)) mod p) = 0 by A35; 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 = ((((x9 - x99) + (s * (y9 - y99))) mod p) * (((x9 - x99) - (s * (y9 - y99))) mod p)) mod p by INT_4:12 .= (((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) mod p by A37, NAT_D:67 ; then 0 = (((((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) mod p) + ((((s * (y9 - y99)) ^2) + ((y9 - y99) ^2)) mod p)) mod p by A36, INT_4:12 .= ((((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) + (((s * (y9 - y99)) ^2) + ((y9 - y99) ^2))) mod p by NAT_D:66 .= (((x9 - x99) ^2) + ((y9 - y99) ^2)) mod p ; then p divides ((x9 - x99) ^2) + ((y9 - y99) ^2) by A3, INT_1:62; then consider i being Integer such that A38: ((x9 - x99) ^2) + ((y9 - y99) ^2) = p * i by INT_1:def_3; A39: p * i = (|.(x9 - x99).| ^2) + ((y9 - y99) ^2) by A38, COMPLEX1:75 .= ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) by COMPLEX1:75 ; y9 in p99 by A32, CARD_1:def_6; then y9 < p99 by NAT_1:44; then A40: y9 <= p9 by NAT_1:13; x99 in p99 by A31, CARD_1:def_6; then x99 < p99 by NAT_1:44; then A41: x99 <= p9 by NAT_1:13; y99 in p99 by A33, CARD_1:def_6; then y99 < p99 by NAT_1:44; then A42: y99 <= p9 by NAT_1:13; x9 in p99 by A30, CARD_1:def_6; then x9 < p99 by NAT_1:44; then A43: x9 <= p9 by NAT_1:13; set m = abs (y9 - y99); A44: ( y9 in NAT & y99 in NAT ) by ORDINAL1:def_12; set n = abs (x9 - x99); ( x9 in NAT & x99 in NAT ) by ORDINAL1:def_12; then reconsider x9 = x9, x99 = x99, y9 = y9, y99 = y99 as Real by A44; abs (y9 - y99) <= p9 - 0 by A40, A42, JGRAPH_1:27; then (abs (y9 - y99)) ^2 <= p9 ^2 by SQUARE_1:15; then A45: (abs (y9 - y99)) ^2 < p by A8, XXREAL_0:2; abs (x9 - x99) <= p9 - 0 by A43, A41, JGRAPH_1:27; then (abs (x9 - x99)) ^2 <= p9 ^2 by SQUARE_1:15; then (abs (x9 - x99)) ^2 < p by A8, XXREAL_0:2; then ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) < p + p by A45, XREAL_1:8; then (i * p) / p < (2 * p) / p by A3, A39, 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 A3, XCMPLX_1:60; then i * 1 < 2 by A3, XCMPLX_1:60; then i + 1 <= 2 by INT_1:7; then A46: (i + 1) - 1 <= 2 - 1 by XREAL_1:9; take abs (x9 - x99) ; ::_thesis: ex m being Nat st p = ((abs (x9 - x99)) ^2) + (m ^2) take abs (y9 - y99) ; ::_thesis: p = ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) <> 0 proof assume A47: ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) = 0 ; ::_thesis: contradiction then (abs (y9 - y99)) ^2 = 0 ; then (abs (y9 - y99)) * (abs (y9 - y99)) = 0 by SQUARE_1:def_1; then abs (y9 - y99) = 0 ; then A48: y9 - y99 = 0 by ABSVALUE:2; (abs (x9 - x99)) ^2 = 0 by A47; then (abs (x9 - x99)) * (abs (x9 - x99)) = 0 by SQUARE_1:def_1; then abs (x9 - x99) = 0 ; then x9 - x99 = 0 by ABSVALUE:2; hence contradiction by A34, A48; ::_thesis: verum end; then i > 0 by A39; then i >= 0 + 1 by INT_1:7; then i = 1 by A46, XXREAL_0:1; hence p = ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) by A39; ::_thesis: verum end; begin definition let I be set ; let f be Function of I,NAT; let J be finite Subset of I; :: original: | redefine funcf | J -> bag of J; correctness coherence f | J is bag of J; ; 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 for number ; correctness coherence for b1 being number st b1 = Sum (f | J) holds b1 is natural ; proof set b = f | J; consider f9 being FinSequence of REAL such that A1: Sum (f | J) = Sum f9 and A2: f9 = (f | J) * (canFS (support (f | J))) by UPROOTS:def_3; rng f9 c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f9 or y in NAT ) assume y in rng f9 ; ::_thesis: y in NAT hence y in NAT by A2, ORDINAL1:def_12; ::_thesis: verum end; then reconsider f9 = f9 as FinSequence of NAT by FINSEQ_1:def_4; Sum f9 is Element of NAT ; hence for b1 being number st b1 = Sum (f | J) holds b1 is natural by A1; ::_thesis: verum end; end; theorem Th24: :: NAT_5:24 for f being Function of NAT,NAT for F being Function of NAT,REAL for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) proof let f be Function of NAT,NAT; ::_thesis: for F being Function of NAT,REAL for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) let F be Function of NAT,REAL; ::_thesis: for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) let J be finite Subset of NAT; ::_thesis: ( f = F & ex k being Nat st J c= Seg k implies Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) ) assume A1: f = F ; ::_thesis: ( for k being Nat holds not J c= Seg k or Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) ) reconsider J9 = J as finite Subset of J by ZFMISC_1:def_1; assume A2: ex k being Nat st J c= Seg k ; ::_thesis: Sum (f | J) = Sum (Func_Seq (F,(Sgm J))) 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; then support f9 c= J9 by PRE_POLY:37; then consider fs being 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)) by RELAT_1:94 .= (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; ::_thesis: verum end; theorem Th25: :: NAT_5:25 for I being non empty set for F being PartFunc of I,REAL for f being Function of I,NAT for J being finite Subset of I st f = F holds Sum (f | J) = Sum (F,J) proof let I be non empty set ; ::_thesis: for F being PartFunc of I,REAL for f being Function of I,NAT for J being finite Subset of I st f = F holds Sum (f | J) = Sum (F,J) let F be PartFunc of I,REAL; ::_thesis: for f being Function of I,NAT for J being finite Subset of I st f = F holds Sum (f | J) = Sum (F,J) let f be Function of I,NAT; ::_thesis: for J being finite Subset of I st f = F holds Sum (f | J) = Sum (F,J) let J be finite Subset of I; ::_thesis: ( f = F implies Sum (f | J) = Sum (F,J) ) 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 ; ::_thesis: Sum (f | J) = Sum (F,J) 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; then J = dom (f | J9) by RELAT_1:62; then support f9 c= J9 by PRE_POLY:37; then consider fs being 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; ::_thesis: verum end; theorem Th26: :: NAT_5:26 for I being set for f being Function of I,NAT for J, K being finite Subset of I st J misses K holds Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) proof let I be set ; ::_thesis: for f being Function of I,NAT for J, K being finite Subset of I st J misses K holds Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) let f be Function of I,NAT; ::_thesis: for J, K being finite Subset of I st J misses K holds Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) let J, K be finite Subset of I; ::_thesis: ( J misses K implies Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) ) assume A1: J misses K ; ::_thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) percases ( I is empty or not I is empty ) ; supposeA2: I is empty ; ::_thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) set b = EmptyBag {}; A3: Sum (EmptyBag {}) = 0 by UPROOTS:11; ( J = {} & f | J = {} ) by A2; hence Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) by A3; ::_thesis: verum end; suppose not I is empty ; ::_thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) then reconsider I9 = I as non empty set ; [:I9,NAT:] c= [:I9,REAL:] by ZFMISC_1:95; 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 ; ::_thesis: verum end; end; end; theorem Th27: :: NAT_5:27 for I, j being set for f being Function of I,NAT for J being finite Subset of I st J = {j} holds Sum (f | J) = f . j proof let I, j be set ; ::_thesis: for f being Function of I,NAT for J being finite Subset of I st J = {j} holds Sum (f | J) = f . j let f be Function of I,NAT; ::_thesis: for J being finite Subset of I st J = {j} holds Sum (f | J) = f . j let J be finite Subset of I; ::_thesis: ( J = {j} implies Sum (f | J) = f . j ) consider f9 being 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} ; ::_thesis: Sum (f | J) = f . 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; then A6: support (f | J) c= J by PRE_POLY:37; percases ( support (f | J) = {} or support (f | J) = J ) by A3, A6, ZFMISC_1:33; supposeA7: support (f | J) = {} ; ::_thesis: Sum (f | J) = f . j now__::_thesis:_not_f_._j_<>_0 assume f . j <> 0 ; ::_thesis: contradiction then (f | J) . j <> 0 by A4, FUNCT_1:49; hence contradiction by A7, PRE_POLY:def_7; ::_thesis: verum end; hence Sum (f | J) = f . j by A1, A2, A7, RVSUM_1:72; ::_thesis: verum end; suppose support (f | J) = J ; ::_thesis: Sum (f | J) = f . j then canFS (support (f | J)) = <*j*> by A3, UPROOTS:4; 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; ::_thesis: verum end; end; end; Lm11: for I, j being set for f, g being Function of I,NAT for J, K being finite Subset of I st J = {j} holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) proof let I, j be set ; ::_thesis: for f, g being Function of I,NAT for J, K being finite Subset of I st J = {j} holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) let f, g be Function of I,NAT; ::_thesis: for J, K being finite Subset of I st J = {j} holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) let J, K be finite Subset of I; ::_thesis: ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) defpred S1[ Nat] means for I, j being set for f, g being Function of I,NAT for 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 S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A2: for n being Nat st n < k holds S1[n] ; ::_thesis: S1[k] thus S1[k] ::_thesis: verum 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, j be set ; ::_thesis: for f, g being Function of I,NAT for J, K being finite Subset of I st J = {j} & k = card K holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) let f, g be Function of I,NAT; ::_thesis: for J, K being finite Subset of I st J = {j} & k = card K holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) let J, K be finite Subset of I; ::_thesis: ( J = {j} & k = card K implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) assume A4: J = {j} ; ::_thesis: ( not k = card K or Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) assume A5: k = card K ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) percases ( k = 0 or k = 1 or k > 1 ) by A3, XXREAL_0:1; supposeA6: k = 0 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) set b = EmptyBag {}; A7: Sum (EmptyBag {}) = 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; ::_thesis: verum end; supposeA9: k = 1 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) set x = the set ; card { the set } = card K by A5, A9, CARD_1:30; then consider k9 being set such that A10: K = {k9} by CARD_1:29; set b = (multnat * [:f,g:]) | [:J,K:]; consider f9 being FinSequence of REAL such that A11: Sum ((multnat * [:f,g:]) | [:J,K:]) = Sum f9 and A12: f9 = ((multnat * [:f,g:]) | [:J,K:]) * (canFS (support ((multnat * [:f,g:]) | [:J,K:]))) 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 ((multnat * [:f,g:]) | [:J,K:]) = [:J,K:] by RELAT_1:62; then A17: support ((multnat * [:f,g:]) | [:J,K:]) c= [:J,K:] by PRE_POLY:37; Sum ((multnat * [:f,g:]) | [:J,K:]) = (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; set n2 = g . k9; A18: (f . j) * (g . k9) = multnat . ((f . j),(g . k9)) 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 .= ((multnat * [:f,g:]) | [:J,K:]) . [j,k9] by A14, FUNCT_1:49 ; percases ( support ((multnat * [:f,g:]) | [:J,K:]) = {} or support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]} ) by A13, A17, ZFMISC_1:33; supposeA19: support ((multnat * [:f,g:]) | [:J,K:]) = {} ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) then (f . j) * (g . k9) = 0 by A18, PRE_POLY:def_7; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A11, A12, A19, RVSUM_1:72; ::_thesis: verum end; suppose support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]} ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) then canFS (support ((multnat * [:f,g:]) | [:J,K:])) = <*[j,k9]*> by UPROOTS:4; then f9 = <*(((multnat * [:f,g:]) | [:J,K:]) . [j,k9])*> by A12, A14, A16, FINSEQ_2:34; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A11, A18, RVSUM_1:73; ::_thesis: verum end; end; end; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A10, Th27; ::_thesis: verum end; supposeA20: k > 1 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) then K <> {} by A5; then consider k9 being set such that A21: k9 in K by XBOOLE_0:def_1; set K0 = {k9}; set K1 = K \ {k9}; reconsider K0 = {k9} as finite Subset of I by A21, ZFMISC_1:31; card K0 < k by A20, CARD_1:30; then A22: ( (- 1) + k < 0 + k & Sum ((multnat * [:f,g:]) | [:J,K0:]) = (f . j) * (Sum (g | K0)) ) by A2, A4, XREAL_1:8; K \ {k9} misses K0 by XBOOLE_1:79; then A23: [:J,(K \ {k9}):] misses [:J,K0:] by ZFMISC_1:104; k9 in K0 by TARSKI:def_1; then not k9 in K \ {k9} by XBOOLE_0:def_5; then A24: card ((K \ {k9}) \/ K0) = (card (K \ {k9})) + 1 by CARD_2:41; A25: (K \ {k9}) \/ K0 = K \/ {k9} by XBOOLE_1:39 .= K by A21, ZFMISC_1:40 ; then [:J,K:] = [:J,(K \ {k9}):] \/ [:J,K0:] by ZFMISC_1:97; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:J,(K \ {k9}):])) + (Sum ((multnat * [:f,g:]) | [:J,K0:])) by A23, Th26 .= ((f . j) * (Sum (g | (K \ {k9})))) + ((f . j) * (Sum (g | K0))) by A2, A4, A5, A24, A25, A22 .= (f . j) * ((Sum (g | (K \ {k9}))) + (Sum (g | K0))) .= (f . j) * (Sum (g | K)) by A25, Th26, XBOOLE_1:79 ; ::_thesis: verum end; end; end; end; for k being Nat holds S1[k] from NAT_1:sch_4(A1); then S1[ card K] ; hence ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) ; ::_thesis: verum end; theorem Th28: :: NAT_5:28 for I being set for f, g being Function of I,NAT for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) proof let I be set ; ::_thesis: for f, g being Function of I,NAT for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) let f, g be Function of I,NAT; ::_thesis: for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) let J, K be finite Subset of I; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) defpred S1[ Nat] means for I being set for f, g being Function of I,NAT for 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 S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A2: for n being Nat st n < k holds S1[n] ; ::_thesis: S1[k] thus S1[k] ::_thesis: verum 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 ; ::_thesis: for f, g being Function of I,NAT for J, K being finite Subset of I st k = card J holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) let f, g be Function of I,NAT; ::_thesis: for J, K being finite Subset of I st k = card J holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) let J, K be finite Subset of I; ::_thesis: ( k = card J implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) ) assume A4: k = card J ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) percases ( k = 0 or k = 1 or k > 1 ) by A3, XXREAL_0:1; suppose k = 0 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) 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; ::_thesis: verum end; supposeA8: k = 1 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) set x = the set ; card { the set } = card J by A4, A8, CARD_1:30; then consider j being set 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; ::_thesis: verum end; supposeA10: k > 1 ; ::_thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) then J <> {} by A4; then consider j being set such that A11: j in J by XBOOLE_0:def_1; set J0 = {j}; set J1 = J \ {j}; reconsider J0 = {j} as finite Subset of I by A11, ZFMISC_1:31; A12: (J \ {j}) \/ J0 = J \/ {j} by XBOOLE_1:39 .= J by A11, ZFMISC_1:40 ; then A13: Sum (f | J) = (Sum (f | (J \ {j}))) + (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; J \ {j} misses J0 by XBOOLE_1:79; then A15: [:(J \ {j}),K:] misses [:J0,K:] by ZFMISC_1:104; j in J0 by TARSKI:def_1; then not j in J \ {j} by XBOOLE_0:def_5; then A16: card ((J \ {j}) \/ J0) = (card (J \ {j})) + 1 by CARD_2:41; [:J,K:] = [:(J \ {j}),K:] \/ [:J0,K:] by A12, ZFMISC_1:97; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:(J \ {j}),K:])) + (Sum ((multnat * [:f,g:]) | [:J0,K:])) by A15, Th26 .= ((Sum (f | (J \ {j}))) * (Sum (g | K))) + ((Sum (f | J0)) * (Sum (g | K))) by A2, A4, A16, A12, A14 .= (Sum (f | J)) * (Sum (g | K)) by A13 ; ::_thesis: verum end; end; end; end; for k being Nat holds S1[k] from NAT_1:sch_4(A1); then S1[ card J] ; hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) ; ::_thesis: verum end; definition let k be Nat; func EXP k -> Function of NAT,NAT means :Def1: :: NAT_5:def 1 for n being Nat holds it . n = n |^ k; existence ex b1 being Function of NAT,NAT st for n being Nat holds b1 . n = n |^ k proof reconsider k9 = k as Element of NAT by ORDINAL1:def_12; deffunc H1( Element of NAT ) -> Element of NAT = $1 |^ k9; consider f being Function of NAT,NAT such that A1: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4(); take f ; ::_thesis: for n being Nat holds f . n = n |^ k for n being Nat holds f . n = n |^ k proof let n be Nat; ::_thesis: f . n = n |^ k reconsider n9 = n as Element of NAT by ORDINAL1:def_12; f . n9 = H1(n9) by A1; hence f . n = n |^ k ; ::_thesis: verum end; hence for n being Nat holds f . n = n |^ k ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,NAT st ( for n being Nat holds b1 . n = n |^ k ) & ( for n being Nat holds b2 . n = n |^ k ) holds b1 = b2 proof let f1, f2 be Function of NAT,NAT; ::_thesis: ( ( for n being Nat holds f1 . n = n |^ k ) & ( for n being Nat holds f2 . n = n |^ k ) implies f1 = f2 ) assume A2: for n being Nat holds f1 . n = n |^ k ; ::_thesis: ( ex n being Nat st not f2 . n = n |^ k or f1 = f2 ) assume A3: for n being Nat holds f2 . n = n |^ k ; ::_thesis: f1 = f2 for x being set st x in NAT holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in NAT implies f1 . x = f2 . x ) assume x in NAT ; ::_thesis: f1 . x = f2 . x then reconsider n = x as Nat ; f1 . n = n |^ k by A2 .= f2 . n by A3 ; hence f1 . x = f2 . x ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines EXP NAT_5:def_1_:_ for k being Nat for b2 being Function of NAT,NAT holds ( b2 = EXP k iff for n being Nat holds b2 . n = n |^ k ); definition let k, n be Nat; func sigma (k,n) -> Element of NAT means :Def2: :: NAT_5:def 2 for m being non zero Nat st n = m holds it = Sum ((EXP k) | (NatDivisors m)) if n <> 0 otherwise it = 0 ; correctness consistency for b1 being Element of NAT holds verum; existence ( ( for b1 being Element of NAT holds verum ) & ( n <> 0 implies ex b1 being Element of NAT st for m being non zero Nat st n = m holds b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b1 being Element of NAT st b1 = 0 ) ); uniqueness for b1, b2 being Element of NAT holds ( ( n <> 0 & ( for m being non zero Nat st n = m holds b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds b2 = Sum ((EXP k) | (NatDivisors m)) ) implies b1 = b2 ) & ( not n <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ); 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 ; ::_thesis: ( ( 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 ) ) thus ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; ::_thesis: ( 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 ) assume n <> 0 ; ::_thesis: ( ex m being non zero Nat st ( n = m & not n1 = Sum ((EXP k) | (NatDivisors m)) ) or ex m being non zero Nat st ( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 ) then reconsider m = n as non zero Nat ; assume for m being non zero Nat st n = m holds n1 = Sum ((EXP k) | (NatDivisors m)) ; ::_thesis: ( ex m being non zero Nat st ( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 ) then A2: n1 = Sum ((EXP k) | (NatDivisors m)) ; assume for m being non zero Nat st n = m holds n2 = Sum ((EXP k) | (NatDivisors m)) ; ::_thesis: n1 = n2 hence n1 = n2 by A2; ::_thesis: verum 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 ; ::_thesis: ex n1 being Element of NAT st for m being non zero Nat st n = m holds n1 = Sum ((EXP k) | (NatDivisors m)) then reconsider n9 = n as non zero Nat ; reconsider n1 = Sum ((EXP k) | (NatDivisors n9)) as Element of NAT by ORDINAL1:def_12; take n1 ; ::_thesis: for m being non zero Nat st n = m holds n1 = Sum ((EXP k) | (NatDivisors m)) let m be non zero Nat; ::_thesis: ( n = m implies n1 = Sum ((EXP k) | (NatDivisors m)) ) assume n = m ; ::_thesis: n1 = Sum ((EXP k) | (NatDivisors m)) hence n1 = Sum ((EXP k) | (NatDivisors m)) ; ::_thesis: verum end; hence ( ( for b1 being Element of NAT holds verum ) & ( n <> 0 implies ex b1 being Element of NAT st for m being non zero Nat st n = m holds b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b1 being Element of NAT st b1 = 0 ) & ( for b1, b2 being Element of NAT holds ( ( n <> 0 & ( for m being non zero Nat st n = m holds b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds b2 = Sum ((EXP k) | (NatDivisors m)) ) implies b1 = b2 ) & ( not n <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ) ) by A1; ::_thesis: verum end; end; :: deftheorem Def2 defines sigma NAT_5:def_2_:_ for k, n being Nat for b3 being Element of NAT holds ( ( n <> 0 implies ( b3 = sigma (k,n) iff for m being non zero Nat st n = m holds b3 = Sum ((EXP k) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b3 = sigma (k,n) iff b3 = 0 ) ) ); definition let k be Nat; func Sigma k -> Function of NAT,NAT means :Def3: :: NAT_5:def 3 for n being Nat holds it . n = sigma (k,n); existence ex b1 being Function of NAT,NAT st for n being Nat holds b1 . n = sigma (k,n) proof deffunc H1( Element of NAT ) -> Element of NAT = sigma (k,$1); consider f being Function of NAT,NAT such that A1: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4(); take f ; ::_thesis: for n being Nat holds f . n = sigma (k,n) let n be Nat; ::_thesis: f . n = sigma (k,n) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; thus f . n = f . n9 .= sigma (k,n) by A1 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,NAT st ( for n being Nat holds b1 . n = sigma (k,n) ) & ( for n being Nat holds b2 . n = sigma (k,n) ) holds b1 = b2 proof let f1, f2 be Function of NAT,NAT; ::_thesis: ( ( for n being Nat holds f1 . n = sigma (k,n) ) & ( for n being Nat holds f2 . n = sigma (k,n) ) implies f1 = f2 ) assume A2: for n being Nat holds f1 . n = sigma (k,n) ; ::_thesis: ( ex n being Nat st not f2 . n = sigma (k,n) or f1 = f2 ) assume A3: for n being Nat holds f2 . n = sigma (k,n) ; ::_thesis: f1 = f2 for x being set st x in NAT holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in NAT implies f1 . x = f2 . x ) assume x in NAT ; ::_thesis: f1 . x = f2 . x then reconsider n = x as Nat ; thus f1 . x = sigma (k,n) by A2 .= f2 . x by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines Sigma NAT_5:def_3_:_ for k being Nat for b2 being Function of NAT,NAT holds ( b2 = Sigma k iff for n being Nat holds b2 . n = sigma (k,n) ); definition let n be Nat; func sigma n -> Element of NAT equals :: NAT_5:def 4 sigma (1,n); correctness coherence sigma (1,n) is Element of NAT ; ; end; :: deftheorem defines sigma NAT_5:def_4_:_ for n being Nat holds sigma n = sigma (1,n); theorem Th29: :: NAT_5:29 for k being Nat holds sigma (k,1) = 1 proof let k be Nat; ::_thesis: sigma (k,1) = 1 set b = (EXP k) | (NatDivisors 1); consider f being FinSequence of REAL such that A1: Sum ((EXP k) | (NatDivisors 1)) = Sum f and A2: f = ((EXP k) | (NatDivisors 1)) * (canFS (support ((EXP k) | (NatDivisors 1)))) 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 ((EXP k) | (NatDivisors 1)) by A3, RELAT_1:57; then A5: ((EXP k) | (NatDivisors 1)) . 1 = (EXP k) . 1 by FUNCT_1:47 .= 1 |^ k by Def1 .= 1 by NEWTON:10 ; A6: support ((EXP k) | (NatDivisors 1)) c= dom ((EXP k) | (NatDivisors 1)) by PRE_POLY:37; for x being set holds ( x in support ((EXP k) | (NatDivisors 1)) iff x = 1 ) proof let x be set ; ::_thesis: ( x in support ((EXP k) | (NatDivisors 1)) iff x = 1 ) hereby ::_thesis: ( x = 1 implies x in support ((EXP k) | (NatDivisors 1)) ) assume x in support ((EXP k) | (NatDivisors 1)) ; ::_thesis: x = 1 then x in NatDivisors 1 by A6, RELAT_1:57; hence x = 1 by MOEBIUS1:41, TARSKI:def_1; ::_thesis: verum end; assume x = 1 ; ::_thesis: x in support ((EXP k) | (NatDivisors 1)) hence x in support ((EXP k) | (NatDivisors 1)) by A5, PRE_POLY:def_7; ::_thesis: verum end; then support ((EXP k) | (NatDivisors 1)) = {1} by TARSKI:def_1; then f = ((EXP k) | (NatDivisors 1)) * <*1*> by A2, UPROOTS:4 .= <*(((EXP k) | (NatDivisors 1)) . 1)*> by A4, FINSEQ_2:34 ; then Sum ((EXP k) | (NatDivisors 1)) = 1 by A5, A1, RVSUM_1:73; hence sigma (k,1) = 1 by Def2; ::_thesis: verum end; theorem Th30: :: NAT_5:30 for p, n being Nat st p is prime holds sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) proof let p, n be Nat; ::_thesis: ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) ) defpred S1[ Nat] means for p being Nat st p is prime holds sigma (p |^ $1) = ((p |^ ($1 + 1)) - 1) / (p - 1); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let p be Nat; ::_thesis: ( p is prime implies sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1) ) reconsider k9 = k + 1, p9 = p as Element of NAT by ORDINAL1:def_12; assume A3: p is prime ; ::_thesis: sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1) 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__::_thesis:_for_x_being_set_holds_not_x_in_J_/\_K let x be set ; ::_thesis: not x in J /\ K assume A7: x in J /\ K ; ::_thesis: contradiction 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 being 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 ; ::_thesis: verum 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) by NEWTON:9 .= p |^ (k + 1) ; 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 ; ::_thesis: ( x in NatDivisors (p |^ (k + 1)) iff x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} ) hereby ::_thesis: ( x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} implies x in NatDivisors (p |^ (k + 1)) ) assume x in NatDivisors (p |^ (k + 1)) ; ::_thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} then x in { (p |^ t) where t is Element of NAT : t <= k + 1 } by A3, Th19; then consider t being Element of NAT such that A12: x = p |^ t and A13: t <= k + 1 ; percases ( t <= k or t > k ) ; suppose t <= k ; ::_thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} 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; ::_thesis: verum end; suppose t > k ; ::_thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} 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; ::_thesis: verum end; end; end; assume A14: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} ; ::_thesis: x in NatDivisors (p |^ (k + 1)) percases ( x in NatDivisors (p |^ k) or x in {(p |^ (k + 1))} ) by A14, XBOOLE_0:def_3; suppose x in NatDivisors (p |^ k) ; ::_thesis: x in NatDivisors (p |^ (k + 1)) then x in { (p |^ t) where t is Element of NAT : t <= k } by A3, Th19; then consider t being 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; ::_thesis: verum end; suppose x in {(p |^ (k + 1))} ; ::_thesis: x in NatDivisors (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; ::_thesis: verum end; end; end; then NatDivisors (p |^ (k + 1)) = (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by TARSKI:1; 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 ; ::_thesis: verum end; end; A17: S1[ 0 ] proof let p be Nat; ::_thesis: ( p is prime implies sigma (p |^ 0) = ((p |^ (0 + 1)) - 1) / (p - 1) ) assume p is prime ; ::_thesis: sigma (p |^ 0) = ((p |^ (0 + 1)) - 1) / (p - 1) 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) by NEWTON:5 ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A17, A1); hence ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) ) ; ::_thesis: verum end; theorem Th31: :: NAT_5:31 for m being Nat for n0 being non zero Nat st m divides n0 & n0 <> m & m <> 1 holds (1 + m) + n0 <= sigma n0 proof let m be Nat; ::_thesis: for n0 being non zero Nat st m divides n0 & n0 <> m & m <> 1 holds (1 + m) + n0 <= sigma n0 let n0 be non zero Nat; ::_thesis: ( m divides n0 & n0 <> m & m <> 1 implies (1 + m) + n0 <= sigma n0 ) assume A1: m divides n0 ; ::_thesis: ( not n0 <> m or not m <> 1 or (1 + m) + n0 <= sigma n0 ) assume A2: n0 <> m ; ::_thesis: ( not m <> 1 or (1 + m) + n0 <= sigma n0 ) assume A3: m <> 1 ; ::_thesis: (1 + m) + n0 <= sigma n0 percases ( n0 = 1 or n0 <> 1 ) ; suppose n0 = 1 ; ::_thesis: (1 + m) + n0 <= sigma n0 hence (1 + m) + n0 <= sigma n0 by A1, A2, WSIERP_1:15; ::_thesis: verum end; supposeA4: n0 <> 1 ; ::_thesis: (1 + m) + n0 <= sigma n0 reconsider X2 = {m,n0} as finite Subset of NAT by Th5; set X1 = {1}; now__::_thesis:_for_x_being_set_holds_not_x_in_{1}_/\_X2 let x be set ; ::_thesis: not x in {1} /\ X2 assume A5: x in {1} /\ X2 ; ::_thesis: contradiction then x in {1} 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; ::_thesis: verum end; then {1} /\ X2 = {} by XBOOLE_0:def_1; then A7: {1} 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) | ((NatDivisors n0) \ X))) + (Sum ((EXP 1) | X)) by XREAL_1:7; for x being set st x in X holds x in NatDivisors n0 proof let x be set ; ::_thesis: ( x in X implies x in NatDivisors n0 ) assume A9: x in X ; ::_thesis: x in NatDivisors n0 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 ; ::_thesis: verum end; then X c= NatDivisors n0 by TARSKI:def_3; then NatDivisors n0 = X \/ ((NatDivisors n0) \ X) by XBOOLE_1:45; then A10: sigma n0 = Sum ((EXP 1) | (X \/ ((NatDivisors n0) \ X))) by Def2 .= (Sum ((EXP 1) | X)) + (Sum ((EXP 1) | ((NatDivisors n0) \ X))) by Th26, XBOOLE_1:79 ; now__::_thesis:_for_x_being_set_holds_not_x_in_X3_/\_X4 let x be set ; ::_thesis: not x in X3 /\ X4 assume A11: x in X3 /\ X4 ; ::_thesis: contradiction 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; ::_thesis: verum 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 = {1} \/ X2 by ENUMSET1:2; then Sum ((EXP 1) | X) = (Sum ((EXP 1) | {1})) + (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) by NEWTON:5 .= (1 + m) + (n0 |^ 1) by NEWTON:5 .= (1 + m) + n0 by NEWTON:5 ; hence (1 + m) + n0 <= sigma n0 by A10, A8; ::_thesis: verum end; end; end; theorem Th32: :: NAT_5:32 for m, k being Nat for n0 being non zero Nat st m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k holds ((1 + m) + k) + n0 <= sigma n0 proof let m, k be Nat; ::_thesis: for n0 being non zero Nat st m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k holds ((1 + m) + k) + n0 <= sigma n0 let n0 be non zero Nat; ::_thesis: ( m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k implies ((1 + m) + k) + n0 <= sigma n0 ) assume A1: m divides n0 ; ::_thesis: ( not k divides n0 or not n0 <> m or not n0 <> k or not m <> 1 or not k <> 1 or not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A2: k divides n0 ; ::_thesis: ( not n0 <> m or not n0 <> k or not m <> 1 or not k <> 1 or not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A3: n0 <> m ; ::_thesis: ( not n0 <> k or not m <> 1 or not k <> 1 or not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A4: n0 <> k ; ::_thesis: ( not m <> 1 or not k <> 1 or not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A5: m <> 1 ; ::_thesis: ( not k <> 1 or not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A6: k <> 1 ; ::_thesis: ( not m <> k or ((1 + m) + k) + n0 <= sigma n0 ) assume A7: m <> k ; ::_thesis: ((1 + m) + k) + n0 <= sigma n0 percases ( n0 = 1 or n0 <> 1 ) ; suppose n0 = 1 ; ::_thesis: ((1 + m) + k) + n0 <= sigma n0 hence ((1 + m) + k) + n0 <= sigma n0 by A1, A3, WSIERP_1:15; ::_thesis: verum end; supposeA8: n0 <> 1 ; ::_thesis: ((1 + m) + k) + n0 <= sigma n0 reconsider X2 = {m,k,n0} as finite Subset of NAT by Lm2; set X1 = {1}; now__::_thesis:_for_x_being_set_holds_not_x_in_{1}_/\_X2 let x be set ; ::_thesis: not x in {1} /\ X2 assume A9: x in {1} /\ X2 ; ::_thesis: contradiction then x in {1} 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; ::_thesis: verum end; then {1} /\ X2 = {} by XBOOLE_0:def_1; then A11: {1} 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) | ((NatDivisors n0) \ X))) + (Sum ((EXP 1) | X)) by XREAL_1:7; now__::_thesis:_for_x_being_set_holds_not_x_in_X5_/\_X6 let x be set ; ::_thesis: not x in X5 /\ X6 assume A13: x in X5 /\ X6 ; ::_thesis: contradiction 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; ::_thesis: verum 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 set st x in X holds x in NatDivisors n0 proof let x be set ; ::_thesis: ( x in X implies x in NatDivisors n0 ) assume A16: x in X ; ::_thesis: x in NatDivisors n0 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 ; ::_thesis: verum end; then X c= NatDivisors n0 by TARSKI:def_3; then NatDivisors n0 = X \/ ((NatDivisors n0) \ X) by XBOOLE_1:45; then A17: sigma n0 = Sum ((EXP 1) | (X \/ ((NatDivisors n0) \ X))) by Def2 .= (Sum ((EXP 1) | X)) + (Sum ((EXP 1) | ((NatDivisors n0) \ X))) by Th26, XBOOLE_1:79 ; now__::_thesis:_for_x_being_set_holds_not_x_in_X3_/\_X4 let x be set ; ::_thesis: not x in X3 /\ X4 assume A18: x in X3 /\ X4 ; ::_thesis: contradiction 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; ::_thesis: verum 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 = {1} \/ X2 by ENUMSET1:4; then Sum ((EXP 1) | X) = (Sum ((EXP 1) | {1})) + (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) by NEWTON:5 .= ((1 + m) + (k |^ 1)) + (n0 |^ 1) by NEWTON:5 .= ((1 + m) + k) + (n0 |^ 1) by NEWTON:5 .= ((1 + m) + k) + n0 by NEWTON:5 ; hence ((1 + m) + k) + n0 <= sigma n0 by A17, A12; ::_thesis: verum end; end; end; theorem Th33: :: NAT_5:33 for m being Nat for n0 being non zero Nat st sigma n0 = n0 + m & m divides n0 & n0 <> m holds ( m = 1 & n0 is prime ) proof let m be Nat; ::_thesis: for n0 being non zero Nat st sigma n0 = n0 + m & m divides n0 & n0 <> m holds ( m = 1 & n0 is prime ) let n0 be non zero Nat; ::_thesis: ( sigma n0 = n0 + m & m divides n0 & n0 <> m implies ( m = 1 & n0 is prime ) ) assume A1: sigma n0 = n0 + m ; ::_thesis: ( not m divides n0 or not n0 <> m or ( m = 1 & n0 is prime ) ) assume A2: m divides n0 ; ::_thesis: ( not n0 <> m or ( m = 1 & n0 is prime ) ) assume A3: n0 <> m ; ::_thesis: ( m = 1 & n0 is prime ) percases ( n0 = 1 or n0 <> 1 ) ; suppose n0 = 1 ; ::_thesis: ( m = 1 & n0 is prime ) then 1 = 1 + m by A1, Th29; hence ( m = 1 & n0 is prime ) by A2, INT_2:3; ::_thesis: verum end; supposeA4: n0 <> 1 ; ::_thesis: ( m = 1 & n0 is prime ) consider k being Nat such that A5: n0 = m * k by A2, NAT_D:def_3; A6: k <> m proof assume k = m ; ::_thesis: contradiction 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 ; ::_thesis: verum end; k = n0 proof A7: ( k divides n0 & k <> 1 ) by A3, A5, NAT_D:def_3; assume A8: k <> n0 ; ::_thesis: contradiction 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 ; ::_thesis: verum end; then n0 / n0 = m by A5, XCMPLX_1:89; hence A9: m = 1 by XCMPLX_1:60; ::_thesis: n0 is prime A10: for k being Nat holds ( not k divides n0 or k = 1 or k = n0 ) proof let k be Nat; ::_thesis: ( not k divides n0 or k = 1 or k = n0 ) assume that A11: k divides n0 and A12: k <> 1 ; ::_thesis: k = n0 assume k <> n0 ; ::_thesis: contradiction 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; ::_thesis: verum end; n0 > 1 by A4, NAT_1:25; hence n0 is prime by A10, INT_2:def_4; ::_thesis: verum end; end; end; definition let f be Function of NAT,NAT; attrf is multiplicative means :Def5: :: NAT_5:def 5 for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds f . (n0 * m0) = (f . n0) * (f . m0); end; :: deftheorem Def5 defines multiplicative NAT_5:def_5_:_ for f being Function of NAT,NAT holds ( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds f . (n0 * m0) = (f . n0) * (f . m0) ); theorem Th34: :: NAT_5:34 for f, F being Function of NAT,NAT st f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) holds F is multiplicative proof let f, F be Function of NAT,NAT; ::_thesis: ( f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) implies F is multiplicative ) assume A1: f is multiplicative ; ::_thesis: ( ex n0 being non zero Nat st not F . n0 = Sum (f | (NatDivisors n0)) or F is multiplicative ) assume A2: for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ; ::_thesis: F is multiplicative for n, m being non zero Nat st n,m are_relative_prime holds F . (n * m) = (F . n) * (F . m) proof let n, m be non zero Nat; ::_thesis: ( n,m are_relative_prime implies F . (n * m) = (F . n) * (F . m) ) set b1 = f | (NatDivisors (n * m)); set b2 = (multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]; consider f1 being FinSequence of REAL such that A3: Sum (f | (NatDivisors (n * m))) = Sum f1 and A4: f1 = (f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m))))) by UPROOTS:def_3; set h9 = multnat | [:(NatDivisors n),(NatDivisors m):]; set g2 = canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])); set g1 = canFS (support (f | (NatDivisors (n * m)))); consider f2 being FinSequence of REAL such that A5: Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = Sum f2 and A6: f2 = ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by UPROOTS:def_3; dom multnat = [:NAT,NAT:] by FUNCT_2:def_1; then A7: dom (multnat | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):] by RELAT_1:62; assume A8: n,m are_relative_prime ; ::_thesis: F . (n * m) = (F . n) * (F . m) for x1, x2 being set st x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 implies x1 = x2 ) assume A9: x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) ; ::_thesis: ( not x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) or not (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 or x1 = x2 ) then consider n1, m1 being set such that A10: ( n1 in NatDivisors n & m1 in NatDivisors m ) and A11: x1 = [n1,m1] by ZFMISC_1:def_2; reconsider n1 = n1, m1 = m1 as Element of NAT by A10; A12: (multnat | [:(NatDivisors n),(NatDivisors m):]) . 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 (multnat | [:(NatDivisors n),(NatDivisors m):]) ; ::_thesis: ( not (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 or x1 = x2 ) then consider n2, m2 being set 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 = n2, m2 = m2 as Element of NAT by A14, A15; assume A17: (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 ; ::_thesis: x1 = x2 A18: (multnat | [:(NatDivisors n),(NatDivisors m):]) . 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; ::_thesis: verum end; then reconsider h9 = multnat | [:(NatDivisors n),(NatDivisors m):] as one-to-one Function by FUNCT_1:def_4; set h = (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))); A19: support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by PRE_POLY:37; dom (multnat * [:f,f:]) = [:NAT,NAT:] by FUNCT_2:def_1; then A20: dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):] by RELAT_1:62; A21: dom [:f,f:] = [:NAT,NAT:] by FUNCT_2:def_1; for x being set st x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) holds x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) proof let x be set ; ::_thesis: ( x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) implies x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) ) A22: rng (canFS (support (f | (NatDivisors (n * m))))) = support (f | (NatDivisors (n * m))) by FUNCT_2:def_3; assume A23: x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) ; ::_thesis: x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) then A24: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x <> 0 by PRE_POLY:def_7; A25: x in [:(NatDivisors n),(NatDivisors m):] by A20, A19, A23; consider n1, m1 being set such that A26: ( n1 in NatDivisors n & m1 in NatDivisors m ) and A27: x = [n1,m1] by A20, A19, A23, ZFMISC_1:def_2; reconsider n1 = n1, m1 = m1 as Element of NAT by A26; A28: n1,m1 are_relative_prime by A8, A26, Th14; reconsider n19 = n1, m19 = m1 as non zero Nat by A26, MOEBIUS1:39; set x9 = ((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1); set fn1 = f . n1; set fm1 = f . m1; ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x = (multnat * [:f,f:]) . x by A20, A19, A23, FUNCT_1:49 .= multnat . ([:f,f:] . x) by A21, A25, FUNCT_1:13 .= multnat . ([:f,f:] . (n1,m1)) by A27, BINOP_1:def_1 .= multnat . [(f . n1),(f . m1)] by FUNCT_3:75 .= multnat . ((f . n1),(f . m1)) by BINOP_1:def_1 .= (f . n1) * (f . m1) by BINOP_2:def_24 .= f . (n19 * m19) by A1, A28, Def5 .= (f | (NatDivisors (n * m))) . (n1 * m1) by A26, Th16, FUNCT_1:49 ; then A29: n1 * m1 in rng (canFS (support (f | (NatDivisors (n * m))))) by A24, A22, PRE_POLY:def_7; then n1 * m1 in dom ((canFS (support (f | (NatDivisors (n * m))))) ") by FUNCT_1:33; then ((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1) in rng ((canFS (support (f | (NatDivisors (n * m))))) ") by FUNCT_1:3; then A30: ((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1) in dom (canFS (support (f | (NatDivisors (n * m))))) by FUNCT_1:33; (canFS (support (f | (NatDivisors (n * m))))) . (((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1)) = n1 * m1 by A29, FUNCT_1:35 .= multnat . (n1,m1) by BINOP_2:def_24 .= multnat . [n1,m1] by BINOP_1:def_1 .= h9 . x by A20, A19, A23, A27, FUNCT_1:49 ; then h9 . x in rng (canFS (support (f | (NatDivisors (n * m))))) by A30, FUNCT_1:def_3; then h9 . x in dom ((canFS (support (f | (NatDivisors (n * m))))) ") by FUNCT_1:33; hence x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) by A7, A20, A19, A23, FUNCT_1:11; ::_thesis: verum end; then support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) by TARSKI:def_3; then rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) by FUNCT_2:def_3; then A31: dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by RELAT_1:27; rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A19, FUNCT_2:def_3; then A32: dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f2 by A6, A31, RELAT_1:27; A33: for x being set st x in dom f2 holds f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) proof let x be set ; ::_thesis: ( x in dom f2 implies f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) ) set x9 = (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x; A34: ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) = (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * ((canFS (support (f | (NatDivisors (n * m))))) ")) * h9 by RELAT_1:36 .= ((f | (NatDivisors (n * m))) * ((canFS (support (f | (NatDivisors (n * m))))) * ((canFS (support (f | (NatDivisors (n * m))))) "))) * h9 by RELAT_1:36 .= ((f | (NatDivisors (n * m))) * (id (rng (canFS (support (f | (NatDivisors (n * m)))))))) * h9 by FUNCT_1:39 .= ((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h9 by FUNCT_2:def_3 ; assume A35: x in dom f2 ; ::_thesis: f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) then A36: x in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by A6, FUNCT_1:11; then A37: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by FUNCT_1:3; then A38: ( support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) & (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) ) by PRE_POLY:37; then consider n1, m1 being set such that A39: ( n1 in NatDivisors n & m1 in NatDivisors m ) and A40: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x = [n1,m1] by A20, ZFMISC_1:def_2; reconsider n1 = n1, m1 = m1 as Element of NAT by A39; A41: n1,m1 are_relative_prime by A8, A39, Th14; reconsider n19 = n1, m19 = m1 as non zero Nat by A39, MOEBIUS1:39; set fn1 = f . n1; set fm1 = f . m1; A42: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in [:(NatDivisors n),(NatDivisors m):] by A20, A38; A43: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = (multnat * [:f,f:]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A20, A38, FUNCT_1:49 .= multnat . ([:f,f:] . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)) by A21, A42, FUNCT_1:13 .= multnat . ([:f,f:] . (n1,m1)) by A40, BINOP_1:def_1 .= multnat . [(f . n1),(f . m1)] by FUNCT_3:75 .= multnat . ((f . n1),(f . m1)) by BINOP_1:def_1 .= (f . n1) * (f . m1) by BINOP_2:def_24 .= f . (n19 * m19) by A1, A41, Def5 ; A44: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) <> 0 by A37, PRE_POLY:def_7; f . (n19 * m19) = (f | (NatDivisors (n * m))) . (n1 * m1) by A39, Th16, FUNCT_1:49; then A45: n1 * m1 in support (f | (NatDivisors (n * m))) by A44, A43, PRE_POLY:def_7; then A46: n1 * m1 in dom (id (support (f | (NatDivisors (n * m))))) ; A47: h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = multnat . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A7, A20, A38, FUNCT_1:47 .= multnat . (n1,m1) by A40, BINOP_1:def_1 .= n1 * m1 by BINOP_2:def_24 ; A48: ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) = (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) . x by A32, A35, FUNCT_1:13 .= ((((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x by RELAT_1:36 .= (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A36, FUNCT_1:13 ; (((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h9) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = ((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) . (h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)) by A7, A20, A38, FUNCT_1:13 .= (f | (NatDivisors (n * m))) . ((id (support (f | (NatDivisors (n * m))))) . (n1 * m1)) by A46, A47, FUNCT_1:13 .= (f | (NatDivisors (n * m))) . (n1 * m1) by A45, FUNCT_1:18 .= ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A39, A43, Th16, FUNCT_1:49 ; hence f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) by A4, A6, A36, A48, A34, FUNCT_1:13; ::_thesis: verum end; dom f = NAT by FUNCT_2:def_1; then A49: dom (f | (NatDivisors (n * m))) = NatDivisors (n * m) by RELAT_1:62; for y being set st y in rng (canFS (support (f | (NatDivisors (n * m))))) holds y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) proof let y be set ; ::_thesis: ( y in rng (canFS (support (f | (NatDivisors (n * m))))) implies y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) ) assume A50: y in rng (canFS (support (f | (NatDivisors (n * m))))) ; ::_thesis: y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) then A51: y in support (f | (NatDivisors (n * m))) ; A52: support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m))) by PRE_POLY:37; then consider n1, m1 being Nat such that A53: ( n1 in NatDivisors n & m1 in NatDivisors m ) and A54: y = n1 * m1 by A8, A49, A51, Th18; reconsider n19 = n1, m19 = m1 as non zero Nat by A53, MOEBIUS1:39; reconsider n1 = n1, m1 = m1 as Element of NAT by ORDINAL1:def_12; A55: n1,m1 are_relative_prime by A8, A53, Th14; A56: (f | (NatDivisors (n * m))) . y <> 0 by A50, PRE_POLY:def_7; A57: [n1,m1] in [:(NatDivisors n),(NatDivisors m):] by A53, ZFMISC_1:def_2; set x = ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1]; A58: [n1,m1] in [:(NatDivisors n),(NatDivisors m):] by A53, ZFMISC_1:def_2; (f | (NatDivisors (n * m))) . y = f . y by A49, A51, A52, FUNCT_1:49 .= (f . n19) * (f . m19) by A1, A54, A55, 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:75 .= multnat . ([:f,f:] . [n1,m1]) by BINOP_1:def_1 .= (multnat * [:f,f:]) . [n1,m1] by A21, FUNCT_1:13 .= ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1] by A58, FUNCT_1:49 ; then [n1,m1] in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A56, PRE_POLY:def_7; then A59: [n1,m1] in rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by FUNCT_2:def_3; then [n1,m1] in dom ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") by FUNCT_1:33; then ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1] in rng ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") by FUNCT_1:3; then A60: ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1] in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by FUNCT_1:33; A61: y = multnat . (n1,m1) by A54, BINOP_2:def_24 .= multnat . [n1,m1] by BINOP_1:def_1 .= (multnat | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1] by A57, FUNCT_1:49 .= h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1])) by A59, FUNCT_1:35 .= (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1]) by A60, FUNCT_1:13 ; (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1]) = [n1,m1] by A59, FUNCT_1:35; then ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1] in dom (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A7, A57, A60, FUNCT_1:11; hence y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A61, FUNCT_1:def_3; ::_thesis: verum end; then rng (canFS (support (f | (NatDivisors (n * m))))) c= rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by TARSKI:def_3; then dom ((canFS (support (f | (NatDivisors (n * m))))) ") c= rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by FUNCT_1:33; then rng (((canFS (support (f | (NatDivisors (n * m))))) ") * (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = rng ((canFS (support (f | (NatDivisors (n * m))))) ") by RELAT_1:28; then A62: rng (((canFS (support (f | (NatDivisors (n * m))))) ") * (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = dom (canFS (support (f | (NatDivisors (n * m))))) by FUNCT_1:33; support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m))) by PRE_POLY:37; then rng (canFS (support (f | (NatDivisors (n * m))))) c= dom (f | (NatDivisors (n * m))) by FUNCT_2:def_3; then dom ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) = dom (canFS (support (f | (NatDivisors (n * m))))) by RELAT_1:27; then A63: rng ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f1 by A4, A62, RELAT_1:36; then for x being set holds ( x in dom f2 iff ( x in dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) & ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x in dom f1 ) ) by A32, FUNCT_1:3; then f2 = f1 * ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A33, FUNCT_1:10; then A64: f1,f2 are_fiberwise_equipotent by A32, A63, CLASSES1:77; thus F . (n * m) = Sum (f | (NatDivisors (n * m))) by A2 .= Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A3, A5, A64, 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 ; ::_thesis: verum end; hence F is multiplicative by Def5; ::_thesis: verum end; theorem Th35: :: NAT_5:35 for k being Nat holds EXP k is multiplicative proof let k be Nat; ::_thesis: EXP k is multiplicative for n, m being non zero Nat st n,m are_relative_prime holds (EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m) proof let n, m be non zero Nat; ::_thesis: ( n,m are_relative_prime implies (EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m) ) assume n,m are_relative_prime ; ::_thesis: (EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m) 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 ; ::_thesis: verum end; hence EXP k is multiplicative by Def5; ::_thesis: verum end; theorem Th36: :: NAT_5:36 for k being Nat holds Sigma k is multiplicative proof let k be Nat; ::_thesis: Sigma k is multiplicative for n being non zero Nat holds (Sigma k) . n = Sum ((EXP k) | (NatDivisors n)) proof let n be non zero Nat; ::_thesis: (Sigma k) . n = Sum ((EXP k) | (NatDivisors n)) thus (Sigma k) . n = sigma (k,n) by Def3 .= Sum ((EXP k) | (NatDivisors n)) by Def2 ; ::_thesis: verum end; hence Sigma k is multiplicative by Th34, Th35; ::_thesis: verum end; theorem Th37: :: NAT_5:37 for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds sigma (n0 * m0) = (sigma n0) * (sigma m0) proof let n0, m0 be non zero Nat; ::_thesis: ( n0,m0 are_relative_prime implies sigma (n0 * m0) = (sigma n0) * (sigma m0) ) assume A1: n0,m0 are_relative_prime ; ::_thesis: sigma (n0 * m0) = (sigma n0) * (sigma m0) 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, Def5 .= (sigma (1,n0)) * ((Sigma 1) . m0) by Def3 .= (sigma n0) * (sigma m0) by Def3 ; ::_thesis: verum end; begin definition let n0 be non zero Nat; attrn0 is perfect means :Def6: :: NAT_5:def 6 sigma n0 = 2 * n0; end; :: deftheorem Def6 defines perfect NAT_5:def_6_:_ for n0 being non zero Nat holds ( n0 is perfect iff sigma n0 = 2 * n0 ); theorem :: NAT_5:38 for p being Nat for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds n0 is perfect proof let p be Nat; ::_thesis: for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds n0 is perfect let n0 be non zero Nat; ::_thesis: ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) implies n0 is perfect ) 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) by NEWTON:5 .= ((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 ; ::_thesis: ( not n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) or n0 is perfect ) A4: now__::_thesis:_not_p_<=_1 assume A5: p <= 1 ; ::_thesis: contradiction percases ( p = 0 or p = 1 ) by A5, NAT_1:25; suppose p = 0 ; ::_thesis: contradiction then (2 |^ p) -' 1 = 1 -' 1 by NEWTON:4 .= 1 - 1 by XREAL_0:def_2 .= 0 ; hence contradiction by A3; ::_thesis: verum end; suppose p = 1 ; ::_thesis: contradiction then (2 |^ p) -' 1 = 2 -' 1 by NEWTON:5 .= 2 - 1 by XREAL_0:def_2 .= 1 ; hence contradiction by A3, INT_2:def_4; ::_thesis: verum end; 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: p -' 2 = p - 2 by XREAL_0:def_2; then A9: p = (p -' 2) + 2 ; 2 |^ p > 1 by A4, NEWTON:86, 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) ; ::_thesis: n0 is perfect p -' 1 = (p -' 2) + 1 by A6, A8, XREAL_0:def_2; then 2 |^ (p -' 1),n2 are_relative_prime by A3, A11, A9, Th1, EULER_1:2; then sigma n0 = (sigma (2 |^ (p -' 1))) * (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, NEWTON:5 .= (((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 by Def6; ::_thesis: verum end; theorem :: NAT_5:39 for n0 being non zero Nat st n0 is even & n0 is perfect holds ex p being Nat st ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) proof let n0 be non zero Nat; ::_thesis: ( n0 is even & n0 is perfect implies ex p being Nat st ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) ) assume n0 is even ; ::_thesis: ( not n0 is perfect or ex p being Nat st ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) ) then consider k9, n9 being 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: (k9 + 1) - 1 = (k9 + 1) -' 1 by XREAL_0:def_2; then A5: (2 |^ (k9 + 1)) - 1 = ((2 |^ (((k9 + 1) -' 1) + 1)) - 2) + 1 .= (((2 |^ ((k9 + 1) -' 1)) * 2) - 2) + 1 by NEWTON:6 .= (2 * ((2 |^ ((k9 + 1) -' 1)) - 1)) + 1 ; assume n0 is perfect ; ::_thesis: ex p being Nat st ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) then A6: sigma n0 = 2 * n0 by Def6; take k9 + 1 ; ::_thesis: ( (2 |^ (k9 + 1)) -' 1 is prime & n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1) ) A7: (2 |^ (k9 + 1)) - 1 > (k9 + 1) - 1 by NEWTON:86, XREAL_1:14; then A8: (2 |^ (k9 + 1)) - 1 = (2 |^ (k9 + 1)) -' 1 by XREAL_0:def_2; sigma (2 |^ ((k9 + 1) -' 1)) = ((2 |^ (((k9 + 1) -' 1) + 1)) - 1) / (2 - 1) by Th30, INT_2:28 .= (2 |^ (k9 + 1)) - 1 by A4 ; then A9: ((2 |^ (k9 + 1)) - 1) * (sigma n9) = (2 * (2 |^ ((k9 + 1) -' 1))) * n9 by A1, A3, A6, A4, Th3, Th37 .= (2 |^ (k9 + 1)) * n9 by A4, NEWTON:6 ; then (2 |^ (k9 + 1)) -' 1 divides (2 |^ (k9 + 1)) * n2 by A8, INT_1:def_3; then (2 |^ (k9 + 1)) -' 1 divides n2 by A8, A5, Th3, EULER_1:13; then consider n99 being Nat such that A10: n9 = ((2 |^ (k9 + 1)) -' 1) * n99 by NAT_D:def_3; (sigma n9) * ((2 |^ (k9 + 1)) - 1) = ((2 |^ (k9 + 1)) * n99) * ((2 |^ (k9 + 1)) - 1) by A8, A9, A10; then A11: sigma n2 = (((2 |^ (k9 + 1)) - 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 k9 + 1 >= 1 + 1 by XREAL_1:7; then 2 |^ (k9 + 1) > 2 by NEWTON:86, XXREAL_0:2; then A13: (2 |^ (k9 + 1)) - 1 > 2 - 1 by XREAL_1:14; then ((2 |^ (k9 + 1)) -' 1) * n2 > 1 * n2 by A8, XREAL_1:68; then A14: n99 = 1 by A10, A12, A11, Th33; hence (2 |^ (k9 + 1)) -' 1 is prime by A8, A10, A12, A13, A11, Th33; ::_thesis: n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1) thus n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1) by A3, A4, A10, A14; ::_thesis: verum end; begin definition func Euler_phi -> Function of NAT,NAT means :Def7: :: NAT_5:def 7 for k being Element of NAT holds it . k = Euler k; existence ex b1 being Function of NAT,NAT st for k being Element of NAT holds b1 . k = Euler k 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 ex b1 being Function of NAT,NAT st for k being Element of NAT holds b1 . k = Euler k ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,NAT st ( for k being Element of NAT holds b1 . k = Euler k ) & ( for k being Element of NAT holds b2 . k = Euler k ) holds b1 = b2 proof A1: for f1, f2 being 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(); let f1, f2 be Function of NAT,NAT; ::_thesis: ( ( for k being Element of NAT holds f1 . k = Euler k ) & ( for k being Element of NAT holds f2 . k = Euler k ) implies f1 = f2 ) assume ( ( for k being Element of NAT holds f1 . k = Euler k ) & ( for k being Element of NAT holds f2 . k = Euler k ) ) ; ::_thesis: f1 = f2 hence f1 = f2 by A1; ::_thesis: verum end; end; :: deftheorem Def7 defines Euler_phi NAT_5:def_7_:_ for b1 being Function of NAT,NAT holds ( b1 = Euler_phi iff for k being Element of NAT holds b1 . k = Euler k ); theorem :: NAT_5:40 for n0 being non zero Nat holds Sum (Euler_phi | (NatDivisors n0)) = n0 proof let n0 be non zero Nat; ::_thesis: Sum (Euler_phi | (NatDivisors n0)) = n0 ( dom Euler_phi = NAT & rng Euler_phi c= REAL ) by FUNCT_2:def_1; then reconsider EU9 = Euler_phi as Function of NAT,REAL by FUNCT_2:2; set X = Seg n0; defpred S1[ set , set ] means $2 = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & $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 Seg n0 holds ex x being Element of bool (Seg n0) st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg n0 implies ex x being Element of bool (Seg n0) st S1[k,x] ) set X9 = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } ; for x being set st x in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } holds x in Seg n0 proof let x be set ; ::_thesis: ( x in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } implies x in Seg n0 ) assume x in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } ; ::_thesis: x in Seg n0 then ex i being Element of NAT st ( i = x & ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) ) ; hence x in Seg n0 ; ::_thesis: verum end; then reconsider X9 = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) } as Element of bool (Seg n0) by TARSKI:def_3; assume k in Seg n0 ; ::_thesis: ex x being Element of bool (Seg n0) st S1[k,x] take X9 ; ::_thesis: S1[k,X9] thus S1[k,X9] ; ::_thesis: verum end; consider fp being FinSequence of bool (Seg n0) such that A3: ( dom fp = Seg n0 & ( for k being Nat st k in Seg n0 holds S1[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 ; ::_thesis: ( k in dom ((Card fp) * (Sgm (NatDivisors n0))) implies ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k ) set k9 = (Sgm (NatDivisors n0)) . k; set Y = { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } ; set Z = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ; deffunc H1( Nat) -> Element of RAT = ($1 * n0) / ((Sgm (NatDivisors n0)) . k); A9: for x being set st x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } holds x in NAT proof let x be set ; ::_thesis: ( x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } implies x in NAT ) assume x in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } ; ::_thesis: x in NAT then ex l being Element of NAT st ( x = l & (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) ; hence x in NAT ; ::_thesis: verum end; assume A10: k in dom ((Card fp) * (Sgm (NatDivisors n0))) ; ::_thesis: ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k then k in dom (Sgm (NatDivisors n0)) by FUNCT_1:11; then (Sgm (NatDivisors n0)) . k in rng (Sgm (NatDivisors n0)) by FUNCT_1:3; then A11: (Sgm (NatDivisors n0)) . k in NatDivisors n0 by A4, FINSEQ_1:def_13; then A12: 1 <= (Sgm (NatDivisors n0)) . k by A3, A7, FINSEQ_1:1; (Sgm (NatDivisors n0)) . k,1 are_relative_prime by WSIERP_1:9; then 1 in { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } by A12; then reconsider Y = { l where l is Element of NAT : ( (Sgm (NatDivisors n0)) . k,l are_relative_prime & l >= 1 & l <= (Sgm (NatDivisors n0)) . k ) } as non empty Subset of NAT by A9, TARSKI:def_3; consider f being Function such that A13: ( dom f = Y & ( for d being Element of Y holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); for y being set holds ( y in rng f iff y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ) proof let y be set ; ::_thesis: ( y in rng f iff y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ) hereby ::_thesis: ( y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } implies y in rng f ) assume y in rng f ; ::_thesis: y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } then consider x being set such that A14: x in dom f and A15: y = f . x by FUNCT_1:def_3; reconsider x = x as Element of Y by A13, A14; A16: 0 < (Sgm (NatDivisors n0)) . k by A11, MOEBIUS1:39; (Sgm (NatDivisors n0)) . k divides n0 by A11, MOEBIUS1:39; then consider j being Nat such that A17: n0 = ((Sgm (NatDivisors n0)) . k) * j by NAT_D:def_3; y = H1(x) by A13, A15 .= x * (n0 / ((Sgm (NatDivisors n0)) . k)) by XCMPLX_1:74 ; then A18: y = x * (j / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k))) by A17, XCMPLX_1:77 .= x * (j / 1) by A16, XCMPLX_1:60 .= x * j ; then reconsider i = y as Element of NAT ; x in Y ; then consider l being Element of NAT such that A19: x = l and A20: (Sgm (NatDivisors n0)) . k,l are_relative_prime and A21: l >= 1 and A22: l <= (Sgm (NatDivisors n0)) . k ; A23: x * j <= ((Sgm (NatDivisors n0)) . k) * 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 Seg n0 by A17, A18, A23; A25: ((Sgm (NatDivisors n0)) . k) gcd l = 1 by A20, INT_2:def_3; n0 / ((Sgm (NatDivisors n0)) . k) = j / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k)) by A17, XCMPLX_1:77 .= j / 1 by A16, XCMPLX_1:60 ; then i gcd n0 = n0 / ((Sgm (NatDivisors n0)) . k) by A19, A17, A18, A25, EULER_1:5; hence y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by A11, A24; ::_thesis: verum end; assume y in { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } ; ::_thesis: y in rng f then consider i being Element of NAT such that A26: i = y and A27: ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) ; i gcd n0 divides i by INT_2:def_2; then consider x being Nat such that A28: i = (i gcd n0) * x by NAT_D:def_3; A29: y = (x * n0) / ((Sgm (NatDivisors n0)) . k) by A26, A27, A28, XCMPLX_1:74; reconsider x = x as Element of NAT by ORDINAL1:def_12; A30: (Sgm (NatDivisors n0)) . k <> 0 by A27, MOEBIUS1:39; A31: ((Sgm (NatDivisors n0)) . k) * (i gcd n0) = n0 / (((Sgm (NatDivisors n0)) . k) / ((Sgm (NatDivisors n0)) . k)) by A27, XCMPLX_1:81 .= n0 / 1 by A30, XCMPLX_1:60 ; then A32: (Sgm (NatDivisors n0)) . k,x are_relative_prime by A27, A28, A30, 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 <= (Sgm (NatDivisors n0)) . k by A27, A28, A30, A31, XREAL_1:68; then x in dom f by A13, A32, A33; then reconsider x = x as Element of Y by A13; y = f . x by A13, A29; hence y in rng f by A13, FUNCT_1:def_3; ::_thesis: verum end; then A34: rng f = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by TARSKI:1; 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 ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume x1 in dom f ; ::_thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) then reconsider x19 = x1 as Element of Y by A13; assume x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) then reconsider x29 = x2 as Element of Y by A13; assume A35: f . x1 = f . x2 ; ::_thesis: x1 = x2 A36: H1(x19) = f . x19 by A13 .= H1(x29) by A13, A35 ; x19 * (n0 / ((Sgm (NatDivisors n0)) . k)) = (x19 * n0) / ((Sgm (NatDivisors n0)) . k) by XCMPLX_1:74 .= x29 * (n0 / ((Sgm (NatDivisors n0)) . k)) by A36, XCMPLX_1:74 ; hence x1 = x2 by A12, XCMPLX_1:5; ::_thesis: verum end; then f is one-to-one by FUNCT_1:def_4; then A37: Y, { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } are_equipotent by A13, A34, WELLORD2:def_4; fp . ((Sgm (NatDivisors n0)) . k) = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & (Sgm (NatDivisors n0)) . k in NatDivisors n0 & h = (Sgm (NatDivisors n0)) . k & i gcd n0 = n0 / h ) } by A3, A7, A11; then card (fp . ((Sgm (NatDivisors n0)) . k)) = card Y by A37, CARD_1:5; then (Card fp) . ((Sgm (NatDivisors n0)) . k) = Euler ((Sgm (NatDivisors n0)) . k) by A7, A11, CARD_3:def_2; then A38: (Card fp) . ((Sgm (NatDivisors n0)) . k) = Euler_phi . ((Sgm (NatDivisors n0)) . k) by Def7; ((Card fp) * (Sgm (NatDivisors n0))) . k = (Card fp) . ((Sgm (NatDivisors n0)) . k) by A10, FUNCT_1:12; hence ((Card fp) * (Sgm (NatDivisors n0))) . k = (Euler_phi * (Sgm (NatDivisors n0))) . k by A8, A10, A38, FUNCT_1:12; ::_thesis: verum 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 set 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 set ; ::_thesis: ( x in NatDivisors n0 iff ( x in Seg n0 & not x in (Card fp) " {0} ) ) A42: y in {0} by TARSKI:def_1; hereby ::_thesis: ( x in Seg n0 & not x in (Card fp) " {0} implies x in NatDivisors n0 ) assume A43: x in NatDivisors n0 ; ::_thesis: ( x in Seg n0 & not x in (Card fp) " {0} ) then reconsider k = x as Element of NAT ; thus x in Seg n0 by A4, A43; ::_thesis: not x in (Card fp) " {0} assume x in (Card fp) " {0} ; ::_thesis: contradiction then consider y being set 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 being 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 Seg n0 by A47, FINSEQ_1:1; 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 Seg n0 & k in NatDivisors n0 & h = k & i9 gcd n0 = n0 / h ) } by A43, A49; hence contradiction by A3, A4, A43, A45; ::_thesis: verum end; assume A51: x in Seg n0 ; ::_thesis: ( x in (Card fp) " {0} or x in NatDivisors 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 Seg n0 & k in NatDivisors n0 & h = k & i9 gcd n0 = n0 / h ) } by A3, A51; assume A53: not x in (Card fp) " {0} ; ::_thesis: x in NatDivisors n0 assume A54: not x in NatDivisors n0 ; ::_thesis: contradiction fp . k = {} proof assume fp . k <> {} ; ::_thesis: contradiction then consider x9 being set such that A55: x9 in fp . k by XBOOLE_0:def_1; ex i being Element of NAT st ( x9 = i & ex h being Nat st ( i in Seg n0 & k in NatDivisors n0 & h = k & i gcd n0 = n0 / h ) ) by A52, A55; hence contradiction by A54; ::_thesis: verum 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; ::_thesis: verum 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; ::_thesis: ( d in dom fp & e in dom fp & d <> e implies fp . d misses fp . e ) assume d in dom fp ; ::_thesis: ( not e in dom fp or not d <> e or fp . d misses fp . e ) then A60: fp . d = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & d in NatDivisors n0 & h = d & i gcd n0 = n0 / h ) } by A3; assume e in dom fp ; ::_thesis: ( not d <> e or fp . d misses fp . e ) then A61: fp . e = { i where i is Element of NAT : ex h being Nat st ( i in Seg n0 & e in NatDivisors n0 & h = e & i gcd n0 = n0 / h ) } by A3; assume A62: d <> e ; ::_thesis: fp . d misses fp . e assume not fp . d misses fp . e ; ::_thesis: contradiction then (fp . d) /\ (fp . e) <> {} by XBOOLE_0:def_7; then consider x being set 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 being Element of NAT st ( x = i1 & ex h being Nat st ( i1 in Seg n0 & 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 being Element of NAT st ( x = i2 & ex h being Nat st ( i2 in Seg n0 & 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; ::_thesis: verum end; A65: for x being set holds ( x in union (rng fp) iff x in Seg n0 ) proof let x be set ; ::_thesis: ( x in union (rng fp) iff x in Seg n0 ) thus ( x in union (rng fp) implies x in Seg n0 ) ; ::_thesis: ( x in Seg n0 implies x in union (rng fp) ) assume A66: x in Seg n0 ; ::_thesis: x in union (rng fp) then reconsider i = x as Nat ; i gcd n0 divides n0 by NAT_D:def_5; then consider h being 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, FINSEQ_1:1; then A74: fp . h in rng fp by FUNCT_1:3; A75: fp . h = { i9 where i9 is Element of NAT : ex h9 being Nat st ( i9 in Seg n0 & 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 fp . h by A66, A71, A75; hence x in union (rng fp) by A74, TARSKI:def_4; ::_thesis: verum end; len fp = len fp ; then card (union (rng fp)) = Sum (Card fp) by A59, INT_5:48; then A76: card (Seg n0) = Sum (Card fp) by A65, TARSKI:1; card (Seg n0) = card n0 by FINSEQ_1:55; then n0 = Sum (Card fp) by A76, CARD_1:def_2; then Sum (Func_Seq (Euler_phi,(Sgm (NatDivisors n0)))) = n0 by A58, A39, BHSP_5:def_4; hence Sum (Euler_phi | (NatDivisors n0)) = n0 by A40, A57, Th24; ::_thesis: verum end;