:: by Adam Grabowski

::

:: Received March 27, 2018

:: Copyright (c) 2018 Association of Mizar Users

registration

ex b_{1} being Nat st

( not b_{1} is zero & b_{1} is square & not b_{1} is trivial )
end;

cluster non trivial V21() V22() V23() V27() non zero complex V32() integer dim-like ext-real non negative square for Nat;

existence ex b

( not b

proof end;

registration

let Z be Subset of REAL;

let f be PartFunc of Z,REAL;

let A be Subset of REAL;

coherence

for b_{1} being PartFunc of Z,REAL st b_{1} = f | A holds

b_{1} is A -defined
;

end;
let f be PartFunc of Z,REAL;

let A be Subset of REAL;

coherence

for b

b

theorem ContCut: :: MOEBIUS3:3

for Z being open Subset of REAL

for A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds

((id Z) ^) | A is continuous

for A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds

((id Z) ^) | A is continuous

proof end;

theorem :: MOEBIUS3:4

for n being Nat

for Z being open Subset of REAL

for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & A = [.1,(n + 1).] holds

integral (((id Z) ^),A) = ln . (n + 1)

for Z being open Subset of REAL

for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & A = [.1,(n + 1).] holds

integral (((id Z) ^),A) = ln . (n + 1)

proof end;

theorem :: MOEBIUS3:5

for n being Nat

for Z being open Subset of REAL

for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & 0 < n & A = [.n,(n + 1).] holds

integral (((id Z) ^),A) = ln . ((n + 1) / n)

for Z being open Subset of REAL

for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & 0 < n & A = [.n,(n + 1).] holds

integral (((id Z) ^),A) = ln . ((n + 1) / n)

proof end;

theorem Th36: :: MOEBIUS3:7

for f being summable Real_Sequence

for n being Nat st f is positive-yielding holds

Sum (f ^\ (n + 1)) > 0

for n being Nat st f is positive-yielding holds

Sum (f ^\ (n + 1)) > 0

proof end;

:: n-th harmonic number

:: deftheorem defines Harmonic MOEBIUS3:def 1 :

for n being Nat holds Harmonic n = (Partial_Sums invNAT) . n;

for n being Nat holds Harmonic n = (Partial_Sums invNAT) . n;

theorem Diesel3: :: MOEBIUS3:21

for A being non empty closed_interval Subset of REAL

for Z being open Subset of REAL

for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds

integral (((id Z) ^),A) < 1 / n

for Z being open Subset of REAL

for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds

integral (((id Z) ^),A) < 1 / n

proof end;

registration
end;

theorem Telescoping: :: MOEBIUS3:24

for a, b, s being Real_Sequence st ( for n being Nat holds s . n = (a . n) + (b . n) ) & ( for k being Nat holds b . k = - (a . (k + 1)) ) holds

for n being Nat holds (Partial_Sums s) . n = (a . 0) + (b . n)

for n being Nat holds (Partial_Sums s) . n = (a . 0) + (b . n)

proof end;

theorem Impor3: :: MOEBIUS3:25

for f1, f2 being Real_Sequence

for n being non trivial Nat st ( for k being non trivial Nat st k <= n holds

f1 . k < f2 . k ) holds

Sum (f1,n,1) < Sum (f2,n,1)

for n being non trivial Nat st ( for k being non trivial Nat st k <= n holds

f1 . k < f2 . k ) holds

Sum (f1,n,1) < Sum (f2,n,1)

proof end;

definition

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = 1 / ((n ^2) - (1 / 4))

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = 1 / ((n ^2) - (1 / 4)) ) & ( for n being Nat holds b_{2} . n = 1 / ((n ^2) - (1 / 4)) ) holds

b_{1} = b_{2}
end;

func Reci-seq1 -> Real_Sequence means :MyDef: :: MOEBIUS3:def 2

for n being Nat holds it . n = 1 / ((n ^2) - (1 / 4));

existence for n being Nat holds it . n = 1 / ((n ^2) - (1 / 4));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem MyDef defines Reci-seq1 MOEBIUS3:def 2 :

