:: The Divergence of the Sum of Prime Reciprocals
:: by Mario Carneiro
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

theorem NatOneLe: :: PRIMRECI:1

for k being Nat holds
( not k is zero iff 1 <= k )

proof end;

theorem LeSqrt: :: PRIMRECI:2

for x, y being Real st x ^2 <= y holds
x <= sqrt y

proof end;

theorem :: PRIMRECI:3

for x, y being Real st x ^2 < y holds
x < sqrt y

proof end;

theorem :: PRIMRECI:4

for x, y being Real st 0 <= x & 0 <= y & x <= y ^2 holds
sqrt x <= y

proof end;

theorem :: PRIMRECI:5

for x, y being Real st 0 <= x & 0 <= y & x < y ^2 holds
sqrt x < y

proof end;

definition

let x be non negative Real;
:: original: [\
redefine func [\x/] -> Nat;
correctness
coherence
[\x/] is Nat;
by INT_1:53;

end;

theorem PartialNonneg: :: PRIMRECI:6

for n being Nat
for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
0 <= (Partial_Sums s) . n

proof end;

theorem PartialLeSum: :: PRIMRECI:7

for i being Nat
for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
(Partial_Sums s) . i <= Sum s

proof end;

theorem SumMono: :: PRIMRECI:8

for i, j being Nat
for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) & i <= j holds
Sum (s ^\ j) <= Sum (s ^\ i)

proof end;

theorem :: PRIMRECI:9

for i being Nat
for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
Sum (s ^\ i) <= Sum s

proof end;

theorem CardSetPrime1: :: PRIMRECI:10

for n being Nat
for p being Prime st p < n holds
(card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n)

proof end;

theorem LePrimeSelf: :: PRIMRECI:11

for n being Nat holds n <= primenumber n

proof end;

theorem LtPrimenumber: :: PRIMRECI:12

for n being Nat
for p being Prime st p < primenumber (n + 1) holds
p <= primenumber n

proof end;

theorem ReciPrimeNotSummable: :: PRIMRECI:13

not ReciPrime is summable

proof end;

registration

cluster ReciPrime -> non summable for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = ReciPrime holds
not b₁ is summable by ReciPrimeNotSummable;

end;