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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) )
Assertion prmrec ¬ 𝐹 ∈ dom ⇝

Proof

Step Hyp Ref Expression
1 prmrec.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) )
2 inss2 ⊢ ( ℙ ∩ ( 1 ... 𝑛 ) ) ⊆ ( 1 ... 𝑛 )
3 elinel2 ⊢ ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... 𝑛 ) )
4 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
5 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℂ )
7 3 4 6 3syl ⊢ ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) → ( 1 / 𝑘 ) ∈ ℂ )
8 7 rgen ⊢ ∀ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) ∈ ℂ
9 2 8 pm3.2i ⊢ ( ( ℙ ∩ ( 1 ... 𝑛 ) ) ⊆ ( 1 ... 𝑛 ) ∧ ∀ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) ∈ ℂ )
10 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
11 10 olci ⊢ ( ( 1 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝑛 ) ∈ Fin )
12 sumss2 ⊢ ( ( ( ( ℙ ∩ ( 1 ... 𝑛 ) ) ⊆ ( 1 ... 𝑛 ) ∧ ∀ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) ∈ ℂ ) ∧ ( ( 1 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝑛 ) ∈ Fin ) ) → Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) , ( 1 / 𝑘 ) , 0 ) )
13 9 11 12 mp2an ⊢ Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) , ( 1 / 𝑘 ) , 0 )
14 elin ⊢ ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ↔ ( 𝑘 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) )
15 14 rbaib ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ↔ 𝑘 ∈ ℙ ) )
16 15 ifbid ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → if ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) , ( 1 / 𝑘 ) , 0 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
17 16 sumeq2i ⊢ Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 )
18 13 17 eqtri ⊢ Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 )
19 4 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
20 prmnn ⊢ ( 𝑘 ∈ ℙ → 𝑘 ∈ ℕ )
21 20 6 syl ⊢ ( 𝑘 ∈ ℙ → ( 1 / 𝑘 ) ∈ ℂ )
22 21 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℙ ) → ( 1 / 𝑘 ) ∈ ℂ )
23 0cnd ⊢ ( ( ⊤ ∧ ¬ 𝑘 ∈ ℙ ) → 0 ∈ ℂ )
24 22 23 ifclda ⊢ ( ⊤ → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
25 24 mptru ⊢ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ
26 eleq1w ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
27 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 1 / 𝑚 ) = ( 1 / 𝑘 ) )
28 26 27 ifbieq1d ⊢ ( 𝑚 = 𝑘 → if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
29 28 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) = ( 𝑘 ∈ ℕ ↦ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
30 29 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ ) → ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
31 19 25 30 sylancl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
32 id ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
33 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
34 32 33 eleqtrdi ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
35 25 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
36 31 34 35 fsumser ⊢ ( 𝑛 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ‘ 𝑛 ) )
37 18 36 syl5eq ⊢ ( 𝑛 ∈ ℕ → Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ‘ 𝑛 ) )
38 37 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( ℙ ∩ ( 1 ... 𝑛 ) ) ( 1 / 𝑘 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ‘ 𝑛 ) )
39 1z ⊢ 1 ∈ ℤ
40 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ( ℤ≥ ‘ 1 ) )
41 39 40 ax-mp ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ( ℤ≥ ‘ 1 )
42 33 fneq2i ⊢ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ( ℤ≥ ‘ 1 ) )
43 41 42 mpbir ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ℕ
44 dffn5 ⊢ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ‘ 𝑛 ) ) )
45 43 44 mpbi ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ‘ 𝑛 ) )
46 38 1 45 3eqtr4i ⊢ 𝐹 = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) )
47 29 prmreclem6 ⊢ ¬ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) ) ) ∈ dom ⇝
48 46 47 eqneltri ⊢ ¬ 𝐹 ∈ dom ⇝