Theorem prmrec 13249

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

Hypothesis

Ref	Expression
prmrec.f	|- F = ( n e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) )

Assertion

Ref	Expression
prmrec	|- -. F e. dom ~~>

Distinct variable group:   k, n

Allowed substitution hints:   F( k, n)

Proof of Theorem prmrec

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2468	. . . . 5 |- ( m = k -> ( m e. Prime <-> k e. Prime ) )
2		oveq2 6052	. . . . 5 |- ( m = k -> ( 1 / m ) = ( 1 / k ) )
3		eqidd 2409	. . . . 5 |- ( m = k -> 0 = 0 )
4	1, 2, 3	ifbieq12d 3725	. . . 4 |- ( m = k -> if ( m e. Prime , ( 1 / m ) , 0 ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
5	4	cbvmptv 4264	. . 3 |- ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) = ( k e. NN |-> if ( k e. Prime , ( 1 / k ) , 0 ) )
6	5	prmreclem6 13248	. 2 |- -. seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) e. dom ~~>
7		inss2 3526	. . . . . . . . 9 |- ( Prime i^i ( 1 ... n ) ) C_ ( 1 ... n )
8	7	sseli 3308	. . . . . . . . . . 11 |- ( k e. ( Prime i^i ( 1 ... n ) ) -> k e. ( 1 ... n ) )
9		elfznn 11040	. . . . . . . . . . 11 |- ( k e. ( 1 ... n ) -> k e. NN )
10		nnrecre 9996	. . . . . . . . . . . 12 |- ( k e. NN -> ( 1 / k ) e. RR )
11	10	recnd 9074	. . . . . . . . . . 11 |- ( k e. NN -> ( 1 / k ) e. CC )
12	8, 9, 11	3syl 19	. . . . . . . . . 10 |- ( k e. ( Prime i^i ( 1 ... n ) ) -> ( 1 / k ) e. CC )
13	12	rgen 2735	. . . . . . . . 9 |- A. k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) e. CC
14	7, 13	pm3.2i 442	. . . . . . . 8 |- ( ( Prime i^i ( 1 ... n ) ) C_ ( 1 ... n ) /\ A. k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) e. CC )
15		fzfi 11270	. . . . . . . . 9 |- ( 1 ... n ) e. Fin
16	15	olci 381	. . . . . . . 8 |- ( ( 1 ... n ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... n ) e. Fin )
17		sumss2 12479	. . . . . . . 8 |- ( ( ( ( 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 ) )
18	14, 16, 17	mp2an 654	. . . . . . 7 |- 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 )
19		elin 3494	. . . . . . . . . 10 |- ( k e. ( Prime i^i ( 1 ... n ) ) <-> ( k e. Prime /\ k e. ( 1 ... n ) ) )
20	19	rbaib 874	. . . . . . . . 9 |- ( k e. ( 1 ... n ) -> ( k e. ( Prime i^i ( 1 ... n ) ) <-> k e. Prime ) )
21	20	ifbid 3721	. . . . . . . 8 |- ( k e. ( 1 ... n ) -> if ( k e. ( Prime i^i ( 1 ... n ) ) , ( 1 / k ) , 0 ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
22	21	sumeq2i 12452	. . . . . . 7 |- 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 )
23	18, 22	eqtri 2428	. . . . . 6 |- sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) = sum_ k e. ( 1 ... n ) if ( k e. Prime , ( 1 / k ) , 0 )
24	9	adantl 453	. . . . . . . 8 |- ( ( n e. NN /\ k e. ( 1 ... n ) ) -> k e. NN )
25		prmnn 13041	. . . . . . . . . . . 12 |- ( k e. Prime -> k e. NN )
26	25, 11	syl 16	. . . . . . . . . . 11 |- ( k e. Prime -> ( 1 / k ) e. CC )
27	26	adantl 453	. . . . . . . . . 10 |- ( ( T. /\ k e. Prime ) -> ( 1 / k ) e. CC )
28		0cn 9044	. . . . . . . . . . 11 |- 0 e. CC
29	28	a1i 11	. . . . . . . . . 10 |- ( ( T. /\ -. k e. Prime ) -> 0 e. CC )
30	27, 29	ifclda 3730	. . . . . . . . 9 |- ( T. -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
31	30	trud 1329	. . . . . . . 8 |- if ( k e. Prime , ( 1 / k ) , 0 ) e. CC
32	5	fvmpt2 5775	. . . . . . . 8 |- ( ( 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 ) )
33	24, 31, 32	sylancl 644	. . . . . . 7 |- ( ( 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 ) )
34		id 20	. . . . . . . 8 |- ( n e. NN -> n e. NN )
35		nnuz 10481	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
36	34, 35	syl6eleq 2498	. . . . . . 7 |- ( n e. NN -> n e. ( ZZ>= ` 1 ) )
37	31	a1i 11	. . . . . . 7 |- ( ( n e. NN /\ k e. ( 1 ... n ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
38	33, 36, 37	fsumser 12483	. . . . . 6 |- ( 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 ) )
39	23, 38	syl5eq 2452	. . . . 5 |- ( 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 ) )
40	39	mpteq2ia 4255	. . . 4 |- ( 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 ) )
41		prmrec.f	. . . 4 |- F = ( n e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) )
42		1z 10271	. . . . . . 7 |- 1 e. ZZ
43		seqfn 11294	. . . . . . 7 |- ( 1 e. ZZ -> seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn ( ZZ>= ` 1 ) )
44	42, 43	ax-mp 8	. . . . . 6 |- seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn ( ZZ>= ` 1 )
45	35	fneq2i 5503	. . . . . 6 |- ( 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 ) )
46	44, 45	mpbir 201	. . . . 5 |- seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) Fn NN
47		dffn5 5735	. . . . 5 |- ( 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 ) ) )
48	46, 47	mpbi 200	. . . 4 |- 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 ) )
49	40, 41, 48	3eqtr4i 2438	. . 3 |- F = seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) )
50	49	eleq1i 2471	. 2 |- ( F e. dom ~~> <-> seq 1 ( + , ( m e. NN |-> if ( m e. Prime , ( 1 / m ) , 0 ) ) ) e. dom ~~> )
51	6, 50	mtbir 291	1 |- -. F e. dom ~~>

Syntax hints:   -. wn 3   \/ wo 358   /\ wa 359   T. wtru 1322   = wceq 1649   e. wcel 1721   A.wral 2670   i^i cin 3283   C_ wss 3284   ifcif 3703   e. cmpt 4230   dom cdm 4841   Fn wfn 5412   ` cfv 5417  (class class class)co 6044   Fincfn 7072   CCcc 8948   0cc0 8950   1c1 8951   + caddc 8953   / cdiv 9637   NNcn 9960   ZZcz 10242   ZZ>=cuz 10448   ...cfz 11003   seq cseq 11282   ~~> cli 12237   sum_csu 12438   Primecprime 13038

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-inf2 7556  ax-cnex 9006  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-mulcom 9014  ax-addass 9015  ax-mulass 9016  ax-distr 9017  ax-i2m1 9018  ax-1ne0 9019  ax-1rid 9020  ax-rnegex 9021  ax-rrecex 9022  ax-cnre 9023  ax-pre-lttri 9024  ax-pre-lttrn 9025  ax-pre-ltadd 9026  ax-pre-mulgt0 9027  ax-pre-sup 9028

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rmo 2678  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-se 4506  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-1st 6312  df-2nd 6313  df-riota 6512  df-recs 6596  df-rdg 6631  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6868  df-map 6983  df-pm 6984  df-en 7073  df-dom 7074  df-sdom 7075  df-fin 7076  df-sup 7408  df-oi 7439  df-card 7786  df-cda 8008  df-pnf 9082  df-mnf 9083  df-xr 9084  df-ltxr 9085  df-le 9086  df-sub 9253  df-neg 9254  df-div 9638  df-nn 9961  df-2 10018  df-3 10019  df-n0 10182  df-z 10243  df-uz 10449  df-q 10535  df-rp 10573  df-fz 11004  df-fzo 11095  df-fl 11161  df-mod 11210  df-seq 11283  df-exp 11342  df-hash 11578  df-cj 11863  df-re 11864  df-im 11865  df-sqr 11999  df-abs 12000  df-clim 12241  df-rlim 12242  df-sum 12439  df-dvds 12812  df-gcd 12966  df-prm 13039  df-pc 13170