:: by Adam Grabowski

::

:: Received July 12, 2013

:: Copyright (c) 2013-2016 Association of Mizar Users

registration

let a, b be non zero Nat;

coherence

not a gcd b is zero by INT_2:5;

coherence

not a lcm b is zero by INT_2:4;

end;
coherence

not a gcd b is zero by INT_2:5;

coherence

not a lcm b is zero by INT_2:4;

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 )

ex k being non zero Nat st

( k <> 1 & k divides a & k divides b )

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

for m, n being Nat holds

( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m )

( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m )

proof end;

definition

existence

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = 1 / (primenumber i);

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = 1 / (primenumber i) ) & ( for i being Nat holds b_{2} . i = 1 / (primenumber i) ) holds

b_{1} = b_{2};

end;

func ReciPrime -> Real_Sequence means :ReciPr: :: MOEBIUS2:def 1

for i being Nat holds it . i = 1 / (primenumber i);

correctness for i being Nat holds it . i = 1 / (primenumber i);

existence

ex b

for i being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem ReciPr defines ReciPrime MOEBIUS2:def 1 :

for b_{1} being Real_Sequence holds

( b_{1} = ReciPrime iff for i being Nat holds b_{1} . i = 1 / (primenumber i) );

for b

( b

definition

correctness

existence

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = 1 / i;

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = 1 / i ) & ( for i being Nat holds b_{2} . i = 1 / i ) holds

b_{1} = b_{2};

end;
existence

ex b

for i being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem DefRec defines invNAT MOEBIUS2:def 2 :

for b_{1} being Real_Sequence holds

( b_{1} = invNAT iff for i being Nat holds b_{1} . i = 1 / i );

for b

( b

registration
end;

registration

let f be nonnegative-yielding Real_Sequence;

coherence

for b_{1} being subsequence of f holds b_{1} is nonnegative-yielding

end;
coherence

for b

proof end;

registration
end;

registration

coherence

for b_{1} being Real_Sequence st b_{1} = Partial_Sums ReciPrime holds

b_{1} is non-decreasing

end;
for b

b

proof 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

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;

ex b_{1} being ManySortedSet of SetPrimes st

( support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ ((p |-count n) div 2) ) )

for b_{1}, b_{2} being ManySortedSet of SetPrimes st support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ ((p |-count n) div 2) ) & support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ ((p |-count n) div 2) ) holds

b_{1} = b_{2}

end;
func SqFactors n -> ManySortedSet of SetPrimes means :SqDef: :: MOEBIUS2:def 3

( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ ((p |-count n) div 2) ) );

existence ( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ ((p |-count n) div 2) ) );

ex b

( support b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem SqDef defines SqFactors MOEBIUS2:def 3 :

for n being non zero Nat

for b_{2} being ManySortedSet of SetPrimes holds

( b_{2} = SqFactors n iff ( support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ ((p |-count n) div 2) ) ) );

for n being non zero Nat

for b

( b

b

registration

let n be non zero Nat;

coherence

( SqFactors n is finite-support & SqFactors n is natural-valued )

end;
coherence

( SqFactors n is finite-support & SqFactors n is natural-valued )

proof end;

registration

let n be non zero Nat;

coherence

for b_{1} being Element of support (SqFactors n) holds b_{1} is natural
;

end;
coherence

for b

:: deftheorem defines SqF MOEBIUS2:def 4 :

for n being non zero Nat holds SqF n = Product (SqFactors n);

for n being non zero Nat holds SqF n = Product (SqFactors n);

registration
end;

definition

let p be Prime;

ex b_{1} being Subset of NAT st

for n being Nat holds

( n in b_{1} iff ( n is square-free & ( for i being Prime st i divides n holds

i <= p ) ) )

for b_{1}, b_{2} being Subset of NAT st ( for n being Nat holds

( n in b_{1} iff ( n is square-free & ( for i being Prime st i divides n holds

i <= p ) ) ) ) & ( for n being Nat holds

( n in b_{2} iff ( n is square-free & ( for i being Prime st i divides n holds

i <= p ) ) ) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds

( n in it iff ( n is square-free & ( for i being Prime st i divides n holds

i <= p ) ) );

ex b

for n being Nat holds

( n in b

i <= p ) ) )

proof end;

uniqueness for b

( n in b

i <= p ) ) ) ) & ( for n being Nat holds

( n in b

i <= p ) ) ) ) holds

b

proof end;

:: deftheorem FG defines FreeGen MOEBIUS2:def 5 :

for p being Prime

for b_{2} being Subset of NAT holds

( b_{2} = FreeGen p iff for n being Nat holds

( n in b_{2} iff ( n is square-free & ( for i being Prime st i divides n holds

i <= p ) ) ) );

for p being Prime

for b

( b

( n in b

i <= p ) ) ) );

registration

ex b_{1} being Nat st

