:: Sequences of Prime Reciprocals -- Preliminaries :: by Adam Grabowski :: :: Received March 27, 2018 :: Copyright (c) 2018 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 by INT_1:def 7; 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 by INT_1:62; 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) by NAT_D:3; 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) by NAT_D:3 .= ((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 in NAT & m in NAT by ORDINAL1:def 12; then 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; {} c= Seg 1; then 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;