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 e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) )
Assertion prmrec 
|- -. F e. dom ~~>

Proof

Step Hyp Ref Expression
1 prmrec.f 
 |-  F = ( n e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) )
2 inss2 
 |-  ( Prime i^i ( 1 ... n ) ) C_ ( 1 ... n )
3 elinel2 
 |-  ( k e. ( Prime i^i ( 1 ... n ) ) -> k e. ( 1 ... n ) )
4 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
5 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
6 5 recnd 
 |-  ( k e. NN -> ( 1 / k ) e. CC )
7 3 4 6 3syl 
 |-  ( k e. ( Prime i^i ( 1 ... n ) ) -> ( 1 / k ) e. CC )
8 7 rgen 
 |-  A. k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) e. CC
9 2 8 pm3.2i 
 |-  ( ( Prime i^i ( 1 ... n ) ) C_ ( 1 ... n ) /\ A. k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) e. CC )
10 fzfi 
 |-  ( 1 ... n ) e. Fin
11 10 olci 
 |-  ( ( 1 ... n ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... n ) e. Fin )
12 sumss2 
 |-  ( ( ( ( Prime i^i ( 1 ... n ) ) C_ ( 1 ... n ) /\ A. k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) e. CC ) /\ ( ( 1 ... n ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... n ) e. Fin ) ) -> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) = sum_ k e. ( 1 ... n ) if ( k e. ( Prime i^i ( 1 ... n ) ) , ( 1 / k ) , 0 ) )
13 9 11 12 mp2an 
 |-  sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) = sum_ k e. ( 1 ... n ) if ( k e. ( Prime i^i ( 1 ... n ) ) , ( 1 / k ) , 0 )
14 elin 
 |-  ( k e. ( Prime i^i ( 1 ... n ) ) <-> ( k e. Prime /\ k e. ( 1 ... n ) ) )
15 14 rbaib 
 |-  ( k e. ( 1 ... n ) -> ( k e. ( Prime i^i ( 1 ... n ) ) <-> k e. Prime ) )
16 15 ifbid 
 |-  ( k e. ( 1 ... n ) -> if ( k e. ( Prime i^i ( 1 ... n ) ) , ( 1 / k ) , 0 ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
17 16 sumeq2i 
 |-  sum_ k e. ( 1 ... n ) if ( k e. ( Prime i^i ( 1 ... n ) ) , ( 1 / k ) , 0 ) = sum_ k e. ( 1 ... n ) if ( k e. Prime , ( 1 / k ) , 0 )
18 13 17 eqtri 
 |-  sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) = sum_ k e. ( 1 ... n ) if ( k e. Prime , ( 1 / k ) , 0 )
19 4 adantl 
 |-  ( ( n e. NN /\ k e. ( 1 ... n ) ) -> k e. NN )
20 prmnn 
 |-  ( k e. Prime -> k e. NN )
21 20 6 syl 
 |-  ( k e. Prime -> ( 1 / k ) e. CC )
22 21 adantl 
 |-  ( ( T. /\ k e. Prime ) -> ( 1 / k ) e. CC )
23 0cnd 
 |-  ( ( T. /\ -. k e. Prime ) -> 0 e. CC )
24 22 23 ifclda 
 |-  ( T. -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
25 24 mptru 
 |-  if ( k e. Prime , ( 1 / k ) , 0 ) e. CC
26 eleq1w 
 |-  ( m = k -> ( m e. Prime <-> k e. Prime ) )
27 oveq2 
 |-  ( m = k -> ( 1 / m ) = ( 1 / k ) )
28 26 27 ifbieq1d 
 |-  ( m = k -> if ( m e. Prime , ( 1 / m ) , 0 ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
29 28 cbvmptv 
 |-  ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) = ( k e. NN |-> if ( k e. Prime , ( 1 / k ) , 0 ) )
30 29 fvmpt2 
 |-  ( ( k e. NN /\ if ( k e. Prime , ( 1 / k ) , 0 ) e. CC ) -> ( ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ` k ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
31 19 25 30 sylancl 
 |-  ( ( n e. NN /\ k e. ( 1 ... n ) ) -> ( ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ` k ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
32 id 
 |-  ( n e. NN -> n e. NN )
33 nnuz 
 |-  NN = ( ZZ>= ` 1 )
34 32 33 eleqtrdi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
35 25 a1i 
 |-  ( ( n e. NN /\ k e. ( 1 ... n ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
36 31 34 35 fsumser 
 |-  ( n e. NN -> sum_ k e. ( 1 ... n ) if ( k e. Prime , ( 1 / k ) , 0 ) = ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) ` n ) )
37 18 36 eqtrid 
 |-  ( n e. NN -> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) = ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) ` n ) )
38 37 mpteq2ia 
 |-  ( n e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) ) = ( n e. NN |-> ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) ` n ) )
39 1z 
 |-  1 e. ZZ
40 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn ( ZZ>= ` 1 ) )
41 39 40 ax-mp 
 |-  seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn ( ZZ>= ` 1 )
42 33 fneq2i 
 |-  ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn NN <-> seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn ( ZZ>= ` 1 ) )
43 41 42 mpbir 
 |-  seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn NN
44 dffn5 
 |-  ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn NN <-> seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) = ( n e. NN |-> ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) ` n ) ) )
45 43 44 mpbi 
 |-  seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) = ( n e. NN |-> ( seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) ` n ) )
46 38 1 45 3eqtr4i 
 |-  F = seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) )
47 29 prmreclem6 
 |-  -. seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) e. dom ~~>
48 46 47 eqneltri 
 |-  -. F e. dom ~~>