( b_{1} is square-free & not b_{1} is zero )
by MOEBIUS1:22;

end;

cluster epsilon-transitive epsilon-connected ordinal natural non zero complex V26() ext-real non negative finite cardinal integer dim-like square-free for set ;

existence ex b

( b

registration

let p be Prime;

ex b_{1} being bag of Seg p st b_{1} is positive-yielding

end;
cluster Relation-like Seg p -defined RAT -valued Function-like V14( Seg p) complex-valued ext-real-valued real-valued natural-valued finite-support positive-yielding for set ;

existence ex b

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 (support g))

for g being positive-yielding bag of Seg p st g = p |-> p holds

g = g * (canFS (support g))

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

for f being positive-yielding bag of Seg p st f = p |-> p holds

Product f = p |^ p

proof end;

registration
end;

registration

let p be Prime;

coherence

for b_{1} being Element of FreeGen p holds not b_{1} is empty
by MOEBIUS1:21, FG;

end;
coherence

for b

:: deftheorem defines BoolePrime MOEBIUS2:def 6 :

for p being Prime holds BoolePrime p = Funcs (((Seg p) /\ SetPrimes),2);

for p being Prime holds BoolePrime p = Funcs (((Seg p) /\ SetPrimes),2);

registration
end;

definition

let p be Prime;

ex b_{1} being Function of (FreeGen p),(BoolePrime p) st

for x being Element of FreeGen p holds b_{1} . x = (pfexp x) | ((Seg p) /\ SetPrimes)

for b_{1}, b_{2} being Function of (FreeGen p),(BoolePrime p) st ( for x being Element of FreeGen p holds b_{1} . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) & ( for x being Element of FreeGen p holds b_{2} . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) holds

b_{1} = b_{2}

end;
func canHom p -> Function of (FreeGen p),(BoolePrime p) means :canH: :: MOEBIUS2:def 7

for x being Element of FreeGen p holds it . x = (pfexp x) | ((Seg p) /\ SetPrimes);

existence for x being Element of FreeGen p holds it . x = (pfexp x) | ((Seg p) /\ SetPrimes);

ex b

for x being Element of FreeGen p holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem canH defines canHom MOEBIUS2:def 7 :

for p being Prime

for b_{2} being Function of (FreeGen p),(BoolePrime p) holds

( b_{2} = canHom p iff for x being Element of FreeGen p holds b_{2} . x = (pfexp x) | ((Seg p) /\ SetPrimes) );

for p being Prime

for b

( b

registration
end;

LmX: for p being Prime holds card (FreeGen p) c= 2 |^ p

proof end;

registration
end;

theorem MB149: :: MOEBIUS2:43

for n being non zero Nat

for p being Prime st p |-count n <> 0 holds

(SqFactors n) . p = p |^ ((p |-count n) div 2)

for p being Prime st p |-count n <> 0 holds

(SqFactors n) . 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) = (SqFactors m) + (SqFactors n)

SqFactors (m * n) = (SqFactors m) + (SqFactors n)

proof end;

registration
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 (support f)) )

( Product f = Product g & g = f * (canFS (support f)) )

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

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 (Product f) >= n

for p being Prime

for f being bag of SetPrimes st f . p = p |^ n holds

p |-count (Product f) >= n

proof end;

definition

let n be non zero Nat;

ex b_{1} being ManySortedSet of SetPrimes st

( support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ (2 * ((p |-count n) div 2)) ) )

for b_{1}, b_{2} being ManySortedSet of SetPrimes st support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ (2 * ((p |-count n) div 2)) ) & support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ (2 * ((p |-count n) div 2)) ) holds

b_{1} = b_{2}

end;
func TSqFactors n -> ManySortedSet of SetPrimes means :TSqDef: :: MOEBIUS2:def 8

( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ (2 * ((p |-count n) div 2)) ) );

existence ( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ (2 * ((p |-count n) div 2)) ) );

ex b

( support b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem TSqDef defines TSqFactors MOEBIUS2:def 8 :

for n being non zero Nat

for b_{2} being ManySortedSet of SetPrimes holds

( b_{2} = TSqFactors n iff ( support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ (2 * ((p |-count n) div 2)) ) ) );

for n being non zero Nat

for b

( b

b

registration

let n be non zero Nat;

coherence

( TSqFactors n is finite-support & TSqFactors n is natural-valued )

end;
coherence

( TSqFactors n is finite-support & TSqFactors n is natural-valued )

proof end;

:: deftheorem defines TSqF MOEBIUS2:def 9 :

for n being non zero Nat holds TSqF n = Product (TSqFactors n);

for n being non zero Nat holds TSqF n = Product (TSqFactors n);

registration
end;

theorem MB149T: :: MOEBIUS2:51

for n being non zero Nat

for p being Prime st p |-count n <> 0 holds

(TSqFactors n) . p = p |^ (2 * ((p |-count n) div 2))

for p being Prime st p |-count n <> 0 holds

(TSqFactors n) . 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) = (TSqFactors m) + (TSqFactors n)