for b_{1} being Real_Sequence holds

( b_{1} = Reci-seq1 iff for n being Nat holds b_{1} . n = 1 / ((n ^2) - (1 / 4)) );

for b

( b

AlgDef: for n being Nat

for a, b being Real holds (rseq (0,1,a,b)) . n = 1 / ((a * n) + b)

proof end;

Tele2: for n being Nat holds Reci-seq1 . n = ((rseq (0,1,1,(- (1 / 2)))) . n) + ((- (rseq (0,1,1,(1 / 2)))) . n)

proof end;

theorem :: MOEBIUS3:27

definition

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = 1 + (1 / (primenumber n))

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

b_{1} = b_{2}
end;

func Reci-seq2 -> Real_Sequence means :My3Def: :: MOEBIUS3:def 3

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

existence for n being Nat holds it . n = 1 + (1 / (primenumber n));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem My3Def defines Reci-seq2 MOEBIUS3:def 3 :

for b_{1} being Real_Sequence holds

( b_{1} = Reci-seq2 iff for n being Nat holds b_{1} . n = 1 + (1 / (primenumber n)) );

for b

( b

:: deftheorem defines SetPrimes MOEBIUS3:def 4 :

for n being Nat holds SetPrimes n = SetPrimes /\ (Seg n);

for n being Nat holds SetPrimes n = SetPrimes /\ (Seg n);

theorem :: MOEBIUS3:35

definition

let n be Nat;

card (SetPrimes n) is Nat ;

end;
:: just to get an index for appropriate sequence of primes

coherence card (SetPrimes n) is Nat ;

theorem KeyValue: :: MOEBIUS3:45

for m being natural-valued finite-support ManySortedSet of SetPrimes

for p being Prime st support m = {p} holds

Product m = m . p

for p being Prime st support m = {p} holds

Product m = m . p

proof end;

registration

let n be non zero Nat;

coherence

for b_{1} being Nat st b_{1} = n div ((SqF n) |^ 2) holds

not b_{1} is square-containing

end;
coherence

for b

not b

proof end;

::: TSqF n should be revised to allow zero for an argument

:: deftheorem defines SquarefreePart MOEBIUS3:def 6 :

for n being non zero Nat holds SquarefreePart n = n div (TSqF n);

for n being non zero Nat holds SquarefreePart n = n div (TSqF n);

Surprise: for n, m being non zero Nat st m ^2 divides SquarefreePart n holds

m = 1

proof end;

theorem :: MOEBIUS3:51

definition

let A be finite Subset of SetPrimes;

coherence

(EmptyBag SetPrimes) +* (id A) is bag of SetPrimes

end;
coherence

(EmptyBag SetPrimes) +* (id A) is bag of SetPrimes

proof end;

:: deftheorem defines -bag MOEBIUS3:def 7 :

for A being finite Subset of SetPrimes holds A -bag = (EmptyBag SetPrimes) +* (id A);

for A being finite Subset of SetPrimes holds A -bag = (EmptyBag SetPrimes) +* (id A);

theorem BagValue: :: MOEBIUS3:55

for A being finite Subset of SetPrimes

for i being object st i in support (A -bag) holds

(A -bag) . i = i

for i being object st i in support (A -bag) holds

(A -bag) . i = i

proof end;

registration
end;

ProdSqF: for A being finite Subset of SetPrimes holds Product (A -bag) is square-free

proof end;

registration

let A be finite Subset of SetPrimes;

coherence

for b_{1} being Nat st b_{1} = Product (A -bag) holds

not b_{1} is square-containing
by ProdSqF;

end;
coherence

for b

not b

theorem :: MOEBIUS3:57

for n being non zero Nat

for x being object st x in bool (SetPrimes n) holds

x is finite Subset of SetPrimes

for x being object st x in bool (SetPrimes n) holds

x is finite Subset of SetPrimes

proof end;

theorem :: MOEBIUS3:58

for n being non zero Nat

for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds

x `1 is finite Subset of SetPrimes

for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds

x `1 is finite Subset of SetPrimes

proof end;

:: Later we should show the connection between sum and products of

:: sequences with exponential function, respectively.

:: sequences with exponential function, respectively.

theorem :: MOEBIUS3:63

for n being Nat holds ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . n

proof end;

definition

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 0 & ( for i being non zero Nat holds b_{1} . i = 1 / (SquarefreePart i) ) )

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

b_{1} = b_{2}

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 0 & ( for i being non zero Nat holds b_{1} . i = 1 / (TSqF i) ) )

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

