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