TSqFactors (m * n) = (TSqFactors m) + (TSqFactors n)

proof end;

registration

let n be non zero Nat;

coherence

for b_{1} being Nat st b_{1} = n div (TSqF n) holds

not b_{1} is square-containing

end;
coherence

for b

not b

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

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

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

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;

coherence

LattStr(# C,L,M #) is join-commutative by BINOP_1:def 2;

end;
let L be commutative BinOp of C;

let M be BinOp of C;

coherence

LattStr(# C,L,M #) is join-commutative by BINOP_1:def 2;

registration

let C be non empty set ;

let L be BinOp of C;

let M be commutative BinOp of C;

coherence

LattStr(# C,L,M #) is meet-commutative by BINOP_1:def 2;

end;
let L be BinOp of C;

let M be commutative BinOp of C;

coherence

LattStr(# C,L,M #) is meet-commutative by BINOP_1:def 2;

registration

let C be non empty set ;

let L be associative BinOp of C;

let M be BinOp of C;

coherence

LattStr(# C,L,M #) is join-associative by BINOP_1:def 3;

end;
let L be associative BinOp of C;

let M be BinOp of C;

coherence

LattStr(# C,L,M #) is join-associative by BINOP_1:def 3;

registration

let C be non empty set ;

let L be BinOp of C;

let M be associative BinOp of C;

coherence

LattStr(# C,L,M #) is meet-associative by BINOP_1:def 3;

end;
let L be BinOp of C;

let M be associative BinOp of C;

coherence

LattStr(# C,L,M #) is meet-associative by BINOP_1:def 3;

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

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

for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds

x gcd y in NatDivisors n

proof end;

registration

coherence

( hcflat is commutative & hcflat is associative ) by NAT_LAT:def 3;

coherence

( lcmlat is commutative & lcmlat is associative ) by NAT_LAT:def 3;

end;
( hcflat is commutative & hcflat is associative ) by NAT_LAT:def 3;

coherence

( lcmlat is commutative & lcmlat is associative ) by NAT_LAT:def 3;

registration

coherence

hcflatplus is commutative by CutComm, HcfLat;

coherence

lcmlatplus is commutative by CutComm, LcmLat;

coherence

hcflatplus is associative by CutAssoc, HcfLat;

coherence

lcmlatplus is associative by CutAssoc, LcmLat;

end;
hcflatplus is commutative by CutComm, HcfLat;

coherence

lcmlatplus is commutative by CutComm, LcmLat;

coherence

hcflatplus is associative by CutAssoc, HcfLat;

coherence

lcmlatplus is associative by CutAssoc, LcmLat;

:: The lattice of natural divisors

definition

let n be non zero Nat;

ex b_{1} being strict SubLattice of NatPlus_Lattice st the carrier of b_{1} = NatDivisors n

for b_{1}, b_{2} being strict SubLattice of NatPlus_Lattice st the carrier of b_{1} = NatDivisors n & the carrier of b_{2} = NatDivisors n holds

b_{1} = b_{2}

end;
func Divisors_Lattice n -> strict SubLattice of NatPlus_Lattice means :DivLat: :: MOEBIUS2:def 10

the carrier of it = NatDivisors n;

existence the carrier of it = NatDivisors n;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DivLat defines Divisors_Lattice MOEBIUS2:def 10 :

for n being non zero Nat

for b_{2} being strict SubLattice of NatPlus_Lattice holds

( b_{2} = Divisors_Lattice n iff the carrier of b_{2} = NatDivisors n );

for n being non zero Nat

for b

( b

registration
end;

theorem OperLat: :: MOEBIUS2:63

for n being non zero Nat

for a, b being Element of (Divisors_Lattice n) holds

( a "\/" b = a lcm b & a "/\" b = a gcd b )

for a, b being Element of (Divisors_Lattice n) 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 (Divisors_Lattice n);

correctness

compatibility

p "\/" q = p lcm q;

by OperLat;

correctness

compatibility

p "/\" q = p gcd q;

by OperLat;

end;
let p, q be Element of (Divisors_Lattice n);

correctness

compatibility

p "\/" q = p lcm q;

by OperLat;

correctness

compatibility

p "/\" q = p gcd q;

by OperLat;

registration

let n be non zero Nat;

coherence

( Divisors_Lattice n is distributive & Divisors_Lattice n is bounded )

end;
coherence

( Divisors_Lattice n is distributive & Divisors_Lattice n is bounded )

proof end;

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

proof end;

registration
end;

registration

let n be non zero Nat;

coherence

for b_{1} being Element of (Divisors_Lattice n) holds not b_{1} is zero

end;
coherence

for b

proof end;