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 … n 1 k
Assertion prmrec ⊢ ¬ F ∈ dom ⁡ ⇝

Proof

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