:: Sequences of Prime Reciprocals -- Preliminaries
:: by Adam Grabowski
::
:: Received March 27, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, INT_1,
SQUARE_1, SEQ_1, MEASURE5, FACIRC_1, FUNCT_4, ABIAN, VALUED_1, REALSET1,
SERIES_1, POWER, FUNCT_7, FINSET_1, CARD_1, MCART_1, MOEBIUS1, RCOMP_1,
SIN_COS, TAYLOR_2, INTEGRA5, PYTHTRIP, BASEL_1, LIMFUNC1, PRE_POLY,
XXREAL_2, PARTFUN1, NEWTON, XXREAL_0, ORDINAL4, XBOOLE_0, REAL_1, INT_2,
TARSKI, PARTFUN3, NAT_1, TAYLOR_1, SEQ_4, XXREAL_1, FDIFF_1, PBOOLE,
NAT_3, CARD_3, VALUED_0, UPROOTS, INT_7, SERIES_3, XCMPLX_0, SUBSET_1,
ZFMISC_1, NUMBERS, MOEBIUS2, MOEBIUS3, INTEGRA1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XTUPLE_0,
XXREAL_0, XCMPLX_0, VALUED_0, ZFMISC_1, FINSET_1, SQUARE_1, ABIAN, INT_1,
INT_2, NAT_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, VALUED_1, FUNCT_4,
FINSEQ_1, PARTFUN3, PRE_POLY, RCOMP_1, FCONT_1, MEASURE5, RFUNCT_1,
SEQ_4, PBOOLE, NAT_D, SEQ_1, SEQ_2, RVSUM_1, SERIES_1, PYTHTRIP, UPROOTS,
BINOP_1, NEWTON, POWER, TAYLOR_1, INT_7, SERIES_3, NAT_3, PEPIN,
MOEBIUS1, MOEBIUS2, PARTFUN1, SIN_COS, RELSET_1, PARTFUN2, FDIFF_1,
LIMFUNC1, INTEGRA5, TAYLOR_2, BASEL_1;
constructors SIN_COS, UPROOTS, INT_7, SERIES_3, COMSEQ_2, INTEGRA1, FCONT_1,
TAYLOR_2, ABIAN, MOEBIUS1, FINSOP_1, RVSUM_1, BAGORDER, SERIES_1, REAL_1,
PARTFUN3, PEPIN, NAT_3, RELSET_1, RECDEF_1, MOEBIUS2, TAYLOR_1, PYTHTRIP,
INTEGRA5, SEQ_4, PARTFUN2, BASEL_1, FDIFF_1, LIMFUNC1;
registrations RELSET_1, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSET_1,
XXREAL_0, FUNCT_1, NEWTON, XCMPLX_0, NUMBERS, ORDINAL1, PRE_POLY, NAT_3,
MOEBIUS2, RCOMP_1, COMSEQ_3, INT_7, SEQ_4, XBOOLE_0, VALUED_0, XXREAL_2,
FUNCT_2, MEASURE5, ABIAN, INTEGRA1, RELAT_1, NEWTON03, XTUPLE_0,
SUBSET_1, VALUED_1, FCONT_3, POWER, NEWTON04;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_2;
equalities SERIES_1, SQUARE_1, BINOP_1, MOEBIUS2, LIMFUNC1;
expansions TARSKI, INT_2, NAT_D;
theorems FINSEQ_2, RVSUM_1, XCMPLX_1, ORDINAL1, SQUARE_1, NAT_1, POWER,
NEWTON, XREAL_1, FINSEQ_1, RELAT_1, XREAL_0, SERIES_1, INTEGRA9,
TAYLOR_1, RFUNCT_1, ENTROPY1, FDIFF_5, FUNCT_2, SEQ_1, XXREAL_0, INT_2,
PEPIN, FUNCT_1, PBOOLE, TARSKI, NAT_3, MOEBIUS1, NAT_D, INT_1, XBOOLE_1,
XBOOLE_0, PARTFUN1, PARTFUN3, SERIES_3, FDIFF_1, NAT_2, VALUED_1,
ZFMISC_1, PRE_POLY, INT_7, FINSEQ_3, PREPOWER, MOEBIUS2, XXREAL_1,
MEASURE5, XXREAL_2, FCONT_1, DIFF_4, TAYLOR_2, INTEGRA5, INTEGRA6,
RSSPACE2, SIN_COS, CATALAN2, PYTHTRIP, CARDFIL4, FUNCT_4, BASEL_1;
schemes NAT_1, SEQ_1, FRAENKEL, NAT_2, FUNCT_3;
begin :: Preliminaries
reserve n,i,k,m for Nat;
reserve p for Prime;
registration
cluster non zero square non trivial for Nat;
existence
proof
4 = 2 ^2; then
4 is non zero square;
hence thesis by NAT_2:28;
end;
end;
registration let Z be Subset of REAL;
let f be PartFunc of Z, REAL;
let A be Subset of REAL;
cluster f | A -> A-defined for PartFunc of Z, REAL;
coherence;
end;
theorem
for Z being Subset of REAL st 0 in Z holds
(id Z)"{0} = {0}
proof
let Z be Subset of REAL;
assume 0 in Z; then
{0} c= Z by ZFMISC_1:31;
hence thesis by FUNCT_2:94;
end;
theorem Counter0:
for Z being Subset of REAL st not 0 in Z holds
(id Z)"{0} = {}
proof
let Z be Subset of REAL;
assume
AA: not 0 in Z;
(id Z)"{0} c= {}
proof
let x be object;
assume x in (id Z)"{0}; then
A2: x in dom id Z & (id Z).x in {0} by FUNCT_1:def 7; then
(id Z).x = x by FUNCT_1:17;
hence thesis by A2,AA,TARSKI:def 1;
end;
hence thesis;
end;
theorem ContCut:
for Z being open Subset of REAL,
A being non empty closed_interval Subset of REAL st
not 0 in Z & A c= Z holds
((id Z)^) | A is continuous
proof
let Z be open Subset of REAL,
A be non empty closed_interval Subset of REAL;
assume
A1: not 0 in Z & A c= Z; then
(id Z)^ is_differentiable_on Z by FDIFF_5:4; then
((id Z)^) | Z is continuous by FDIFF_1:25;
hence thesis by A1,FCONT_1:16;
end;
theorem
for Z being open Subset of REAL,
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
let Z be open Subset of REAL,
A be non empty closed_interval Subset of REAL;
assume
Z1: Z = right_open_halfline 0 & A = [.1,n+1.]; then
N1: not 0 in Z by XXREAL_1:4;
A1: A c= Z
proof
let x be object;
assume aa: x in A; then
reconsider xx = x as Real;
1 <= xx & xx <= n + 1 by aa,Z1,XXREAL_1:1;
hence thesis by Z1,XXREAL_1:235;
end;
set f = id Z;
a3: dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2
.= Z \ {} by Counter0,N1
.= Z;
B1: lower_bound A = 1 by Z1,XREAL_1:31,XXREAL_2:25;
B2: upper_bound A = n + 1 by Z1,XREAL_1:31,XXREAL_2:29;
(id Z)^ | A is continuous by ContCut,A1,N1; then
integral ((id Z)^,A) = ln.(upper_bound A)-ln.(lower_bound A)
by A1,Z1,TAYLOR_1:18,a3,INTEGRA9:61
.= ln.(n + 1) - (1 - 1) by ENTROPY1:2,B1,B2
.= ln.(n + 1);
hence thesis;
end;
theorem
for Z being open Subset of REAL,
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
let Z be open Subset of REAL,
A be non empty closed_interval Subset of REAL;
assume
Z1: Z = right_open_halfline 0 & 0 < n & A = [.n, n+1.];
N1: not 0 in Z by XXREAL_1:4,Z1;
A1: A c= Z
proof
let x be object;
assume aa: x in A; then
reconsider xx = x as Real;
n <= xx & xx <= n + 1 by aa,Z1,XXREAL_1:1;
hence thesis by XXREAL_1:235,Z1;
end;
set f = id Z;
a3: dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2
.= Z \ {} by Counter0,N1
.= Z;
B1: lower_bound A = n by Z1,XREAL_1:31,XXREAL_2:25;
B2: upper_bound A = n + 1 by Z1,XREAL_1:31,XXREAL_2:29;
(id Z)^ | A is continuous by ContCut,A1,N1; then
integral ((id Z)^,A) = ln.(upper_bound A)-ln.(lower_bound A)
by A1,Z1,TAYLOR_1:18,a3,INTEGRA9:61
.= ln.((n + 1) / n) by Z1,DIFF_4:4,B1,B2;
hence thesis;
end;
theorem MacPositive:
for x,r being Real st x > 0 & r > 0 holds
Maclaurin(exp_R,].-r,r.[,x) is positive-yielding
proof
let x,r be Real;
assume
A0: x > 0 & r > 0;
set f = Maclaurin(exp_R,].-r,r.[,x);
for r being Real st r in rng f holds 0 < r
proof
let r be Real;
assume r in rng f; then
consider xx being object such that
A1: xx in dom f & r = f.xx by FUNCT_1:def 3;
reconsider nn = xx as Element of NAT by A1;
r = x |^ nn / (nn!) by A1,TAYLOR_2:8,A0;
hence thesis by A0;
end;
hence thesis by PARTFUN3:def 1;
end;
theorem Th36:
for f be summable Real_Sequence, n be Nat st
f is positive-yielding holds
Sum (f ^\ (n+1)) > 0
proof
let f be summable Real_Sequence, n be Nat;
assume
A0: f is positive-yielding;
set LS = f ^\ (n + 1);
A2: for i be Nat holds 0 <= LS.i
proof
let i be Nat;
a1: LS.i = f.(n+1+i) by NAT_1:def 3;
n+1+i in NAT by ORDINAL1:def 12; then
n+1+i in dom f by FUNCT_2:def 1; then
f.(n+1+i) in rng f by FUNCT_1:3;
hence thesis by PARTFUN3:def 1,A0,a1;
end;
ex i be Nat st i in dom LS & 0 < LS.i
proof
consider j be Nat such that
A3: n + 1 <= j;
j - (n + 1) in NAT by A3,INT_1:5; then
reconsider i = j - (n + 1) as Nat;
take i;
A4: n + 1 + i = j;
aa: dom LS = NAT by FUNCT_2:def 1;
A6: LS.i = f.j by NAT_1:def 3,A4;
j in NAT by ORDINAL1:def 12; then
j in dom f by FUNCT_2:def 1; then
f.j in rng f by FUNCT_1:3;
hence thesis by aa,A6,A0,PARTFUN3:def 1,ORDINAL1:def 12;
end; then
consider k be Nat such that
A6: k in dom LS & LS.k > 0;
LS is summable by SERIES_1:12;
hence thesis by A6,RSSPACE2:3,A2;
end;
begin :: Harmonic Numbers
:: n-th harmonic number
definition let n be Nat;
func Harmonic n -> Real equals
(Partial_Sums invNAT).n;
coherence;
end;
theorem Harm0:
Harmonic 0 = 0
proof
Harmonic 0 = invNAT.0 by SERIES_1:def 1
.= 1 / 0 by MOEBIUS2:def 2
.= 0;
hence thesis;
end;
theorem Harmon1:
Harmonic (n + 1) = Harmonic n + 1 / (n + 1)
proof
(Partial_Sums invNAT).(n + 1)
= (Partial_Sums invNAT).n + invNAT.(n + 1) by SERIES_1:def 1
.= Harmonic n + 1 / (n + 1) by MOEBIUS2:def 2;
hence thesis;
end;
theorem Harm1:
Harmonic 1 = 1
proof
Harmonic (0 + 1) = Harmonic 0 + 1 / (0 + 1) by Harmon1
.= 1 by Harm0;
hence thesis;
end;
theorem
Harmonic 2 = 3 / 2
proof
Harmonic (1 + 1) = Harmonic 1 + 1 / (1 + 1) by Harmon1
.= 3 / 2 by Harm1;
hence thesis;
end;
begin :: On Exponents and Logarithms
theorem LogZero:
ln.1 = 0
proof
A2: number_e <> 1 by TAYLOR_1:11;
A1: 1 in right_open_halfline 0 by XXREAL_1:235;
ln.1 = log(number_e, 1) by A1,TAYLOR_1:def 2,def 3
.= 0 by TAYLOR_1:11,A2,POWER:51;
hence thesis;
end;
theorem
for x being Real st x > 0 holds
exp_R.x > x + 1 ::: shorter proof of strenghtened BOR_CANT:2
proof
let x be Real;
assume
AA: x > 0;
set r = 1;
set f = Maclaurin(exp_R,].-r,r.[,x);
A4: exp_R.x = Sum f by TAYLOR_2:16;
A2: f.0 = x |^ 0 / (0!) by TAYLOR_2:8
.= 1 by NEWTON:4,12;
A3: f.1 = x |^ 1 / (1!) by TAYLOR_2:8
.= x by NEWTON:13;
SS: f is absolutely_summable by TAYLOR_2:16; then
A6: Sum f = (Partial_Sums f).1 + Sum (f ^\ (1 + 1)) by SERIES_1:15
.= ((Partial_Sums f).0 + f.(0 + 1)) + Sum (f ^\ (1 + 1))
by SERIES_1:def 1
.= (1 + x) + Sum (f ^\ (1 + 1)) by A2,A3,SERIES_1:def 1;
f is positive-yielding & f is summable by MacPositive,AA,SS;
hence thesis by A4,A6,XREAL_1:29,Th36;
end;
theorem Diesel1:
for x being Real st x > 0 holds
ln.(x + 1) < x
proof
let x be Real;
assume x > 0; then
x + 1 > 1 by XREAL_1:29; then
ln.(x + 1) < (x + 1) - 1 by ENTROPY1:2;
hence thesis;
end;
theorem Diesel2:
for n being Nat st n > 0 holds
ln.((n + 1) / n) < 1 / n
proof
let n be Nat;
assume
A1: n > 0;
(n + 1) / n = n / n + 1 / n by XCMPLX_1:62
.= 1 + 1 / n by A1,XCMPLX_1:60;
hence thesis by Diesel1,A1;
end;
theorem LogExp:
for x being Real holds
ln.(exp_R.x) = x
proof
let x be Real;
A1: exp_R.x in right_open_halfline 0 by XXREAL_1:235,SIN_COS:54;
log (number_e, exp_R.x) = x by TAYLOR_1:13;
hence thesis by A1,TAYLOR_1:def 3,def 2;
end;
theorem LogMono:
for x,y being Real st 0 < x < y holds
ln.x < ln.y
proof
let x,y be Real;
assume
A1: 0 < x < y; then
A2: x in right_open_halfline 0 & y in right_open_halfline 0 by XXREAL_1:235;
number_e > 1 by XXREAL_0:2,TAYLOR_1:11; then
log (number_e, x) < log (number_e, y) by A1,POWER:57; then
(log_number_e).x < log (number_e, y) by A2,TAYLOR_1:def 2;
hence thesis by TAYLOR_1:def 3,TAYLOR_1:def 2,A2;
end;
theorem
for n being non zero Nat holds
ln.(n+1) > 0
proof
let n be non zero Nat;
0 + 1 < n + 1 by XREAL_1:8;
hence thesis by LogZero,LogMono;
end;
theorem LogAdd:
for x,y being Real st 0 < x & 0 < y holds
ln.(x * y) = ln.x + ln.y
proof
let x,y be Real;
assume
A1: 0 < x & 0 < y; then
A2: x in right_open_halfline 0 & y in right_open_halfline 0 by XXREAL_1:235;
a2: x * y in right_open_halfline 0 by XXREAL_1:235,A1;
A3: number_e > 1 by XXREAL_0:2,TAYLOR_1:11;
ln.(x * y) = log (number_e,x * y) by a2,TAYLOR_1:def 2,def 3
.= log (number_e,x) + log(number_e,y) by POWER:53,A1,A3
.= log (number_e,x) + (log_number_e).y by TAYLOR_1:def 2,A2
.= ln.x + ln.y by TAYLOR_1:def 3,def 2,A2;
hence thesis;
end;
theorem
for x being Real holds
ex y being non zero Nat st x < ln.(ln.(y + 1))
proof
let x be Real;
set N = [/ exp_R.(exp_R.x) \];
A1: exp_R.(exp_R.x) > 0 by SIN_COS:54; then
N > 0; then
N in NAT by INT_1:3; then
reconsider N as non zero Nat by SIN_COS:54,INT_1:def 7;
take N;
A3: exp_R.x > 0 by SIN_COS:54;
ln.(exp_R.(exp_R.x)) < ln.(N + 1) by A1,LogMono,INT_1:32; then
exp_R.x < ln.(N + 1) by LogExp; then
ln.(exp_R.x) < ln.(ln.(N + 1)) by A3,LogMono;
hence thesis by LogExp;
end;
theorem Diesel3:
for A being non empty closed_interval Subset of REAL,
Z being open Subset of REAL,
n being non zero Nat st
Z = right_open_halfline 0 & A = [.n, n+1.] holds
integral ((id Z)^,A) < 1 / n
proof
let A be non empty closed_interval Subset of REAL,
Z be open Subset of REAL,
n be non zero Nat;
assume
aa: Z = right_open_halfline 0 & A = [.n, n+1.];
N1: not 0 in Z by aa,XXREAL_1:4;
A1: A c= Z
proof
let x be object;
assume BB: x in A; then
reconsider xx = x as Real;
n <= xx & xx <= n + 1 by BB,aa,XXREAL_1:1;
hence thesis by aa,XXREAL_1:235;
end;
set f = id Z;
a3: dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2
.= Z \ {} by Counter0,N1
.= Z;
B1: lower_bound A = n by aa,XREAL_1:31,XXREAL_2:25;
B2: upper_bound A = n + 1 by aa,XREAL_1:31,XXREAL_2:29;
(id Z)^ | A is continuous by ContCut,A1,N1; then
integral ((id Z)^,A) = ln.(upper_bound A)-ln.(lower_bound A)
by A1,aa,TAYLOR_1:18,a3,INTEGRA9:61
.= ln.((n + 1) / n) by B1,B2,DIFF_4:4;
hence thesis by Diesel2;
end;
theorem
for n being non zero Nat holds
ln.(n + 1) < Harmonic n
proof
let n be non zero Nat;
set A = [.1, n+1.];
0 + 1 <= n + 1 by XREAL_1:31; then
reconsider A as non empty closed_interval Subset of REAL
by MEASURE5:def 3,XXREAL_1:1;
WA: A = [' 1, n + 1 '] by XREAL_1:31,INTEGRA5:def 3;
reconsider Z = right_open_halfline 0 as open Subset of REAL;
N1: not 0 in Z by XXREAL_1:4;
A1: A c= Z
proof
let x be object;
assume
a1: x in A; then
reconsider xx = x as Real;
1 <= xx & xx <= n + 1 by a1,XXREAL_1:1;
hence thesis by XXREAL_1:235;
end;
set f = id Z;
NN: dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2
.= Z \ {} by Counter0,N1
.= Z;
B1: lower_bound A = 1 by XREAL_1:31,XXREAL_2:25;
B2: upper_bound A = n + 1 by XREAL_1:31,XXREAL_2:29;
(id Z)^ | A is continuous by ContCut,A1,N1; then
KL: integral ((id Z)^,A) = ln.(upper_bound A) - ln.(lower_bound A)
by A1,TAYLOR_1:18,NN,INTEGRA9:61
.= ln.(n + 1) - (1 - 1) by ENTROPY1:2,B1,B2
.= ln.(n + 1);
set g = (id Z)^;
defpred P[Nat] means
integral (g,1,$1 + 1) < Harmonic $1;
reconsider AA = ['1,1+1'] as non empty closed_interval Subset of REAL;
AA = [.1,1+1.] by INTEGRA5:def 3; then
integral (g, AA) < 1 / 1 by Diesel3; then
I1: P[1] by Harm1,INTEGRA5:def 4;
I2: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume s0: P[k];
set a = 1, b = k + 1 + 1, c = k + 1;
W0: a <= b by XREAL_1:31;
Za: [. a,b .] c= ]. 0, +infty .[ by XXREAL_1:249; then
W3: [' a,b '] c= dom g by XREAL_1:31,INTEGRA5:def 3,NN;
set B = [' a, b '];
B c= Z by Za,INTEGRA5:def 3,XREAL_1:31; then
v1: ((id Z)^) | B is continuous by ContCut,N1; then
W2: g is_integrable_on [' a,b '] by INTEGRA5:11,W3;
W4: g | [' a,b '] is bounded by INTEGRA5:10,W3,v1;
a <= c & c <= b by XREAL_1:31; then
c in [. a,b .] by XXREAL_1:1; then
c in [' a,b '] by XREAL_1:31,INTEGRA5:def 3; then
W1: integral(g,a,b) = integral(g,a,c) + integral(g,c,b)
by W0,W2,W3,W4,INTEGRA6:17;
set AB = ['k+1, k+1+1'];
AB = [.k+1, k+1+1.] by INTEGRA5:def 3,NAT_1:11; then
integral (g,AB) < 1 / (k + 1) by Diesel3; then
integral (g,k + 1, k + 1 + 1) < 1 / (k + 1)
by NAT_1:11,INTEGRA5:def 4; then
integral (g,1,k + 1) + integral (g,k + 1, k + 1 + 1) <
Harmonic k + 1 / (k + 1) by s0,XREAL_1:8;
hence thesis by Harmon1,W1;
end;
KK: for n being non zero Nat holds P[n] from NAT_1:sch 10(I1,I2);
integral (g,1,n + 1) < Harmonic n by KK;
hence thesis by KL,INTEGRA5:def 4,WA,XREAL_1:31;
end;
theorem
for n1, n2 being Nat st n1 ^2 = n2 ^2 holds
n1 = n2
proof
let n1, n2 be Nat;
assume n1 ^2 = n2 ^2; then
n1 = sqrt (n2 ^2) by SQUARE_1:22;
hence thesis by SQUARE_1:22;
end;
registration let n be non trivial Nat;
cluster n ^2 -> non trivial;
coherence
proof
n >= 1 + 1 by NAT_2:29; then
A1: n > 1 by NAT_1:13; then
n ^2 > n by SQUARE_1:14;
hence thesis by NAT_2:28,A1;
end;
end;
::$N Telescoping series
theorem Telescoping:
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)
proof
let a,b,s be Real_Sequence;
assume that
Z1: (for n being Nat holds s.n = a.n + b.n) and
Z2: (for k being Nat holds b.k = -(a.(k+1)));
let n be Nat;
defpred P[Nat] means
(Partial_Sums s).$1 = (a.0) + (b.$1);
(Partial_Sums s).0 = s.0 by SERIES_1:def 1
.= (a.0) + (b.0) by Z1; then
A1: P[0];
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
(Partial_Sums s).(k+1) = (a.0) + (b.k) + s.(k + 1) by SERIES_1:def 1
.= (a.0) + (b.k) + (a.(k + 1) + b.(k + 1)) by Z1
.= (a.0) + (-a.(k+1)) + (a.(k + 1) + b.(k + 1)) by Z2
.= (a.0) + b.(k + 1);
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Impor3:
for f1, f2 being Real_Sequence,
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
let f1, f2 be Real_Sequence,
n be non trivial Nat;
assume
A1: for k being non trivial Nat st k <= n holds f1.k < f2.k;
defpred X[Nat] means
(for k being non trivial Nat st k <= $1 holds
f1.k < f2.k) implies
Partial_Sums(f1).$1 - Partial_Sums(f1).1 <
Partial_Sums(f2).$1 - Partial_Sums(f2).1;
Partial_Sums(f1).2 = Partial_Sums(f1).1 + f1.(1+1) &
Partial_Sums(f2).2 = Partial_Sums(f2).1 + f2.(1+1) by SERIES_1:def 1;
then
a1: X[2];
A2: for n being non trivial Nat st X[n] holds X[n+1]
proof
let n be non trivial Nat such that
A3: X[n];
assume
B1: for k being non trivial Nat st k <= n+1 holds f1.k < f2.k;
A4: f1.(n+1) < f2.(n+1) by B1;
ZZ: Partial_Sums(f1).(n+1) = Partial_Sums(f1).n + f1.(n+1) &
Partial_Sums(f2).(n+1) = Partial_Sums(f2).n + f2.(n+1)
by SERIES_1:def 1;
G1: n <= n + 1 by NAT_1:11;
for k being non trivial Nat st k <= n holds f1.k < f2.k
proof
let k be non trivial Nat;
assume k <= n; then
k <= n + 1 by G1,XXREAL_0:2;
hence thesis by B1;
end; then
f1.(n+1) + (Partial_Sums(f1).n - Partial_Sums(f1).1) <
f2.(n+1) + (Partial_Sums(f2).n - Partial_Sums(f2).1)
by A3,A4,XREAL_1:8;
hence thesis by ZZ;
end;
for n being non trivial Nat holds X[n] from NAT_2:sch 2(a1,A2);
hence thesis by A1;
end;
begin :: Some Special Sequences
definition
func Reci-seq1 -> Real_Sequence means :MyDef:
for n being Nat holds
it.n = 1 / (n ^2 - 1 / 4);
existence
proof
deffunc F(Nat) = 1 / ($1 ^2 - 1 / 4);
ex f being Real_Sequence st
for n being Nat holds f.n = F(n) from SEQ_1:sch 1;
hence thesis;
end;
uniqueness
proof
deffunc F(Nat) = 1 / ($1 ^2 - 1 / 4);
let f1,f2 be Real_Sequence such that
A1: f1.n = F(n) and
A2: f2.n = F(n);
let n be Element of NAT;
thus f1.n = F(n) by A1
.= f2.n by A2;
end;
end;
theorem Tele1:
for n being Nat holds
Reci-seq1.n = 1 / (n - 1 / 2) - 1 / (n + 1 / 2)
proof
let n be Nat;
set a = 1 / 2;
not 1 / 2 is Nat
proof
assume
A4: 1 / 2 is Nat;
0 <= 1 / 2 & 1 / 2 <= 0 + 1;
hence thesis by A4,NAT_1:9;
end; then
A2: n - a <> 0;
1 / (n - a) - 1 / (n + a)
= (1 * (n + a)) / ((n - a) * (n + a)) - 1 / (n + a) by XCMPLX_1:91
.= (1 * (n + a)) / ((n - a) * (n + a)) -
(1 * (n - a)) / ((n + a) * (n - a)) by A2,XCMPLX_1:91
.= ((n + a) - (n - a)) / ((n + a) * (n - a)) by XCMPLX_1:120
.= 1 / (n ^2 - 1 / 4);
hence thesis by MyDef;
end;
AlgDef:
for n being Nat,
a,b being Real holds
rseq (0,1,a,b).n = 1 / (a * n + b)
proof
let n be Nat, a,b be Real;
rseq(0,1,a,b).n = (0*n+1)/(a*n+b) by BASEL_1:5;
hence thesis;
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
let n be Nat;
A3: Reci-seq1.n = 1 / (n - 1 / 2) - 1 / (n + 1 / 2) by Tele1
.= 1 / (n - 1 / 2) + - 1 / (n + 1 / 2);
A1: ((rseq (0,1,1, -1/2))).n = 1 / (1 * n + - 1 / 2) by AlgDef;
(- rseq (0,1,1, 1 / 2)).n = -((rseq (0,1,1, 1 / 2)).n) by VALUED_1:8
.= - 1 / (1 * n + 1 / 2) by AlgDef;
hence thesis by A1,A3;
end;
theorem
Reci-seq1 = (rseq (0,1,1, -1/2)) + (- rseq (0,1,1, 1 / 2))
by SEQ_1:7,Tele2;
theorem
for n being Nat holds
(Partial_Sums Reci-seq1).n < -2
proof
let n be Nat;
set s = Reci-seq1;
set a = rseq (0,1,1, -1/2);
set b = -(rseq (0,1,1, 1/2));
ff: for k being Nat holds b.k = -(a.(k+1))
proof
let k be Nat;
b.k = - (((rseq (0,1,1, 1 / 2))).k) by VALUED_1:8
.= - 1 / (1 * k + 1 / 2) by AlgDef
.= - 1 / (1 * (k + 1) + - 1 / 2)
.= - (a.(k + 1)) by AlgDef;
hence thesis;
end;
w3: a.0 = 1 / (1 * 0 + - 1 / 2) by AlgDef
.= -2;
b.n = -(((rseq (0,1,1, 1/2))).n) by VALUED_1:8
.= - (1 / (1 * n + 1 / 2)) by AlgDef
.= - 1 / (n + 1 / 2); then
-2 + b.n < -2 + 0 by XREAL_1:8;
hence thesis by w3,ff,Telescoping,Tele2;
end;
theorem Seq3:
for n being Nat holds
Sum (Reci-seq1, n, 1) < 2 / 3
proof
let n be Nat;
set s = Reci-seq1;
set a = rseq (0,1,1, -1/2);
set b = -(rseq (0,1,1, 1/2));
ff: for k being Nat holds b.k = -(a.(k+1))
proof
let k be Nat;
b.k = - (((rseq (0,1,1, 1 / 2))).k) by VALUED_1:8
.= - 1 / (1 * k + 1 / 2) by AlgDef
.= - 1 / (1 * (k + 1) + - 1 / 2)
.= - (a.(k + 1)) by AlgDef;
hence thesis;
end;
W2: a.0 = 1 / (1 * 0 + - 1 / 2) by AlgDef
.= -2;
V1: a.1 = 1 / (1 * 1 + - 1 / 2) by AlgDef
.= 2;
V2: b.0 = -(((rseq (0,1,1, 1/2))).0) by VALUED_1:8
.= - (1 / (1 * 0 + 1 / 2)) by AlgDef
.= - 2;
V3: b.1 = -(((rseq (0,1,1, 1/2))).1) by VALUED_1:8
.= - (1 / (1 * 1 + 1 / 2)) by AlgDef
.= - 2 / 3;
s.0 = (a.0 + b.0) by Tele2; then
V4: s.0 + s.1 = (a.0 + b.0) + (a.1 + b.1) by Tele2
.= -2 + -2 / 3 by V1,V3,W2,V2;
V5: (Partial_Sums s).1 = (Partial_Sums s).0 + s.(0 + 1) by SERIES_1:def 1
.= -2 + -2 / 3 by V4,SERIES_1:def 1;
W1: b.n = -(((rseq (0,1,1, 1/2))).n) by VALUED_1:8
.= - (1 / (1 * n + 1 / 2)) by AlgDef
.= - 1 / (n + 1 / 2);
W3: (Partial_Sums s).n = -2 + b.n by W2,ff,Telescoping,Tele2;
b.n + 2 / 3 < 0 + 2 / 3 by XREAL_1:8,W1;
hence thesis by W3,V5;
end;
registration
cluster Basel-seq -> summable;
coherence
proof
for n being Nat st n >= 1 holds Basel-seq.n = 1 / n to_power 2
proof
let n be Nat;
assume n >= 1;
Basel-seq.n = 1 / (n ^2) by BASEL_1:31
.= 1 / (n to_power 2) by NEWTON:81;
hence thesis;
end;
hence thesis by SERIES_1:32;
end;
end;
theorem
for n being Nat holds
(Partial_Sums Reci-seq1).n = -2 + - 1 / (n + 1 / 2)
proof
let n be Nat;
set s = Reci-seq1;
set a = rseq (0,1,1, -1/2);
set b = -(rseq (0,1,1, 1/2));
ff: for k being Nat holds b.k = -(a.(k+1))
proof
let k be Nat;
b.k = - (((rseq (0,1,1, 1 / 2))).k) by VALUED_1:8
.= - 1 / (1 * k + 1 / 2) by AlgDef
.= - 1 / (1 * (k + 1) + - 1 / 2)
.= - (a.(k + 1)) by AlgDef;
hence thesis;
end;
W2: a.0 = 1 / (1 * 0 + - 1 / 2) by AlgDef
.= -2;
b.n = -(((rseq (0,1,1, 1/2))).n) by VALUED_1:8
.= - (1 / (1 * n + 1 / 2)) by AlgDef
.= - 1 / (n + 1 / 2);
hence thesis by W2,ff,Telescoping,Tele2;
end;
theorem Impor2:
for n being non trivial Nat holds
Sum (Basel-seq, n, 1) < Sum (Reci-seq1, n, 1)
proof
let n be non trivial Nat;
for k being non trivial Nat st k <= n holds Basel-seq.k < Reci-seq1.k
proof
let k be non trivial Nat;
assume k <= n;
Z1: Basel-seq.k = 1 / (k^2) by BASEL_1:31;
Z2: Reci-seq1.k = 1 / (k^2 - 1 / 4) by MyDef;
k >= 1 + 1 by NAT_2:29; then
k > 1 by NAT_1:13; then
k^2 > 1 ^2 by SQUARE_1:16; then
k^2 - 1 / 4 > 1 - 1 / 4 by XREAL_1:14; then
k^2 - 1 / 4 > 3 / 4;
hence thesis by Z1,Z2,XREAL_1:76,44;
end;
hence thesis by Impor3;
end;
theorem Important:
for n being non trivial Nat holds
Sum (Basel-seq, n) < 5 / 3
proof
let n be non trivial Nat;
Z2: Sum (Basel-seq, n)
= (Partial_Sums Basel-seq).(0 + 1) + ((Partial_Sums Basel-seq).n -
(Partial_Sums Basel-seq).1)
.= ((Partial_Sums Basel-seq).0 + Basel-seq.1) +
((Partial_Sums Basel-seq).n -
(Partial_Sums Basel-seq).1) by SERIES_1:def 1
.= Basel-seq.0 + Basel-seq.1 + ((Partial_Sums Basel-seq).n -
(Partial_Sums Basel-seq).1) by SERIES_1:def 1
.= 1 / (0 ^2) + Basel-seq.1 + Sum (Basel-seq, n, 1) by BASEL_1:31
.= 1 / 0 + 1 / (1 ^2) + Sum (Basel-seq, n, 1) by BASEL_1:31
.= 1 + Sum (Basel-seq, n, 1);
Z5: Sum (Basel-seq, n) < 1 + Sum (Reci-seq1, n, 1) by Z2,XREAL_1:8,Impor2;
1 + Sum (Reci-seq1, n, 1) < 1 + 2 / 3 by XREAL_1:8,Seq3;
hence thesis by Z5,XXREAL_0:2;
end;
theorem ::: Similar bound in BASEL series, counted independently
(Partial_Sums Basel-seq).n < 5 / 3
proof
per cases by NAT_2:28;
suppose n is non trivial; then
Sum (Basel-seq, n) < 5 / 3 by Important;
hence thesis;
end;
suppose n = 0; then
(Partial_Sums Basel-seq).n = Basel-seq.0 by SERIES_1:def 1
.= 1 / (0 ^2) by BASEL_1:31
.= 0;
hence thesis;
end;
suppose
F: n = 1;
(Partial_Sums Basel-seq).(0+1) = (Partial_Sums Basel-seq).0 + Basel-seq.1
by SERIES_1:def 1
.= Basel-seq.0 + Basel-seq.1 by SERIES_1:def 1
.= 1 / (0 ^2) + Basel-seq.1 by BASEL_1:31
.= 0 + Basel-seq.1
.= 0 + 1 / (1 ^2) by BASEL_1:31
.= 1;
hence thesis by F;
end;
end;
definition
func Reci-seq2 -> Real_Sequence means :My3Def:
for n being Nat holds
it.n = 1 + 1 / primenumber n;
existence
proof
deffunc F(Nat) = 1 + 1 / primenumber $1;
ex f being Real_Sequence st
for n being Nat holds f.n = F(n) from SEQ_1:sch 1;
hence thesis;
end;
uniqueness
proof
deffunc F(Nat) = 1 + 1 / primenumber $1;
let f1,f2 be Real_Sequence such that
A1: f1.n = F(n) and
A2: f2.n = F(n);
let n be Element of NAT;
thus f1.n = F(n) by A1
.= f2.n by A2;
end;
end; :: similar functor is in MOEBIUS2
theorem
Sum Sgm {1} = 1
proof
Sum <*1*> = 1;
hence thesis by FINSEQ_3:44;
end;
definition let n be Nat;
func SetPrimes n -> Subset of NAT equals
SetPrimes /\ Seg n;
coherence;
end;
registration let n be Nat;
cluster SetPrimes n -> finite;
coherence;
end;
theorem
for m, n being Nat st m <= n holds
SetPrimes m c= SetPrimes n by XBOOLE_1:26,FINSEQ_1:5;
theorem PrimesSet:
n+1 is not Prime implies SetPrimes (n+1) = SetPrimes n
proof
A1: SetPrimes (n+1) = SetPrimes /\ (Seg n \/ {n+1}) by FINSEQ_1:9
.= (SetPrimes n) \/ (SetPrimes /\ {n+1}) by XBOOLE_1:23;
assume n+1 is not Prime; then
not n+1 in SetPrimes by NEWTON:def 6; then
SetPrimes /\ {n+1} = {} by XBOOLE_0:def 7,ZFMISC_1:50;
hence SetPrimes (n+1) = SetPrimes n by A1;
end;
theorem SetPrime1:
SetPrimes 0 = {} & SetPrimes 1 = {}
proof
0+1 is not Prime by INT_2:def 4; then
SetPrimes (0+1) = SetPrimes 0 by PrimesSet;
hence thesis;
end;
theorem PrimesSet2:
n+1 is Prime implies SetPrimes (n+1) = SetPrimes n \/ {n+1}
proof
A1: SetPrimes (n+1) = SetPrimes /\ (Seg n \/ {n+1}) by FINSEQ_1:9
.= (SetPrimes n) \/ (SetPrimes /\ {n+1}) by XBOOLE_1:23;
assume n+1 is Prime; then
n+1 in SetPrimes by NEWTON:def 6;
hence thesis by A1,ZFMISC_1:46;
end;
theorem P1NotPrime:
for p being Prime st p > 2 holds
p+1 is not Prime
proof
let p be Prime;
assume
S1: p > 2; then
p+1 > 2+1 by XREAL_1:8; then
S3: p+1 > 2 by XXREAL_0:2;
p is odd by S1,PEPIN:17;
hence thesis by S3,PEPIN:17;
end;
theorem Set2:
SetPrimes 2 = {2}
proof
not 1 is Prime by INT_2:def 4; then
A1: not 1 in SetPrimes by NEWTON:def 6;
2 in SetPrimes by NEWTON:def 6,INT_2:28;
hence thesis by ZFMISC_1:54,A1,FINSEQ_1:2;
end;
theorem
not n+1 in SetPrimes n
proof
assume n+1 in SetPrimes n; then
n+1 in Seg n by XBOOLE_0:def 4; then
n+1 <= n by FINSEQ_1:1;
hence thesis by NAT_1:13;
end;
definition let n be Nat;
:: just to get an index for appropriate sequence of primes
func indexp n -> Nat equals
card SetPrimes n;
coherence;
end;
theorem Krzys1:
for n being Nat holds
indexp n <= n
proof
let n be Nat;
card SetPrimes n <= card Seg n by NAT_1:43,XBOOLE_1:17;
hence thesis;
end;
begin :: Squarefree and Square-containing Parts of a Natural Number
theorem
for n being non zero Nat holds
n = (TSqF n) * (n div TSqF n)
proof
let n be non zero Nat;
TSqF n divides n by MOEBIUS2:53; then
A2: n mod TSqF n = 0;
set i2 = TSqF n;
n = (n div i2) * i2 + (n mod i2) by INT_1:59
.= (n div i2) * i2 by A2;
hence thesis;
end;
theorem Skup: ::: MOEBIUS2:45 strenghtened
for n being non zero Nat holds (SqF n) |^ 2 divides n
proof
deffunc F(non zero Nat) = (Product SqFactors $1) |^ 2;
deffunc F1(non zero Nat) = Product SqFactors $1;
deffunc G(non zero Nat) = (SqFactors $1);
defpred P[Nat] means for n being non zero Nat st
support G(n) c= Seg $1 holds F(n) divides n;
let n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by MOEBIUS1:14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support G(n) by MOEBIUS2:def 3;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let n be non zero Nat such that
A5: support G(n) c= Seg (k+1);
A6: support pfexp n = support G(n) by MOEBIUS2:def 3;
per cases;
suppose
A7: not support G(n) c= Seg k;
set p = k+1;
set e = p |-count n;
set s = p |^ e;
A8: now
assume
A9: not k+1 in support G(n);
support G(n) c= Seg k
proof
let x be object;
assume
A10: x in support G(n);
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 thesis by A11,FINSEQ_1:1;
end;
hence contradiction by A7;
end; then
A12: p is Prime by A6,NAT_3:34; then
A13: p > 1 by INT_2:def 4; then
s divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = s * t;
reconsider s, t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product G(s) = Product f and
A16: f = (G(s)) * canFS(support G(s)) by NAT_3:def 5;
A17: dom G(s) = SetPrimes by PARTFUN1:def 2;
A18: support ppf s = support pfexp s by NAT_3:def 9; then
A19: support ppf s = support G(s) by MOEBIUS2:def 3;
(pfexp n).p = e by A12,NAT_3:def 8; then
e <> 0 by A6,A8,PRE_POLY:def 7; then
A21: support ppf s = {p} by A12,A18,NAT_3:42; then
A22: p in support pfexp s by A18,TARSKI:def 1;
A23: support G(t) c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A24: x in support G(t);
then reconsider m = x as Nat;
A25: x in support pfexp t by A24,MOEBIUS2:def 3;
A26: now
assume
A27: m = p;
(pfexp t).p = f by A12,NAT_3:def 8;
then f <> 0 by A25,A27,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A28: f = 1 + g by NAT_1:10;
p |^ f divides t by A13,NAT_3:def 7;
then consider u being Nat such that
A29: t = (p |^ f)*u;
n = s * (((p |^ g)*p)*u) by A14,A28,A29,NEWTON:6
.= s*p * ((p |^ g)*u)
.= (p |^ (e+1))*((p |^ g)*u) by NEWTON:6;
then p |^ (e+1) divides n;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support G(t) c= support G(n) by A6,MOEBIUS2:def 3;
then m in support G(n) by A24;
then m <= k+1 by A5,FINSEQ_1:1;
then m < p 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 thesis by A30,FINSEQ_1:1;
end; then
A31: F(t) divides t by A4;
support G(s) = {p} by A18,A21,MOEBIUS2:def 3;
then f = (G(s))*<*p*> by A16,FINSEQ_1:94
.= <* (G(s)).p *> by FINSEQ_2:34,A17,A8; then
h1: Product G(s) = (G(s)).p by A15,RVSUM_1:95
.= p |^ ((p |-count s) div 2) by A22,MOEBIUS2:def 3;
H2: p |-count s <= p |-count n by A12,NAT_3:25,INT_2:def 4;
set j = p |-count s;
j = 2 * (j div 2) + (j mod 2) by NAT_D:2; then
Sb: 2 * (j div 2) <= j by NAT_1:11;
(p |^ ((p |-count s) div 2)) |^ 2 =
p |^ (((p |-count s) div 2) * 2) by NEWTON:9; then
ZZ: (p |^ ((p |-count s) div 2)) |^ 2 divides p |^ e
by Sb,NEWTON:89,H2,XXREAL_0:2;
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 G(t) by MOEBIUS2:def 3;
A34: now
assume (support ppf s) meets (support ppf t);
then consider x being object 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 G(t) by MOEBIUS2:def 3;
x = p by A21,A35,TARSKI:def 1;
then p <= k by A23,A37,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A38: u divides t1 by NAT_D:def 5;
A39: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
then u > 1 by A39,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider r being Element of NAT such that
A40: r is prime and
A41: r divides u by INT_2:31;
u divides s1 by NAT_D:def 5;
then r divides s1 by A41,NAT_D:4;
then r = 1 or r = p by A12,INT_2:def 4,A40,NAT_3:5;
then p in support pfexp t
by NAT_3:37,A40,A41,A38,NAT_D:4;
then p in support G(t) by MOEBIUS2:def 3;
then k+1 <= k by A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then F(n) = (Product (G(s)+G(t))) |^ 2 by A14,MOEBIUS2:44
.= (F1(s) * F1(t)) |^ 2 by A34,A19,A33,NAT_3:19
.= F(s) * F(t) by NEWTON:7;
hence thesis by A14,h1,ZZ,A31,NAT_3:1;
end;
suppose
support G(n) c= Seg k;
hence thesis by A4;
end;
end;
A42: P[0]
proof
let n be non zero Nat;
assume support G(n) c= Seg 0;
then support G(n) = {};
then G(n) = EmptyBag SetPrimes by PRE_POLY:81;
then F(n) = 1 |^ 2 by NAT_3:20 .= 1;
hence thesis by NAT_D:6;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A42,A3);
hence thesis by A1,A2;
end;
theorem KeyValue:
for m being finite-support natural-valued ManySortedSet of SetPrimes,
p being Prime st support m = {p} holds
Product m = m.p
proof
let m be finite-support natural-valued ManySortedSet of SetPrimes,
p be Prime;
assume
A1: support m = {p};
consider f being FinSequence of COMPLEX such that
A15: Product m = Product f and
A16: f = m * canFS (support m) by NAT_3:def 5;
Z1: m * <*p*> = <*m.p*>
proof
D1: rng <*p*> = {p} by FINSEQ_1:39;
d2: p in SetPrimes by NEWTON:def 6;
dom m = SetPrimes by PARTFUN1:def 2; then
B1: dom (m * <*p*>) = dom <*p*> by D1,d2,RELAT_1:27,ZFMISC_1:31
.= Seg 1 by FINSEQ_1:38;
B2: dom (m * <*p*>) = dom <*m.p*> by B1,FINSEQ_1:38;
for x being object st x in dom (m * <*p*>) holds
(m * <*p*>).x = (<*m.p*>).x
proof
let x be object;
assume
C1: x in dom (m * <*p*>); then
C2: x = 1 by B1,TARSKI:def 1,FINSEQ_1:2; then
(m * <*p*>).x = m.(<*p*>.1) by FUNCT_1:12,C1
.= (<*m.p*>).x by C2;
hence thesis;
end;
hence thesis by B2,FUNCT_1:2;
end;
f = <*m.p*> by Z1,FINSEQ_1:94,A16,A1;
hence thesis by RVSUM_1:95,A15;
end;
theorem Cosik:
for n being non zero Nat holds (SqF n) |^ 2 = TSqF n
proof
deffunc F(non zero Nat) = (Product SqFactors $1) |^ 2;
deffunc F1(non zero Nat) = Product SqFactors $1;
deffunc G(non zero Nat) = SqFactors $1;
deffunc H(non zero Nat) = Product TSqFactors $1;
defpred P[Nat] means for n being non zero Nat st
support G(n) c= Seg $1 holds F(n) = H(n);
let n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by MOEBIUS1:14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support G(n) by MOEBIUS2:def 3;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let n be non zero Nat such that
A5: support G(n) c= Seg (k+1);
A6: support pfexp n = support G(n) by MOEBIUS2:def 3;
per cases;
suppose
A7: not support G(n) c= Seg k;
set p = k+1;
set e = p |-count n;
set s = p |^ e;
A8: now
assume
A9: not k+1 in support G(n);
support G(n) c= Seg k
proof
let x be object;
assume
A10: x in support G(n);
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 thesis by A11,FINSEQ_1:1;
end;
hence contradiction by A7;
end; then
A12: p is Prime by A6,NAT_3:34; then
A13: p > 1 by INT_2:def 4; then
s divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = s * t;
reconsider s, t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product G(s) = Product f and
A16: f = (G(s)) * canFS(support G(s)) by NAT_3:def 5;
A17: dom G(s) = SetPrimes by PARTFUN1:def 2;
A18: support ppf s = support pfexp s by NAT_3:def 9; then
A19: support ppf s = support G(s) by MOEBIUS2:def 3;
(pfexp n).p = e by A12,NAT_3:def 8; then
e <> 0 by A6,A8,PRE_POLY:def 7; then
A21: support ppf s = {p} by A12,A18,NAT_3:42; then
A22: p in support pfexp s by A18,TARSKI:def 1;
A23: support G(t) c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A24: x in support G(t);
then reconsider m = x as Nat;
A25: x in support pfexp t by A24,MOEBIUS2:def 3;
A26: now
assume
A27: m = p;
(pfexp t).p = f by A12,NAT_3:def 8;
then f <> 0 by A25,A27,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A28: f = 1 + g by NAT_1:10;
p |^ f divides t by A13,NAT_3:def 7;
then consider u being Nat such that
A29: t = (p |^ f)*u;
n = s * (((p |^ g)*p)*u) by A14,A28,A29,NEWTON:6
.= s*p * ((p |^ g)*u)
.= (p |^ (e+1))*((p |^ g)*u) by NEWTON:6;
then p |^ (e+1) divides n;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support G(t) c= support G(n) by A6,MOEBIUS2:def 3;
then m in support G(n) by A24;
then m <= k+1 by A5,FINSEQ_1:1;
then m < p 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 thesis by A30,FINSEQ_1:1;
end; then
A31: F(t) = H(t) by A4;
a21: support G(s) = {p} by A18,A21,MOEBIUS2:def 3;
Aa1: support TSqFactors s = {p} by A18,A21,MOEBIUS2:def 8;
f = (G(s))*<*p*> by A16,FINSEQ_1:94,a21
.= <* (G(s)).p *> by FINSEQ_2:34,A17,A8; then
Product G(s) = (G(s)).p by A15,RVSUM_1:95
.= p |^ ((p |-count s) div 2) by A22,MOEBIUS2:def 3; then
aa1: (Product G(s)) |^ 2 = p |^ (2 * ((p |-count s) div 2)) by NEWTON:9
.= (TSqFactors s).p by A22,MOEBIUS2:def 8
.= Product TSqFactors s by A12,KeyValue,Aa1;
set j = p |-count s;
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 G(t) by MOEBIUS2:def 3;
A34: now
assume (support ppf s) meets (support ppf t);
then consider x being object 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 G(t) by MOEBIUS2:def 3;
x = p by A21,A35,TARSKI:def 1;
then p <= k by A23,A37,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
ZZ: s1,t1 are_coprime
proof
set u = s1 gcd t1;
A38: u divides t1 by NAT_D:def 5;
A39: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
then u > 1 by A39,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider r being Element of NAT such that
A40: r is prime and
A41: r divides u by INT_2:31;
u divides s1 by NAT_D:def 5;
then r divides s1 by A41,NAT_D:4;
then r = 1 or r = p by A12,INT_2:def 4,A40,NAT_3:5;
then p in support pfexp t
by NAT_3:37,A40,A41,A38,NAT_D:4;
then p in support G(t) by MOEBIUS2:def 3;
then k+1 <= k by A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
support TSqFactors s = support pfexp s &
support TSqFactors t = support pfexp t by MOEBIUS2:def 8; then
za: support TSqFactors s = support ppf s &
support TSqFactors t = support ppf t by NAT_3:def 9;
F(n) = (Product (G(s)+G(t))) |^ 2 by A14,MOEBIUS2:44,ZZ
.= (F1(s) * F1(t)) |^ 2 by A34,A19,A33,NAT_3:19
.= (F1(s)) |^ 2 * (F1(t) |^ 2) by NEWTON:7
.= Product (TSqFactors s + TSqFactors t) by za,NAT_3:19,aa1,A31,A34
.= H(n) by A14,ZZ,MOEBIUS2:52;
hence thesis;
end;
suppose
support G(n) c= Seg k;
hence thesis by A4;
end;
end;
A42: P[0]
proof
let n be non zero Nat;
assume support G(n) c= Seg 0; then
J1: support G(n) = {};
then G(n) = EmptyBag SetPrimes by PRE_POLY:81;
then
BB: F(n) = 1 |^ 2 by NAT_3:20 .= 1;
support TSqFactors n = support pfexp n by MOEBIUS2:def 8
.= support G(n) by MOEBIUS2:def 3; then
TSqFactors n = EmptyBag SetPrimes by PRE_POLY:81,J1;
hence thesis by BB,NAT_3:20;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A42,A3);
hence thesis by A1,A2;
end;
registration
let n be non zero Nat;
cluster n div ((SqF n) |^ 2) -> square-free for Nat;
coherence
proof
set TS = (SqF n) |^ 2;
TS = TSqF n by Cosik;
hence thesis;
end;
end;
::: TSqF n should be revised to allow zero for an argument
definition let n be non zero Nat;
func SquarefreePart n -> non zero Nat equals
n div TSqF n;
coherence
proof
(SqF n) |^ 2 divides n by Skup; then
TSqF n divides n by Cosik; then
n = (TSqF n) * (n div TSqF n);
hence thesis;
end;
end;
registration let n be non zero Nat;
cluster SquarefreePart n -> square-free;
coherence;
end;
theorem Canonical: ::: squarefree-decompose
for n being non zero Nat holds
n = (SquarefreePart n) * (SqF n) ^2
proof
let n be non zero Nat;
(SqF n) |^ 2 divides n by Skup; then
TSqF n divides n by Cosik; then
n = (TSqF n) * (n div TSqF n)
.= ((SqF n) |^2) * (n div TSqF n) by Cosik
.= ((SqF n) ^2) * (n div TSqF n) by NEWTON:81;
hence thesis;
end;
theorem
for n being non zero Nat holds
support pfexp n c= Seg n
proof
let n be non zero Nat;
let x be object;
assume
A1: x in support pfexp n; then
reconsider k = x as Prime by NAT_3:34;
A3: 1 < k by INT_2:def 4;
k <= n by NAT_D:7,A1,NAT_3:36;
hence thesis by FINSEQ_1:1,A3;
end;
theorem ::: a kind of generalized MOEBIUS1:14
for n being non zero Nat holds
support ppf n c= Seg n
proof
let n be non zero Nat;
let x be object;
assume x in support ppf n; then
A1: x in support pfexp n by NAT_3:def 9; then
reconsider k = x as Prime by NAT_3:34;
A3: 1 < k by INT_2:def 4;
k <= n by NAT_D:7,A1,NAT_3:36;
hence thesis by FINSEQ_1:1,A3;
end;
theorem
for n being non zero Nat holds
Seg SquarefreePart n c= Seg n
proof
let n be non zero Nat;
n = (SquarefreePart n) * ((SqF n) ^2) by Canonical; then
SquarefreePart n divides n; then
SquarefreePart n <= n by NAT_D:7;
hence thesis by FINSEQ_1:5;
end;
Surprise:
for n,m being non zero Nat st m^2 divides SquarefreePart n holds
m = 1
proof
let n,m be non zero Nat;
assume
A0: m^2 divides SquarefreePart n;
assume m <> 1; then
consider p being Prime such that
A1: p divides m by MOEBIUS1:5;
p^2 divides m^2 by A1,PYTHTRIP:6; then
p ^2 divides SquarefreePart n by A0,NAT_D:4; then
p |^2 divides SquarefreePart n by NEWTON:81; then
1 + 1 <= p |-count SquarefreePart n by MOEBIUS2:40;
hence thesis by MOEBIUS1:24,NAT_1:13;
end;
theorem
for k,n being non zero Nat holds
k^2 divides SquarefreePart n iff k = 1 by Surprise,NAT_D:6;
theorem
for m,n being non zero Nat st
SquarefreePart n = SquarefreePart m &
TSqF m = TSqF n holds
m = n
proof
let m,n be non zero Nat;
assume
A1: SquarefreePart n = SquarefreePart m &
TSqF m = TSqF n;
m = (SquarefreePart m) * (SqF m) ^2 by Canonical
.= (SquarefreePart m) * ((SqF m) |^2) by NEWTON:81
.= (SquarefreePart n) * TSqF n by A1,Cosik
.= (SquarefreePart n) * (SqF n) |^2 by Cosik
.= (SquarefreePart n) * (SqF n) ^2 by NEWTON:81
.= n by Canonical;
hence thesis;
end;
begin :: Generating Bags from Subsets of Prime Numbers
definition let A be finite Subset of SetPrimes;
func A-bag -> bag of SetPrimes equals
(EmptyBag SetPrimes) +* (id A);
coherence
proof
set f = (EmptyBag SetPrimes) +* (id A);
dom f = (dom EmptyBag SetPrimes) \/ dom id A by FUNCT_4:def 1
.= SetPrimes \/ dom id A by PARTFUN1:def 2
.= SetPrimes by XBOOLE_1:12; then
reconsider f as ManySortedSet of SetPrimes
by PARTFUN1:def 2,RELAT_1:def 18;
support f c= A
proof
let x be object;
assume
a10: x in support f;
x in A
proof
assume not x in A; then
not x in dom id A; then
f.x = (EmptyBag SetPrimes).x by FUNCT_4:11
.= 0 by PBOOLE:5;
hence thesis by a10,PRE_POLY:def 7;
end;
hence thesis;
end;
hence thesis by PRE_POLY:def 8;
end;
end;
theorem BagSupport:
for A being finite Subset of SetPrimes holds
support (A-bag) = A
proof
let A being finite Subset of SetPrimes;
set f = A-bag;
B1: support f c= A
proof
let x be object;
assume
a10: x in support f;
x in A
proof
assume not x in A; then
not x in dom id A; then
f.x = (EmptyBag SetPrimes).x by FUNCT_4:11
.= 0 by PBOOLE:5;
hence thesis by a10,PRE_POLY:def 7;
end;
hence thesis;
end;
A c= support f
proof
let x be object;
assume
E1: x in A; then
x in dom id A; then
f.x = (id A).x by FUNCT_4:13
.= x by E1,FUNCT_1:17; then
f.x is Prime by NEWTON:def 6,E1;
hence thesis by PRE_POLY:def 7;
end;
hence thesis by B1,XBOOLE_0:def 10;
end;
theorem
for A being finite Subset of SetPrimes st A = {} holds
A-bag = EmptyBag SetPrimes
proof
let A be finite Subset of SetPrimes;
assume A = {}; then
support (A-bag) = {} by BagSupport;
hence thesis by PRE_POLY:81;
end;
theorem BagValue:
for A being finite Subset of SetPrimes
for i being object st i in support (A-bag) holds
(A-bag).i = i
proof
let A be finite Subset of SetPrimes;
let i be object;
assume aa: i in support (A-bag); then
A2: i in A by BagSupport;
A1: i in dom id A by aa,BagSupport;
(A-bag).i = (id A).i by A1,FUNCT_4:13
.= i by A2,FUNCT_1:17;
hence thesis;
end;
theorem
for A,B be finite Subset of SetPrimes st
A-bag = B-bag holds
A = B
proof
let A,B be finite Subset of SetPrimes;
assume A-bag = B-bag; then
A = support (B-bag) by BagSupport;
hence thesis by BagSupport;
end;
registration let A be finite Subset of SetPrimes;
cluster A-bag -> prime-factorization-like;
coherence
proof
for x being Prime st x in support (A-bag)
ex n be Nat st 0 < n & (A-bag).x = x |^n
proof
let x be Prime;
assume x in support (A-bag); then
(A-bag).x = x |^1 by BagValue;
hence thesis;
end;
hence thesis by INT_7:def 1;
end;
end;
ProdSqF:
for A being finite Subset of SetPrimes holds
Product (A-bag) is square-free
proof
let A be finite Subset of SetPrimes;
set n = Product (A-bag);
reconsider n as non zero Nat by MOEBIUS2:26;
C2: Product (A-bag) = Product ppf n by NAT_3:61;
ZW: ppf n = A-bag by INT_7:15,C2;
not ex p being Prime st p |^ 2 divides n
proof
given p1 being Prime such that
K1: p1 |^ 2 divides n;
K2: p1 |-count (p1 |^ 2) <= p1 |-count n by NAT_3:30,K1;
set m = p1 |-count n;
W2: m >= 2 by K2,NAT_3:25,INT_2:def 4;
(p1 |^ 1) divides (p1 |^ 2) by NEWTON:89; then
V1: p1 in support pfexp n by NAT_3:37,K1,NAT_D:4; then
W1: (ppf n).p1 = p1 |^ m by NAT_3:def 9;
p1 in support ppf n by V1,NAT_3:def 9; then
p1 = p1 |^ m by W1,BagValue,ZW;
hence thesis by PREPOWER:13,W2,INT_2:def 4;
end;
hence thesis by MOEBIUS1:def 1;
end;
registration let A be finite Subset of SetPrimes;
cluster Product (A-bag) -> square-free for Nat;
coherence by ProdSqF;
end;
theorem
for n being non zero Nat
for x being object st x in bool SetPrimes n holds
x is finite Subset of SetPrimes
proof
let n be non zero Nat;
let x be object;
assume G1: x in bool SetPrimes n;
reconsider g1 = x as Subset of SetPrimes n by G1;
SetPrimes n c= SetPrimes by XBOOLE_1:17; then
g1 c= SetPrimes;
hence thesis;
end;
theorem
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
proof
let n be non zero Nat;
let x be object;
assume G1: x in [:bool SetPrimes n, Seg n:];
x is pair by CARDFIL4:4,G1; then
x = [x`1,x`2]; then
reconsider g1 = x`1 as Subset of SetPrimes n by G1,ZFMISC_1:87;
SetPrimes n c= SetPrimes by XBOOLE_1:17; then
g1 c= SetPrimes;
hence thesis;
end;
:: Later we should show the connection between sum and products of
:: sequences with exponential function, respectively.
theorem
rseq(0,1,1,0) = invNAT
proof
for n being Element of NAT holds
rseq(0,1,1,0).n = invNAT.n
proof
let n be Element of NAT;
rseq(0,1,1,0).n = 1 / (1 * n + 0) by AlgDef
.= invNAT.n by MOEBIUS2:def 2;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
indexp 0 = 0;
theorem GreaterProduct:
for n being Nat holds
(Partial_Product Reci-seq2).n > 0
proof
let n be Nat;
for k being Nat holds Reci-seq2.k > 0
proof
let k be Nat;
Reci-seq2.k = 1 + 1 / primenumber k by My3Def;
hence thesis;
end;
hence thesis by SERIES_3:43;
end;
theorem Crucial5X:
for n being Nat holds
ln.((Partial_Product Reci-seq2).n) <= (Partial_Sums ReciPrime).n
proof
let n be Nat;
defpred P[Nat] means
ln.((Partial_Product Reci-seq2).$1) <=
((Partial_Sums ReciPrime).$1);
B1: (Partial_Product Reci-seq2).0 = Reci-seq2.0 by SERIES_3:def 1
.= 1 + 1 / 2 by MOEBIUS2:8,My3Def;
(Partial_Sums ReciPrime).0 = ReciPrime.0 by SERIES_1:def 1
.= 1 / 2 by MOEBIUS2:8,MOEBIUS2:def 1; then
A1: P[0] by B1,Diesel1;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
B1: P[k];
C1: (Partial_Product Reci-seq2).k > 0 by GreaterProduct;
C2: Reci-seq2.(k+1) > 0
proof
Reci-seq2.(k+1) = 1 + 1 / primenumber (k+1) by My3Def;
hence thesis;
end;
(Partial_Product Reci-seq2).(k+1) =
(Partial_Product Reci-seq2).k * (Reci-seq2.(k+1))
by SERIES_3:def 1; then
ln.((Partial_Product Reci-seq2).(k+1)) =
ln.((Partial_Product Reci-seq2).k) + ln.((Reci-seq2.(k+1)))
by LogAdd,C1,C2; then
D5: ln.((Partial_Product Reci-seq2).(k+1)) <=
((Partial_Sums ReciPrime).k) + ln.((Reci-seq2.(k+1))) by XREAL_1:7,B1;
D3: (Partial_Sums ReciPrime).(k+1) =
(Partial_Sums ReciPrime).k + (ReciPrime.(k+1)) by SERIES_1:def 1;
ln.((Reci-seq2.(k+1))) < ReciPrime.(k+1)
proof
D1: Reci-seq2.(k+1) = 1 + 1 / primenumber (k+1) by My3Def;
ReciPrime.(k+1) = 1 / primenumber (k+1) by MOEBIUS2:def 1;
hence thesis by D1,Diesel1;
end; then
((Partial_Sums ReciPrime).k) + ln.((Reci-seq2.(k+1))) <
((Partial_Sums ReciPrime).k) + ReciPrime.(k+1) by XREAL_1:8;
hence thesis by D5,XXREAL_0:2,D3;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
for n being Nat holds
ln.((Partial_Product Reci-seq2).(indexp n)) <= (Partial_Sums ReciPrime).n
proof
let n be Nat;
A1: ln.((Partial_Product Reci-seq2).(indexp n)) <=
(Partial_Sums ReciPrime).(indexp n) by Crucial5X;
for i being Nat holds ReciPrime.i >= 0
proof
let i be Nat;
ReciPrime.i = 1 / primenumber i by MOEBIUS2:def 1;
hence thesis;
end; then
(Partial_Sums ReciPrime).(indexp n) <=
(Partial_Sums ReciPrime).n by Krzys1,CATALAN2:52;
hence thesis by A1,XXREAL_0:2;
end;
definition
func Reci-Sqf-> Real_Sequence means :MySumDef:
it.0 = 0 &
for i being non zero Nat holds it.i = 1 / SquarefreePart i;
existence
proof
deffunc G(Nat,object) = In (1 / SquarefreePart ($1 + 1), REAL);
deffunc A() = In(0,REAL);
consider f be sequence of REAL such that
A1: f.0 = A() &
for n be Nat holds f.(n+1) = G(n,f.n) from NAT_1:sch 12;
reconsider f as Real_Sequence;
take f;
thus f.0 = 0 by A1;
let n be non zero Nat;
consider k be Nat such that
A2: k + 1 = n by NAT_1:6;
f.(k+1) = G(k,f.k) by A1
.= 1/SquarefreePart (k + 1);
hence thesis by A2;
end;
uniqueness
proof
let f1, f2 be Real_Sequence such that
A1: f1.0 = 0 &
for i being non zero Nat holds f1.i = 1 / SquarefreePart i and
A2: f2.0 = 0 &
for i being non zero Nat holds f2.i = 1 / SquarefreePart i;
for n being Element of NAT holds f1.n = f2.n
proof
let n be Element of NAT;
per cases;
suppose n = 0;
hence thesis by A2,A1;
end;
suppose n <> 0; then
reconsider nn = n as non zero Nat;
f1.nn = 1 / SquarefreePart nn by A1 .= f2.nn by A2;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
func Reci-TSq -> Real_Sequence means :MySum2Def:
it.0 = 0 &
for i being non zero Nat holds it.i = 1 / TSqF i;
existence
proof
deffunc G(Nat,object) = In (1 / TSqF ($1 + 1),REAL);
deffunc A() = In(0,REAL);
consider f be sequence of REAL such that
A1: f.0 = A() &
for n be Nat holds f.(n+1) = G(n,f.n) from NAT_1:sch 12;
reconsider f as Real_Sequence;
take f;
thus f.0 = 0 by A1;
let n be non zero Nat;
consider k be Nat such that
A2: k + 1 = n by NAT_1:6;
f.(k+1) = G(k,f.k) by A1
.= 1 / TSqF (k + 1);
hence thesis by A2;
end;
uniqueness
proof
let f1, f2 be Real_Sequence such that
A1: f1.0 = 0 &
for i being non zero Nat holds f1.i = 1 / TSqF i and
A2: f2.0 = 0 &
for i being non zero Nat holds f2.i = 1 / TSqF i;
for n being Element of NAT holds f1.n = f2.n
proof
let n be Element of NAT;
per cases;
suppose n = 0;
hence thesis by A2,A1;
end;
suppose n <> 0; then
reconsider nn = n as non zero Nat;
f1.nn = 1 / TSqF nn by A1 .= f2.nn by A2;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Core1:
rseq (0,1,1,0) = Reci-Sqf (#) Reci-TSq
proof
for n being Nat holds
(rseq (0,1,1,0)).n = (Reci-Sqf.n) * (Reci-TSq.n)
proof
let n be Nat;
A1: (rseq (0,1,1,0)).n = 1 / (1 * n + 0) by AlgDef;
per cases;
suppose
A2: n = 0; then
(rseq (0,1,1,0)).n = 1 / (1 * 0 + 0) by AlgDef
.= (Reci-Sqf.n) * 0
.= (Reci-Sqf.n) * (Reci-TSq.n) by MySum2Def,A2;
hence thesis;
end;
suppose n <> 0; then
reconsider nn = n as non zero Nat;
A3: TSqF nn = (SqF nn) |^2 by Cosik
.= (SqF nn)^2 by NEWTON:81;
A4: Reci-TSq.nn = 1 / TSqF nn by MySum2Def;
1 / nn = 1 / ((SquarefreePart nn) * (TSqF nn)) by Canonical,A3
.= (1 / (SquarefreePart nn)) * (1 / (TSqF nn)) by XCMPLX_1:102;
hence thesis by MySumDef,A1,A4;
end;
end;
hence thesis by SEQ_1:8;
end;
reserve s, s1, s2 for Real_Sequence;
theorem Seqs1:
for n being Nat holds Reci-Sqf.n >= 0
proof
let n be Nat;
per cases;
suppose n = 0;
hence thesis by MySumDef;
end;
suppose n <> 0; then
reconsider nn = n as non zero Nat;
Reci-Sqf.n = 1 / SquarefreePart nn by MySumDef;
hence thesis;
end;
end;
theorem Seqs4:
for n being Nat holds Reci-TSq.n >= 0
proof
let n be Nat;
per cases;
suppose n = 0;
hence thesis by MySum2Def;
end;
suppose n <> 0; then
reconsider nn = n as non zero Nat;
Reci-TSq.n = 1 / TSqF nn by MySum2Def;
hence thesis;
end;
end;
theorem
for n being Nat holds Basel-seq.n >= 0
proof
let n be Nat;
Basel-seq.n = 1 / (n ^2) by BASEL_1:31;
hence thesis;
end;
theorem :::Seqs5:
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;
func Compose n -> Function of [:bool SetPrimes n, Seg n:], NAT means
for x being Element of [:bool SetPrimes n, Seg n:],
A being finite Subset of SetPrimes,
k being Nat st x = [A, k] holds
it.x = (Product ((A,1)-bag)) * k ^2;
existence
proof
defpred P[object,object,object] means
for A being finite Subset of SetPrimes, k being Nat st
A = $1 & k = $2 holds
$3 = Product ((A,1)-bag) * k ^2;
A1: for x,y,z1,z2 being object st
x in bool SetPrimes n & y in Seg n & P[x,y,z1] & P[x,y,z2]
holds z1 = z2
proof
let x,y,z1,z2 be object;
assume
a1: x in bool SetPrimes n & y in Seg n & P[x,y,z1] & P[x,y,z2]; then
reconsider xa = x as Subset of SetPrimes n;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
xa c= SetPrimes by a4; then
reconsider S = xa as finite Subset of SetPrimes;
set xx = (S,1)-bag;
reconsider yy = y as Nat by a1;
z1 = Product xx * yy ^2 by a1;
hence thesis by a1;
end;
A2: for x,y being object st x in bool SetPrimes n & y in Seg n
ex z being object st P[x,y,z]
proof
let x,y be object;
assume
a1: x in bool SetPrimes n & y in Seg n;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
reconsider xx = x as Subset of SetPrimes n by a1;
xx c= SetPrimes by a4; then
reconsider xx = x as finite Subset of SetPrimes;
reconsider yy = y as Nat by a1;
ex z being object st P[x,y,z]
proof
take Product ((xx,1)-bag) * yy ^2;
thus thesis;
end;
hence thesis;
end;
ex f being Function st dom f = [:bool SetPrimes n,Seg n:] &
for x,y being object st x in bool SetPrimes n & y in Seg n
holds P[x,y,f.(x,y)] from FUNCT_3:sch 1(A1,A2); then
consider f being Function such that
D1: dom f = [:bool SetPrimes n, Seg n:] &
for x,y being object st x in bool SetPrimes n & y in Seg n
holds P[x,y,f.(x,y)];
rng f c= NAT
proof
let g be object;
assume g in rng f; then
consider gg being object such that
E1: gg in dom f & g = f.gg by FUNCT_1:def 3;
G0: gg is pair by CARDFIL4:4,E1,D1; then
G3: gg = [gg`1,gg`2]; then
Z1: gg`1 in bool SetPrimes n by E1,D1,ZFMISC_1:87;
reconsider g1 = gg`1 as Subset of SetPrimes n by G3,E1,D1,ZFMISC_1:87;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
g1 c= SetPrimes by a4; then
reconsider g1 = gg`1 as finite Subset of SetPrimes;
Z2: gg`2 in Seg n by E1,D1,G3,ZFMISC_1:87; then
reconsider yy = gg`2 as Nat;
f.(g1,yy) = (Product ((g1,1)-bag)) * yy ^2 by Z1,D1,Z2;
hence thesis by E1,G0;
end; then
reconsider f as Function of [:bool SetPrimes n,Seg n:], NAT
by D1,FUNCT_2:2;
take f;
let x be Element of [:bool SetPrimes n, Seg n:],
A be finite Subset of SetPrimes,
k be Nat;
assume
D2: x = [A, k]; then
D3: A in bool SetPrimes n by ZFMISC_1:87;
k in Seg n by D2,ZFMISC_1:87; then
P[A,k,f.(A,k)] by D3,D1;
hence thesis by D2;
end;
uniqueness
proof
let f1, f2 be Function of [:bool SetPrimes n, Seg n:], NAT;
assume that
A1: for x being Element of [:bool SetPrimes n, Seg n:],
A being finite Subset of SetPrimes,
k being Nat st x = [A, k] holds
f1.x = (Product ((A,1)-bag)) * k ^2 and
A2: for x being Element of [:bool SetPrimes n, Seg n:],
A being finite Subset of SetPrimes,
k being Nat st x = [A, k] holds
f2.x = (Product ((A,1)-bag)) * k ^2;
for x being object st x in [:bool SetPrimes n, Seg n:]
holds f1.x = f2.x
proof
let x be object;
assume
G1: x in [:bool SetPrimes n, Seg n:]; then
G0: x is pair by CARDFIL4:4; then
G3: x = [x`1,x`2]; then
reconsider xx = x`1 as Subset of SetPrimes n by G1,ZFMISC_1:87;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
xx c= SetPrimes by a4; then
reconsider xx = x`1 as finite Subset of SetPrimes;
x`2 in Seg n by G1,G3,ZFMISC_1:87; then
reconsider yy = x`2 as Nat;
G2: x = [xx,yy] by G0; then
f1.x = (Product ((xx,1)-bag)) * yy ^2 by G1,A1 .= f2.x by A2,G1,G2;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem
(Partial_Sums Basel-seq).n >= 0
proof
for n being Nat holds Basel-seq.n >= 0
proof
let n be Nat;
Basel-seq.n = 1 / (n^2) by BASEL_1:31;
hence thesis;
end;
hence thesis by SERIES_3:34;
end;
begin :: On Reciprocals of Products of Prime Numbers
definition let n be Nat;
func ReciProducts n -> Subset of REAL equals
the set of all 1 / Product Sgm X where X is Subset of SetPrimes n;
coherence
proof
set Y = the set of all 1 / Product Sgm X where X is Subset of SetPrimes n;
Y c= REAL
proof
let x be object;
assume x in Y; then
consider X being Subset of SetPrimes n such that
A1: x = 1 / Product Sgm X;
thus thesis by A1,XREAL_0:def 1;
end;
hence thesis;
end;
end;
registration let n be Nat;
cluster ReciProducts n -> finite;
correctness
proof
set Y = ReciProducts n;
deffunc F(Subset of SetPrimes n) = 1 / Product Sgm $1;
A3: Y c= { F(X) where X is Element of bool SetPrimes n :
X in bool SetPrimes n }
proof
let x be object;
assume x in Y; then
consider X being Subset of SetPrimes n such that
B1: x = 1 / Product Sgm X;
thus thesis by B1;
end;
A1: bool SetPrimes n is finite;
{ F(w) where w is Element of bool SetPrimes n:
w in bool SetPrimes n } is finite from FRAENKEL:sch 21(A1);
hence thesis by A3;
end;
end;
theorem
ReciProducts 0 = { 1 }
proof
the set of all 1 / Product Sgm X where X is Subset of SetPrimes 0 = {1}
proof
T1: the set of all 1 / Product Sgm X where X is Subset of SetPrimes 0 c= {1}
proof
let x be object;
assume x in the set of all
1 / Product Sgm X where X is Subset of SetPrimes 0; then
consider X being Subset of SetPrimes 0 such that
C1: x = 1 / Product Sgm X;
Sgm X = {} by FINSEQ_3:43;
hence thesis by TARSKI:def 1,C1,RVSUM_1:94;
end;
{1} c=
the set of all 1 / Product Sgm X where X is Subset of SetPrimes 0
proof
let x be object;
assume x in {1}; then
S1: x = 1 / Product Sgm {} by FINSEQ_3:43,RVSUM_1:94,TARSKI:def 1;
{} c= SetPrimes 0;
hence thesis by S1;
end;
hence thesis by T1,TARSKI:2;
end;
hence thesis;
end;
theorem
for p being Prime st p > 2 holds
ReciProducts (p+1) = ReciProducts p
proof
let p be Prime;
assume p > 2; then
p+1 is not prime by P1NotPrime; then
SetPrimes (p+1) = SetPrimes p by PrimesSet;
hence thesis;
end;
theorem
for p being Nat st p+1 is not Prime holds
ReciProducts (p+1) = ReciProducts p
proof
let p be Nat;
assume p+1 is not Prime; then
SetPrimes (p+1) = SetPrimes p by PrimesSet;
hence thesis;
end;
theorem
ReciProducts 1 = { 1 }
proof
the set of all 1 / Product Sgm X where X is Subset of SetPrimes 1 = {1}
proof
T1: the set of all 1 / Product Sgm X where
X is Subset of SetPrimes 1 c= {1}
proof
let x be object;
assume x in the set of all
1 / Product Sgm X where X is Subset of SetPrimes 1; then
consider X being Subset of SetPrimes 1 such that
C1: x = 1 / Product Sgm X;
Sgm X = {} by FINSEQ_3:43,SetPrime1;
hence thesis by TARSKI:def 1,C1,RVSUM_1:94;
end;
{1} c= the set of all 1 / Product Sgm X where X is Subset of SetPrimes 1
proof
let x be object;
assume x in {1}; then
S1: x = 1 / Product Sgm {} by FINSEQ_3:43,RVSUM_1:94,TARSKI:def 1;
{} c= SetPrimes 1;
hence thesis by S1;
end;
hence thesis by T1,TARSKI:2;
end;
hence thesis;
end;
theorem
ReciProducts 2 = { 1 / 2, 1 }
proof
Sgm {2} = <*2*> by FINSEQ_3:44; then
A2: 1 / Product Sgm {2} = 1 / 2 by RVSUM_1:95;
{2} c= SetPrimes 2 by Set2; then
S1: 1 / 2 in ReciProducts 2 by A2;
A4: Product Sgm {} = 1 by RVSUM_1:94,FINSEQ_1:51;
Z1: {} c= SetPrimes 2;
1 / Product Sgm {} = 1 by A4; then
1 in ReciProducts 2 by Z1; then
ZZ: { 1 / 2, 1 } c= ReciProducts 2 by ZFMISC_1:32,S1;
ReciProducts 2 c= {1 / 2, 1}
proof
let x be object;
assume x in ReciProducts 2; then
consider X being Subset of SetPrimes 2 such that
N1: x = 1 / Product Sgm X;
X = {} or X = {2} by ZFMISC_1:33,Set2;
hence thesis by TARSKI:def 2,N1,A4,A2;
end;
hence thesis by TARSKI:2,ZZ;
end;
theorem ReciSubset:
for n be Nat holds
ReciProducts n c= ReciProducts (n+1)
proof
let n be Nat;
let x be object;
n <= n+1 by NAT_1:13; then
A0: SetPrimes n c= SetPrimes (n+1) by XBOOLE_1:26,FINSEQ_1:5;
assume x in ReciProducts n; then
consider X being Subset of SetPrimes n such that
A1: x = 1 / Product Sgm X;
X c= SetPrimes (n+1) by A0;
hence thesis by A1;
end;
theorem
for n be 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}
proof
let n be Nat;
assume
A0: n+1 is Prime;
T1: ReciProducts (n+1) c= ReciProducts n
\/ {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X}
proof
let x be object;
assume x in ReciProducts (n+1); then
consider X being Subset of SetPrimes (n+1) such that
A1: x = 1 / Product Sgm X;
X c= SetPrimes (n+1); then
A2: X c= SetPrimes n \/ {n+1} by A0,PrimesSet2;
per cases;
suppose
n+1 in X; then
x in {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X} by A1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not n+1 in X; then
X c= SetPrimes n by A2,ZFMISC_1:135; then
x in ReciProducts n by A1;
hence thesis by XBOOLE_0:def 3;
end;
end;
ReciProducts n \/
{1 / Product Sgm X where X is Subset of SetPrimes (n+1) : n+1 in X}
c= ReciProducts (n+1)
proof
let x be object;
assume x in
ReciProducts n
\/ {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X}; then
per cases by XBOOLE_0:def 3;
suppose Z1: x in ReciProducts n;
ReciProducts n c= ReciProducts (n+1) by ReciSubset;
hence thesis by Z1;
end;
suppose x in {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X}; then
consider X being Subset of SetPrimes (n+1) such that
B1: x = 1 / Product Sgm X & n+1 in X;
thus thesis by B1;
end;
end;
hence thesis by T1,TARSKI:2;
end;
theorem
for n be 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}
proof
let n be Nat;
assume
A0: n+1 is Prime;
T1: ReciProducts (n+1) c=
{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
let x be object;
assume x in ReciProducts (n+1); then
consider X being Subset of SetPrimes (n+1) such that
A1: x = 1 / Product Sgm X;
X c= SetPrimes (n+1); then
A2: X c= SetPrimes n \/ {n+1} by A0,PrimesSet2;
per cases;
suppose
n+1 in X; then
x in {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X} by A1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
SS: not n+1 in X; then
X c= SetPrimes n by A2,ZFMISC_1:135; then
x in {1 / Product Sgm X where X is Subset of SetPrimes n :
not n+1 in X} by SS,A1;
hence thesis by XBOOLE_0:def 3;
end;
end;
{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}
c= ReciProducts (n+1)
proof
let x be object;
assume x in
{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}; then
per cases by XBOOLE_0:def 3;
suppose x in
{1 / Product Sgm X where X is Subset of SetPrimes n :
not n+1 in X}; then
consider X being Subset of SetPrimes n such that
I1: x = 1 / Product Sgm X & not n+1 in X;
n <= n+1 by NAT_1:13; then
SetPrimes n c= SetPrimes (n+1) by XBOOLE_1:26,FINSEQ_1:5; then
X c= SetPrimes (n+1);
hence thesis by I1;
end;
suppose x in {1 / Product Sgm X where X is Subset of SetPrimes (n+1) :
n+1 in X}; then
consider X being Subset of SetPrimes (n+1) such that
B1: x = 1 / Product Sgm X & n+1 in X;
thus thesis by B1;
end;
end;
hence thesis by T1,TARSKI:2;
end;