Theorem prmorcht

Description: Relate the primorial (product of the first n primes) to the Chebyshev function. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Hypothesis	prmorcht.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
Assertion	prmorcht	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( θ ‘ 𝐴 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		prmorcht.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
2		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
3		chtval	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑘 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ ℕ → ( θ ‘ 𝐴 ) = Σ 𝑘 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) )
5		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
6		ppisval2	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
7	2 5 6	sylancl	⊢ ( 𝐴 ∈ ℕ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
8		nnz	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
9		flid	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
10	8 9	syl	⊢ ( 𝐴 ∈ ℕ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
11	10	oveq2d	⊢ ( 𝐴 ∈ ℕ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( 1 ... 𝐴 ) )
12	11	ineq1d	⊢ ( 𝐴 ∈ ℕ → ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 1 ... 𝐴 ) ∩ ℙ ) )
13	7 12	eqtrd	⊢ ( 𝐴 ∈ ℕ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 1 ... 𝐴 ) ∩ ℙ ) )
14	13	sumeq1d	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) )
15		inss1	⊢ ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 )
16		elinel1	⊢ ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) → 𝑘 ∈ ( 1 ... 𝐴 ) )
17		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℕ )
18	17	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → 𝑘 ∈ ℕ )
19	18	nnrpd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → 𝑘 ∈ ℝ+ )
20	19	relogcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ 𝑘 ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ 𝑘 ) ∈ ℂ )
22	16 21	sylan2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑘 ) ∈ ℂ )
23	22	ralrimiva	⊢ ( 𝐴 ∈ ℕ → ∀ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) ∈ ℂ )
24		fzfi	⊢ ( 1 ... 𝐴 ) ∈ Fin
25	24	olci	⊢ ( ( 1 ... 𝐴 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝐴 ) ∈ Fin )
26		sumss2	⊢ ( ( ( ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 ) ∧ ∀ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) ∈ ℂ ) ∧ ( ( 1 ... 𝐴 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝐴 ) ∈ Fin ) ) → Σ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
27	25 26	mpan2	⊢ ( ( ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 ) ∧ ∀ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) ∈ ℂ ) → Σ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
28	15 23 27	sylancr	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
29	14 28	eqtrd	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
30	4 29	eqtrd	⊢ ( 𝐴 ∈ ℕ → ( θ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
31		elin	⊢ ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ↔ ( 𝑘 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ℙ ) )
32	31	baibr	⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → ( 𝑘 ∈ ℙ ↔ 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) )
33	32	ifbid	⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) = if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 ) )
34	33	sumeq2i	⊢ Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ 𝑘 ) , 0 )
35	30 34	eqtr4di	⊢ ( 𝐴 ∈ ℕ → ( θ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) )
36		eleq1w	⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
37		fveq2	⊢ ( 𝑛 = 𝑘 → ( log ‘ 𝑛 ) = ( log ‘ 𝑘 ) )
38	36 37	ifbieq1d	⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) )
39		eqid	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) )
40		fvex	⊢ ( log ‘ 𝑘 ) ∈ V
41		0cn	⊢ 0 ∈ ℂ
42	41	elexi	⊢ 0 ∈ V
43	40 42	ifex	⊢ if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) ∈ V
44	38 39 43	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) )
45	18 44	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) )
46		elnnuz	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
47	46	biimpi	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
48		ifcl	⊢ ( ( ( log ‘ 𝑘 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) ∈ ℂ )
49	21 41 48	sylancl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) ∈ ℂ )
50	45 47 49	fsumser	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝐴 ) if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ) ‘ 𝐴 ) )
51	35 50	eqtrd	⊢ ( 𝐴 ∈ ℕ → ( θ ‘ 𝐴 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ) ‘ 𝐴 ) )
52	51	fveq2d	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( θ ‘ 𝐴 ) ) = ( exp ‘ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ) ‘ 𝐴 ) ) )
53		addcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ ) → ( 𝑘 + 𝑝 ) ∈ ℂ )
54	53	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ ) ) → ( 𝑘 + 𝑝 ) ∈ ℂ )
55	45 49	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) ∈ ℂ )
56		efadd	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ ) → ( exp ‘ ( 𝑘 + 𝑝 ) ) = ( ( exp ‘ 𝑘 ) · ( exp ‘ 𝑝 ) ) )
57	56	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ ) ) → ( exp ‘ ( 𝑘 + 𝑝 ) ) = ( ( exp ‘ 𝑘 ) · ( exp ‘ 𝑝 ) ) )
58		1nn	⊢ 1 ∈ ℕ
59		ifcl	⊢ ( ( 𝑘 ∈ ℕ ∧ 1 ∈ ℕ ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
60	18 58 59	sylancl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
61	60	nnrpd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℝ+ )
62	61	reeflogd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( exp ‘ ( log ‘ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
63		fvif	⊢ ( log ‘ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , ( log ‘ 1 ) )
64		log1	⊢ ( log ‘ 1 ) = 0
65		ifeq2	⊢ ( ( log ‘ 1 ) = 0 → if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , ( log ‘ 1 ) ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 ) )
66	64 65	ax-mp	⊢ if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , ( log ‘ 1 ) ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 )
67	63 66	eqtri	⊢ ( log ‘ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) = if ( 𝑘 ∈ ℙ , ( log ‘ 𝑘 ) , 0 )
68	45 67	eqtr4di	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) = ( log ‘ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
69	68	fveq2d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( exp ‘ ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) ) = ( exp ‘ ( log ‘ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) ) )
70		id	⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
71	36 70	ifbieq1d	⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
72		vex	⊢ 𝑘 ∈ V
73	58	elexi	⊢ 1 ∈ V
74	72 73	ifex	⊢ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ V
75	71 1 74	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
76	18 75	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
77	62 69 76	3eqtr4d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( exp ‘ ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
78	54 55 47 57 77	seqhomo	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ) ‘ 𝐴 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝐴 ) )
79	52 78	eqtrd	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( θ ‘ 𝐴 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝐴 ) )