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 eqtrid ⊒ ( 𝑛 ∈ β„• β†’ Ξ£ π‘˜ ∈ ( β„™ ∩ ( 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 ⇝