:: MOEBIUS1 semantic presentation
begin
Lm1: for X, Y, Z, x being set st X misses Y & x in X /\ Z holds
not x in Y /\ Z
proof
let X, Y, Z, x be set ; ::_thesis: ( X misses Y & x in X /\ Z implies not x in Y /\ Z )
assume that
A1: X misses Y and
A2: x in X /\ Z ; ::_thesis: not x in Y /\ Z
X /\ Z misses Y /\ Z by A1, XBOOLE_1:76;
hence not x in Y /\ Z by A2, XBOOLE_0:3; ::_thesis: verum
end;
scheme :: MOEBIUS1:sch 1
LambdaNATC{ F1() -> Element of NAT , F2() -> set , F3( set ) -> set } :
ex f being Function of NAT,F2() st
( f . 0 = F1() & ( for x being non zero Element of NAT holds f . x = F3(x) ) )
provided
A1: F1() in F2() and
A2: for x being non zero Element of NAT holds F3(x) in F2()
proof
deffunc H1( set ) -> Element of NAT = F1();
defpred S1[ set ] means $1 = 0 ;
A3: for x being set st x in NAT holds
( ( S1[x] implies H1(x) in F2() ) & ( not S1[x] implies F3(x) in F2() ) ) by A1, A2;
ex f being Function of NAT,F2() st
for x being set st x in NAT holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = F3(x) ) ) from FUNCT_2:sch_5(A3);
then consider f being Function of NAT,F2() such that
A4: for x being set st x in NAT holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = F3(x) ) ) ;
take f ; ::_thesis: ( f . 0 = F1() & ( for x being non zero Element of NAT holds f . x = F3(x) ) )
thus f . 0 = F1() by A4; ::_thesis: for x being non zero Element of NAT holds f . x = F3(x)
let x be non zero Element of NAT ; ::_thesis: f . x = F3(x)
thus f . x = F3(x) by A4; ::_thesis: verum
end;
registration
cluster non zero epsilon-transitive epsilon-connected ordinal natural V11() real V13() non prime finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() for Element of NAT ;
existence
ex b1 being Element of NAT st
( not b1 is prime & not b1 is zero ) by INT_2:29;
end;
theorem Th1: :: MOEBIUS1:1
for n being non zero Nat st n <> 1 holds
n >= 2
proof
let n be non zero Nat; ::_thesis: ( n <> 1 implies n >= 2 )
assume A1: n <> 1 ; ::_thesis: n >= 2
assume n < 2 ; ::_thesis: contradiction
then n < 1 + 1 ;
then n <= 0 + 1 by NAT_1:13;
hence contradiction by A1, NAT_1:8; ::_thesis: verum
end;
theorem :: MOEBIUS1:2
for k, n, i being Nat st 1 <= k holds
( i in Seg n iff k * i in Seg (k * n) )
proof
let k, n, i be Nat; ::_thesis: ( 1 <= k implies ( i in Seg n iff k * i in Seg (k * n) ) )
assume A1: 1 <= k ; ::_thesis: ( i in Seg n iff k * i in Seg (k * n) )
hereby ::_thesis: ( k * i in Seg (k * n) implies i in Seg n )
assume A2: i in Seg n ; ::_thesis: k * i in Seg (k * n)
then i <= n by FINSEQ_1:1;
then A3: k * i <= k * n by NAT_1:4;
1 <= i by A2, FINSEQ_1:1;
then 1 * 1 <= k * i by A1, XREAL_1:66;
hence k * i in Seg (k * n) by A3, FINSEQ_1:1; ::_thesis: verum
end;
assume A4: k * i in Seg (k * n) ; ::_thesis: i in Seg n
then 0 < i by FINSEQ_1:1;
then A5: 0 + 1 <= i by NAT_1:13;
k * i <= k * n by A4, FINSEQ_1:1;
then i <= n by A1, XREAL_1:68;
hence i in Seg n by A5, FINSEQ_1:1; ::_thesis: verum
end;
theorem :: MOEBIUS1:3
for m, n being Element of NAT holds
( not m,n are_relative_prime or m > 0 or n > 0 )
proof
let a, b be Element of NAT ; ::_thesis: ( not a,b are_relative_prime or a > 0 or b > 0 )
assume a,b are_relative_prime ; ::_thesis: ( a > 0 or b > 0 )
then ( a is odd or b is odd ) by PYTHTRIP:10;
hence ( a > 0 or b > 0 ) by ABIAN:12; ::_thesis: verum
end;
Lm2: for n being Nat st n <> 1 holds
ex p being Prime st p divides n
proof
let n be Nat; ::_thesis: ( n <> 1 implies ex p being Prime st p divides n )
assume A1: n <> 1 ; ::_thesis: ex p being Prime st p divides n
percases ( n is zero or not n is zero ) ;
suppose n is zero ; ::_thesis: ex p being Prime st p divides n
hence ex p being Prime st p divides n by INT_2:28, NAT_D:6; ::_thesis: verum
end;
suppose not n is zero ; ::_thesis: ex p being Prime st p divides n
then ex p being Element of NAT st
( p is prime & p divides n ) by A1, Th1, INT_2:31;
hence ex p being Prime st p divides n ; ::_thesis: verum
end;
end;
end;
theorem Th4: :: MOEBIUS1:4
for n being non prime Element of NAT st n <> 1 holds
ex p being Prime st
( p divides n & p <> n )
proof
let n be non prime Element of NAT ; ::_thesis: ( n <> 1 implies ex p being Prime st
( p divides n & p <> n ) )
assume n <> 1 ; ::_thesis: ex p being Prime st
( p divides n & p <> n )
then ex p being Prime st p divides n by Lm2;
hence ex p being Prime st
( p divides n & p <> n ) ; ::_thesis: verum
end;
theorem Th5: :: MOEBIUS1:5
for n being Nat st n <> 1 holds
ex p being Prime st p divides n
proof
let n be Nat; ::_thesis: ( n <> 1 implies ex p being Prime st p divides n )
A1: n in NAT by ORDINAL1:def_12;
assume A2: n <> 1 ; ::_thesis: ex p being Prime st p divides n
percases ( n is Prime or not n is Prime ) ;
suppose n is Prime ; ::_thesis: ex p being Prime st p divides n
hence ex p being Prime st p divides n ; ::_thesis: verum
end;
suppose n is not Prime ; ::_thesis: ex p being Prime st p divides n
then ex p being Prime st
( p divides n & p <> n ) by A1, A2, Th4;
hence ex p being Prime st p divides n ; ::_thesis: verum
end;
end;
end;
theorem Th6: :: MOEBIUS1:6
for p being Prime
for n being non zero Nat holds
( p divides n iff p |-count n > 0 )
proof
let p be Prime; ::_thesis: for n being non zero Nat holds
( p divides n iff p |-count n > 0 )
let n be non zero Nat; ::_thesis: ( p divides n iff p |-count n > 0 )
A1: p <> 1 by INT_2:def_4;
thus ( p divides n implies p |-count n > 0 ) ::_thesis: ( p |-count n > 0 implies p divides n )
proof
assume A2: p divides n ; ::_thesis: p |-count n > 0
p |-count n >= 1
proof
assume p |-count n < 1 ; ::_thesis: contradiction
then p |-count n = 0 by NAT_1:25;
then not p |^ (0 + 1) divides n by A1, NAT_3:def_7;
hence contradiction by A2, NEWTON:5; ::_thesis: verum
end;
hence p |-count n > 0 ; ::_thesis: verum
end;
assume p |-count n > 0 ; ::_thesis: p divides n
then reconsider d = p |-count n as non zero Nat ;
p <> 1 by INT_2:def_4;
then p |^ d divides n by NAT_3:def_7;
then p |^ (0 + 1) divides n by NAT_3:4;
hence p divides n by NEWTON:5; ::_thesis: verum
end;
theorem Th7: :: MOEBIUS1:7
support (ppf 1) = {}
proof
support (pfexp 1) = {} ;
hence support (ppf 1) = {} by NAT_3:def_9; ::_thesis: verum
end;
theorem Th8: :: MOEBIUS1:8
for p being Prime holds support (ppf p) = {p}
proof
let p be Prime; ::_thesis: support (ppf p) = {p}
support (pfexp p) = {p} by NAT_3:43;
hence support (ppf p) = {p} by NAT_3:def_9; ::_thesis: verum
end;
theorem Th9: :: MOEBIUS1:9
for n, m being Nat
for p being Prime st n <> 0 & m <= p |-count n holds
p |^ m divides n
proof
let n, m be Nat; ::_thesis: for p being Prime st n <> 0 & m <= p |-count n holds
p |^ m divides n
let p be Prime; ::_thesis: ( n <> 0 & m <= p |-count n implies p |^ m divides n )
assume that
A1: n <> 0 and
A2: m <= p |-count n ; ::_thesis: p |^ m divides n
A3: p |^ m divides p |^ (p |-count n) by A2, NEWTON:89;
p > 1 by INT_2:def_4;
then p |^ (p |-count n) divides n by A1, NAT_3:def_7;
hence p |^ m divides n by A3, NAT_D:4; ::_thesis: verum
end;
theorem Th10: :: MOEBIUS1:10
for a being Element of NAT
for p being Prime st p |^ 2 divides a holds
p divides a
proof
let a be Element of NAT ; ::_thesis: for p being Prime st p |^ 2 divides a holds
p divides a
let p be Prime; ::_thesis: ( p |^ 2 divides a implies p divides a )
assume p |^ 2 divides a ; ::_thesis: p divides a
then consider t being Nat such that
A1: a = (p |^ 2) * t by NAT_D:def_3;
a = (p * p) * t by A1, WSIERP_1:1
.= p * (p * t) ;
hence p divides a by NAT_D:def_3; ::_thesis: verum
end;
theorem Th11: :: MOEBIUS1:11
for p being prime Element of NAT
for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n
proof
let p be prime Element of NAT ; ::_thesis: for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n
let a, b be non zero Element of NAT ; ::_thesis: ( a,b are_relative_prime & p |^ 2 divides a * b & not p |^ 2 divides a implies p |^ 2 divides b )
assume that
A1: a,b are_relative_prime and
A2: p |^ 2 divides a * b ; ::_thesis: ( p |^ 2 divides a or p |^ 2 divides b )
p divides p |^ 2 by NAT_3:3;
then A3: p divides a * b by A2, NAT_D:4;
percases ( p divides a or p divides b ) by A3, NEWTON:80;
suppose p divides a ; ::_thesis: ( p |^ 2 divides a or p |^ 2 divides b )
then A4: not p divides b by A1, PYTHTRIP:def_2;
p,b are_relative_prime
proof
reconsider k = p gcd b as Element of NAT by ORDINAL1:def_12;
assume not p,b are_relative_prime ; ::_thesis: contradiction
then A5: k <> 1 by INT_2:def_3;
( k divides p & k divides b ) by NAT_D:def_5;
hence contradiction by A4, A5, INT_2:def_4; ::_thesis: verum
end;
then p * p,b are_relative_prime by EULER_1:14;
then p |^ 2,b are_relative_prime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; ::_thesis: verum
end;
suppose p divides b ; ::_thesis: ( p |^ 2 divides a or p |^ 2 divides b )
then A6: not p divides a by A1, PYTHTRIP:def_2;
p,a are_relative_prime
proof
reconsider k = p gcd a as Element of NAT by ORDINAL1:def_12;
assume not p,a are_relative_prime ; ::_thesis: contradiction
then A7: k <> 1 by INT_2:def_3;
( k divides p & k divides a ) by NAT_D:def_5;
hence contradiction by A6, A7, INT_2:def_4; ::_thesis: verum
end;
then p * p,a are_relative_prime by EULER_1:14;
then p |^ 2,a are_relative_prime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; ::_thesis: verum
end;
end;
end;
theorem Th12: :: MOEBIUS1:12
for n being Nat
for N being Rbag of NAT st support N = {n} holds
Sum N = N . n
proof
let n be Nat; ::_thesis: for N being Rbag of NAT st support N = {n} holds
Sum N = N . n
let N be Rbag of NAT ; ::_thesis: ( support N = {n} implies Sum N = N . n )
reconsider F = <*(N . n)*> as FinSequence of REAL ;
assume A1: support N = {n} ; ::_thesis: Sum N = N . n
then {n} c= dom N by PRE_POLY:37;
then n in dom N by ZFMISC_1:31;
then A2: F = N * <*n*> by FINSEQ_2:34
.= N * (canFS (support N)) by A1, UPROOTS:4 ;
Sum F = N . n by FINSOP_1:11;
hence Sum N = N . n by A2, UPROOTS:def_3; ::_thesis: verum
end;
registration
cluster canFS {} -> empty ;
coherence
canFS {} is empty ;
end;
theorem :: MOEBIUS1:13
for n being Nat
for p being Prime st p divides n holds
{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
proof
let n be Nat; ::_thesis: for p being Prime st p divides n holds
{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
let p be Prime; ::_thesis: ( p divides n implies { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )
assume A1: p divides n ; ::_thesis: { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
set B = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ;
set A = { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ;
thus { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } c= { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } :: according to XBOOLE_0:def_10 ::_thesis: { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } c= { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } or x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )
assume x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ; ::_thesis: x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
then consider d being Element of NAT such that
A2: d = x and
A3: d > 0 and
A4: d divides n and
A5: p divides d ;
consider d1 being Nat such that
A6: d = p * d1 by A5, NAT_D:def_3;
consider d2 being Nat such that
A7: n = d * d2 by A4, NAT_D:def_3;
n = p * (d1 * d2) by A6, A7;
then p divides n by NAT_D:def_3;
then p * (n div p) = p * (d1 * d2) by A6, A7, NAT_D:3;
then n div p = d1 * d2 by XCMPLX_1:5;
then A8: d1 divides n div p by NAT_D:def_3;
( d1 in NAT & d1 > 0 ) by A3, A6, ORDINAL1:def_12;
hence x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } by A2, A6, A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } or x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } )
assume x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ; ::_thesis: x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }
then consider d being Element of NAT such that
A9: p * d = x and
A10: d > 0 and
A11: d divides n div p ;
reconsider d1 = x as Element of NAT by A9;
consider d2 being Nat such that
A12: n div p = d * d2 by A11, NAT_D:def_3;
(n div p) * p = (d * d2) * p by A12;
then n = d2 * (d * p) by A1, NAT_D:3;
then A13: d1 divides n by A9, NAT_D:def_3;
p divides d1 by A9, NAT_D:def_3;
hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A10, A13; ::_thesis: verum
end;
theorem Th14: :: MOEBIUS1:14
for n being non zero Nat ex k being Element of NAT st support (ppf n) c= Seg k
proof
let n be non zero Nat; ::_thesis: ex k being Element of NAT st support (ppf n) c= Seg k
A1: support (ppf n) = support (pfexp n) by NAT_3:def_9;
percases ( support (ppf n) is empty or not support (ppf n) is empty ) ;
supposeA2: support (ppf n) is empty ; ::_thesis: ex k being Element of NAT st support (ppf n) c= Seg k
take 0 ; ::_thesis: support (ppf n) c= Seg 0
thus support (ppf n) c= Seg 0 by A2; ::_thesis: verum
end;
suppose not support (ppf n) is empty ; ::_thesis: ex k being Element of NAT st support (ppf n) c= Seg k
then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1;
take max S ; ::_thesis: ( max S is Element of REAL & max S is Element of NAT & support (ppf n) c= Seg (max S) )
A3: support (ppf n) c= Seg (max S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf n) or x in Seg (max S) )
assume A4: x in support (ppf n) ; ::_thesis: x in Seg (max S)
then reconsider m = x as Nat ;
x is Prime by A1, A4, NAT_3:34;
then A5: 1 <= m by INT_2:def_4;
m <= max S by A4, XXREAL_2:def_8;
hence x in Seg (max S) by A5, FINSEQ_1:1; ::_thesis: verum
end;
max S is Element of NAT by ORDINAL1:def_12;
hence ( max S is Element of REAL & max S is Element of NAT & support (ppf n) c= Seg (max S) ) by A3; ::_thesis: verum
end;
end;
end;
theorem Th15: :: MOEBIUS1:15
for n being non zero Element of NAT
for p being Prime st not p in support (ppf n) holds
p |-count n = 0
proof
let n be non zero Element of NAT ; ::_thesis: for p being Prime st not p in support (ppf n) holds
p |-count n = 0
let p be Prime; ::_thesis: ( not p in support (ppf n) implies p |-count n = 0 )
assume A1: not p in support (ppf n) ; ::_thesis: p |-count n = 0
assume p |-count n <> 0 ; ::_thesis: contradiction
then (ppf n) . p = p |^ (p |-count n) by NAT_3:56;
hence contradiction by A1, PRE_POLY:def_7; ::_thesis: verum
end;
theorem Th16: :: MOEBIUS1:16
for k being Element of NAT
for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k holds
k + 1 is Prime
proof
let k be Element of NAT ; ::_thesis: for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k holds
k + 1 is Prime
let n be non zero Element of NAT ; ::_thesis: ( support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k implies k + 1 is Prime )
assume that
A1: support (ppf n) c= Seg (k + 1) and
A2: not support (ppf n) c= Seg k ; ::_thesis: k + 1 is Prime
k + 1 in support (ppf n)
proof
assume not k + 1 in support (ppf n) ; ::_thesis: contradiction
then A3: {(k + 1)} misses support (ppf n) by ZFMISC_1:50;
(support (ppf n)) \ {(k + 1)} c= (Seg (k + 1)) \ {(k + 1)} by A1, XBOOLE_1:33;
then support (ppf n) c= (Seg (k + 1)) \ {(k + 1)} by A3, XBOOLE_1:83;
hence contradiction by A2, FINSEQ_1:10; ::_thesis: verum
end;
then k + 1 in support (pfexp n) by NAT_3:def_9;
hence k + 1 is Prime by NAT_3:34; ::_thesis: verum
end;
theorem Th17: :: MOEBIUS1:17
for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds
support (ppf m) c= support (ppf n)
proof
let m, n be non zero Nat; ::_thesis: ( ( for p being Prime holds p |-count m <= p |-count n ) implies support (ppf m) c= support (ppf n) )
assume A1: for p being Prime holds p |-count m <= p |-count n ; ::_thesis: support (ppf m) c= support (ppf n)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf m) or x in support (ppf n) )
assume A2: x in support (ppf m) ; ::_thesis: x in support (ppf n)
then x in support (pfexp m) by NAT_3:def_9;
then reconsider p = x as Prime by NAT_3:34;
(ppf m) . p <> 0 by A2, PRE_POLY:def_7;
then p |-count m <> 0 by NAT_3:55;
then p |-count n > 0 by A1;
then (ppf n) . p = p |^ (p |-count n) by NAT_3:56;
hence x in support (ppf n) by PRE_POLY:def_7; ::_thesis: verum
end;
theorem Th18: :: MOEBIUS1:18
for k being Element of NAT
for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds
ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
proof
let k be Element of NAT ; ::_thesis: for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds
ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
let n be non zero Element of NAT ; ::_thesis: ( support (ppf n) c= Seg (k + 1) implies ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) )
assume A1: support (ppf n) c= Seg (k + 1) ; ::_thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
percases ( support (ppf n) c= Seg k or not support (ppf n) c= Seg k ) ;
supposeA2: support (ppf n) c= Seg k ; ::_thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
take n ; ::_thesis: ex e being Element of NAT st
( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )
take e = 0 ; ::_thesis: ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )
(k + 1) |^ e = 1 by NEWTON:4;
hence ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) ) by A2; ::_thesis: verum
end;
supposeA3: not support (ppf n) c= Seg k ; ::_thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
now__::_thesis:_k_+_1_in_support_(ppf_n)
assume A4: not k + 1 in support (ppf n) ; ::_thesis: contradiction
support (ppf n) c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf n) or x in Seg k )
assume A5: x in support (ppf n) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
x in support (pfexp n) by A5, NAT_3:def_9;
then x is Prime by NAT_3:34;
then A6: 1 <= m by INT_2:def_4;
m <= k + 1 by A1, A5, FINSEQ_1:1;
then m < k + 1 by A4, A5, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A6, FINSEQ_1:1; ::_thesis: verum
end;
hence contradiction by A3; ::_thesis: verum
end;
then k + 1 in support (pfexp n) by NAT_3:def_9;
then A7: r is Prime by NAT_3:34;
then A8: r > 1 by INT_2:def_4;
then r |^ (r |-count n) divides n by NAT_3:def_7;
then consider t being Nat such that
A9: n = (r |^ (r |-count n)) * t by NAT_D:def_3;
reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A9, ORDINAL1:def_12;
A10: support (ppf t) = support (pfexp t) by NAT_3:def_9;
A11: support (ppf t) c= Seg k
proof
set f = r |-count t;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf t) or x in Seg k )
assume A12: x in support (ppf t) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
A13: x in support (pfexp t) by A12, NAT_3:def_9;
A14: now__::_thesis:_not_m_=_r
assume A15: m = r ; ::_thesis: contradiction
(pfexp t) . r = r |-count t by A7, NAT_3:def_8;
then r |-count t <> 0 by A13, A15, PRE_POLY:def_7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A16: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A8, NAT_3:def_7;
then consider u being Nat such that
A17: t = (r |^ (r |-count t)) * u by NAT_D:def_3;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
n = s * (((r |^ g) * r) * u) by A9, A16, A17, NEWTON:6
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def_3;
hence contradiction by A8, NAT_3:def_7; ::_thesis: verum
end;
support (pfexp t) c= support (pfexp n) by A9, NAT_3:45;
then support (ppf t) c= support (ppf n) by A10, NAT_3:def_9;
then m in support (ppf n) by A12;
then m <= k + 1 by A1, FINSEQ_1:1;
then m < r by A14, XXREAL_0:1;
then A18: m <= k by NAT_1:13;
x is Prime by A13, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A18, FINSEQ_1:1; ::_thesis: verum
end;
A19: r |-count n <> 0
proof
assume r |-count n = 0 ; ::_thesis: contradiction
then n = 1 * t by A9, NEWTON:4;
hence contradiction by A3, A11; ::_thesis: verum
end;
take m = t; ::_thesis: ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
take e = (k + 1) |-count n; ::_thesis: ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )
support (ppf s) = support (pfexp s) by NAT_3:def_9;
then A20: support (ppf s) = {r} by A7, A19, NAT_3:42;
A21: now__::_thesis:_not_support_(ppf_s)_meets_support_(ppf_t)
assume support (ppf s) meets support (ppf t) ; ::_thesis: contradiction
then consider x being set such that
A22: x in support (ppf s) and
A23: x in support (ppf t) by XBOOLE_0:3;
x = r by A20, A22, TARSKI:def_1;
then r <= k by A11, A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )
proof
let p be Prime; ::_thesis: ( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )
hereby ::_thesis: ( not p in support (ppf m) implies p |-count m <= p |-count n )
assume p in support (ppf m) ; ::_thesis: p |-count m = p |-count n
then not p in support (ppf s) by A21, XBOOLE_0:3;
then A24: p |-count s = 0 by Th15;
p |-count n = (p |-count (r |^ e)) + (p |-count t) by A9, NAT_3:28;
hence p |-count m = p |-count n by A24; ::_thesis: verum
end;
assume not p in support (ppf m) ; ::_thesis: p |-count m <= p |-count n
hence p |-count m <= p |-count n by Th15; ::_thesis: verum
end;
hence ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) by A9, A11; ::_thesis: verum
end;
end;
end;
theorem Th19: :: MOEBIUS1:19
for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds
m divides n
proof
defpred S1[ Element of NAT ] means for k, l being non zero Element of NAT st support (ppf k) c= Seg $1 & support (ppf l) c= Seg $1 & ( for p being Prime holds p |-count k <= p |-count l ) holds
k divides l;
let m, n be non zero Nat; ::_thesis: ( ( for p being Prime holds p |-count m <= p |-count n ) implies m divides n )
A1: ( m is Element of NAT & n is Element of NAT ) by ORDINAL1:def_12;
consider k being Element of NAT such that
A2: support (ppf n) c= Seg k by Th14;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let m, n be non zero Element of NAT ; ::_thesis: ( support (ppf m) c= Seg (k + 1) & support (ppf n) c= Seg (k + 1) & ( for p being Prime holds p |-count m <= p |-count n ) implies m divides n )
assume that
A5: support (ppf m) c= Seg (k + 1) and
A6: support (ppf n) c= Seg (k + 1) and
A7: for p being Prime holds p |-count m <= p |-count n ; ::_thesis: m divides n
percases ( ( not support (ppf n) c= Seg k & support (ppf m) c= Seg k ) or ( not support (ppf n) c= Seg k & not support (ppf m) c= Seg k ) or support (ppf n) c= Seg k ) ;
supposeA8: ( not support (ppf n) c= Seg k & support (ppf m) c= Seg k ) ; ::_thesis: m divides n
reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
now__::_thesis:_k_+_1_in_support_(ppf_n)
assume A9: not k + 1 in support (ppf n) ; ::_thesis: contradiction
support (ppf n) c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf n) or x in Seg k )
assume A10: x in support (ppf n) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
x in support (pfexp n) by A10, NAT_3:def_9;
then x is Prime by NAT_3:34;
then A11: 1 <= m by INT_2:def_4;
m <= k + 1 by A6, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A11, FINSEQ_1:1; ::_thesis: verum
end;
hence contradiction by A8; ::_thesis: verum
end;
then A12: k + 1 in support (pfexp n) by NAT_3:def_9;
then A13: r is Prime by NAT_3:34;
then A14: r > 1 by INT_2:def_4;
then r |^ (r |-count n) divides n by NAT_3:def_7;
then consider t being Nat such that
A15: n = (r |^ (r |-count n)) * t by NAT_D:def_3;
A16: t divides n by A15, NAT_D:def_3;
reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A15, ORDINAL1:def_12;
A17: support (ppf t) = support (pfexp t) by NAT_3:def_9;
A18: support (ppf t) c= Seg k
proof
set f = r |-count t;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf t) or x in Seg k )
assume A19: x in support (ppf t) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
A20: x in support (pfexp t) by A19, NAT_3:def_9;
A21: now__::_thesis:_not_m_=_r
assume A22: m = r ; ::_thesis: contradiction
(pfexp t) . r = r |-count t by A13, NAT_3:def_8;
then r |-count t <> 0 by A20, A22, PRE_POLY:def_7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A23: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A14, NAT_3:def_7;
then consider u being Nat such that
A24: t = (r |^ (r |-count t)) * u by NAT_D:def_3;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
n = s * (((r |^ g) * r) * u) by A15, A23, A24, NEWTON:6
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def_3;
hence contradiction by A14, NAT_3:def_7; ::_thesis: verum
end;
support (pfexp t) c= support (pfexp n) by A15, NAT_3:45;
then support (ppf t) c= support (ppf n) by A17, NAT_3:def_9;
then m in support (ppf n) by A19;
then m <= k + 1 by A6, FINSEQ_1:1;
then m < r by A21, XXREAL_0:1;
then A25: m <= k by NAT_1:13;
x is Prime by A20, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A25, FINSEQ_1:1; ::_thesis: verum
end;
A26: support (ppf s) = support (pfexp s) by NAT_3:def_9;
r |-count n <> 0
proof
assume r |-count n = 0 ; ::_thesis: contradiction
then not r divides n by A14, NAT_3:27;
hence contradiction by A12, NAT_3:36; ::_thesis: verum
end;
then A27: support (ppf s) = {r} by A13, A26, NAT_3:42;
A28: now__::_thesis:_not_support_(ppf_s)_meets_support_(ppf_t)
assume support (ppf s) meets support (ppf t) ; ::_thesis: contradiction
then consider x being set such that
A29: x in support (ppf s) and
A30: x in support (ppf t) by XBOOLE_0:3;
x = r by A27, A29, TARSKI:def_1;
then r <= k by A18, A30, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
A31: ( support (ppf m) c= Seg k & support (ppf t) c= Seg k & ( for p being Prime holds p |-count m <= p |-count t ) implies m divides t ) by A4;
( support (ppf n) = support (pfexp n) & support (ppf t) = support (pfexp t) ) by NAT_3:def_9;
then A32: support (ppf n) = (support (ppf s)) \/ (support (ppf t)) by A15, A26, NAT_3:46;
A33: for p being Prime holds p |-count m <= p |-count t
proof
let p be Prime; ::_thesis: p |-count m <= p |-count t
A34: p |-count n = (p |-count (r |^ (r |-count n))) + (p |-count t) by A15, NAT_3:28;
percases ( p in support (ppf n) or not p in support (ppf n) ) ;
supposeA35: p in support (ppf n) ; ::_thesis: p |-count m <= p |-count t
percases ( p in support (ppf s) or p in support (ppf t) ) by A32, A35, XBOOLE_0:def_3;
suppose p in support (ppf s) ; ::_thesis: p |-count m <= p |-count t
then A36: p = k + 1 by A27, TARSKI:def_1;
percases ( p in support (ppf m) or not p in support (ppf m) ) ;
suppose p in support (ppf m) ; ::_thesis: p |-count m <= p |-count t
then p <= k by A8, FINSEQ_1:1;
hence p |-count m <= p |-count t by A36, NAT_1:13; ::_thesis: verum
end;
suppose not p in support (ppf m) ; ::_thesis: p |-count m <= p |-count t
hence p |-count m <= p |-count t by Th15; ::_thesis: verum
end;
end;
end;
suppose p in support (ppf t) ; ::_thesis: p |-count m <= p |-count t
then not p in support (ppf s) by A28, XBOOLE_0:3;
then p |-count s = 0 by Th15;
hence p |-count m <= p |-count t by A7, A34; ::_thesis: verum
end;
end;
end;
suppose not p in support (ppf n) ; ::_thesis: p |-count m <= p |-count t
then p |-count n = 0 by Th15;
hence p |-count m <= p |-count t by A7; ::_thesis: verum
end;
end;
end;
then support (ppf m) c= support (ppf t) by Th17;
hence m divides n by A16, A18, A33, A31, NAT_D:4, XBOOLE_1:1; ::_thesis: verum
end;
supposeA37: ( not support (ppf n) c= Seg k & not support (ppf m) c= Seg k ) ; ::_thesis: m divides n
then reconsider w = k + 1 as Prime by A5, Th16;
consider m1 being non zero Element of NAT , e1 being Element of NAT such that
A38: support (ppf m1) c= Seg k and
A39: m = m1 * ((k + 1) |^ e1) and
A40: for p being Prime holds
( ( p in support (ppf m1) implies p |-count m1 = p |-count m ) & ( not p in support (ppf m1) implies p |-count m1 <= p |-count m ) ) by A5, Th18;
consider m2 being non zero Element of NAT , e2 being Element of NAT such that
A41: support (ppf m2) c= Seg k and
A42: n = m2 * ((k + 1) |^ e2) and
A43: for p being Prime holds
( ( p in support (ppf m2) implies p |-count m2 = p |-count n ) & ( not p in support (ppf m2) implies p |-count m2 <= p |-count n ) ) by A6, Th18;
A44: not w divides m2
proof
assume w divides m2 ; ::_thesis: contradiction
then w in support (pfexp m2) by NAT_3:37;
then w in support (ppf m2) by NAT_3:def_9;
then w <= k by A41, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
A45: k + 1 is Prime by A5, A37, Th16;
for p being Prime holds p |-count m1 <= p |-count m2
proof
let p be Prime; ::_thesis: p |-count m1 <= p |-count m2
percases ( ( p in support (ppf m1) & p in support (ppf m2) ) or ( not p in support (ppf m1) & p in support (ppf m2) ) or ( p in support (ppf m1) & not p in support (ppf m2) ) or ( not p in support (ppf m1) & not p in support (ppf m2) ) ) ;
suppose ( p in support (ppf m1) & p in support (ppf m2) ) ; ::_thesis: p |-count m1 <= p |-count m2
then ( p |-count m1 = p |-count m & p |-count m2 = p |-count n ) by A40, A43;
hence p |-count m1 <= p |-count m2 by A7; ::_thesis: verum
end;
suppose ( not p in support (ppf m1) & p in support (ppf m2) ) ; ::_thesis: p |-count m1 <= p |-count m2
hence p |-count m1 <= p |-count m2 by Th15; ::_thesis: verum
end;
supposeA46: ( p in support (ppf m1) & not p in support (ppf m2) ) ; ::_thesis: p |-count m1 <= p |-count m2
m1 divides m by A39, NAT_D:def_3;
then A47: p |-count m1 <= p |-count m by NAT_3:30;
A48: p > 1 by INT_2:def_4;
p in support (pfexp m1) by A46, NAT_3:def_9;
then p divides m1 by NAT_3:36;
then p |-count m1 <> 0 by A48, NAT_3:27;
then p |-count m1 > 0 ;
then p |-count n > 0 by A7, A47;
then A49: p divides n by A48, NAT_3:27;
p |-count m2 = 0 by A46, Th15;
then not p divides m2 by A48, NAT_3:27;
then p divides (k + 1) |^ e2 by A42, A49, NEWTON:80;
then p divides k + 1 by NAT_3:5;
then A50: p = k + 1 by A45, A48, INT_2:def_4;
k < k + 1 by NAT_1:13;
hence p |-count m1 <= p |-count m2 by A38, A46, A50, FINSEQ_1:1; ::_thesis: verum
end;
suppose ( not p in support (ppf m1) & not p in support (ppf m2) ) ; ::_thesis: p |-count m1 <= p |-count m2
hence p |-count m1 <= p |-count m2 by Th15; ::_thesis: verum
end;
end;
end;
then A51: m1 divides m2 by A4, A38, A41;
A52: not w divides m1
proof
assume w divides m1 ; ::_thesis: contradiction
then w in support (pfexp m1) by NAT_3:37;
then w in support (ppf m1) by NAT_3:def_9;
then w <= k by A38, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
A53: w > 1 by INT_2:def_4;
then w |-count (w |^ e2) = e2 by NAT_3:25;
then A54: w |-count n = (w |-count m2) + e2 by A42, NAT_3:28
.= 0 + e2 by A53, A44, NAT_3:27
.= e2 ;
w |-count (w |^ e1) = e1 by A53, NAT_3:25;
then w |-count m = (w |-count m1) + e1 by A39, NAT_3:28
.= 0 + e1 by A53, A52, NAT_3:27
.= e1 ;
then (k + 1) |^ e1 divides (k + 1) |^ e2 by A7, A54, NEWTON:89;
hence m divides n by A39, A42, A51, NAT_3:1; ::_thesis: verum
end;
supposeA55: support (ppf n) c= Seg k ; ::_thesis: m divides n
support (ppf m) c= support (ppf n) by A7, Th17;
then support (ppf m) c= Seg k by A55, XBOOLE_1:1;
hence m divides n by A4, A7, A55; ::_thesis: verum
end;
end;
end;
A56: S1[ 0 ]
proof
let k, l be non zero Element of NAT ; ::_thesis: ( support (ppf k) c= Seg 0 & support (ppf l) c= Seg 0 & ( for p being Prime holds p |-count k <= p |-count l ) implies k divides l )
assume that
A57: support (ppf k) c= Seg 0 and
support (ppf l) c= Seg 0 and
for p being Prime holds p |-count k <= p |-count l ; ::_thesis: k divides l
support (ppf k) = {} by A57, XBOOLE_1:3;
then A58: support (pfexp k) = {} by NAT_3:def_9;
percases ( k <> 1 or k = 1 ) ;
suppose k <> 1 ; ::_thesis: k divides l
then ex p being Prime st p divides k by Lm2;
hence k divides l by A58, NAT_3:37; ::_thesis: verum
end;
suppose k = 1 ; ::_thesis: k divides l
hence k divides l by NAT_D:6; ::_thesis: verum
end;
end;
end;
A59: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A56, A3);
assume A60: for p being Prime holds p |-count m <= p |-count n ; ::_thesis: m divides n
then support (ppf m) c= support (ppf n) by Th17;
then support (ppf m) c= Seg k by A2, XBOOLE_1:1;
hence m divides n by A60, A59, A2, A1; ::_thesis: verum
end;
begin
definition
let x be Nat;
attrx is square-containing means :Def1: :: MOEBIUS1:def 1
ex p being Prime st p |^ 2 divides x;
end;
:: deftheorem Def1 defines square-containing MOEBIUS1:def_1_:_
for x being Nat holds
( x is square-containing iff ex p being Prime st p |^ 2 divides x );
theorem Th20: :: MOEBIUS1:20
for n being Nat st ex p being non zero Nat st
( p <> 1 & p |^ 2 divides n ) holds
n is square-containing
proof
let n be Nat; ::_thesis: ( ex p being non zero Nat st
( p <> 1 & p |^ 2 divides n ) implies n is square-containing )
given p being non zero Nat such that A1: p <> 1 and
A2: p |^ 2 divides n ; ::_thesis: n is square-containing
consider r being Prime such that
A3: r divides p by A1, Lm2;
r |^ 2 divides p |^ 2 by A3, WSIERP_1:14;
then r |^ 2 divides n by A2, NAT_D:4;
hence n is square-containing by Def1; ::_thesis: verum
end;
notation
let x be Nat;
antonym square-free x for square-containing ;
end;
theorem Th21: :: MOEBIUS1:21
0 is square-containing
proof
set p = the Prime;
the Prime |^ 2 divides 0 by NAT_D:6;
hence 0 is square-containing by Def1; ::_thesis: verum
end;
theorem Th22: :: MOEBIUS1:22
1 is square-free
proof
assume 1 is square-containing ; ::_thesis: contradiction
then consider n being Prime such that
A1: n |^ 2 divides 1 by Def1;
n * n divides 1 by A1, WSIERP_1:1;
then ( n = 1 or n = - 1 ) by WSIERP_1:15, XCMPLX_1:182;
hence contradiction by INT_2:def_4; ::_thesis: verum
end;
theorem Th23: :: MOEBIUS1:23
for p being Prime holds p is square-free
proof
let p be Prime; ::_thesis: p is square-free
assume p is square-containing ; ::_thesis: contradiction
then consider n being Prime such that
A1: n |^ 2 divides p by Def1;
A2: n divides n |^ 2 by NAT_3:3;
then A3: n divides p by A1, NAT_D:4;
percases ( n = 1 or n = p ) by A3, INT_2:def_4;
suppose n = 1 ; ::_thesis: contradiction
hence contradiction by INT_2:def_4; ::_thesis: verum
end;
suppose n = p ; ::_thesis: contradiction
then n = n |^ 2 by A1, A2, NAT_D:5;
then n |^ 1 = n |^ 2 by NEWTON:5;
then n <= 1 by PEPIN:30;
hence contradiction by INT_2:def_4; ::_thesis: verum
end;
end;
end;
registration
cluster prime -> square-free for Element of NAT ;
coherence
for b1 being Element of NAT st b1 is prime holds
b1 is square-free by Th23;
end;
definition
func SCNAT -> Subset of NAT means :Def2: :: MOEBIUS1:def 2
for n being Nat holds
( n in it iff n is square-free );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff n is square-free )
proof
defpred S1[ Nat] means $1 is square-free ;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds
( n in X iff S1[n] ) from SUBSET_1:sch_3();
take X ; ::_thesis: for n being Nat holds
( n in X iff n is square-free )
let n be Nat; ::_thesis: ( n in X iff n is square-free )
thus ( n in X implies n is square-free ) by A1; ::_thesis: ( n is square-free implies n in X )
assume A2: n is square-free ; ::_thesis: n in X
n is Element of NAT by INT_1:3;
hence n in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff n is square-free ) ) & ( for n being Nat holds
( n in b2 iff n is square-free ) ) holds
b1 = b2
proof
let X1, X2 be Subset of NAT; ::_thesis: ( ( for n being Nat holds
( n in X1 iff n is square-free ) ) & ( for n being Nat holds
( n in X2 iff n is square-free ) ) implies X1 = X2 )
defpred S1[ Nat] means $1 is square-free ;
assume that
A3: for n being Nat holds
( n in X1 iff n is square-free ) and
A4: for n being Nat holds
( n in X2 iff n is square-free ) ; ::_thesis: X1 = X2
A5: for y being Element of NAT holds
( y in X2 iff S1[y] ) by A4;
A6: for y being Element of NAT holds
( y in X1 iff S1[y] ) by A3;
thus X1 = X2 from SUBSET_1:sch_2(A6, A5); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines SCNAT MOEBIUS1:def_2_:_
for b1 being Subset of NAT holds
( b1 = SCNAT iff for n being Nat holds
( n in b1 iff n is square-free ) );
registration
cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-free for set ;
existence
ex b1 being Nat st b1 is square-free by Th22;
cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-containing for set ;
existence
ex b1 being Nat st b1 is square-containing
proof
take 4 ; ::_thesis: 4 is square-containing
2 |^ 2 = 2 * 2 by NEWTON:81
.= 4 ;
hence 4 is square-containing by Def1, INT_2:28; ::_thesis: verum
end;
end;
registration
cluster non trivial natural square -> square-containing for set ;
coherence
for b1 being Nat st b1 is square & not b1 is trivial holds
b1 is square-containing
proof
let n be Nat; ::_thesis: ( n is square & not n is trivial implies n is square-containing )
assume A1: ( n is square & not n is trivial ) ; ::_thesis: n is square-containing
then consider m being Nat such that
A2: n = m ^2 by PYTHTRIP:def_3;
A3: m |^ 2 divides n by A2, WSIERP_1:1;
( m <> 1 ^2 & m <> 0 ^2 ) by A1, A2, NAT_2:28;
hence n is square-containing by A3, Th20; ::_thesis: verum
end;
end;
theorem Th24: :: MOEBIUS1:24
for n being Nat st n is square-free holds
for p being Prime holds p |-count n <= 1
proof
let n be Nat; ::_thesis: ( n is square-free implies for p being Prime holds p |-count n <= 1 )
assume A1: n is square-free ; ::_thesis: for p being Prime holds p |-count n <= 1
given p being Prime such that A2: p |-count n > 1 ; ::_thesis: contradiction
p |-count n >= 1 + 1 by A2, NAT_1:13;
then p |^ 2 divides n by A1, Th9, Th21;
hence contradiction by A1, Def1; ::_thesis: verum
end;
theorem Th25: :: MOEBIUS1:25
for m, n being Nat st m * n is square-free holds
m is square-free
proof
let m, n be Nat; ::_thesis: ( m * n is square-free implies m is square-free )
assume A1: m * n is square-free ; ::_thesis: m is square-free
assume m is square-containing ; ::_thesis: contradiction
then consider p being Prime such that
A2: p |^ 2 divides m by Def1;
p |^ 2 divides m * n by A2, NAT_D:9;
hence contradiction by A1, Def1; ::_thesis: verum
end;
theorem Th26: :: MOEBIUS1:26
for m, n being Nat st m is square-free & n divides m holds
n is square-free
proof
let m, n be Nat; ::_thesis: ( m is square-free & n divides m implies n is square-free )
assume that
A1: m is square-free and
A2: n divides m ; ::_thesis: n is square-free
ex x being Nat st m = n * x by A2, NAT_D:def_3;
hence n is square-free by A1, Th25; ::_thesis: verum
end;
theorem Th27: :: MOEBIUS1:27
for p being Prime
for m, d being Nat st m is square-free & p divides m & d divides m div p holds
( d divides m & not p divides d )
proof
let p be Prime; ::_thesis: for m, d being Nat st m is square-free & p divides m & d divides m div p holds
( d divides m & not p divides d )
let m, d be Nat; ::_thesis: ( m is square-free & p divides m & d divides m div p implies ( d divides m & not p divides d ) )
assume that
A1: m is square-free and
A2: p divides m ; ::_thesis: ( not d divides m div p or ( d divides m & not p divides d ) )
assume d divides m div p ; ::_thesis: ( d divides m & not p divides d )
then consider z being Nat such that
A3: m div p = d * z by NAT_D:def_3;
A4: (m div p) * p = (d * z) * p by A3;
then m = d * (z * p) by A2, NAT_D:3;
hence d divides m by NAT_D:def_3; ::_thesis: not p divides d
assume p divides d ; ::_thesis: contradiction
then consider w being Nat such that
A5: d = p * w by NAT_D:def_3;
m = (w * (p * p)) * z by A2, A4, A5, NAT_D:3
.= (w * (p |^ 2)) * z by WSIERP_1:1
.= (p |^ 2) * (w * z) ;
then p |^ 2 divides m by NAT_D:def_3;
hence contradiction by A1, Def1; ::_thesis: verum
end;
theorem Th28: :: MOEBIUS1:28
for p being Prime
for m, d being Nat st p divides m & d divides m & not p divides d holds
d divides m div p
proof
let p be Prime; ::_thesis: for m, d being Nat st p divides m & d divides m & not p divides d holds
d divides m div p
let m, d be Nat; ::_thesis: ( p divides m & d divides m & not p divides d implies d divides m div p )
assume that
A1: p divides m and
A2: d divides m and
A3: not p divides d ; ::_thesis: d divides m div p
consider z being Nat such that
A4: m = d * z by A2, NAT_D:def_3;
p divides z by A1, A3, A4, NEWTON:80;
then consider u being Nat such that
A5: z = p * u by NAT_D:def_3;
m = (d * u) * p by A4, A5;
then m div p = d * u by NAT_D:18;
hence d divides m div p by NAT_D:def_3; ::_thesis: verum
end;
theorem :: MOEBIUS1:29
for p being Prime
for m being Nat st m is square-free & p divides m holds
{ d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
proof
let p be Prime; ::_thesis: for m being Nat st m is square-free & p divides m holds
{ d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
let m be Nat; ::_thesis: ( m is square-free & p divides m implies { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) } )
assume that
A1: m is square-free and
A2: p divides m ; ::_thesis: { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
set B = { d where d is Element of NAT : ( 0 < d & d divides m div p ) } ;
set A = { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } ;
thus { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } c= { d where d is Element of NAT : ( 0 < d & d divides m div p ) } :: according to XBOOLE_0:def_10 ::_thesis: { d where d is Element of NAT : ( 0 < d & d divides m div p ) } c= { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } or x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } )
assume x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } ; ::_thesis: x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
then consider d being Element of NAT such that
A3: ( d = x & 0 < d ) and
A4: ( d divides m & not p divides d ) ;
d divides m div p by A2, A4, Th28;
hence x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } or x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } )
assume x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } ; ::_thesis: x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) }
then consider d being Element of NAT such that
A5: ( d = x & 0 < d ) and
A6: d divides m div p ;
( d divides m & not p divides d ) by A1, A2, A6, Th27;
hence x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } by A5; ::_thesis: verum
end;
begin
definition
let n be Nat;
func Moebius n -> real number means :Def3: :: MOEBIUS1:def 3
it = 0 if n is square-containing
otherwise ex n9 being non zero Nat st
( n9 = n & it = (- 1) |^ (card (support (ppf n9))) );
consistency
for b1 being real number holds verum ;
existence
( ( n is square-containing implies ex b1 being real number st b1 = 0 ) & ( not n is square-containing implies ex b1 being real number ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) ) )
proof
thus ( n is square-containing implies ex r being real number st r = 0 ) ; ::_thesis: ( not n is square-containing implies ex b1 being real number ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) )
( n is square-free implies ex n9 being non zero Nat st
( n9 = n & ex r being real number st r = (- 1) |^ (card (support (ppf n9))) ) )
proof
assume A1: n is square-free ; ::_thesis: ex n9 being non zero Nat st
( n9 = n & ex r being real number st r = (- 1) |^ (card (support (ppf n9))) )
n is non zero Nat
proof
set p = the Prime;
assume n is not non zero Nat ; ::_thesis: contradiction
then the Prime |^ 2 divides n by NAT_D:6;
hence contradiction by A1, Def1; ::_thesis: verum
end;
then reconsider n9 = n as non zero Nat ;
ex r being real number st r = (- 1) |^ (card (support (ppf n9))) ;
hence ex n9 being non zero Nat st
( n9 = n & ex r being real number st r = (- 1) |^ (card (support (ppf n9))) ) ; ::_thesis: verum
end;
hence ( not n is square-containing implies ex b1 being real number ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being real number holds
( ( n is square-containing & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n is square-containing & ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) & ex n9 being non zero Nat st
( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) implies b1 = b2 ) ) ;
end;
:: deftheorem Def3 defines Moebius MOEBIUS1:def_3_:_
for n being Nat
for b2 being real number holds
( ( n is square-containing implies ( b2 = Moebius n iff b2 = 0 ) ) & ( not n is square-containing implies ( b2 = Moebius n iff ex n9 being non zero Nat st
( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) ) ) );
theorem Th30: :: MOEBIUS1:30
Moebius 1 = 1
proof
Moebius 1 = (- 1) |^ (card 0) by Def3, Th7, Th22
.= 1 by NEWTON:4 ;
hence Moebius 1 = 1 ; ::_thesis: verum
end;
theorem :: MOEBIUS1:31
Moebius 2 = - 1
proof
Moebius 2 = (- 1) |^ (card (support (ppf 2))) by Def3, INT_2:28
.= (- 1) |^ (card {2}) by Th8, INT_2:28
.= (- 1) |^ 1 by CARD_1:30 ;
hence Moebius 2 = - 1 by NEWTON:5; ::_thesis: verum
end;
theorem :: MOEBIUS1:32
Moebius 3 = - 1
proof
Moebius 3 = (- 1) |^ (card (support (ppf 3))) by Def3, PEPIN:41
.= (- 1) |^ (card {3}) by Th8, PEPIN:41
.= (- 1) |^ 1 by CARD_1:30 ;
hence Moebius 3 = - 1 by NEWTON:5; ::_thesis: verum
end;
theorem Th33: :: MOEBIUS1:33
for n being Nat st n is square-free holds
Moebius n <> 0
proof
let n be Nat; ::_thesis: ( n is square-free implies Moebius n <> 0 )
assume n is square-free ; ::_thesis: Moebius n <> 0
then consider n9 being non zero Nat such that
A1: ( n9 = n & Moebius n = (- 1) |^ (card (support (ppf n9))) ) by Def3;
Moebius n = (- 1) |^ (card (support (ppf n9))) by A1;
hence Moebius n <> 0 by CARD_4:3; ::_thesis: verum
end;
registration
let n be square-free Nat;
cluster Moebius n -> non zero real ;
coherence
not Moebius n is empty by Th33;
end;
theorem Th34: :: MOEBIUS1:34
for p being Prime holds Moebius p = - 1
proof
let p be Prime; ::_thesis: Moebius p = - 1
reconsider p1 = p as prime Element of NAT by ORDINAL1:def_12;
Moebius p = (- 1) |^ (card (support (ppf p1))) by Def3
.= (- 1) |^ (card {p}) by Th8
.= (- 1) |^ 1 by CARD_1:30 ;
hence Moebius p = - 1 by NEWTON:5; ::_thesis: verum
end;
theorem Th35: :: MOEBIUS1:35
for m, n being non zero Element of NAT st m,n are_relative_prime holds
Moebius (m * n) = (Moebius m) * (Moebius n)
proof
let a, b be non zero Element of NAT ; ::_thesis: ( a,b are_relative_prime implies Moebius (a * b) = (Moebius a) * (Moebius b) )
assume A1: a,b are_relative_prime ; ::_thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
percases ( ( a is square-free & b is square-free ) or ( a is square-free & b is square-containing ) or ( a is square-containing & b is square-free ) or ( a is square-containing & b is square-containing ) ) ;
supposeA2: ( a is square-free & b is square-free ) ; ::_thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
A3: a * b is square-free
proof
assume a * b is square-containing ; ::_thesis: contradiction
then consider p being Prime such that
A4: p |^ 2 divides a * b by Def1;
p in NAT by ORDINAL1:def_12;
then ( p |^ 2 divides a or p |^ 2 divides b ) by A1, A4, Th11;
hence contradiction by A2, Def1; ::_thesis: verum
end;
A5: Moebius a = (- 1) |^ (card (support (ppf a))) by A2, Def3;
card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, NAT_3:47;
then card (support (ppf (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by NAT_3:def_9
.= (card (support (pfexp a))) + (card (support (ppf b))) by NAT_3:def_9
.= (card (support (ppf a))) + (card (support (ppf b))) by NAT_3:def_9 ;
then Moebius (a * b) = (- 1) |^ ((card (support (ppf a))) + (card (support (ppf b)))) by A3, Def3
.= ((- 1) |^ (card (support (ppf a)))) * ((- 1) |^ (card (support (ppf b)))) by NEWTON:8 ;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A2, A5, Def3; ::_thesis: verum
end;
supposeA6: ( a is square-free & b is square-containing ) ; ::_thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A7: p |^ 2 divides b by Def1;
p |^ 2 divides a * b by A7, NAT_D:9;
then A8: a * b is square-containing by Def1;
Moebius b = 0 by A6, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A8, Def3; ::_thesis: verum
end;
supposeA9: ( a is square-containing & b is square-free ) ; ::_thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A10: p |^ 2 divides a by Def1;
p |^ 2 divides a * b by A10, NAT_D:9;
then A11: a * b is square-containing by Def1;
Moebius a = 0 by A9, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A11, Def3; ::_thesis: verum
end;
supposeA12: ( a is square-containing & b is square-containing ) ; ::_thesis: Moebius (a * b) = (Moebius a) * (Moebius b)
then consider p being Prime such that
A13: p |^ 2 divides a by Def1;
p |^ 2 divides a * b by A13, NAT_D:9;
then A14: a * b is square-containing by Def1;
Moebius a = 0 by A12, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A14, Def3; ::_thesis: verum
end;
end;
end;
theorem :: MOEBIUS1:36
for p being Prime
for n being Element of NAT st 1 <= n & n * p is square-free holds
Moebius (n * p) = - (Moebius n)
proof
let p be Prime; ::_thesis: for n being Element of NAT st 1 <= n & n * p is square-free holds
Moebius (n * p) = - (Moebius n)
let a be Element of NAT ; ::_thesis: ( 1 <= a & a * p is square-free implies Moebius (a * p) = - (Moebius a) )
assume that
A1: 1 <= a and
A2: a * p is square-free ; ::_thesis: Moebius (a * p) = - (Moebius a)
A3: p in NAT by ORDINAL1:def_12;
a,p are_relative_prime
proof
assume not a,p are_relative_prime ; ::_thesis: contradiction
then consider q being prime Nat such that
A4: q divides a and
A5: q divides p by PYTHTRIP:def_2;
( q = 1 or q = p ) by A5, INT_2:def_4;
then p * p divides a * p by A3, A4, INT_2:def_4, PYTHTRIP:7;
then p |^ 2 divides a * p by WSIERP_1:1;
hence contradiction by A2, Def1; ::_thesis: verum
end;
then Moebius (a * p) = (Moebius a) * (Moebius p) by A1, A3, Th35
.= (Moebius a) * (- 1) by Th34 ;
hence Moebius (a * p) = - (Moebius a) ; ::_thesis: verum
end;
theorem :: MOEBIUS1:37
for m, n being non zero Element of NAT st not m,n are_relative_prime holds
Moebius (m * n) = 0
proof
let m, n be non zero Element of NAT ; ::_thesis: ( not m,n are_relative_prime implies Moebius (m * n) = 0 )
assume not m,n are_relative_prime ; ::_thesis: Moebius (m * n) = 0
then consider p being prime Nat such that
A1: ( p divides m & p divides n ) by PYTHTRIP:def_2;
reconsider p = p as prime Element of NAT by ORDINAL1:def_12;
p * p divides m * n by A1, NAT_3:1;
then p |^ 2 divides m * n by WSIERP_1:1;
then m * n is square-containing by Def1;
hence Moebius (m * n) = 0 by Def3; ::_thesis: verum
end;
theorem Th38: :: MOEBIUS1:38
for n being Nat holds
( n in SCNAT iff Moebius n <> 0 )
proof
let n be Nat; ::_thesis: ( n in SCNAT iff Moebius n <> 0 )
hereby ::_thesis: ( Moebius n <> 0 implies n in SCNAT )
assume n in SCNAT ; ::_thesis: Moebius n <> 0
then n is square-free by Def2;
hence Moebius n <> 0 ; ::_thesis: verum
end;
assume Moebius n <> 0 ; ::_thesis: n in SCNAT
then n is square-free by Def3;
hence n in SCNAT by Def2; ::_thesis: verum
end;
begin
definition
let n be Nat;
func NatDivisors n -> Subset of NAT equals :: MOEBIUS1:def 4
{ k where k is Element of NAT : ( k <> 0 & k divides n ) } ;
coherence
{ k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT
proof
{ k where k is Element of NAT : ( k <> 0 & k divides n ) } c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( k <> 0 & k divides n ) } or x in NAT )
assume x in { k where k is Element of NAT : ( k <> 0 & k divides n ) } ; ::_thesis: x in NAT
then ex k being Element of NAT st
( k = x & k <> 0 & k divides n ) ;
hence x in NAT ; ::_thesis: verum
end;
hence { k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT ; ::_thesis: verum
end;
end;
:: deftheorem defines NatDivisors MOEBIUS1:def_4_:_
for n being Nat holds NatDivisors n = { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;
theorem :: MOEBIUS1:39
for n, k being Nat holds
( k in NatDivisors n iff ( 0 < k & k divides n ) )
proof
let n, k be Nat; ::_thesis: ( k in NatDivisors n iff ( 0 < k & k divides n ) )
hereby ::_thesis: ( 0 < k & k divides n implies k in NatDivisors n )
assume k in NatDivisors n ; ::_thesis: ( 0 < k & k divides n )
then ex l being Element of NAT st
( l = k & l <> 0 & l divides n ) ;
hence ( 0 < k & k divides n ) ; ::_thesis: verum
end;
assume A1: ( 0 < k & k divides n ) ; ::_thesis: k in NatDivisors n
k is Element of NAT by ORDINAL1:def_12;
hence k in NatDivisors n by A1; ::_thesis: verum
end;
theorem Th40: :: MOEBIUS1:40
for n being non zero Nat holds NatDivisors n c= Seg n
proof
let n be non zero Nat; ::_thesis: NatDivisors n c= Seg n
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NatDivisors n or x in Seg n )
assume x in NatDivisors n ; ::_thesis: x in Seg n
then consider k being Element of NAT such that
A1: x = k and
A2: ( k <> 0 & k divides n ) ;
( 1 <= k & k <= n ) by A2, NAT_1:14, NAT_D:7;
hence x in Seg n by A1, FINSEQ_1:1; ::_thesis: verum
end;
registration
let n be non zero Nat;
cluster NatDivisors n -> finite with_non-empty_elements ;
coherence
( NatDivisors n is finite & NatDivisors n is with_non-empty_elements )
proof
set P = NatDivisors n;
A1: not 0 in NatDivisors n
proof
assume 0 in NatDivisors n ; ::_thesis: contradiction
then ex k being Element of NAT st
( k = 0 & k <> 0 & k divides n ) ;
hence contradiction ; ::_thesis: verum
end;
NatDivisors n c= Seg n by Th40;
hence ( NatDivisors n is finite & NatDivisors n is with_non-empty_elements ) by A1, MEASURE6:def_2; ::_thesis: verum
end;
end;
theorem Th41: :: MOEBIUS1:41
NatDivisors 1 = {1}
proof
thus NatDivisors 1 c= {1} :: according to XBOOLE_0:def_10 ::_thesis: {1} c= NatDivisors 1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NatDivisors 1 or x in {1} )
assume x in NatDivisors 1 ; ::_thesis: x in {1}
then consider k being Element of NAT such that
A1: x = k and
k <> 0 and
A2: k divides 1 ;
k = 1 by A2, WSIERP_1:15;
hence x in {1} by A1, ZFMISC_1:31; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in NatDivisors 1 )
assume A3: x in {1} ; ::_thesis: x in NatDivisors 1
then reconsider m = x as Element of NAT ;
( m <> 0 & m divides 1 ) by A3, TARSKI:def_1;
hence x in NatDivisors 1 ; ::_thesis: verum
end;
begin
definition
let X be set ;
func SMoebius X -> ManySortedSet of NAT means :Def5: :: MOEBIUS1:def 5
( support it = X /\ SCNAT & ( for k being Element of NAT st k in support it holds
it . k = Moebius k ) );
existence
ex b1 being ManySortedSet of NAT st
( support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds
b1 . k = Moebius k ) )
proof
defpred S1[ set ] means $1 in X /\ SCNAT;
deffunc H1( Element of NAT ) -> Element of NAT = 0 ;
deffunc H2( Element of NAT ) -> real number = Moebius $1;
ex f being ManySortedSet of NAT st
for i being Element of NAT st i in NAT holds
( ( S1[i] implies f . i = H2(i) ) & ( not S1[i] implies f . i = H1(i) ) ) from PRE_CIRC:sch_2();
then consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT st i in NAT holds
( ( S1[i] implies f . i = H2(i) ) & ( not S1[i] implies f . i = H1(i) ) ) ;
A2: support f c= SCNAT
proof
dom f = NAT by PARTFUN1:def_2;
then A3: support f c= NAT by PRE_POLY:37;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support f or x in SCNAT )
assume A4: x in support f ; ::_thesis: x in SCNAT
then A5: f . x <> 0 by PRE_POLY:def_7;
percases ( S1[x] or not S1[x] ) ;
suppose S1[x] ; ::_thesis: x in SCNAT
hence x in SCNAT by XBOOLE_0:def_4; ::_thesis: verum
end;
suppose not S1[x] ; ::_thesis: x in SCNAT
hence x in SCNAT by A1, A4, A5, A3; ::_thesis: verum
end;
end;
end;
A6: support f = X /\ SCNAT
proof
thus support f c= X /\ SCNAT :: according to XBOOLE_0:def_10 ::_thesis: X /\ SCNAT c= support f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support f or x in X /\ SCNAT )
assume A7: x in support f ; ::_thesis: x in X /\ SCNAT
then x in SCNAT by A2;
then reconsider i = x as Element of NAT ;
assume not x in X /\ SCNAT ; ::_thesis: contradiction
then f . i = 0 by A1;
hence contradiction by A7, PRE_POLY:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ SCNAT or x in support f )
assume A8: x in X /\ SCNAT ; ::_thesis: x in support f
then reconsider i = x as Element of NAT ;
x in SCNAT by A8, XBOOLE_0:def_4;
then A9: Moebius i <> 0 by Th38;
f . i = Moebius i by A1, A8;
hence x in support f by A9, PRE_POLY:def_7; ::_thesis: verum
end;
reconsider f = f as ManySortedSet of NAT ;
take f ; ::_thesis: ( support f = X /\ SCNAT & ( for k being Element of NAT st k in support f holds
f . k = Moebius k ) )
thus support f = X /\ SCNAT by A6; ::_thesis: for k being Element of NAT st k in support f holds
f . k = Moebius k
let k be Element of NAT ; ::_thesis: ( k in support f implies f . k = Moebius k )
assume k in support f ; ::_thesis: f . k = Moebius k
hence f . k = Moebius k by A1, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of NAT st support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds
b1 . k = Moebius k ) & support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds
b2 . k = Moebius k ) holds
b1 = b2
proof
let f, g be ManySortedSet of NAT ; ::_thesis: ( support f = X /\ SCNAT & ( for k being Element of NAT st k in support f holds
f . k = Moebius k ) & support g = X /\ SCNAT & ( for k being Element of NAT st k in support g holds
g . k = Moebius k ) implies f = g )
assume that
A10: support f = X /\ SCNAT and
A11: for k being Element of NAT st k in support f holds
f . k = Moebius k and
A12: support g = X /\ SCNAT and
A13: for k being Element of NAT st k in support g holds
g . k = Moebius k ; ::_thesis: f = g
for i being set st i in NAT holds
f . i = g . i
proof
let i be set ; ::_thesis: ( i in NAT implies f . i = g . i )
assume i in NAT ; ::_thesis: f . i = g . i
then reconsider j = i as Element of NAT ;
percases ( j in support f or not j in support f ) ;
supposeA14: j in support f ; ::_thesis: f . i = g . i
hence f . i = Moebius j by A11
.= g . i by A10, A12, A13, A14 ;
::_thesis: verum
end;
supposeA15: not j in support f ; ::_thesis: f . i = g . i
hence f . i = 0 by PRE_POLY:def_7
.= g . i by A10, A12, A15, PRE_POLY:def_7 ;
::_thesis: verum
end;
end;
end;
hence f = g by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines SMoebius MOEBIUS1:def_5_:_
for X being set
for b2 being ManySortedSet of NAT holds
( b2 = SMoebius X iff ( support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds
b2 . k = Moebius k ) ) );
registration
let X be set ;
cluster SMoebius X -> real-valued ;
coherence
SMoebius X is real-valued
proof
rng (SMoebius X) c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (SMoebius X) or y in REAL )
assume y in rng (SMoebius X) ; ::_thesis: y in REAL
then consider i being set such that
A1: i in dom (SMoebius X) and
A2: (SMoebius X) . i = y by FUNCT_1:def_3;
dom (SMoebius X) = NAT by PARTFUN1:def_2;
then reconsider i = i as Nat by A1;
percases ( i in support (SMoebius X) or not i in support (SMoebius X) ) ;
supposeA3: i in support (SMoebius X) ; ::_thesis: y in REAL
then i in X /\ SCNAT by Def5;
then y = Moebius i by A2, A3, Def5;
hence y in REAL by XREAL_0:def_1; ::_thesis: verum
end;
suppose not i in support (SMoebius X) ; ::_thesis: y in REAL
then (SMoebius X) . i = 0 by PRE_POLY:def_7;
hence y in REAL by A2; ::_thesis: verum
end;
end;
end;
hence SMoebius X is real-valued by VALUED_0:def_3; ::_thesis: verum
end;
end;
registration
let X be finite set ;
cluster SMoebius X -> finite-support ;
coherence
SMoebius X is finite-support
proof
support (SMoebius X) = X /\ SCNAT by Def5;
hence SMoebius X is finite-support by PRE_POLY:def_8; ::_thesis: verum
end;
end;
theorem :: MOEBIUS1:42
Sum (SMoebius (NatDivisors 1)) = 1
proof
reconsider J = 1 as Element of NAT ;
reconsider M = ({1},1) -bag as Rbag of NAT ;
A1: 1 in {1} by TARSKI:def_1;
A2: 1 in SCNAT by Def2, Th22;
J in {1} by TARSKI:def_1;
then J in {1} /\ SCNAT by A2, XBOOLE_0:def_4;
then J in support (SMoebius {1}) by Def5;
then A3: (SMoebius {1}) . 1 = 1 by Def5, Th30;
{1} c= SCNAT by A2, ZFMISC_1:31;
then A4: {1} /\ SCNAT = {1} by XBOOLE_1:28;
for x being set st x in NAT holds
(SMoebius {1}) . x = M . x
proof
let x be set ; ::_thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )
percases ( x in {1} or not x in {1} ) ;
supposeA5: x in {1} ; ::_thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )
then x = 1 by TARSKI:def_1;
hence ( x in NAT implies (SMoebius {1}) . x = M . x ) by A3, A5, UPROOTS:7; ::_thesis: verum
end;
supposeA6: not x in {1} ; ::_thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )
then A7: not x in support (SMoebius {1}) by A4, Def5;
M . x = 0 by A6, UPROOTS:6
.= (SMoebius {1}) . x by A7, PRE_POLY:def_7 ;
hence ( x in NAT implies (SMoebius {1}) . x = M . x ) ; ::_thesis: verum
end;
end;
end;
then ( support M = {1} & SMoebius {1} = M ) by PBOOLE:3, UPROOTS:8;
then Sum (SMoebius (NatDivisors 1)) = M . 1 by Th12, Th41
.= 1 by A1, UPROOTS:7 ;
hence Sum (SMoebius (NatDivisors 1)) = 1 ; ::_thesis: verum
end;
theorem :: MOEBIUS1:43
for X, Y being finite Subset of NAT st X misses Y holds
(support (SMoebius X)) \/ (support (SMoebius Y)) = support ((SMoebius X) + (SMoebius Y))
proof
let X, Y be finite Subset of NAT; ::_thesis: ( X misses Y implies (support (SMoebius X)) \/ (support (SMoebius Y)) = support ((SMoebius X) + (SMoebius Y)) )
assume A1: X misses Y ; ::_thesis: (support (SMoebius X)) \/ (support (SMoebius Y)) = support ((SMoebius X) + (SMoebius Y))
thus (support (SMoebius X)) \/ (support (SMoebius Y)) c= support ((SMoebius X) + (SMoebius Y)) :: according to XBOOLE_0:def_10 ::_thesis: support ((SMoebius X) + (SMoebius Y)) c= (support (SMoebius X)) \/ (support (SMoebius Y))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (support (SMoebius X)) \/ (support (SMoebius Y)) or x in support ((SMoebius X) + (SMoebius Y)) )
( support (SMoebius X) = X /\ SCNAT & support (SMoebius Y) = Y /\ SCNAT ) by Def5;
then A2: support (SMoebius X) misses support (SMoebius Y) by A1, XBOOLE_1:76;
assume A3: x in (support (SMoebius X)) \/ (support (SMoebius Y)) ; ::_thesis: x in support ((SMoebius X) + (SMoebius Y))
percases ( x in support (SMoebius X) or x in support (SMoebius Y) ) by A3, XBOOLE_0:def_3;
supposeA4: x in support (SMoebius X) ; ::_thesis: x in support ((SMoebius X) + (SMoebius Y))
then not x in support (SMoebius Y) by A2, XBOOLE_0:3;
then (SMoebius Y) . x = 0 by PRE_POLY:def_7;
then ((SMoebius X) . x) + ((SMoebius Y) . x) <> 0 by A4, PRE_POLY:def_7;
then ((SMoebius X) + (SMoebius Y)) . x <> 0 by PRE_POLY:def_5;
hence x in support ((SMoebius X) + (SMoebius Y)) by PRE_POLY:def_7; ::_thesis: verum
end;
supposeA5: x in support (SMoebius Y) ; ::_thesis: x in support ((SMoebius X) + (SMoebius Y))
then not x in support (SMoebius X) by A2, XBOOLE_0:3;
then (SMoebius X) . x = 0 by PRE_POLY:def_7;
then ((SMoebius X) . x) + ((SMoebius Y) . x) <> 0 by A5, PRE_POLY:def_7;
then ((SMoebius X) + (SMoebius Y)) . x <> 0 by PRE_POLY:def_5;
hence x in support ((SMoebius X) + (SMoebius Y)) by PRE_POLY:def_7; ::_thesis: verum
end;
end;
end;
thus support ((SMoebius X) + (SMoebius Y)) c= (support (SMoebius X)) \/ (support (SMoebius Y)) by PRE_POLY:75; ::_thesis: verum
end;
theorem :: MOEBIUS1:44
for X, Y being finite Subset of NAT st X misses Y holds
SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)
proof
let X, Y be finite Subset of NAT; ::_thesis: ( X misses Y implies SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y) )
A1: support (SMoebius (X \/ Y)) = (X \/ Y) /\ SCNAT by Def5
.= (X /\ SCNAT) \/ (Y /\ SCNAT) by XBOOLE_1:23 ;
assume A2: X misses Y ; ::_thesis: SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)
for x being set st x in NAT holds
(SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x
proof
let x be set ; ::_thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )
percases ( x in support (SMoebius (X \/ Y)) or not x in support (SMoebius (X \/ Y)) ) ;
supposeA3: x in support (SMoebius (X \/ Y)) ; ::_thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )
percases ( x in X /\ SCNAT or x in Y /\ SCNAT ) by A1, A3, XBOOLE_0:def_3;
supposeA4: x in X /\ SCNAT ; ::_thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )
then reconsider k = x as Element of NAT ;
A5: k in support (SMoebius X) by A4, Def5;
not x in Y /\ SCNAT by A2, A4, Lm1;
then A6: not k in support (SMoebius Y) by Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, Def5
.= (Moebius k) + ((SMoebius Y) . k) by A6, PRE_POLY:def_7
.= ((SMoebius X) . k) + ((SMoebius Y) . k) by A5, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by PRE_POLY:def_5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; ::_thesis: verum
end;
supposeA7: x in Y /\ SCNAT ; ::_thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )
then consider k being Element of NAT such that
A8: k = x ;
not x in X /\ SCNAT by A2, A7, Lm1;
then A9: not k in support (SMoebius X) by A8, Def5;
A10: k in support (SMoebius Y) by A7, A8, Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, A8, Def5
.= (Moebius k) + ((SMoebius X) . k) by A9, PRE_POLY:def_7
.= ((SMoebius Y) . k) + ((SMoebius X) . k) by A10, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by A8, PRE_POLY:def_5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; ::_thesis: verum
end;
end;
end;
supposeA11: not x in support (SMoebius (X \/ Y)) ; ::_thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )
then not x in Y /\ SCNAT by A1, XBOOLE_0:def_3;
then A12: not x in support (SMoebius Y) by Def5;
not x in X /\ SCNAT by A1, A11, XBOOLE_0:def_3;
then A13: not x in support (SMoebius X) by Def5;
(SMoebius (X \/ Y)) . x = 0 by A11, PRE_POLY:def_7
.= ((SMoebius Y) . x) + 0 by A12, PRE_POLY:def_7
.= ((SMoebius Y) . x) + ((SMoebius X) . x) by A13, PRE_POLY:def_7
.= ((SMoebius X) + (SMoebius Y)) . x by PRE_POLY:def_5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; ::_thesis: verum
end;
end;
end;
hence SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y) by PBOOLE:3; ::_thesis: verum
end;
begin
definition
let n be non zero Nat;
func PFactors n -> ManySortedSet of SetPrimes means :Def6: :: MOEBIUS1:def 6
( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it . p = p ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p ) )
proof
defpred S1[ set , set ] means for p being Prime st $1 = p holds
( ( p in support (pfexp n) implies $2 = p ) & ( not p in support (pfexp n) implies $2 = 0 ) );
A1: for x being set st x in SetPrimes holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in SetPrimes implies ex y being set st S1[x,y] )
assume x in SetPrimes ; ::_thesis: ex y being set st S1[x,y]
then reconsider i = x as prime Element of NAT by NEWTON:def_6;
percases ( i in support (pfexp n) or not i in support (pfexp n) ) ;
supposeA2: i in support (pfexp n) ; ::_thesis: ex y being set st S1[x,y]
take i ; ::_thesis: S1[x,i]
let p be Prime; ::_thesis: ( x = p implies ( ( p in support (pfexp n) implies i = p ) & ( not p in support (pfexp n) implies i = 0 ) ) )
assume p = x ; ::_thesis: ( ( p in support (pfexp n) implies i = p ) & ( not p in support (pfexp n) implies i = 0 ) )
hence ( ( p in support (pfexp n) implies i = p ) & ( not p in support (pfexp n) implies i = 0 ) ) by A2; ::_thesis: verum
end;
supposeA3: not i in support (pfexp n) ; ::_thesis: ex y being set st S1[x,y]
take 0 ; ::_thesis: S1[x, 0 ]
let p be Prime; ::_thesis: ( x = p implies ( ( p in support (pfexp n) implies 0 = p ) & ( not p in support (pfexp n) implies 0 = 0 ) ) )
assume p = x ; ::_thesis: ( ( p in support (pfexp n) implies 0 = p ) & ( not p in support (pfexp n) implies 0 = 0 ) )
hence ( ( p in support (pfexp n) implies 0 = p ) & ( not p in support (pfexp n) implies 0 = 0 ) ) by A3; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A4: dom f = SetPrimes and
A5: for x being set st x in SetPrimes holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A6: support f c= SetPrimes by A4, PRE_POLY:37;
A7: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_support_f_implies_x_in_support_(pfexp_n)_)_&_(_x_in_support_(pfexp_n)_implies_x_in_support_f_)_)
let x be set ; ::_thesis: ( ( x in support f implies x in support (pfexp n) ) & ( x in support (pfexp n) implies x in support f ) )
hereby ::_thesis: ( x in support (pfexp n) implies x in support f )
assume A8: x in support f ; ::_thesis: x in support (pfexp n)
then x in SetPrimes by A6;
then reconsider i = x as prime Element of NAT by NEWTON:def_6;
assume not x in support (pfexp n) ; ::_thesis: contradiction
then f . i = 0 by A5, A6, A8;
hence contradiction by A8, PRE_POLY:def_7; ::_thesis: verum
end;
assume A9: x in support (pfexp n) ; ::_thesis: x in support f
then x in SetPrimes ;
then reconsider i = x as prime Element of NAT by NEWTON:def_6;
f . i = i by A5, A9;
hence x in support f by PRE_POLY:def_7; ::_thesis: verum
end;
reconsider f = f as ManySortedSet of SetPrimes by A4, PARTFUN1:def_2, RELAT_1:def_18;
take f ; ::_thesis: ( support f = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f . p = p ) )
thus support f = support (pfexp n) by A7, TARSKI:1; ::_thesis: for p being Nat st p in support (pfexp n) holds
f . p = p
let p be Nat; ::_thesis: ( p in support (pfexp n) implies f . p = p )
assume A10: p in support (pfexp n) ; ::_thesis: f . p = p
then p is Prime by NAT_3:34;
hence f . p = p by A5, A10; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p ) holds
b1 = b2
proof
let it1, it2 be ManySortedSet of SetPrimes ; ::_thesis: ( support it1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it1 . p = p ) & support it2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it2 . p = p ) implies it1 = it2 )
assume that
A11: support it1 = support (pfexp n) and
A12: for p being Nat st p in support (pfexp n) holds
it1 . p = p and
A13: support it2 = support (pfexp n) and
A14: for p being Nat st p in support (pfexp n) holds
it2 . p = p ; ::_thesis: it1 = it2
now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_
it1_._i_=_it2_._i
let i be set ; ::_thesis: ( i in SetPrimes implies it1 . b1 = it2 . b1 )
assume i in SetPrimes ; ::_thesis: it1 . b1 = it2 . b1
then reconsider p = i as prime Element of NAT by NEWTON:def_6;
percases ( p in support (pfexp n) or not p in support (pfexp n) ) ;
supposeA15: p in support (pfexp n) ; ::_thesis: it1 . b1 = it2 . b1
hence it1 . i = p by A12
.= it2 . i by A14, A15 ;
::_thesis: verum
end;
supposeA16: not p in support (pfexp n) ; ::_thesis: it1 . b1 = it2 . b1
hence it1 . i = 0 by A11, PRE_POLY:def_7
.= it2 . i by A13, A16, PRE_POLY:def_7 ;
::_thesis: verum
end;
end;
end;
hence it1 = it2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines PFactors MOEBIUS1:def_6_:_
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = PFactors n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p ) ) );
registration
let n be non zero Nat;
cluster PFactors n -> natural-valued finite-support ;
coherence
( PFactors n is finite-support & PFactors n is natural-valued )
proof
A1: rng (PFactors n) c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (PFactors n) or x in NAT )
assume x in rng (PFactors n) ; ::_thesis: x in NAT
then consider y being set such that
A2: y in dom (PFactors n) and
A3: (PFactors n) . y = x by FUNCT_1:def_3;
A4: y in SetPrimes by A2, PARTFUN1:def_2;
percases ( y in support (pfexp n) or not y in support (pfexp n) ) ;
suppose y in support (pfexp n) ; ::_thesis: x in NAT
then x = y by A3, Def6;
hence x in NAT by A4; ::_thesis: verum
end;
suppose not y in support (pfexp n) ; ::_thesis: x in NAT
then not y in support (PFactors n) by Def6;
then x = 0 by A3, PRE_POLY:def_7;
hence x in NAT ; ::_thesis: verum
end;
end;
end;
support (PFactors n) = support (pfexp n) by Def6;
hence ( PFactors n is finite-support & PFactors n is natural-valued ) by A1, PRE_POLY:def_8, VALUED_0:def_6; ::_thesis: verum
end;
end;
theorem Th45: :: MOEBIUS1:45
PFactors 1 = EmptyBag SetPrimes
proof
set f = PFactors 1;
for z being set st z in dom (PFactors 1) holds
(PFactors 1) . z = 0
proof
let z be set ; ::_thesis: ( z in dom (PFactors 1) implies (PFactors 1) . z = 0 )
assume z in dom (PFactors 1) ; ::_thesis: (PFactors 1) . z = 0
then z in SetPrimes by PARTFUN1:def_2;
then reconsider z = z as Element of NAT ;
support (pfexp 1) = {} ;
then not z in support (PFactors 1) by Def6;
hence (PFactors 1) . z = 0 by PRE_POLY:def_7; ::_thesis: verum
end;
then A1: PFactors 1 = (dom (PFactors 1)) --> 0 by FUNCOP_1:11;
dom (PFactors 1) = SetPrimes by PARTFUN1:def_2;
hence PFactors 1 = EmptyBag SetPrimes by A1, PRE_POLY:def_13; ::_thesis: verum
end;
theorem Th46: :: MOEBIUS1:46
for p being Prime holds (PFactors p) * <*p*> = <*p*>
proof
let p be Prime; ::_thesis: (PFactors p) * <*p*> = <*p*>
set f = <*p*>;
set g = PFactors p;
A1: dom ((PFactors p) * <*p*>) = {1}
proof
thus dom ((PFactors p) * <*p*>) c= {1} :: according to XBOOLE_0:def_10 ::_thesis: {1} c= dom ((PFactors p) * <*p*>)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((PFactors p) * <*p*>) or x in {1} )
assume x in dom ((PFactors p) * <*p*>) ; ::_thesis: x in {1}
then x in dom <*p*> by FUNCT_1:11;
hence x in {1} by FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom ((PFactors p) * <*p*>) )
assume A2: x in {1} ; ::_thesis: x in dom ((PFactors p) * <*p*>)
then x = 1 by TARSKI:def_1;
then <*p*> . x = p by FINSEQ_1:def_8;
then <*p*> . x in SetPrimes by NEWTON:def_6;
then A3: <*p*> . x in dom (PFactors p) by PARTFUN1:def_2;
x in dom <*p*> by A2, FINSEQ_1:2, FINSEQ_1:38;
hence x in dom ((PFactors p) * <*p*>) by A3, FUNCT_1:11; ::_thesis: verum
end;
A4: for x being set st x in dom ((PFactors p) * <*p*>) holds
((PFactors p) * <*p*>) . x = <*p*> . x
proof
let x be set ; ::_thesis: ( x in dom ((PFactors p) * <*p*>) implies ((PFactors p) * <*p*>) . x = <*p*> . x )
(pfexp p) . p <> 0 by NAT_3:38;
then A5: p in support (pfexp p) by PRE_POLY:def_7;
assume A6: x in dom ((PFactors p) * <*p*>) ; ::_thesis: ((PFactors p) * <*p*>) . x = <*p*> . x
then A7: x = 1 by A1, TARSKI:def_1;
then ((PFactors p) * <*p*>) . 1 = (PFactors p) . (<*p*> . 1) by A6, FUNCT_1:12
.= (PFactors p) . p by FINSEQ_1:def_8
.= p by A5, Def6
.= <*p*> . 1 by FINSEQ_1:def_8 ;
hence ((PFactors p) * <*p*>) . x = <*p*> . x by A7; ::_thesis: verum
end;
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
hence (PFactors p) * <*p*> = <*p*> by A1, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th47: :: MOEBIUS1:47
for p being Prime
for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>
proof
let p be Prime; ::_thesis: for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>
let n be non zero Nat; ::_thesis: (PFactors (p |^ n)) * <*p*> = <*p*>
set s = p |^ n;
set f = <*p*>;
set g = PFactors (p |^ n);
A1: dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A2: dom ((PFactors (p |^ n)) * <*p*>) = {1}
proof
thus dom ((PFactors (p |^ n)) * <*p*>) c= {1} :: according to XBOOLE_0:def_10 ::_thesis: {1} c= dom ((PFactors (p |^ n)) * <*p*>)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((PFactors (p |^ n)) * <*p*>) or x in {1} )
assume x in dom ((PFactors (p |^ n)) * <*p*>) ; ::_thesis: x in {1}
hence x in {1} by A1, FUNCT_1:11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom ((PFactors (p |^ n)) * <*p*>) )
assume A3: x in {1} ; ::_thesis: x in dom ((PFactors (p |^ n)) * <*p*>)
then x = 1 by TARSKI:def_1;
then <*p*> . x = p by FINSEQ_1:def_8;
then <*p*> . x in SetPrimes by NEWTON:def_6;
then A4: <*p*> . x in dom (PFactors (p |^ n)) by PARTFUN1:def_2;
x in dom <*p*> by A3, FINSEQ_1:2, FINSEQ_1:38;
hence x in dom ((PFactors (p |^ n)) * <*p*>) by A4, FUNCT_1:11; ::_thesis: verum
end;
A5: for x being set st x in dom ((PFactors (p |^ n)) * <*p*>) holds
((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x
proof
let x be set ; ::_thesis: ( x in dom ((PFactors (p |^ n)) * <*p*>) implies ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x )
(pfexp p) . p <> 0 by NAT_3:38;
then p in support (pfexp p) by PRE_POLY:def_7;
then A6: p in support (pfexp (p |^ n)) by NAT_3:48;
assume A7: x in dom ((PFactors (p |^ n)) * <*p*>) ; ::_thesis: ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x
then A8: x = 1 by A2, TARSKI:def_1;
then ((PFactors (p |^ n)) * <*p*>) . 1 = (PFactors (p |^ n)) . (<*p*> . 1) by A7, FUNCT_1:12
.= (PFactors (p |^ n)) . p by FINSEQ_1:def_8
.= p by A6, Def6
.= <*p*> . 1 by FINSEQ_1:def_8 ;
hence ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x by A8; ::_thesis: verum
end;
dom ((PFactors (p |^ n)) * <*p*>) = dom <*p*> by A2, FINSEQ_1:2, FINSEQ_1:38;
hence (PFactors (p |^ n)) * <*p*> = <*p*> by A5, FUNCT_1:2; ::_thesis: verum
end;
theorem Th48: :: MOEBIUS1:48
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
(PFactors n) . p = 0
proof
let p be Prime; ::_thesis: for n being non zero Nat st p |-count n = 0 holds
(PFactors n) . p = 0
let n be non zero Nat; ::_thesis: ( p |-count n = 0 implies (PFactors n) . p = 0 )
assume p |-count n = 0 ; ::_thesis: (PFactors n) . p = 0
then (pfexp n) . p = 0 by NAT_3:def_8;
then not p in support (pfexp n) by PRE_POLY:def_7;
then not p in support (PFactors n) by Def6;
hence (PFactors n) . p = 0 by PRE_POLY:def_7; ::_thesis: verum
end;
theorem Th49: :: MOEBIUS1:49
for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
(PFactors n) . p = p
proof
let n be non zero Nat; ::_thesis: for p being Prime st p |-count n <> 0 holds
(PFactors n) . p = p
let p be Prime; ::_thesis: ( p |-count n <> 0 implies (PFactors n) . p = p )
assume p |-count n <> 0 ; ::_thesis: (PFactors n) . p = p
then (pfexp n) . p <> 0 by NAT_3:def_8;
then p in support (pfexp n) by PRE_POLY:def_7;
hence (PFactors n) . p = p by Def6; ::_thesis: verum
end;
theorem Th50: :: MOEBIUS1:50
for m, n being non zero Element of NAT st m,n are_relative_prime holds
PFactors (m * n) = (PFactors m) + (PFactors n)
proof
let a, b be non zero Element of NAT ; ::_thesis: ( a,b are_relative_prime implies PFactors (a * b) = (PFactors a) + (PFactors b) )
reconsider an = a, bn = b as non zero Nat ;
assume A1: a,b are_relative_prime ; ::_thesis: PFactors (a * b) = (PFactors a) + (PFactors b)
now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_
(PFactors_(a_*_b))_._i_=_((PFactors_a)_+_(PFactors_b))_._i
let i be set ; ::_thesis: ( i in SetPrimes implies (PFactors (a * b)) . b1 = ((PFactors a) + (PFactors b)) . b1 )
assume i in SetPrimes ; ::_thesis: (PFactors (a * b)) . b1 = ((PFactors a) + (PFactors b)) . b1
then reconsider p = i as prime Element of NAT by NEWTON:def_6;
A2: p |-count (an * bn) = (p |-count a) + (p |-count b) by NAT_3:28;
A3: a gcd b = 1 by A1, INT_2:def_3;
A4: p > 1 by INT_2:def_4;
percases ( p |-count (a * b) = 0 or p |-count (a * b) <> 0 ) ;
supposeA5: p |-count (a * b) = 0 ; ::_thesis: (PFactors (a * b)) . b1 = ((PFactors a) + (PFactors b)) . b1
then A6: p |-count b = 0 by A2;
A7: p |-count a = 0 by A2, A5;
thus (PFactors (a * b)) . i = 0 by A5, Th48
.= 0 + ((PFactors b) . i) by A6, Th48
.= ((PFactors a) . i) + ((PFactors b) . i) by A7, Th48
.= ((PFactors a) + (PFactors b)) . i by PRE_POLY:def_5 ; ::_thesis: verum
end;
supposeA8: p |-count (a * b) <> 0 ; ::_thesis: (PFactors (a * b)) . b1 = ((PFactors a) + (PFactors b)) . b1
thus (PFactors (a * b)) . i = ((PFactors a) + (PFactors b)) . i ::_thesis: verum
proof
percases ( p |-count a <> 0 or p |-count b <> 0 ) by A2, A8;
supposeA9: p |-count a <> 0 ; ::_thesis: (PFactors (a * b)) . i = ((PFactors a) + (PFactors b)) . i
A10: now__::_thesis:_not_p_|-count_b_<>_0
consider ka being Nat such that
A11: p |-count a = ka + 1 by A9, NAT_1:6;
reconsider ka = ka as Element of NAT by ORDINAL1:def_12;
p |^ (p |-count a) divides a by A4, NAT_3:def_7;
then p * (p |^ ka) divides a by A11, NEWTON:6;
then consider la being Nat such that
A12: a = (p * (p |^ ka)) * la by NAT_D:def_3;
a = p * ((p |^ ka) * la) by A12;
then A13: p divides a by NAT_D:def_3;
assume p |-count b <> 0 ; ::_thesis: contradiction
then consider kb being Nat such that
A14: p |-count b = kb + 1 by NAT_1:6;
reconsider kb = kb as Element of NAT by ORDINAL1:def_12;
p |^ (p |-count b) divides b by A4, NAT_3:def_7;
then p * (p |^ kb) divides b by A14, NEWTON:6;
then consider lb being Nat such that
A15: b = (p * (p |^ kb)) * lb by NAT_D:def_3;
b = p * ((p |^ kb) * lb) by A15;
then p divides b by NAT_D:def_3;
then p divides 1 by A3, A13, NAT_D:def_5;
hence contradiction by A4, NAT_D:7; ::_thesis: verum
end;
thus (PFactors (a * b)) . i = p by A8, Th49
.= ((PFactors a) . p) + 0 by A9, Th49
.= ((PFactors a) . p) + ((PFactors b) . p) by A10, Th48
.= ((PFactors a) + (PFactors b)) . i by PRE_POLY:def_5 ; ::_thesis: verum
end;
supposeA16: p |-count b <> 0 ; ::_thesis: (PFactors (a * b)) . i = ((PFactors a) + (PFactors b)) . i
A17: now__::_thesis:_not_p_|-count_a_<>_0
assume p |-count a <> 0 ; ::_thesis: contradiction
then consider ka being Nat such that
A18: p |-count a = ka + 1 by NAT_1:6;
reconsider ka = ka as Element of NAT by ORDINAL1:def_12;
p |^ (p |-count a) divides a by A4, NAT_3:def_7;
then p * (p |^ ka) divides a by A18, NEWTON:6;
then consider la being Nat such that
A19: a = (p * (p |^ ka)) * la by NAT_D:def_3;
a = p * ((p |^ ka) * la) by A19;
then A20: p divides a by NAT_D:def_3;
consider kb being Nat such that
A21: p |-count b = kb + 1 by A16, NAT_1:6;
reconsider kb = kb as Element of NAT by ORDINAL1:def_12;
p |^ (p |-count b) divides b by A4, NAT_3:def_7;
then p * (p |^ kb) divides b by A21, NEWTON:6;
then consider lb being Nat such that
A22: b = (p * (p |^ kb)) * lb by NAT_D:def_3;
b = p * ((p |^ kb) * lb) by A22;
then p divides b by NAT_D:def_3;
then p divides 1 by A3, A20, NAT_D:def_5;
hence contradiction by A4, NAT_D:7; ::_thesis: verum
end;
thus (PFactors (a * b)) . i = p by A8, Th49
.= 0 + ((PFactors b) . p) by A16, Th49
.= ((PFactors a) . p) + ((PFactors b) . p) by A17, Th48
.= ((PFactors a) + (PFactors b)) . i by PRE_POLY:def_5 ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence PFactors (a * b) = (PFactors a) + (PFactors b) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MOEBIUS1:51
for n being non zero Element of NAT
for A being finite Subset of NAT st A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } holds
SMoebius A = EmptyBag NAT
proof
let n be non zero Element of NAT ; ::_thesis: for A being finite Subset of NAT st A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } holds
SMoebius A = EmptyBag NAT
let A be finite Subset of NAT; ::_thesis: ( A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } implies SMoebius A = EmptyBag NAT )
assume A1: A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } ; ::_thesis: SMoebius A = EmptyBag NAT
A2: A misses SCNAT
proof
assume A meets SCNAT ; ::_thesis: contradiction
then consider x being set such that
A3: x in A and
A4: x in SCNAT by XBOOLE_0:3;
ex k being Element of NAT st
( k = x & 0 < k & k divides n & k is square-containing ) by A1, A3;
hence contradiction by A4, Def2; ::_thesis: verum
end;
for x being set st x in NAT holds
(SMoebius A) . x = (EmptyBag NAT) . x
proof
let x be set ; ::_thesis: ( x in NAT implies (SMoebius A) . x = (EmptyBag NAT) . x )
assume x in NAT ; ::_thesis: (SMoebius A) . x = (EmptyBag NAT) . x
then reconsider k = x as Element of NAT ;
support (SMoebius A) = A /\ SCNAT by Def5
.= {} by A2, XBOOLE_0:def_7 ;
then (SMoebius A) . k = 0 by PRE_POLY:def_7;
hence (SMoebius A) . x = (EmptyBag NAT) . x by PRE_POLY:52; ::_thesis: verum
end;
hence SMoebius A = EmptyBag NAT by PBOOLE:3; ::_thesis: verum
end;
begin
definition
let n be non zero Nat;
func Radical n -> Element of NAT equals :: MOEBIUS1:def 7
Product (PFactors n);
coherence
Product (PFactors n) is Element of NAT ;
end;
:: deftheorem defines Radical MOEBIUS1:def_7_:_
for n being non zero Nat holds Radical n = Product (PFactors n);
theorem Th52: :: MOEBIUS1:52
for n being non zero Nat holds Radical n > 0
proof
let n be non zero Nat; ::_thesis: Radical n > 0
assume Radical n <= 0 ; ::_thesis: contradiction
then Product (PFactors n) = 0 ;
then consider f being FinSequence of COMPLEX such that
A1: Product f = 0 and
A2: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def_5;
for k being Nat holds
( not k in dom f or not f . k = 0 )
proof
given k being Nat such that A3: k in dom f and
A4: f . k = 0 ; ::_thesis: contradiction
k in dom (canFS (support (PFactors n))) by A2, A3, FUNCT_1:11;
then A5: ( rng (canFS (support (PFactors n))) c= support (PFactors n) & (canFS (support (PFactors n))) . k in rng (canFS (support (PFactors n))) ) by FINSEQ_1:def_4, FUNCT_1:3;
then (canFS (support (PFactors n))) . k in support (PFactors n) ;
then reconsider p = (canFS (support (PFactors n))) . k as prime Element of NAT by NEWTON:def_6;
p in support (PFactors n) by A5;
then A6: p in support (pfexp n) by Def6;
f . k = (PFactors n) . p by A2, A3, FUNCT_1:12
.= p by A6, Def6 ;
hence contradiction by A4; ::_thesis: verum
end;
hence contradiction by A1, RVSUM_1:103; ::_thesis: verum
end;
registration
let n be non zero Nat;
cluster Radical n -> non zero ;
coherence
not Radical n is empty by Th52;
end;
theorem :: MOEBIUS1:53
for p being Prime holds p = Radical p
proof
let p be Prime; ::_thesis: p = Radical p
A1: support (PFactors p) = support (pfexp p) by Def6
.= {p} by NAT_3:43 ;
reconsider p = p as prime Element of NAT by ORDINAL1:def_12;
reconsider f = <*p*> as FinSequence of NAT ;
rng f c= NAT by FINSEQ_1:def_4;
then rng f c= COMPLEX by NUMBERS:20, XBOOLE_1:1;
then A2: ( Product f = p & f is FinSequence of COMPLEX ) by FINSEQ_1:def_4, RVSUM_1:95;
f = (PFactors p) * <*p*> by Th46
.= (PFactors p) * (canFS {p}) by UPROOTS:4 ;
hence p = Radical p by A1, A2, NAT_3:def_5; ::_thesis: verum
end;
theorem Th54: :: MOEBIUS1:54
for p being Prime
for n being non zero Element of NAT holds Radical (p |^ n) = p
proof
let p be Prime; ::_thesis: for n being non zero Element of NAT holds Radical (p |^ n) = p
let n be non zero Element of NAT ; ::_thesis: Radical (p |^ n) = p
reconsider p = p as prime Element of NAT by ORDINAL1:def_12;
reconsider f = <*p*> as FinSequence of NAT ;
set s = p |^ n;
A1: f = (PFactors (p |^ n)) * <*p*> by Th47
.= (PFactors (p |^ n)) * (canFS {p}) by UPROOTS:4 ;
rng f c= NAT by FINSEQ_1:def_4;
then rng f c= COMPLEX by NUMBERS:20, XBOOLE_1:1;
then A2: ( Product f = p & f is FinSequence of COMPLEX ) by FINSEQ_1:def_4, RVSUM_1:95;
support (PFactors (p |^ n)) = support (pfexp (p |^ n)) by Def6
.= support (pfexp p) by NAT_3:48
.= {p} by NAT_3:43 ;
hence Radical (p |^ n) = p by A1, A2, NAT_3:def_5; ::_thesis: verum
end;
theorem Th55: :: MOEBIUS1:55
for n being non zero Nat holds Radical n divides n
proof
defpred S1[ Nat] means for n being non zero Nat st support (PFactors n) c= Seg $1 holds
Radical n divides n;
let n be non zero Nat; ::_thesis: Radical n divides n
A1: ex mS being Element of NAT st support (ppf n) c= Seg mS by Th14;
A2: support (ppf n) = support (pfexp n) by NAT_3:def_9
.= support (PFactors n) by Def6 ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let n be non zero Nat; ::_thesis: ( support (PFactors n) c= Seg (k + 1) implies Radical n divides n )
assume A5: support (PFactors n) c= Seg (k + 1) ; ::_thesis: Radical n divides n
A6: support (pfexp n) = support (PFactors n) by Def6;
percases ( not support (PFactors n) c= Seg k or support (PFactors n) c= Seg k ) ;
supposeA7: not support (PFactors n) c= Seg k ; ::_thesis: Radical n divides n
set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);
A8: now__::_thesis:_k_+_1_in_support_(PFactors_n)
assume A9: not k + 1 in support (PFactors n) ; ::_thesis: contradiction
support (PFactors n) c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (PFactors n) or x in Seg k )
assume A10: x in support (PFactors n) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
m <= k + 1 by A5, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then A11: m <= k by NAT_1:13;
x is Prime by A6, A10, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A11, FINSEQ_1:1; ::_thesis: verum
end;
hence contradiction by A7; ::_thesis: verum
end;
then A12: k + 1 is Prime by A6, NAT_3:34;
then A13: k + 1 > 1 by INT_2:def_4;
then (k + 1) |^ ((k + 1) |-count n) divides n by NAT_3:def_7;
then consider t being Nat such that
A14: n = ((k + 1) |^ ((k + 1) |-count n)) * t by NAT_D:def_3;
reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product (PFactors s) = Product f and
A16: f = (PFactors s) * (canFS (support (PFactors s))) by NAT_3:def_5;
A17: dom (PFactors s) = SetPrimes by PARTFUN1:def_2;
A18: support (ppf s) = support (pfexp s) by NAT_3:def_9;
then A19: support (ppf s) = support (PFactors s) by Def6;
(pfexp n) . (k + 1) = (k + 1) |-count n by A12, NAT_3:def_8;
then A20: (k + 1) |-count n <> 0 by A6, A8, PRE_POLY:def_7;
then A21: support (ppf s) = {(k + 1)} by A12, A18, NAT_3:42;
then A22: k + 1 in support (pfexp s) by A18, TARSKI:def_1;
A23: support (PFactors t) c= Seg k
proof
set f = (k + 1) |-count t;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (PFactors t) or x in Seg k )
assume A24: x in support (PFactors t) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
A25: x in support (pfexp t) by A24, Def6;
A26: now__::_thesis:_not_m_=_k_+_1
assume A27: m = k + 1 ; ::_thesis: contradiction
(pfexp t) . (k + 1) = (k + 1) |-count t by A12, NAT_3:def_8;
then (k + 1) |-count t <> 0 by A25, A27, PRE_POLY:def_7;
then (k + 1) |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A28: (k + 1) |-count t = 1 + g by NAT_1:10;
(k + 1) |^ ((k + 1) |-count t) divides t by A13, NAT_3:def_7;
then consider u being Nat such that
A29: t = ((k + 1) |^ ((k + 1) |-count t)) * u by NAT_D:def_3;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A14, A28, A29, NEWTON:6
.= (s * (k + 1)) * (((k + 1) |^ g) * u)
.= ((k + 1) |^ (((k + 1) |-count n) + 1)) * (((k + 1) |^ g) * u) by NEWTON:6 ;
then (k + 1) |^ (((k + 1) |-count n) + 1) divides n by NAT_D:def_3;
hence contradiction by A13, NAT_3:def_7; ::_thesis: verum
end;
support (pfexp t) c= support (pfexp n) by A14, NAT_3:45;
then support (PFactors t) c= support (PFactors n) by A6, Def6;
then m in support (PFactors n) by A24;
then m <= k + 1 by A5, FINSEQ_1:1;
then m < k + 1 by A26, XXREAL_0:1;
then A30: m <= k by NAT_1:13;
x is Prime by A25, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A30, FINSEQ_1:1; ::_thesis: verum
end;
then A31: Radical t divides t by A4;
support (PFactors s) = {(k + 1)} by A18, A21, Def6;
then f = (PFactors s) * <*(k + 1)*> by A16, UPROOTS:4
.= <*((PFactors s) . (k + 1))*> by A8, A17, FINSEQ_2:34 ;
then Product (PFactors s) = (PFactors s) . (k + 1) by A15, RVSUM_1:95
.= k + 1 by A22, Def6 ;
then A32: Radical s divides s by A20, NAT_3:3;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def_12;
support (ppf t) = support (pfexp t) by NAT_3:def_9;
then A33: support (ppf t) = support (PFactors t) by Def6;
A34: now__::_thesis:_not_support_(ppf_s)_meets_support_(ppf_t)
assume support (ppf s) meets support (ppf t) ; ::_thesis: contradiction
then consider x being set such that
A35: x in support (ppf s) and
A36: x in support (ppf t) by XBOOLE_0:3;
x in support (pfexp t) by A36, NAT_3:def_9;
then A37: x in support (PFactors t) by Def6;
x = k + 1 by A21, A35, TARSKI:def_1;
then k + 1 <= k by A23, A37, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
s1,t1 are_relative_prime
proof
set u = s1 gcd t1;
A38: s1 gcd t1 divides t1 by NAT_D:def_5;
s1 gcd t1 <> 0 by INT_2:5;
then A39: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume not s1,t1 are_relative_prime ; ::_thesis: contradiction
then s1 gcd t1 <> 1 by INT_2:def_3;
then s1 gcd t1 > 1 by A39, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A40: r is prime and
A41: r divides s1 gcd t1 by INT_2:31;
s1 gcd t1 divides s1 by NAT_D:def_5;
then r divides s1 by A41, NAT_D:4;
then r divides k + 1 by A40, NAT_3:5;
then ( r = 1 or r = k + 1 ) by A12, INT_2:def_4;
then k + 1 divides t1 by A40, A41, A38, INT_2:def_4, NAT_D:4;
then k + 1 in support (pfexp t) by A12, NAT_3:37;
then k + 1 in support (PFactors t) by Def6;
then k + 1 <= k by A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
then Radical n = Product ((PFactors s) + (PFactors t)) by A14, Th50
.= (Radical s) * (Radical t) by A34, A19, A33, NAT_3:19 ;
hence Radical n divides n by A14, A32, A31, NAT_3:1; ::_thesis: verum
end;
suppose support (PFactors n) c= Seg k ; ::_thesis: Radical n divides n
hence Radical n divides n by A4; ::_thesis: verum
end;
end;
end;
A42: S1[ 0 ]
proof
let n be non zero Nat; ::_thesis: ( support (PFactors n) c= Seg 0 implies Radical n divides n )
A43: {} c= support (PFactors n) by XBOOLE_1:2;
assume support (PFactors n) c= Seg 0 ; ::_thesis: Radical n divides n
then support (PFactors n) = {} by A43, XBOOLE_0:def_10;
then PFactors n = EmptyBag SetPrimes by BAGORDER:19;
then Radical n = 1 by NAT_3:20;
hence Radical n divides n by NAT_D:6; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A42, A3);
hence Radical n divides n by A1, A2; ::_thesis: verum
end;
theorem Th56: :: MOEBIUS1:56
for p being Prime
for n being non zero Nat holds
( p divides n iff p divides Radical n )
proof
let p be Prime; ::_thesis: for n being non zero Nat holds
( p divides n iff p divides Radical n )
let n be non zero Nat; ::_thesis: ( p divides n iff p divides Radical n )
thus ( p divides n implies p divides Radical n ) ::_thesis: ( p divides Radical n implies p divides n )
proof
assume that
A1: p divides n and
A2: not p divides Radical n ; ::_thesis: contradiction
A3: p in support (pfexp n) by A1, NAT_3:37;
then A4: p in support (PFactors n) by Def6;
then p in rng (canFS (support (PFactors n))) by FUNCT_2:def_3;
then consider y being set such that
A5: y in dom (canFS (support (PFactors n))) and
A6: p = (canFS (support (PFactors n))) . y by FUNCT_1:def_3;
consider f being FinSequence of COMPLEX such that
A7: Product (PFactors n) = Product f and
A8: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def_5;
( rng (PFactors n) c= NAT & rng f c= rng (PFactors n) ) by A8, RELAT_1:26, VALUED_0:def_6;
then A9: rng f c= NAT by XBOOLE_1:1;
support (PFactors n) c= dom (PFactors n) by PRE_POLY:37;
then A10: y in dom f by A4, A8, A5, A6, FUNCT_1:11;
reconsider f = f as FinSequence of NAT by A9, FINSEQ_1:def_4;
(PFactors n) . p = p by A3, Def6;
then f . y = p by A8, A6, A10, FUNCT_1:12;
then p in rng f by A10, FUNCT_1:3;
hence contradiction by A2, A7, NAT_3:7; ::_thesis: verum
end;
assume A11: p divides Radical n ; ::_thesis: p divides n
Radical n divides n by Th55;
hence p divides n by A11, NAT_D:4; ::_thesis: verum
end;
theorem Th57: :: MOEBIUS1:57
for k being non zero Nat st k is square-free holds
Radical k = k
proof
let k be non zero Nat; ::_thesis: ( k is square-free implies Radical k = k )
assume A1: k is square-free ; ::_thesis: Radical k = k
for i being set st i in SetPrimes holds
(PFactors k) . i = (ppf k) . i
proof
let i be set ; ::_thesis: ( i in SetPrimes implies (PFactors k) . i = (ppf k) . i )
assume i in SetPrimes ; ::_thesis: (PFactors k) . i = (ppf k) . i
then reconsider p = i as prime Element of NAT by NEWTON:def_6;
percases ( p in support (pfexp k) or not p in support (pfexp k) ) ;
supposeA2: p in support (pfexp k) ; ::_thesis: (PFactors k) . i = (ppf k) . i
A3: p <> 1 by INT_2:def_4;
p |-count k <> 0
proof
assume p |-count k = 0 ; ::_thesis: contradiction
then not p divides k by A3, NAT_3:27;
hence contradiction by A2, NAT_3:36; ::_thesis: verum
end;
then A4: p |-count k >= 1 by NAT_1:14;
p |-count k <= 1 by A1, Th24;
then p |-count k = 1 by A4, XXREAL_0:1;
then (ppf k) . p = p |^ 1 by A2, NAT_3:def_9
.= p by NEWTON:5 ;
hence (PFactors k) . i = (ppf k) . i by A2, Def6; ::_thesis: verum
end;
supposeA5: not p in support (pfexp k) ; ::_thesis: (PFactors k) . i = (ppf k) . i
then not p in support (PFactors k) by Def6;
then A6: (PFactors k) . p = 0 by PRE_POLY:def_7;
not p in support (ppf k) by A5, NAT_3:def_9;
hence (PFactors k) . i = (ppf k) . i by A6, PRE_POLY:def_7; ::_thesis: verum
end;
end;
end;
then PFactors k = ppf k by PBOOLE:3;
hence Radical k = k by NAT_3:61; ::_thesis: verum
end;
theorem :: MOEBIUS1:58
for n being non zero Nat holds Radical n <= n by Th55, NAT_D:7;
theorem :: MOEBIUS1:59
for p being Prime
for n being non zero Nat holds p |-count (Radical n) <= p |-count n by Th55, NAT_3:30;
theorem :: MOEBIUS1:60
for n being non zero Nat holds
( Radical n = 1 iff n = 1 )
proof
let n be non zero Nat; ::_thesis: ( Radical n = 1 iff n = 1 )
thus ( Radical n = 1 implies n = 1 ) ::_thesis: ( n = 1 implies Radical n = 1 )
proof
A1: rng (PFactors n) c= NAT by VALUED_0:def_6;
consider f being FinSequence of COMPLEX such that
A2: Product (PFactors n) = Product f and
A3: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def_5;
rng f c= rng (PFactors n) by A3, RELAT_1:26;
then rng f c= NAT by A1, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
assume A4: Radical n = 1 ; ::_thesis: n = 1
assume n <> 1 ; ::_thesis: contradiction
then consider p being Prime such that
A5: p divides n by Th5;
A6: p in support (pfexp n) by A5, NAT_3:37;
then A7: p in support (PFactors n) by Def6;
then p in rng (canFS (support (PFactors n))) by FUNCT_2:def_3;
then consider y being set such that
A8: ( y in dom (canFS (support (PFactors n))) & p = (canFS (support (PFactors n))) . y ) by FUNCT_1:def_3;
(PFactors n) . p = p by A6, Def6;
then A9: f . y = p by A3, A8, FUNCT_1:13;
support (PFactors n) c= dom (PFactors n) by PRE_POLY:37;
then y in dom f by A3, A7, A8, FUNCT_1:11;
then ( 1 < p & p in rng f ) by A9, FUNCT_1:3, INT_2:def_4;
hence contradiction by A4, A2, NAT_3:7, NAT_D:7; ::_thesis: verum
end;
thus ( n = 1 implies Radical n = 1 ) by Th45, NAT_3:20; ::_thesis: verum
end;
theorem Th61: :: MOEBIUS1:61
for p being Prime
for n being non zero Nat holds p |-count (Radical n) <= 1
proof
defpred S1[ Nat] means for n being non zero Nat st support (PFactors n) c= Seg $1 holds
for p being Prime holds p |-count (Radical n) <= 1;
let p be Prime; ::_thesis: for n being non zero Nat holds p |-count (Radical n) <= 1
let n be non zero Nat; ::_thesis: p |-count (Radical n) <= 1
A1: ex mS being Element of NAT st support (ppf n) c= Seg mS by Th14;
A2: support (ppf n) = support (pfexp n) by NAT_3:def_9
.= support (PFactors n) by Def6 ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let n be non zero Nat; ::_thesis: ( support (PFactors n) c= Seg (k + 1) implies for p being Prime holds p |-count (Radical n) <= 1 )
assume A5: support (PFactors n) c= Seg (k + 1) ; ::_thesis: for p being Prime holds p |-count (Radical n) <= 1
A6: support (pfexp n) = support (PFactors n) by Def6;
percases ( not support (PFactors n) c= Seg k or support (PFactors n) c= Seg k ) ;
supposeA7: not support (PFactors n) c= Seg k ; ::_thesis: for p being Prime holds p |-count (Radical n) <= 1
let p be Prime; ::_thesis: p |-count (Radical n) <= 1
reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
A8: now__::_thesis:_k_+_1_in_support_(PFactors_n)
assume A9: not k + 1 in support (PFactors n) ; ::_thesis: contradiction
support (PFactors n) c= Seg k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (PFactors n) or x in Seg k )
assume A10: x in support (PFactors n) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
m <= k + 1 by A5, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then A11: m <= k by NAT_1:13;
x is Prime by A6, A10, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A11, FINSEQ_1:1; ::_thesis: verum
end;
hence contradiction by A7; ::_thesis: verum
end;
then A12: r is Prime by A6, NAT_3:34;
then A13: r > 1 by INT_2:def_4;
then r |^ (r |-count n) divides n by NAT_3:def_7;
then consider t being Nat such that
A14: n = (r |^ (r |-count n)) * t by NAT_D:def_3;
reconsider s = r |^ (r |-count n), t = t as non zero Nat by A14;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def_12;
A15: support (ppf s) = support (pfexp s) by NAT_3:def_9;
then A16: support (ppf s) = support (PFactors s) by Def6;
A17: support (PFactors t) c= Seg k
proof
set f = r |-count t;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (PFactors t) or x in Seg k )
assume A18: x in support (PFactors t) ; ::_thesis: x in Seg k
then reconsider m = x as Nat ;
A19: x in support (pfexp t) by A18, Def6;
A20: now__::_thesis:_not_m_=_r
assume A21: m = r ; ::_thesis: contradiction
(pfexp t) . r = r |-count t by A12, NAT_3:def_8;
then r |-count t <> 0 by A19, A21, PRE_POLY:def_7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A22: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A13, NAT_3:def_7;
then consider u being Nat such that
A23: t = (r |^ (r |-count t)) * u by NAT_D:def_3;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
n = s * (((r |^ g) * r) * u) by A14, A22, A23, NEWTON:6
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def_3;
hence contradiction by A13, NAT_3:def_7; ::_thesis: verum
end;
support (pfexp t) c= support (pfexp n) by A14, NAT_3:45;
then support (PFactors t) c= support (PFactors n) by A6, Def6;
then m in support (PFactors n) by A18;
then m <= k + 1 by A5, FINSEQ_1:1;
then m < r by A20, XXREAL_0:1;
then A24: m <= k by NAT_1:13;
x is Prime by A19, NAT_3:34;
then 1 <= m by INT_2:def_4;
hence x in Seg k by A24, FINSEQ_1:1; ::_thesis: verum
end;
(pfexp n) . r = r |-count n by A12, NAT_3:def_8;
then A25: r |-count n <> 0 by A6, A8, PRE_POLY:def_7;
A26: p |-count (Radical s) <= 1
proof
percases ( p = r or p <> r ) ;
supposeA27: p = r ; ::_thesis: p |-count (Radical s) <= 1
A28: p > 1 by INT_2:def_4;
Radical s = r by A25, A27, Th54;
hence p |-count (Radical s) <= 1 by A27, A28, NAT_3:22; ::_thesis: verum
end;
suppose p <> r ; ::_thesis: p |-count (Radical s) <= 1
then p,r are_relative_prime by A12, INT_2:30;
then A29: not p divides r by PYTHTRIP:def_2;
A30: p > 1 by INT_2:def_4;
p |-count s = (r |-count n) * (p |-count r) by NAT_3:32
.= (r |-count n) * 0 by A29, A30, NAT_3:27
.= 0 ;
hence p |-count (Radical s) <= 1 by Th55, NAT_3:30; ::_thesis: verum
end;
end;
end;
A31: support (ppf s) = {r} by A12, A25, A15, NAT_3:42;
A32: now__::_thesis:_not_support_(ppf_s)_meets_support_(ppf_t)
assume support (ppf s) meets support (ppf t) ; ::_thesis: contradiction
then consider x being set such that
A33: x in support (ppf s) and
A34: x in support (ppf t) by XBOOLE_0:3;
x in support (pfexp t) by A34, NAT_3:def_9;
then A35: x in support (PFactors t) by Def6;
x = r by A31, A33, TARSKI:def_1;
then r <= k by A17, A35, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
support (ppf t) = support (pfexp t) by NAT_3:def_9;
then A36: support (ppf t) = support (PFactors t) by Def6;
A37: ( p |-count (Radical s) = 0 or p |-count (Radical t) = 0 )
proof
assume that
A38: p |-count (Radical s) <> 0 and
A39: p |-count (Radical t) <> 0 ; ::_thesis: contradiction
p |-count t > 0 by A39, Th55, NAT_3:30;
then (PFactors t) . p <> 0 by Th49;
then A40: p in support (PFactors t) by PRE_POLY:def_7;
p |-count s > 0 by A38, Th55, NAT_3:30;
then (PFactors s) . p <> 0 by Th49;
then p in support (PFactors s) by PRE_POLY:def_7;
hence contradiction by A32, A16, A36, A40, XBOOLE_0:3; ::_thesis: verum
end;
s1,t1 are_relative_prime
proof
set u = s1 gcd t1;
A41: s1 gcd t1 divides t1 by NAT_D:def_5;
s1 gcd t1 <> 0 by INT_2:5;
then A42: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume not s1,t1 are_relative_prime ; ::_thesis: contradiction
then s1 gcd t1 <> 1 by INT_2:def_3;
then s1 gcd t1 > 1 by A42, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider w being Element of NAT such that
A43: w is prime and
A44: w divides s1 gcd t1 by INT_2:31;
s1 gcd t1 divides s1 by NAT_D:def_5;
then w divides s1 by A44, NAT_D:4;
then w divides r by A43, NAT_3:5;
then ( w = 1 or w = r ) by A12, INT_2:def_4;
then r divides t1 by A43, A44, A41, INT_2:def_4, NAT_D:4;
then r in support (pfexp t) by A12, NAT_3:37;
then r in support (PFactors t) by Def6;
then k + 1 <= k by A17, FINSEQ_1:1;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
then Radical n = Product ((PFactors s) + (PFactors t)) by A14, Th50
.= (Radical s) * (Radical t) by A32, A16, A36, NAT_3:19 ;
then p |-count (Radical n) = (p |-count (Radical t)) + (p |-count (Radical s)) by NAT_3:28;
hence p |-count (Radical n) <= 1 by A4, A17, A37, A26; ::_thesis: verum
end;
suppose support (PFactors n) c= Seg k ; ::_thesis: for p being Prime holds p |-count (Radical n) <= 1
hence for p being Prime holds p |-count (Radical n) <= 1 by A4; ::_thesis: verum
end;
end;
end;
A45: S1[ 0 ]
proof
let n be non zero Nat; ::_thesis: ( support (PFactors n) c= Seg 0 implies for p being Prime holds p |-count (Radical n) <= 1 )
assume A46: support (PFactors n) c= Seg 0 ; ::_thesis: for p being Prime holds p |-count (Radical n) <= 1
let p be Prime; ::_thesis: p |-count (Radical n) <= 1
{} c= support (PFactors n) by XBOOLE_1:2;
then support (PFactors n) = {} by A46, XBOOLE_0:def_10;
then A47: PFactors n = EmptyBag SetPrimes by BAGORDER:19;
not p divides Radical n
proof
assume p divides Radical n ; ::_thesis: contradiction
then A48: p divides 1 by A47, NAT_3:20;
1 divides p by NAT_D:6;
then p = 1 by A48, NAT_D:5;
hence contradiction by INT_2:def_4; ::_thesis: verum
end;
hence p |-count (Radical n) <= 1 by Th6; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A45, A3);
hence p |-count (Radical n) <= 1 by A1, A2; ::_thesis: verum
end;
Lm3: for n being non zero Nat
for p being Prime holds not p |^ 2 divides Radical n
proof
let n be non zero Nat; ::_thesis: for p being Prime holds not p |^ 2 divides Radical n
let p be Prime; ::_thesis: not p |^ 2 divides Radical n
set PR = p |-count (Radical n);
A1: p <> 1 by INT_2:def_4;
assume A2: p |^ 2 divides Radical n ; ::_thesis: contradiction
A3: p |-count (Radical n) is non zero Element of NAT
proof
assume p |-count (Radical n) is not non zero Element of NAT ; ::_thesis: contradiction
then not p |^ (0 + 1) divides Radical n by A1, NAT_3:def_7;
then not p divides Radical n by NEWTON:5;
hence contradiction by A2, Th10; ::_thesis: verum
end;
p |-count (Radical n) >= 2
proof
assume p |-count (Radical n) < 2 ; ::_thesis: contradiction
then p |-count (Radical n) = 1 by A3, NAT_1:23;
then not p |^ (1 + 1) divides Radical n by A1, NAT_3:def_7;
hence contradiction by A2; ::_thesis: verum
end;
then p |-count (Radical n) > 1 by XXREAL_0:2;
hence contradiction by Th61; ::_thesis: verum
end;
Lm4: for n being non zero Nat holds Radical n is square-free
proof
let n be non zero Nat; ::_thesis: Radical n is square-free
assume Radical n is square-containing ; ::_thesis: contradiction
then ex p being Prime st p |^ 2 divides Radical n by Def1;
hence contradiction by Lm3; ::_thesis: verum
end;
registration
let n be non zero Nat;
cluster Radical n -> square-free ;
coherence
not Radical n is square-containing by Lm4;
end;
theorem :: MOEBIUS1:62
for n being non zero Nat holds Radical (Radical n) = Radical n by Th57;
theorem :: MOEBIUS1:63
for n being non zero Element of NAT
for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n
proof
let n be non zero Element of NAT ; ::_thesis: for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n
let p be Prime; ::_thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } ; ::_thesis: x in Seg n
then consider k being Element of NAT such that
A1: x = k and
A2: k > 0 and
A3: k divides Radical n and
p divides k ;
A4: 1 <= k by A2, NAT_1:14;
A5: Radical n <= n by Th55, NAT_D:7;
k <= Radical n by A3, NAT_D:7;
then k <= n by A5, XXREAL_0:2;
hence x in Seg n by A1, A4, FINSEQ_1:1; ::_thesis: verum
end;
theorem :: MOEBIUS1:64
for n being non zero Element of NAT
for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n
proof
let n be non zero Element of NAT ; ::_thesis: for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n
let p be Prime; ::_thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } ; ::_thesis: x in Seg n
then consider k being Element of NAT such that
A1: x = k and
A2: k > 0 and
A3: k divides Radical n and
not p divides k ;
A4: 1 <= k by A2, NAT_1:14;
A5: Radical n <= n by Th55, NAT_D:7;
k <= Radical n by A3, NAT_D:7;
then k <= n by A5, XXREAL_0:2;
hence x in Seg n by A1, A4, FINSEQ_1:1; ::_thesis: verum
end;
Lm5: for m, n being non zero Element of NAT st m divides n & m is square-free holds
m divides Radical n
proof
let m, n be non zero Element of NAT ; ::_thesis: ( m divides n & m is square-free implies m divides Radical n )
assume that
A1: m divides n and
A2: m is square-free ; ::_thesis: m divides Radical n
for p being Prime holds p |-count m <= p |-count (Radical n)
proof
let p be Prime; ::_thesis: p |-count m <= p |-count (Radical n)
A3: p > 1 by INT_2:def_4;
percases ( p divides m or not p divides m ) ;
suppose p divides m ; ::_thesis: p |-count m <= p |-count (Radical n)
then p divides n by A1, NAT_D:4;
then p divides Radical n by Th56;
then A4: p |-count (Radical n) <> 0 by A3, NAT_3:27;
p |-count (Radical n) <= 1 by Th61;
then A5: p |-count (Radical n) < 1 + 1 by NAT_1:13;
p |-count m <= 1 by A2, Th24;
hence p |-count m <= p |-count (Radical n) by A5, A4, NAT_1:23; ::_thesis: verum
end;
suppose not p divides m ; ::_thesis: p |-count m <= p |-count (Radical n)
hence p |-count m <= p |-count (Radical n) by A3, NAT_3:27; ::_thesis: verum
end;
end;
end;
hence m divides Radical n by Th19; ::_thesis: verum
end;
theorem Th65: :: MOEBIUS1:65
for k, n being non zero Nat holds
( ( k divides n & k is square-free ) iff k divides Radical n )
proof
let k, n be non zero Nat; ::_thesis: ( ( k divides n & k is square-free ) iff k divides Radical n )
A1: ( k divides Radical n implies ( k divides n & k is square-free ) )
proof
assume A2: k divides Radical n ; ::_thesis: ( k divides n & k is square-free )
Radical n divides n by Th55;
hence ( k divides n & k is square-free ) by A2, Th26, NAT_D:4; ::_thesis: verum
end;
( k is non zero Element of NAT & n is non zero Element of NAT ) by ORDINAL1:def_12;
hence ( ( k divides n & k is square-free ) iff k divides Radical n ) by A1, Lm5; ::_thesis: verum
end;
theorem :: MOEBIUS1:66
for n being non zero Nat holds { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
proof
let n be non zero Nat; ::_thesis: { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
thus { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } c= { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } :: according to XBOOLE_0:def_10 ::_thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } c= { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } or x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } ; ::_thesis: x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
then consider k1 being Element of NAT such that
A1: k1 = x and
A2: 0 < k1 and
A3: ( k1 divides n & k1 is square-free ) ;
k1 divides Radical n by A2, A3, Th65;
hence x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } by A1, A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } or x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } ; ::_thesis: x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) }
then consider k1 being Element of NAT such that
A4: ( x = k1 & 0 < k1 ) and
A5: k1 divides Radical n ;
A6: k1 is square-free by A5, Th26;
Radical n divides n by Th55;
then k1 divides n by A5, NAT_D:4;
hence x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } by A4, A6; ::_thesis: verum
end;