:: On Square-free Numbers
::
:: Copyright (c) 2013-2021 Association of Mizar Users

registration
let a, b be non zero Nat;
cluster a gcd b -> non zero ;
coherence
not a gcd b is zero
by INT_2:5;
cluster a lcm b -> non zero ;
coherence
not a lcm b is zero
by INT_2:4;
end;

registration
let n be Nat;
reduce 0 -' n to 0 ;
reducibility
proof end;
end;

theorem :: MOEBIUS2:1
for n, i being Nat st n >= 2 |^ ((2 * i) + 2) holds
n / 2 >= (2 |^ i) * (sqrt n)
proof end;

theorem :: MOEBIUS2:2
for n being Nat holds support () c= SetPrimes
proof end;

theorem FOT1: :: MOEBIUS2:3
for n being non zero Nat holds n - ((n div 2) * 2) <= 1
proof end;

theorem FOTN: :: MOEBIUS2:4
for a, n being non zero Nat holds (n div a) * a <= n
proof end;

theorem RelPrimeEx: :: MOEBIUS2:5
for a, b being non zero Nat st not a,b are_coprime holds
ex k being non zero Nat st
( k <> 1 & k divides a & k divides b )
proof end;

theorem DivNonZero: :: MOEBIUS2:6
for n, a being non zero Nat st a divides n holds
n div a <> 0
proof end;

theorem INT615: :: MOEBIUS2:7
for i, j being Nat st i,j are_coprime holds
i lcm j = i * j
proof end;

registration
let f be natural-valued FinSequence;
coherence
proof end;
end;

theorem :: MOEBIUS2:8
proof end;

theorem LS2: :: MOEBIUS2:9
proof end;

theorem :: MOEBIUS2:10
proof end;

theorem LS3: :: MOEBIUS2:11
proof end;

theorem :: MOEBIUS2:12
proof end;

lem6: 2 divides 2 * 3
;

lem8: 2 divides 2 * 4
;

lem9: 3 divides 3 * 3
;

lem10: 2 divides 2 * 5
;

lem12: 2 divides 2 * 6
;

theorem :: MOEBIUS2:13
proof end;

theorem LS4: :: MOEBIUS2:14
proof end;

theorem :: MOEBIUS2:15
proof end;

theorem LS11: :: MOEBIUS2:16
proof end;

theorem :: MOEBIUS2:17
proof end;

theorem LS13: :: MOEBIUS2:18
proof end;

theorem :: MOEBIUS2:19
proof end;

theorem :: MOEBIUS2:20
for m, n being Nat holds
proof end;

theorem Cosik1: :: MOEBIUS2:21
for n, m being Nat holds
proof end;

definition
func ReciPrime -> Real_Sequence means :ReciPr: :: MOEBIUS2:def 1
for i being Nat holds it . i = 1 / ();
correctness
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / ()
;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / () ) & ( for i being Nat holds b2 . i = 1 / () ) holds
b1 = b2
;
proof end;
end;

:: deftheorem ReciPr defines ReciPrime MOEBIUS2:def 1 :
for b1 being Real_Sequence holds
( b1 = ReciPrime iff for i being Nat holds b1 . i = 1 / () );

notation
let f be Real_Sequence;
antonym divergent f for convergent ;
end;

registration
coherence
proof end;
end;

registration
coherence
not ReciPrime is divergent
;
end;

definition
func invNAT -> Real_Sequence means :DefRec: :: MOEBIUS2:def 2
for i being Nat holds it . i = 1 / i;
correctness
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / i
;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / i ) & ( for i being Nat holds b2 . i = 1 / i ) holds
b1 = b2
;
proof end;
end;

:: deftheorem DefRec defines invNAT MOEBIUS2:def 2 :
for b1 being Real_Sequence holds
( b1 = invNAT iff for i being Nat holds b1 . i = 1 / i );

registration
coherence
proof end;
end;

registration
coherence
not invNAT is divergent
proof end;
end;

theorem LimId: :: MOEBIUS2:22
proof end;

theorem RecSub: :: MOEBIUS2:23
proof end;

registration
let f be nonnegative-yielding Real_Sequence;
coherence
for b1 being subsequence of f holds b1 is nonnegative-yielding
proof end;
end;

registration
coherence by RecSub;
end;

theorem :: MOEBIUS2:24

registration
coherence
for b1 being Real_Sequence st b1 = Partial_Sums ReciPrime holds
b1 is non-decreasing
proof end;
end;

theorem :: MOEBIUS2:25
for f being nonnegative-yielding Real_Sequence st f is summable holds
for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p
proof end;

