prmorcht

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

		Ref	Expression
	Hypothesis	prmorcht.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
	Assertion	prmorcht	$⊢ A \in ℕ \to e^{θ (A)} = seq 1 (\times F) (A)$

Proof

Step	Hyp	Ref	Expression
1		prmorcht.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
2		nnre	$⊢ A \in ℕ \to A \in ℝ$
3		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{k \in [0, A] \cap ℙ} \log k$
4	2 3	syl	$⊢ A \in ℕ \to θ (A) = \sum_{k \in [0, A] \cap ℙ} \log k$
5		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
6		ppisval2	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq 1}) \to [0, A] \cap ℙ = (1 \dots ⌊A⌋) \cap ℙ$
7	2 5 6	sylancl	$⊢ A \in ℕ \to [0, A] \cap ℙ = (1 \dots ⌊A⌋) \cap ℙ$
8		nnz	$⊢ A \in ℕ \to A \in ℤ$
9		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
10	8 9	syl	$⊢ A \in ℕ \to ⌊A⌋ = A$
11	10	oveq2d	$⊢ A \in ℕ \to (1 \dots ⌊A⌋) = (1 \dots A)$
12	11	ineq1d	$⊢ A \in ℕ \to (1 \dots ⌊A⌋) \cap ℙ = (1 \dots A) \cap ℙ$
13	7 12	eqtrd	$⊢ A \in ℕ \to [0, A] \cap ℙ = (1 \dots A) \cap ℙ$
14	13	sumeq1d	$⊢ A \in ℕ \to \sum_{k \in [0, A] \cap ℙ} \log k = \sum_{k \in (1 \dots A) \cap ℙ} \log k$
15		inss1	$⊢ (1 \dots A) \cap ℙ \subseteq (1 \dots A)$
16		elinel1	$⊢ k \in ((1 \dots A) \cap ℙ) \to k \in (1 \dots A)$
17		elfznn	$⊢ k \in (1 \dots A) \to k \in ℕ$
18	17	adantl	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to k \in ℕ$
19	18	nnrpd	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to k \in ℝ^{+}$
20	19	relogcld	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to \log k \in ℝ$
21	20	recnd	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to \log k \in ℂ$
22	16 21	sylan2	$⊢ (A \in ℕ \land k \in ((1 \dots A) \cap ℙ)) \to \log k \in ℂ$
23	22	ralrimiva	$⊢ A \in ℕ \to \forall k \in ((1 \dots A) \cap ℙ) \log k \in ℂ$
24		fzfi	$⊢ (1 \dots A) \in Fin$
25	24	olci	$⊢ ((1 \dots A) \subseteq ℤ_{\geq 1} \lor (1 \dots A) \in Fin)$
26		sumss2	$⊢ (((1 \dots A) \cap ℙ \subseteq (1 \dots A) \land \forall k \in ((1 \dots A) \cap ℙ) \log k \in ℂ) \land ((1 \dots A) \subseteq ℤ_{\geq 1} \lor (1 \dots A) \in Fin)) \to \sum_{k \in (1 \dots A) \cap ℙ} \log k = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
27	25 26	mpan2	$⊢ ((1 \dots A) \cap ℙ \subseteq (1 \dots A) \land \forall k \in ((1 \dots A) \cap ℙ) \log k \in ℂ) \to \sum_{k \in (1 \dots A) \cap ℙ} \log k = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
28	15 23 27	sylancr	$⊢ A \in ℕ \to \sum_{k \in (1 \dots A) \cap ℙ} \log k = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
29	14 28	eqtrd	$⊢ A \in ℕ \to \sum_{k \in [0, A] \cap ℙ} \log k = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
30	4 29	eqtrd	$⊢ A \in ℕ \to θ (A) = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
31		elin	$⊢ k \in ((1 \dots A) \cap ℙ) \leftrightarrow (k \in (1 \dots A) \land k \in ℙ)$
32	31	baibr	$⊢ k \in (1 \dots A) \to (k \in ℙ \leftrightarrow k \in ((1 \dots A) \cap ℙ))$
33	32	ifbid	$⊢ k \in (1 \dots A) \to if (k \in ℙ, \log k, 0) = if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
34	33	sumeq2i	$⊢ \sum_{k = 1}^{A} if (k \in ℙ, \log k, 0) = \sum_{k = 1}^{A} if (k \in ((1 \dots A) \cap ℙ), \log k, 0)$
35	30 34	eqtr4di	$⊢ A \in ℕ \to θ (A) = \sum_{k = 1}^{A} if (k \in ℙ, \log k, 0)$
36		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
37		fveq2	$⊢ n = k \to \log n = \log k$
38	36 37	ifbieq1d	$⊢ n = k \to if (n \in ℙ, \log n, 0) = if (k \in ℙ, \log k, 0)$
39		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) = (n \in ℕ ⟼ if (n \in ℙ, \log n, 0))$
40		fvex	$⊢ \log k \in V$
41		0cn	$⊢ 0 \in ℂ$
42	41	elexi	$⊢ 0 \in V$
43	40 42	ifex	$⊢ if (k \in ℙ, \log k, 0) \in V$
44	38 39 43	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k) = if (k \in ℙ, \log k, 0)$
45	18 44	syl	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to (n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k) = if (k \in ℙ, \log k, 0)$
46		elnnuz	$⊢ A \in ℕ \leftrightarrow A \in ℤ_{\geq 1}$
47	46	biimpi	$⊢ A \in ℕ \to A \in ℤ_{\geq 1}$
48		ifcl	$⊢ (\log k \in ℂ \land 0 \in ℂ) \to if (k \in ℙ, \log k, 0) \in ℂ$
49	21 41 48	sylancl	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to if (k \in ℙ, \log k, 0) \in ℂ$
50	45 47 49	fsumser	$⊢ A \in ℕ \to \sum_{k = 1}^{A} if (k \in ℙ, \log k, 0) = seq 1 (+ (n \in ℕ ⟼ if (n \in ℙ, \log n, 0))) (A)$
51	35 50	eqtrd	$⊢ A \in ℕ \to θ (A) = seq 1 (+ (n \in ℕ ⟼ if (n \in ℙ, \log n, 0))) (A)$
52	51	fveq2d	$⊢ A \in ℕ \to e^{θ (A)} = e^{seq 1 (+ (n \in ℕ ⟼ if (n \in ℙ, \log n, 0))) (A)}$
53		addcl	$⊢ (k \in ℂ \land p \in ℂ) \to k + p \in ℂ$
54	53	adantl	$⊢ (A \in ℕ \land (k \in ℂ \land p \in ℂ)) \to k + p \in ℂ$
55	45 49	eqeltrd	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to (n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k) \in ℂ$
56		efadd	$⊢ (k \in ℂ \land p \in ℂ) \to e^{k + p} = e^{k} e^{p}$
57	56	adantl	$⊢ (A \in ℕ \land (k \in ℂ \land p \in ℂ)) \to e^{k + p} = e^{k} e^{p}$
58		1nn	$⊢ 1 \in ℕ$
59		ifcl	$⊢ (k \in ℕ \land 1 \in ℕ) \to if (k \in ℙ, k, 1) \in ℕ$
60	18 58 59	sylancl	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to if (k \in ℙ, k, 1) \in ℕ$
61	60	nnrpd	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to if (k \in ℙ, k, 1) \in ℝ^{+}$
62	61	reeflogd	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to e^{\log if (k \in ℙ, k, 1)} = if (k \in ℙ, k, 1)$
63		fvif	$⊢ \log if (k \in ℙ, k, 1) = if (k \in ℙ, \log k, \log 1)$
64		log1	$⊢ \log 1 = 0$
65		ifeq2	$⊢ \log 1 = 0 \to if (k \in ℙ, \log k, \log 1) = if (k \in ℙ, \log k, 0)$
66	64 65	ax-mp	$⊢ if (k \in ℙ, \log k, \log 1) = if (k \in ℙ, \log k, 0)$
67	63 66	eqtri	$⊢ \log if (k \in ℙ, k, 1) = if (k \in ℙ, \log k, 0)$
68	45 67	eqtr4di	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to (n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k) = \log if (k \in ℙ, k, 1)$
69	68	fveq2d	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to e^{(n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k)} = e^{\log if (k \in ℙ, k, 1)}$
70		id	$⊢ n = k \to n = k$
71	36 70	ifbieq1d	$⊢ n = k \to if (n \in ℙ, n, 1) = if (k \in ℙ, k, 1)$
72		vex	$⊢ k \in V$
73	58	elexi	$⊢ 1 \in V$
74	72 73	ifex	$⊢ if (k \in ℙ, k, 1) \in V$
75	71 1 74	fvmpt	$⊢ k \in ℕ \to F (k) = if (k \in ℙ, k, 1)$
76	18 75	syl	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to F (k) = if (k \in ℙ, k, 1)$
77	62 69 76	3eqtr4d	$⊢ (A \in ℕ \land k \in (1 \dots A)) \to e^{(n \in ℕ ⟼ if (n \in ℙ, \log n, 0)) (k)} = F (k)$
78	54 55 47 57 77	seqhomo	$⊢ A \in ℕ \to e^{seq 1 (+ (n \in ℕ ⟼ if (n \in ℙ, \log n, 0))) (A)} = seq 1 (\times F) (A)$
79	52 78	eqtrd	$⊢ A \in ℕ \to e^{θ (A)} = seq 1 (\times F) (A)$

Metamath Proof Explorer

Theorem prmorcht

Proof