Metamath Proof Explorer

Theorem efchtcl

Description: The Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 7-Apr-2016)

		Ref	Expression
	Assertion	efchtcl	$⊢ A \in ℝ \to e^{θ (A)} \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
2	1	fveq2d	$⊢ A \in ℝ \to e^{θ (A)} = e^{\sum_{p \in [0, A] \cap ℙ} \log p}$
3		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
4		simpr	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
5	4	elin2d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
6		prmnn	$⊢ p \in ℙ \to p \in ℕ$
7	5 6	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
8	7	nnrpd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
9	8	relogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
10	8	reeflogd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to e^{\log p} = p$
11	10 7	eqeltrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to e^{\log p} \in ℕ$
12	3 9 11	efnnfsumcl	$⊢ A \in ℝ \to e^{\sum_{p \in [0, A] \cap ℙ} \log p} \in ℕ$
13	2 12	eqeltrd	$⊢ A \in ℝ \to e^{θ (A)} \in ℕ$