definition
let n be non zero Nat;
func SqFactors n -> ManySortedSet of SetPrimes means :SqDef: :: MOEBIUS2:def 3
( support it = support () & ( for p being Nat st p in support () holds
it . p = p |^ ((p |-count n) div 2) ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support () & ( for p being Nat st p in support () holds
b1 . p = p |^ ((p |-count n) div 2) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support () & ( for p being Nat st p in support () holds
b1 . p = p |^ ((p |-count n) div 2) ) & support b2 = support () & ( for p being Nat st p in support () holds
b2 . p = p |^ ((p |-count n) div 2) ) holds
b1 = b2
proof end;
end;

:: deftheorem SqDef defines SqFactors MOEBIUS2:def 3 :
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = SqFactors n iff ( support b2 = support () & ( for p being Nat st p in support () holds
b2 . p = p |^ ((p |-count n) div 2) ) ) );

registration
let n be non zero Nat;
coherence
proof end;
end;

registration
let n be non zero Nat;
cluster -> natural for Element of support ();
coherence
for b1 being Element of support () holds b1 is natural
;
end;

definition
let n be non zero Nat;
func SqF n -> Nat equals :: MOEBIUS2:def 4
Product ();
coherence
Product () is Nat
;
end;

:: deftheorem defines SqF MOEBIUS2:def 4 :
for n being non zero Nat holds SqF n = Product ();

theorem Matsu: :: MOEBIUS2:26
for f being bag of SetPrimes holds Product f <> 0
proof end;

registration
let n be non zero Nat;
cluster SqF n -> non zero ;
coherence
not SqF n is zero
by Matsu;
end;

definition
let p be Prime;
func FreeGen p -> Subset of NAT means :FG: :: MOEBIUS2:def 5
for n being Nat holds
( n in it iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) )
proof end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) & ( for n being Nat holds
( n in b2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem FG defines FreeGen MOEBIUS2:def 5 :
for p being Prime
for b2 being Subset of NAT holds
( b2 = FreeGen p iff for n being Nat holds
( n in b2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) );

theorem Ex1: :: MOEBIUS2:27
for p being Prime holds 1 in FreeGen p
proof end;

theorem :: MOEBIUS2:28
for p being Prime holds not 0 in FreeGen p by ;

registration
existence
ex b1 being Nat st
( b1 is square-free & not b1 is zero )
by MOEBIUS1:22;
end;

registration
let p be Prime;
existence
ex b1 being bag of Seg p st b1 is positive-yielding
proof end;
end;

theorem Thds: :: MOEBIUS2:29
for p being Prime
for f being positive-yielding bag of Seg p holds dom f = support f
proof end;

theorem domcanFS: :: MOEBIUS2:30
for p being Prime holds dom (canFS (Seg p)) = Seg p
proof end;

theorem :: MOEBIUS2:31
for A being finite set holds dom () = Seg (card A)
proof end;

theorem ThCon: :: MOEBIUS2:32
for p being Prime
for g being positive-yielding bag of Seg p st g = p |-> p holds
g = g * (canFS ())
proof end;

theorem :: MOEBIUS2:33
for p being Prime
for f being positive-yielding bag of Seg p st f = p |-> p holds
Product f = p |^ p
proof end;

theorem Lm1: :: MOEBIUS2:34
for p being Prime
for n being non zero Nat st n in FreeGen p holds
support () c= Seg p
proof end;

theorem :: MOEBIUS2:35
for p being Prime
for n being non zero Nat st n in FreeGen p holds
card (support ()) <= p
proof end;

theorem LmRng: :: MOEBIUS2:36
for n being non zero square-free Nat holds rng () c= 2
proof end;

theorem WOW: :: MOEBIUS2:37
for m, n being non zero Nat st pfexp m = pfexp n holds
m = n
proof end;

registration
let p be Prime;
cluster FreeGen p -> non empty ;
coherence
not FreeGen p is empty
by Ex1;
end;

registration
let p be Prime;
cluster -> non empty for Element of FreeGen p;
coherence
for b1 being Element of FreeGen p holds not b1 is empty
by ;
end;

definition
let p be Prime;
func BoolePrime p -> set equals :: MOEBIUS2:def 6
Funcs (((Seg p) /\ SetPrimes),2);
coherence
Funcs (((Seg p) /\ SetPrimes),2) is set
;
end;

:: deftheorem defines BoolePrime MOEBIUS2:def 6 :
for p being Prime holds BoolePrime p = Funcs (((Seg p) /\ SetPrimes),2);

registration
let p be Prime;
coherence ;
end;

definition
let p be Prime;
func canHom p -> Function of (),() means :canH: :: MOEBIUS2:def 7
for x being Element of FreeGen p holds it . x = () | ((Seg p) /\ SetPrimes);
existence
ex b1 being Function of (),() st
for x being Element of FreeGen p holds b1 . x = () | ((Seg p) /\ SetPrimes)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being Element of FreeGen p holds b1 . x = () | ((Seg p) /\ SetPrimes) ) & ( for x being Element of FreeGen p holds b2 . x = () | ((Seg p) /\ SetPrimes) ) holds
b1 = b2
proof end;
end;

:: deftheorem canH defines canHom MOEBIUS2:def 7 :
for p being Prime
for b2 being Function of (),() holds
( b2 = canHom p iff for x being Element of FreeGen p holds b2 . x = () | ((Seg p) /\ SetPrimes) );

registration
let p be Prime;
coherence
proof end;
end;

theorem FinCar: :: MOEBIUS2:38
for p being Prime holds card () c= card ()
proof end;

LmX: for p being Prime holds card () c= 2 |^ p
proof end;

registration
let p be Prime;
coherence
proof end;
end;

theorem :: MOEBIUS2:39
for p being Prime holds card () <= 2 |^ p
proof end;

theorem Ciek: :: MOEBIUS2:40
for n, i being Nat
for p being Prime st n <> 0 & p |^ i divides n holds
i <= p |-count n
proof end;

theorem MoInv: :: MOEBIUS2:41
for n being Nat st n <> 0 & ( for p being Prime holds p |-count n <= 1 ) holds
n is square-free
proof end;

theorem MB148: :: MOEBIUS2:42
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
() . p = 0
proof end;

theorem MB149: :: MOEBIUS2:43
for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
() . p = p |^ ((p |-count n) div 2)
proof end;

theorem MB150: :: MOEBIUS2:44
for m, n being non zero Nat st m,n are_coprime holds
SqFactors (m * n) = () + ()
proof end;

theorem :: MOEBIUS2:45
for n being non zero Nat holds SqF n divides n
proof end;

registration
let n be non zero Nat;
coherence
proof end;
end;

theorem Matsu0: :: MOEBIUS2:46
for f being bag of SetPrimes ex g being FinSequence of NAT st
( Product f = Product g & g = f * (canFS ()) )
proof end;

theorem Matsu1: :: MOEBIUS2:47
for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |^ n divides Product f
proof end;

theorem BZE: :: MOEBIUS2:48
for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |-count () >= n
proof end;

definition
let n be non zero Nat;
func TSqFactors n -> ManySortedSet of SetPrimes means :TSqDef: :: MOEBIUS2:def 8
( support it = support () & ( for p being Nat st p in support () holds
it . p = p |^ (2 * ((p |-count n) div 2)) ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support () & ( for p being Nat st p in support () holds
b1 . p = p |^ (2 * ((p |-count n) div 2)) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support () & ( for p being Nat st p in support () holds
b1 . p = p |^ (2 * ((p |-count n) div 2)) ) & support b2 = support () & ( for p being Nat st p in support () holds
b2 . p = p |^ (2 * ((p |-count n) div 2)) ) holds
b1 = b2
proof end;
end;

:: deftheorem TSqDef defines TSqFactors MOEBIUS2:def 8 :
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = TSqFactors n iff ( support b2 = support () & ( for p being Nat st p in support () holds
b2 . p = p |^ (2 * ((p |-count n) div 2)) ) ) );

theorem :: MOEBIUS2:49
for n being non zero Nat holds TSqFactors n = () |^ 2
proof end;

registration
let n be non zero Nat;
coherence
proof end;
end;

definition
let n be non zero Nat;
func TSqF n -> Nat equals :: MOEBIUS2:def 9
Product ();
coherence
Product () is Nat
;
end;

:: deftheorem defines TSqF MOEBIUS2:def 9 :
for n being non zero Nat holds TSqF n = Product ();

registration
let n be non zero Nat;
cluster TSqF n -> non zero ;
coherence
not TSqF n is zero
by Matsu;
end;

theorem MB148T: :: MOEBIUS2:50
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
() . p = 0
proof end;

theorem MB149T: :: MOEBIUS2:51
for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
() . p = p |^ (2 * ((p |-count n) div 2))
proof end;

theorem MB150T: :: MOEBIUS2:52
for m, n being non zero Nat st m,n are_coprime holds
TSqFactors (m * n) = () + ()
proof end;

registration
let n be non zero Nat;
coherence ;
end;

theorem Skup: :: MOEBIUS2:53
for n being non zero Nat holds TSqF n divides n
proof end;

registration
let n be non zero Nat;
cluster n div (TSqF n) -> square-free for Nat;
coherence
for b1 being Nat st b1 = n div (TSqF n) holds
not b1 is square-containing
proof end;
end;

theorem SqCon1: :: MOEBIUS2:54
for n, k being non zero Nat st k <> 1 & k ^2 divides n holds
n is square-containing
proof end;

theorem DivRelPrime: :: MOEBIUS2:55
for n being non zero square-free Nat
for a being non zero Nat st a divides n holds
a,n div a are_coprime
proof end;

theorem CutComm: :: MOEBIUS2:56
for A, C being non empty set
for L being commutative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative
proof end;

theorem CutAssoc: :: MOEBIUS2:57
for A, C being non empty set
for L being associative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is associative
proof end;

registration
let C be non empty set ;
let L be commutative BinOp of C;
let M be BinOp of C;
cluster LattStr(# C,L,M #) -> join-commutative ;
coherence
LattStr(# C,L,M #) is join-commutative
by BINOP_1:def 2;
end;

registration
let C be non empty set ;
let L be BinOp of C;
let M be commutative BinOp of C;
cluster LattStr(# C,L,M #) -> meet-commutative ;
coherence
LattStr(# C,L,M #) is meet-commutative
by BINOP_1:def 2;
end;

registration
let C be non empty set ;
let L be associative BinOp of C;
let M be BinOp of C;
cluster LattStr(# C,L,M #) -> join-associative ;
coherence
LattStr(# C,L,M #) is join-associative
by BINOP_1:def 3;
end;

registration
let C be non empty set ;
let L be BinOp of C;
let M be associative BinOp of C;
cluster LattStr(# C,L,M #) -> meet-associative ;
coherence
LattStr(# C,L,M #) is meet-associative
by BINOP_1:def 3;
end;

theorem DivInPlus: :: MOEBIUS2:58
for n being non zero Nat holds NatDivisors n c= NATPLUS by NAT_LAT:def 6;

theorem LCMDiv: :: MOEBIUS2:59
for n being non zero Nat
for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x lcm y in NatDivisors n
proof end;

theorem GCDDiv: :: MOEBIUS2:60
for n being non zero Nat
for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x gcd y in NatDivisors n
proof end;

registration
let n be non zero Nat;
cluster NatDivisors n -> non empty ;
coherence
not NatDivisors n is empty
by MOEBIUS1:39;
end;

registration
coherence by NAT_LAT:def 3;
coherence by NAT_LAT:def 3;
end;

theorem HcfLat: :: MOEBIUS2:61
proof end;

theorem LcmLat: :: MOEBIUS2:62
proof end;

registration
coherence by ;
coherence by ;
coherence by ;
coherence by ;
end;

:: The lattice of natural divisors
definition
let n be non zero Nat;
func Divisors_Lattice n -> strict SubLattice of NatPlus_Lattice means :DivLat: :: MOEBIUS2:def 10
the carrier of it = NatDivisors n;
existence
ex b1 being strict SubLattice of NatPlus_Lattice st the carrier of b1 = NatDivisors n
proof end;
uniqueness
for b1, b2 being strict SubLattice of NatPlus_Lattice st the carrier of b1 = NatDivisors n & the carrier of b2 = NatDivisors n holds
b1 = b2
proof end;
end;

:: deftheorem DivLat defines Divisors_Lattice MOEBIUS2:def 10 :
for n being non zero Nat
for b2 being strict SubLattice of NatPlus_Lattice holds
( b2 = Divisors_Lattice n iff the carrier of b2 = NatDivisors n );

registration
let n be non zero Nat;
cluster the carrier of () -> natural-membered ;
coherence
the carrier of () is natural-membered
proof end;
end;

theorem OperLat: :: MOEBIUS2:63
for n being non zero Nat
for a, b being Element of () holds
( a "\/" b = a lcm b & a "/\" b = a gcd b )
proof end;

registration
let n be non zero Nat;
let p, q be Element of ();
identify p "\/" q with p lcm q;
correctness
compatibility
p "\/" q = p lcm q
;
by OperLat;
identify p "/\" q with p gcd q;
correctness
compatibility
p "/\" q = p gcd q
;
by OperLat;
end;

registration
let n be non zero Nat;
coherence
not Divisors_Lattice n is empty
;
end;

registration
let n be non zero Nat;
coherence
proof end;
end;

theorem TopBot: :: MOEBIUS2:64
for n being non zero Nat holds
( Top () = n & Bottom () = 1 )
proof end;

SquareBool0: for n being non zero square-free Nat holds Divisors_Lattice n is Boolean
proof end;

registration
let n be non zero square-free Nat;
coherence by SquareBool0;
end;

registration
let n be non zero Nat;
cluster -> non zero for Element of the carrier of ();
coherence
for b1 being Element of () holds not b1 is zero
proof end;
end;

theorem :: MOEBIUS2:65
for n being non zero Nat holds
( Divisors_Lattice n is Boolean iff n is square-free )
proof end;