Metamath Proof Explorer

Theorem prmrec

Description: The sum of the reciprocals of the primes diverges. Theorem 1.13 in ApostolNT p. 18. This is the "second" proof at http://en.wikipedia.org/wiki/Prime_harmonic_series , attributed to Paul Erdős. This is Metamath 100 proof #81. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis prmrec.f ⊢F=n∈ℕ⟼∑k∈ℙ∩1…n1k
Assertion prmrec ⊢¬F∈dom⁡⇝

Proof

Step Hyp Ref Expression
1 prmrec.f ⊢F=n∈ℕ⟼∑k∈ℙ∩1…n1k
2 inss2 ⊢ℙ∩1…n⊆1…n
3 elinel2 ⊢k∈ℙ∩1…n→k∈1…n
4 elfznn ⊢k∈1…n→k∈ℕ
5 nnrecre ⊢k∈ℕ→1k∈ℝ
6 5 recnd ⊢k∈ℕ→1k∈ℂ
7 3 4 6 3syl ⊢k∈ℙ∩1…n→1k∈ℂ
8 7 rgen ⊢∀k∈ℙ∩1…n1k∈ℂ
9 2 8 pm3.2i ⊢ℙ∩1…n⊆1…n∧∀k∈ℙ∩1…n1k∈ℂ
10 fzfi ⊢1…n∈Fin
11 10 olci ⊢1…n⊆ℤ≥1∨1…n∈Fin
12 sumss2 ⊢ℙ∩1…n⊆1…n∧∀k∈ℙ∩1…n1k∈ℂ∧1…n⊆ℤ≥1∨1…n∈Fin→∑k∈ℙ∩1…n1k=∑k=1nifk∈ℙ∩1…n1k0
13 9 11 12 mp2an ⊢∑k∈ℙ∩1…n1k=∑k=1nifk∈ℙ∩1…n1k0
14 elin ⊢k∈ℙ∩1…n↔k∈ℙ∧k∈1…n
15 14 rbaib ⊢k∈1…n→k∈ℙ∩1…n↔k∈ℙ
16 15 ifbid ⊢k∈1…n→ifk∈ℙ∩1…n1k0=ifk∈ℙ1k0
17 16 sumeq2i ⊢∑k=1nifk∈ℙ∩1…n1k0=∑k=1nifk∈ℙ1k0
18 13 17 eqtri ⊢∑k∈ℙ∩1…n1k=∑k=1nifk∈ℙ1k0
19 4 adantl ⊢n∈ℕ∧k∈1…n→k∈ℕ
20 prmnn ⊢k∈ℙ→k∈ℕ
21 20 6 syl ⊢k∈ℙ→1k∈ℂ
22 21 adantl ⊢⊤∧k∈ℙ→1k∈ℂ
23 0cnd ⊢⊤∧¬k∈ℙ→0∈ℂ
24 22 23 ifclda ⊢⊤→ifk∈ℙ1k0∈ℂ
25 24 mptru ⊢ifk∈ℙ1k0∈ℂ
26 eleq1w ⊢m=k→m∈ℙ↔k∈ℙ
27 oveq2 ⊢m=k→1m=1k
28 26 27 ifbieq1d ⊢m=k→ifm∈ℙ1m0=ifk∈ℙ1k0
29 28 cbvmptv ⊢m∈ℕ⟼ifm∈ℙ1m0=k∈ℕ⟼ifk∈ℙ1k0
30 29 fvmpt2 ⊢k∈ℕ∧ifk∈ℙ1k0∈ℂ→m∈ℕ⟼ifm∈ℙ1m0⁡k=ifk∈ℙ1k0
31 19 25 30 sylancl ⊢n∈ℕ∧k∈1…n→m∈ℕ⟼ifm∈ℙ1m0⁡k=ifk∈ℙ1k0
32 id ⊢n∈ℕ→n∈ℕ
33 nnuz ⊢ℕ=ℤ≥1
34 32 33 eleqtrdi ⊢n∈ℕ→n∈ℤ≥1
35 25 a1i ⊢n∈ℕ∧k∈1…n→ifk∈ℙ1k0∈ℂ
36 31 34 35 fsumser ⊢n∈ℕ→∑k=1nifk∈ℙ1k0=seq1+m∈ℕ⟼ifm∈ℙ1m0⁡n
37 18 36 eqtrid ⊢n∈ℕ→∑k∈ℙ∩1…n1k=seq1+m∈ℕ⟼ifm∈ℙ1m0⁡n
38 37 mpteq2ia ⊢n∈ℕ⟼∑k∈ℙ∩1…n1k=n∈ℕ⟼seq1+m∈ℕ⟼ifm∈ℙ1m0⁡n
39 1z ⊢1∈ℤ
40 seqfn ⊢1∈ℤ→seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℤ≥1
41 39 40 ax-mp ⊢seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℤ≥1
42 33 fneq2i ⊢seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℕ↔seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℤ≥1
43 41 42 mpbir ⊢seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℕ
44 dffn5 ⊢seq1+m∈ℕ⟼ifm∈ℙ1m0Fnℕ↔seq1+m∈ℕ⟼ifm∈ℙ1m0=n∈ℕ⟼seq1+m∈ℕ⟼ifm∈ℙ1m0⁡n
45 43 44 mpbi ⊢seq1+m∈ℕ⟼ifm∈ℙ1m0=n∈ℕ⟼seq1+m∈ℕ⟼ifm∈ℙ1m0⁡n
46 38 1 45 3eqtr4i ⊢F=seq1+m∈ℕ⟼ifm∈ℙ1m0
47 29 prmreclem6 ⊢¬seq1+m∈ℕ⟼ifm∈ℙ1m0∈dom⁡⇝
48 46 47 eqneltri ⊢¬F∈dom⁡⇝