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