b_{1} = b_{2}
end;

func Reci-Sqf -> Real_Sequence means :MySumDef: :: MOEBIUS3:def 8

( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / (SquarefreePart i) ) );

existence ( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / (SquarefreePart i) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

func Reci-TSq -> Real_Sequence means :MySum2Def: :: MOEBIUS3:def 9

( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / (TSqF i) ) );

existence ( it . 0 = 0 & ( for i being non zero Nat holds it . i = 1 / (TSqF i) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem MySumDef defines Reci-Sqf MOEBIUS3:def 8 :

for b_{1} being Real_Sequence holds

( b_{1} = Reci-Sqf iff ( b_{1} . 0 = 0 & ( for i being non zero Nat holds b_{1} . i = 1 / (SquarefreePart i) ) ) );

for b

( b

:: deftheorem MySum2Def defines Reci-TSq MOEBIUS3:def 9 :

for b_{1} being Real_Sequence holds

( b_{1} = Reci-TSq iff ( b_{1} . 0 = 0 & ( for i being non zero Nat holds b_{1} . i = 1 / (TSqF i) ) ) );

for b

( b

theorem :: MOEBIUS3:68

for n being Nat holds (Partial_Sums (rseq (0,1,1,0))) . n <= ((Partial_Sums Reci-Sqf) . n) * ((Partial_Sums Reci-TSq) . n) by SERIES_3:39, Seqs1, Seqs4, Core1;

definition

let n be non zero Nat;

ex b_{1} being Function of [:(bool (SetPrimes n)),(Seg n):],NAT st

for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b_{1} . x = (Product ((A,1) -bag)) * (k ^2)

for b_{1}, b_{2} being Function of [:(bool (SetPrimes n)),(Seg n):],NAT st ( for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b_{1} . x = (Product ((A,1) -bag)) * (k ^2) ) & ( for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b_{2} . x = (Product ((A,1) -bag)) * (k ^2) ) holds

b_{1} = b_{2}

end;
func Compose n -> Function of [:(bool (SetPrimes n)),(Seg n):],NAT means :: MOEBIUS3:def 10

for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

it . x = (Product ((A,1) -bag)) * (k ^2);

existence for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

it . x = (Product ((A,1) -bag)) * (k ^2);

ex b

for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b

proof end;

uniqueness for b

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b

b

proof end;

:: deftheorem defines Compose MOEBIUS3:def 10 :

for n being non zero Nat

for b_{2} being Function of [:(bool (SetPrimes n)),(Seg n):],NAT holds

( b_{2} = Compose n iff for x being Element of [:(bool (SetPrimes n)),(Seg n):]

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b_{2} . x = (Product ((A,1) -bag)) * (k ^2) );

for n being non zero Nat

for b

( b

for A being finite Subset of SetPrimes

for k being Nat st x = [A,k] holds

b

definition

let n be Nat;

{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } is Subset of REAL

end;
func ReciProducts n -> Subset of REAL equals :: MOEBIUS3:def 11

{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;

coherence { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;

{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } is Subset of REAL

proof end;

:: deftheorem defines ReciProducts MOEBIUS3:def 11 :

for n being Nat holds ReciProducts n = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;

for n being Nat holds ReciProducts n = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;

theorem :: MOEBIUS3:76

for n being Nat st n + 1 is Prime holds

ReciProducts (n + 1) = (ReciProducts n) \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

ReciProducts (n + 1) = (ReciProducts n) \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

proof end;

theorem :: MOEBIUS3:77

for n being Nat st n + 1 is Prime holds

ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

proof end;